Revision 53206908 src/normalization.ml
src/normalization.ml  

95  95  
96  96 
let unfold_offsets e offsets = 
97  97 
let add_offset e d = 
98 
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; 

99 
let res = *) 

98 
(*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*) 

100  99 
{ e with 
101  100 
expr_tag = Utils.new_tag (); 
102  101 
expr_loc = d.Dimension.dim_loc; 
103  102 
expr_type = Types.array_element_type e.expr_type; 
104 
expr_desc = Expr_access (e, d) } 

105 
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) 

106 
in 

103 
expr_desc = Expr_access (e, d) } in 

107  104 
List.fold_left add_offset e offsets 
108  105  
109  106 
(* Create an alias for [expr], if none exists yet *) 
...  ...  
121  118 
(Clocks.clock_list_of_clock expr.expr_clock) in 
122  119 
let new_def = 
123  120 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
124 
in 

125 
(* Format.eprintf "Checking def of alias: %a > %a@." (fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *) 

126 
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr 

121 
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr 

127  122  
128  123 
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) 
129  124 
and [opt] is true *) 
130 
let mk_expr_alias_opt opt node defvars expr = 

125 
let mk_expr_alias_opt opt node (defs, vars) expr = 

126 
(*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  127 
match expr.expr_desc with 
132  128 
 Expr_ident alias > 
133 
defvars, expr


129 
(defs, vars), expr


134  130 
 _ > 
135 
if opt 

136 
then 

137 
mk_expr_alias node defvars expr 

138 
else 

139 
defvars, expr 

131 
match get_expr_alias defs expr with 

132 
 Some eq > 

133 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 

134 
(defs, vars), replace_expr aliases expr 

135 
 None > 

136 
if opt 

137 
then 

138 
let new_aliases = 

139 
List.map2 

140 
(mk_fresh_var node expr.expr_loc) 

141 
(Types.type_list_of_type expr.expr_type) 

142 
(Clocks.clock_list_of_clock expr.expr_clock) in 

143 
let new_def = 

144 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 

145 
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr 

146 
else 

147 
(defs, vars), expr 

140  148  
141  149 
(* Create a (normalized) expression from [ref_e], 
142  150 
replacing description with [norm_d], 
...  ...  
159  167 
) elist (defvars, []) 
160  168  
161  169 
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;*)


170 
(*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  171 
match expr.expr_desc with 
164  172 
 Expr_const _ 
165  173 
 Expr_ident _ > defvars, unfold_offsets expr offsets 
...  ...  
179  187 
let defvars, norm_elist = 
180  188 
normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias) defvars elist in 
181  189 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
182 
 Expr_appl (id, args, None) 

183 
when Basic_library.is_internal_fun id


190 
 Expr_appl (id, args, None)


191 
when Basic_library.is_homomorphic_fun id


184  192 
&& Types.is_array_type expr.expr_type > 
185  193 
let defvars, norm_args = 
186  194 
normalize_list 
...  ...  
192  200 
(expr_list_of_expr args) 
193  201 
in 
194  202 
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 >


203 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr >


196  204 
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in 
197  205 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 
198  206 
 Expr_appl (id, args, r) > 
...  ...  
203  211 
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in 
204  212 
normalize_expr ~alias:alias node offsets defvars norm_expr 
205  213 
else 
206 
mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr


214 
mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr


207  215 
 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  216 
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr) 
209  217 
 Expr_arrow (e1,e2) > 
...  ...  
251  259 
hl (defvars, []) 
252  260  
253  261 
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;*)


262 
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)


255  263 
match expr.expr_desc with 
256  264 
 Expr_power (e1, d) when offsets = [] > 
257  265 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
...  ...  
262  270 
 Expr_array elist when offsets = [] > 
263  271 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
264  272 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 
265 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id >


273 
 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr >


266  274 
let defvars, norm_args = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in 
267  275 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
268  276 
 _ > normalize_expr ~alias:alias node offsets defvars expr 
...  ...  
310  318 
defvars', {eq with eq_lhs = lhs' } 
311  319  
312  320 
let rec normalize_eq node defvars eq = 
321 
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) 

313  322 
match eq.eq_rhs.expr_desc with 
314  323 
 Expr_pre _ 
315  324 
 Expr_fby _ > 
...  ...  
321  330 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
322  331 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
323  332 
(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 >


333 
 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type >


325  334 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
326  335 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
327  336 
(norm_eq::defs', vars') 
...  ...  
353  362 
List.fold_left ( 
354  363 
fun (vars, def_accu, assert_accu) assert_ > 
355  364 
let assert_expr = assert_.assert_expr in 
356 
let (defs, vars'), expr = 

357 
normalize_expr 

358 
~alias:true


359 
node 

365 
let (defs, vars'), expr =


366 
normalize_expr


367 
~alias:false


368 
node


360  369 
[] (* empty offset for arrays *) 
361  370 
([], vars) (* defvar only contains vars *) 
362  371 
assert_expr 
...  ...  
368  377 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
369  378  
370  379 
let new_annots = 
371 
if !Options.traces then 

380 
if !Options.horntraces then


372  381 
begin 
373  382 
(* Compute traceability info: 
374  383 
 gather newly bound variables 
...  ...  
401  410 
node_asserts = asserts; 
402  411 
node_annot = new_annots; 
403  412 
} 
404 
in ((*Printers.pp_node Format.err_formatter node;*) 

405 
node 

406 
) 

407  
413 
in ((*Printers.pp_node Format.err_formatter node;*) node) 

408  414  
409  415 
let normalize_decl decl = 
410  416 
match decl.top_decl_desc with 
Also available in: Unified diff