types.mli 7.83 KB
Newer Older
1 2
open Ident

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

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

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

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

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

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

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

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

  val contains: abs -> t -> bool
end

83 84
(** Algebra **)

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

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

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

94
type descr = t
95

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

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

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

105 106
(** Boolean connectives **)

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

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

117
val non_constructed : t
118
val non_constructed_or_absent : t
119

120 121
(** Constructors **)

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

124 125
val interval : BoolIntervals.t -> t
val atom     : BoolAtoms.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     : BoolChars.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 146 147 148 149 150 151
(** Positive systems and least solutions **)

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

157
  val solve: v -> Node.t
158 159 160 161 162
end

(** Normalization **)

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

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

185 186 187 188
  val constraint_on_2: normal -> descr -> descr
    (* constraint_on_2 n t1:  maximal t2 such that (t1,t2) <= n *)
    (* Assumption: t1 <= pi1(n) *)

189 190
  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
191 192 193 194


  val clean_normal: t -> t
    (* Merge rectangles with same second component *)
195 196 197
end

module Record : sig
198
  val any : t
199 200
  val absent : t
  val absent_node : Node.t
201 202
  val or_absent: t -> t
  val any_or_absent: t
203
  val any_or_absent_node : Node.t
204

205 206
  val has_absent: t -> bool
  val has_record: t -> bool
207

208 209
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
210

211 212 213
  val pi : label -> t -> t
    (* May contain absent *)

214
  val project : t -> label -> t
215 216
    (* Raise Not_found if label is not necessarily present *)

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


223
  val first_label: t -> label
224
  val all_labels: t -> LabelSet.t
225

226
  val empty_cases: t -> bool * bool
227

228 229
  val merge: t -> t -> t
  val remove_field: t -> label -> t
230

231
  val get: t -> ((bool * t) label_map * bool * bool) list
232 233 234 235 236 237 238


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
239 240
end

241
module Arrow : sig
242
  val any : t
243

244
  val sample: t -> t
245

246
  val check_strenghten: t -> t -> t
247 248 249 250 251 252 253
    (* [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.
    *)

254
  val check_iface: (t * t) list -> t -> bool
255

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

261 262 263
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
264 265 266 267 268 269

  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
270 271 272
end


273
module Int : sig
274
  val has_int : t -> Intervals.V.t -> bool
275
  val get: t -> BoolIntervals.t
276
  val any : t
277 278
end

279
module Atom : sig
280
  val has_atom : t -> Atoms.V.t -> bool
281
  val get: t -> BoolAtoms.t
282
  val any : t
283 284
end

285
module Char : sig
286
  val has_char : t -> Chars.V.t -> bool
287
  val is_empty : t -> bool
288
  val get: t -> BoolChars.t
289
  val any : t
290 291
end

292 293
val get_abstract: t -> Abstract.t

294
val normalize : t -> t
295

296
(** Subtyping  **)
297

298 299 300
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
301
val disjoint : t -> t -> bool
302
val equiv : t -> t -> bool
303

304 305 306 307 308 309 310 311 312
(** 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. *)


313 314
module Print :
sig
315
  val register_global : string -> Ns.QName.t -> t -> unit
316
  val print_const : Format.formatter -> const -> unit
317
  val print: Format.formatter -> t -> unit
318
  val print_node: Format.formatter -> Node.t -> unit
319 320 321

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

  val to_string: t -> string
324
end
325

Jérôme Maloberti's avatar
Jérôme Maloberti committed
326 327 328 329 330 331
module Service :
sig
  val to_service_params: t -> service_params
  val to_string: service_params -> string
end

332 333 334 335 336
module Witness: sig
  type witness
  val print_witness: Format.formatter -> witness -> unit
end
val witness: t -> Witness.witness
337

338 339 340 341 342 343 344 345

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