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