|
1
|
open Utils
|
|
2
|
|
|
3
|
(* Clock carriers basically correspond to the "c" in "x when c" *)
|
|
4
|
type carrier_desc =
|
|
5
|
| Carry_const of ident
|
|
6
|
| Carry_name
|
|
7
|
| Carry_var
|
|
8
|
| Carry_link of carrier_expr
|
|
9
|
|
|
10
|
(* Carriers are scoped, to detect clock extrusion. In other words, we check the
|
|
11
|
scope of a clock carrier before generalizing it. *)
|
|
12
|
and carrier_expr = {
|
|
13
|
mutable carrier_desc : carrier_desc;
|
|
14
|
mutable carrier_scoped : bool;
|
|
15
|
carrier_id : int;
|
|
16
|
}
|
|
17
|
|
|
18
|
type t = {
|
|
19
|
mutable cdesc : clock_desc;
|
|
20
|
mutable cscoped : bool;
|
|
21
|
cid : int;
|
|
22
|
}
|
|
23
|
|
|
24
|
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
|
|
25
|
and clock_desc =
|
|
26
|
| Carrow of t * t
|
|
27
|
| Ctuple of t list
|
|
28
|
| Con of t * carrier_expr * ident
|
|
29
|
| Cvar (* of clock_set *)
|
|
30
|
(* Monomorphic clock variable *)
|
|
31
|
| Cunivar
|
|
32
|
(* of clock_set *)
|
|
33
|
(* Polymorphic clock variable *)
|
|
34
|
| Clink of t
|
|
35
|
(* During unification, make links instead of substitutions *)
|
|
36
|
| Ccarrying of carrier_expr * t
|
|
37
|
|
|
38
|
type error =
|
|
39
|
| Clock_clash of t * t
|
|
40
|
| Cannot_be_polymorphic of t
|
|
41
|
| Invalid_imported_clock of t
|
|
42
|
| Invalid_const of t
|
|
43
|
| Factor_zero
|
|
44
|
| Carrier_mismatch of carrier_expr * carrier_expr
|
|
45
|
| Carrier_extrusion of t * carrier_expr
|
|
46
|
| Clock_extrusion of t * t
|
|
47
|
|
|
48
|
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
|
|
49
|
complexity. *)
|
|
50
|
val pp: Format.formatter -> t -> unit
|
|
51
|
|
|
52
|
val pp_suffix: Format.formatter -> t -> unit
|
|
53
|
|
|
54
|
val new_var: bool -> t
|
|
55
|
|
|
56
|
val new_univar: unit -> t
|
|
57
|
|
|
58
|
val new_ck: clock_desc -> bool -> t
|
|
59
|
|
|
60
|
val new_carrier: carrier_desc -> bool -> carrier_expr
|
|
61
|
|
|
62
|
val bottom: t
|
|
63
|
|
|
64
|
val repr: t -> t
|
|
65
|
val carrier_repr: carrier_expr -> carrier_expr
|
|
66
|
|
|
67
|
val simplify: t -> t
|
|
68
|
|
|
69
|
val clock_on: t -> carrier_expr -> ident -> t
|
|
70
|
|
|
71
|
val clock_of_clock_list: t list -> t
|
|
72
|
val clock_list_of_clock: t -> t list
|
|
73
|
|
|
74
|
val root: t -> t
|
|
75
|
|
|
76
|
val branch: t -> (carrier_expr * ident) list
|
|
77
|
|
|
78
|
val common_prefix: (carrier_expr * ident) list -> (carrier_expr * ident) list -> (carrier_expr * ident) list
|
|
79
|
|
|
80
|
val clock_of_root_branch: t -> (carrier_expr * ident) list -> t
|
|
81
|
|
|
82
|
val split_arrow: t -> t * t
|
|
83
|
|
|
84
|
val clock_current: t -> t
|
|
85
|
|
|
86
|
val uneval: ident -> carrier_expr -> unit
|
|
87
|
|
|
88
|
val get_carrier_name: t -> carrier_expr option
|
|
89
|
|
|
90
|
val equal: t -> t -> bool
|
|
91
|
|
|
92
|
(* Disjunction relation between variables based upon their static clocks. *)
|
|
93
|
val disjoint: t -> t -> bool
|
|
94
|
|
|
95
|
val const_of_carrier: carrier_expr -> ident
|
|
96
|
|
|
97
|
val pp_error: Format.formatter -> error -> unit
|
|
98
|
|
|
99
|
exception Unify of t * t
|
|
100
|
exception Scope_carrier of carrier_expr
|
|
101
|
exception Scope_clock of t
|
|
102
|
exception Error of Location.t * error
|
|
103
|
exception Mismatch of carrier_expr * carrier_expr
|