Revision c518d082
Added by Xavier Thirioux almost 9 years ago
src/clock_calculus.ml  

251  251 
cr1.carrier_desc < Carry_link cr2; 
252  252 
update_scope_carrier cr1.carrier_scoped cr2 
253  253 
end 
254 
 _,_ > (assert false) 

254 
 _,_ > assert false 

255  
256 
(* Semiunifies two clock carriers *) 

257 
let semi_unify_carrier cr1 cr2 = 

258 
let cr1 = carrier_repr cr1 in 

259 
let cr2 = carrier_repr cr2 in 

260 
if cr1=cr2 then () 

261 
else 

262 
match cr1.carrier_desc, cr2.carrier_desc with 

263 
 Carry_const id1, Carry_const id2 > 

264 
if id1 <> id2 then raise (Mismatch (cr1, cr2)) 

265 
 Carry_const _, Carry_name > 

266 
begin 

267 
cr2.carrier_desc < Carry_link cr1; 

268 
update_scope_carrier cr2.carrier_scoped cr1 

269 
end 

270 
 Carry_name, Carry_const _ > raise (Mismatch (cr1, cr2)) 

271 
 Carry_name, Carry_name > 

272 
if cr1.carrier_id < cr2.carrier_id then 

273 
begin 

274 
cr2.carrier_desc < Carry_link cr1; 

275 
update_scope_carrier cr2.carrier_scoped cr1 

276 
end 

277 
else 

278 
begin 

279 
cr1.carrier_desc < Carry_link cr2; 

280 
update_scope_carrier cr1.carrier_scoped cr2 

281 
end 

282 
 _,_ > assert false 

255  283  
256  284 
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify 
257  285 
(ck1,ck2)] if the clocks are not unifiable.*) 
...  ...  
355  383 
subsume ck2 (CSet_pck (b,(a,b))); 
356  384 
let ck2' = simplify (new_ck (Pck_phase (ck2,(a,b))) true) in 
357  385 
unify pck1' ck2' 
358 
(* Corner case for some functions like ite, need to unify guard clock 

359 
with output clocks *) 

360 
(* 

361 
 Ctuple ckl, (Cvar _) > List.iter (unify ck2) ckl 

362 
 (Cvar _), Ctuple ckl > List.iter (unify ck1) ckl 

363 
*) 

386 
 Cunivar _, _  _, Cunivar _ > () 

387 
 _,_ > raise (Unify (ck1,ck2)) 

388  
389 
(** [unify ck1 ck2] semiunifies clocks [ck1] and [ck2]. Raises [Unify 

390 
(ck1,ck2)] if the clocks are not semiunifiable.*) 

391 
let rec semi_unify ck1 ck2 = 

392 
let ck1 = repr ck1 in 

393 
let ck2 = repr ck2 in 

394 
if ck1=ck2 then 

395 
() 

396 
else 

397 
match ck1.cdesc,ck2.cdesc with 

398 
 Cvar cset1,Cvar cset2> 

399 
if ck1.cid < ck2.cid then 

400 
begin 

401 
ck2.cdesc < Clink (simplify ck1); 

402 
update_scope ck2.cscoped ck1 

403 
end 

404 
else 

405 
begin 

406 
ck1.cdesc < Clink (simplify ck2); 

407 
update_scope ck1.cscoped ck2 

408 
end 

409 
 (Cvar cset,_) > raise (Unify (ck1,ck2)) 

410 
 (_, (Cvar cset)) when (not (occurs ck2 ck1)) > 

411 
update_scope ck2.cscoped ck1; 

412 
ck2.cdesc < Clink (simplify ck1) 

413 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 

414 
semi_unify_carrier cr1 cr2; 

415 
semi_unify ck1' ck2' 

416 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 

417 
raise (Unify (ck1,ck2)) 

418 
 Carrow (c1,c2), Carrow (c1',c2') > 

419 
begin 

420 
semi_unify c1 c1'; 

421 
semi_unify c2 c2' 

422 
end 

423 
 Ctuple ckl1, Ctuple ckl2 > 

424 
if (List.length ckl1) <> (List.length ckl2) then 

425 
raise (Unify (ck1,ck2)); 

426 
List.iter2 semi_unify ckl1 ckl2 

427 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 

428 
semi_unify_carrier c1 c2; 

429 
semi_unify ck' ck'' 

364  430 
 Cunivar _, _  _, Cunivar _ > () 
365  431 
 _,_ > raise (Unify (ck1,ck2)) 
366  432  
...  ...  
442  508 
 Mismatch (cr1,cr2) > 
443  509 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
444  510  
511 
let try_semi_unify ck1 ck2 loc = 

512 
try 

513 
semi_unify ck1 ck2 

514 
with 

515 
 Unify (ck1',ck2') > 

516 
raise (Error (loc, Clock_clash (ck1',ck2'))) 

517 
 Subsume (ck,cset) > 

518 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 

519 
 Mismatch (cr1,cr2) > 

520 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 

521  
445  522 
(* Checks whether ck1 is a subtype of ck2 *) 
446  523 
let rec clock_subtyping ck1 ck2 = 
447  524 
match (repr ck1).cdesc, (repr ck2).cdesc with 
...  ...  
775  852 
let clock_prog env decls = 
776  853 
List.fold_left (fun e decl > clock_top_decl e decl) env decls 
777  854  
855 
(* Once the Lustre program is fully clocked, 

856 
we must get back to the original description of clocks, 

857 
with constant parameters, instead of unifiable internal variables. *) 

858  
859 
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions, 

860 
i.e. replacing unifiable second_order variables with the original carrier names. 

861 
Once restored in this formulation, clocks may be meaningfully printed. 

862 
*) 

863 
let uneval_vdecl_generics vdecl = 

864 
if Types.is_clock_type vdecl.var_type 

865 
then 

866 
match get_carrier_name vdecl.var_clock with 

867 
 None > (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false) 

868 
 Some cr > Clocks.uneval vdecl.var_id cr 

869  
870 
let uneval_node_generics vdecls = 

871 
List.iter uneval_vdecl_generics vdecls 

872  
873 
let uneval_top_generics decl = 

874 
match decl.top_decl_desc with 

875 
 Node nd > 

876 
uneval_node_generics (nd.node_inputs @ nd.node_outputs) 

877 
 ImportedNode nd > 

878 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 

879 
 ImportedFun nd > 

880 
() 

881 
 Consts clist > () 

882 
 Open _ > () 

883  
884 
let uneval_prog_generics prog = 

885 
List.iter uneval_top_generics prog 

886  
778  887 
let check_env_compat header declared computed = 
888 
uneval_prog_generics header; 

779  889 
Env.iter declared (fun k decl_clock_k > 
780  890 
let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in 
781 
try_unify decl_clock_k computed_c Location.dummy_loc 

891 
try_semi_unify decl_clock_k computed_c Location.dummy_loc


782  892 
) 
783  893 
(* Local Variables: *) 
784  894 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
 added generation of clock information in interface (.lusi) files
 added clock checking between interface and implementation files