1
|
(* Multiple export channels for switched systems: - lustre - matlab - text *)
|
2
|
open Lustre_types
|
3
|
open Machine_code_types
|
4
|
open Seal_utils
|
5
|
|
6
|
let verbose = true
|
7
|
|
8
|
let process_sw vars f_e sw =
|
9
|
let process_branch g_opt up =
|
10
|
let el = List.map (fun (v, e) -> v, f_e e) up in
|
11
|
(* Sorting list of elements, according to vars, safety check to ensure that
|
12
|
no variable is forgotten. *)
|
13
|
let el, forgotten =
|
14
|
List.fold_right
|
15
|
(fun v (res, remaining) ->
|
16
|
let vid = v.var_id in
|
17
|
if List.mem_assoc vid remaining then
|
18
|
List.assoc vid remaining :: res, List.remove_assoc vid remaining
|
19
|
else (
|
20
|
Format.eprintf
|
21
|
"Looking for variable %s in remaining expressions: [%a]@." vid
|
22
|
(Utils.fprintf_list ~sep:";@ " (fun fmt (id, e) ->
|
23
|
Format.fprintf fmt "(%s -> %a)" id Printers.pp_expr e))
|
24
|
remaining;
|
25
|
assert false (* Missing variable v in list *)))
|
26
|
vars ([], el)
|
27
|
in
|
28
|
assert (forgotten = []);
|
29
|
let loc = (List.hd el).expr_loc in
|
30
|
let new_e = Corelang.mkexpr loc (Expr_tuple el) in
|
31
|
match g_opt with
|
32
|
| None ->
|
33
|
None, new_e, loc
|
34
|
| Some g ->
|
35
|
let g = f_e g in
|
36
|
let ee = Corelang.mkeexpr loc g in
|
37
|
let new_e =
|
38
|
if verbose then
|
39
|
{
|
40
|
new_e with
|
41
|
expr_annot =
|
42
|
Some { annots = [ [ "seal"; "guards" ], ee ]; annot_loc = loc };
|
43
|
}
|
44
|
else new_e
|
45
|
in
|
46
|
Some g, new_e, loc
|
47
|
in
|
48
|
let rec process_sw f_e sw =
|
49
|
match sw with
|
50
|
| [] ->
|
51
|
assert false
|
52
|
| [ (g_opt, up) ] ->
|
53
|
(* last case, no need to guard it *)
|
54
|
let _, up_e, _ = process_branch g_opt up in
|
55
|
up_e
|
56
|
| (g_opt, up) :: tl -> (
|
57
|
let g_opt, up_e, loc = process_branch g_opt up in
|
58
|
match g_opt with
|
59
|
| None ->
|
60
|
Format.eprintf "SEAL issue: process_sw with %a"
|
61
|
(pp_sys Printers.pp_expr) sw;
|
62
|
assert false (* How could this happen anyway ? *)
|
63
|
| Some g ->
|
64
|
let tl_e = process_sw f_e tl in
|
65
|
Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)))
|
66
|
in
|
67
|
process_sw f_e sw
|
68
|
|
69
|
let sw_to_lustre m sw_init sw_step init_out update_out =
|
70
|
let orig_nd = m.mname in
|
71
|
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
|
72
|
let vl =
|
73
|
(* vl are memories *)
|
74
|
match sw_init with
|
75
|
| [] ->
|
76
|
[] (* the system is stateless. Returning an empty list shall do the job *)
|
77
|
| (_, up) :: _ ->
|
78
|
List.map (fun (v, _) -> v) up
|
79
|
in
|
80
|
let loc = Location.dummy_loc in
|
81
|
let mem_eq =
|
82
|
if m.mmemory = [] then []
|
83
|
else
|
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
|
[
|
87
|
Eq
|
88
|
{
|
89
|
eq_loc = loc;
|
90
|
eq_lhs = vl;
|
91
|
eq_rhs = Corelang.mkexpr loc (Expr_arrow (e_init, e_step));
|
92
|
};
|
93
|
]
|
94
|
in
|
95
|
let output_eq =
|
96
|
let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
|
97
|
let e_update_out =
|
98
|
process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out
|
99
|
in
|
100
|
[
|
101
|
Eq
|
102
|
{
|
103
|
eq_loc = loc;
|
104
|
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;
|
105
|
eq_rhs = Corelang.mkexpr loc (Expr_arrow (e_init_out, e_update_out));
|
106
|
};
|
107
|
]
|
108
|
in
|
109
|
let new_nd =
|
110
|
{
|
111
|
copy_nd with
|
112
|
node_id = copy_nd.node_id ^ "_seal";
|
113
|
node_locals = m.mmemory;
|
114
|
node_stmts = mem_eq @ output_eq;
|
115
|
}
|
116
|
in
|
117
|
new_nd, orig_nd
|
118
|
|
119
|
let funsw_to_lustre m update_out =
|
120
|
let orig_nd = m.mname in
|
121
|
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
|
122
|
let output_eq =
|
123
|
let e_update_out =
|
124
|
process_sw copy_nd.node_outputs (fun x -> x) update_out
|
125
|
in
|
126
|
[
|
127
|
Eq
|
128
|
{
|
129
|
eq_loc = Location.dummy_loc;
|
130
|
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;
|
131
|
eq_rhs = e_update_out;
|
132
|
};
|
133
|
]
|
134
|
in
|
135
|
let new_nd =
|
136
|
{
|
137
|
copy_nd with
|
138
|
node_id = copy_nd.node_id ^ "_seal";
|
139
|
node_locals = [];
|
140
|
node_stmts = output_eq;
|
141
|
}
|
142
|
in
|
143
|
new_nd, orig_nd
|
144
|
|
145
|
let to_lustre basename prog new_node orig_node =
|
146
|
let loc = Location.dummy_loc in
|
147
|
Global.type_env := Typing.type_node !Global.type_env new_node loc;
|
148
|
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
|
149
|
|
150
|
(* Format.eprintf "%a@." Printers.pp_node new_node; *)
|
151
|
|
152
|
(* Main output *)
|
153
|
let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
|
154
|
let new_top =
|
155
|
Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
|
156
|
in
|
157
|
let out = open_out output_file in
|
158
|
let fmt = Format.formatter_of_out_channel out in
|
159
|
Format.fprintf fmt "%a@." Printers.pp_prog [ new_top ];
|
160
|
|
161
|
(* Verif output *)
|
162
|
let output_file_verif =
|
163
|
!Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus"
|
164
|
in
|
165
|
let out_verif = open_out output_file_verif in
|
166
|
let fmt_verif = Format.formatter_of_out_channel out_verif in
|
167
|
let check_nd = Lustre_utils.check_eq new_node orig_node in
|
168
|
let check_top =
|
169
|
Corelang.mktop_decl Location.dummy_loc output_file_verif false
|
170
|
(Node check_nd)
|
171
|
in
|
172
|
Format.fprintf fmt_verif "%a@." Printers.pp_prog
|
173
|
(prog @ [ new_top; check_top ])
|
174
|
|
175
|
let node_to_lustre basename prog m sw_init sw_step init_out update_out =
|
176
|
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
|
177
|
to_lustre basename prog new_node orig_nd
|
178
|
|
179
|
let fun_to_lustre basename prog m update_out =
|
180
|
let new_node, orig_nd = funsw_to_lustre m update_out in
|
181
|
to_lustre basename prog new_node orig_nd
|