types.mli 7.97 KB
Newer Older
1 2
open Ident

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
module Vars : sig 
  module V : Custom.T with type t = string
  include Bool.S
end

module BoolAtoms : BoolVar.S with
  type bt = Atoms.t and
  type elem = Atoms.t Custom.pairvar
module BoolIntervals : BoolVar.S with
  type bt = Intervals.t and
  type elem = Intervals.t Custom.pairvar
module BoolChars : BoolVar.S with
  type bt = Chars.t and
  type elem = Chars.t Custom.pairvar
module BoolVars : BoolVar.S with type elem = Vars.t Custom.pairvar

19 20
type const = 
  | Integer of Intervals.V.t
21
  | Atom of Atoms.V.t
22
  | Var of Vars.V.t
23 24 25 26 27 28
  | 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
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
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;;
52

53
module Const: Custom.T with type t = const
54

55
(*
56 57 58
module CompUnit : sig
  include Custom.T

59
  val get_current: unit -> t
60 61
  val mk: U.t -> t
  val value: t -> U.t
62
  val print_qual: Format.formatter -> t -> unit
63 64 65 66 67 68 69 70 71

  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
72
*)
73

74
module Abstract : sig
75 76
  module T : Custom.T with type t = string
  type abs = T.t
77 78 79
  type t
  val any: t
  val atom: abs -> t
80
  val compare: t -> t -> int
81 82 83 84 85 86 87 88

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

  val contains: abs -> t -> bool
end

89 90
(** Algebra **)

91 92
include Custom.T
module Node : Custom.T
93

94 95 96 97 98 99
module Pair : Bool.S with type elem = (Node.t * Node.t)
module BoolPair : BoolVar.S with type bt = Pair.t and type elem = Pair.t Custom.pairvar 

module Rec : Bool.S with type elem = bool * Node.t Ident.label_map
module BoolRec : BoolVar.S with type bt = Rec.t and type elem = Rec.t Custom.pairvar

100
type descr = t
101

102 103
val make: unit -> Node.t
val define: Node.t -> t -> unit
104

105 106
val cons: t -> Node.t
val internalize: Node.t -> Node.t
107

108 109
val id: Node.t -> int
val descr: Node.t -> t
110

111 112
(** Boolean connectives **)

113 114 115 116 117 118
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
119

120
val any_node : Node.t
121
val empty_node : Node.t
122

123
val non_constructed : t
124
val non_constructed_or_absent : t
125

126 127
(** Constructors **)

128 129
type pair_kind = [ `Normal | `XML ]

130 131
val interval : BoolIntervals.t -> t
val atom     : BoolAtoms.t -> t
132 133 134 135
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
136
  (* bool = true -> open record; bool = false -> closed record *)
137
val record_fields : bool * Node.t label_map -> t
138
val char     : BoolChars.t -> t
139
val constant : const -> t
140
val abstract : Abstract.t -> t
141

142 143
(** Helpers *)

144 145
val tuple : Node.t list -> t

146
val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
147

148
val empty_closed_record: t
149
val empty_open_record: t
150

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

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

163
  val solve: v -> Node.t
164 165 166 167 168
end

(** Normalization **)

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

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

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

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


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

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

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

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

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

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

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


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

232
  val empty_cases: t -> bool * bool
233

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

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


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

247
module Arrow : sig
248
  val any : t
249

250
  val sample: t -> t
251

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

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

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

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

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


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

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

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

298 299
val get_abstract: t -> Abstract.t

300
val normalize : t -> t
301

302
(** Subtyping  **)
303

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

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


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

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

  val to_string: t -> string
330
end
331

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

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

344 345 346 347 348 349 350 351

module Cache: sig
  type 'a cache
  val emp: 'a cache
  val find: (t -> 'a) -> t -> 'a cache -> 'a cache * 'a

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