types.mli 7.83 KB
Newer Older
1
2
open Ident

3
module BoolAtoms : BoolVar.S with
4
  type s = Atoms.t and
5
6
  type elem = Atoms.t Custom.pairvar
module BoolIntervals : BoolVar.S with
7
  type s = Intervals.t and
8
9
  type elem = Intervals.t Custom.pairvar
module BoolChars : BoolVar.S with
10
  type s = Chars.t and
11
12
  type elem = Chars.t Custom.pairvar

13
14
type const = 
  | Integer of Intervals.V.t
15
  | Atom of Atoms.V.t
16
  | Var of BoolVar.Vars.V.t
17
18
19
20
21
22
  | 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
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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;;
46

47
module Const: Custom.T with type t = const
48

49
(*
50
51
52
module CompUnit : sig
  include Custom.T

53
  val get_current: unit -> t
54
55
  val mk: U.t -> t
  val value: t -> U.t
56
  val print_qual: Format.formatter -> t -> unit
57
58
59
60
61
62
63
64
65

  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
66
*)
67

68
module Abstract : sig
69
70
  module T : Custom.T with type t = string
  type abs = T.t
71
72
73
  type t
  val any: t
  val atom: abs -> t
74
  val compare: t -> t -> int
75
76
77
78
79
80
81
82

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

  val contains: abs -> t -> bool
end

83
84
(** Algebra **)

85
86
include Custom.T
module Node : Custom.T
87

88
module Pair : Bool.S with type elem = (Node.t * Node.t)
89
module BoolPair : BoolVar.S with type s = Pair.t and type elem = Pair.t Custom.pairvar 
90
91

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

94
type descr = t
95

96
97
val make: unit -> Node.t
val define: Node.t -> t -> unit
98

99
100
val cons: t -> Node.t
val internalize: Node.t -> Node.t
101

102
103
val id: Node.t -> int
val descr: Node.t -> t
104

105
106
(** Boolean connectives **)

107
108
109
110
111
112
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
113

114
val any_node : Node.t
115
val empty_node : Node.t
116

117
val non_constructed : t
118
val non_constructed_or_absent : t
119

120
121
(** Constructors **)

122
123
type pair_kind = [ `Normal | `XML ]

124
125
val interval : BoolIntervals.t -> t
val atom     : BoolAtoms.t -> t
126
127
128
129
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
130
  (* bool = true -> open record; bool = false -> closed record *)
131
val record_fields : bool * Node.t label_map -> t
132
val char     : BoolChars.t -> t
133
val constant : const -> t
134
val abstract : Abstract.t -> t
135

136
137
(** Helpers *)

138
139
val tuple : Node.t list -> t

140
val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
141

142
val empty_closed_record: t
143
val empty_open_record: t
144

145
146
147
148
149
150
151
(** Positive systems and least solutions **)

module Positive :
sig
  type v
  val forward: unit -> v
  val define: v -> v -> unit
152
  val ty: t -> v
153
154
  val cup: v list -> v
  val times: v -> v -> v
155
  val xml: v -> v -> v
156

157
  val solve: v -> Node.t
158
159
160
161
162
end

(** Normalization **)

module Product : sig
163
164
  val any : t
  val any_xml : t
165
  val any_of: pair_kind -> t
166
167
  val other : ?kind:pair_kind -> t -> t
  val is_product : ?kind:pair_kind -> t -> bool
168
169
170

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
171
  val is_empty: t -> bool
172
  val get: ?kind:pair_kind -> descr -> t
173
174
  val pi1: t -> descr
  val pi2: t -> descr
175
  val pi2_restricted: descr -> t -> descr
176
177
178
179
180
181
182
    
  (* 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
183
  val normal: ?kind:pair_kind -> descr -> normal
184

185
186
187
188
  val constraint_on_2: normal -> descr -> descr
    (* constraint_on_2 n t1:  maximal t2 such that (t1,t2) <= n *)
    (* Assumption: t1 <= pi1(n) *)

189
190
  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
191
192
193
194


  val clean_normal: t -> t
    (* Merge rectangles with same second component *)
195
196
197
end

module Record : sig
198
  val any : t
199
200
  val absent : t
  val absent_node : Node.t
201
202
  val or_absent: t -> t
  val any_or_absent: t
203
  val any_or_absent_node : Node.t
204

205
206
  val has_absent: t -> bool
  val has_record: t -> bool
207

208
209
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
210

211
212
213
  val pi : label -> t -> t
    (* May contain absent *)

214
  val project : t -> label -> t
215
216
    (* Raise Not_found if label is not necessarily present *)

217
  val condition : t -> label -> t -> t
218
    (* condition t1 l t2 : What must follow if field l hash type t2 *)
219
220
  val project_opt : t -> label -> t
  val has_empty_record: t -> bool
221
222


223
  val first_label: t -> label
224
  val all_labels: t -> LabelSet.t
225

226
  val empty_cases: t -> bool * bool
227

228
229
  val merge: t -> t -> t
  val remove_field: t -> label -> t
230

231
  val get: t -> ((bool * t) label_map * bool * bool) list
232
233
234
235
236
237
238


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
239
240
end

241
module Arrow : sig
242
  val any : t
243

244
  val sample: t -> t
245

246
  val check_strenghten: t -> t -> t
247
248
249
250
251
252
253
    (* [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.
    *)

254
  val check_iface: (t * t) list -> t -> bool
255

256
  type t
257
  val is_empty: t -> bool
258
259
  val get: descr -> t
    (* Always succeed; no check <= Arrow.any *)
260

261
262
263
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
264
265
266
267
268
269

  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
270
271
272
end


273
module Int : sig
274
  val has_int : t -> Intervals.V.t -> bool
275
  val get: t -> BoolIntervals.t
276
  val any : t
277
278
end

279
module Atom : sig
280
  val has_atom : t -> Atoms.V.t -> bool
281
  val get: t -> BoolAtoms.t
282
  val any : t
283
284
end

285
module Char : sig
286
  val has_char : t -> Chars.V.t -> bool
287
  val is_empty : t -> bool
288
  val get: t -> BoolChars.t
289
  val any : t
290
291
end

292
293
val get_abstract: t -> Abstract.t

294
val normalize : t -> t
295

296
(** Subtyping  **)
297

298
299
300
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
301
val disjoint : t -> t -> bool
302
val equiv : t -> t -> bool
303

304
305
306
307
308
309
310
311
312
(** 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. *)


313
314
module Print :
sig
315
  val register_global : string -> Ns.QName.t -> t -> unit
316
  val print_const : Format.formatter -> const -> unit
317
  val print: Format.formatter -> t -> unit
318
  val print_node: Format.formatter -> Node.t -> unit
319
320
321

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

  val to_string: t -> string
324
end
325

Jérôme Maloberti's avatar
Jérôme Maloberti committed
326
327
328
329
330
331
module Service :
sig
  val to_service_params: t -> service_params
  val to_string: service_params -> string
end

332
333
334
335
336
module Witness: sig
  type witness
  val print_witness: Format.formatter -> witness -> unit
end
val witness: t -> Witness.witness
337

338
339
340
341
342
343
344
345

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