Project

General

Profile

« Previous | Next » 

Revision 6cbbe1c1

Added by LĂ©lio Brun 8 months ago

start again with spec representation

View differences:

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