|
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
|
}
|