Revision 52cfee34 src/clock_calculus.ml
src/clock_calculus.ml  

519  519 
 Mismatch (cr1,cr2) > 
520  520 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
521  521  
522 
(* Checks whether ck1 is a subtype of ck2 *)


523 
let rec clock_subtyping ck1 ck2 =


522 
(* ck1 is a subtype of ck2 *) 

523 
let rec sub_unify sub ck1 ck2 =


524  524 
match (repr ck1).cdesc, (repr ck2).cdesc with 
525 
 Ccarrying _ , Ccarrying _ > unify ck1 ck2 

526 
 Ccarrying (cr', ck'), _ > unify ck' ck2 

527 
 _ > unify ck1 ck2 

525 
 Ctuple [c1] , Ctuple [c2] > sub_unify sub c1 c2 

526 
 Ctuple cl1 , Ctuple cl2 > 

527 
if List.length cl1 <> List.length cl2 

528 
then raise (Unify (ck1, ck2)) 

529 
else List.iter2 (sub_unify sub) cl1 cl2 

530 
 Ctuple [c1] , _ > sub_unify sub c1 ck2 

531 
 _ , Ctuple [c2] > sub_unify sub ck1 c2 

532 
 Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 > 

533 
begin 

534 
unify_carrier cr1 cr2; 

535 
sub_unify sub c1 c2 

536 
end 

537 
 Ccarrying (cr1, c1), Ccarrying (cr2, c2)> 

538 
begin 

539 
unify_carrier cr1 cr2; 

540 
sub_unify sub c1 c2 

541 
end 

542 
 Ccarrying (_, c1) , _ when sub > sub_unify sub c1 ck2 

543 
 _ > unify ck1 ck2 

544  
545 
let try_sub_unify sub ck1 ck2 loc = 

546 
try 

547 
sub_unify sub ck1 ck2 

548 
with 

549 
 Unify (ck1',ck2') > 

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

551 
 Subsume (ck,cset) > 

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

553 
 Mismatch (cr1,cr2) > 

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

528  555  
529  556 
(* Clocks a list of arguments of Lustre builtin operators: 
530  557 
 type each expression, remove carriers of clocks as 
...  ...  
539  566  
540  567 
(* emulates a subtyping relation between clocks c and (cr : c), 
541  568 
used during node application only *) 
542 
and clock_subtyping_arg env real_arg formal_clock = 

569 
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =


543  570 
let loc = real_arg.expr_loc in 
544  571 
let real_clock = clock_expr env real_arg in 
545 
try 

546 
clock_subtyping real_clock formal_clock 

547 
with 

548 
 Unify (ck1',ck2') > 

549 
raise (Error (loc, Clock_clash (real_clock, formal_clock))) 

550 
 Subsume (ck,cset) > 

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

552 
 Mismatch (cr1,cr2) > 

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

572 
try_sub_unify sub real_clock formal_clock loc 

554  573  
555  574 
(* computes clocks for node application *) 
556  575 
and clock_appl env f args clock_reset loc = 
...  ...  
779  798 
let ck_outs = clock_of_vlist nd.node_outputs in 
780  799 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
781  800 
unify_imported_clock None ck_node; 
782 
(*Log.report ~level:3 (fun fmt > print_ck fmt ck_node);*)


801 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node);


783  802 
(* Local variables may contain firstorder carrier variables that should be generalized. 
784  803 
That's not the case for types. *) 
785  804 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; 
...  ...  
789  808 
(* if (is_main && is_polymorphic ck_node) then 
790  809 
raise (Error (loc,(Cannot_be_polymorphic ck_node))); 
791  810 
*) 
811 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 

792  812 
nd.node_clock < ck_node; 
793  813 
Env.add_value env nd.node_id ck_node 
794  814  
...  ...  
832  852 
nd.nodei_clock < ck_node; 
833  853 
Env.add_value env nd.nodei_id ck_node 
834  854  
835 
let clock_function env loc fcn = 

836 
let new_env = clock_var_decl_list env false fcn.fun_inputs in 

837 
ignore(clock_var_decl_list new_env false fcn.fun_outputs); 

838 
let ck_ins = clock_of_vlist fcn.fun_inputs in 

839 
let ck_outs = clock_of_vlist fcn.fun_outputs in 

840 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 

841 
unify_imported_clock None ck_node; 

842 
check_imported_pclocks loc ck_node; 

843 
try_generalize ck_node loc; 

844 
Env.add_value env fcn.fun_id ck_node 

845  
846  855 
let clock_top_consts env clist = 
847  856 
List.fold_left (fun env cdecl > 
848  857 
let ck = new_var false in 
...  ...  
855  864 
clock_node env decl.top_decl_loc nd 
856  865 
 ImportedNode nd > 
857  866 
clock_imported_node env decl.top_decl_loc nd 
858 
 ImportedFun fcn > 

859 
clock_function env decl.top_decl_loc fcn 

860  867 
 Consts clist > 
861  868 
clock_top_consts env clist 
862  869 
 Open _ > 
...  ...  
891  898 
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs) 
892  899 
 ImportedNode nd > 
893  900 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
894 
 ImportedFun nd > 

895 
() 

896  901 
 Consts clist > () 
897  902 
 Open _ > () 
898  903 
Also available in: Unified diff