Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/inliner.ml | ||
---|---|---|
14 | 14 |
open Utils |
15 | 15 |
|
16 | 16 |
(* Local annotations are declared with the following key /inlining/: true *) |
17 |
let keyword = ["inlining"]
|
|
17 |
let keyword = [ "inlining" ]
|
|
18 | 18 |
|
19 |
let is_inline_expr expr = |
|
20 |
match expr.expr_annot with |
|
21 |
| Some ann -> |
|
22 |
List.exists (fun (key, _) -> key = keyword) ann.annots |
|
23 |
| None -> false |
|
19 |
let is_inline_expr expr = |
|
20 |
match expr.expr_annot with |
|
21 |
| Some ann -> |
|
22 |
List.exists (fun (key, _) -> key = keyword) ann.annots |
|
23 |
| None -> |
|
24 |
false |
|
24 | 25 |
|
25 |
let check_node_name id = (fun t -> |
|
26 |
match t.top_decl_desc with |
|
27 |
| Node nd -> nd.node_id = id |
|
28 |
| _ -> false) |
|
26 |
let check_node_name id t = |
|
27 |
match t.top_decl_desc with Node nd -> nd.node_id = id | _ -> false |
|
29 | 28 |
|
30 | 29 |
let is_node_var node v = |
31 |
try |
|
32 |
ignore (Corelang.get_node_var v node); true |
|
33 |
with Not_found -> false |
|
30 |
try |
|
31 |
ignore (Corelang.get_node_var v node); |
|
32 |
true |
|
33 |
with Not_found -> false |
|
34 | 34 |
|
35 | 35 |
(* let rename_expr rename expr = expr_replace_var rename expr *) |
36 |
(* |
|
37 |
let rename_eq rename eq = |
|
38 |
{ eq with |
|
39 |
eq_lhs = List.map rename eq.eq_lhs; |
|
40 |
eq_rhs = rename_expr rename eq.eq_rhs |
|
41 |
} |
|
42 |
*) |
|
43 |
|
|
36 |
(* let rename_eq rename eq = { eq with eq_lhs = List.map rename eq.eq_lhs; |
|
37 |
eq_rhs = rename_expr rename eq.eq_rhs } *) |
|
38 |
|
|
44 | 39 |
let rec add_expr_reset_cond cond expr = |
45 | 40 |
let aux = add_expr_reset_cond cond in |
46 |
let new_desc =
|
|
41 |
let new_desc = |
|
47 | 42 |
match expr.expr_desc with |
48 |
| Expr_const _ |
|
49 |
| Expr_ident _ -> expr.expr_desc |
|
50 |
| Expr_tuple el -> Expr_tuple (List.map aux el) |
|
51 |
| Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e) |
|
52 |
|
|
53 |
| Expr_arrow (e1, e2) -> |
|
43 |
| Expr_const _ | Expr_ident _ -> |
|
44 |
expr.expr_desc |
|
45 |
| Expr_tuple el -> |
|
46 |
Expr_tuple (List.map aux el) |
|
47 |
| Expr_ite (c, t, e) -> |
|
48 |
Expr_ite (aux c, aux t, aux e) |
|
49 |
| Expr_arrow (e1, e2) -> |
|
54 | 50 |
(* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *) |
55 | 51 |
let e1 = aux e1 and e2 = aux e2 in |
56 | 52 |
(* inlining is performed before typing. we can leave the fields free *) |
57 | 53 |
let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in |
58 |
Expr_arrow (e1, new_e2) |
|
59 |
|
|
60 |
| Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *) |
|
61 |
|
|
62 |
| Expr_array el -> Expr_array (List.map aux el) |
|
63 |
| Expr_access (e, dim) -> Expr_access (aux e, dim) |
|
64 |
| Expr_power (e, dim) -> Expr_power (aux e, dim) |
|
65 |
| Expr_pre e -> Expr_pre (aux e) |
|
66 |
| Expr_when (e, id, l) -> Expr_when (aux e, id, l) |
|
67 |
| Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases) |
|
68 |
|
|
69 |
| Expr_appl (id, args, reset_opt) -> |
|
54 |
Expr_arrow (e1, new_e2) |
|
55 |
| Expr_fby _ -> |
|
56 |
assert false (* TODO: deal with fby. This hasn't been much handled yet *) |
|
57 |
| Expr_array el -> |
|
58 |
Expr_array (List.map aux el) |
|
59 |
| Expr_access (e, dim) -> |
|
60 |
Expr_access (aux e, dim) |
|
61 |
| Expr_power (e, dim) -> |
|
62 |
Expr_power (aux e, dim) |
|
63 |
| Expr_pre e -> |
|
64 |
Expr_pre (aux e) |
|
65 |
| Expr_when (e, id, l) -> |
|
66 |
Expr_when (aux e, id, l) |
|
67 |
| Expr_merge (id, cases) -> |
|
68 |
Expr_merge (id, List.map (fun (l, e) -> l, aux e) cases) |
|
69 |
| Expr_appl (id, args, reset_opt) -> |
|
70 | 70 |
(* we "add" cond to the reset field. *) |
71 |
let new_reset = match reset_opt with |
|
72 |
None -> cond |
|
73 |
| Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond'] |
|
71 |
let new_reset = |
|
72 |
match reset_opt with |
|
73 |
| None -> |
|
74 |
cond |
|
75 |
| Some cond' -> |
|
76 |
mkpredef_call cond'.expr_loc "||" [ cond; cond' ] |
|
74 | 77 |
in |
75 | 78 |
Expr_appl (id, args, Some new_reset) |
76 |
|
|
77 |
|
|
78 | 79 |
in |
80 |
|
|
79 | 81 |
{ expr with expr_desc = new_desc } |
80 | 82 |
|
81 | 83 |
let add_eq_reset_cond cond eq = |
82 | 84 |
{ eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs } |
83 |
(* |
|
84 |
let get_static_inputs input_arg_list = |
|
85 |
List.fold_right (fun (vdecl, arg) res -> |
|
86 |
if vdecl.var_dec_const |
|
87 |
then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res |
|
88 |
else res) |
|
89 |
input_arg_list [] |
|
90 |
|
|
91 |
let get_carrier_inputs input_arg_list = |
|
92 |
List.fold_right (fun (vdecl, arg) res -> |
|
93 |
if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc |
|
94 |
then (vdecl.var_id, ident_of_expr arg) :: res |
|
95 |
else res) |
|
96 |
input_arg_list [] |
|
97 |
*) |
|
98 |
(* |
|
99 |
expr, locals', eqs = inline_call id args' reset locals node nodes |
|
100 |
|
|
101 |
We select the called node equations and variables. |
|
102 |
renamed_inputs = args |
|
85 |
(* let get_static_inputs input_arg_list = List.fold_right (fun (vdecl, arg) res |
|
86 |
-> if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) |
|
87 |
:: res else res) input_arg_list [] |
|
88 |
|
|
89 |
let get_carrier_inputs input_arg_list = List.fold_right (fun (vdecl, arg) res |
|
90 |
-> if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc then |
|
91 |
(vdecl.var_id, ident_of_expr arg) :: res else res) input_arg_list [] *) |
|
92 |
(* expr, locals', eqs = inline_call id args' reset locals node nodes |
|
93 |
|
|
94 |
We select the called node equations and variables. renamed_inputs = args |
|
103 | 95 |
renamed_eqs |
104 | 96 |
|
105 |
the resulting expression is tuple_of_renamed_outputs |
|
106 |
|
|
107 |
TODO: convert the specification/annotation/assert and inject them |
|
108 |
*) |
|
97 |
the resulting expression is tuple_of_renamed_outputs |
|
98 |
|
|
99 |
TODO: convert the specification/annotation/assert and inject them *) |
|
109 | 100 |
|
110 | 101 |
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr, |
111 |
locals, eqs, asserts) |
|
112 |
*) |
|
102 |
locals, eqs, asserts) *) |
|
113 | 103 |
let inline_call node loc uid args reset locals caller = |
114 | 104 |
let rename v = |
115 |
if v = tag_true || v = tag_false || not (is_node_var node v) then v else |
|
116 |
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) |
|
105 |
if v = tag_true || v = tag_false || not (is_node_var node v) then v |
|
106 |
else |
|
107 |
Corelang.mk_new_node_name caller |
|
108 |
(Format.sprintf "%s_%i_%s" node.node_id uid v) |
|
117 | 109 |
in |
118 | 110 |
let eqs, auts = get_node_eqs node in |
119 | 111 |
let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in |
120 | 112 |
let auts' = List.map (rename_aut (fun x -> x) rename) auts in |
121 |
let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in |
|
122 |
let static_inputs, dynamic_inputs = List.partition (fun (vdecl, _) -> vdecl.var_dec_const) input_arg_list in |
|
123 |
let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in |
|
124 |
let carrier_inputs, _ = List.partition (fun (vdecl, _) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in |
|
125 |
let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in |
|
113 |
let input_arg_list = |
|
114 |
List.combine node.node_inputs (Corelang.expr_list_of_expr args) |
|
115 |
in |
|
116 |
let static_inputs, dynamic_inputs = |
|
117 |
List.partition (fun (vdecl, _) -> vdecl.var_dec_const) input_arg_list |
|
118 |
in |
|
119 |
let static_inputs = |
|
120 |
List.map |
|
121 |
(fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) |
|
122 |
static_inputs |
|
123 |
in |
|
124 |
let carrier_inputs, _ = |
|
125 |
List.partition |
|
126 |
(fun (vdecl, _) -> |
|
127 |
Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) |
|
128 |
dynamic_inputs |
|
129 |
in |
|
130 |
let carrier_inputs = |
|
131 |
List.map |
|
132 |
(fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) |
|
133 |
carrier_inputs |
|
134 |
in |
|
126 | 135 |
let rename_static v = |
127 |
try |
|
128 |
snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
|
|
129 |
with Not_found -> Dimension.mkdim_ident loc v in
|
|
136 |
try snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
|
|
137 |
with Not_found -> Dimension.mkdim_ident loc v
|
|
138 |
in |
|
130 | 139 |
let rename_carrier v = |
131 |
try |
|
132 |
snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
|
|
133 |
with Not_found -> v in
|
|
140 |
try snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
|
|
141 |
with Not_found -> v
|
|
142 |
in |
|
134 | 143 |
let rename_var v = |
135 | 144 |
let vdecl = |
136 | 145 |
Corelang.mkvar_decl v.var_loc |
137 |
(rename v.var_id, |
|
138 |
{ v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc }, |
|
139 |
{ v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc }, |
|
140 |
v.var_dec_const, |
|
141 |
Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value, |
|
142 |
v.var_parent_nodeid (* we keep the original parent name *) |
|
143 |
) in |
|
144 |
begin |
|
145 |
(* |
|
146 |
(try |
|
147 |
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs); |
|
148 |
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ())) |
|
149 |
with Not_found -> ()); |
|
150 |
(try |
|
151 |
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) |
|
152 |
with Not_found -> ()); |
|
153 |
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*) |
|
154 |
*) |
|
155 |
vdecl |
|
156 |
end |
|
146 |
( rename v.var_id, |
|
147 |
{ |
|
148 |
v.var_dec_type with |
|
149 |
ty_dec_desc = |
|
150 |
Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc; |
|
151 |
}, |
|
152 |
{ |
|
153 |
v.var_dec_clock with |
|
154 |
ck_dec_desc = |
|
155 |
Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc; |
|
156 |
}, |
|
157 |
v.var_dec_const, |
|
158 |
Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value, |
|
159 |
v.var_parent_nodeid (* we keep the original parent name *) ) |
|
160 |
in |
|
161 |
(* (try Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty |
|
162 |
vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id |
|
163 |
static_inputs); Typing.unify vdecl.var_type (Type_predef.type_static |
|
164 |
(List.assoc v.var_id static_inputs) (Types.new_var ())) with Not_found -> |
|
165 |
()); (try Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier |
|
166 |
(List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) with |
|
167 |
Not_found -> ()); (*Format.eprintf "Inliner.inline_call res=%a@." |
|
168 |
Printers.pp_var vdecl;*) *) |
|
169 |
vdecl |
|
157 | 170 |
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) |
158 | 171 |
in |
159 | 172 |
let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in |
160 | 173 |
let outputs' = List.map rename_var node.node_outputs in |
161 | 174 |
let locals' = |
162 |
(List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) |
|
163 |
@ (List.map rename_var node.node_locals) |
|
164 |
in |
|
175 |
List.map |
|
176 |
(fun (vdecl, arg) -> |
|
177 |
let vdecl' = rename_var vdecl in |
|
178 |
{ vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) |
|
179 |
static_inputs |
|
180 |
@ List.map rename_var node.node_locals |
|
181 |
in |
|
165 | 182 |
(* checking we are at the appropriate (early) step: node_checks and |
166 | 183 |
node_gencalls should be empty (not yet assigned) *) |
167 | 184 |
assert (node.node_checks = []); |
168 | 185 |
assert (node.node_gencalls = []); |
169 | 186 |
|
170 | 187 |
(* Expressing reset locally in equations *) |
171 |
let eqs_r' = |
|
172 |
let all_eqs = (List.map (fun eq -> Eq eq) eqs') @ (List.map (fun aut -> Aut aut) auts') in |
|
188 |
let eqs_r' = |
|
189 |
let all_eqs = |
|
190 |
List.map (fun eq -> Eq eq) eqs' @ List.map (fun aut -> Aut aut) auts' |
|
191 |
in |
|
173 | 192 |
match reset with |
174 |
None -> all_eqs |
|
175 |
| Some cond -> ( |
|
176 |
assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *) |
|
193 |
| None -> |
|
194 |
all_eqs |
|
195 |
| Some cond -> |
|
196 |
assert (auts' = []); |
|
197 |
(* TODO: we do not handle properly automaton in case of reset call *) |
|
177 | 198 |
List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs' |
178 |
) |
|
179 |
in |
|
180 |
let assign_inputs = Eq (mkeq loc (List.map (fun v -> v.var_id) inputs', |
|
181 |
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in |
|
182 |
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') |
|
183 | 199 |
in |
184 |
let asserts' = (* We rename variables in assert expressions *) |
|
185 |
List.map |
|
186 |
(fun a -> |
|
187 |
{a with assert_expr = |
|
188 |
let expr = a.assert_expr in |
|
189 |
rename_expr (fun x -> x) rename expr |
|
190 |
}) |
|
191 |
node.node_asserts |
|
200 |
let assign_inputs = |
|
201 |
Eq |
|
202 |
(mkeq loc |
|
203 |
( List.map (fun v -> v.var_id) inputs', |
|
204 |
expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs) )) |
|
192 | 205 |
in |
193 |
let annots' = |
|
194 |
Plugins.inline_annots rename node.node_annot |
|
206 |
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') in |
|
207 |
let asserts' = |
|
208 |
(* We rename variables in assert expressions *) |
|
209 |
List.map |
|
210 |
(fun a -> |
|
211 |
{ |
|
212 |
a with |
|
213 |
assert_expr = |
|
214 |
(let expr = a.assert_expr in |
|
215 |
rename_expr (fun x -> x) rename expr); |
|
216 |
}) |
|
217 |
node.node_asserts |
|
195 | 218 |
in |
196 |
expr, |
|
197 |
inputs'@outputs'@locals'@locals, |
|
198 |
assign_inputs::eqs_r', |
|
199 |
asserts', |
|
200 |
annots' |
|
201 |
|
|
202 |
|
|
219 |
let annots' = Plugins.inline_annots rename node.node_annot in |
|
220 |
( expr, |
|
221 |
inputs' @ outputs' @ locals' @ locals, |
|
222 |
assign_inputs :: eqs_r', |
|
223 |
asserts', |
|
224 |
annots' ) |
|
203 | 225 |
|
204 | 226 |
let inline_table = Hashtbl.create 23 |
205 | 227 |
|
206 |
(* |
|
207 |
new_expr, new_locals, new_eqs = inline_expr expr locals node nodes |
|
208 |
|
|
228 |
(* new_expr, new_locals, new_eqs = inline_expr expr locals node nodes |
|
229 |
|
|
209 | 230 |
Each occurence of a node in nodes in the expr should be replaced by fresh |
210 |
variables and the code of called node instance added to new_eqs |
|
211 |
|
|
212 |
*) |
|
213 |
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes = |
|
214 |
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
|
215 |
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in |
|
216 |
let inline_tuple el = |
|
217 |
List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> |
|
218 |
let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in |
|
219 |
e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots' |
|
220 |
) el ([], locals, [], [], []) |
|
221 |
in |
|
222 |
let inline_pair e1 e2 = |
|
223 |
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in |
|
231 |
variables and the code of called node instance added to new_eqs *) |
|
232 |
let rec inline_expr ?(selection_on_annotation = false) expr locals node nodes = |
|
233 |
let inline_expr = inline_expr ~selection_on_annotation in |
|
234 |
let inline_node = inline_node ~selection_on_annotation in |
|
235 |
let inline_tuple el = |
|
236 |
List.fold_right |
|
237 |
(fun e (el_tail, locals, eqs, asserts, annots) -> |
|
238 |
let e', locals', eqs', asserts', annots' = |
|
239 |
inline_expr e locals node nodes |
|
240 |
in |
|
241 |
e' :: el_tail, locals', eqs' @ eqs, asserts @ asserts', annots @ annots') |
|
242 |
el ([], locals, [], [], []) |
|
243 |
in |
|
244 |
let inline_pair e1 e2 = |
|
245 |
let el', l', eqs', asserts', annots' = inline_tuple [ e1; e2 ] in |
|
224 | 246 |
match el' with |
225 |
| [e1'; e2'] -> e1', e2', l', eqs', asserts', annots' |
|
226 |
| _ -> assert false |
|
247 |
| [ e1'; e2' ] -> |
|
248 |
e1', e2', l', eqs', asserts', annots' |
|
249 |
| _ -> |
|
250 |
assert false |
|
227 | 251 |
in |
228 |
let inline_triple e1 e2 e3 =
|
|
229 |
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
|
|
252 |
let inline_triple e1 e2 e3 = |
|
253 |
let el', l', eqs', asserts', annots' = inline_tuple [ e1; e2; e3 ] in
|
|
230 | 254 |
match el' with |
231 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots' |
|
232 |
| _ -> assert false |
|
255 |
| [ e1'; e2'; e3' ] -> |
|
256 |
e1', e2', e3', l', eqs', asserts', annots' |
|
257 |
| _ -> |
|
258 |
assert false |
|
233 | 259 |
in |
234 |
|
|
260 |
|
|
235 | 261 |
match expr.expr_desc with |
236 | 262 |
| Expr_appl (id, args, reset) -> |
237 |
let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in |
|
238 |
if List.exists (check_node_name id) nodes && (* the current node call is provided |
|
239 |
as arguments nodes *) |
|
240 |
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, |
|
241 |
it is explicitely inlined here *) |
|
242 |
then ( |
|
243 |
(* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *) |
|
244 |
(* The node should be inlined *) |
|
245 |
(* let _ = Format.eprintf "Inlining call to %s@." id in *) |
|
246 |
let called = try List.find (check_node_name id) nodes |
|
247 |
with Not_found -> (assert false) in |
|
248 |
let called = node_of_top called in |
|
249 |
let called' = inline_node called nodes in |
|
250 |
let expr, locals', eqs'', asserts'', annots'' = |
|
251 |
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in |
|
252 |
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots'' |
|
253 |
) |
|
254 |
else |
|
255 |
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
|
256 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, |
|
257 |
locals', |
|
258 |
eqs', |
|
259 |
asserts', |
|
260 |
annots' |
|
261 |
|
|
263 |
let args', locals', eqs', asserts', annots' = |
|
264 |
inline_expr args locals node nodes |
|
265 |
in |
|
266 |
if |
|
267 |
List.exists (check_node_name id) nodes |
|
268 |
&& (* the current node call is provided as arguments nodes *) |
|
269 |
((not selection_on_annotation) || is_inline_expr expr) |
|
270 |
(* and if selection on annotation is activated, it is explicitely inlined |
|
271 |
here *) |
|
272 |
then |
|
273 |
(* Format.eprintf "Inlining call to %s in expression %a@." id |
|
274 |
Printers.pp_expr expr; *) |
|
275 |
(* The node should be inlined *) |
|
276 |
(* let _ = Format.eprintf "Inlining call to %s@." id in *) |
|
277 |
let called = |
|
278 |
try List.find (check_node_name id) nodes |
|
279 |
with Not_found -> assert false |
|
280 |
in |
|
281 |
let called = node_of_top called in |
|
282 |
let called' = inline_node called nodes in |
|
283 |
let expr, locals', eqs'', asserts'', annots'' = |
|
284 |
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node |
|
285 |
in |
|
286 |
expr, locals', eqs' @ eqs'', asserts' @ asserts'', annots' @ annots'' |
|
287 |
else |
|
288 |
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
|
289 |
( { expr with expr_desc = Expr_appl (id, args', reset) }, |
|
290 |
locals', |
|
291 |
eqs', |
|
292 |
asserts', |
|
293 |
annots' ) |
|
262 | 294 |
(* For other cases, we just keep the structure, but convert sub-expressions *) |
263 |
| Expr_const _ |
|
264 |
| Expr_ident _ -> expr, locals, [], [], []
|
|
265 |
| Expr_tuple el ->
|
|
266 |
let el', l', eqs', asserts', annots' = inline_tuple el in
|
|
267 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
|
|
295 |
| Expr_const _ | Expr_ident _ ->
|
|
296 |
expr, locals, [], [], []
|
|
297 |
| Expr_tuple el -> |
|
298 |
let el', l', eqs', asserts', annots' = inline_tuple el in |
|
299 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots' |
|
268 | 300 |
| Expr_ite (g, t, e) -> |
269 |
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
|
|
270 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
|
|
301 |
let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in |
|
302 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots' |
|
271 | 303 |
| Expr_arrow (e1, e2) -> |
272 |
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
|
|
273 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
|
|
304 |
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |
|
305 |
{ expr with expr_desc = Expr_arrow (e1', e2') }, l', eqs', asserts', annots'
|
|
274 | 306 |
| Expr_fby (e1, e2) -> |
275 |
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
|
|
276 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
|
|
307 |
let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |
|
308 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots' |
|
277 | 309 |
| Expr_array el -> |
278 |
let el', l', eqs', asserts', annots' = inline_tuple el in
|
|
279 |
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
|
|
310 |
let el', l', eqs', asserts', annots' = inline_tuple el in |
|
311 |
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots' |
|
280 | 312 |
| Expr_access (e, dim) -> |
281 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
282 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
|
|
313 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
314 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots' |
|
283 | 315 |
| Expr_power (e, dim) -> |
284 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
285 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
|
|
316 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
317 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots' |
|
286 | 318 |
| Expr_pre e -> |
287 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
288 |
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
|
|
319 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
|
|
320 |
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots' |
|
289 | 321 |
| Expr_when (e, id, label) -> |
290 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |
|
291 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots' |
|
322 |
let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |
|
323 |
( { expr with expr_desc = Expr_when (e', id, label) }, |
|
324 |
l', |
|
325 |
eqs', |
|
326 |
asserts', |
|
327 |
annots' ) |
|
292 | 328 |
| Expr_merge (id, branches) -> |
293 |
let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in |
|
294 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
|
295 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots' |
|
296 |
|
|
297 |
and inline_node ?(selection_on_annotation=false) node nodes = |
|
329 |
let el, l', eqs', asserts', annots' = |
|
330 |
inline_tuple (List.map snd branches) |
|
331 |
in |
|
332 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
|
333 |
( { expr with expr_desc = Expr_merge (id, branches') }, |
|
334 |
l', |
|
335 |
eqs', |
|
336 |
asserts', |
|
337 |
annots' ) |
|
338 |
|
|
339 |
and inline_node ?(selection_on_annotation = false) node nodes = |
|
298 | 340 |
try copy_node (Hashtbl.find inline_table node.node_id) |
299 | 341 |
with Not_found -> |
300 |
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
|
|
342 |
let inline_expr = inline_expr ~selection_on_annotation in |
|
301 | 343 |
let eqs, auts = get_node_eqs node in |
302 |
assert (auts = []); (* No inlining of automaton yet. One should visit each |
|
303 |
handler eqs and perform similar computation *) |
|
304 |
let new_locals, stmts, asserts, annots = |
|
305 |
List.fold_left (fun (locals, stmts, asserts, annots) eq -> |
|
306 |
let eq_rhs', locals', new_stmts', asserts', annots' = |
|
307 |
inline_expr eq.eq_rhs locals node nodes |
|
308 |
in |
|
309 |
locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots |
|
310 |
) (node.node_locals, [], node.node_asserts, node.node_annot) eqs |
|
344 |
assert (auts = []); |
|
345 |
(* No inlining of automaton yet. One should visit each handler eqs and |
|
346 |
perform similar computation *) |
|
347 |
let new_locals, stmts, asserts, annots = |
|
348 |
List.fold_left |
|
349 |
(fun (locals, stmts, asserts, annots) eq -> |
|
350 |
let eq_rhs', locals', new_stmts', asserts', annots' = |
|
351 |
inline_expr eq.eq_rhs locals node nodes |
|
352 |
in |
|
353 |
( locals', |
|
354 |
Eq { eq with eq_rhs = eq_rhs' } :: new_stmts' @ stmts, |
|
355 |
asserts' @ asserts, |
|
356 |
annots' @ annots )) |
|
357 |
(node.node_locals, [], node.node_asserts, node.node_annot) |
|
358 |
eqs |
|
311 | 359 |
in |
312 |
let inlined = |
|
313 |
{ node with |
|
314 |
node_locals = new_locals; |
|
315 |
node_stmts = stmts; |
|
316 |
node_asserts = asserts; |
|
317 |
node_annot = annots; |
|
360 |
let inlined = |
|
361 |
{ |
|
362 |
node with |
|
363 |
node_locals = new_locals; |
|
364 |
node_stmts = stmts; |
|
365 |
node_asserts = asserts; |
|
366 |
node_annot = annots; |
|
318 | 367 |
} |
319 | 368 |
in |
320 |
begin |
|
321 |
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) |
|
322 |
Hashtbl.add inline_table node.node_id inlined; |
|
323 |
inlined |
|
324 |
end |
|
369 |
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) |
|
370 |
Hashtbl.add inline_table node.node_id inlined; |
|
371 |
inlined |
|
325 | 372 |
|
326 | 373 |
let inline_all_calls node nodes = |
327 | 374 |
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
328 | 375 |
{ node with top_decl_desc = Node (inline_node nd nodes) } |
329 |
|
|
330 |
|
|
331 |
|
|
332 |
|
|
333 | 376 |
|
334 | 377 |
let witness filename main_name orig inlined (* type_env clock_env *) = |
335 | 378 |
let loc = Location.dummy_loc in |
336 | 379 |
let rename_local_node nodes prefix id = |
337 |
if List.exists (check_node_name id) nodes then |
|
338 |
prefix ^ id |
|
339 |
else |
|
340 |
id |
|
380 |
if List.exists (check_node_name id) nodes then prefix ^ id else id |
|
341 | 381 |
in |
342 |
let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with |
|
343 |
Node nd -> nd | _ -> assert false in |
|
344 |
|
|
382 |
let main_orig_node = |
|
383 |
match (List.find (check_node_name main_name) orig).top_decl_desc with |
|
384 |
| Node nd -> |
|
385 |
nd |
|
386 |
| _ -> |
|
387 |
assert false |
|
388 |
in |
|
389 |
|
|
345 | 390 |
let orig_rename = rename_local_node orig "orig_" in |
346 | 391 |
let inlined_rename = rename_local_node inlined "inlined_" in |
347 |
let identity = (fun x -> x) in |
|
348 |
let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in |
|
349 |
let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in |
|
392 |
let identity x = x in |
|
393 |
let is_node top = |
|
394 |
match top.top_decl_desc with Node _ -> true | _ -> false |
|
395 |
in |
|
396 |
let orig = |
|
397 |
rename_prog orig_rename (* f_node *) identity (* f_var *) identity |
|
398 |
(* f_const *) orig |
|
399 |
in |
|
350 | 400 |
let inlined = rename_prog inlined_rename identity identity inlined in |
351 | 401 |
let nodes_origs, others = List.partition is_node orig in |
352 | 402 |
let nodes_inlined, _ = List.partition is_node inlined in |
353 | 403 |
|
354 |
(* One ok_i boolean variable per output var *)
|
|
404 |
(* One ok_i boolean variable per output var *) |
|
355 | 405 |
let nb_outputs = List.length main_orig_node.node_outputs in |
356 | 406 |
let ok_ident = "OK" in |
357 |
let ok_i = List.map (fun id ->
|
|
358 |
mkvar_decl
|
|
359 |
loc
|
|
360 |
(Format.sprintf "%s_%i" ok_ident id,
|
|
361 |
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
|
|
362 |
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
|
|
363 |
false,
|
|
364 |
None,
|
|
365 |
None
|
|
366 |
) |
|
367 |
) (Utils.enumerate nb_outputs)
|
|
407 |
let ok_i = |
|
408 |
List.map
|
|
409 |
(fun id ->
|
|
410 |
mkvar_decl loc
|
|
411 |
( Format.sprintf "%s_%i" ok_ident id,
|
|
412 |
{ ty_dec_desc = Tydec_bool; ty_dec_loc = loc },
|
|
413 |
{ ck_dec_desc = Ckdec_any; ck_dec_loc = loc },
|
|
414 |
false,
|
|
415 |
None,
|
|
416 |
None ))
|
|
417 |
(Utils.enumerate nb_outputs)
|
|
368 | 418 |
in |
369 | 419 |
|
370 | 420 |
(* OK = ok_1 and ok_2 and ... ok_n-1 *) |
371 |
let ok_output = mkvar_decl |
|
372 |
loc |
|
373 |
(ok_ident, |
|
374 |
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
|
375 |
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
|
376 |
false, |
|
377 |
None, |
|
378 |
None |
|
379 |
) |
|
421 |
let ok_output = |
|
422 |
mkvar_decl loc |
|
423 |
( ok_ident, |
|
424 |
{ ty_dec_desc = Tydec_bool; ty_dec_loc = loc }, |
|
425 |
{ ck_dec_desc = Ckdec_any; ck_dec_loc = loc }, |
|
426 |
false, |
|
427 |
None, |
|
428 |
None ) |
|
380 | 429 |
in |
381 | 430 |
let main_ok_expr = |
382 | 431 |
let mkv x = mkexpr loc (Expr_ident x) in |
383 | 432 |
match ok_i with |
384 |
| [] -> assert false |
|
385 |
| [x] -> mkv x.var_id |
|
386 |
| hd::tl -> |
|
387 |
List.fold_left (fun accu elem -> |
|
388 |
mkpredef_call loc "&&" [mkv elem.var_id; accu] |
|
389 |
) (mkv hd.var_id) tl |
|
433 |
| [] -> |
|
434 |
assert false |
|
435 |
| [ x ] -> |
|
436 |
mkv x.var_id |
|
437 |
| hd :: tl -> |
|
438 |
List.fold_left |
|
439 |
(fun accu elem -> mkpredef_call loc "&&" [ mkv elem.var_id; accu ]) |
|
440 |
(mkv hd.var_id) tl |
|
390 | 441 |
in |
391 | 442 |
|
392 | 443 |
(* Building main node *) |
393 |
|
|
394 | 444 |
let ok_i_eq = |
395 |
{ eq_loc = loc; |
|
445 |
{ |
|
446 |
eq_loc = loc; |
|
396 | 447 |
eq_lhs = List.map (fun v -> v.var_id) ok_i; |
397 |
eq_rhs = |
|
398 |
let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
|
399 |
let call_orig = |
|
400 |
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
|
401 |
let call_inlined = |
|
402 |
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
|
403 |
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
|
404 |
mkexpr loc (Expr_appl ("=", args, None)) |
|
405 |
} in |
|
406 |
let ok_eq = |
|
407 |
{ eq_loc = loc; |
|
408 |
eq_lhs = [ok_ident]; |
|
409 |
eq_rhs = main_ok_expr; |
|
410 |
} in |
|
411 |
let main_node = { |
|
412 |
node_id = "check"; |
|
413 |
node_type = Types.new_var (); |
|
414 |
node_clock = Clocks.new_var true; |
|
415 |
node_inputs = main_orig_node.node_inputs; |
|
416 |
node_outputs = [ok_output]; |
|
417 |
node_locals = ok_i; |
|
418 |
node_gencalls = []; |
|
419 |
node_checks = []; |
|
420 |
node_asserts = []; |
|
421 |
node_stmts = [Eq ok_i_eq; Eq ok_eq]; |
|
422 |
node_dec_stateless = false; |
|
423 |
node_stateless = None; |
|
424 |
node_spec = Some |
|
425 |
(Contract |
|
426 |
(mk_contract_guarantees None |
|
427 |
(mkeexpr loc (mkexpr loc (Expr_ident ok_ident))) |
|
428 |
) |
|
429 |
); |
|
430 |
node_annot = []; |
|
431 |
node_iscontract = true; |
|
448 |
eq_rhs = |
|
449 |
(let inputs = |
|
450 |
expr_of_expr_list loc |
|
451 |
(List.map |
|
452 |
(fun v -> mkexpr loc (Expr_ident v.var_id)) |
|
453 |
main_orig_node.node_inputs) |
|
454 |
in |
|
455 |
let call_orig = |
|
456 |
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) |
|
457 |
in |
|
458 |
let call_inlined = |
|
459 |
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) |
|
460 |
in |
|
461 |
let args = mkexpr loc (Expr_tuple [ call_orig; call_inlined ]) in |
|
462 |
mkexpr loc (Expr_appl ("=", args, None))); |
|
463 |
} |
|
464 |
in |
|
465 |
let ok_eq = { eq_loc = loc; eq_lhs = [ ok_ident ]; eq_rhs = main_ok_expr } in |
|
466 |
let main_node = |
|
467 |
{ |
|
468 |
node_id = "check"; |
|
469 |
node_type = Types.new_var (); |
|
470 |
node_clock = Clocks.new_var true; |
|
471 |
node_inputs = main_orig_node.node_inputs; |
|
472 |
node_outputs = [ ok_output ]; |
|
473 |
node_locals = ok_i; |
|
474 |
node_gencalls = []; |
|
475 |
node_checks = []; |
|
476 |
node_asserts = []; |
|
477 |
node_stmts = [ Eq ok_i_eq; Eq ok_eq ]; |
|
478 |
node_dec_stateless = false; |
|
479 |
node_stateless = None; |
|
480 |
node_spec = |
|
481 |
Some |
|
482 |
(Contract |
|
483 |
(mk_contract_guarantees None |
|
484 |
(mkeexpr loc (mkexpr loc (Expr_ident ok_ident))))); |
|
485 |
node_annot = []; |
|
486 |
node_iscontract = true; |
|
432 | 487 |
} |
433 | 488 |
in |
434 |
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in |
|
435 |
let new_prog = others@nodes_origs@nodes_inlined@main in |
|
436 |
(* |
|
437 |
let _ = Typing.type_prog type_env new_prog in |
|
438 |
let _ = Clock_calculus.clock_prog clock_env new_prog in |
|
439 |
*) |
|
440 |
|
|
441 |
let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |
|
489 |
let main = |
|
490 |
[ |
|
491 |
{ |
|
492 |
top_decl_desc = Node main_node; |
|
493 |
top_decl_loc = loc; |
|
494 |
top_decl_owner = filename; |
|
495 |
top_decl_itf = false; |
|
496 |
}; |
|
497 |
] |
|
498 |
in |
|
499 |
let new_prog = others @ nodes_origs @ nodes_inlined @ main in |
|
500 |
|
|
501 |
(* let _ = Typing.type_prog type_env new_prog in let _ = |
|
502 |
Clock_calculus.clock_prog clock_env new_prog in *) |
|
503 |
let witness_file = |
|
504 |
Options_management.get_witness_dir filename ^ "/" ^ "inliner_witness.lus" |
|
505 |
in |
|
442 | 506 |
let witness_out = open_out witness_file in |
443 | 507 |
let witness_fmt = Format.formatter_of_out_channel witness_out in |
444 |
begin |
|
445 |
List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i); |
|
446 |
Format.fprintf witness_fmt |
|
447 |
"(* Generated lustre file to check validity of inlining process *)@."; |
|
448 |
Printers.pp_prog witness_fmt new_prog; |
|
449 |
Format.fprintf witness_fmt "@."; |
|
450 |
() |
|
451 |
end (* xx *) |
|
508 |
List.iter |
|
509 |
(fun vdecl -> |
|
510 |
Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) |
|
511 |
(ok_output :: ok_i); |
|
512 |
Format.fprintf witness_fmt |
|
513 |
"(* Generated lustre file to check validity of inlining process *)@."; |
|
514 |
Printers.pp_prog witness_fmt new_prog; |
|
515 |
Format.fprintf witness_fmt "@."; |
|
516 |
() |
|
517 |
(* xx *) |
|
452 | 518 |
|
453 | 519 |
let global_inline prog (*type_env clock_env*) = |
454 | 520 |
(* We select the main node desc *) |
455 | 521 |
let main_node, other_nodes, _ = |
456 | 522 |
List.fold_right |
457 |
(fun top (main_opt, nodes, others) -> |
|
458 |
match top.top_decl_desc with |
|
459 |
| Node nd when nd.node_id = !Options.main_node -> |
|
460 |
Some top, nodes, others |
|
461 |
| Node _ -> main_opt, top::nodes, others |
|
462 |
| _ -> main_opt, nodes, top::others) |
|
463 |
prog (None, [], []) |
|
523 |
(fun top (main_opt, nodes, others) -> |
|
524 |
match top.top_decl_desc with |
|
525 |
| Node nd when nd.node_id = !Options.main_node -> |
|
526 |
Some top, nodes, others |
|
527 |
| Node _ -> |
|
528 |
main_opt, top :: nodes, others |
|
529 |
| _ -> |
|
530 |
main_opt, nodes, top :: others) |
|
531 |
prog (None, [], []) |
|
464 | 532 |
in |
465 | 533 |
|
466 | 534 |
(* Recursively each call of a node in the top node is replaced *) |
467 | 535 |
let main_node = Utils.desome main_node in |
468 | 536 |
let main_node' = inline_all_calls main_node other_nodes in |
469 |
let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
|
|
470 |
(* Code snippet from unstable branch. May be used when reactivating witnesses.
|
|
471 |
let res = main_node'::other_tops in
|
|
472 |
if !Options.witnesses then (
|
|
473 |
witness
|
|
474 |
basename
|
|
475 |
(match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false)
|
|
476 |
prog res type_env clock_env
|
|
477 |
);
|
|
478 |
*) |
|
537 |
let res = |
|
538 |
List.map
|
|
539 |
(fun top ->
|
|
540 |
if check_node_name !Options.main_node top then main_node' else top)
|
|
541 |
prog
|
|
542 |
in
|
|
543 |
(* Code snippet from unstable branch. May be used when reactivating witnesses.
|
|
544 |
let res = main_node'::other_tops in if !Options.witnesses then ( witness
|
|
545 |
basename (match main_node.top_decl_desc with Node nd -> nd.node_id | _ ->
|
|
546 |
assert false) prog res type_env clock_env ); *)
|
|
479 | 547 |
res |
480 | 548 |
|
481 | 549 |
let pp_inline_calls fmt prog = |
482 | 550 |
let local_anns = Annotations.get_expr_annotations keyword in |
483 |
let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |
|
551 |
let nodes_with_anns = |
|
552 |
List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns |
|
553 |
in |
|
484 | 554 |
Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]" |
485 |
(fprintf_list ~sep:"" |
|
486 |
(fun fmt top -> |
|
487 |
match top.top_decl_desc with |
|
488 |
| Node nd when ISet.mem nd.node_id nodes_with_anns -> |
|
489 |
Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " |
|
490 |
nd.node_id |
|
491 |
(fprintf_list ~sep:"@ " (fun fmt tag -> Format.fprintf fmt "%i" tag)) |
|
492 |
(List.fold_left |
|
493 |
(fun accu (id, tag) -> if id = nd.node_id then tag::accu else accu) |
|
494 |
[] |
|
495 |
local_anns |
|
496 |
) |
|
497 |
(* | Node nd -> Format.fprintf fmt "%s: no inline annotations" nd.node_id *) |
|
498 |
| _ -> () |
|
499 |
)) |
|
555 |
(fprintf_list ~sep:"" (fun fmt top -> |
|
556 |
match top.top_decl_desc with |
|
557 |
| Node nd when ISet.mem nd.node_id nodes_with_anns -> |
|
558 |
Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " nd.node_id |
|
559 |
(fprintf_list ~sep:"@ " (fun fmt tag -> |
|
560 |
Format.fprintf fmt "%i" tag)) |
|
561 |
(List.fold_left |
|
562 |
(fun accu (id, tag) -> |
|
563 |
if id = nd.node_id then tag :: accu else accu) |
|
564 |
[] local_anns) |
|
565 |
(* | Node nd -> Format.fprintf fmt "%s: no inline annotations" |
|
566 |
nd.node_id *) |
|
567 |
| _ -> |
|
568 |
())) |
|
500 | 569 |
prog |
501 |
|
|
502 |
|
|
570 |
|
|
503 | 571 |
let local_inline prog (* type_env clock_env *) = |
504 | 572 |
Log.report ~level:2 (fun fmt -> Format.fprintf fmt ".. @[<v 2>Inlining@,"); |
505 | 573 |
let local_anns = Annotations.get_expr_annotations keyword in |
506 |
let prog =
|
|
574 |
let prog = |
|
507 | 575 |
if local_anns != [] then ( |
508 |
let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |
|
509 |
ISet.iter (fun node_id -> Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Node %s has local expression annotations@ " node_id)) |
|
510 |
nodes_with_anns; |
|
511 |
List.fold_right (fun top accu -> |
|
512 |
( match top.top_decl_desc with |
|
513 |
| Node nd when ISet.mem nd.node_id nodes_with_anns -> |
|
514 |
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "[local inline] Processing node %s@ " nd.node_id); |
|
515 |
let inlined_node = inline_node ~selection_on_annotation:true nd prog in |
|
516 |
(* Format.eprintf "Before inline@.%a@.After:@.%a@." *) |
|
517 |
(* Printers.pp_node nd *) |
|
518 |
(* Printers.pp_node inlined_node; *) |
|
519 |
{ top with top_decl_desc = Node inlined_node } |
|
520 |
|
|
521 |
| _ -> top |
|
522 |
)::accu) prog [] |
|
523 |
|
|
524 |
) |
|
576 |
let nodes_with_anns = |
|
577 |
List.fold_left |
|
578 |
(fun accu (k, _) -> ISet.add k accu) |
|
579 |
ISet.empty local_anns |
|
580 |
in |
|
581 |
ISet.iter |
|
582 |
(fun node_id -> |
|
583 |
Log.report ~level:2 (fun fmt -> |
|
584 |
Format.fprintf fmt "Node %s has local expression annotations@ " |
|
585 |
node_id)) |
|
586 |
nodes_with_anns; |
|
587 |
List.fold_right |
|
588 |
(fun top accu -> |
|
589 |
(match top.top_decl_desc with |
|
590 |
| Node nd when ISet.mem nd.node_id nodes_with_anns -> |
|
591 |
Log.report ~level:2 (fun fmt -> |
|
592 |
Format.fprintf fmt "[local inline] Processing node %s@ " |
|
593 |
nd.node_id); |
|
594 |
let inlined_node = |
|
595 |
inline_node ~selection_on_annotation:true nd prog |
|
596 |
in |
|
597 |
(* Format.eprintf "Before inline@.%a@.After:@.%a@." *) |
|
598 |
(* Printers.pp_node nd *) |
|
599 |
(* Printers.pp_node inlined_node; *) |
|
600 |
{ top with top_decl_desc = Node inlined_node } |
|
601 |
| _ -> |
|
602 |
top) |
|
603 |
:: accu) |
|
604 |
prog []) |
|
525 | 605 |
else ( |
526 |
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "No local inline information!@ ");
|
|
527 |
prog
|
|
528 |
) |
|
606 |
Log.report ~level:2 (fun fmt -> |
|
607 |
Format.fprintf fmt "No local inline information!@ ");
|
|
608 |
prog)
|
|
529 | 609 |
in |
530 | 610 |
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@,"); |
531 | 611 |
prog |
Also available in: Unified diff
reformatting