types.mli 7.25 KB
Newer Older
1 2
open Ident

3 4
type const = 
  | Integer of Intervals.V.t
5
  | Atom of Atoms.V.t
6
  | Var of Atoms.V.t
7 8 9 10 11 12
  | 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
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
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;;
36

37
module Const: Custom.T with type t = const
38

39
(*
40 41 42
module CompUnit : sig
  include Custom.T

43
  val get_current: unit -> t
44 45
  val mk: U.t -> t
  val value: t -> U.t
46
  val print_qual: Format.formatter -> t -> unit
47 48 49 50 51 52 53 54 55

  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
56
*)
57

58
module Abstract : sig
59 60
  module T : Custom.T with type t = string
  type abs = T.t
61 62 63
  type t
  val any: t
  val atom: abs -> t
64
  val compare: t -> t -> int
65 66 67 68 69 70 71 72

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

  val contains: abs -> t -> bool
end

73 74
(** Algebra **)

75 76
include Custom.T
module Node : Custom.T
77

78
type descr = t
79

80 81
val make: unit -> Node.t
val define: Node.t -> t -> unit
82

83 84
val cons: t -> Node.t
val internalize: Node.t -> Node.t
85

86 87
val id: Node.t -> int
val descr: Node.t -> t
88

89 90
(** Boolean connectives **)

91 92 93 94 95 96
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
97

98
val any_node : Node.t
99
val empty_node : Node.t
100

101
val non_constructed : t
102
val non_constructed_or_absent : t
103

104 105
(** Constructors **)

106 107
type pair_kind = [ `Normal | `XML ]

108 109
val interval : Intervals.t -> t
val atom     : Atoms.t -> t
110
val vars     : Atoms.t -> t
111 112 113 114
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
115
  (* bool = true -> open record; bool = false -> closed record *)
116
val record_fields : bool * Node.t label_map -> t
117 118
val char     : Chars.t -> t
val constant : const -> t
119
val abstract : Abstract.t -> t
120

121 122
(** Helpers *)

123 124
val tuple : Node.t list -> t

125
val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
126

127
val empty_closed_record: t
128
val empty_open_record: t
129

130 131 132 133 134 135 136
(** Positive systems and least solutions **)

module Positive :
sig
  type v
  val forward: unit -> v
  val define: v -> v -> unit
137
  val ty: t -> v
138 139
  val cup: v list -> v
  val times: v -> v -> v
140
  val xml: v -> v -> v
141

142
  val solve: v -> Node.t
143 144 145 146 147
end

(** Normalization **)

module Product : sig
148 149
  val any : t
  val any_xml : t
150
  val any_of: pair_kind -> t
151 152
  val other : ?kind:pair_kind -> t -> t
  val is_product : ?kind:pair_kind -> t -> bool
153 154 155

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
156
  val is_empty: t -> bool
157
  val get: ?kind:pair_kind -> descr -> t
158 159
  val pi1: t -> descr
  val pi2: t -> descr
160
  val pi2_restricted: descr -> t -> descr
161 162 163 164 165 166 167
    
  (* 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
168
  val normal: ?kind:pair_kind -> descr -> normal
169

170 171 172 173
  val constraint_on_2: normal -> descr -> descr
    (* constraint_on_2 n t1:  maximal t2 such that (t1,t2) <= n *)
    (* Assumption: t1 <= pi1(n) *)

174 175
  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
176 177 178 179


  val clean_normal: t -> t
    (* Merge rectangles with same second component *)
180 181 182
end

module Record : sig
183
  val any : t
184 185
  val absent : t
  val absent_node : Node.t
186 187
  val or_absent: t -> t
  val any_or_absent: t
188
  val any_or_absent_node : Node.t
189

190 191
  val has_absent: t -> bool
  val has_record: t -> bool
192

193 194
  val split : t -> label -> Product.t
  val split_normal : t -> label -> Product.normal
195

196 197 198
  val pi : label -> t -> t
    (* May contain absent *)

199
  val project : t -> label -> t
200 201
    (* Raise Not_found if label is not necessarily present *)

202
  val condition : t -> label -> t -> t
203
    (* condition t1 l t2 : What must follow if field l hash type t2 *)
204 205
  val project_opt : t -> label -> t
  val has_empty_record: t -> bool
206 207


208
  val first_label: t -> label
209
  val all_labels: t -> LabelSet.t
210

211
  val empty_cases: t -> bool * bool
212

213 214
  val merge: t -> t -> t
  val remove_field: t -> label -> t
215

216
  val get: t -> ((bool * t) label_map * bool * bool) list
217 218 219 220 221 222 223


  type t
  val focus: descr -> label -> t
  val get_this: t -> descr
  val need_others: t -> bool
  val constraint_on_others: t -> descr -> descr
224 225
end

226
module Arrow : sig
227
  val any : t
228

229
  val sample: t -> t
230

231
  val check_strenghten: t -> t -> t
232 233 234 235 236 237 238
    (* [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.
    *)

239
  val check_iface: (t * t) list -> t -> bool
240

241
  type t
242
  val is_empty: t -> bool
243 244
  val get: descr -> t
    (* Always succeed; no check <= Arrow.any *)
245

246 247 248
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
249 250 251 252 253 254

  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
255 256 257
end


258
module Int : sig
259
  val has_int : t -> Intervals.V.t -> bool
260 261
  val get: t -> Intervals.t
  val any : t
262 263
end

264
module Atom : sig
265
  val has_atom : t -> Atoms.V.t -> bool
266 267
  val get: t -> Atoms.t
  val any : t
268 269
end

270
module Char : sig
271
  val has_char : t -> Chars.V.t -> bool
272 273 274
  val is_empty : t -> bool
  val get: t -> Chars.t
  val any : t
275 276
end

277 278
val get_abstract: t -> Abstract.t

279
val normalize : t -> t
280

281
(** Subtyping  **)
282

283 284 285
val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool
286
val disjoint : t -> t -> bool
287
val equiv : t -> t -> bool
288

289 290 291 292 293 294 295 296 297
(** 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. *)


298 299
module Print :
sig
300
  val register_global : string -> Ns.QName.t -> t -> unit
301
  val print_const : Format.formatter -> const -> unit
302
  val print: Format.formatter -> t -> unit
303
  val print_node: Format.formatter -> Node.t -> unit
304 305 306

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

  val to_string: t -> string
309
end
310

Jérôme Maloberti's avatar
Jérôme Maloberti committed
311 312 313 314 315 316
module Service :
sig
  val to_service_params: t -> service_params
  val to_string: service_params -> string
end

317 318 319 320 321
module Witness: sig
  type witness
  val print_witness: Format.formatter -> witness -> unit
end
val witness: t -> Witness.witness
322

323 324 325 326 327 328 329 330

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