Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/normalization.ml | ||
---|---|---|
16 | 16 |
|
17 | 17 |
(* To update thank to some command line options *) |
18 | 18 |
let debug = ref false |
19 |
|
|
19 |
|
|
20 | 20 |
(** Normalisation iters through the AST of expressions and bind fresh definition |
21 | 21 |
when some criteria are met. This creation of fresh definition is performed by |
22 | 22 |
the function mk_expr_alias_opt when the alias argument is on. |
... | ... | |
32 | 32 |
definitions. |
33 | 33 |
*) |
34 | 34 |
|
35 |
type param_t = |
|
36 |
{ |
|
37 |
unfold_arrow_active: bool; |
|
38 |
force_alias_ite: bool; |
|
39 |
force_alias_internal_fun: bool; |
|
40 |
} |
|
35 |
type param_t = { |
|
36 |
unfold_arrow_active : bool; |
|
37 |
force_alias_ite : bool; |
|
38 |
force_alias_internal_fun : bool; |
|
39 |
} |
|
40 |
|
|
41 |
let params = |
|
42 |
ref |
|
43 |
{ |
|
44 |
unfold_arrow_active = false; |
|
45 |
force_alias_ite = false; |
|
46 |
force_alias_internal_fun = false; |
|
47 |
} |
|
41 | 48 |
|
42 |
let params = ref |
|
43 |
{ |
|
44 |
unfold_arrow_active = false; |
|
45 |
force_alias_ite = false; |
|
46 |
force_alias_internal_fun =false; |
|
47 |
} |
|
49 |
type norm_ctx_t = { |
|
50 |
parentid : ident; |
|
51 |
vars : var_decl list; |
|
52 |
is_output : ident -> bool; |
|
53 |
} |
|
48 | 54 |
|
49 |
type norm_ctx_t =
|
|
55 |
let expr_true loc ck =
|
|
50 | 56 |
{ |
51 |
parentid: ident; |
|
52 |
vars: var_decl list; |
|
53 |
is_output: ident -> bool; |
|
57 |
expr_tag = Utils.new_tag (); |
|
58 |
expr_desc = Expr_const (Const_tag tag_true); |
|
59 |
expr_type = Type_predef.type_bool; |
|
60 |
expr_clock = ck; |
|
61 |
expr_delay = Delay.new_var (); |
|
62 |
expr_annot = None; |
|
63 |
expr_loc = loc; |
|
54 | 64 |
} |
55 | 65 |
|
56 |
|
|
57 |
let expr_true loc ck = |
|
58 |
{ expr_tag = Utils.new_tag (); |
|
59 |
expr_desc = Expr_const (Const_tag tag_true); |
|
60 |
expr_type = Type_predef.type_bool; |
|
61 |
expr_clock = ck; |
|
62 |
expr_delay = Delay.new_var (); |
|
63 |
expr_annot = None; |
|
64 |
expr_loc = loc } |
|
65 |
|
|
66 | 66 |
let expr_false loc ck = |
67 |
{ expr_tag = Utils.new_tag (); |
|
68 |
expr_desc = Expr_const (Const_tag tag_false); |
|
69 |
expr_type = Type_predef.type_bool; |
|
70 |
expr_clock = ck; |
|
71 |
expr_delay = Delay.new_var (); |
|
72 |
expr_annot = None; |
|
73 |
expr_loc = loc } |
|
67 |
{ |
|
68 |
expr_tag = Utils.new_tag (); |
|
69 |
expr_desc = Expr_const (Const_tag tag_false); |
|
70 |
expr_type = Type_predef.type_bool; |
|
71 |
expr_clock = ck; |
|
72 |
expr_delay = Delay.new_var (); |
|
73 |
expr_annot = None; |
|
74 |
expr_loc = loc; |
|
75 |
} |
|
74 | 76 |
|
75 | 77 |
let expr_once loc ck = |
76 |
{ expr_tag = Utils.new_tag (); |
|
77 |
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); |
|
78 |
expr_type = Type_predef.type_bool; |
|
79 |
expr_clock = ck; |
|
80 |
expr_delay = Delay.new_var (); |
|
81 |
expr_annot = None; |
|
82 |
expr_loc = loc } |
|
78 |
{ |
|
79 |
expr_tag = Utils.new_tag (); |
|
80 |
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck); |
|
81 |
expr_type = Type_predef.type_bool; |
|
82 |
expr_clock = ck; |
|
83 |
expr_delay = Delay.new_var (); |
|
84 |
expr_annot = None; |
|
85 |
expr_loc = loc; |
|
86 |
} |
|
83 | 87 |
|
84 | 88 |
let is_expr_once = |
85 | 89 |
let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in |
86 | 90 |
fun expr -> Corelang.is_eq_expr expr dummy_expr_once |
87 | 91 |
|
88 | 92 |
let unfold_arrow expr = |
89 |
match expr.expr_desc with |
|
90 |
| Expr_arrow (e1, e2) -> |
|
91 |
let loc = expr.expr_loc in |
|
92 |
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in |
|
93 |
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } |
|
94 |
| _ -> assert false |
|
95 |
|
|
96 |
|
|
93 |
match expr.expr_desc with |
|
94 |
| Expr_arrow (e1, e2) -> |
|
95 |
let loc = expr.expr_loc in |
|
96 |
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in |
|
97 |
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) } |
|
98 |
| _ -> assert false |
|
97 | 99 |
|
98 | 100 |
(* Get the equation in [defs] with [expr] as rhs, if any *) |
99 | 101 |
let get_expr_alias defs expr = |
100 |
try Some (List.find (fun eq -> Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock && is_eq_expr eq.eq_rhs expr) defs) |
|
101 |
with |
|
102 |
| Not_found -> None |
|
103 |
|
|
102 |
try |
|
103 |
Some |
|
104 |
(List.find |
|
105 |
(fun eq -> |
|
106 |
Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock |
|
107 |
&& is_eq_expr eq.eq_rhs expr) |
|
108 |
defs) |
|
109 |
with Not_found -> None |
|
110 |
|
|
104 | 111 |
(* Replace [expr] with (tuple of) [locals] *) |
105 | 112 |
let replace_expr locals expr = |
106 |
match locals with |
|
107 |
| [] -> assert false |
|
108 |
| [v] -> { expr with |
|
109 |
expr_tag = Utils.new_tag (); |
|
110 |
expr_desc = Expr_ident v.var_id } |
|
111 |
| _ -> { expr with |
|
112 |
expr_tag = Utils.new_tag (); |
|
113 |
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } |
|
113 |
match locals with |
|
114 |
| [] -> assert false |
|
115 |
| [ v ] -> |
|
116 |
{ expr with expr_tag = Utils.new_tag (); expr_desc = Expr_ident v.var_id } |
|
117 |
| _ -> |
|
118 |
{ |
|
119 |
expr with |
|
120 |
expr_tag = Utils.new_tag (); |
|
121 |
expr_desc = Expr_tuple (List.map expr_of_vdecl locals); |
|
122 |
} |
|
114 | 123 |
|
115 |
|
|
116 | 124 |
(* IS IT USED ? TODO |
117 | 125 |
(* Create an alias for [expr], if none exists yet *) |
118 | 126 |
let mk_expr_alias (parentid, vars) (defs, vars) expr = |
... | ... | |
133 | 141 |
(* 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; *) |
134 | 142 |
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
135 | 143 |
*) |
136 |
|
|
144 |
|
|
137 | 145 |
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) |
138 | 146 |
and [opt] is true |
139 | 147 |
|
... | ... | |
141 | 149 |
*) |
142 | 150 |
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr = |
143 | 151 |
if !debug then |
144 |
Log.report ~plugin:"normalization" ~level:2 |
|
145 |
(fun fmt -> Format.fprintf fmt "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); |
|
152 |
Log.report ~plugin:"normalization" ~level:2 (fun fmt -> |
|
153 |
Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt |
|
154 |
Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck |
|
155 |
expr.expr_clock); |
|
146 | 156 |
match expr.expr_desc with |
147 |
| Expr_ident _ -> |
|
148 |
(defs, vars), expr |
|
149 |
| _ -> |
|
150 |
match get_expr_alias defs expr with |
|
151 |
| Some eq -> |
|
152 |
(* Format.eprintf "Found a preexisting definition@."; *) |
|
153 |
let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in |
|
154 |
(defs, vars), replace_expr aliases expr |
|
155 |
| None -> |
|
156 |
(* Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; |
|
157 |
* Format.eprintf "existing defs are: @[[%a@]]@." |
|
158 |
* (fprintf_list ~sep:"@ "(fun fmt eq -> |
|
159 |
* Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a" |
|
160 |
* Clocks.print_ck eq.eq_rhs.expr_clock |
|
161 |
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) |
|
162 |
* (is_eq_expr eq.eq_rhs expr) |
|
163 |
* Printers.pp_node_eq eq)) |
|
164 |
* defs; *) |
|
165 |
if opt |
|
166 |
then |
|
167 |
let new_aliases = |
|
168 |
List.map2 |
|
169 |
(mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc) |
|
170 |
(Types.type_list_of_type expr.expr_type) |
|
171 |
(Clocks.clock_list_of_clock expr.expr_clock) in |
|
172 |
let new_def = |
|
173 |
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
|
174 |
in |
|
175 |
(* Typing and Registering machine type *) |
|
176 |
let _ = if Machine_types.is_active then |
|
177 |
Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr |
|
178 |
in |
|
179 |
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr |
|
180 |
else |
|
181 |
(defs, vars), expr |
|
182 |
|
|
183 |
(* Similar fonctions for dimensions *) |
|
157 |
| Expr_ident _ -> (defs, vars), expr |
|
158 |
| _ -> ( |
|
159 |
match get_expr_alias defs expr with |
|
160 |
| Some eq -> |
|
161 |
(* Format.eprintf "Found a preexisting definition@."; *) |
|
162 |
let aliases = |
|
163 |
List.map |
|
164 |
(fun id -> List.find (fun v -> v.var_id = id) vars) |
|
165 |
eq.eq_lhs |
|
166 |
in |
|
167 |
(defs, vars), replace_expr aliases expr |
|
168 |
| None -> |
|
169 |
(* |
|
170 |
Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt; |
|
171 |
* Format.eprintf "existing defs are: @[[%a@]]@." |
|
172 |
* (fprintf_list ~sep:"@ "(fun fmt eq -> |
|
173 |
* Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a" |
|
174 |
* Clocks.print_ck eq.eq_rhs.expr_clock |
|
175 |
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock) |
|
176 |
* (is_eq_expr eq.eq_rhs expr) |
|
177 |
* Printers.pp_node_eq eq)) |
|
178 |
* defs; *) |
|
179 |
if opt then |
|
180 |
let new_aliases = |
|
181 |
List.map2 |
|
182 |
(mk_fresh_var |
|
183 |
(norm_ctx.parentid, norm_ctx.vars @ vars) |
|
184 |
expr.expr_loc) |
|
185 |
(Types.type_list_of_type expr.expr_type) |
|
186 |
(Clocks.clock_list_of_clock expr.expr_clock) |
|
187 |
in |
|
188 |
let new_def = |
|
189 |
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr) |
|
190 |
in |
|
191 |
(* Typing and Registering machine type *) |
|
192 |
let _ = |
|
193 |
if Machine_types.is_active then |
|
194 |
Machine_types.type_def |
|
195 |
(norm_ctx.parentid, norm_ctx.vars) |
|
196 |
new_aliases expr |
|
197 |
in |
|
198 |
(new_def :: defs, new_aliases @ vars), replace_expr new_aliases expr |
|
199 |
else (defs, vars), expr) |
|
200 |
|
|
201 |
(* Similar fonctions for dimensions *) |
|
184 | 202 |
let mk_dim_alias opt norm_ctx (defs, vars) dim = |
185 | 203 |
match dim.Dimension.dim_desc with |
186 |
| Dimension.Dbool _ | Dint _ |
|
187 |
| Dident _ -> (defs, vars), dim (* Keep the same *)
|
|
188 |
| _ when opt -> (* Cast to expression, normalizing *)
|
|
189 |
let e = expr_of_dimension dim in
|
|
190 |
let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in
|
|
191 |
defvars, dimension_of_expr e
|
|
192 |
|
|
193 |
| _ -> (defs, vars), dim (* Keep the same *)
|
|
194 |
|
|
204 |
| Dimension.Dbool _ | Dint _ | Dident _ ->
|
|
205 |
(defs, vars), dim (* Keep the same *)
|
|
206 |
| _ when opt -> |
|
207 |
(* Cast to expression, normalizing *)
|
|
208 |
let e = expr_of_dimension dim in
|
|
209 |
let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in
|
|
210 |
defvars, dimension_of_expr e |
|
211 |
| _ -> (defs, vars), dim |
|
212 |
(* Keep the same *) |
|
195 | 213 |
|
196 | 214 |
let unfold_offsets norm_ctx defvars e offsets = |
197 | 215 |
let add_offset (defvars, e) d = |
198 | 216 |
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; *) |
199 |
let defvars, d = mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d in |
|
200 |
let new_e = |
|
201 |
{ e with |
|
217 |
let defvars, d = |
|
218 |
mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d |
|
219 |
in |
|
220 |
let new_e = |
|
221 |
{ |
|
222 |
e with |
|
202 | 223 |
expr_tag = Utils.new_tag (); |
203 | 224 |
expr_loc = d.Dimension.dim_loc; |
204 | 225 |
expr_type = Types.array_element_type e.expr_type; |
205 |
expr_desc = Expr_access (e, d) } |
|
226 |
expr_desc = Expr_access (e, d); |
|
227 |
} |
|
206 | 228 |
in |
207 | 229 |
defvars, new_e |
208 |
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) |
|
230 |
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
|
|
209 | 231 |
in |
210 |
List.fold_left add_offset (defvars, e) offsets
|
|
232 |
List.fold_left add_offset (defvars, e) offsets |
|
211 | 233 |
|
212 |
|
|
213 | 234 |
(* Create a (normalized) expression from [ref_e], |
214 | 235 |
replacing description with [norm_d], |
215 | 236 |
taking propagated [offsets] into account |
216 | 237 |
in order to change expression type *) |
217 | 238 |
let mk_norm_expr offsets ref_e norm_d = |
218 | 239 |
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) |
219 |
let drop_array_type ty = |
|
220 |
Types.map_tuple_type Types.array_element_type ty in
|
|
221 |
{ ref_e with
|
|
240 |
let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in
|
|
241 |
{
|
|
242 |
ref_e with
|
|
222 | 243 |
expr_desc = norm_d; |
223 |
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } |
|
224 |
|
|
244 |
expr_type = |
|
245 |
Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type; |
|
246 |
} |
|
247 |
|
|
225 | 248 |
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *) |
226 | 249 |
let normalize_list alias norm_ctx offsets norm_element defvars elist = |
227 | 250 |
List.fold_right |
228 | 251 |
(fun t (defvars, qlist) -> |
229 | 252 |
let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in |
230 |
(defvars, norm_t :: qlist)
|
|
231 |
) elist (defvars, [])
|
|
253 |
defvars, norm_t :: qlist) |
|
254 |
elist (defvars, []) |
|
232 | 255 |
|
233 |
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr = |
|
256 |
let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets |
|
257 |
defvars expr = |
|
234 | 258 |
(* 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; *) |
235 | 259 |
match expr.expr_desc with |
236 |
| Expr_const _ |
|
237 |
| Expr_ident _ -> |
|
238 |
unfold_offsets norm_ctx defvars expr offsets |
|
260 |
| Expr_const _ | Expr_ident _ -> unfold_offsets norm_ctx defvars expr offsets |
|
239 | 261 |
| Expr_array elist -> |
240 |
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in |
|
241 |
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in |
|
242 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
262 |
let defvars, norm_elist = |
|
263 |
normalize_list alias norm_ctx offsets |
|
264 |
(fun _ -> normalize_array_expr ~alias:true) |
|
265 |
defvars elist |
|
266 |
in |
|
267 |
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in |
|
268 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
243 | 269 |
| Expr_power (e1, d) when offsets = [] -> |
244 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |
|
245 |
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in |
|
246 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
270 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
|
271 |
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
|
|
272 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
|
247 | 273 |
| Expr_power (e1, _) -> |
248 |
normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
|
|
274 |
normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1
|
|
249 | 275 |
| Expr_access (e1, d) -> |
250 |
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |
|
251 |
|
|
276 |
normalize_expr ~alias norm_ctx (d :: offsets) defvars e1 |
|
252 | 277 |
| Expr_tuple elist -> |
253 |
let defvars, norm_elist = |
|
254 |
normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in |
|
255 |
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) |
|
278 |
let defvars, norm_elist = |
|
279 |
normalize_list alias norm_ctx offsets |
|
280 |
(fun alias -> normalize_expr ~alias ~alias_basic:false) |
|
281 |
defvars elist |
|
282 |
in |
|
283 |
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) |
|
256 | 284 |
| Expr_appl (id, args, None) |
257 |
when Basic_library.is_homomorphic_fun id |
|
258 |
&& Types.is_array_type expr.expr_type -> |
|
259 |
let defvars, norm_args = |
|
260 |
normalize_list |
|
261 |
alias |
|
262 |
norm_ctx |
|
263 |
offsets |
|
264 |
(fun _ -> normalize_array_expr ~alias:true) |
|
265 |
defvars |
|
266 |
(expr_list_of_expr args) |
|
267 |
in |
|
268 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
|
269 |
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr |
|
270 |
&& not (!params.force_alias_internal_fun || alias_basic) -> |
|
271 |
let defvars, norm_args = normalize_expr ~alias:true norm_ctx offsets defvars args in |
|
272 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) |
|
285 |
when Basic_library.is_homomorphic_fun id |
|
286 |
&& Types.is_array_type expr.expr_type -> |
|
287 |
let defvars, norm_args = |
|
288 |
normalize_list alias norm_ctx offsets |
|
289 |
(fun _ -> normalize_array_expr ~alias:true) |
|
290 |
defvars (expr_list_of_expr args) |
|
291 |
in |
|
292 |
( defvars, |
|
293 |
mk_norm_expr offsets expr |
|
294 |
(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) ) |
|
295 |
| Expr_appl (id, args, None) |
|
296 |
when Basic_library.is_expr_internal_fun expr |
|
297 |
&& not (!params.force_alias_internal_fun || alias_basic) -> |
|
298 |
let defvars, norm_args = |
|
299 |
normalize_expr ~alias:true norm_ctx offsets defvars args |
|
300 |
in |
|
301 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) |
|
273 | 302 |
| Expr_appl (id, args, r) -> |
274 |
let defvars, r = |
|
275 |
match r with |
|
276 |
| None -> defvars, None |
|
277 |
| Some r -> |
|
278 |
let defvars, norm_r = normalize_expr ~alias_basic:true norm_ctx [] defvars r in |
|
279 |
defvars, Some norm_r |
|
280 |
in |
|
281 |
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in |
|
282 |
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in |
|
283 |
if offsets <> [] |
|
284 |
then |
|
285 |
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in |
|
286 |
normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr |
|
287 |
else |
|
288 |
mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic |
|
289 |
|| not (Basic_library.is_expr_internal_fun expr))) |
|
290 |
norm_ctx defvars norm_expr |
|
303 |
let defvars, r = |
|
304 |
match r with |
|
305 |
| None -> defvars, None |
|
306 |
| Some r -> |
|
307 |
let defvars, norm_r = |
|
308 |
normalize_expr ~alias_basic:true norm_ctx [] defvars r |
|
309 |
in |
|
310 |
defvars, Some norm_r |
|
311 |
in |
|
312 |
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in |
|
313 |
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in |
|
314 |
if offsets <> [] then |
|
315 |
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in |
|
316 |
normalize_expr ~alias norm_ctx offsets defvars norm_expr |
|
317 |
else |
|
318 |
mk_expr_alias_opt |
|
319 |
(alias |
|
320 |
&& (!params.force_alias_internal_fun || alias_basic |
|
321 |
|| not (Basic_library.is_expr_internal_fun expr))) |
|
322 |
norm_ctx defvars norm_expr |
|
291 | 323 |
| Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) -> |
292 |
(* Here we differ from Colaco paper: arrows are pushed to the top *) |
|
293 |
normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr) |
|
294 |
| Expr_arrow (e1,e2) -> |
|
295 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |
|
296 |
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in |
|
297 |
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in |
|
298 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
324 |
(* Here we differ from Colaco paper: arrows are pushed to the top *) |
|
325 |
normalize_expr ~alias norm_ctx offsets defvars (unfold_arrow expr) |
|
326 |
| Expr_arrow (e1, e2) -> |
|
327 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |
|
328 |
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in |
|
329 |
let norm_expr = |
|
330 |
mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) |
|
331 |
in |
|
332 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
299 | 333 |
| Expr_pre e -> |
300 |
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in |
|
301 |
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in |
|
302 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
334 |
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
|
|
335 |
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
|
|
336 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
|
303 | 337 |
| Expr_fby (e1, e2) -> |
304 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |
|
305 |
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in |
|
306 |
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in |
|
307 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
338 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
|
339 |
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
|
|
340 |
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
|
|
341 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
|
308 | 342 |
| Expr_when (e, c, l) -> |
309 |
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in |
|
310 |
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) |
|
343 |
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
|
|
344 |
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
|
|
311 | 345 |
| Expr_ite (c, t, e) -> |
312 |
let defvars, norm_c = normalize_guard norm_ctx defvars c in |
|
313 |
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in |
|
314 |
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in |
|
315 |
let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in |
|
316 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
346 |
let defvars, norm_c = normalize_guard norm_ctx defvars c in |
|
347 |
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in |
|
348 |
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in |
|
349 |
let norm_expr = |
|
350 |
mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) |
|
351 |
in |
|
352 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
317 | 353 |
| Expr_merge (c, hl) -> |
318 |
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in |
|
319 |
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in |
|
320 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr |
|
354 |
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
|
|
355 |
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
|
|
356 |
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
|
321 | 357 |
|
322 | 358 |
(* Creates a conditional with a merge construct, which is more lazy *) |
323 | 359 |
(* |
... | ... | |
330 | 366 |
and normalize_branches norm_ctx offsets defvars hl = |
331 | 367 |
List.fold_right |
332 | 368 |
(fun (t, h) (defvars, norm_q) -> |
333 |
let (defvars, norm_h) = normalize_cond_expr norm_ctx offsets defvars h in |
|
334 |
defvars, (t, norm_h) :: norm_q |
|
335 |
) |
|
369 |
let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in |
|
370 |
defvars, (t, norm_h) :: norm_q) |
|
336 | 371 |
hl (defvars, []) |
337 | 372 |
|
338 |
and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
|
|
373 |
and normalize_array_expr ?(alias = true) norm_ctx offsets defvars expr =
|
|
339 | 374 |
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) |
340 | 375 |
match expr.expr_desc with |
341 | 376 |
| Expr_power (e1, d) when offsets = [] -> |
342 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in |
|
343 |
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) |
|
377 |
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
|
378 |
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
|
|
344 | 379 |
| Expr_power (e1, _) -> |
345 |
normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1 |
|
346 |
| Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |
|
380 |
normalize_array_expr ~alias norm_ctx (List.tl offsets) defvars e1 |
|
381 |
| Expr_access (e1, d) -> |
|
382 |
normalize_array_expr ~alias norm_ctx (d :: offsets) defvars e1 |
|
347 | 383 |
| Expr_array elist when offsets = [] -> |
348 |
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in |
|
349 |
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) |
|
384 |
let defvars, norm_elist = |
|
385 |
normalize_list alias norm_ctx offsets |
|
386 |
(fun _ -> normalize_array_expr ~alias:true) |
|
387 |
defvars elist |
|
388 |
in |
|
389 |
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) |
|
350 | 390 |
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr -> |
351 |
let defvars, norm_args = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in |
|
352 |
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) |
|
353 |
| _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr |
|
354 |
|
|
355 |
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr = |
|
391 |
let defvars, norm_args = |
|
392 |
normalize_list alias norm_ctx offsets |
|
393 |
(fun _ -> normalize_array_expr ~alias:true) |
|
394 |
defvars (expr_list_of_expr args) |
|
395 |
in |
|
396 |
( defvars, |
|
397 |
mk_norm_expr offsets expr |
|
398 |
(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) ) |
|
399 |
| _ -> normalize_expr ~alias norm_ctx offsets defvars expr |
|
400 |
|
|
401 |
and normalize_cond_expr ?(alias = true) norm_ctx offsets defvars expr = |
|
356 | 402 |
(* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *) |
357 | 403 |
match expr.expr_desc with |
358 | 404 |
| Expr_access (e1, d) -> |
359 |
normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1
|
|
405 |
normalize_cond_expr ~alias norm_ctx (d :: offsets) defvars e1
|
|
360 | 406 |
| Expr_ite (c, t, e) -> |
361 |
let defvars, norm_c = normalize_guard norm_ctx defvars c in |
|
362 |
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in |
|
363 |
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in |
|
364 |
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) |
|
407 |
let defvars, norm_c = normalize_guard norm_ctx defvars c in
|
|
408 |
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
|
|
409 |
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
|
|
410 |
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
|
|
365 | 411 |
| Expr_merge (c, hl) -> |
366 |
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in |
|
367 |
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) |
|
412 |
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
|
|
413 |
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
|
|
368 | 414 |
| _ when !params.force_alias_ite -> |
369 |
(* Forcing alias creation for then/else expressions *) |
|
370 |
let defvars, norm_expr = |
|
371 |
normalize_expr ~alias:alias norm_ctx offsets defvars expr |
|
372 |
in |
|
373 |
mk_expr_alias_opt true norm_ctx defvars norm_expr |
|
374 |
| _ -> (* default case without the force_alias_ite option *) |
|
375 |
normalize_expr ~alias:alias norm_ctx offsets defvars expr |
|
376 |
|
|
415 |
(* Forcing alias creation for then/else expressions *) |
|
416 |
let defvars, norm_expr = |
|
417 |
normalize_expr ~alias norm_ctx offsets defvars expr |
|
418 |
in |
|
419 |
mk_expr_alias_opt true norm_ctx defvars norm_expr |
|
420 |
| _ -> |
|
421 |
(* default case without the force_alias_ite option *) |
|
422 |
normalize_expr ~alias norm_ctx offsets defvars expr |
|
423 |
|
|
377 | 424 |
and normalize_guard norm_ctx defvars expr = |
378 |
let defvars, norm_expr = normalize_expr ~alias_basic:true norm_ctx [] defvars expr in |
|
425 |
let defvars, norm_expr = |
|
426 |
normalize_expr ~alias_basic:true norm_ctx [] defvars expr |
|
427 |
in |
|
379 | 428 |
mk_expr_alias_opt true norm_ctx defvars norm_expr |
380 | 429 |
|
381 | 430 |
(* outputs cannot be memories as well. If so, introduce new local variable. |
... | ... | |
383 | 432 |
let decouple_outputs norm_ctx defvars eq = |
384 | 433 |
let rec fold_lhs defvars lhs tys cks = |
385 | 434 |
match lhs, tys, cks with |
386 |
| [], [], [] -> defvars, [] |
|
387 |
| v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in |
|
388 |
if norm_ctx.is_output v |
|
389 |
then |
|
390 |
let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in |
|
391 |
let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in |
|
392 |
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q |
|
393 |
else |
|
394 |
(defs_q, vars_q), v::lhs_q |
|
395 |
| _ -> assert false in |
|
435 |
| [], [], [] -> defvars, [] |
|
436 |
| v :: qv, t :: qt, c :: qc -> |
|
437 |
let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in |
|
438 |
if norm_ctx.is_output v then |
|
439 |
let newvar = |
|
440 |
mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c |
|
441 |
in |
|
442 |
let neweq = mkeq eq.eq_loc ([ v ], expr_of_vdecl newvar) in |
|
443 |
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q |
|
444 |
else (defs_q, vars_q), v :: lhs_q |
|
445 |
| _ -> assert false |
|
446 |
in |
|
396 | 447 |
let defvars', lhs' = |
397 |
fold_lhs |
|
398 |
defvars |
|
399 |
eq.eq_lhs |
|
448 |
fold_lhs defvars eq.eq_lhs |
|
400 | 449 |
(Types.type_list_of_type eq.eq_rhs.expr_type) |
401 |
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in |
|
402 |
defvars', {eq with eq_lhs = lhs' } |
|
450 |
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) |
|
451 |
in |
|
452 |
defvars', { eq with eq_lhs = lhs' } |
|
403 | 453 |
|
404 | 454 |
let normalize_eq norm_ctx defvars eq = |
405 |
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*) |
|
455 |
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
|
|
406 | 456 |
match eq.eq_rhs.expr_desc with |
407 |
| Expr_pre _ |
|
408 |
| Expr_fby _ -> |
|
409 |
let (defvars', eq') = decouple_outputs norm_ctx defvars eq in |
|
410 |
let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs in |
|
411 |
let norm_eq = { eq' with eq_rhs = norm_rhs } in |
|
412 |
(norm_eq::defs', vars') |
|
457 |
| Expr_pre _ | Expr_fby _ -> |
|
458 |
let defvars', eq' = decouple_outputs norm_ctx defvars eq in |
|
459 |
let (defs', vars'), norm_rhs = |
|
460 |
normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs |
|
461 |
in |
|
462 |
let norm_eq = { eq' with eq_rhs = norm_rhs } in |
|
463 |
norm_eq :: defs', vars' |
|
413 | 464 |
| Expr_array _ -> |
414 |
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |
|
415 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
416 |
(norm_eq::defs', vars') |
|
417 |
| Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type -> |
|
418 |
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |
|
419 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
420 |
(norm_eq::defs', vars') |
|
465 |
let (defs', vars'), norm_rhs = |
|
466 |
normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs |
|
467 |
in |
|
468 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
469 |
norm_eq :: defs', vars' |
|
470 |
| Expr_appl (id, _, None) |
|
471 |
when Basic_library.is_homomorphic_fun id |
|
472 |
&& Types.is_array_type eq.eq_rhs.expr_type -> |
|
473 |
let (defs', vars'), norm_rhs = |
|
474 |
normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs |
|
475 |
in |
|
476 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
477 |
norm_eq :: defs', vars' |
|
421 | 478 |
| Expr_appl _ -> |
422 |
let (defs', vars'), norm_rhs = normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |
|
423 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
424 |
(norm_eq::defs', vars') |
|
479 |
let (defs', vars'), norm_rhs = |
|
480 |
normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs |
|
481 |
in |
|
482 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
483 |
norm_eq :: defs', vars' |
|
425 | 484 |
| _ -> |
426 |
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs in |
|
427 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
428 |
norm_eq::defs', vars' |
|
485 |
let (defs', vars'), norm_rhs = |
|
486 |
normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs |
|
487 |
in |
|
488 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
|
489 |
norm_eq :: defs', vars' |
|
429 | 490 |
|
430 | 491 |
let normalize_eq_split norm_ctx defvars eq = |
431 | 492 |
try |
432 | 493 |
let defs, vars = normalize_eq norm_ctx defvars eq in |
433 |
List.fold_right (fun eq (def, vars) -> |
|
494 |
List.fold_right |
|
495 |
(fun eq (def, vars) -> |
|
434 | 496 |
let eq_defs = Splitting.tuple_split_eq eq in |
435 |
if eq_defs = [eq] then |
|
436 |
eq::def, vars |
|
437 |
else |
|
438 |
List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs |
|
439 |
) defs ([], vars) |
|
440 |
|
|
441 |
with ex -> ( |
|
497 |
if eq_defs = [ eq ] then eq :: def, vars |
|
498 |
else List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs) |
|
499 |
defs ([], vars) |
|
500 |
with ex -> |
|
442 | 501 |
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq; |
443 | 502 |
raise ex |
444 |
) |
|
445 | 503 |
|
446 | 504 |
(* Projecting an eexpr to an eexpr associated to a single |
447 | 505 |
variable. Returns the updated ee, the bounded variable and the |
448 | 506 |
associated statement *) |
449 |
let normalize_pred_eexpr norm_ctx (def,vars) ee = |
|
450 |
assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *) |
|
507 |
let normalize_pred_eexpr norm_ctx (def, vars) ee = |
|
508 |
assert (ee.eexpr_quantifiers = []); |
|
509 |
(* We do not normalize quantifiers yet. This is for very far future. *) |
|
451 | 510 |
(* don't do anything is eexpr is just a variable *) |
452 | 511 |
let skip = |
453 | 512 |
match ee.eexpr_qfexpr.expr_desc with |
454 | 513 |
| Expr_ident _ | Expr_const _ -> true |
455 | 514 |
| _ -> false |
456 | 515 |
in |
457 |
if skip then |
|
458 |
ee, (def, vars) |
|
459 |
else ( |
|
516 |
if skip then ee, (def, vars) |
|
517 |
else |
|
460 | 518 |
(* New output variable *) |
461 | 519 |
let output_id = "spec" ^ string_of_int ee.eexpr_tag in |
462 |
let output_var = |
|
463 |
mkvar_decl |
|
464 |
ee.eexpr_loc |
|
465 |
(output_id, |
|
466 |
mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *) |
|
467 |
mkclock ee.eexpr_loc Ckdec_any, |
|
468 |
false (* not a constant *), |
|
469 |
None, |
|
470 |
None |
|
471 |
) |
|
520 |
let output_var = |
|
521 |
mkvar_decl ee.eexpr_loc |
|
522 |
( output_id, |
|
523 |
mktyp ee.eexpr_loc Tydec_bool, |
|
524 |
(* It is a predicate, hence a bool *) |
|
525 |
mkclock ee.eexpr_loc Ckdec_any, |
|
526 |
false (* not a constant *), |
|
527 |
None, |
|
528 |
None ) |
|
472 | 529 |
in |
473 | 530 |
let output_expr = expr_of_vdecl output_var in |
474 | 531 |
(* Rebuilding an eexpr with a silly expression, just a variable *) |
... | ... | |
476 | 533 |
|
477 | 534 |
(* Now processing a fresh equation output_id = eexpr_qfexpr. We |
478 | 535 |
inline possible calls within, normalize it and type/clock the |
479 |
result. *) |
|
480 |
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in |
|
481 |
|
|
536 |
result. *) |
|
537 |
let eq = mkeq ee.eexpr_loc ([ output_id ], ee.eexpr_qfexpr) in |
|
482 | 538 |
|
483 | 539 |
(* (\* Inlining any calls *\) |
484 | 540 |
* let nodes = get_nodes decls in |
... | ... | |
489 | 545 |
* else |
490 | 546 |
* assert false (\* TODO *\) |
491 | 547 |
* in *) |
492 |
|
|
548 |
|
|
493 | 549 |
(* Normalizing expr and eqs *) |
494 |
let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in |
|
495 |
let vars = output_var :: vars in |
|
496 |
(* let todefine = |
|
497 |
List.fold_left |
|
498 |
(fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) |
|
499 |
(ISet.add output_id ISet.empty) vars in |
|
500 |
*) |
|
550 |
let defs, vars = |
|
551 |
List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ] |
|
552 |
in |
|
553 |
let vars = output_var :: vars in |
|
554 |
|
|
555 |
(* let todefine = |
|
556 |
List.fold_left |
|
557 |
(fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m) |
|
558 |
(ISet.add output_id ISet.empty) vars in |
|
559 |
*) |
|
501 | 560 |
|
502 | 561 |
(* Typing / Clocking *) |
503 | 562 |
try |
504 | 563 |
ignore (Typing.type_var_decl_list vars !Global.type_env vars); |
505 |
(* |
|
564 |
|
|
565 |
(* |
|
506 | 566 |
let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *) |
507 | 567 |
(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *) |
508 | 568 |
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in |
... | ... | |
515 | 575 |
(*Format.eprintf "normalized eqs %a@.@?" |
516 | 576 |
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *) |
517 | 577 |
*) |
578 |
ee', (defs, vars) |
|
579 |
with Types.Error (loc, err) as exc -> |
|
580 |
eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee |
|
581 |
Types.pp_error err |
|
582 |
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) |
|
583 |
defs Location.pp_loc loc; |
|
518 | 584 |
|
519 |
ee', (defs, vars) |
|
520 |
|
|
521 |
with (Types.Error (loc,err)) as exc -> |
|
522 |
eprintf "Typing error for eexpr %a: %a%a%a@." |
|
523 |
Printers.pp_eexpr ee |
|
524 |
Types.pp_error err |
|
525 |
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs |
|
526 |
Location.pp_loc loc |
|
527 |
|
|
528 |
|
|
529 |
; |
|
530 |
raise exc |
|
531 |
|
|
532 |
) |
|
533 |
|
|
534 |
(* |
|
585 |
raise exc |
|
586 |
|
|
587 |
(* |
|
535 | 588 |
|
536 | 589 |
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in |
537 | 590 |
(* Calls are first inlined *) |
... | ... | |
580 | 633 |
|
581 | 634 |
; |
582 | 635 |
raise exc |
583 |
*) |
|
584 |
|
|
636 |
*) |
|
585 | 637 |
|
586 |
(* We use node local vars to make sure we are creating fresh variables *)
|
|
638 |
(* We use node local vars to make sure we are creating fresh variables *) |
|
587 | 639 |
let normalize_spec parentid (in_vars, out_vars, l_vars) s = |
588 | 640 |
(* Original set of variables actually visible from here: in/out and |
589 | 641 |
spec locals (no node locals) *) |
590 | 642 |
let orig_vars = in_vars @ out_vars @ s.locals in |
591 | 643 |
(* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *) |
592 |
let not_is_orig_var v = |
|
593 |
List.for_all ((!=) v) orig_vars in
|
|
594 |
let norm_ctx = {
|
|
595 |
parentid = parentid;
|
|
644 |
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
|
|
645 |
let norm_ctx =
|
|
646 |
{
|
|
647 |
parentid; |
|
596 | 648 |
vars = in_vars @ out_vars @ l_vars; |
597 |
is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *); |
|
649 |
is_output = |
|
650 |
(fun _ -> false) (* no need to introduce fresh variables for outputs *); |
|
598 | 651 |
} |
599 | 652 |
in |
600 | 653 |
(* Normalizing existing stmts *) |
601 |
let eqs, auts = List.fold_right (fun s (el,al) -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in |
|
602 |
if auts != [] then assert false; (* Automata should be expanded by now. *) |
|
603 |
let defsvars = |
|
604 |
List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs |
|
654 |
let eqs, auts = |
|
655 |
List.fold_right |
|
656 |
(fun s (el, al) -> |
|
657 |
match s with Eq e -> e :: el, al | Aut a -> el, a :: al) |
|
658 |
s.stmts ([], []) |
|
605 | 659 |
in |
660 |
if auts != [] then assert false; |
|
661 |
(* Automata should be expanded by now. *) |
|
662 |
let defsvars = List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in |
|
606 | 663 |
(* Iterate through predicates and normalize them on the go, creating |
607 | 664 |
fresh variables for any guarantees/assumes/require/ensure *) |
608 | 665 |
let process_predicates l defvars = |
609 | 666 |
(* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *) |
610 |
let res = List.fold_right (fun ee (accu, defvars) -> |
|
611 |
let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in |
|
612 |
ee'::accu, defvars |
|
613 |
) l ([], defvars) |
|
667 |
let res = |
|
668 |
List.fold_right |
|
669 |
(fun ee (accu, defvars) -> |
|
670 |
let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in |
|
671 |
ee' :: accu, defvars) |
|
672 |
l ([], defvars) |
|
614 | 673 |
in |
615 | 674 |
(* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res)); |
616 | 675 |
* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *) |
617 | 676 |
res |
618 | 677 |
in |
619 | 678 |
|
620 |
|
|
621 | 679 |
let assume', defsvars = process_predicates s.assume defsvars in |
622 | 680 |
let guarantees', defsvars = process_predicates s.guarantees defsvars in |
623 | 681 |
let modes', (defs, vars) = |
624 |
List.fold_right (
|
|
625 |
fun m (accu_m, defsvars) ->
|
|
682 |
List.fold_right |
|
683 |
(fun m (accu_m, defsvars) ->
|
|
626 | 684 |
let require', defsvars = process_predicates m.require defsvars in |
627 | 685 |
let ensure', defsvars = process_predicates m.ensure defsvars in |
628 |
{ m with require = require'; ensure = ensure' }:: accu_m, defsvars
|
|
629 |
) s.modes ([], defsvars)
|
|
686 |
{ m with require = require'; ensure = ensure' } :: accu_m, defsvars)
|
|
687 |
s.modes ([], defsvars) |
|
630 | 688 |
in |
631 |
|
|
632 |
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *) |
|
633 |
new_locals, defs, |
|
634 |
{s with |
|
635 |
(* locals = s.locals @ new_locals; *) |
|
636 |
stmts = []; |
|
637 |
assume = assume'; |
|
638 |
guarantees = guarantees'; |
|
639 |
modes = modes' |
|
640 |
} |
|
689 |
|
|
690 |
let new_locals = List.filter not_is_orig_var vars in |
|
691 |
(* removing inouts and initial locals ones *) |
|
692 |
( new_locals, |
|
693 |
defs, |
|
694 |
{ |
|
695 |
s with |
|
696 |
(* locals = s.locals @ new_locals; *) |
|
697 |
stmts = []; |
|
698 |
assume = assume'; |
|
699 |
guarantees = guarantees'; |
|
700 |
modes = modes'; |
|
701 |
} ) |
|
641 | 702 |
(* let nee _ = () in |
642 | 703 |
* (\*normalize_eexpr decls iovars in *\) |
643 | 704 |
* List.iter nee s.assume; |
... | ... | |
646 | 707 |
* List.iter nee m.require; |
647 | 708 |
* List.iter nee m.ensure |
648 | 709 |
* ) s.modes; *) |
649 |
|
|
650 | 710 |
|
651 |
|
|
652 |
|
|
653 |
|
|
654 |
|
|
655 | 711 |
(* The normalization phase introduces new local variables |
656 | 712 |
- output cannot be memories. If this happen, new local variables acting as |
657 | 713 |
memories are introduced. |
... | ... | |
671 | 727 |
*) |
672 | 728 |
let normalize_node node = |
673 | 729 |
reset_cpt_fresh (); |
674 |
let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
|
|
675 |
let not_is_orig_var v = |
|
676 |
List.for_all ((!=) v) orig_vars in
|
|
677 |
let norm_ctx = {
|
|
730 |
let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in
|
|
731 |
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
|
|
732 |
let norm_ctx =
|
|
733 |
{
|
|
678 | 734 |
parentid = node.node_id; |
679 | 735 |
vars = get_node_vars node; |
680 |
is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs); |
|
736 |
is_output = |
|
737 |
(fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs); |
|
681 | 738 |
} |
682 | 739 |
in |
683 | 740 |
|
684 | 741 |
let eqs, auts = get_node_eqs node in |
685 |
if auts != [] then assert false; (* Automata should be expanded by now. *) |
|
742 |
if auts != [] then assert false; |
|
743 |
(* Automata should be expanded by now. *) |
|
686 | 744 |
let spec, new_vars, eqs = |
687 |
begin |
|
688 |
(* Update mutable fields of eexpr to perform normalization of |
|
689 |
specification. |
|
690 |
|
|
691 |
Careful: we do not normalize annotations, since they can have the form |
|
692 |
x = (a, b, c) *) |
|
693 |
match node.node_spec with |
|
694 |
| None |
|
695 |
| Some (NodeSpec _) -> node.node_spec, [], eqs |
|
696 |
| Some (Contract s) -> |
|
697 |
let new_locals, new_stmts, s' = normalize_spec |
|
698 |
node.node_id |
|
699 |
(node.node_inputs, node.node_outputs, node.node_locals) |
|
700 |
s |
|
701 |
in |
|
702 |
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals; |
|
703 |
* Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *) |
|
704 |
Some (Contract s'), new_locals, new_stmts@eqs |
|
705 |
end |
|
745 |
(* Update mutable fields of eexpr to perform normalization of |
|
746 |
specification. |
|
747 |
|
|
748 |
Careful: we do not normalize annotations, since they can have the form |
|
749 |
x = (a, b, c) *) |
|
750 |
match node.node_spec with |
|
751 |
| None | Some (NodeSpec _) -> node.node_spec, [], eqs |
|
752 |
| Some (Contract s) -> |
|
753 |
let new_locals, new_stmts, s' = |
|
754 |
normalize_spec node.node_id |
|
755 |
(node.node_inputs, node.node_outputs, node.node_locals) |
|
756 |
s |
|
757 |
in |
|
758 |
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals; |
|
759 |
* Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *) |
|
760 |
Some (Contract s'), new_locals, new_stmts @ eqs |
|
706 | 761 |
in |
707 | 762 |
let defs, vars = |
708 |
List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in |
|
763 |
List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs |
|
764 |
in |
|
709 | 765 |
(* Normalize the asserts *) |
710 | 766 |
let vars, assert_defs, asserts = |
711 |
List.fold_left ( |
|
712 |
fun (vars, def_accu, assert_accu) assert_ -> |
|
713 |
let assert_expr = assert_.assert_expr in |
|
714 |
let (defs, vars'), expr = |
|
715 |
normalize_expr |
|
716 |
~alias:true (* forcing introduction of new equations for fcn calls *) |
|
717 |
norm_ctx |
|
718 |
[] (* empty offset for arrays *) |
|
719 |
([], vars) (* defvar only contains vars *) |
|
720 |
assert_expr |
|
721 |
in |
|
767 |
List.fold_left |
|
768 |
(fun (vars, def_accu, assert_accu) assert_ -> |
|
769 |
let assert_expr = assert_.assert_expr in |
|
770 |
let (defs, vars'), expr = |
|
771 |
normalize_expr ~alias:true |
|
772 |
(* forcing introduction of new equations for fcn calls *) |
|
773 |
norm_ctx [] |
|
774 |
(* empty offset for arrays *) |
|
775 |
([], vars) |
|
776 |
(* defvar only contains vars *) |
|
777 |
assert_expr |
|
778 |
in |
|
722 | 779 |
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) |
723 |
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu |
|
724 |
) (vars, [], []) node.node_asserts in |
|
725 |
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout |
|
726 |
vars and initial locals ones *) |
|
727 |
|
|
728 |
let all_locals = node.node_locals @ new_locals in (* we add again, at the |
|
729 |
beginning of the list the |
|
730 |
local declared ones *) |
|
731 |
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) |
|
780 |
( vars', |
|
781 |
defs @ def_accu, |
|
782 |
{ assert_ with assert_expr = expr } :: assert_accu )) |
|
783 |
(vars, [], []) node.node_asserts |
|
784 |
in |
|
785 |
let new_locals = List.filter not_is_orig_var vars in |
|
786 |
|
|
787 |
(* we filter out inout |
|
788 |
vars and initial locals ones *) |
|
789 |
let all_locals = node.node_locals @ new_locals in |
|
732 | 790 |
|
791 |
(* we add again, at the |
|
792 |
beginning of the list the |
|
793 |
local declared ones *) |
|
794 |
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) |
|
733 | 795 |
|
734 | 796 |
(* Updating annotations: traceability and machine types for fresh variables *) |
735 |
|
|
797 |
|
|
736 | 798 |
(* Compute traceability info: |
737 | 799 |
- gather newly bound variables |
738 | 800 |
- compute the associated expression without aliases |
739 |
*)
|
|
801 |
*) |
|
740 | 802 |
let new_annots = |
741 | 803 |
if !Options.traces then |
742 |
begin |
|
743 |
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in |
|
744 |
let norm_traceability = { |
|
745 |
annots = List.map (fun v -> |
|
746 |
let eq = |
|
747 |
try |
|
748 |
List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) |
|
749 |
with Not_found -> |
|
750 |
( |
|
751 |
Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; |
|
752 |
assert false |
|
753 |
) |
|
754 |
in |
|
755 |
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in |
|
756 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
|
757 |
Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"]; |
|
758 |
(["traceability"], pair) |
|
759 |
) diff_vars; |
|
760 |
annot_loc = Location.dummy_loc |
|
761 |
} |
|
762 |
in |
|
763 |
norm_traceability::node.node_annot |
|
764 |
end |
|
765 |
else |
|
766 |
node.node_annot |
|
804 |
let diff_vars = |
|
805 |
List.filter (fun v -> not (List.mem v node.node_locals)) all_locals |
|
806 |
in |
|
807 |
let norm_traceability = |
|
808 |
{ |
|
809 |
annots = |
|
810 |
List.map |
|
811 |
(fun v -> |
|
812 |
let eq = |
|
813 |
try |
|
814 |
List.find |
|
815 |
(fun eq -> |
|
816 |
List.exists (fun v' -> v' = v.var_id) eq.eq_lhs) |
|
817 |
(defs @ assert_defs) |
|
818 |
with Not_found -> |
|
819 |
Format.eprintf |
|
820 |
"Traceability annotation generation: var %s not found@." |
|
821 |
v.var_id; |
|
822 |
assert false |
|
823 |
in |
|
824 |
let expr = |
|
825 |
substitute_expr diff_vars (defs @ assert_defs) eq.eq_rhs |
|
826 |
in |
|
827 |
let pair = |
|
828 |
mkeexpr expr.expr_loc |
|
829 |
(mkexpr expr.expr_loc |
|
830 |
(Expr_tuple |
|
831 |
[ expr_of_ident v.var_id expr.expr_loc; expr ])) |
|
832 |
in |
|
833 |
Annotations.add_expr_ann node.node_id pair.eexpr_tag |
|
834 |
[ "traceability" ]; |
|
835 |
[ "traceability" ], pair) |
|
836 |
diff_vars; |
|
837 |
annot_loc = Location.dummy_loc; |
|
838 |
} |
|
839 |
in |
|
840 |
norm_traceability :: node.node_annot |
|
841 |
else node.node_annot |
|
767 | 842 |
in |
768 | 843 |
|
769 | 844 |
let new_annots = |
770 |
List.fold_left (fun annots v ->
|
|
771 |
if Machine_types.is_active && Machine_types.is_exportable v then
|
|
772 |
let typ = Machine_types.get_specified_type v in
|
|
773 |
let typ_name = Machine_types.type_name typ in
|
|
774 |
|
|
775 |
let loc = v.var_loc in |
|
776 |
let typ_as_string =
|
|
777 |
mkexpr
|
|
778 |
loc
|
|
779 |
(Expr_const
|
|
780 |
(Const_string typ_name))
|
|
781 |
in
|
|
782 |
let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
|
|
783 |
Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
|
|
784 |
{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
|
|
785 |
else
|
|
786 |
annots
|
|
787 |
) new_annots new_locals
|
|
845 |
List.fold_left |
|
846 |
(fun annots v ->
|
|
847 |
if Machine_types.is_active && Machine_types.is_exportable v then (
|
|
848 |
let typ = Machine_types.get_specified_type v in
|
|
849 |
let typ_name = Machine_types.type_name typ in |
|
850 |
|
|
851 |
let loc = v.var_loc in
|
|
852 |
let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in
|
|
853 |
let pair =
|
|
854 |
expr_to_eexpr
|
|
855 |
(expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])
|
|
856 |
in
|
|
857 |
Annotations.add_expr_ann node.node_id pair.eexpr_tag
|
|
858 |
Machine_types.keyword;
|
|
859 |
{ annots = [ Machine_types.keyword, pair ]; annot_loc = loc }
|
|
860 |
:: annots)
|
|
861 |
else annots)
|
|
862 |
new_annots new_locals |
|
788 | 863 |
in |
789 |
|
|
790 |
|
|
864 |
|
|
791 | 865 |
let node = |
792 |
{ node with |
|
866 |
{ |
|
867 |
node with |
|
793 | 868 |
node_locals = all_locals; |
794 | 869 |
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs); |
795 | 870 |
node_asserts = asserts; |
796 | 871 |
node_annot = new_annots; |
797 | 872 |
node_spec = spec; |
798 | 873 |
} |
799 |
in ((*Printers.pp_node Format.err_formatter node;*)
|
|
800 |
node
|
|
801 |
)
|
|
874 |
in |
|
875 |
(*Printers.pp_node Format.err_formatter node;*)
|
|
876 |
node
|
|
802 | 877 |
|
803 | 878 |
let normalize_inode nd = |
804 | 879 |
reset_cpt_fresh (); |
805 | 880 |
match nd.nodei_spec with |
806 |
None | Some (NodeSpec _) -> nd
|
|
807 |
| Some (Contract _) -> assert false
|
|
808 |
|
|
809 |
let normalize_decl (decl: top_decl) : top_decl = |
|
881 |
| None | Some (NodeSpec _) -> nd
|
|
882 |
| Some (Contract _) -> assert false |
|
883 |
|
|
884 |
let normalize_decl (decl : top_decl) : top_decl =
|
|
810 | 885 |
match decl.top_decl_desc with |
811 | 886 |
| Node nd -> |
812 |
let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
|
|
813 |
update_node nd.node_id decl'; |
|
814 |
decl' |
|
887 |
let decl' = { decl with top_decl_desc = Node (normalize_node nd) } in
|
|
888 |
update_node nd.node_id decl';
|
|
889 |
decl'
|
|
815 | 890 |
| ImportedNode nd -> |
816 |
let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode nd)} in |
|
817 |
update_node nd.nodei_id decl'; |
|
818 |
decl' |
|
819 |
|
|
820 |
| Include _| Open _ | Const _ | TypeDef _ -> decl |
|
891 |
let decl' = |
|
892 |
{ decl with top_decl_desc = ImportedNode (normalize_inode nd) } |
|
893 |
in |
|
894 |
update_node nd.nodei_id decl'; |
|
895 |
decl' |
|
896 |
| Include _ | Open _ | Const _ | TypeDef _ -> decl |
|
821 | 897 |
|
822 | 898 |
let normalize_prog p decls = |
823 | 899 |
(* Backend specific configurations for normalization *) |
... | ... | |
826 | 902 |
(* Main algorithm: iterates over nodes *) |
827 | 903 |
List.map normalize_decl decls |
828 | 904 |
|
829 |
|
|
830 | 905 |
(* Fake interface for outside uses *) |
831 | 906 |
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr = |
832 |
mk_expr_alias_opt |
|
833 |
opt |
|
834 |
{parentid = parentid; vars = ctx_vars; is_output = (fun _ -> false) } |
|
835 |
(defs, vars) |
|
836 |
expr |
|
907 |
mk_expr_alias_opt opt |
|
908 |
{ parentid; vars = ctx_vars; is_output = (fun _ -> false) } |
|
909 |
(defs, vars) expr |
|
837 | 910 |
|
838 |
|
|
839 |
(* Local Variables: *) |
|
840 |
(* compile-command:"make -C .." *) |
|
841 |
(* End: *) |
|
842 |
|
|
911 |
(* Local Variables: *) |
|
912 |
(* compile-command:"make -C .." *) |
|
913 |
(* End: *) |
Also available in: Unified diff
reformatting