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 = true
|
10
|
|
11
|
let sw_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
|
let new_nd =
|
70
|
{ copy_nd with
|
71
|
node_id = copy_nd.node_id ^ "_seal";
|
72
|
node_locals = m.mmemory;
|
73
|
node_stmts = [Eq
|
74
|
{ eq_loc = loc;
|
75
|
eq_lhs = vl;
|
76
|
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
|
77
|
};
|
78
|
Eq
|
79
|
{ eq_loc = loc;
|
80
|
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;
|
81
|
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
|
82
|
};
|
83
|
];
|
84
|
(*node_spec = Some (Contract contract);*)
|
85
|
|
86
|
(*
|
87
|
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
|
88
|
|
89
|
|
90
|
ecrire une expression
|
91
|
|
92
|
(mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2)
|
93
|
|
94
|
Il faut aussi calculer la fonction de sortie
|
95
|
|
96
|
out1,out2 = if garde1 then e1,e2 else if garde2 ....
|
97
|
*)
|
98
|
}
|
99
|
in
|
100
|
new_nd, orig_nd
|
101
|
|
102
|
|
103
|
let to_lustre basename prog m sw_init sw_step init_out update_out =
|
104
|
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
|
105
|
|
106
|
(* Format.eprintf "%a@." Printers.pp_node new_node; *)
|
107
|
|
108
|
(* Main output *)
|
109
|
let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
|
110
|
let new_top =
|
111
|
Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
|
112
|
in
|
113
|
let out = open_out output_file in
|
114
|
let fmt = Format.formatter_of_out_channel out in
|
115
|
Format.fprintf fmt "%a@." Printers.pp_prog [new_top];
|
116
|
|
117
|
(* Verif output *)
|
118
|
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
|
119
|
let out_verif = open_out output_file_verif in
|
120
|
let fmt_verif = Format.formatter_of_out_channel out_verif in
|
121
|
let check_nd = Lustre_utils.check_eq new_node orig_nd in
|
122
|
let check_top =
|
123
|
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
|
124
|
in
|
125
|
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]);
|