types.mli 7.97 KB
Newer Older
1
2
open Ident

3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
module Vars : sig 
  module V : Custom.T with type t = string
  include Bool.S
end

module BoolAtoms : BoolVar.S with
  type bt = Atoms.t and
  type elem = Atoms.t Custom.pairvar
module BoolIntervals : BoolVar.S with
  type bt = Intervals.t and
  type elem = Intervals.t Custom.pairvar
module BoolChars : BoolVar.S with
  type bt = Chars.t and
  type elem = Chars.t Custom.pairvar
module BoolVars : BoolVar.S with type elem = Vars.t Custom.pairvar

19
20
type const = 
  | Integer of Intervals.V.t
21
  | Atom of Atoms.V.t
22
  | Var of Vars.V.t
23
24
25
26
27
28
  | Char of Chars.V.t
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const

Jérôme Maloberti's avatar
Jérôme Maloberti committed
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
type service_params =
  | TProd of service_params * service_params
  | TOption of service_params 
  | TList of string * service_params
  | TSet of service_params
  | TSum of service_params * service_params
  | TString of string
  | TInt of string
  | TInt32 of string
  | TInt64 of string
  | TFloat of string 
  | TBool of string
  | TFile of string
      (* | TUserType of string * (string -> 'a) * ('a -> string) *)
  | TCoord of string 
  | TCoordv of service_params * string
  | TESuffix of string 
  | TESuffixs of string
      (*  | TESuffixu of (string * (string -> 'a) * ('a -> string)) *)
  | TSuffix of (bool * service_params)
  | TUnit 
  | TAny
  | TConst of string;;
52

53
module Const: Custom.T with type t = const
54

55
(*
56
57
58
module CompUnit : sig
  include Custom.T

59
  val get_current: unit -> t
60
61
  val mk: U.t -> t
  val value: t -> U.t
62
  val print_qual: Format.formatter -> t -> unit
63
64
65
66
67
68
69
70
71

  val enter: t -> unit
  val leave: unit -> unit
  val close_serialize: unit -> t list

  val pervasives: t

  module Tbl : Inttbl.S with type key = t
end
72
*)
73

74
module Abstract : sig
75
76
  module T : Custom.T with type t = string
  type abs = T.t
77
78
79
  type t
  val any: t
  val atom: abs -> t
80
  val compare: t -> t -> int
81
82
83
84
85
86
87
88

  module V : sig
    type t = abs * Obj.t
  end

  val contains: abs -> t -> bool
end

89
90
(** Algebra **)

91
92
include Custom.T
module Node : Custom.T
93

94
95
96
97
98
99
module Pair : Bool.S with type elem = (Node.t * Node.t)
module BoolPair : BoolVar.S with type bt = Pair.t and type elem = Pair.t Custom.pairvar 

module Rec : Bool.S with type elem = bool * Node.t Ident.label_map
module BoolRec : BoolVar.S with type bt = Rec.t and type elem = Rec.t Custom.pairvar

100
type descr = t
101

102
103
val make: unit -> Node.t
val define: Node.t -> t -> unit
104

105
106
val cons: t -> Node.t
val internalize: Node.t -> Node.t
107

108
109
val id: Node.t -> int
val descr: Node.t -> t
110

111
112
(** Boolean connectives **)

113
114
115
116
117
118
val cup    : t -> t -> t
val cap    : t -> t -> t
val diff   : t -> t -> t
val neg    : t -> t
val empty  : t
val any    : t
119

120
val any_node : Node.t
121
val empty_node : Node.t
122

123
val non_constructed : t
124
val non_constructed_or_absent : t
125

126
127
(** Constructors **)

128
129
type pair_kind = [ `Normal | `XML ]

130
131
val interval : BoolIntervals.t -> t
val atom     : BoolAtoms.t -> t
132
133
134
135
val times    : Node.t -> Node.t -> t
val xml      : Node.t -> Node.t -> t
val arrow    : Node.t -> Node.t -> t
val record   : label -> Node.t -> t
136
  (* bool = true -> open record; bool = false -> closed record *)
137
val record_fields : bool * Node.t label_map -> t
138
val char     : BoolChars.t -> t
139
val constant : const -> t
140
val abstract : Abstract.t -> t
141

142
143
(** Helpers *)

144
145
val tuple : Node.t list -> t

146
val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
147

148
val empty_closed_record: t
149
val empty_open_record: t
150

151
152
153
154
155
156
157
(** Positive systems and least solutions **)

module Positive :
sig
  type v
  val forward: unit -> v
  val define: v -> v -> unit
158
  val ty: t -> v
159
160
  val cup: v list -> v
  val times: v -> v -> v
161
  val xml: v -> v -> v
162

163
  val solve: v -> Node.t
164
165
166
167
168
end

(** Normalization **)

module Product : sig
169
170
  val any : t
  val any_xml : t
171
  val any_of: pair_kind -> t
172
173
  val other : ?kind:pair_kind -> t -> t
  val is_product : ?kind:pair_kind -> t -> bool
174
175
176

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
177
  val is_empty: t -> bool
178
  val get: ?kind:pair_kind -> descr -> t
179
180
  val pi1: t -> descr
  val pi2: t -> descr
181
  val pi2_restricted: descr -> t -> descr
182
183
184
185
186
187
188
    
  (* Intersection with (pi1,Any) *)
  val restrict_1: t -> descr -> t

  (* List of non-empty rectangles whose first projection
     are pair-wise disjunct *)
  type normal = t
189
  val normal: ?kind:pair_kind -> descr -> normal
190

191
192
193
194
  val constraint_on_2: normal -> descr -> descr
    (* constraint_on_2 n t1:  maximal t2 such that (t1,t2) <= n *)
    (* Assumption: t1 <= pi1(n) *)

195
196
  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
197
198
199
200


  val clean_normal: t -> t
    (* Merge rectangles with same second component *)
201
202
203
end

module Record : sig
204
  val any : t
205
206
  val absent : t
  val absent_node : Node.t
207
208
  val or_absent: t -> t
  val any_or_absent: t
209
  val any_or_absent_node : Node.t
210

211
212
  val has_absent: t -> bool
  val has_record: t -> bool
213

214
215
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
216

217
218
219
  val pi : label -> t -> t
    (* May contain absent *)

220
  val project : t -> label -> t
221
222
    (* Raise Not_found if label is not necessarily present *)

223
  val condition : t -> label -> t -> t
224
    (* condition t1 l t2 : What must follow if field l hash type t2 *)
225
226
  val project_opt : t -> label -> t
  val has_empty_record: t -> bool
227
228


229
  val first_label: t -> label
230
  val all_labels: t -> LabelSet.t
231

232
  val empty_cases: t -> bool * bool
233

234
235
  val merge: t -> t -> t
  val remove_field: t -> label -> t
236

237
  val get: t -> ((bool * t) label_map * bool * bool) list
238
239
240
241
242
243
244


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
245
246
end

247
module Arrow : sig
248
  val any : t
249

250
  val sample: t -> t
251

252
  val check_strenghten: t -> t -> t
253
254
255
256
257
258
259
    (* [check_strenghten t s]
       Assume that [t] is an intersection of arrow types
       representing the interface of an abstraction;
       check that this abstraction has type [s] (otherwise raise Not_found)
       and returns a refined type for this abstraction.
    *)

260
  val check_iface: (t * t) list -> t -> bool
261

262
  type t
263
  val is_empty: t -> bool
264
265
  val get: descr -> t
    (* Always succeed; no check <= Arrow.any *)
266

267
268
269
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
270
271
272
273
274
275

  val need_arg : t -> bool
    (* True if the type of the argument is needed to obtain
       the type of the result (must use [apply]; otherwise,
       [apply_noarg] is enough *)
  val apply_noarg : t -> descr
276
277
278
end


279
module Int : sig
280
  val has_int : t -> Intervals.V.t -> bool
281
  val get: t -> BoolIntervals.t
282
  val any : t
283
284
end

285
module Atom : sig
286
  val has_atom : t -> Atoms.V.t -> bool
287
  val get: t -> BoolAtoms.t
288
  val any : t
289
290
end

291
module Char : sig
292
  val has_char : t -> Chars.V.t -> bool
293
  val is_empty : t -> bool
294
  val get: t -> BoolChars.t
295
  val any : t
296
297
end

298
299
val get_abstract: t -> Abstract.t

300
val normalize : t -> t
301

302
(** Subtyping  **)
303

304
305
306
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
307
val disjoint : t -> t -> bool
308
val equiv : t -> t -> bool
309

310
311
312
313
314
315
316
317
318
(** Tools for compilation of PM **)

val cond_partition: t -> (t * t) list -> t list
  (* The second argument is a list of pair of types (ti,si)
     interpreted as the question "member of ti under the assumption si".
     The result is a partition of the first argument which is precise enough
     to answer all the questions. *)


319
320
module Print :
sig
321
  val register_global : string -> Ns.QName.t -> t -> unit
322
  val print_const : Format.formatter -> const -> unit
323
  val print: Format.formatter -> t -> unit
324
  val print_node: Format.formatter -> Node.t -> unit
325
326
327

  (* Don't try to find a global name at toplevel *)
  val print_noname: Format.formatter -> t -> unit
328
329

  val to_string: t -> string
330
end
331

Jérôme Maloberti's avatar
Jérôme Maloberti committed
332
333
334
335
336
337
module Service :
sig
  val to_service_params: t -> service_params
  val to_string: service_params -> string
end

338
339
340
341
342
module Witness: sig
  type witness
  val print_witness: Format.formatter -> witness -> unit
end
val witness: t -> Witness.witness
343

344
345
346
347
348
349
350
351

module Cache: sig
  type 'a cache
  val emp: 'a cache
  val find: (t -> 'a) -> t -> 'a cache -> 'a cache * 'a

  val memo: (t -> 'a) -> (t -> 'a)
end