Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/tools/seal/seal_export.ml  

1 
(* Multiple export channels for switched systems: 

2 
 lustre 

3 
 matlab 

4 
 text 

5 
*) 

1 
(* Multiple export channels for switched systems:  lustre  matlab  text *) 

6  2 
open Lustre_types 
7  3 
open Machine_code_types 
8  4 
open Seal_utils 
...  ...  
11  7  
12  8 
let process_sw vars f_e sw = 
13  9 
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) 

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) 

36  27 
in 
37  28 
assert (forgotten = []); 
38  29 
let loc = (List.hd el).expr_loc in 
39  30 
let new_e = Corelang.mkexpr loc (Expr_tuple el) in 
40  31 
match g_opt with 
41 
None > None, new_e, loc 

32 
 None > 

33 
None, new_e, loc 

42  34 
 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 

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 

52  47 
in 
53 
let rec process_sw f_e sw =


48 
let rec process_sw f_e sw = 

54  49 
match sw with 
55 
 [] > assert false 

56 
 [g_opt,up] > ((* last case, no need to guard it *) 

50 
 [] > 

51 
assert false 

52 
 [ (g_opt, up) ] > 

53 
(* last case, no need to guard it *) 

57  54 
let _, up_e, _ = process_branch g_opt up in 
58  55 
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 Printers.pp_expr) 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)) 

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

72  66 
in 
73  67 
process_sw f_e sw 
74  68  
75 


76  69 
let sw_to_lustre m sw_init sw_step init_out update_out = 
77  70 
let orig_nd = m.mname in 
78  71 
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in 
79 
let vl = (* vl are memories *) 

72 
let vl = 

73 
(* vl are memories *) 

80  74 
match sw_init with 
81 
 [] > [] (* the system is stateless. Returning an empty list 

82 
shall do the job *) 

83 


84 
 (_, up)::_ > 

85 
List.map (fun (v,_) > v) up 

75 
 [] > 

76 
[] (* the system is stateless. Returning an empty list shall do the job *) 

77 
 (_, up) :: _ > 

78 
List.map (fun (v, _) > v) up 

86  79 
in 
87  80 
let loc = Location.dummy_loc in 
88  81 
let mem_eq = 
89 
if m.mmemory = [] then 

90 
[] 

82 
if m.mmemory = [] then [] 

91  83 
else 
92  84 
let e_init = process_sw m.mmemory (fun x > x) sw_init in 
93  85 
let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in 
94 
[Eq 

95 
{ eq_loc = loc; 

96 
eq_lhs = vl; 

97 
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step)) 

98 
}] 

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 
] 

99  94 
in 
100  95 
let output_eq = 
101  96 
let e_init_out = process_sw copy_nd.node_outputs (fun x > x) init_out in 
102 
let e_update_out = process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in 

103 
[ 

97 
let e_update_out = 

98 
process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out 

99 
in 

100 
[ 

104  101 
Eq 
105 
{ eq_loc = loc; 

106 
eq_lhs = List.map (fun v > v.var_id) copy_nd.node_outputs; 

107 
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out)) 

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)); 

108  106 
}; 
109  107 
] 
110  108 
in 
111  109 
let new_nd = 
112 
{ copy_nd with 

110 
{ 

111 
copy_nd with 

113  112 
node_id = copy_nd.node_id ^ "_seal"; 
114  113 
node_locals = m.mmemory; 
115  114 
node_stmts = mem_eq @ output_eq; 
...  ...  
117  116 
in 
118  117 
new_nd, orig_nd 
119  118  
120 


121  119 
let funsw_to_lustre m update_out = 
122  120 
let orig_nd = m.mname in 
123  121 
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in 
124  122 
let output_eq = 
125 
let e_update_out = process_sw copy_nd.node_outputs (fun x > x) update_out in 

126 
[ 

123 
let e_update_out = 

124 
process_sw copy_nd.node_outputs (fun x > x) update_out 

125 
in 

126 
[ 

127  127 
Eq 
128 
{ eq_loc = Location.dummy_loc; 

129 
eq_lhs = List.map (fun v > v.var_id) copy_nd.node_outputs; 

130 
eq_rhs = e_update_out 

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; 

131  132 
}; 
132  133 
] 
133  134 
in 
134  135 
let new_nd = 
135 
{ copy_nd with 

136 
{ 

137 
copy_nd with 

136  138 
node_id = copy_nd.node_id ^ "_seal"; 
137  139 
node_locals = []; 
138  140 
node_stmts = output_eq; 
139  141 
} 
140  142 
in 
141  143 
new_nd, orig_nd 
142 


143 


144  144  
145  145 
let to_lustre basename prog new_node orig_node = 
146  146 
let loc = Location.dummy_loc in 
...  ...  
156  156 
in 
157  157 
let out = open_out output_file in 
158  158 
let fmt = Format.formatter_of_out_channel out in 
159 
Format.fprintf fmt "%a@." Printers.pp_prog [new_top];


159 
Format.fprintf fmt "%a@." Printers.pp_prog [ new_top ];


160  160  
161  161 
(* Verif output *) 
162 
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in 

162 
let output_file_verif = 

163 
!Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" 

164 
in 

163  165 
let out_verif = open_out output_file_verif in 
164  166 
let fmt_verif = Format.formatter_of_out_channel out_verif in 
165  167 
let check_nd = Lustre_utils.check_eq new_node orig_node in 
166  168 
let check_top = 
167 
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) 

169 
Corelang.mktop_decl Location.dummy_loc output_file_verif false 

170 
(Node check_nd) 

168  171 
in 
169 
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]) 

170 


172 
Format.fprintf fmt_verif "%a@." Printers.pp_prog 

173 
(prog @ [ new_top; check_top ]) 

174  
171  175 
let node_to_lustre basename prog m sw_init sw_step init_out update_out = 
172  176 
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in 
173  177 
to_lustre basename prog new_node orig_nd 
...  ...  
175  179 
let fun_to_lustre basename prog m update_out = 
176  180 
let new_node, orig_nd = funsw_to_lustre m update_out in 
177  181 
to_lustre basename prog new_node orig_nd 
178 
Also available in: Unified diff
reformatting