1+ open Solver_intf
2+
3+ module type Const = sig
4+ include Lattice
5+ val legacy : t
6+ end
7+
8+ module type Common = sig
9+ module Const : Const
10+
11+ type error
12+ type 'd t
13+ type l = (allowed * disallowed ) t
14+ type r = (disallowed * allowed ) t
15+ type lr = (allowed * allowed ) t
16+
17+ val min : lr
18+ val max : lr
19+ val disallow_right : ('l * 'r ) t -> ('l * disallowed ) t
20+ val disallow_left : ('l * 'r ) t -> (disallowed * 'r ) t
21+ val allow_right : ('l * allowed ) t -> ('l * 'r ) t
22+ val allow_left : (allowed * 'r ) t -> ('l * 'r ) t
23+ val newvar : ?hint : string -> unit -> ('l * 'r ) t
24+ val submode : (allowed * 'r ) t -> ('l * allowed ) t -> (unit , error ) result
25+ val equate : lr -> lr -> (unit , error ) result
26+ val submode_exn : (allowed * 'r ) t -> ('l * allowed ) t -> unit
27+ val equate_exn : lr -> lr -> unit
28+ val join : (allowed * 'r ) t list -> left_only t
29+ val meet : ('l * allowed ) t list -> right_only t
30+ val newvar_above : ?hint : string -> (allowed * 'r ) t -> ('l * 'r_ ) t * bool
31+ val newvar_below : ?hint : string -> ('l * allowed ) t -> ('l_ * 'r ) t * bool
32+
33+ val print :
34+ ?verbose : bool -> ?axis : string -> unit -> Format .formatter -> ('l * 'r ) t -> unit
35+
36+ val constrain_lower : (allowed * 'r ) t -> Const .t
37+ val constrain_upper : ('l * allowed ) t -> Const .t
38+ val check_const : ('l * 'r ) t -> Const .t option
39+ val of_const : Const .t -> ('l * 'r ) t
40+ val legacy : lr
41+ end
42+
43+ type ('loc, 'lin, 'uni) modes = {
44+ locality : 'loc ;
45+ linearity : 'lin ;
46+ uniqueness : 'uni ;
47+ }
48+
49+ module type Alloc_or_Value = sig
50+ module Locality : Common
51+ module Uniqueness : Common
52+ module Linearity : Common
53+ module Const : sig
54+ include Const with type t =
55+ (Locality.Const. t, Linearity.Const. t, Uniqueness.Const. t) modes
56+ val close_over : t -> t
57+ val partial_apply : t -> t
58+ end
59+
60+ type error = [ `Locality | `Uniqueness | `Linearity ]
61+
62+ include Common with module Const := Const and type error := error
63+
64+ (* some over-riding *)
65+ val print : ?verbose : bool -> unit -> Format .formatter -> ('l * 'r ) t -> unit
66+
67+ val check_const :
68+ ('l * 'r ) t ->
69+ ( Locality.Const .t option ,
70+ Linearity.Const .t option ,
71+ Uniqueness.Const .t option )
72+ modes
73+
74+ val locality : ('l * 'r ) t -> ('l * 'r ) Locality .t
75+ val uniqueness : ('l * 'r ) t -> ('l * 'r ) Uniqueness .t
76+ val linearity : ('l * 'r ) t -> ('l * 'r ) Linearity .t
77+ val max_with_uniqueness : ('l * 'r ) Uniqueness .t -> (disallowed * 'r ) t
78+ val min_with_uniqueness : ('l * 'r ) Uniqueness .t -> ('l * disallowed ) t
79+ val min_with_locality : ('l * 'r ) Locality .t -> ('l * disallowed ) t
80+ val max_with_locality : ('l * 'r ) Locality .t -> (disallowed * 'r ) t
81+ val min_with_linearity : ('l * 'r ) Linearity .t -> ('l * disallowed ) t
82+ val max_with_linearity : ('l * 'r ) Linearity .t -> (disallowed * 'r ) t
83+ val set_locality_min : ('l * 'r ) t -> ('l * disallowed ) t
84+ val set_locality_max : ('l * 'r ) t -> (disallowed * 'r ) t
85+ val set_linearity_min : ('l * 'r ) t -> ('l * disallowed ) t
86+ val set_linearity_max : ('l * 'r ) t -> (disallowed * 'r ) t
87+ val set_uniqueness_min : ('l * 'r ) t -> ('l * disallowed ) t
88+ val set_uniqueness_max : ('l * 'r ) t -> (disallowed * 'r ) t
89+ val constrain_legacy : lr -> Const .t
90+
91+ val close_over : lr -> l
92+ val partial_apply : (allowed * 'r ) t -> l
93+
94+ val newvar_below_comonadic : ?hint : string -> ('l * allowed ) t -> ('l * 'r ) t
95+ * bool
96+ end
97+
98+ module type S = sig
99+ type nonrec allowed = allowed
100+ type nonrec disallowed = disallowed
101+
102+ module Locality : sig
103+ module Const : sig
104+ type t = Global | Local
105+ include Const with type t : = t
106+ end
107+ type error = unit
108+
109+ include Common with module Const := Const and type error := error
110+
111+ val global : lr
112+ val local : lr
113+ val constrain_legacy : (allowed * 'r ) t -> Const .t
114+ end
115+
116+ module Regionality : sig
117+ module Const : sig
118+ type t = Global | Regional | Local
119+ include Const with type t : = t
120+ end
121+ type error = unit
122+ include Common with module Const := Const and type error : = error
123+
124+ val global : lr
125+ val regional : lr
126+ val local : lr
127+ val constrain_legacy : (allowed * 'r ) t -> Const .t
128+ end
129+
130+ module Linearity : sig
131+ module Const : sig
132+ type t = Many | Once
133+ include Const with type t : = t
134+ end
135+ type error = unit
136+ include Common with module Const := Const and type error : = error
137+
138+ val many : lr
139+ val once : lr
140+ val constrain_legacy : (allowed * 'r ) t -> Const .t
141+ end
142+
143+ module Uniqueness : sig
144+
145+ module Const : sig
146+
147+ type t = Unique | Shared
148+ include Const with type t : = t
149+ end
150+ type error = unit
151+ include Common with module Const := Const and type error : = error
152+
153+ val shared : lr
154+ val unique : lr
155+ val constrain_legacy : ('l * allowed ) t -> Const .t
156+ end
157+
158+ module Value :
159+ Alloc_or_Value
160+ with module Locality := Regionality
161+ and module Uniqueness := Uniqueness
162+ and module Linearity := Linearity
163+
164+
165+ module Alloc :
166+ Alloc_or_Value
167+ with module Locality := Locality
168+ and module Uniqueness := Uniqueness
169+ and module Linearity := Linearity
170+
171+ val unique_to_linear : ('l * 'r ) Uniqueness .t -> ('r * 'l ) Linearity .t
172+ val linear_to_unique : ('l * 'r ) Linearity .t -> ('r * 'l ) Uniqueness .t
173+ val local_to_regional : ('l * 'r ) Locality .t -> ('l * disallowed ) Regionality .t
174+ val regional_to_local : ('l * 'r ) Regionality .t -> ('l * 'r ) Locality .t
175+ val locality_as_regionality : ('l * 'r ) Locality .t -> ('l * 'r ) Regionality .t
176+ val regional_to_global : ('l * 'r ) Regionality .t -> ('l * 'r ) Locality .t
177+ val global_to_regional : ('l * 'r ) Locality .t -> (disallowed * 'r ) Regionality .t
178+ val alloc_as_value : ('l * 'r ) Alloc .t -> ('l * 'r ) Value .t
179+ val alloc_to_value_l2r : ('l * 'r ) Alloc .t -> ('l * disallowed ) Value .t
180+
181+ (* not used; only for completeness*)
182+ val alloc_to_value_g2r : ('l * 'r ) Alloc .t -> (disallowed * 'r ) Value .t
183+ val value_to_alloc_r2g : ('l * 'r ) Value .t -> ('l * 'r ) Alloc .t
184+ val value_to_alloc_r2l : ('l * 'r ) Value .t -> ('l * 'r ) Alloc .t
185+
186+ module Const : sig
187+ val unique_to_linear : Uniqueness.Const .t -> Linearity.Const .t
188+ end
189+
190+ end
0 commit comments