Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
src/normalization.ml | ||
---|---|---|
127 | 127 |
|
128 | 128 |
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) |
129 | 129 |
and [opt] is true *) |
130 |
let mk_expr_alias_opt opt node defvars expr = |
|
130 |
let mk_expr_alias_opt opt node (defs, vars) expr = |
|
131 |
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*) |
|
131 | 132 |
match expr.expr_desc with |
132 | 133 |
| Expr_ident alias -> |
133 |
defvars, expr
|
|
134 |
(defs, vars), expr
|
|
134 | 135 |
| _ -> |
135 |
if opt |
|
136 |
then |
|
137 |
mk_expr_alias node defvars expr |
|
138 |
else |
|
139 |
defvars, expr |
|
136 |
match get_expr_alias defs expr with |
|
137 |
| Some eq -> |
|
138 |
let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in |
|
139 |
(defs, vars), replace_expr aliases expr |
|
140 |
| None -> |
|
141 |
if opt |
|
142 |
then |
|
143 |
let new_aliases = |
|
144 |
List.map2 |
|
145 |
(mk_fresh_var node expr.expr_loc) |
|
146 |
(Types.type_list_of_type expr.expr_type) |
|
147 |
(Clocks.clock_list_of_clock expr.expr_clock) in |
|
148 |
let new_def = |
|
149 |
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
|
150 |
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
|
151 |
else |
|
152 |
(defs, vars), expr |
|
140 | 153 |
|
141 | 154 |
(* Create a (normalized) expression from [ref_e], |
142 | 155 |
replacing description with [norm_d], |
... | ... | |
159 | 172 |
) elist (defvars, []) |
160 | 173 |
|
161 | 174 |
let rec normalize_expr ?(alias=true) node offsets defvars expr = |
162 |
(* Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
|
175 |
(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
|
163 | 176 |
match expr.expr_desc with |
164 | 177 |
| Expr_const _ |
165 | 178 |
| Expr_ident _ -> defvars, unfold_offsets expr offsets |
... | ... | |
180 | 193 |
normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in |
181 | 194 |
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) |
182 | 195 |
| Expr_appl (id, args, None) |
183 |
when Basic_library.is_internal_fun id
|
|
196 |
when Basic_library.is_homomorphic_fun id
|
|
184 | 197 |
&& Types.is_array_type expr.expr_type -> |
185 | 198 |
let defvars, norm_args = |
186 | 199 |
normalize_list |
... | ... | |
192 | 205 |
(expr_list_of_expr args) |
193 | 206 |
in |
194 | 207 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
195 |
| Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
|
|
208 |
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
|
|
196 | 209 |
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in |
197 | 210 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) |
198 | 211 |
| Expr_appl (id, args, r) -> |
... | ... | |
203 | 216 |
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in |
204 | 217 |
normalize_expr ~alias:alias node offsets defvars norm_expr |
205 | 218 |
else |
206 |
mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr
|
|
219 |
mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr
|
|
207 | 220 |
| Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) -> (* Here we differ from Colaco paper: arrows are pushed to the top *) |
208 | 221 |
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr) |
209 | 222 |
| Expr_arrow (e1,e2) -> |
... | ... | |
251 | 264 |
hl (defvars, []) |
252 | 265 |
|
253 | 266 |
and normalize_array_expr ?(alias=true) node offsets defvars expr = |
254 |
(* Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
|
267 |
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
|
255 | 268 |
match expr.expr_desc with |
256 | 269 |
| Expr_power (e1, d) when offsets = [] -> |
257 | 270 |
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in |
... | ... | |
262 | 275 |
| Expr_array elist when offsets = [] -> |
263 | 276 |
let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in |
264 | 277 |
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) |
265 |
| Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
|
|
278 |
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
|
|
266 | 279 |
let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in |
267 | 280 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
268 | 281 |
| _ -> normalize_expr ~alias:alias node offsets defvars expr |
... | ... | |
310 | 323 |
defvars', {eq with eq_lhs = lhs' } |
311 | 324 |
|
312 | 325 |
let rec normalize_eq node defvars eq = |
326 |
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) |
|
313 | 327 |
match eq.eq_rhs.expr_desc with |
314 | 328 |
| Expr_pre _ |
315 | 329 |
| Expr_fby _ -> |
... | ... | |
321 | 335 |
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in |
322 | 336 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
323 | 337 |
(norm_eq::defs', vars') |
324 |
| Expr_appl (id, _, None) when Basic_library.is_internal_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
|
|
338 |
| Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
|
|
325 | 339 |
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in |
326 | 340 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
327 | 341 |
(norm_eq::defs', vars') |
... | ... | |
353 | 367 |
List.fold_left ( |
354 | 368 |
fun (vars, def_accu, assert_accu) assert_ -> |
355 | 369 |
let assert_expr = assert_.assert_expr in |
356 |
let (defs, vars'), expr = |
|
357 |
normalize_expr |
|
358 |
~alias:true
|
|
359 |
node |
|
370 |
let (defs, vars'), expr =
|
|
371 |
normalize_expr
|
|
372 |
~alias:false
|
|
373 |
node
|
|
360 | 374 |
[] (* empty offset for arrays *) |
361 | 375 |
([], vars) (* defvar only contains vars *) |
362 | 376 |
assert_expr |
... | ... | |
379 | 393 |
annots = List.map (fun v -> |
380 | 394 |
let eq = |
381 | 395 |
try |
382 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) |
|
383 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
|
396 |
List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) |
|
397 |
with Not_found -> |
|
398 |
( |
|
399 |
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; |
|
400 |
assert false |
|
401 |
) |
|
402 |
in |
|
384 | 403 |
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in |
385 | 404 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
386 | 405 |
(["traceability"], pair) |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04