Revision 6cbbe1c1
Added by Lélio Brun about 2 years ago
| src/clock_calculus.ml | ||
|---|---|---|
| 49 | 49 |
match cr.carrier_desc with |
| 50 | 50 |
| Carry_const _ |
| 51 | 51 |
| Carry_name -> |
| 52 |
if cr.carrier_scoped then
|
|
| 53 |
raise (Scope_carrier cr);
|
|
| 54 |
cr.carrier_desc <- Carry_var
|
|
| 52 |
if cr.carrier_scoped then |
|
| 53 |
raise (Scope_carrier cr); |
|
| 54 |
cr.carrier_desc <- Carry_var |
|
| 55 | 55 |
| Carry_var -> () |
| 56 | 56 |
| Carry_link cr' -> generalize_carrier cr' |
| 57 | 57 |
|
| 58 | 58 |
(** Promote monomorphic clock variables to polymorphic clock variables. *) |
| 59 | 59 |
(* Generalize by side-effects *) |
| 60 | 60 |
let rec generalize ck = |
| 61 |
match ck.cdesc with
|
|
| 62 |
| Carrow (ck1,ck2) ->
|
|
| 63 |
generalize ck1; generalize ck2
|
|
| 64 |
| Ctuple clist ->
|
|
| 65 |
List.iter generalize clist
|
|
| 66 |
| Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
|
|
| 67 |
| Cvar ->
|
|
| 68 |
if ck.cscoped then
|
|
| 69 |
raise (Scope_clock ck);
|
|
| 70 |
ck.cdesc <- Cunivar
|
|
| 71 |
| Cunivar -> ()
|
|
| 72 |
| Clink ck' ->
|
|
| 73 |
generalize ck'
|
|
| 74 |
| Ccarrying (cr,ck') ->
|
|
| 75 |
generalize_carrier cr; generalize ck'
|
|
| 61 |
match ck.cdesc with |
|
| 62 |
| Carrow (ck1,ck2) -> |
|
| 63 |
generalize ck1; generalize ck2 |
|
| 64 |
| Ctuple clist -> |
|
| 65 |
List.iter generalize clist |
|
| 66 |
| Con (ck',cr,_) -> generalize ck'; generalize_carrier cr |
|
| 67 |
| Cvar -> |
|
| 68 |
if ck.cscoped then |
|
| 69 |
raise (Scope_clock ck); |
|
| 70 |
ck.cdesc <- Cunivar
|
|
| 71 |
| Cunivar -> ()
|
|
| 72 |
| Clink ck' -> |
|
| 73 |
generalize ck' |
|
| 74 |
| Ccarrying (cr,ck') -> |
|
| 75 |
generalize_carrier cr; generalize ck' |
|
| 76 | 76 |
|
| 77 | 77 |
let try_generalize ck_node loc = |
| 78 | 78 |
try |
| 79 | 79 |
generalize ck_node |
| 80 |
with (Scope_carrier cr) -> |
|
| 80 |
with |
|
| 81 |
| Scope_carrier cr -> |
|
| 81 | 82 |
raise (Error (loc, Carrier_extrusion (ck_node, cr))) |
| 82 |
| (Scope_clock ck) ->
|
|
| 83 |
| Scope_clock ck ->
|
|
| 83 | 84 |
raise (Error (loc, Clock_extrusion (ck_node, ck))) |
| 84 | 85 |
|
| 85 | 86 |
(* Clocks instanciation *) |
| ... | ... | |
| 414 | 415 |
let rec aux ck = |
| 415 | 416 |
match (repr ck).cdesc with |
| 416 | 417 |
| Cvar -> |
| 417 |
begin
|
|
| 418 |
match !ck_var with
|
|
| 419 |
| None ->
|
|
| 420 |
ck_var:=Some ck
|
|
| 421 |
| Some v ->
|
|
| 422 |
(* cannot fail *)
|
|
| 423 |
try_unify ck v loc
|
|
| 424 |
end
|
|
| 418 |
begin |
|
| 419 |
match !ck_var with |
|
| 420 |
| None -> |
|
| 421 |
ck_var := Some ck
|
|
| 422 |
| Some v -> |
|
| 423 |
(* cannot fail *) |
|
| 424 |
try_unify ck v loc |
|
| 425 |
end |
|
| 425 | 426 |
| Ctuple cl -> |
| 426 |
List.iter aux cl
|
|
| 427 |
List.iter aux cl |
|
| 427 | 428 |
| Carrow (ck1,ck2) -> |
| 428 |
aux ck1; aux ck2
|
|
| 429 |
aux ck1; aux ck2 |
|
| 429 | 430 |
| Ccarrying (_, ck1) -> |
| 430 |
aux ck1
|
|
| 431 |
aux ck1 |
|
| 431 | 432 |
| Con (ck1, _, _) -> aux ck1 |
| 432 | 433 |
| _ -> () |
| 433 | 434 |
in |
| ... | ... | |
| 611 | 612 |
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in |
| 612 | 613 |
environment [env] *) |
| 613 | 614 |
let clock_eq env eq = |
| 614 |
let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in |
|
| 615 |
let expr_lhs = expr_of_expr_list eq.eq_loc |
|
| 616 |
(List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in |
|
| 615 | 617 |
let ck_rhs = clock_expr env eq.eq_rhs in |
| 616 | 618 |
clock_subtyping_arg env expr_lhs ck_rhs |
| 617 | 619 |
|
| ... | ... | |
| 649 | 651 |
else |
| 650 | 652 |
*) |
| 651 | 653 |
if Types.get_clock_base_type vdecl.var_type <> None |
| 652 |
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
|
|
| 654 |
then new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
|
|
| 653 | 655 |
else ck in |
| 654 | 656 |
(if vdecl.var_dec_const |
| 655 | 657 |
then match vdecl.var_dec_value with |
| ... | ... | |
| 685 | 687 |
List.iter (clock_eq new_env) eqs; |
| 686 | 688 |
let ck_ins = clock_of_vlist nd.node_inputs in |
| 687 | 689 |
let ck_outs = clock_of_vlist nd.node_outputs in |
| 688 |
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in |
|
| 690 |
let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
|
|
| 689 | 691 |
unify_imported_clock None ck_node loc; |
| 690 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
|
|
| 692 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
|
|
| 691 | 693 |
(* Local variables may contain first-order carrier variables that should be generalized. |
| 692 | 694 |
That's not the case for types. *) |
| 693 | 695 |
try_generalize ck_node loc; |
| ... | ... | |
| 699 | 701 |
(* if (is_main && is_polymorphic ck_node) then |
| 700 | 702 |
raise (Error (loc,(Cannot_be_polymorphic ck_node))); |
| 701 | 703 |
*) |
| 702 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
|
|
| 704 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck ck_node);
|
|
| 703 | 705 |
nd.node_clock <- ck_node; |
| 704 | 706 |
Env.add_value env nd.node_id ck_node |
| 705 | 707 |
|
Also available in: Unified diff
start again with spec representation