types.mli 9.01 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 solve: v -> Node.t
160 161 162 163 164
end

(** Normalization **)

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

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

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

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


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

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

208 209
  val has_absent: t -> bool
  val has_record: t -> bool
210

211 212
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
213

214 215 216
  val pi : label -> t -> t
    (* May contain absent *)

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

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


226
  val first_label: t -> label
227
  val all_labels: t -> LabelSet.t
228

229
  val empty_cases: t -> bool * bool
230

231 232
  val merge: t -> t -> t
  val remove_field: t -> label -> t
233

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


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
242 243
end

244
module Arrow : sig
245
  val any : t
246

247
  val sample: t -> t
248

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

257
  val check_iface: (t * t) list -> t -> bool
258

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

264 265
  val getpair: descr -> BoolPair.t

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

  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
275 276 277
end


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

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

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

297 298
val get_abstract: t -> Abstract.t

299
val normalize : t -> t
300

301
(** Subtyping  **)
302

303 304 305
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
306
val disjoint : t -> t -> bool
307
val equiv : t -> t -> bool
308

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


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

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

  val to_string: t -> string
329
end
330

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

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

343

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

  val memo: (t -> 'a) -> (t -> 'a)
end
351 352

module Tallying : sig
353 354 355 356

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

358 359
  exception UnSatConstr

360
  module CS : sig
361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387
    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
    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

    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
    val cup : s -> s -> s
    val cap : s -> s -> s
388 389
  end

390
  val norm : t -> CS.s
391 392
  val merge : CS.m -> CS.s
  val solve : CS.s -> CS.e list
393 394
  val unify : CS.e -> (Var.var * t) list
  val tallying : (t * t) list -> (Var.var * t) list list
395

396 397
end