types.ml 86.2 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
module Abstract =
struct
105
  module T = Custom.String
106 107 108 109 110 111 112 113 114 115
  type abs = T.t

  module V =
  struct
    type t = abs * Obj.t
  end

  include SortedList.FiniteCofinite(T)

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

123 124 125 126
  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
127

128 129
end

130 131
type pair_kind = [ `Normal | `XML ]

Pietro Abate's avatar
Pietro Abate committed
132
module BoolAtoms : BoolVar.S with
133
  type s = Atoms.t = BoolVar.Make(Atoms)
Pietro Abate's avatar
Pietro Abate committed
134
module BoolIntervals : BoolVar.S with
135
  type s = Intervals.t = BoolVar.Make(Intervals)
Pietro Abate's avatar
Pietro Abate committed
136
module BoolChars : BoolVar.S with
137
  type s = Chars.t = BoolVar.Make(Chars)
138

139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172

module TLV = struct

  open Var
  (* s : top level variables
   * f : all free variables in the subtree
   * b : true if the type contains only variables *)
  type t =  { s : Set.t ; f : Set.t ; b : bool }

  let empty = { s = Set.empty ; f = Set.empty ; b = true }
  let singleton v = { s = Set.singleton v; f = Set.singleton v; b = true }

  (* return the max of top level variables *)
  let max x = Set.max_elt x.s

  let pair x y = {
    b = false ; 
    s = Set.empty ; 
    f = Set.union x.f y.f 
  }

  let union x y = {
    b = x.b && y.b;
    s = Set.union x.s y.s ;
    f = Set.union x.f y.f ;
  }

  let inter x y = {
    b = x.b && y.b;
    s = Set.inter x.s y.s ;
    f = Set.inter x.f y.f ;
  }

  let diff x y = {
173
    b = x.b && y.b;
174 175 176 177 178 179 180 181 182
    s = Set.diff x.s y.s; 
    f = Set.diff x.f y.f;
  }

  (* true if it contains only one variable *)
  let is_single x = x.b && (Set.cardinal x.f = 1) && (Set.cardinal x.s = 1)
  let no_variables x = (x.b == false) && (Set.cardinal x.f = 0)

end
183

Pietro Abate's avatar
Pietro Abate committed
184
module rec Descr :
185
sig
Pietro Abate's avatar
Pietro Abate committed
186
  (* each kind is represented as a union of itersection of types
187 188 189
   * the type is a union of all kinds
   *
   * we add a new field that contains only variables.
Pietro Abate's avatar
Pietro Abate committed
190
   * Inv :
191 192 193 194 195 196 197 198 199 200 201 202
     * if the bdd of ANY kind is composed only of variables,
       the we move it in vars:
     * From a bdd we move all variables to vars: that belong to
     * to a path in the bdd that contains only variables and end in
     * true
     * A bdd never contains a path that ends in 1 and contains only variables
     *
     * (t1 v a ) ^ ( t2 v b )
     * we need to distribute variables for the intersection
     * (t1 ^ t2) v (t1 ^ b) v (t2 ^ a) v (a ^ b)
     * before we were doing only t1 ^ t2
   *)
203
  type s = {
204 205 206
    atoms : BoolAtoms.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
207 208 209 210
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
211
    abstract: Abstract.t;
212 213 214
    (* this is used in record to flag the fact that the type of a label is
     * absent . It is used for optional arguments in functions as ?Int
     * is the union of Int ^ undef where undef is a type with absent : true *)
215 216 217
    absent: bool;
    (* maintains the list of all toplevel type variables in s
     * and a flag that is true if s contains only variables, false otherwise *)
218
    toplvars : TLV.t
219
  }
220
  include Custom.T with type t = s
221
  val empty: t
222 223
end =
struct
224
  type s = {
225 226 227
    atoms : BoolAtoms.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
228 229 230 231
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
232
    abstract: Abstract.t;
233
    absent: bool;
234
    toplvars : TLV.t
235
  }
236
  type t = s
237

238 239 240 241
  let print_lst ppf =
    List.iter (fun f -> f ppf; Format.fprintf ppf " |")

  let dump ppf d =
242
    Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>"
243
      BoolAtoms.dump d.atoms
244 245
      BoolIntervals.dump d.ints
      BoolChars.dump d.chars
246
      BoolPair.dump d.times
247
      BoolPair.dump d.arrow
248 249
      BoolRec.dump d.record
      BoolPair.dump d.xml
250 251
      Abstract.dump d.abstract
      d.absent
252

Pietro Abate's avatar
Pietro Abate committed
253 254 255 256
  let empty = {
    times = BoolPair.empty;
    xml   = BoolPair.empty;
    arrow = BoolPair.empty;
257
    record= BoolRec.empty;
258 259 260
    ints  = BoolIntervals.empty;
    atoms = BoolAtoms.empty;
    chars = BoolChars.empty;
261
    abstract = Abstract.empty;
262
    absent= false;
263
    toplvars = TLV.empty
264 265
  }

266 267 268 269 270 271 272 273 274 275 276
  let check a =
    BoolChars.check a.chars;
    BoolIntervals.check a.ints;
    BoolAtoms.check a.atoms;
    BoolPair.check a.times;
    BoolPair.check a.xml;
    BoolPair.check a.arrow;
    BoolRec.check a.record;
    Abstract.check a.abstract;
    ()

277
  let equal a b =
278
    (a == b) || (
279 280 281
      (BoolAtoms.equal a.atoms b.atoms) &&
      (BoolChars.equal a.chars b.chars) &&
      (BoolIntervals.equal a.ints  b.ints) &&
282 283 284 285
      (BoolPair.equal a.times b.times) &&
      (BoolPair.equal a.xml b.xml) &&
      (BoolPair.equal a.arrow b.arrow) &&
      (BoolRec.equal a.record b.record) &&
286
      (Abstract.equal a.abstract b.abstract) &&
287 288
      (a.absent == b.absent)
    )
289 290

  let compare a b =
Pietro Abate's avatar
Pietro Abate committed
291
    if a == b then 0
292 293 294
    else let c = BoolAtoms.compare a.atoms b.atoms in if c <> 0 then c
    else let c = BoolChars.compare a.chars b.chars in if c <> 0 then c
    else let c = BoolIntervals.compare a.ints b.ints in if c <> 0 then c
295 296 297 298
    else let c = BoolPair.compare a.times b.times in if c <> 0 then c
    else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
    else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
    else let c = BoolRec.compare a.record b.record in if c <> 0 then c
299
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
300 301 302
    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
303

304
  let hash a =
305 306 307
    let accu = BoolChars.hash a.chars in
    let accu = 17 * accu + BoolIntervals.hash a.ints in
    let accu = 17 * accu + BoolAtoms.hash a.atoms in
308 309 310 311 312 313 314
    let accu = 17 * accu + BoolPair.hash a.times in
    let accu = 17 * accu + BoolPair.hash a.xml in
    let accu = 17 * accu + BoolPair.hash a.arrow in
    let accu = 17 * accu + BoolRec.hash a.record in
    let accu = 17 * accu + Abstract.hash a.abstract in
    let accu = if a.absent then accu+5 else accu in
    accu
315

316 317 318
end
and Node :
sig
319
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
320 321 322 323 324
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
325
  val mk: int -> Descr.t -> t
326
end =
327

328
struct
329
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
330
  let check n = ()
331
  let dump ppf n = Format.fprintf ppf "X%i" n.id
332
  let hash x = x.id + Compunit.hash x.cu
Pietro Abate's avatar
Pietro Abate committed
333
  let compare x y =
334 335 336
    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))
  let mk id d = { id = id; cu = Compunit.current (); descr = d }
337 338
end

339 340
and Pair : Bool.S with type elem = (Node.t * Node.t) =
  Bool.Make(Custom.Pair(Node)(Node))
Pietro Abate's avatar
Pietro Abate committed
341
and BoolPair : BoolVar.S with
342
  type s = Pair.t = BoolVar.Make(Pair)
343

344 345 346 347 348
(* 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" *)
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
  Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
349 350
and BoolRec : BoolVar.S with
  type s = Rec.t = BoolVar.Make(Rec)
351

352 353
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
354 355
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
356

357 358 359
type descr = Descr.t
type node = Node.t
include Descr
360

361 362
let forward_print = ref (fun _ _ -> assert false)

Pietro Abate's avatar
Pietro Abate committed
363 364
let make () =
  incr count;
365 366
  Node.mk !count empty

Pietro Abate's avatar
Pietro Abate committed
367
let define n d =
368 369
  n.Node.descr <- d

Pietro Abate's avatar
Pietro Abate committed
370 371
let cons d =
  incr count;
372 373
  Node.mk !count d

374 375 376 377
let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id

378 379 380
(* two representation possible. either all fields (except vars) are full, OR
 * the field vars is full.
 *)
381
let any =  {
Pietro Abate's avatar
Pietro Abate committed
382 383 384 385
  times = BoolPair.full;
  xml   = BoolPair.full;
  arrow = BoolPair.full;
  record= BoolRec.full;
386 387 388
  ints  = BoolIntervals.full;
  atoms = BoolAtoms.full;
  chars = BoolChars.full;
389
  abstract = Abstract.any;
390
  absent= false;
391
  toplvars = TLV.empty
392
}
393 394

let non_constructed =
Pietro Abate's avatar
Pietro Abate committed
395
  { any with
396
      times = empty.times; xml = empty.xml; record = empty.record }
Pietro Abate's avatar
Pietro Abate committed
397 398

let non_constructed_or_absent =
399
  { non_constructed with absent = true }
400

Pietro Abate's avatar
Pietro Abate committed
401
(* Descr.t type constructors *)
402 403 404 405 406
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }

(* XXX toplevel variables are not properly set for records *)
Pietro Abate's avatar
Pietro Abate committed
407 408
let record label t =
  { empty with
409
      record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }
410
let record_fields x =
411
  { empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
412

413
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
414
let var a =  {
415
  (* Atm = Any ^ a *)
416
  times = BoolPair.vars a;
Pietro Abate's avatar
Pietro Abate committed
417 418 419
  xml   = BoolPair.vars a;
  arrow = BoolPair.vars a;
  record= BoolRec.vars a;
420 421 422
  ints  = BoolIntervals.vars a;
  atoms = BoolAtoms.vars a;
  chars = BoolChars.vars a;
423
  abstract = Abstract.empty;
424
  absent= false;
425
  toplvars = TLV.singleton a
426 427
}

428
let is_var t = TLV.is_single t.toplvars
429
let no_var t = TLV.no_variables t.toplvars
430

431 432
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
433
let abstract a = { empty with abstract = a }
434 435

let get_abstract t = t.abstract
436

Pietro Abate's avatar
Pietro Abate committed
437
let cup x y =
438
  if x == y then x else {
439 440 441
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
442
    record= BoolRec.cup x.record y.record;
443 444 445
    ints  = BoolIntervals.cup x.ints  y.ints;
    atoms = BoolAtoms.cup x.atoms y.atoms;
    chars = BoolChars.cup x.chars y.chars;
446
    abstract = Abstract.cup x.abstract y.abstract;
447
    absent= x.absent || y.absent;
448
    toplvars = TLV.union x.toplvars y.toplvars
449
  }
450

Pietro Abate's avatar
Pietro Abate committed
451
let cap x y =
452
  if x == y then x else {
453
    ints  = BoolIntervals.cap x.ints y.ints;
454 455
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
456
    record= BoolRec.cap x.record y.record;
457
    arrow = BoolPair.cap x.arrow y.arrow;
458 459
    atoms = BoolAtoms.cap x.atoms y.atoms;
    chars = BoolChars.cap x.chars y.chars;
460
    abstract = Abstract.cap x.abstract y.abstract;
461
    absent= x.absent && y.absent;
462
    toplvars = TLV.inter x.toplvars y.toplvars
463
  }
464

Pietro Abate's avatar
Pietro Abate committed
465
let diff x y =
466
  if x == y then empty else {
467 468 469
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
470
    record= BoolRec.diff x.record y.record;
471
    ints  = BoolIntervals.diff x.ints y.ints;
472 473
    atoms = BoolAtoms.diff x.atoms y.atoms;
    chars = BoolChars.diff x.chars y.chars;
474
    abstract = Abstract.diff x.abstract y.abstract;
475
    absent= x.absent && not y.absent;
476
    toplvars = TLV.diff x.toplvars y.toplvars
477
  }
Pietro Abate's avatar
Pietro Abate committed
478

479 480
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
481 482 483
  (BoolChars.trivially_disjoint a.chars b.chars) &&
  (BoolIntervals.trivially_disjoint a.ints b.ints) &&
  (BoolAtoms.trivially_disjoint a.atoms b.atoms) &&
484 485 486
  (BoolPair.trivially_disjoint a.times b.times) &&
  (BoolPair.trivially_disjoint a.xml b.xml) &&
  (BoolPair.trivially_disjoint a.arrow b.arrow) &&
487
  (BoolRec.trivially_disjoint a.record b.record) &&
488
  (Abstract.disjoint a.abstract b.abstract) &&
489
  (not (a.absent && b.absent))
490

491
let rec constant = function
492 493 494
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
495
  | Pair (x,y) -> times (const_node x) (const_node y)
496
  | Xml (x,y) -> xml (const_node x) (const_node y)
497
  | Record x -> record_fields (false ,LabelMap.map const_node x)
498 499
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
Pietro Abate's avatar
Pietro Abate committed
500
      else
501 502 503
	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)
504

505 506
let neg x = diff any x

507
let any_node = cons any
508
let empty_node = cons empty
509

510
module LabelS = Set.Make(Label)
511

Pietro Abate's avatar
Pietro Abate committed
512
let any_or_absent = { any with absent = true }
513
let only_absent = { empty with absent = true }
514

515
let get_record r =
Pietro Abate's avatar
Pietro Abate committed
516 517
  let labs accu (_,r) =
    List.fold_left
518
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
519
  let extend descrs labs (o,r) =
520 521 522 523 524
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
Pietro Abate's avatar
Pietro Abate committed
525
	      | (l2,x)::r when l1 == l2 ->
526 527 528
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
Pietro Abate's avatar
Pietro Abate committed
529
		  if not o then
530
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
531 532
		  aux (i+1) labs r
    in
533
    aux 0 labs (LabelMap.get r);
534 535 536
    o
  in
  let line (p,n) =
Pietro Abate's avatar
Pietro Abate committed
537
    let labels =
538 539
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
540
    let nlab = List.length labels in
541
    let mk () = Array.create nlab any_or_absent in
542 543

    let pos = mk () in
Pietro Abate's avatar
Pietro Abate committed
544 545
    let opos = List.fold_left
		 (fun accu x ->
546 547 548 549 550 551 552 553 554 555 556
		    (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
557
  List.map line (Rec.get r)
558

559 560 561 562 563
(* 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)
564
let cap_product any_left any_right l =
Pietro Abate's avatar
Pietro Abate committed
565
  List.fold_left
566
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
567
    (any_left,any_right)
568
    l
569
let any_pair = { empty with times = any.times }
570

571 572 573
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

574
exception NotEmpty
575

576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
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
    | WAbstract of Abstract.elem option

    | 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
593
  and witness_slot =
594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609
      { 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
	| WAbstract (Some t) -> 7 + 17 * Abstract.T.hash t
Pietro Abate's avatar
Pietro Abate committed
610
	| WPair (_,_,s)
611 612 613 614 615 616
	| 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
617
	| WRecord (r,o,_) ->
618 619 620
	    (if o then 2 else 3) + 257 * LabelMap.hash hash_small r
	| WFun (f,_) ->
	    4 + 257 *
Pietro Abate's avatar
Pietro Abate committed
621 622
	      (Hashtbl.hash
		 (List.map
623
		    (function (x,None) -> 17 * hash_small x
Pietro Abate's avatar
Pietro Abate committed
624
		       | (x,Some y) ->
625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643
			   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
	| WAbstract (Some t1), WAbstract (Some t2) -> Abstract.T.equal t1 t2
	| _ -> w1 == w2

      let equal w1 w2 = match w1,w2 with
Pietro Abate's avatar
Pietro Abate committed
644 645
	| WPair (p1,q1,_), WPair (p2,q2,_)
	| WXml (p1,q1,_), WXml (p2,q2,_) ->
646 647 648 649 650 651 652 653
	    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
654
					   | Some y1, Some y2 ->
655 656 657 658 659 660 661 662 663
					       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
664
  let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty;
665 666
		   wnodes_out = NodeSet.empty }

667 668 669 670
  let () =
    Stats.register Stats.Summary
      (fun ppf -> Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)

671 672 673 674 675 676 677 678 679 680 681
  let rec print_witness ppf = function
    | 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
682
    | WPair (w1,w2,_) ->
683
	Format.fprintf ppf "(%a,%a)" print_witness w1 print_witness w2
Pietro Abate's avatar
Pietro Abate committed
684
    | WXml (w1,w2,_) ->
685 686 687 688
	Format.fprintf ppf "XML(%a,%a)" print_witness w1 print_witness w2
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
Pietro Abate's avatar
Pietro Abate committed
689
	  (fun l w -> Format.fprintf ppf " %a=%a"
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707
	     Label.print_attr l print_witness w)
	  ws;
	if o then Format.fprintf ppf " ..";
	Format.fprintf ppf " }"
    | WFun (f,_) ->
	Format.fprintf ppf "FUN{";
	List.iter (fun (x,y) ->
		     Format.fprintf ppf " %a->" print_witness x;
		     match y with
		       | None -> Format.fprintf ppf "#"
		       | Some y -> print_witness ppf y) f;
	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
708

709 710
  let wmk w =  (* incr wuid; w *)  (* hash-consing disabled *)
    try WHash.find wmemo w
Pietro Abate's avatar
Pietro Abate committed
711 712
    with Not_found ->
      incr wuid;
713
      WHash.add wmemo w w;
Pietro Abate's avatar
Pietro Abate committed
714
(*      Format.fprintf Format.std_formatter "W:%a@."
715 716 717 718 719 720 721 722
	print_witness w; *)
      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()))

723
  let bool_pair f =
Pietro Abate's avatar
Pietro Abate committed
724 725 726
    Pair.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
727 728 729
      ~atom:f

  let bool_rec f =
Pietro Abate's avatar
Pietro Abate committed
730 731 732
    Rec.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
733 734 735 736 737 738 739 740 741 742 743 744
      ~atom:f

  let rec node_has n = function
    | WXml (_,_,s) | WPair (_,_,s) | WFun (_,s) | WRecord (_,_,s) as w ->
	if NodeSet.mem n s.wnodes_in then true
	else if NodeSet.mem n s.wnodes_out then false
	else (let r = type_has (descr n) w in
	      if r then s.wnodes_in <- NodeSet.add n s.wnodes_in
	      else s.wnodes_out <- NodeSet.add n s.wnodes_out;
	      r)
    | w -> type_has (descr n) w

745 746
  (* type_has checks if a witness is contained in the union of
   * the leafs of a bdd, ignoring all variables. *)
747
  and type_has t = function
748 749 750
    | WInt i -> Intervals.contains i (BoolIntervals.leafconj t.ints)
    | WChar c -> Chars.contains c (BoolChars.leafconj t.chars)
    | WAtom a -> Atoms.contains_sample a (BoolAtoms.leafconj t.atoms)
Pietro Abate's avatar
Pietro Abate committed
751 752 753
    | WPair (w1,w2,_) ->
	bool_pair
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
754
	  (BoolPair.leafconj t.times)
755
    | WXml (w1,w2,_) ->
Pietro Abate's avatar
Pietro Abate committed
756
	bool_pair
757
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
758
	  (BoolPair.leafconj t.xml)
759
    | WFun (f,_) ->
Pietro Abate's avatar
Pietro Abate committed
760
	bool_pair
761 762 763 764 765 766
	  (fun (n1,n2) ->
	     List.for_all
	       (fun (x,y) ->
		  not (node_has n1 x) ||
		    (match y with None -> false
		       | Some y -> node_has n2 y))
Pietro Abate's avatar
Pietro Abate committed
767
	       f)
768
	  (BoolPair.leafconj t.arrow)
769
    | WRecord (f,o,_) ->
Pietro Abate's avatar
Pietro Abate committed
770
	bool_rec
771 772 773
	  (fun (o',f') ->
	     ((not o) || o') && (
	       let checked = ref 0 in
Pietro Abate's avatar
Pietro Abate committed
774 775
	       try
		 LabelMap.iteri
776
		   (fun l n ->
Pietro Abate's avatar
Pietro Abate committed
777
		      let w =
778 779 780
			try let w = LabelMap.assoc l f in incr checked; w
			with Not_found -> WAbsent in
		      if not (node_has n w) then raise Exit
Pietro Abate's avatar
Pietro Abate committed
781
		   ) f';
782 783 784 785 786
		 o' || (LabelMap.length f == !checked)
		   (* All the remaining fields cannot be WAbsent
		      because of an invariant. Otherwise, we must
		      check that all are WAbsent here. *)
	       with Exit -> false))
787
	  (BoolRec.leafconj t.record)
788 789 790 791
    | WAbsent -> t.absent
    | WAbstract a -> Abstract.contains_sample a t.abstract
end

Pietro Abate's avatar
Pietro Abate committed
792
type slot = { mutable status : status;
793 794
	       mutable notify : notify;
	       mutable active : bool }
795 796
and status = Empty | NEmpty of Witness.witness | Maybe
and notify = Nothing | Do of slot * (Witness.witness -> unit) * notify
797 798

let slot_empty = { status = Empty; active = false; <