types.mli 9.25 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

145
val subst : t -> Var.var * t -> t
146

147 148 149 150 151 152 153
(** Positive systems and least solutions **)

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

159
  val decompose : t -> v
160
  val substitute : t -> Var.var -> t
161
  val solve: v -> Node.t
162 163 164 165 166
end

(** Normalization **)

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

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

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

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


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

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

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

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

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

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

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


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

231
  val empty_cases: t -> bool * bool
232

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

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


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

246
module Arrow : sig
247
  val any : t
248

249
  val sample: t -> t
250

251
  val check_strenghten: t -> t -> t
252 253 254 255 256 257 258
    (* [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.
    *)

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

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

266 267
  val getpair: descr -> BoolPair.t

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

  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
277 278 279
end


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

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

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

299 300
val get_abstract: t -> Abstract.t

301
val normalize : t -> t
302

303
(** Subtyping  **)
304

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

311 312 313 314 315 316 317 318 319
(** 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. *)


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

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

  val to_string: t -> string
331
end
332

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

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

345

346
module Cache : sig
347 348 349 350 351 352
  type 'a cache
  val emp: 'a cache
  val find: (t -> 'a) -> t -> 'a cache -> 'a cache * 'a

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

module Tallying : sig
355 356 357 358

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

360 361
  exception UnSatConstr

362
  module CS : sig
363 364 365 366 367 368 369 370
    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
371 372 373 374
    module ES : sig
      include Set.S with type elt = descr E.t
      val print : Format.formatter -> t -> unit
    end
375 376 377 378 379 380 381 382
    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
383
    type es = ES.t
384 385 386 387 388 389 390 391 392

    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
393 394
    val union : s -> s -> s
    val prod : s -> s -> s
395 396
  end

397
  val norm : t -> CS.s
398
  val merge : CS.m -> CS.s
399 400
  val solve : CS.s -> CS.es
  val unify : CS.e -> CS.e
401
  val tallying : (t * t) list -> (Var.var * t) list list
402

403 404
end

Pietro Abate's avatar
Pietro Abate committed
405 406
  val appl : t -> t -> (Var.var * t) list list