types.mli 9.33 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 114 115
val no_var : t -> bool
val is_var : t -> bool

116
val any_node : Node.t
117
val empty_node : Node.t
118

119
val non_constructed : t
120
val non_constructed_or_absent : t
121

122 123
(** Constructors **)

124 125
type pair_kind = [ `Normal | `XML ]

126
val var      : Var.var -> t
127 128
val interval : Intervals.t -> t
val atom     : Atoms.t -> t
129 130 131 132
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
133
  (** bool = true -> open record; bool = false -> closed record *)
134
val record_fields : bool * Node.t label_map -> t
135
val char     : Chars.t -> t
136
val constant : const -> t
137
val abstract : Abstract.t -> t
138

139 140
(** Helpers *)

141 142
val tuple : Node.t list -> t

143
val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
144

145
val empty_closed_record: t
146
val empty_open_record: t
147

Pietro Abate's avatar
Pietro Abate committed
148
(*
149
val subst : t -> Var.var * t -> t
Pietro Abate's avatar
Pietro Abate committed
150
*)
151

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

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

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

(** Normalization **)

module Product : sig
174 175
  val any : t
  val any_xml : t
176
  val any_of: pair_kind -> t
177 178
  val other : ?kind:pair_kind -> t -> t
  val is_product : ?kind:pair_kind -> t -> bool
179 180 181

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

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

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


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

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

216 217
  val has_absent: t -> bool
  val has_record: t -> bool
218

219 220
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
221

222 223 224
  val pi : label -> t -> t
    (* May contain absent *)

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

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


234
  val first_label: t -> label
235
  val all_labels: t -> LabelSet.t
236

237
  val empty_cases: t -> bool * bool
238

239 240
  val merge: t -> t -> t
  val remove_field: t -> label -> t
241

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


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
250 251
end

252
module Arrow : sig
253
  val any : t
254

255
  val sample: t -> t
256

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

265
  val check_iface: (t * t) list -> t -> bool
266

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

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
Pietro Abate's avatar
Pietro Abate committed
390
    type sl = (Var.var * t) list list
391 392 393 394 395 396 397 398 399

    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
400 401
    val union : s -> s -> s
    val prod : s -> s -> s
402 403
  end

404
  val norm : t -> CS.s
405
  val merge : CS.m -> CS.s
406 407
  val solve : CS.s -> CS.es
  val unify : CS.e -> CS.e
Pietro Abate's avatar
Pietro Abate committed
408
  val tallying : (t * t) list -> CS.sl
409

410 411
end

Pietro Abate's avatar
Pietro Abate committed
412
val apply : t -> t -> Tallying.CS.sl