Revision 3b2bd83d src/normalization.ml
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