types.mli 9.37 KB
Newer Older
1 2
open Ident

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

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

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

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

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

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

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

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

  val contains: abs -> t -> bool
end

82 83
(** Algebra **)

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

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

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

93
type descr = t
94

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

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

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

104 105
(** Boolean connectives **)

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

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

116
val non_constructed : t
117
val non_constructed_or_absent : t
118

119 120
(** Constructors **)

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

123
val var      : Var.var -> t
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

Pietro Abate's avatar
Pietro Abate committed
145
(*
146
val subst : t -> Var.var * t -> t
Pietro Abate's avatar
Pietro Abate committed
147
*)
148

149 150 151 152 153 154 155
(** Positive systems and least solutions **)

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

161
  val decompose : t -> v
Pietro Abate's avatar
Pietro Abate committed
162 163
  val substitute : t -> (Var.var * t) -> t
  val substituterec : t -> Var.var -> t
164
  val solve: v -> Node.t
Pietro Abate's avatar
Pietro Abate committed
165
  val substitutefree : t -> t
166 167 168 169 170
end

(** Normalization **)

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

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
179
  val is_empty: t -> bool
180
  val get: ?kind:pair_kind -> descr -> t
181
  val getpair: ?kind:pair_kind -> descr -> BoolPair.t
182 183
  val pi1: t -> descr
  val pi2: t -> descr
184
  val pi2_restricted: descr -> t -> descr
185 186 187 188 189 190 191
    
  (* 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
192
  val normal: ?kind:pair_kind -> descr -> normal
193

194 195 196 197
  val constraint_on_2: normal -> descr -> descr
    (* constraint_on_2 n t1:  maximal t2 such that (t1,t2) <= n *)
    (* Assumption: t1 <= pi1(n) *)

198 199
  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
200 201 202 203


  val clean_normal: t -> t
    (* Merge rectangles with same second component *)
204 205 206
end

module Record : sig
207
  val any : t
208 209
  val absent : t
  val absent_node : Node.t
210 211
  val or_absent: t -> t
  val any_or_absent: t
212
  val any_or_absent_node : Node.t
213

214 215
  val has_absent: t -> bool
  val has_record: t -> bool
216

217 218
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
219

220 221 222
  val pi : label -> t -> t
    (* May contain absent *)

223
  val project : t -> label -> t
224 225
    (* Raise Not_found if label is not necessarily present *)

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


232
  val first_label: t -> label
233
  val all_labels: t -> LabelSet.t
234

235
  val empty_cases: t -> bool * bool
236

237 238
  val merge: t -> t -> t
  val remove_field: t -> label -> t
239

240
  val get: t -> ((bool * t) label_map * bool * bool) list
241 242 243 244 245 246 247


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
248 249
end

250
module Arrow : sig
251
  val any : t
252

253
  val sample: t -> t
254

255
  val check_strenghten: t -> t -> t
256 257 258 259 260 261 262
    (* [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.
    *)

263
  val check_iface: (t * t) list -> t -> bool
264

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

270 271
  val getpair: descr -> BoolPair.t

272 273 274
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
275 276 277 278 279 280

  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
281 282 283
end


284
module Int : sig
285
  val has_int : t -> Intervals.V.t -> bool
286
  val get: t -> BoolIntervals.t
287
  val any : t
288 289
end

290
module Atom : sig
291
  val has_atom : t -> Atoms.V.t -> bool
292
  val get: t -> BoolAtoms.t
293
  val any : t
294 295
end

296
module Char : sig
297
  val has_char : t -> Chars.V.t -> bool
298
  val is_empty : t -> bool
299
  val get: t -> BoolChars.t
300
  val any : t
301 302
end

303 304
val get_abstract: t -> Abstract.t

305
val normalize : t -> t
306

307
(** Subtyping  **)
308

309 310 311
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
312
val disjoint : t -> t -> bool
313
val equiv : t -> t -> bool
314

315 316 317 318 319 320 321 322 323
(** 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. *)


324 325
module Print :
sig
326
  val register_global : string -> Ns.QName.t -> t -> unit
327
  val print_const : Format.formatter -> const -> unit
328
  val print: Format.formatter -> t -> unit
329
  val print_node: Format.formatter -> Node.t -> unit
330 331 332

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

  val to_string: t -> string
335
end
336

Jérôme Maloberti's avatar
Jérôme Maloberti committed
337 338 339 340 341 342
module Service :
sig
  val to_service_params: t -> service_params
  val to_string: service_params -> string
end

343
module Witness : sig
344 345 346 347
  type witness
  val print_witness: Format.formatter -> witness -> unit
end
val witness: t -> Witness.witness
348

349

350
module Cache : sig
351 352 353 354 355 356
  type 'a cache
  val emp: 'a cache
  val find: (t -> 'a) -> t -> 'a cache -> 'a cache * 'a

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

module Tallying : sig
359 360 361 362

  type constr =
  |Pos of (Var.var * t) (** alpha <= t | alpha \in P *)
  |Neg of (t * Var.var) (** t <= alpha | alpha \in N *)
363

364
  exception UnSatConstr
365 366
  exception Step1Fail
  exception Step2Fail
367

368
  module CS : sig
369 370 371 372 373 374 375 376
    module M : sig 
      include Map.S with type key = (bool * Var.var)
      val print : Format.formatter -> descr t -> unit
    end
    module E : sig
      include Map.S with type key = Var.var
      val print : Format.formatter -> descr t -> unit
    end
377 378 379 380
    module ES : sig
      include Set.S with type elt = descr E.t
      val print : Format.formatter -> t -> unit
    end
381 382 383 384 385 386 387 388
    module S : sig
      include Set.S with type elt = descr M.t
      val print : Format.formatter -> t -> unit
    end

    type s = S.t
    type m = t M.t
    type e = t E.t
389
    type es = ES.t
390 391 392 393 394 395 396 397 398

    val print : Format.formatter -> s -> unit
    val print_m : Format.formatter -> m -> unit
    val print_e : Format.formatter -> e -> unit

    val merge : m -> m -> m
    val singleton : constr -> s
    val sat : s
    val unsat : s
Pietro Abate's avatar
Pietro Abate committed
399 400
    val union : s -> s -> s
    val prod : s -> s -> s
401 402
  end

403
  val norm : t -> CS.s
404
  val merge : CS.m -> CS.s
405 406
  val solve : CS.s -> CS.es
  val unify : CS.e -> CS.e
407
  val tallying : (t * t) list -> (Var.var * t) list list
408

409 410
end

Pietro Abate's avatar
Pietro Abate committed
411
val apply : t -> t -> (Var.var * t) list list