Skip to content
Snippets Groups Projects
Commit 9c654082 authored by Pierre Loic Garoche's avatar Pierre Loic Garoche
Browse files

[lustresf] work in progress. Added global env with initial values

parent f4050bef
No related branches found
No related tags found
No related merge requests found
......@@ -122,8 +122,8 @@ sig
val pp_cond : Format.formatter -> t -> unit
end
module Condition =
module Condition =
struct
type t =
| Quote of base_condition_t
......@@ -155,3 +155,8 @@ struct
end
let _ = (module Condition : ConditionType)
module GlobalVarDef =
struct
type t = {variable: LustreSpec.var_decl; init_val: LustreSpec.expr}
end
......@@ -39,7 +39,7 @@ type 'prog_t src_components_t =
| Junction of junction_name_t * transitions_t
| SFFunction of 'prog_t
type prog_t = Program of state_name_t * prog_t src_components_t list * LustreSpec.var_decl list
type prog_t = Program of state_name_t * prog_t src_components_t list * (LustreSpec.var_decl * LustreSpec.expr) list
type scope_t = Constant | Input | Local | Output | Parameter
......@@ -159,7 +159,7 @@ struct
Format.fprintf fmt "Main node name: %s@ %a@ %a@"
name
(pp_src pp_sffunction) component_list
pp_vars vars
pp_vars (List.map fst vars)
let pp_scope fmt src =
Format.fprintf fmt (match src with
......
......@@ -129,25 +129,31 @@ let json_parse _ file pp =
end) in
let module Sem = CPS.Semantics (T) (Model) in
let prog = Sem.code_gen modularmode in
let header = List.map Corelang.mktop [
(LustreSpec.Open (false,"lustrec_math"));
(LustreSpec.Open (false,"conv"));
(LustreSpec.Open (true,"locallib"));
]
in
let prog =header@prog in
Options.print_dec_types := true;
Format.printf "%a@." Printers.pp_prog prog;
(* Format.printf "%a@." Printers.pp_prog prog; *)
let auto_file = "sf_gen_test_auto.lus" in (* Could be changed *)
let auto_out = open_out auto_file in
let auto_fmt = Format.formatter_of_out_channel auto_out in
Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
let prog = (LustreSpec.Open ("math",false))::prog
Format.eprintf "Print initial lustre model with automaton in sf_gen_test_auto.lus@.";
let prog, deps = Compiler_stages.stage1 prog "" "" in
Format.printf "%a@." Printers.pp_prog prog;
(* Format.printf "%a@." Printers.pp_prog prog; *)
let noauto_file = "sf_gen_test_noauto.lus" in (* Could be changed *)
let noauto_out = open_out noauto_file in
let noauto_fmt = Format.formatter_of_out_channel noauto_out in
Format.fprintf noauto_fmt "%a@." Printers.pp_prog prog
Format.fprintf noauto_fmt "%a@." Printers.pp_prog prog;
Format.eprintf "Print expanded lustre model in sf_gen_test_noauto.lus@.";
()
with Parse.Error (l, err) -> Format.eprintf "Parse error at loc %a : %a@.@?" Location.pp_loc l Parse.pp_error err
......
......@@ -3,7 +3,13 @@ open SF
let name = "simple"
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
let condition x = condition {
expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true));
cinputs = [];
coutputs = [];
cvariables = [];
}
let action _ = no_action
let model : prog_t =
......
......@@ -5,8 +5,12 @@ open SF
let verbose = false
let actionv x = no_action (*TODO if verbose then action x else no_action*)
let action x = no_action (* TODO *)
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
let condition x = condition {
expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true));
cinputs = [];
coutputs = [];
cvariables = [];
}
let name = "stopwatch"
let model =
......@@ -250,8 +254,12 @@ let model =
int_typ, (* type *)
Corelang.dummy_clock_dec, (* clock *)
false, (* not a constant *)
None (* no default value *)
)
None, (* no default value *)
None (* no parent known *)
),
(* Default value is zero *)
Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (LustreSpec.Const_int 0))
)
["cent";
"sec";
......
......@@ -8,10 +8,10 @@ struct
module Prog =
struct
let init, defs, state_vars =
let init, defs, state_vars, globals =
let Program (init, defs, globals) = M.model in
let state_vars = SF.states M.model in
init, defs, state_vars
init, defs, state_vars, globals
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *)
end
......
......@@ -7,7 +7,8 @@ let ff = Format.fprintf
module LustrePrinter (
Vars : sig
val state_vars : ActiveStates.Vars.t
val global_vars : LustreSpec.var_decl list
val global_vars : GlobalVarDef.t list
end) : TransformerType =
struct
include TransformerStub
......@@ -53,7 +54,7 @@ struct
let loc = Location.dummy_loc in
Corelang.mkvar_decl
loc
(name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None)
(name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None, None (*"__no_parent__" *))
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ
let state_vars_to_vdecl_list ?(prefix="") vars =
......@@ -115,7 +116,7 @@ struct
LustreSpec.ty_dec_loc = Location.dummy_loc;
}
let event_var = mkvar "event" event_type
let event_var = mkvar "event" event_type
let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13
......@@ -327,13 +328,15 @@ struct
let (vars', tr') = tr "sin_" "sout_" in
pp_name call args;
let funname = Format.flush_str_formatter () in
let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
let node =
Corelang.mktop (
LustreSpec.Node {LustreSpec.node_id = funname;
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
node_inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars;
node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
node_inputs = inputs;
node_outputs = outputs;
node_locals = mk_locals vars'; (* TODO: add global vars *)
node_gencalls = [];
node_checks = [];
......@@ -346,14 +349,30 @@ struct
)
in
[node]
(* TODO
C'est pas evident.
Il faut faire les choses suivantes:
- rajouter dans un ensemble les variables manipulées localement
- on doit comprendre comment les variables globales sont injectées dans le modele final:
- le node principal doit uniquement les afficher. Il peut les initialiser avec les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.
- elles peuvent/doivent etre dans input et output de ce node thetacallD
*)
let mk_main_loop () =
(* let loc = Location.dummy_loc in *)
let call_stmt =
(* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
let init = mkexpr
(LustreSpec.Expr_tuple (List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars)))
let init =
let init_state_false =
List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in
let init_globals =
List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars in
mkexpr (LustreSpec.Expr_tuple (init_state_false @ init_globals))
in
let args = (Corelang.expr_of_vdecl event_var)::
(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
......@@ -363,13 +382,16 @@ struct
let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
in
let inputs = List.map Corelang.copy_var_decl [event_var] in
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
(* TODO add the globals as sout_data_x entry values *)
let node_principal =
Corelang.mktop (
LustreSpec.Node {LustreSpec.node_id = "principal_loop";
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
node_inputs = List.map Corelang.copy_var_decl [event_var];
node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
node_inputs = inputs;
node_outputs = outputs;
node_locals = []; (* TODO: add global vars *)
node_gencalls = [];
node_checks = [];
......@@ -381,7 +403,7 @@ struct
node_annot = []}
)
in
node_principal
node_principal
let mkprincipal tr =
......
......@@ -63,7 +63,9 @@ let _ =
| GenLus ->
let module Model = (val model) in
let state_vars = Datatype.SF.states Model.model in
let global_vars = Datatype.SF.global_vars Model.model in
let global_vars =
List.map (fun (v,e) -> {Basetypes.GlobalVarDef.variable = v; init_val = e;})
(Datatype.SF.global_vars Model.model) in
let module T = CPS_lustre_generator.LustrePrinter (struct
let state_vars = state_vars
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment