Revision ca7ff3f7
Added by LĂ©lio Brun 7 months 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