lustrec / src / tools / seal / seal_export.ml @ d75eb6f1
History  View  Annotate  Download (3.66 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  
9 
let verbose = false 
10 

11 
let to_lustre m sw_init sw_step init_out update_out = 
12 
let orig_nd = m.mname in 
13 
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in 
14 
let vl = (* memories *) 
15 
match sw_init with 
16 
 [] > assert false 
17 
 (gl, up)::_ > List.map (fun (v,_) > v) up 
18 
in 
19 
(* let add_pre sw = 
20 
List.map (fun (gl, up) > 
21 
List.map (fun (g,b) > 
22 
if not b then 
23 
assert false (* should be guaranted by constrauction *) 
24 
else 
25 
add_pre_expr vl g) gl, 
26 
List.map (fun (v,e) > add_pre_expr vl e) up 
27 
) sw 
28 
in 
29 
*) 
30 

31 
let rec process_sw f_e sw = 
32 
let process_branch g_opt up = 
33 
let el = List.map (fun (v,e) > f_e e) up in 
34 
let loc = (List.hd el).expr_loc in 
35 
let new_e = Corelang.mkexpr loc (Expr_tuple el) in 
36 
match g_opt with 
37 
None > None, new_e, loc 
38 
 Some g > 
39 
let g = f_e g in 
40 
let ee = Corelang.mkeexpr loc g in 
41 
let new_e = if verbose then 
42 
{new_e with 
43 
expr_annot = 
44 
Some ({annots = [["seal";"guards"],ee]; 
45 
annot_loc = loc})} else new_e 
46 
in 
47 
Some g, new_e, loc 
48 
in 
49 
match sw with 
50 
 [] > assert false 
51 
 [g_opt,up] > ((* last case, no need to guard it *) 
52 
let _, up_e, _ = process_branch g_opt up in 
53 
up_e 
54 
) 
55 
 (g_opt,up)::tl > 
56 
let g_opt, up_e, loc = process_branch g_opt up in 
57 
match g_opt with 
58 
 None > assert false (* How could this happen anyway ? *) 
59 
 Some g > 
60 
let tl_e = process_sw f_e tl in 
61 
Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
62 
in 
63 

64 
let e_init = process_sw (fun x > x) sw_init in 
65 
let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in 
66 
let e_init_out = process_sw (fun x > x) init_out in 
67 
let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in 
68 
let loc = Location.dummy_loc in 
69 
{ copy_nd with 
70 
node_id = copy_nd.node_id ^ "_seal"; 
71 
node_locals = m.mmemory; 
72 
node_stmts = [Eq 
73 
{ eq_loc = loc; 
74 
eq_lhs = vl; 
75 
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step)) 
76 
}; 
77 
Eq 
78 
{ eq_loc = loc; 
79 
eq_lhs = List.map (fun v > v.var_id) copy_nd.node_outputs; 
80 
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out)) 
81 
}; 
82 
] 
83 
(* 
84 
il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes 
85  
86  
87 
ecrire une expression 
88  
89 
(mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2) 
90  
91 
Il faut aussi calculer la fonction de sortie 
92  
93 
out1,out2 = if garde1 then e1,e2 else if garde2 .... 
94 
*) 
95 
} 