lustrec / src / tools / seal / seal_export.ml @ 03c767b1
History  View  Annotate  Download (4.88 KB)
1 
(* Multiple export channels for switched systems: 

2 
 lustre 
3 
 matlab 
4 
 text 
5 
*) 
6 
open Lustre_types 
7 
open Machine_code_types 
8 
open Seal_utils 
9  
10 
let verbose = true 
11  
12 
let process_sw vars f_e sw = 
13 
let process_branch g_opt up = 
14 
let el = List.map (fun (v,e) > v, f_e e) up in 
15 
(* Sorting list of elements, according to vars, safety check to 
16 
ensure that no variable is forgotten. *) 
17 
let el, forgotten = List.fold_right (fun v (res, remaining) > 
18 
let vid = v.var_id in 
19 
if List.mem_assoc vid remaining then 
20 
((List.assoc vid remaining)::res), 
21 
(List.remove_assoc vid remaining) 
22 
else ( 
23 
Format.eprintf 
24 
"Looking for variable %s in remaining expressions: [%a]@." 
25 
vid 
26 
(Utils.fprintf_list ~sep:";@ " 
27 
(fun fmt (id,e) > 
28 
Format.fprintf fmt 
29 
"(%s > %a)" 
30 
id 
31 
Printers.pp_expr e)) 
32 
remaining; 
33 
assert false (* Missing variable v in list *) 
34 
) 
35 
) vars ([], el) 
36 
in 
37 
assert (forgotten = []); 
38 
let loc = (List.hd el).expr_loc in 
39 
let new_e = Corelang.mkexpr loc (Expr_tuple el) in 
40 
match g_opt with 
41 
None > None, new_e, loc 
42 
 Some g > 
43 
let g = f_e g in 
44 
let ee = Corelang.mkeexpr loc g in 
45 
let new_e = if verbose then 
46 
{new_e with 
47 
expr_annot = 
48 
Some ({annots = [["seal";"guards"],ee]; 
49 
annot_loc = loc})} else new_e 
50 
in 
51 
Some g, new_e, loc 
52 
in 
53 
let rec process_sw f_e sw = 
54 
match sw with 
55 
 [] > assert false 
56 
 [g_opt,up] > ((* last case, no need to guard it *) 
57 
let _, up_e, _ = process_branch g_opt up in 
58 
up_e 
59 
) 
60 
 (g_opt,up)::tl > 
61 
let g_opt, up_e, loc = process_branch g_opt up in 
62 
match g_opt with 
63 
 None > ( 
64 
Format.eprintf "SEAL issue: process_sw with %a" 
65 
pp_sys sw 
66 
; 
67 
assert false (* How could this happen anyway ? *) 
68 
) 
69 
 Some g > 
70 
let tl_e = process_sw f_e tl in 
71 
Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
72 
in 
73 
process_sw f_e sw 
74  
75 

76 
let sw_to_lustre m sw_init sw_step init_out update_out = 
77 
let orig_nd = m.mname in 
78 
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in 
79 
let vl = (* memories *) 
80 
match sw_init with 
81 
 [] > assert false 
82 
 (gl, up)::_ > List.map (fun (v,_) > v) up 
83 
in 
84 
let e_init = process_sw m.mmemory (fun x > x) sw_init in 
85 
let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in 
86 
let e_init_out = process_sw copy_nd.node_outputs (fun x > x) init_out in 
87 
let e_update_out = process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in 
88 
let loc = Location.dummy_loc in 
89 
let new_nd = 
90 
{ copy_nd with 
91 
node_id = copy_nd.node_id ^ "_seal"; 
92 
node_locals = m.mmemory; 
93 
node_stmts = [Eq 
94 
{ eq_loc = loc; 
95 
eq_lhs = vl; 
96 
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step)) 
97 
}; 
98 
Eq 
99 
{ eq_loc = loc; 
100 
eq_lhs = List.map (fun v > v.var_id) copy_nd.node_outputs; 
101 
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out)) 
102 
}; 
103 
]; 
104 
} 
105 
in 
106 
new_nd, orig_nd 
107  
108 

109 
let to_lustre basename prog m sw_init sw_step init_out update_out = 
110 
let loc = Location.dummy_loc in 
111 
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in 
112 
Global.type_env := Typing.type_node !Global.type_env new_node loc; 
113 
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node; 
114  
115 
(* Format.eprintf "%a@." Printers.pp_node new_node; *) 
116  
117 
(* Main output *) 
118 
let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in 
119 
let new_top = 
120 
Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node) 
121 
in 
122 
let out = open_out output_file in 
123 
let fmt = Format.formatter_of_out_channel out in 
124 
Format.fprintf fmt "%a@." Printers.pp_prog [new_top]; 
125  
126 
(* Verif output *) 
127 
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in 
128 
let out_verif = open_out output_file_verif in 
129 
let fmt_verif = Format.formatter_of_out_channel out_verif in 
130 
let check_nd = Lustre_utils.check_eq new_node orig_nd in 
131 
let check_top = 
132 
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) 
133 
in 
134 
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]); 