Revision d3e4c22f 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 first-order 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