types.mli 8.34 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 : Intervals.t -> t
val atom     : Atoms.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     : Chars.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
  val getpair: ?kind:pair_kind -> descr -> BoolPair.t
174 175
  val pi1: t -> descr
  val pi2: t -> descr
176
  val pi2_restricted: descr -> t -> descr
177 178 179 180 181 182 183
    
  (* 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
184
  val normal: ?kind:pair_kind -> descr -> normal
185

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

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


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

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

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

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

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

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

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


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

227
  val empty_cases: t -> bool * bool
228

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

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


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

242
module Arrow : sig
243
  val any : t
244

245
  val sample: t -> t
246

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

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

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

262 263
  val getpair: descr -> BoolPair.t

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

  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
273 274 275
end


276
module Int : sig
277
  val has_int : t -> Intervals.V.t -> bool
278
  val get: t -> BoolIntervals.t
279
  val any : t
280 281
end

282
module Atom : sig
283
  val has_atom : t -> Atoms.V.t -> bool
284
  val get: t -> BoolAtoms.t
285
  val any : t
286 287
end

288
module Char : sig
289
  val has_char : t -> Chars.V.t -> bool
290
  val is_empty : t -> bool
291
  val get: t -> BoolChars.t
292
  val any : t
293 294
end

295 296
val get_abstract: t -> Abstract.t

297
val normalize : t -> t
298

299
(** Subtyping  **)
300

301 302 303
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
304
val disjoint : t -> t -> bool
305
val equiv : t -> t -> bool
306

307 308 309 310 311 312 313 314 315
(** 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. *)


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

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

  val to_string: t -> string
327
end
328

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

335
module Witness : sig
336 337 338 339
  type witness
  val print_witness: Format.formatter -> witness -> unit
end
val witness: t -> Witness.witness
340

341

342
module Cache : sig
343 344 345 346 347 348
  type 'a cache
  val emp: 'a cache
  val find: (t -> 'a) -> t -> 'a cache -> 'a cache * 'a

  val memo: (t -> 'a) -> (t -> 'a)
end
349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368

module Tallying : sig
  type constr = (bool * Custom.var * t)

  module CS : sig
    type key = (bool * Custom.var)
    module M : Map.S with type key = key
    module S : Set.S with type elt = t M.t
    type cset = S.t
    val merge : S.elt -> S.elt -> S.elt
    val singleton : constr -> cset
    val sat : cset
    val unsat : cset
    val cup : cset -> cset -> cset
    val cap : cset -> cset -> cset
  end

  val norm : t -> CS.cset
end