types.ml 96.8 KB
Newer Older
1
open Ident
2
open Encodings
3

4
let count = ref 0
Pietro Abate's avatar
Pietro Abate committed
5

6 7 8 9
let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)

Pietro Abate's avatar
Pietro Abate committed
10
(*
11 12 13 14 15 16 17 18
To be sure not to use generic comparison ...
*)
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1

Pietro Abate's avatar
Pietro Abate committed
19
type const =
20
  | Integer of Intervals.V.t
21
  | Atom of Atoms.V.t
22
  | Char of Chars.V.t
23 24 25 26
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
27

Jérôme Maloberti's avatar
Jérôme Maloberti committed
28 29
type service_params =
  | TProd of service_params * service_params
Pietro Abate's avatar
Pietro Abate committed
30
  | TOption of service_params
Jérôme Maloberti's avatar
Jérôme Maloberti committed
31 32 33 34 35 36 37
  | 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
Pietro Abate's avatar
Pietro Abate committed
38
  | TFloat of string
Jérôme Maloberti's avatar
Jérôme Maloberti committed
39 40 41
  | TBool of string
  | TFile of string
      (* | TUserType of string * (string -> 'a) * ('a -> string) *)
Pietro Abate's avatar
Pietro Abate committed
42
  | TCoord of string
Jérôme Maloberti's avatar
Jérôme Maloberti committed
43
  | TCoordv of service_params * string
Pietro Abate's avatar
Pietro Abate committed
44
  | TESuffix of string
Jérôme Maloberti's avatar
Jérôme Maloberti committed
45 46 47
  | TESuffixs of string
      (*  | TESuffixu of (string * (string -> 'a) * ('a -> string)) *)
  | TSuffix of (bool * service_params)
Pietro Abate's avatar
Pietro Abate committed
48
  | TUnit
Jérôme Maloberti's avatar
Jérôme Maloberti committed
49 50 51
  | TAny
  | TConst of string;;

52 53 54
module Const = struct
  type t = const

55 56
  let check _ = ()
  let dump ppf _ = Format.fprintf ppf "<Types.Const.t>"
57 58

  let rec compare c1 c2 = match (c1,c2) with
59
    | Integer x, Integer y -> Intervals.V.compare x y
60 61
    | Integer _, _ -> -1
    | _, Integer _ -> 1
62
    | Atom x, Atom y -> Atoms.V.compare x y
63 64
    | Atom _, _ -> -1
    | _, Atom _ -> 1
65

66
    | Char x, Char y -> Chars.V.compare x y
67 68 69
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
70 71
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
72 73 74
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
75 76
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
77 78 79
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
80
	LabelMap.compare compare x y
81 82 83
    | Record _, _ -> -1
    | _, Record _ -> 1
    | String (i1,j1,s1,r1), String (i2,j2,s2,r2) ->
Pietro Abate's avatar
Pietro Abate committed
84
	let c = Pervasives.compare i1 i2 in if c <> 0 then c
85 86 87
	else let c = Pervasives.compare j1 j2 in if c <> 0 then c
	else let c = U.compare s1 s2 in if c <> 0 then c (* Should compare
							    only the substring *)
88 89 90 91 92 93 94 95 96 97
	else compare r1 r2

  let rec hash = function
    | Integer x -> 1 + 17 * (Intervals.V.hash x)
    | Atom x -> 2 + 17 * (Atoms.V.hash x)
    | Char x -> 3 + 17 * (Chars.V.hash x)
    | Pair (x,y) -> 4 + 17 * (hash x) + 257 * (hash y)
    | Xml (x,y) -> 5 + 17 * (hash x) + 257 * (hash y)
    | Record x -> 6 + 17 * (LabelMap.hash hash x)
    | String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash r
98
      (* Note: improve hash for String *)
99

100 101
  let equal c1 c2 = compare c1 c2 = 0
end
102

103 104 105
module Abstracts
  =
struct
106
  module T = Custom.String
107

108
  module V = struct type t = T.t * Obj.t end
109 110

  include SortedList.FiniteCofinite(T)
111 112 113 114 115
  let trivially_disjoint = disjoint
  let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
  let get _ = assert false
  let iter _ = assert false

116
  let full = any
117 118

  let print = function
119
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
120
    | Cofinite l ->
121 122 123 124
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]
125

126 127 128 129
  let contains_sample s t = match s,t with
    | None, Cofinite _ -> true
    | None, Finite _ -> false
    | Some s, t -> contains s t
Pietro Abate's avatar
Pietro Abate committed
130

131 132
end

133
type pair_kind = [ `Normal | `XML ]
134 135 136 137 138 139 140 141 142 143 144 145 146
type type_kind = [ `atoms | `intervals | `chars | `times | `xml | `arrow | `record | `abstracts ]

let pp_type_kind ppf k =
  Format.fprintf ppf "%s" (match k with
    `atoms  -> "atoms" 
  | `intervals -> "intervals"
  | `chars -> "chars"
  | `times -> "times"
  | `xml -> "xml"
  | `arrow -> "arrow"
  | `record -> "record"
  | `abstracts  -> "abstracts"
  )
147

148 149 150 151 152 153 154 155 156 157 158 159 160
type ('atoms, 'ints, 'chars, 'times, 'xml, 'arrow, 'record, 'abstract) descr_ =
  {
    atoms    : 'atoms;
    ints     : 'ints;
    chars    : 'chars;
    times    : 'times;
    xml      : 'xml;
    arrow    : 'arrow;
    record   : 'record;
    abstract : 'abstract;
    absent   : bool;
  }

161
module type VarTypeSig =
162 163 164
  sig
    include Bool.V
    type descr
165
    val kind : type_kind
166 167
    val inj : t -> descr
    val proj : descr -> t
168
    val update : descr -> t -> descr
169
  end
170

171 172 173 174 175 176 177 178 179
let empty_descr_ = { atoms = Bool.empty;
		     ints = Bool.empty;
		     chars = Bool.empty;
		     times = Bool.empty;
		     xml = Bool.empty;
		     arrow = Bool.empty;
		     record = Bool.empty;
		     abstract = Bool.empty;
		     absent = false }
180

Pietro Abate's avatar
Pietro Abate committed
181
module rec Descr :
182
sig
183
  include Custom.T with
184 185
	    type t = (VarAtoms.t, VarIntervals.t, VarChars.t, VarTimes.t,
		      VarXml.t, VarArrow.t, VarRec.t, VarAbstracts.t) descr_
186
  val empty: t
Julien Lopez's avatar
Julien Lopez committed
187
  val any : t
Julien Lopez's avatar
Julien Lopez committed
188
  val is_empty : t -> bool
189 190
  val get_absent : t -> bool
  val set_absent : t -> bool -> t
191 192
end =
struct
193

194 195
  type t = (VarAtoms.t, VarIntervals.t, VarChars.t, VarTimes.t,
	    VarXml.t, VarArrow.t, VarRec.t, VarAbstracts.t) descr_
196

197
  let dump ppf d =
198 199 200 201 202
    Format.fprintf ppf "@[<v 1>types:@\n\
@<1>    atoms: %a@\n\
@<1>     ints: %a@\n\
@<1>    chars: %a@\n\
@<1>    times: %a@\n\
203
@<1>      xml: %a@\n\
204 205 206 207
@<1>    arrow: %a@\n\
@<1>   record: %a@\n\
@<1> abstract: %a@\n\
@<1>   absent: %b@]@\n"
208 209 210 211 212 213 214 215
      VarAtoms.dump d.atoms
      VarIntervals.dump d.ints
      VarChars.dump d.chars
      VarTimes.dump d.times
      VarXml.dump d.xml
      VarArrow.dump d.arrow
      VarRec.dump d.record
      VarAbstracts.dump d.abstract
216
      d.absent
217

218
  let empty = empty_descr_
219

Julien Lopez's avatar
Julien Lopez committed
220
  let any =  {
221 222 223 224 225 226 227 228
    ints  = VarIntervals.full;
    atoms = VarAtoms.full;
    chars = VarChars.full;
    times = VarTimes.full;
    xml   = VarXml.full;
    arrow = VarArrow.full;
    record = VarRec.full;
    abstract = VarAbstracts.full;
229
    absent = false;
Julien Lopez's avatar
Julien Lopez committed
230 231
  }

232
  let check a =
233 234 235 236 237 238 239 240
    VarChars.check a.chars;
    VarIntervals.check a.ints;
    VarAtoms.check a.atoms;
    VarTimes.check a.times;
    VarXml.check a.xml;
    VarArrow.check a.arrow;
    VarRec.check a.record;
    VarAbstracts.check a.abstract;
241 242
    ()

243
  let equal a b =
244
    (a == b) || (
245 246 247 248 249 250 251 252
      (VarAtoms.equal a.atoms b.atoms) &&
      (VarChars.equal a.chars b.chars) &&
      (VarIntervals.equal a.ints  b.ints) &&
      (VarTimes.equal a.times b.times) &&
      (VarXml.equal a.xml b.xml) &&
      (VarArrow.equal a.arrow b.arrow) &&
      (VarRec.equal a.record b.record) &&
      (VarAbstracts.equal a.abstract b.abstract) &&
253 254
      (a.absent == b.absent)
    )
255

Julien Lopez's avatar
Julien Lopez committed
256
  let is_empty a =
257 258 259 260 261 262 263 264
    (VarAtoms.is_empty a.atoms) &&
      (VarChars.is_empty a.chars) &&
      (VarIntervals.is_empty a.ints) &&
      (VarTimes.is_empty a.times) &&
      (VarXml.is_empty a.xml) &&
      (VarArrow.is_empty a.arrow) &&
      (VarRec.is_empty a.record) &&
      (VarAbstracts.is_empty a.abstract)
Julien Lopez's avatar
Julien Lopez committed
265

266
  let compare a b =
Pietro Abate's avatar
Pietro Abate committed
267
    if a == b then 0
268 269 270 271 272 273 274 275
    else let c = VarAtoms.compare a.atoms b.atoms in if c <> 0 then c
    else let c = VarChars.compare a.chars b.chars in if c <> 0 then c
    else let c = VarIntervals.compare a.ints b.ints in if c <> 0 then c
    else let c = VarTimes.compare a.times b.times in if c <> 0 then c
    else let c = VarXml.compare a.xml b.xml in if c <> 0 then c
    else let c = VarArrow.compare a.arrow b.arrow in if c <> 0 then c
    else let c = VarRec.compare a.record b.record in if c <> 0 then c
    else let c = VarAbstracts.compare a.abstract b.abstract in if c <> 0 then c
276 277 278
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
Pietro Abate's avatar
Pietro Abate committed
279

280
  let hash a =
281 282 283 284 285 286 287 288
    let accu = VarChars.hash a.chars in
    let accu = 17 * accu + VarIntervals.hash a.ints in
    let accu = 17 * accu + VarAtoms.hash a.atoms in
    let accu = 17 * accu + VarTimes.hash a.times in
    let accu = 17 * accu + VarXml.hash a.xml in
    let accu = 17 * accu + VarArrow.hash a.arrow in
    let accu = 17 * accu + VarRec.hash a.record in
    let accu = 17 * accu + VarAbstracts.hash a.abstract in
289 290
    let accu = if a.absent then accu+5 else accu in
    accu
291

292 293
  let get_absent t = t.absent
  let set_absent t b = { t with absent = b }
294 295 296
end
and Node :
sig
297
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
298 299 300 301 302
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
303
  val mk: int -> Descr.t -> t
304
end =
305

306
struct
307
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
308
  let check n = ()
309
  let dump ppf n = Format.fprintf ppf "X%i" n.id
310
  let hash x = x.id + Compunit.hash x.cu
Pietro Abate's avatar
Pietro Abate committed
311
  let compare x y =
312 313
    let c = x.id - y.id in if c = 0 then Compunit.compare x.cu y.cu else c
  let equal x y = x==y || (x.id == y.id && (Compunit.equal x.cu y.cu))
314

315
  let mk id d = { id = id; cu = Compunit.current (); descr = d }
316

317
end
318
and VarAtoms : VarTypeSig with type Atom.t = Atoms.t
319 320 321 322 323
			 and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Atoms)
     type descr = Descr.t
324
     let kind = `atoms
325 326
     let inj t = { empty_descr_ with atoms = t }
     let proj t = t.atoms
327
     let update t d = { t with atoms = d }
328 329
   end

330
and VarIntervals : VarTypeSig with type Atom.t = Intervals.t
331 332 333 334 335
			     and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Intervals)
     type descr = Descr.t
336
     let kind = `intervals
337 338
     let inj t = { empty_descr_ with ints = t }
     let proj t = t.ints
339
     let update t d = { t with ints = d }
340 341
   end

342
and VarChars : VarTypeSig with type Atom.t = Chars.t
343 344 345 346 347
			 and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Chars)
     type descr = Descr.t
348
     let kind = `chars
349 350
     let inj t = { empty_descr_ with chars = t }
     let proj t = t.chars
351
     let update t d = { t with chars = d }
352 353
   end

354
and VarAbstracts : VarTypeSig with type Atom.t = Abstracts.t
355 356 357 358 359
			     and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Abstracts)
     type descr = Descr.t
360
     let kind = `abstracts
361 362
     let inj t = { empty_descr_ with abstract = t }
     let proj t = t.abstract
363
     let update t d = { t with abstract = d }
364
   end
365

366 367
and Pair : Bool.S with type elem = (Node.t * Node.t) =
  Bool.Make(Custom.Pair(Node)(Node))
368

369
and VarTimes : VarTypeSig with module Atom = Pair
370 371 372 373
                              and type descr = Descr.t
=
  struct include Bool.MakeVar(Pair)
  type descr = Descr.t
374
  let kind = `times
375 376
  let inj (t : t) : descr = { empty_descr_ with times = t }
  let proj (t : descr) : t = t.times
377
  let update (t : descr) (d : t) : descr = { t with times = d }
378 379
end

380
and VarXml : VarTypeSig with module Atom = Pair
381 382 383 384
                       and type descr = Descr.t
=
  struct include Bool.MakeVar(Pair)
  type descr = Descr.t
385
  let kind = `xml
386 387
  let inj (t : t) : descr = { empty_descr_ with xml = t }
  let proj (t : descr) : t = t.xml
388
  let update (t : descr) (d : t) : descr = { t with xml = d }
389 390
end

391
and VarArrow : VarTypeSig with module Atom = Pair
392 393 394 395
                       and type descr = Descr.t
=
  struct include Bool.MakeVar(Pair)
  type descr = Descr.t
396
  let kind = `arrow
397 398
  let inj (t : t) : descr = { empty_descr_ with arrow = t }
  let proj (t : descr) : t = t.arrow
399
  let update (t : descr) (d : t) : descr = { t with arrow = d }
400
end
401

402 403 404
(* bool = true means that the record is open that is, that
 * the labels that are not in the domain of the map are
 * equal to "any" *)
405

406 407
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
  Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
408

409
and VarRec : VarTypeSig with module Atom = Rec
410 411 412 413
                       and type descr = Descr.t
=
  struct include Bool.MakeVar(Rec)
  type descr = Descr.t
414
  let kind = `record
415 416
  let inj (t : t) : descr = { empty_descr_ with record = t }
  let proj (t : descr) : t = t.record
417
  let update (t : descr) (d : t) : descr = { t with record = d }
418
end
419

420
module type VarType = VarTypeSig with type descr = Descr.t
421
type var_type = (module VarType)
422

423 424
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
425 426
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
427

428 429 430
type descr = Descr.t
type node = Node.t
include Descr
431

432 433
let dummy_print = (fun _ _ -> assert false)
let forward_print = ref dummy_print
434

Pietro Abate's avatar
Pietro Abate committed
435 436
let make () =
  incr count;
437 438
  Node.mk !count empty

Pietro Abate's avatar
Pietro Abate committed
439
let define n d =
440 441
  n.Node.descr <- d

Pietro Abate's avatar
Pietro Abate committed
442 443
let cons d =
  incr count;
444 445
  Node.mk !count d

446 447 448 449
let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id

450
let non_constructed =
Pietro Abate's avatar
Pietro Abate committed
451
  { any with
452
      times = empty.times; xml = empty.xml; record = empty.record }
Pietro Abate's avatar
Pietro Abate committed
453 454

let non_constructed_or_absent =
455
  { non_constructed with absent = true }
456

Pietro Abate's avatar
Pietro Abate committed
457
(* Descr.t type constructors *)
458 459 460
let times x y = VarTimes.inj (VarTimes.atom (`Atm (Pair.atom (x,y))))
let xml x y = VarXml.inj (VarXml.atom (`Atm (Pair.atom (x,y))))
let arrow x y = VarArrow.inj (VarArrow.atom (`Atm (Pair.atom (x,y))))
461

Pietro Abate's avatar
Pietro Abate committed
462
let record label t =
463
  VarRec.inj (VarRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))))
464

465
let record_fields x =
466
  VarRec.inj (VarRec.atom (`Atm (Rec.atom x)))
467

468
let atom a = VarAtoms.inj (VarAtoms.atom (`Atm a))
469 470

(* Atm = Any ^ a *)
471 472
let var a =
  {
473 474 475 476 477 478 479 480
  ints  = VarIntervals.var a;
  atoms = VarAtoms.var a;
  chars = VarChars.var a;
  times = VarTimes.var a;
  xml   = VarXml.var a;
  arrow = VarArrow.var a;
  record= VarRec.var a;
  abstract = VarAbstracts.var a;
481
  absent = false;
482 483
}

484 485 486
let char c = VarChars.inj (VarChars.atom (`Atm c))
let interval i = VarIntervals.inj (VarIntervals.atom (`Atm i))
let abstract a = VarAbstracts.inj (VarAbstracts.atom (`Atm a))
487

Pietro Abate's avatar
Pietro Abate committed
488
let cup x y =
489
  if x == y then x else
490
    {
491
      ints  = VarIntervals.cup x.ints y.ints;
492 493 494 495 496 497 498
      atoms = VarAtoms.cup x.atoms y.atoms;
      chars = VarChars.cup x.chars y.chars;
      times = VarTimes.cup x.times y.times;
      xml   = VarXml.cup x.xml y.xml;
      arrow = VarArrow.cup x.arrow y.arrow;
      record= VarRec.cup x.record y.record;
      abstract = VarAbstracts.cup x.abstract y.abstract;
499 500
      absent = x.absent || y.absent;
    }
501

Pietro Abate's avatar
Pietro Abate committed
502
let cap x y =
503
  if x == y then x else
504
    {
505 506 507 508 509 510 511 512
      atoms = VarAtoms.cap x.atoms y.atoms;
      ints  = VarIntervals.cap x.ints y.ints;
      chars = VarChars.cap x.chars y.chars;
      times = VarTimes.cap x.times y.times;
      xml   = VarXml.cap x.xml y.xml;
      arrow = VarArrow.cap x.arrow y.arrow;
      record = VarRec.cap x.record y.record;
      abstract = VarAbstracts.cap x.abstract y.abstract;
513
      absent= x.absent && y.absent;
514
    }
515

Pietro Abate's avatar
Pietro Abate committed
516
let diff x y =
517
  if x == y then empty else
518
    {
519 520 521 522 523 524 525 526
      atoms = VarAtoms.diff x.atoms y.atoms;
      ints  = VarIntervals.diff x.ints y.ints;
      chars = VarChars.diff x.chars y.chars;
      times = VarTimes.diff x.times y.times;
      xml   = VarXml.diff x.xml y.xml;
      arrow = VarArrow.diff x.arrow y.arrow;
      record= VarRec.diff x.record y.record;
      abstract = VarAbstracts.diff x.abstract y.abstract;
527
      absent= x.absent && not y.absent;
528
    }
Pietro Abate's avatar
Pietro Abate committed
529

530 531
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
532 533 534 535 536 537 538 539
  (VarChars.trivially_disjoint a.chars b.chars) &&
  (VarIntervals.trivially_disjoint a.ints b.ints) &&
  (VarAtoms.trivially_disjoint a.atoms b.atoms) &&
  (VarTimes.trivially_disjoint a.times b.times) &&
  (VarXml.trivially_disjoint a.xml b.xml) &&
  (VarArrow.trivially_disjoint a.arrow b.arrow) &&
  (VarRec.trivially_disjoint a.record b.record) &&
  (VarAbstracts.trivially_disjoint a.abstract b.abstract) &&
540
  (not (a.absent && b.absent))
541

542
let rec constant = function
543 544 545
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
546
  | Pair (x,y) -> times (const_node x) (const_node y)
547
  | Xml (x,y) -> xml (const_node x) (const_node y)
548
  | Record x -> record_fields (false ,LabelMap.map const_node x)
549 550
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
Pietro Abate's avatar
Pietro Abate committed
551
      else
552 553 554
	let (ch,i') = U.next s i in
	constant (Pair (Char (Chars.V.mk_int ch), String (i',j,s,c)))
and const_node c = cons (constant c)
555

556 557
let neg x = diff any x

558
let any_node = cons any
559
let empty_node = cons empty
560

561
module LabelS = Set.Make(Label)
562

Pietro Abate's avatar
Pietro Abate committed
563
let any_or_absent = { any with absent = true }
564
let only_absent = { empty with absent = true }
565

566
let get_record r =
Pietro Abate's avatar
Pietro Abate committed
567 568
  let labs accu (_,r) =
    List.fold_left
569
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
570
  let extend descrs labs (o,r) =
571 572 573 574 575
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
Pietro Abate's avatar
Pietro Abate committed
576
	      | (l2,x)::r when l1 == l2 ->
577 578 579
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
Pietro Abate's avatar
Pietro Abate committed
580
		  if not o then
581
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
582 583
		  aux (i+1) labs r
    in
584
    aux 0 labs (LabelMap.get r);
585 586 587
    o
  in
  let line (p,n) =
Pietro Abate's avatar
Pietro Abate committed
588
    let labels =
589 590
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
591
    let nlab = List.length labels in
592
    let mk () = Array.create nlab any_or_absent in
593 594

    let pos = mk () in
Pietro Abate's avatar
Pietro Abate committed
595 596
    let opos = List.fold_left
		 (fun accu x ->
597 598 599 600 601 602 603 604 605 606 607
		    (extend pos labels x) && accu)
		 true p in
    let p = (opos, pos) in

    let n = List.map (fun x ->
			let neg = mk () in
			let o = extend neg labels x in
			(o,neg)
		     ) n in
    (labels,p,n)
  in
608
  List.map line (Rec.get r)
609

610 611 612 613 614
(* Subtyping algorithm *)

let diff_t d t = diff d (descr t)
let cap_t d t = cap d (descr t)
let cup_t d t = cup d (descr t)
615
let cap_product any_left any_right l =
Pietro Abate's avatar
Pietro Abate committed
616
  List.fold_left
617
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
618
    (any_left,any_right)
619
    l
620
let any_pair = { empty with times = any.times }
621

622 623 624
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

625
exception NotEmpty
626

627 628 629 630 631 632 633 634 635
module Witness = struct

  module NodeSet = Set.Make(Node)

  type witness =
    | WInt of Intervals.V.t
    | WAtom of Atoms.sample
    | WChar of Chars.V.t
    | WAbsent
636
    | WAbstract of Abstracts.elem option
637 638 639 640 641 642 643

    | WPair of witness * witness * witness_slot
    | WXml of witness * witness * witness_slot
    | WRecord of witness label_map * bool * witness_slot
	(* Invariant: WAbsent cannot actually appear *)

    | WFun of (witness * witness option) list * witness_slot
Pietro Abate's avatar
Pietro Abate committed
644
  and witness_slot =
645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
      { mutable wnodes_in: NodeSet.t;
	mutable wnodes_out: NodeSet.t;
	mutable wuid: int }

  module WHash = Hashtbl.Make(
    struct
      type t = witness
      let hash_small = function
	| WInt i -> 17 * Intervals.V.hash i
	| WChar c -> 1 + 17 * Chars.V.hash c
	| WAtom None -> 2
	| WAtom (Some (ns,None)) -> 3 + 17 * Ns.Uri.hash ns
	| WAtom (Some (_,Some t)) -> 4 + 17 * Ns.Label.hash t
	| WAbsent -> 5
	| WAbstract None -> 6
660
	| WAbstract (Some t) -> 7 + 17 * Abstracts.T.hash t
Pietro Abate's avatar
Pietro Abate committed
661
	| WPair (_,_,s)
662 663 664 665 666 667
	| WXml (_,_,s)
	| WRecord (_,_,s)
	| WFun (_,s) -> 8 + 17 * s.wuid
      let hash = function
	| WPair (p1,p2,_) -> 257 * hash_small p1 + 65537 * hash_small p2
	| WXml (p1,p2,_) -> 1 + 257 * hash_small p1 + 65537 * hash_small p2
Pietro Abate's avatar
Pietro Abate committed
668
	| WRecord (r,o,_) ->
669 670 671
	    (if o then 2 else 3) + 257 * LabelMap.hash hash_small r
	| WFun (f,_) ->
	    4 + 257 *
Pietro Abate's avatar
Pietro Abate committed
672 673
	      (Hashtbl.hash
		 (List.map
674
		    (function (x,None) -> 17 * hash_small x
Pietro Abate's avatar
Pietro Abate committed
675
		       | (x,Some y) ->
676 677 678 679 680 681 682 683 684 685 686 687 688 689 690
			   1 + 17 * hash_small x + 257 * hash_small y)
		    f)
	      )
	| _ -> assert false

      let equal_small w1 w2 = match w1,w2 with
	| WInt i1, WInt i2 -> Intervals.V.equal i1 i2
	| WChar c1, WChar c2 -> Chars.V.equal c1 c2
	| WAtom None, WAtom None -> true
	| WAtom (Some (ns1,None)), WAtom (Some (ns2,None)) ->
	    Ns.Uri.equal ns1 ns2
	| WAtom (Some (_,Some t1)), WAtom (Some (_,Some t2)) ->
	    Ns.Label.equal t1 t2
	| WAbsent, WAbsent -> true
	| WAbstract None, WAbstract None -> false
691
	| WAbstract (Some t1), WAbstract (Some t2) -> Abstracts.T.equal t1 t2
692 693 694
	| _ -> w1 == w2

      let equal w1 w2 = match w1,w2 with
Pietro Abate's avatar
Pietro Abate committed
695 696
	| WPair (p1,q1,_), WPair (p2,q2,_)
	| WXml (p1,q1,_), WXml (p2,q2,_) ->
697 698 699 700 701 702 703 704
	    equal_small p1 p2 && equal_small q1 q2
	| WRecord (r1,o1,_), WRecord (r2,o2,_) ->
	    o1 == o2 && (LabelMap.equal equal_small r1 r2)
	| WFun (f1,_), WFun (f2,_) ->
	    List.length f1 = List.length f2 &&
		List.for_all2
		(fun (x1,y1) (x2,y2) ->
		   equal_small x1 x2 && (match y1,y2 with
Pietro Abate's avatar
Pietro Abate committed
705
					   | Some y1, Some y2 ->
706 707 708 709 710 711 712 713 714
					       equal_small y1 y2
					   | None, None -> true
					   | _ -> false)
		) f1 f2
	| _ -> false
    end)

  let wmemo = WHash.create 1024
  let wuid = ref 0
Pietro Abate's avatar
Pietro Abate committed
715
  let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty;
716 717
		   wnodes_out = NodeSet.empty }

718 719 720 721
  let () =
    Stats.register Stats.Summary
      (fun ppf -> Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)

722
  let rec pp ppf = function
723 724 725 726 727 728 729 730 731 732
    | WInt i ->
	Format.fprintf ppf "%a" Intervals.V.print i
    | WChar c ->
	Format.fprintf ppf "%a" Chars.V.print c
    | WAtom None ->
	Format.fprintf ppf "`#:#"
    | WAtom (Some (ns,None)) ->
	Format.fprintf ppf "`%a" Ns.InternalPrinter.print_any_ns ns
    | WAtom (Some (_,Some t)) ->
	Format.fprintf ppf "`%a" Ns.Label.print_attr t
Pietro Abate's avatar
Pietro Abate committed
733
    | WPair (w1,w2,_) ->
734
	Format.fprintf ppf "(%a,%a)" pp w1 pp w2
Pietro Abate's avatar
Pietro Abate committed
735
    | WXml (w1,w2,_) ->
736
	Format.fprintf ppf "XML(%a,%a)" pp w1 pp w2
737 738 739
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
Pietro Abate's avatar
Pietro Abate committed
740
	  (fun l w -> Format.fprintf ppf " %a=%a"
741
	     Label.print_attr l pp w)
742 743 744 745 746 747
	  ws;
	if o then Format.fprintf ppf " ..";
	Format.fprintf ppf " }"
    | WFun (f,_) ->
	Format.fprintf ppf "FUN{";
	List.iter (fun (x,y) ->
748
		     Format.fprintf ppf " %a->" pp x;
749 750
		     match y with
		       | None -> Format.fprintf ppf "#"
751
		       | Some y -> pp ppf y) f;
752 753 754 755 756 757 758
	Format.fprintf ppf " }"
    | WAbstract None ->
	Format.fprintf ppf "Abstract(..)"
    | WAbstract (Some s) ->
	Format.fprintf ppf "Abstract(%s)" s
    | WAbsent ->
	Format.fprintf ppf "Absent"
Pietro Abate's avatar
Pietro Abate committed
759

760 761
  let printf = pp Format.std_formatter

762 763
  let wmk w =  (* incr wuid; w *)  (* hash-consing disabled *)
    try WHash.find wmemo w
Pietro Abate's avatar
Pietro Abate committed
764 765
    with Not_found ->
      incr wuid;
766
      WHash.add wmemo w w;
Pietro Abate's avatar
Pietro Abate committed
767
(*      Format.fprintf Format.std_formatter "W:%a@."
768
	pp w; *)
769 770 771 772 773 774 775
      w

  let wpair p1 p2 = wmk (WPair (p1,p2, wslot()))
  let wxml p1 p2 = wmk (WXml (p1,p2, wslot()))
  let wrecord r o = wmk (WRecord (r,o, wslot()))
  let wfun f = wmk (WFun (f, wslot()))

776
  let bool_pair f =
Pietro Abate's avatar
Pietro Abate committed
777 778 779
    Pair.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
780 781 782
      ~atom:f

  let bool_rec f =
Pietro Abate's avatar
Pietro Abate committed
783 784 785
    Rec.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
786 787
      ~atom:f