Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/corelang.ml | ||
---|---|---|
14 | 14 |
open Machine_code_types |
15 | 15 |
(*open Dimension*) |
16 | 16 |
|
17 |
|
|
18 |
module VDeclModule = |
|
19 |
struct (* Node module *) |
|
17 |
module VDeclModule = struct |
|
18 |
(* Node module *) |
|
20 | 19 |
type t = var_decl |
20 |
|
|
21 | 21 |
let compare v1 v2 = compare v1.var_id v2.var_id |
22 | 22 |
end |
23 | 23 |
|
24 |
module VMap = Map.Make(VDeclModule) |
|
24 |
module VMap = Map.Make (VDeclModule)
|
|
25 | 25 |
|
26 |
module VSet: sig |
|
26 |
module VSet : sig
|
|
27 | 27 |
include Set.S |
28 |
val pp: Format.formatter -> t -> unit |
|
29 |
val get: ident -> t -> elt |
|
30 |
end with type elt = var_decl = |
|
31 |
struct |
|
32 |
include Set.Make(VDeclModule) |
|
33 |
let pp fmt s = |
|
34 |
Format.fprintf fmt "{@[%a}@]" (Utils.fprintf_list ~sep:",@ " Printers.pp_var) (elements s) |
|
35 |
(* Strangley the find_first function of Set.Make is incorrect (at |
|
36 |
the current time of writting this comment. Had to switch to |
|
37 |
lists *) |
|
38 |
let get id s = List.find (fun v -> v.var_id = id) (elements s) |
|
39 |
end |
|
40 |
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
|
41 | 28 |
|
42 |
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
|
29 |
val pp : Format.formatter -> t -> unit |
|
30 |
|
|
31 |
val get : ident -> t -> elt |
|
32 |
end |
|
33 |
with type elt = var_decl = struct |
|
34 |
include Set.Make (VDeclModule) |
|
35 |
|
|
36 |
let pp fmt s = |
|
37 |
Format.fprintf fmt "{@[%a}@]" |
|
38 |
(Utils.fprintf_list ~sep:",@ " Printers.pp_var) |
|
39 |
(elements s) |
|
43 | 40 |
|
41 |
(* Strangley the find_first function of Set.Make is incorrect (at the current |
|
42 |
time of writting this comment. Had to switch to lists *) |
|
43 |
let get id s = List.find (fun v -> v.var_id = id) (elements s) |
|
44 |
end |
|
44 | 45 |
|
46 |
let dummy_type_dec = |
|
47 |
{ ty_dec_desc = Tydec_any; ty_dec_loc = Location.dummy_loc } |
|
48 |
|
|
49 |
let dummy_clock_dec = |
|
50 |
{ ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy_loc } |
|
45 | 51 |
|
46 | 52 |
(************************************************************) |
47 | 53 |
(* *) |
48 | 54 |
|
49 |
let mktyp loc d = |
|
50 |
{ ty_dec_desc = d; ty_dec_loc = loc } |
|
55 |
let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc } |
|
51 | 56 |
|
52 |
let mkclock loc d = |
|
53 |
{ ck_dec_desc = d; ck_dec_loc = loc } |
|
57 |
let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc } |
|
54 | 58 |
|
55 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) = |
|
59 |
let mkvar_decl loc ?(orig = false) |
|
60 |
(id, ty_dec, ck_dec, is_const, value, parentid) = |
|
56 | 61 |
assert (value = None || is_const); |
57 |
{ var_id = id; |
|
62 |
{ |
|
63 |
var_id = id; |
|
58 | 64 |
var_orig = orig; |
59 | 65 |
var_dec_type = ty_dec; |
60 | 66 |
var_dec_clock = ck_dec; |
... | ... | |
63 | 69 |
var_parent_nodeid = parentid; |
64 | 70 |
var_type = Types.new_var (); |
65 | 71 |
var_clock = Clocks.new_var true; |
66 |
var_loc = loc } |
|
72 |
var_loc = loc; |
|
73 |
} |
|
67 | 74 |
|
68 | 75 |
let dummy_var_decl name typ = |
69 | 76 |
{ |
... | ... | |
74 | 81 |
var_dec_const = false; |
75 | 82 |
var_dec_value = None; |
76 | 83 |
var_parent_nodeid = None; |
77 |
var_type = typ;
|
|
84 |
var_type = typ; |
|
78 | 85 |
var_clock = Clocks.new_ck Clocks.Cvar true; |
79 |
var_loc = Location.dummy_loc |
|
86 |
var_loc = Location.dummy_loc;
|
|
80 | 87 |
} |
81 | 88 |
|
82 | 89 |
let mkexpr loc d = |
83 |
{ expr_tag = Utils.new_tag (); |
|
90 |
{ |
|
91 |
expr_tag = Utils.new_tag (); |
|
84 | 92 |
expr_desc = d; |
85 | 93 |
expr_type = Types.new_var (); |
86 | 94 |
expr_clock = Clocks.new_var true; |
87 | 95 |
expr_delay = Delay.new_var (); |
88 | 96 |
expr_annot = None; |
89 |
expr_loc = loc } |
|
97 |
expr_loc = loc; |
|
98 |
} |
|
90 | 99 |
|
91 |
let var_decl_of_const ?(parentid=None) c = |
|
92 |
{ var_id = c.const_id; |
|
100 |
let var_decl_of_const ?(parentid = None) c = |
|
101 |
{ |
|
102 |
var_id = c.const_id; |
|
93 | 103 |
var_orig = true; |
94 | 104 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
95 | 105 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
... | ... | |
98 | 108 |
var_parent_nodeid = parentid; |
99 | 109 |
var_type = c.const_type; |
100 | 110 |
var_clock = Clocks.new_var false; |
101 |
var_loc = c.const_loc } |
|
111 |
var_loc = c.const_loc; |
|
112 |
} |
|
102 | 113 |
|
103 | 114 |
let mk_new_name used id = |
104 | 115 |
let rec new_name name cpt = |
105 |
if used name |
|
106 |
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
|
107 |
else name |
|
108 |
in new_name id 1 |
|
109 |
|
|
110 |
let mkeq loc (lhs, rhs) = |
|
111 |
{ eq_lhs = lhs; |
|
112 |
eq_rhs = rhs; |
|
113 |
eq_loc = loc } |
|
114 |
|
|
115 |
let mkassert loc expr = |
|
116 |
{ assert_loc = loc; |
|
117 |
assert_expr = expr |
|
118 |
} |
|
116 |
if used name then new_name (sprintf "_%s_%i" id cpt) (cpt + 1) else name |
|
117 |
in |
|
118 |
new_name id 1 |
|
119 |
|
|
120 |
let mkeq loc (lhs, rhs) = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc } |
|
121 |
|
|
122 |
let mkassert loc expr = { assert_loc = loc; assert_expr = expr } |
|
119 | 123 |
|
120 | 124 |
let mktop_decl loc own itf d = |
121 |
{ top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf } |
|
125 |
{ |
|
126 |
top_decl_desc = d; |
|
127 |
top_decl_loc = loc; |
|
128 |
top_decl_owner = own; |
|
129 |
top_decl_itf = itf; |
|
130 |
} |
|
122 | 131 |
|
123 | 132 |
let mkpredef_call loc funname args = |
124 | 133 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
125 | 134 |
|
126 |
let is_clock_dec_type cty = |
|
127 |
match cty with |
|
128 |
| Tydec_clock _ -> true |
|
129 |
| _ -> false |
|
135 |
let is_clock_dec_type cty = match cty with Tydec_clock _ -> true | _ -> false |
|
130 | 136 |
|
131 | 137 |
let const_of_top top_decl = |
132 |
match top_decl.top_decl_desc with |
|
133 |
| Const c -> c |
|
134 |
| _ -> assert false |
|
138 |
match top_decl.top_decl_desc with Const c -> c | _ -> assert false |
|
135 | 139 |
|
136 | 140 |
let node_of_top top_decl = |
137 |
match top_decl.top_decl_desc with |
|
138 |
| Node nd -> nd |
|
139 |
| _ -> raise Not_found |
|
141 |
match top_decl.top_decl_desc with Node nd -> nd | _ -> raise Not_found |
|
140 | 142 |
|
141 | 143 |
let imported_node_of_top top_decl = |
142 | 144 |
match top_decl.top_decl_desc with |
143 |
| ImportedNode ind -> ind |
|
144 |
| _ -> assert false |
|
145 |
| ImportedNode ind -> |
|
146 |
ind |
|
147 |
| _ -> |
|
148 |
assert false |
|
145 | 149 |
|
146 | 150 |
let typedef_of_top top_decl = |
147 |
match top_decl.top_decl_desc with |
|
148 |
| TypeDef tdef -> tdef |
|
149 |
| _ -> assert false |
|
151 |
match top_decl.top_decl_desc with TypeDef tdef -> tdef | _ -> assert false |
|
150 | 152 |
|
151 | 153 |
let dependency_of_top top_decl = |
152 | 154 |
match top_decl.top_decl_desc with |
153 |
| Open (local, dep) -> (local, dep) |
|
154 |
| _ -> assert false |
|
155 |
| Open (local, dep) -> |
|
156 |
local, dep |
|
157 |
| _ -> |
|
158 |
assert false |
|
155 | 159 |
|
156 | 160 |
let consts_of_enum_type top_decl = |
157 | 161 |
match top_decl.top_decl_desc with |
158 |
| TypeDef tdef -> |
|
159 |
(match tdef.tydef_desc with
|
|
162 |
| TypeDef tdef -> (
|
|
163 |
match tdef.tydef_desc with |
|
160 | 164 |
| Tydec_enum tags -> |
161 |
List.map |
|
162 |
(fun tag -> |
|
163 |
let cdecl = { |
|
164 |
const_id = tag; |
|
165 |
const_loc = top_decl.top_decl_loc; |
|
166 |
const_value = Const_tag tag; |
|
167 |
const_type = Type_predef.type_const tdef.tydef_id |
|
168 |
} in |
|
169 |
{ top_decl with top_decl_desc = Const cdecl }) |
|
170 |
tags |
|
171 |
| _ -> []) |
|
172 |
| _ -> assert false |
|
165 |
List.map |
|
166 |
(fun tag -> |
|
167 |
let cdecl = |
|
168 |
{ |
|
169 |
const_id = tag; |
|
170 |
const_loc = top_decl.top_decl_loc; |
|
171 |
const_value = Const_tag tag; |
|
172 |
const_type = Type_predef.type_const tdef.tydef_id; |
|
173 |
} |
|
174 |
in |
|
175 |
{ top_decl with top_decl_desc = Const cdecl }) |
|
176 |
tags |
|
177 |
| _ -> |
|
178 |
[]) |
|
179 |
| _ -> |
|
180 |
assert false |
|
173 | 181 |
|
174 | 182 |
(************************************************************) |
175 | 183 |
(* Eexpr functions *) |
176 | 184 |
(************************************************************) |
177 | 185 |
|
178 |
|
|
179 | 186 |
let empty_contract = |
180 | 187 |
{ |
181 |
consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc; |
|
188 |
consts = []; |
|
189 |
locals = []; |
|
190 |
stmts = []; |
|
191 |
assume = []; |
|
192 |
guarantees = []; |
|
193 |
modes = []; |
|
194 |
imports = []; |
|
195 |
spec_loc = Location.dummy_loc; |
|
182 | 196 |
} |
183 | 197 |
|
184 |
(* For const declaration we do as for regular lustre node. |
|
185 |
But for local flows we registered the variable and the lustre flow definition *)
|
|
198 |
(* For const declaration we do as for regular lustre node. But for local flows
|
|
199 |
we registered the variable and the lustre flow definition *)
|
|
186 | 200 |
let mk_contract_var id is_const type_opt expr loc = |
187 | 201 |
let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in |
188 | 202 |
if is_const then |
189 |
let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in |
|
190 |
{ empty_contract with consts = [v]; spec_loc = loc; } |
|
203 |
let v = |
|
204 |
mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) |
|
205 |
in |
|
206 |
{ empty_contract with consts = [ v ]; spec_loc = loc } |
|
191 | 207 |
else |
192 |
let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in |
|
193 |
let eq = mkeq loc ([id], expr) in |
|
194 |
{ empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; } |
|
208 |
let v = |
|
209 |
mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) |
|
210 |
in |
|
211 |
let eq = mkeq loc ([ id ], expr) in |
|
212 |
{ empty_contract with locals = [ v ]; stmts = [ Eq eq ]; spec_loc = loc } |
|
195 | 213 |
|
196 |
let eexpr_add_name eexpr eexpr_name = |
|
197 |
{ eexpr with eexpr_name } |
|
214 |
let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name } |
|
198 | 215 |
|
199 | 216 |
let mk_contract_guarantees name eexpr = |
200 |
{ empty_contract with guarantees = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc } |
|
217 |
{ |
|
218 |
empty_contract with |
|
219 |
guarantees = [ eexpr_add_name eexpr name ]; |
|
220 |
spec_loc = eexpr.eexpr_loc; |
|
221 |
} |
|
201 | 222 |
|
202 | 223 |
let mk_contract_assume name eexpr = |
203 |
{ empty_contract with assume = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc } |
|
224 |
{ |
|
225 |
empty_contract with |
|
226 |
assume = [ eexpr_add_name eexpr name ]; |
|
227 |
spec_loc = eexpr.eexpr_loc; |
|
228 |
} |
|
204 | 229 |
|
205 | 230 |
let mk_contract_mode id rl el loc = |
206 |
{ empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc } |
|
231 |
{ |
|
232 |
empty_contract with |
|
233 |
modes = [ { mode_id = id; require = rl; ensure = el; mode_loc = loc } ]; |
|
234 |
spec_loc = loc; |
|
235 |
} |
|
207 | 236 |
|
208 | 237 |
let mk_contract_import id ins outs loc = |
209 |
{ empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc } |
|
238 |
{ |
|
239 |
empty_contract with |
|
240 |
imports = |
|
241 |
[ { import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc } ]; |
|
242 |
spec_loc = loc; |
|
243 |
} |
|
210 | 244 |
|
211 |
|
|
212 |
let merge_contracts ann1 ann2 = (* keeping the first item loc *) |
|
213 |
{ consts = ann1.consts @ ann2.consts; |
|
245 |
let merge_contracts ann1 ann2 = |
|
246 |
(* keeping the first item loc *) |
|
247 |
{ |
|
248 |
consts = ann1.consts @ ann2.consts; |
|
214 | 249 |
locals = ann1.locals @ ann2.locals; |
215 | 250 |
stmts = ann1.stmts @ ann2.stmts; |
216 | 251 |
assume = ann1.assume @ ann2.assume; |
217 | 252 |
guarantees = ann1.guarantees @ ann2.guarantees; |
218 | 253 |
modes = ann1.modes @ ann2.modes; |
219 | 254 |
imports = ann1.imports @ ann2.imports; |
220 |
spec_loc = ann1.spec_loc |
|
255 |
spec_loc = ann1.spec_loc;
|
|
221 | 256 |
} |
222 | 257 |
|
223 | 258 |
let mkeexpr loc expr = |
224 |
{ eexpr_tag = Utils.new_tag (); |
|
259 |
{ |
|
260 |
eexpr_tag = Utils.new_tag (); |
|
225 | 261 |
eexpr_qfexpr = expr; |
226 | 262 |
eexpr_quantifiers = []; |
227 | 263 |
eexpr_name = None; |
228 | 264 |
eexpr_type = Types.new_var (); |
229 | 265 |
eexpr_clock = Clocks.new_var true; |
230 |
eexpr_loc = loc } |
|
266 |
eexpr_loc = loc; |
|
267 |
} |
|
231 | 268 |
|
232 |
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
|
|
269 |
let extend_eexpr q e = { e with eexpr_quantifiers = q @ e.eexpr_quantifiers }
|
|
233 | 270 |
|
234 |
(* |
|
235 |
let mkepredef_call loc funname args = |
|
236 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
|
271 |
(* let mkepredef_call loc funname args = mkeexpr loc (EExpr_appl (funname, |
|
272 |
mkeexpr loc (EExpr_tuple args), None)) |
|
237 | 273 |
|
238 |
let mkepredef_unary_call loc funname arg = |
|
239 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
|
240 |
*) |
|
274 |
let mkepredef_unary_call loc funname arg = mkeexpr loc (EExpr_appl (funname, |
|
275 |
arg, None)) *) |
|
241 | 276 |
|
242 | 277 |
let merge_expr_annot ann1 ann2 = |
243 | 278 |
match ann1, ann2 with |
244 |
| None, None -> assert false |
|
245 |
| Some _, None -> ann1 |
|
246 |
| None, Some _ -> ann2 |
|
247 |
| Some ann1, Some ann2 -> Some { |
|
248 |
annots = ann1.annots @ ann2.annots; |
|
249 |
annot_loc = ann1.annot_loc |
|
250 |
} |
|
279 |
| None, None -> |
|
280 |
assert false |
|
281 |
| Some _, None -> |
|
282 |
ann1 |
|
283 |
| None, Some _ -> |
|
284 |
ann2 |
|
285 |
| Some ann1, Some ann2 -> |
|
286 |
Some { annots = ann1.annots @ ann2.annots; annot_loc = ann1.annot_loc } |
|
251 | 287 |
|
252 | 288 |
let update_expr_annot node_id e annot = |
253 |
List.iter (fun (key, _) ->
|
|
254 |
Annotations.add_expr_ann node_id e.expr_tag key
|
|
255 |
) annot.annots;
|
|
289 |
List.iter |
|
290 |
(fun (key, _) -> Annotations.add_expr_ann node_id e.expr_tag key)
|
|
291 |
annot.annots;
|
|
256 | 292 |
e.expr_annot <- merge_expr_annot e.expr_annot (Some annot); |
257 | 293 |
e |
258 | 294 |
|
259 |
|
|
260 |
let mkinstr ?lustre_eq ?(instr_spec=[]) instr_desc = { |
|
261 |
instr_desc; |
|
262 |
(* lustre_expr = lustre_expr; *) |
|
263 |
instr_spec; |
|
264 |
lustre_eq; |
|
265 |
} |
|
295 |
let mkinstr ?lustre_eq ?(instr_spec = []) instr_desc = |
|
296 |
{ instr_desc; (* lustre_expr = lustre_expr; *) |
|
297 |
instr_spec; lustre_eq } |
|
266 | 298 |
|
267 | 299 |
let get_instr_desc i = i.instr_desc |
300 |
|
|
268 | 301 |
let update_instr_desc i id = { i with instr_desc = id } |
269 | 302 |
|
270 | 303 |
(***********************************************************) |
271 | 304 |
(* Fast access to nodes, by name *) |
272 | 305 |
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
306 |
|
|
273 | 307 |
let consts_table = Hashtbl.create 30 |
274 | 308 |
|
275 | 309 |
let print_node_table fmt () = |
276 |
begin |
|
277 |
Format.fprintf fmt "{ /* node table */@."; |
|
278 |
Hashtbl.iter (fun id nd -> |
|
279 |
Format.fprintf fmt "%s |-> %a" |
|
280 |
id |
|
281 |
Printers.pp_short_decl nd |
|
282 |
) node_table; |
|
283 |
Format.fprintf fmt "}@." |
|
284 |
end |
|
310 |
Format.fprintf fmt "{ /* node table */@."; |
|
311 |
Hashtbl.iter |
|
312 |
(fun id nd -> Format.fprintf fmt "%s |-> %a" id Printers.pp_short_decl nd) |
|
313 |
node_table; |
|
314 |
Format.fprintf fmt "}@." |
|
285 | 315 |
|
286 | 316 |
let print_consts_table fmt () = |
287 |
begin |
|
288 |
Format.fprintf fmt "{ /* consts table */@."; |
|
289 |
Hashtbl.iter (fun id const -> |
|
290 |
Format.fprintf fmt "%s |-> %a" |
|
291 |
id |
|
292 |
Printers.pp_const_decl (const_of_top const) |
|
293 |
) consts_table; |
|
294 |
Format.fprintf fmt "}@." |
|
295 |
end |
|
317 |
Format.fprintf fmt "{ /* consts table */@."; |
|
318 |
Hashtbl.iter |
|
319 |
(fun id const -> |
|
320 |
Format.fprintf fmt "%s |-> %a" id Printers.pp_const_decl |
|
321 |
(const_of_top const)) |
|
322 |
consts_table; |
|
323 |
Format.fprintf fmt "}@." |
|
296 | 324 |
|
297 | 325 |
let node_name td = |
298 |
match td.top_decl_desc with |
|
299 |
| Node nd -> nd.node_id |
|
300 |
| ImportedNode nd -> nd.nodei_id |
|
301 |
| _ -> assert false |
|
326 |
match td.top_decl_desc with |
|
327 |
| Node nd -> |
|
328 |
nd.node_id |
|
329 |
| ImportedNode nd -> |
|
330 |
nd.nodei_id |
|
331 |
| _ -> |
|
332 |
assert false |
|
302 | 333 |
|
303 | 334 |
let is_generic_node td = |
304 |
match td.top_decl_desc with |
|
305 |
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
|
306 |
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
|
307 |
| _ -> assert false |
|
335 |
match td.top_decl_desc with |
|
336 |
| Node nd -> |
|
337 |
List.exists (fun v -> v.var_dec_const) nd.node_inputs |
|
338 |
| ImportedNode nd -> |
|
339 |
List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
|
340 |
| _ -> |
|
341 |
assert false |
|
308 | 342 |
|
309 | 343 |
let node_inputs td = |
310 |
match td.top_decl_desc with |
|
311 |
| Node nd -> nd.node_inputs |
|
312 |
| ImportedNode nd -> nd.nodei_inputs |
|
313 |
| _ -> assert false |
|
344 |
match td.top_decl_desc with |
|
345 |
| Node nd -> |
|
346 |
nd.node_inputs |
|
347 |
| ImportedNode nd -> |
|
348 |
nd.nodei_inputs |
|
349 |
| _ -> |
|
350 |
assert false |
|
351 |
|
|
352 |
let node_from_name id = Hashtbl.find node_table id |
|
314 | 353 |
|
315 |
let node_from_name id = |
|
316 |
Hashtbl.find node_table id |
|
317 |
|
|
318 |
let update_node id top = |
|
319 |
Hashtbl.replace node_table id top |
|
354 |
let update_node id top = Hashtbl.replace node_table id top |
|
320 | 355 |
|
321 | 356 |
let is_imported_node td = |
322 |
match td.top_decl_desc with |
|
323 |
| Node _ -> false |
|
324 |
| ImportedNode _ -> true |
|
325 |
| _ -> assert false |
|
357 |
match td.top_decl_desc with |
|
358 |
| Node _ -> |
|
359 |
false |
|
360 |
| ImportedNode _ -> |
|
361 |
true |
|
362 |
| _ -> |
|
363 |
assert false |
|
326 | 364 |
|
327 | 365 |
let is_node_contract nd = |
328 |
match nd.node_spec with |
|
329 |
| Some (Contract _) -> true |
|
330 |
| _ -> false |
|
331 |
|
|
366 |
match nd.node_spec with Some (Contract _) -> true | _ -> false |
|
367 |
|
|
332 | 368 |
let get_node_contract nd = |
333 |
match nd.node_spec with |
|
334 |
| Some (Contract c) -> c |
|
335 |
| _ -> assert false |
|
336 |
|
|
369 |
match nd.node_spec with Some (Contract c) -> c | _ -> assert false |
|
370 |
|
|
337 | 371 |
let is_contract td = |
338 |
match td.top_decl_desc with |
|
339 |
| Node nd -> is_node_contract nd |
|
340 |
| _ -> false |
|
372 |
match td.top_decl_desc with Node nd -> is_node_contract nd | _ -> false |
|
341 | 373 |
|
342 | 374 |
(* alias and type definition table *) |
343 | 375 |
|
344 | 376 |
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false |
345 | 377 |
|
346 |
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) |
|
347 |
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) |
|
348 |
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *) |
|
349 |
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real}) |
|
378 |
let top_int_type = mktop (TypeDef { tydef_id = "int"; tydef_desc = Tydec_int }) |
|
379 |
|
|
380 |
let top_bool_type = |
|
381 |
mktop (TypeDef { tydef_id = "bool"; tydef_desc = Tydec_bool }) |
|
382 |
|
|
383 |
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = |
|
384 |
Tydec_float}) *) |
|
385 |
let top_real_type = |
|
386 |
mktop (TypeDef { tydef_id = "real"; tydef_desc = Tydec_real }) |
|
350 | 387 |
|
351 | 388 |
let type_table = |
352 |
Utils.create_hashtable 20 [ |
|
353 |
Tydec_int , top_int_type; |
|
354 |
Tydec_bool , top_bool_type; |
|
355 |
(* Tydec_float, top_float_type; *) |
|
356 |
Tydec_real , top_real_type |
|
357 |
] |
|
389 |
Utils.create_hashtable 20 |
|
390 |
[ |
|
391 |
Tydec_int, top_int_type; |
|
392 |
Tydec_bool, top_bool_type; |
|
393 |
(* Tydec_float, top_float_type; *) |
|
394 |
Tydec_real, top_real_type; |
|
395 |
] |
|
358 | 396 |
|
359 | 397 |
let print_type_table fmt () = |
360 |
begin |
|
361 |
Format.fprintf fmt "{ /* type table */@."; |
|
362 |
Hashtbl.iter (fun tydec tdef -> |
|
363 |
Format.fprintf fmt "%a |-> %a" |
|
364 |
Printers.pp_var_type_dec_desc tydec |
|
365 |
Printers.pp_typedef (typedef_of_top tdef) |
|
366 |
) type_table; |
|
367 |
Format.fprintf fmt "}@." |
|
368 |
end |
|
398 |
Format.fprintf fmt "{ /* type table */@."; |
|
399 |
Hashtbl.iter |
|
400 |
(fun tydec tdef -> |
|
401 |
Format.fprintf fmt "%a |-> %a" Printers.pp_var_type_dec_desc tydec |
|
402 |
Printers.pp_typedef (typedef_of_top tdef)) |
|
403 |
type_table; |
|
404 |
Format.fprintf fmt "}@." |
|
369 | 405 |
|
370 | 406 |
let rec is_user_type typ = |
371 | 407 |
match typ with |
372 |
| Tydec_int | Tydec_bool | Tydec_real |
|
373 |
(* | Tydec_float *) | Tydec_any | Tydec_const _ -> false |
|
374 |
| Tydec_clock typ' -> is_user_type typ' |
|
375 |
| _ -> true |
|
408 |
| Tydec_int |
|
409 |
| Tydec_bool |
|
410 |
| Tydec_real (* | Tydec_float *) |
|
411 |
| Tydec_any |
|
412 |
| Tydec_const _ -> |
|
413 |
false |
|
414 |
| Tydec_clock typ' -> |
|
415 |
is_user_type typ' |
|
416 |
| _ -> |
|
417 |
true |
|
376 | 418 |
|
377 | 419 |
let get_repr_type typ = |
378 | 420 |
let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in |
... | ... | |
380 | 422 |
|
381 | 423 |
let rec coretype_equal ty1 ty2 = |
382 | 424 |
let res = |
383 |
match ty1, ty2 with |
|
384 |
| Tydec_any , _ |
|
385 |
| _ , Tydec_any -> assert false |
|
386 |
| Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2 |
|
387 |
| Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc |
|
388 |
in (not (is_user_type ty1')) && coretype_equal ty1' ty2 |
|
389 |
| _ , Tydec_const _ -> coretype_equal ty2 ty1 |
|
390 |
| Tydec_int , Tydec_int |
|
391 |
| Tydec_real , Tydec_real |
|
392 |
(* | Tydec_float , Tydec_float *) |
|
393 |
| Tydec_bool , Tydec_bool -> true |
|
394 |
| Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2 |
|
395 |
| Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2 |
|
396 |
| Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2 |
|
397 |
| Tydec_struct fl1 , Tydec_struct fl2 -> |
|
398 |
List.length fl1 = List.length fl2 |
|
399 |
&& List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2) |
|
400 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1) |
|
401 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2) |
|
402 |
| _ -> false |
|
403 |
in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res) |
|
425 |
match ty1, ty2 with |
|
426 |
| Tydec_any, _ | _, Tydec_any -> |
|
427 |
assert false |
|
428 |
| Tydec_const _, Tydec_const _ -> |
|
429 |
get_repr_type ty1 = get_repr_type ty2 |
|
430 |
| Tydec_const _, _ -> |
|
431 |
let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc in |
|
432 |
(not (is_user_type ty1')) && coretype_equal ty1' ty2 |
|
433 |
| _, Tydec_const _ -> |
|
434 |
coretype_equal ty2 ty1 |
|
435 |
| Tydec_int, Tydec_int |
|
436 |
| Tydec_real, Tydec_real |
|
437 |
(* | Tydec_float , Tydec_float *) |
|
438 |
| Tydec_bool, Tydec_bool -> |
|
439 |
true |
|
440 |
| Tydec_clock ty1, Tydec_clock ty2 -> |
|
441 |
coretype_equal ty1 ty2 |
|
442 |
| Tydec_array (d1, ty1), Tydec_array (d2, ty2) -> |
|
443 |
Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2 |
|
444 |
| Tydec_enum tl1, Tydec_enum tl2 -> |
|
445 |
List.sort compare tl1 = List.sort compare tl2 |
|
446 |
| Tydec_struct fl1, Tydec_struct fl2 -> |
|
447 |
List.length fl1 = List.length fl2 |
|
448 |
&& List.for_all2 |
|
449 |
(fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2) |
|
450 |
(List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl1) |
|
451 |
(List.sort (fun (f1, _) (f2, _) -> compare f1 f2) fl2) |
|
452 |
| _ -> |
|
453 |
false |
|
454 |
in |
|
455 |
(*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc |
|
456 |
ty1 Printers.pp_var_type_dec_desc ty2 res;*) |
|
457 |
res |
|
404 | 458 |
|
405 | 459 |
let tag_default = "default" |
406 | 460 |
|
407 | 461 |
let const_is_bool c = |
408 |
match c with |
|
409 |
| Const_tag t -> t = tag_true || t = tag_false |
|
410 |
| _ -> false |
|
462 |
match c with Const_tag t -> t = tag_true || t = tag_false | _ -> false |
|
411 | 463 |
|
412 | 464 |
(* Computes the negation of a boolean constant *) |
413 | 465 |
let const_negation c = |
414 | 466 |
assert (const_is_bool c); |
415 | 467 |
match c with |
416 |
| Const_tag t when t = tag_true -> Const_tag tag_false |
|
417 |
| _ -> Const_tag tag_true |
|
468 |
| Const_tag t when t = tag_true -> |
|
469 |
Const_tag tag_false |
|
470 |
| _ -> |
|
471 |
Const_tag tag_true |
|
418 | 472 |
|
419 | 473 |
let const_or c1 c2 = |
420 | 474 |
assert (const_is_bool c1 && const_is_bool c2); |
421 | 475 |
match c1, c2 with |
422 |
| Const_tag t1, _ when t1 = tag_true -> c1 |
|
423 |
| _ , Const_tag t2 when t2 = tag_true -> c2 |
|
424 |
| _ -> Const_tag tag_false |
|
476 |
| Const_tag t1, _ when t1 = tag_true -> |
|
477 |
c1 |
|
478 |
| _, Const_tag t2 when t2 = tag_true -> |
|
479 |
c2 |
|
480 |
| _ -> |
|
481 |
Const_tag tag_false |
|
425 | 482 |
|
426 | 483 |
let const_and c1 c2 = |
427 | 484 |
assert (const_is_bool c1 && const_is_bool c2); |
428 | 485 |
match c1, c2 with |
429 |
| Const_tag t1, _ when t1 = tag_false -> c1 |
|
430 |
| _ , Const_tag t2 when t2 = tag_false -> c2 |
|
431 |
| _ -> Const_tag tag_true |
|
486 |
| Const_tag t1, _ when t1 = tag_false -> |
|
487 |
c1 |
|
488 |
| _, Const_tag t2 when t2 = tag_false -> |
|
489 |
c2 |
|
490 |
| _ -> |
|
491 |
Const_tag tag_true |
|
432 | 492 |
|
433 | 493 |
let const_xor c1 c2 = |
434 | 494 |
assert (const_is_bool c1 && const_is_bool c2); |
435 |
match c1, c2 with |
|
436 |
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
|
437 |
| _ -> Const_tag tag_false |
|
495 |
match c1, c2 with |
|
496 |
| Const_tag t1, Const_tag t2 when t1 <> t2 -> |
|
497 |
Const_tag tag_true |
|
498 |
| _ -> |
|
499 |
Const_tag tag_false |
|
438 | 500 |
|
439 | 501 |
let const_impl c1 c2 = |
440 | 502 |
assert (const_is_bool c1 && const_is_bool c2); |
441 | 503 |
match c1, c2 with |
442 |
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
|
443 |
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
|
444 |
| _ -> Const_tag tag_false |
|
504 |
| Const_tag t1, _ when t1 = tag_false -> |
|
505 |
Const_tag tag_true |
|
506 |
| _, Const_tag t2 when t2 = tag_true -> |
|
507 |
Const_tag tag_true |
|
508 |
| _ -> |
|
509 |
Const_tag tag_false |
|
445 | 510 |
|
446 | 511 |
(* To guarantee uniqueness of tags in enum types *) |
447 | 512 |
let tag_table = |
448 |
Utils.create_hashtable 20 [ |
|
449 |
tag_true, top_bool_type; |
|
450 |
tag_false, top_bool_type |
|
451 |
] |
|
513 |
Utils.create_hashtable 20 |
|
514 |
[ tag_true, top_bool_type; tag_false, top_bool_type ] |
|
452 | 515 |
|
453 | 516 |
(* To guarantee uniqueness of fields in struct types *) |
454 |
let field_table = |
|
455 |
Utils.create_hashtable 20 [ |
|
456 |
] |
|
517 |
let field_table = Utils.create_hashtable 20 [] |
|
457 | 518 |
|
458 | 519 |
let get_enum_type_tags cty = |
459 |
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*) |
|
460 |
match cty with |
|
461 |
| Tydec_bool -> [tag_true; tag_false] |
|
462 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
463 |
| Tydec_enum tl -> tl |
|
464 |
| _ -> assert false) |
|
465 |
| _ -> assert false |
|
520 |
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*) |
|
521 |
match cty with |
|
522 |
| Tydec_bool -> |
|
523 |
[ tag_true; tag_false ] |
|
524 |
| Tydec_const _ -> ( |
|
525 |
match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
526 |
| Tydec_enum tl -> |
|
527 |
tl |
|
528 |
| _ -> |
|
529 |
assert false) |
|
530 |
| _ -> |
|
531 |
assert false |
|
466 | 532 |
|
467 | 533 |
let get_struct_type_fields cty = |
468 |
match cty with |
|
469 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
470 |
| Tydec_struct fl -> fl |
|
471 |
| _ -> assert false) |
|
472 |
| _ -> assert false |
|
534 |
match cty with |
|
535 |
| Tydec_const _ -> ( |
|
536 |
match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
537 |
| Tydec_struct fl -> |
|
538 |
fl |
|
539 |
| _ -> |
|
540 |
assert false) |
|
541 |
| _ -> |
|
542 |
assert false |
|
473 | 543 |
|
474 |
let const_of_bool b = |
|
475 |
Const_tag (if b then tag_true else tag_false) |
|
544 |
let const_of_bool b = Const_tag (if b then tag_true else tag_false) |
|
476 | 545 |
|
477 | 546 |
(* let get_const c = snd (Hashtbl.find consts_table c) *) |
478 | 547 |
|
479 | 548 |
let ident_of_expr expr = |
480 |
match expr.expr_desc with |
|
481 |
| Expr_ident id -> id |
|
482 |
| _ -> assert false |
|
549 |
match expr.expr_desc with Expr_ident id -> id | _ -> assert false |
|
483 | 550 |
|
484 | 551 |
(* Generate a new ident expression from a declared variable *) |
485 | 552 |
let expr_of_vdecl v = |
486 |
{ expr_tag = Utils.new_tag (); |
|
553 |
{ |
|
554 |
expr_tag = Utils.new_tag (); |
|
487 | 555 |
expr_desc = Expr_ident v.var_id; |
488 | 556 |
expr_type = v.var_type; |
489 | 557 |
expr_clock = v.var_clock; |
490 | 558 |
expr_delay = Delay.new_var (); |
491 | 559 |
expr_annot = None; |
492 |
expr_loc = v.var_loc } |
|
560 |
expr_loc = v.var_loc; |
|
561 |
} |
|
493 | 562 |
|
494 | 563 |
(* Caution, returns an untyped and unclocked expression *) |
495 | 564 |
let expr_of_ident id loc = |
496 |
{expr_tag = Utils.new_tag (); |
|
497 |
expr_desc = Expr_ident id; |
|
498 |
expr_type = Types.new_var (); |
|
499 |
expr_clock = Clocks.new_var true; |
|
500 |
expr_delay = Delay.new_var (); |
|
501 |
expr_loc = loc; |
|
502 |
expr_annot = None} |
|
565 |
{ |
|
566 |
expr_tag = Utils.new_tag (); |
|
567 |
expr_desc = Expr_ident id; |
|
568 |
expr_type = Types.new_var (); |
|
569 |
expr_clock = Clocks.new_var true; |
|
570 |
expr_delay = Delay.new_var (); |
|
571 |
expr_loc = loc; |
|
572 |
expr_annot = None; |
|
573 |
} |
|
503 | 574 |
|
504 | 575 |
let is_tuple_expr expr = |
505 |
match expr.expr_desc with |
|
506 |
| Expr_tuple _ -> true |
|
507 |
| _ -> false |
|
576 |
match expr.expr_desc with Expr_tuple _ -> true | _ -> false |
|
508 | 577 |
|
509 | 578 |
let expr_list_of_expr expr = |
510 |
match expr.expr_desc with |
|
511 |
| Expr_tuple elist -> elist |
|
512 |
| _ -> [expr] |
|
579 |
match expr.expr_desc with Expr_tuple elist -> elist | _ -> [ expr ] |
|
513 | 580 |
|
514 | 581 |
let expr_of_expr_list loc elist = |
515 |
match elist with |
|
516 |
| [t] -> { t with expr_loc = loc } |
|
517 |
| t::_ -> |
|
582 |
match elist with |
|
583 |
| [ t ] -> |
|
584 |
{ t with expr_loc = loc } |
|
585 |
| t :: _ -> |
|
518 | 586 |
let tlist = List.map (fun e -> e.expr_type) elist in |
519 | 587 |
let clist = List.map (fun e -> e.expr_clock) elist in |
520 |
{ t with expr_desc = Expr_tuple elist; |
|
521 |
expr_type = Type_predef.type_tuple tlist; |
|
522 |
expr_clock = Clock_predef.ck_tuple clist; |
|
523 |
expr_tag = Utils.new_tag (); |
|
524 |
expr_loc = loc } |
|
525 |
| _ -> assert false |
|
588 |
{ |
|
589 |
t with |
|
590 |
expr_desc = Expr_tuple elist; |
|
591 |
expr_type = Type_predef.type_tuple tlist; |
|
592 |
expr_clock = Clock_predef.ck_tuple clist; |
|
593 |
expr_tag = Utils.new_tag (); |
|
594 |
expr_loc = loc; |
|
595 |
} |
|
596 |
| _ -> |
|
597 |
assert false |
|
526 | 598 |
|
527 | 599 |
let call_of_expr expr = |
528 |
match expr.expr_desc with |
|
529 |
| Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r) |
|
530 |
| _ -> assert false |
|
600 |
match expr.expr_desc with |
|
601 |
| Expr_appl (f, args, r) -> |
|
602 |
f, expr_list_of_expr args, r |
|
603 |
| _ -> |
|
604 |
assert false |
|
531 | 605 |
|
532 |
|
|
533 |
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
|
|
606 |
(* Conversion from dimension expr to standard expr, for the purpose of printing, |
|
607 |
typing, etc... *)
|
|
534 | 608 |
let rec expr_of_dimension dim = |
535 | 609 |
let open Dimension in |
536 | 610 |
let expr = |
537 |
match dim.dim_desc with |
|
538 |
| Dbool b -> |
|
539 |
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
|
540 |
| Dint i -> |
|
541 |
mkexpr dim.dim_loc (Expr_const (Const_int i)) |
|
542 |
| Dident id -> |
|
543 |
mkexpr dim.dim_loc (Expr_ident id) |
|
544 |
| Dite (c, t, e) -> |
|
545 |
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
|
546 |
| Dappl (id, args) -> |
|
547 |
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) |
|
548 |
| Dlink dim' -> expr_of_dimension dim' |
|
549 |
| Dvar |
|
550 |
| Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim; |
|
551 |
assert false) |
|
611 |
match dim.dim_desc with |
|
612 |
| Dbool b -> |
|
613 |
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
|
614 |
| Dint i -> |
|
615 |
mkexpr dim.dim_loc (Expr_const (Const_int i)) |
|
616 |
| Dident id -> |
|
617 |
mkexpr dim.dim_loc (Expr_ident id) |
|
618 |
| Dite (c, t, e) -> |
|
619 |
mkexpr dim.dim_loc |
|
620 |
(Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
|
621 |
| Dappl (id, args) -> |
|
622 |
mkexpr dim.dim_loc |
|
623 |
(Expr_appl |
|
624 |
( id, |
|
625 |
expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), |
|
626 |
None )) |
|
627 |
| Dlink dim' -> |
|
628 |
expr_of_dimension dim' |
|
629 |
| Dvar | Dunivar -> |
|
630 |
Format.eprintf "internal error: Corelang.expr_of_dimension %a@." |
|
631 |
Dimension.pp_dimension dim; |
|
632 |
assert false |
|
552 | 633 |
in |
553 |
{ expr |
|
554 |
with |
|
555 |
expr_type = Types.new_ty Types.type_int; |
|
556 |
} |
|
557 |
|
|
634 |
{ expr with expr_type = Types.new_ty Types.type_int } |
|
635 |
|
|
558 | 636 |
let dimension_of_const loc const = |
559 | 637 |
let open Dimension in |
560 |
match const with |
|
561 |
| Const_int i -> mkdim_int loc i |
|
562 |
| Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true) |
|
563 |
| _ -> raise InvalidDimension |
|
564 |
|
|
565 |
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments |
|
566 |
into dimension expressions *) |
|
638 |
match const with |
|
639 |
| Const_int i -> |
|
640 |
mkdim_int loc i |
|
641 |
| Const_tag t when t = tag_true || t = tag_false -> |
|
642 |
mkdim_bool loc (t = tag_true) |
|
643 |
| _ -> |
|
644 |
raise InvalidDimension |
|
645 |
|
|
646 |
(* Conversion from standard expr to dimension expr, for the purpose of injecting |
|
647 |
static call arguments into dimension expressions *) |
|
567 | 648 |
let rec dimension_of_expr expr = |
568 | 649 |
let open Dimension in |
569 | 650 |
match expr.expr_desc with |
570 |
| Expr_const c -> dimension_of_const expr.expr_loc c |
|
571 |
| Expr_ident id -> mkdim_ident expr.expr_loc id |
|
651 |
| Expr_const c -> |
|
652 |
dimension_of_const expr.expr_loc c |
|
653 |
| Expr_ident id -> |
|
654 |
mkdim_ident expr.expr_loc id |
|
572 | 655 |
| Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr -> |
573 |
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in |
|
574 |
if k = None then raise InvalidDimension; |
|
575 |
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) |
|
576 |
| Expr_ite (i, t, e) -> |
|
577 |
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) |
|
578 |
| _ -> raise InvalidDimension (* not a simple dimension expression *) |
|
579 |
|
|
580 |
|
|
581 |
let sort_handlers hl = |
|
582 |
List.sort (fun (t, _) (t', _) -> compare t t') hl |
|
656 |
let k = |
|
657 |
Types.get_static_value (Env.lookup_value Basic_library.type_env f) |
|
658 |
in |
|
659 |
if k = None then raise InvalidDimension; |
|
660 |
mkdim_appl expr.expr_loc f |
|
661 |
(List.map dimension_of_expr (expr_list_of_expr args)) |
|
662 |
| Expr_ite (i, t, e) -> |
|
663 |
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) |
|
664 |
(dimension_of_expr e) |
|
665 |
| _ -> |
|
666 |
raise InvalidDimension |
|
667 |
(* not a simple dimension expression *) |
|
668 |
|
|
669 |
let sort_handlers hl = List.sort (fun (t, _) (t', _) -> compare t t') hl |
|
583 | 670 |
|
584 |
|
|
585 | 671 |
let rec is_eq_const c1 c2 = |
586 | 672 |
match c1, c2 with |
587 |
| Const_real r1, Const_real _ |
|
588 |
-> Real.eq r1 r1 |
|
589 |
| Const_struct lcl1, Const_struct lcl2 |
|
590 |
-> List.length lcl1 = List.length lcl2 |
|
591 |
&& List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2 |
|
592 |
| _ -> c1 = c2 |
|
593 |
|
|
594 |
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with |
|
595 |
| Expr_const c1, Expr_const c2 -> is_eq_const c1 c2 |
|
596 |
| Expr_ident i1, Expr_ident i2 -> i1 = i2 |
|
597 |
| Expr_array el1, Expr_array el2 |
|
598 |
| Expr_tuple el1, Expr_tuple el2 -> |
|
599 |
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
|
600 |
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
|
601 |
| Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
|
602 |
| Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2 |
|
603 |
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *) |
|
673 |
| Const_real r1, Const_real _ -> |
|
674 |
Real.eq r1 r1 |
|
675 |
| Const_struct lcl1, Const_struct lcl2 -> |
|
676 |
List.length lcl1 = List.length lcl2 |
|
677 |
&& List.for_all2 |
|
678 |
(fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) |
|
679 |
lcl1 lcl2 |
|
680 |
| _ -> |
|
681 |
c1 = c2 |
|
682 |
|
|
683 |
let rec is_eq_expr e1 e2 = |
|
684 |
match e1.expr_desc, e2.expr_desc with |
|
685 |
| Expr_const c1, Expr_const c2 -> |
|
686 |
is_eq_const c1 c2 |
|
687 |
| Expr_ident i1, Expr_ident i2 -> |
|
688 |
i1 = i2 |
|
689 |
| Expr_array el1, Expr_array el2 | Expr_tuple el1, Expr_tuple el2 -> |
|
690 |
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
|
691 |
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> |
|
692 |
is_eq_expr e1 e1' && is_eq_expr e2 e2' |
|
693 |
| Expr_fby (e1, e2), Expr_fby (e1', e2') -> |
|
694 |
is_eq_expr e1 e1' && is_eq_expr e2 e2' |
|
695 |
| Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> |
|
696 |
is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2 |
|
697 |
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && |
|
698 |
is_eq_expr e2 e2' *) |
|
604 | 699 |
(* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *) |
605 |
| Expr_pre e, Expr_pre e' -> is_eq_expr e e' |
|
606 |
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
|
607 |
| Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl') |
|
608 |
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
|
700 |
| Expr_pre e, Expr_pre e' -> |
|
701 |
is_eq_expr e e' |
|
702 |
| Expr_when (e, i, l), Expr_when (e', i', l') -> |
|
703 |
l = l' && i = i' && is_eq_expr e e' |
|
704 |
| Expr_merge (i, hl), Expr_merge (i', hl') -> |
|
705 |
i = i' |
|
706 |
&& List.for_all2 |
|
707 |
(fun (t, h) (t', h') -> t = t' && is_eq_expr h h') |
|
708 |
(sort_handlers hl) (sort_handlers hl') |
|
709 |
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> |
|
710 |
i = i' && r = r' && is_eq_expr e e' |
|
609 | 711 |
| Expr_power (e1, i1), Expr_power (e2, i2) |
610 |
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
|
611 |
| _ -> false |
|
712 |
| Expr_access (e1, i1), Expr_access (e2, i2) -> |
|
713 |
is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
|
714 |
| _ -> |
|
715 |
false |
|
612 | 716 |
|
613 |
let get_node_vars nd = |
|
614 |
nd.node_inputs @ nd.node_locals @ nd.node_outputs |
|
717 |
let get_node_vars nd = nd.node_inputs @ nd.node_locals @ nd.node_outputs |
|
615 | 718 |
|
616 | 719 |
let mk_new_node_name nd id = |
617 | 720 |
let used_vars = get_node_vars nd in |
618 | 721 |
let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in |
619 | 722 |
mk_new_name used id |
620 | 723 |
|
621 |
let get_var id var_list = |
|
622 |
List.find (fun v -> v.var_id = id) var_list |
|
724 |
let get_var id var_list = List.find (fun v -> v.var_id = id) var_list |
|
623 | 725 |
|
624 | 726 |
let get_node_var id node = |
625 |
try |
|
626 |
get_var id (get_node_vars node)
|
|
627 |
with Not_found -> begin
|
|
628 |
(* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
|
|
727 |
try get_var id (get_node_vars node)
|
|
728 |
with Not_found ->
|
|
729 |
(* Format.eprintf "Unable to find variable %s in node %s@.@?" id
|
|
730 |
node.node_id; *)
|
|
629 | 731 |
raise Not_found |
630 |
end |
|
631 |
|
|
632 | 732 |
|
633 | 733 |
let get_node_eqs = |
634 | 734 |
let get_eqs stmts = |
635 | 735 |
List.fold_right |
636 | 736 |
(fun stmt (res_eq, res_aut) -> |
637 |
match stmt with |
|
638 |
| Eq eq -> eq :: res_eq, res_aut |
|
639 |
| Aut aut -> res_eq, aut::res_aut) |
|
640 |
stmts |
|
641 |
([], []) in |
|
737 |
match stmt with |
|
738 |
| Eq eq -> |
|
739 |
eq :: res_eq, res_aut |
|
740 |
| Aut aut -> |
|
741 |
res_eq, aut :: res_aut) |
|
742 |
stmts ([], []) |
|
743 |
in |
|
642 | 744 |
let table_eqs = Hashtbl.create 23 in |
643 |
(fun nd ->
|
|
745 |
fun nd -> |
|
644 | 746 |
try |
645 |
let (old, res) = Hashtbl.find table_eqs nd.node_id
|
|
646 |
in if old == nd.node_stmts then res else raise Not_found
|
|
647 |
with Not_found ->
|
|
747 |
let old, res = Hashtbl.find table_eqs nd.node_id in
|
|
748 |
if old == nd.node_stmts then res else raise Not_found |
|
749 |
with Not_found -> |
|
648 | 750 |
let res = get_eqs nd.node_stmts in |
649 |
begin |
|
650 |
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); |
|
651 |
res |
|
652 |
end) |
|
751 |
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); |
|
752 |
res |
|
653 | 753 |
|
654 | 754 |
let get_node_eq id node = |
655 | 755 |
let eqs, _ = get_node_eqs node in |
656 |
try |
|
657 |
List.find (fun eq -> List.mem id eq.eq_lhs) eqs |
|
658 |
with |
|
659 |
Not_found -> (* Shall be defined in automata auts *) raise Not_found |
|
660 |
|
|
661 |
let get_nodes prog = |
|
662 |
List.fold_left ( |
|
663 |
fun nodes decl -> |
|
756 |
try List.find (fun eq -> List.mem id eq.eq_lhs) eqs |
|
757 |
with Not_found -> (* Shall be defined in automata auts *) |
|
758 |
raise Not_found |
|
759 |
|
|
760 |
let get_nodes prog = |
|
761 |
List.fold_left |
|
762 |
(fun nodes decl -> |
|
664 | 763 |
match decl.top_decl_desc with |
665 |
| Node _ -> decl::nodes |
|
666 |
| Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes |
|
667 |
) [] prog |
|
764 |
| Node _ -> |
|
765 |
decl :: nodes |
|
766 |
| Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> |
|
767 |
nodes) |
|
768 |
[] prog |
|
668 | 769 |
|> List.rev |
669 | 770 |
|
670 |
let get_imported_nodes prog =
|
|
671 |
List.fold_left (
|
|
672 |
fun nodes decl -> |
|
771 |
let get_imported_nodes prog = |
|
772 |
List.fold_left |
|
773 |
(fun nodes decl ->
|
|
673 | 774 |
match decl.top_decl_desc with |
674 |
| ImportedNode _ -> decl::nodes |
|
675 |
| Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes |
|
676 |
) [] prog |
|
677 |
|
|
678 |
let get_consts prog = |
|
679 |
List.fold_right ( |
|
680 |
fun decl consts -> |
|
775 |
| ImportedNode _ -> |
|
776 |
decl :: nodes |
|
777 |
| Const _ | Node _ | Include _ | Open _ | TypeDef _ -> |
|
778 |
nodes) |
|
779 |
[] prog |
|
780 |
|
|
781 |
let get_consts prog = |
|
782 |
List.fold_right |
|
783 |
(fun decl consts -> |
|
681 | 784 |
match decl.top_decl_desc with |
682 |
| Const _ -> decl::consts |
|
683 |
| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts |
|
684 |
) prog [] |
|
685 |
|
|
686 |
let get_typedefs prog = |
|
687 |
List.fold_right ( |
|
688 |
fun decl types -> |
|
785 |
| Const _ -> |
|
786 |
decl :: consts |
|
787 |
| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> |
|
788 |
consts) |
|
789 |
prog [] |
|
790 |
|
|
791 |
let get_typedefs prog = |
|
792 |
List.fold_right |
|
793 |
(fun decl types -> |
|
689 | 794 |
match decl.top_decl_desc with |
690 |
| TypeDef _ -> decl::types |
|
691 |
| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types |
|
692 |
) prog [] |
|
795 |
| TypeDef _ -> |
|
796 |
decl :: types |
|
797 |
| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> |
|
798 |
types) |
|
799 |
prog [] |
|
693 | 800 |
|
694 | 801 |
let get_dependencies prog = |
695 |
List.fold_right (
|
|
696 |
fun decl deps -> |
|
802 |
List.fold_right |
|
803 |
(fun decl deps ->
|
|
697 | 804 |
match decl.top_decl_desc with |
698 |
| Open _ -> decl::deps |
|
699 |
| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps |
|
700 |
) prog [] |
|
805 |
| Open _ -> |
|
806 |
decl :: deps |
|
807 |
| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> |
|
808 |
deps) |
|
809 |
prog [] |
|
701 | 810 |
|
702 | 811 |
let get_node_interface nd = |
703 |
{nodei_id = nd.node_id; |
|
704 |
nodei_type = nd.node_type; |
|
705 |
nodei_clock = nd.node_clock; |
|
706 |
nodei_inputs = nd.node_inputs; |
|
707 |
nodei_outputs = nd.node_outputs; |
|
708 |
nodei_stateless = nd.node_dec_stateless; |
|
709 |
nodei_spec = nd.node_spec; |
|
710 |
(* nodei_annot = nd.node_annot; *) |
|
711 |
nodei_prototype = None; |
|
712 |
nodei_in_lib = []; |
|
713 |
} |
|
812 |
{ |
|
813 |
nodei_id = nd.node_id; |
|
814 |
nodei_type = nd.node_type; |
|
815 |
nodei_clock = nd.node_clock; |
|
816 |
nodei_inputs = nd.node_inputs; |
|
817 |
nodei_outputs = nd.node_outputs; |
|
818 |
nodei_stateless = nd.node_dec_stateless; |
|
819 |
nodei_spec = nd.node_spec; |
|
820 |
(* nodei_annot = nd.node_annot; *) |
|
821 |
nodei_prototype = None; |
|
822 |
nodei_in_lib = []; |
|
823 |
} |
|
714 | 824 |
|
715 | 825 |
(************************************************************************) |
716 |
(* Renaming / Copying *)
|
|
826 |
(* Renaming / Copying *)
|
|
717 | 827 |
|
718 | 828 |
let copy_var_decl vdecl = |
719 |
mkvar_decl |
|
720 |
vdecl.var_loc |
|
721 |
~orig:vdecl.var_orig |
|
722 |
( |
|
723 |
vdecl.var_id, |
|
829 |
mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig |
|
830 |
( vdecl.var_id, |
|
724 | 831 |
vdecl.var_dec_type, |
725 | 832 |
vdecl.var_dec_clock, |
726 | 833 |
vdecl.var_dec_const, |
727 | 834 |
vdecl.var_dec_value, |
728 |
vdecl.var_parent_nodeid |
|
729 |
) |
|
835 |
vdecl.var_parent_nodeid ) |
|
730 | 836 |
|
731 |
let copy_const cdecl = |
|
732 |
{ cdecl with const_type = Types.new_var () } |
|
837 |
let copy_const cdecl = { cdecl with const_type = Types.new_var () } |
|
733 | 838 |
|
734 | 839 |
let copy_node nd = |
735 |
{ nd with |
|
736 |
node_type = Types.new_var (); |
|
737 |
node_clock = Clocks.new_var true; |
|
738 |
node_inputs = List.map copy_var_decl nd.node_inputs; |
|
739 |
node_outputs = List.map copy_var_decl nd.node_outputs; |
|
740 |
node_locals = List.map copy_var_decl nd.node_locals; |
|
840 |
{ |
|
841 |
nd with |
|
842 |
node_type = Types.new_var (); |
|
843 |
node_clock = Clocks.new_var true; |
|
844 |
node_inputs = List.map copy_var_decl nd.node_inputs; |
|
845 |
node_outputs = List.map copy_var_decl nd.node_outputs; |
|
846 |
node_locals = List.map copy_var_decl nd.node_locals; |
|
741 | 847 |
node_gencalls = []; |
742 |
node_checks = [];
|
|
848 |
node_checks = []; |
|
743 | 849 |
node_stateless = None; |
744 | 850 |
} |
745 | 851 |
|
746 | 852 |
let copy_top top = |
747 | 853 |
match top.top_decl_desc with |
748 |
| Node nd -> { top with top_decl_desc = Node (copy_node nd) } |
|
749 |
| Const c -> { top with top_decl_desc = Const (copy_const c) } |
|
750 |
| _ -> top |
|
854 |
| Node nd -> |
|
855 |
{ top with top_decl_desc = Node (copy_node nd) } |
|
856 |
| Const c -> |
|
857 |
{ top with top_decl_desc = Const (copy_const c) } |
|
858 |
| _ -> |
|
859 |
top |
|
751 | 860 |
|
752 |
let copy_prog top_list = |
|
753 |
List.map copy_top top_list |
|
861 |
let copy_prog top_list = List.map copy_top top_list |
|
754 | 862 |
|
755 |
|
|
756 | 863 |
let rec rename_static rename cty = |
757 |
match cty with |
|
758 |
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
|
759 |
| Tydec_clock cty -> Tydec_clock (rename_static rename cty) |
|
760 |
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
|
761 |
| _ -> cty |
|
864 |
match cty with |
|
865 |
| Tydec_array (d, cty') -> |
|
866 |
Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
|
867 |
| Tydec_clock cty -> |
|
868 |
Tydec_clock (rename_static rename cty) |
|
869 |
| Tydec_struct fl -> |
|
870 |
Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
|
871 |
| _ -> |
|
872 |
cty |
|
762 | 873 |
|
763 | 874 |
let rename_carrier rename cck = |
764 |
match cck with |
|
765 |
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
|
766 |
| _ -> cck |
|
875 |
match cck with |
|
876 |
| Ckdec_bool cl -> |
|
877 |
Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
|
878 |
| _ -> |
|
879 |
cck |
|
767 | 880 |
|
768 |
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
|
|
881 |
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) |
|
769 | 882 |
|
770 | 883 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |
771 |
(* let rec expr_replace_var fvar expr = *) |
|
772 |
(* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *) |
|
773 |
|
|
774 |
(* and expr_desc_replace_var fvar expr_desc = *) |
|
775 |
(* match expr_desc with *) |
|
776 |
(* | Expr_const _ -> expr_desc *) |
|
777 |
(* | Expr_ident i -> Expr_ident (fvar i) *) |
|
778 |
(* | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *) |
|
779 |
(* | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *) |
|
780 |
(* | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *) |
|
781 |
(* | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *) |
|
782 |
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *) |
|
783 |
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) *) |
|
784 |
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *) |
|
785 |
(* | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *) |
|
786 |
(* | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *) |
|
787 |
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *) |
|
788 |
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *) |
|
789 |
|
|
790 |
|
|
791 |
|
|
792 |
let rec rename_expr f_node f_var expr = |
|
793 |
{ expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc } |
|
794 |
and rename_expr_desc f_node f_var expr_desc = |
|
795 |
let re = rename_expr f_node f_var in |
|
796 |
match expr_desc with |
|
797 |
| Expr_const _ -> expr_desc |
|
798 |
| Expr_ident i -> Expr_ident (f_var i) |
|
799 |
| Expr_array el -> Expr_array (List.map re el) |
|
800 |
| Expr_access (e1, d) -> Expr_access (re e1, d) |
|
801 |
| Expr_power (e1, d) -> Expr_power (re e1, d) |
|
802 |
| Expr_tuple el -> Expr_tuple (List.map re el) |
|
803 |
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
|
804 |
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
|
805 |
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
|
806 |
| Expr_pre e' -> Expr_pre (re e') |
|
807 |
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
|
808 |
| Expr_merge (i, hl) -> |
|
809 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
|
810 |
| Expr_appl (i, e', i') -> |
|
811 |
Expr_appl (f_node i, re e', Utils.option_map re i') |
|
812 |
|
|
813 |
let rename_var f_var v = { |
|
814 |
(copy_var_decl v) with |
|
815 |
var_id = f_var v.var_id; |
|
816 |
var_type = v.var_type; |
|
817 |
var_clock = v.var_clock; |
|
818 |
} |
|
819 |
|
|
820 |
let rename_vars f_var = List.map (rename_var f_var) |
|
821 |
|
|
822 |
let rec rename_eq f_node f_var eq = { eq with |
|
823 |
eq_lhs = List.map f_var eq.eq_lhs; |
|
824 |
eq_rhs = rename_expr f_node f_var eq.eq_rhs |
|
825 |
} |
|
826 |
and rename_handler f_node f_var h = {h with |
|
827 |
hand_state = f_var h.hand_state; |
|
828 |
hand_unless = List.map ( |
|
829 |
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id |
|
830 |
) h.hand_unless; |
|
831 |
hand_until = List.map ( |
|
832 |
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id |
|
833 |
) h.hand_until; |
|
834 |
hand_locals = rename_vars f_var h.hand_locals; |
|
835 |
hand_stmts = rename_stmts f_node f_var h.hand_stmts; |
|
836 |
hand_annots = rename_annots f_node f_var h.hand_annots; |
|
837 |
|
|
838 |
} |
|
839 |
and rename_aut f_node f_var aut = { aut with |
|
840 |
aut_id = f_var aut.aut_id; |
|
841 |
aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers; |
|
842 |
} |
|
843 |
and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with |
|
844 |
| Eq eq -> Eq (rename_eq f_node f_var eq) |
|
845 |
| Aut at -> Aut (rename_aut f_node f_var at)) |
|
846 |
stmts |
|
847 |
and rename_annotl f_node f_var annots = |
|
848 |
List.map |
|
849 |
(fun (key, value) -> key, rename_eexpr f_node f_var value) |
|
850 |
annots |
|
851 |
and rename_annot f_node f_var annot = |
|
852 |
{ annot with annots = rename_annotl f_node f_var annot.annots } |
|
853 |
and rename_annots f_node f_var annots = |
|
854 |
List.map (rename_annot f_node f_var) annots |
|
884 |
(* let rec expr_replace_var fvar expr = *) |
|
885 |
(* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *) |
|
886 |
|
|
887 |
(* and expr_desc_replace_var fvar expr_desc = *) |
|
888 |
(* match expr_desc with *) |
|
889 |
(* | Expr_const _ -> expr_desc *) |
|
890 |
(* | Expr_ident i -> Expr_ident (fvar i) *) |
|
891 |
(* | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *) |
|
892 |
(* | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *) |
|
893 |
(* | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *) |
|
894 |
(* | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *) |
|
895 |
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var |
|
896 |
fvar t, expr_replace_var fvar e) *) |
|
897 |
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, |
|
898 |
expr_replace_var fvar e2) *) |
|
899 |
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var |
|
900 |
fvar e2) *) |
|
901 |
(* | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *) |
|
902 |
(* | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *) |
|
903 |
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, |
|
904 |
expr_replace_var fvar h)) hl) *) |
|
905 |
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', |
|
906 |
Utils.option_map (expr_replace_var fvar) i') *) |
|
907 |
|
|
908 |
let rec rename_expr f_node f_var expr = |
|
909 |
{ expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc } |
|
910 |
|
|
911 |
and rename_expr_desc f_node f_var expr_desc = |
|
912 |
let re = rename_expr f_node f_var in |
|
913 |
match expr_desc with |
|
914 |
| Expr_const _ -> |
|
915 |
expr_desc |
|
916 |
| Expr_ident i -> |
|
917 |
Expr_ident (f_var i) |
|
918 |
| Expr_array el -> |
|
919 |
Expr_array (List.map re el) |
|
920 |
| Expr_access (e1, d) -> |
|
921 |
Expr_access (re e1, d) |
|
922 |
| Expr_power (e1, d) -> |
|
923 |
Expr_power (re e1, d) |
|
924 |
| Expr_tuple el -> |
|
925 |
Expr_tuple (List.map re el) |
|
926 |
| Expr_ite (c, t, e) -> |
|
927 |
Expr_ite (re c, re t, re e) |
|
928 |
| Expr_arrow (e1, e2) -> |
|
929 |
Expr_arrow (re e1, re e2) |
|
930 |
| Expr_fby (e1, e2) -> |
|
931 |
Expr_fby (re e1, re e2) |
|
932 |
| Expr_pre e' -> |
|
933 |
Expr_pre (re e') |
|
934 |
| Expr_when (e', i, l) -> |
|
935 |
Expr_when (re e', f_var i, l) |
|
936 |
| Expr_merge (i, hl) -> |
|
937 |
Expr_merge (f_var i, List.map (fun (t, h) -> t, re h) hl) |
|
938 |
| Expr_appl (i, e', i') -> |
|
939 |
Expr_appl (f_node i, re e', Utils.option_map re i') |
|
940 |
|
|
941 |
let rename_var f_var v = |
|
942 |
{ |
|
943 |
(copy_var_decl v) with |
|
944 |
var_id = f_var v.var_id; |
|
945 |
var_type = v.var_type; |
|
946 |
var_clock = v.var_clock; |
|
947 |
} |
|
948 |
|
|
949 |
let rename_vars f_var = List.map (rename_var f_var) |
|
950 |
|
|
951 |
let rec rename_eq f_node f_var eq = |
|
952 |
{ |
|
953 |
eq with |
|
954 |
eq_lhs = List.map f_var eq.eq_lhs; |
|
955 |
eq_rhs = rename_expr f_node f_var eq.eq_rhs; |
|
956 |
} |
|
957 |
|
|
958 |
and rename_handler f_node f_var h = |
|
959 |
{ |
|
960 |
h with |
|
961 |
hand_state = f_var h.hand_state; |
|
962 |
hand_unless = |
|
963 |
List.map |
|
964 |
(fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id) |
|
965 |
h.hand_unless; |
|
966 |
hand_until = |
|
967 |
List.map |
|
968 |
(fun (l, e, b, id) -> l, rename_expr f_node f_var e, b, f_var id) |
|
969 |
h.hand_until; |
|
970 |
hand_locals = rename_vars f_var h.hand_locals; |
|
971 |
hand_stmts = rename_stmts f_node f_var h.hand_stmts; |
Also available in: Unified diff
reformatting