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

4 5
let (@@) f a = f a

6
let count = ref 0
Pietro Abate's avatar
Pietro Abate committed
7

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

Pietro Abate's avatar
Pietro Abate committed
12
(*
13 14 15 16 17 18 19 20
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
21
type const =
22
  | Integer of Intervals.V.t
23
  | Atom of Atoms.V.t
24
  | Char of Chars.V.t
25 26 27 28
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
29

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

54 55 56
module Const = struct
  type t = const

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

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

68
    | Char x, Char y -> Chars.V.compare x y
69 70 71
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
72 73
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
74 75 76
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
77 78
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
79 80 81
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
82
	LabelMap.compare compare x y
83 84 85
    | Record _, _ -> -1
    | _, Record _ -> 1
    | String (i1,j1,s1,r1), String (i2,j2,s2,r2) ->
Pietro Abate's avatar
Pietro Abate committed
86
	let c = Pervasives.compare i1 i2 in if c <> 0 then c
87 88 89
	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 *)
90 91 92 93 94 95 96 97 98 99
	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
100
      (* Note: improve hash for String *)
101

102 103
  let equal c1 c2 = compare c1 c2 = 0
end
104

105 106 107
module Abstracts
  =
struct
108
  module T = Custom.String
109

110
  module V = struct type t = T.t * Obj.t end
111 112

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

118
  let full = any
119 120

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

128 129 130 131
  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
132

133 134
end

135 136
type pair_kind = [ `Normal | `XML ]

137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
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;
  }



152 153 154 155
module BoolAtoms = Bool.MakeVar(Atoms)
module BoolIntervals = Bool.MakeVar(Intervals)
module BoolChars = Bool.MakeVar(Chars)
module BoolAbstracts = Bool.MakeVar(Abstracts)
156

Pietro Abate's avatar
Pietro Abate committed
157
module rec Descr :
158
sig
159 160 161
  include Custom.T with
	    type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolPair.t,
		      BoolPair.t, BoolPair.t, BoolRec.t, BoolAbstracts.t) descr_
162
  val empty: t
Julien Lopez's avatar
Julien Lopez committed
163
  val any : t
Julien Lopez's avatar
Julien Lopez committed
164
  val is_empty : t -> bool
165 166
end =
struct
167 168 169

  type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolPair.t,
	    BoolPair.t, BoolPair.t, BoolRec.t, BoolAbstracts.t) descr_
170

171
  let dump ppf d =
172 173 174 175 176 177 178 179 180 181
    Format.fprintf ppf "@[<v 1>types:@\n\
@<1>    atoms: %a@\n\
@<1>     ints: %a@\n\
@<1>    chars: %a@\n\
@<1>    times: %a@\n\
@<1>    arrow: %a@\n\
@<1>   record: %a@\n\
@<1>      xml: %a@\n\
@<1> abstract: %a@\n\
@<1>   absent: %b@]@\n"
182
      BoolAtoms.dump d.atoms
183 184
      BoolIntervals.dump d.ints
      BoolChars.dump d.chars
185
      BoolPair.dump d.times
186
      BoolPair.dump d.arrow
187 188
      BoolRec.dump d.record
      BoolPair.dump d.xml
189
      BoolAbstracts.dump d.abstract
190
      d.absent
191

Pietro Abate's avatar
Pietro Abate committed
192 193 194 195
  let empty = {
    times = BoolPair.empty;
    xml   = BoolPair.empty;
    arrow = BoolPair.empty;
196
    record= BoolRec.empty;
197 198 199
    ints  = BoolIntervals.empty;
    atoms = BoolAtoms.empty;
    chars = BoolChars.empty;
200
    abstract = BoolAbstracts.empty;
201
    absent = false;
202 203
  }

Julien Lopez's avatar
Julien Lopez committed
204 205 206 207
  let any =  {
    times = BoolPair.full;
    xml   = BoolPair.full;
    arrow = BoolPair.full;
208
    record = BoolRec.full;
Julien Lopez's avatar
Julien Lopez committed
209 210 211
    ints  = BoolIntervals.full;
    atoms = BoolAtoms.full;
    chars = BoolChars.full;
212
    abstract = BoolAbstracts.full;
213
    absent = false;
Julien Lopez's avatar
Julien Lopez committed
214 215
  }

216 217 218 219 220 221 222 223
  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;
224
    BoolAbstracts.check a.abstract;
225 226
    ()

227
  let equal a b =
228
    (a == b) || (
229 230 231
      (BoolAtoms.equal a.atoms b.atoms) &&
      (BoolChars.equal a.chars b.chars) &&
      (BoolIntervals.equal a.ints  b.ints) &&
232 233 234 235
      (BoolPair.equal a.times b.times) &&
      (BoolPair.equal a.xml b.xml) &&
      (BoolPair.equal a.arrow b.arrow) &&
      (BoolRec.equal a.record b.record) &&
236
      (BoolAbstracts.equal a.abstract b.abstract) &&
237 238
      (a.absent == b.absent)
    )
239

Julien Lopez's avatar
Julien Lopez committed
240 241 242 243 244 245 246 247
  let is_empty a =
    (BoolAtoms.is_empty a.atoms) &&
      (BoolChars.is_empty a.chars) &&
      (BoolIntervals.is_empty a.ints) &&
      (BoolPair.is_empty a.times) &&
      (BoolPair.is_empty a.xml) &&
      (BoolPair.is_empty a.arrow) &&
      (BoolRec.is_empty a.record) &&
248
      (BoolAbstracts.is_empty a.abstract)
Julien Lopez's avatar
Julien Lopez committed
249

250
  let compare a b =
Pietro Abate's avatar
Pietro Abate committed
251
    if a == b then 0
252 253 254
    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
255 256 257 258
    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
259
    else let c = BoolAbstracts.compare a.abstract b.abstract in if c <> 0 then c
260 261 262
    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
263

264
  let hash a =
265 266 267
    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
268 269 270 271
    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
272
    let accu = 17 * accu + BoolAbstracts.hash a.abstract in
273 274
    let accu = if a.absent then accu+5 else accu in
    accu
275

276 277 278
end
and Node :
sig
279
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
280 281 282 283 284
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
285
  val mk: int -> Descr.t -> t
286
end =
287

288
struct
289
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
290
  let check n = ()
291
  let dump ppf n = Format.fprintf ppf "X%i" n.id
292
  let hash x = x.id + Compunit.hash x.cu
Pietro Abate's avatar
Pietro Abate committed
293
  let compare x y =
294 295
    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))
296

297
  let mk id d = { id = id; cu = Compunit.current (); descr = d }
298 299 300



301 302
end

303 304
and Pair : Bool.S with type elem = (Node.t * Node.t) =
  Bool.Make(Custom.Pair(Node)(Node))
305
and BoolPair : Bool.V with module Atom = Pair = Bool.MakeVar(Pair)
306

307 308 309
(* 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" *)
310

311 312
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
  Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
313 314

and BoolRec : Bool.V with module Atom = Rec = Bool.MakeVar(Rec)
315

316 317
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
318 319
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
320

321 322 323
type descr = Descr.t
type node = Node.t
include Descr
324

325 326
let dummy_print = (fun _ _ -> assert false)
let forward_print = ref dummy_print
327

Pietro Abate's avatar
Pietro Abate committed
328 329
let make () =
  incr count;
330 331
  Node.mk !count empty

Pietro Abate's avatar
Pietro Abate committed
332
let define n d =
333 334
  n.Node.descr <- d

Pietro Abate's avatar
Pietro Abate committed
335 336
let cons d =
  incr count;
337 338
  Node.mk !count d

339 340 341 342
let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id

343
let non_constructed =
Pietro Abate's avatar
Pietro Abate committed
344
  { any with
345
      times = empty.times; xml = empty.xml; record = empty.record }
Pietro Abate's avatar
Pietro Abate committed
346 347

let non_constructed_or_absent =
348
  { non_constructed with absent = true }
349

Pietro Abate's avatar
Pietro Abate committed
350
(* Descr.t type constructors *)
351 352 353
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))) }
354

Pietro Abate's avatar
Pietro Abate committed
355
let record label t =
356
  { empty with record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }
357

358
let record_fields x =
359
  { empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
360

361
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
362 363

(* Atm = Any ^ a *)
364 365 366 367 368 369 370 371 372 373
let var a =
  {
  times = BoolPair.var a;
  xml   = BoolPair.var a;
  arrow = BoolPair.var a;
  record= BoolRec.var a;
  ints  = BoolIntervals.var a;
  atoms = BoolAtoms.var a;
  chars = BoolChars.var a;
  abstract = BoolAbstracts.var a;
374
  absent = false;
375 376
}

377 378
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
379
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) }
380

Pietro Abate's avatar
Pietro Abate committed
381
let cup x y =
382
  if x == y then x else
383
    {
384 385 386 387 388 389 390
      times = BoolPair.cup x.times y.times;
      xml   = BoolPair.cup x.xml y.xml;
      arrow = BoolPair.cup x.arrow y.arrow;
      record= BoolRec.cup x.record y.record;
      ints  = BoolIntervals.cup x.ints  y.ints;
      atoms = BoolAtoms.cup x.atoms y.atoms;
      chars = BoolChars.cup x.chars y.chars;
391
      abstract = BoolAbstracts.cup x.abstract y.abstract;
392 393
      absent = x.absent || y.absent;
    }
394

Pietro Abate's avatar
Pietro Abate committed
395
let cap x y =
396
  if x == y then x else
397
    {
398 399 400
      ints  = BoolIntervals.cap x.ints y.ints;
      times = BoolPair.cap x.times y.times;
      xml   = BoolPair.cap x.xml y.xml;
401
      record = BoolRec.cap x.record y.record;
402 403 404
      arrow = BoolPair.cap x.arrow y.arrow;
      atoms = BoolAtoms.cap x.atoms y.atoms;
      chars = BoolChars.cap x.chars y.chars;
405
      abstract = BoolAbstracts.cap x.abstract y.abstract;
406
      absent= x.absent && y.absent;
407
    }
408

Pietro Abate's avatar
Pietro Abate committed
409
let diff x y =
410
  if x == y then empty else
411
    {
412 413 414 415 416 417 418
      times = BoolPair.diff x.times y.times;
      xml   = BoolPair.diff x.xml y.xml;
      arrow = BoolPair.diff x.arrow y.arrow;
      record= BoolRec.diff x.record y.record;
      ints  = BoolIntervals.diff x.ints y.ints;
      atoms = BoolAtoms.diff x.atoms y.atoms;
      chars = BoolChars.diff x.chars y.chars;
419
      abstract = BoolAbstracts.diff x.abstract y.abstract;
420
      absent= x.absent && not y.absent;
421
    }
Pietro Abate's avatar
Pietro Abate committed
422

423 424
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
425 426 427
  (BoolChars.trivially_disjoint a.chars b.chars) &&
  (BoolIntervals.trivially_disjoint a.ints b.ints) &&
  (BoolAtoms.trivially_disjoint a.atoms b.atoms) &&
428 429 430
  (BoolPair.trivially_disjoint a.times b.times) &&
  (BoolPair.trivially_disjoint a.xml b.xml) &&
  (BoolPair.trivially_disjoint a.arrow b.arrow) &&
431
  (BoolRec.trivially_disjoint a.record b.record) &&
432
  (BoolAbstracts.trivially_disjoint a.abstract b.abstract) &&
433
  (not (a.absent && b.absent))
434

435
let rec constant = function
436 437 438
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
439
  | Pair (x,y) -> times (const_node x) (const_node y)
440
  | Xml (x,y) -> xml (const_node x) (const_node y)
441
  | Record x -> record_fields (false ,LabelMap.map const_node x)
442 443
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
Pietro Abate's avatar
Pietro Abate committed
444
      else
445 446 447
	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)
448

449 450
let neg x = diff any x

451
let any_node = cons any
452
let empty_node = cons empty
453

454
module LabelS = Set.Make(Label)
455

Pietro Abate's avatar
Pietro Abate committed
456
let any_or_absent = { any with absent = true }
457
let only_absent = { empty with absent = true }
458

459
let get_record r =
Pietro Abate's avatar
Pietro Abate committed
460 461
  let labs accu (_,r) =
    List.fold_left
462
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
463
  let extend descrs labs (o,r) =
464 465 466 467 468
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
Pietro Abate's avatar
Pietro Abate committed
469
	      | (l2,x)::r when l1 == l2 ->
470 471 472
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
Pietro Abate's avatar
Pietro Abate committed
473
		  if not o then
474
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
475 476
		  aux (i+1) labs r
    in
477
    aux 0 labs (LabelMap.get r);
478 479 480
    o
  in
  let line (p,n) =
Pietro Abate's avatar
Pietro Abate committed
481
    let labels =
482 483
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
484
    let nlab = List.length labels in
485
    let mk () = Array.create nlab any_or_absent in
486 487

    let pos = mk () in
Pietro Abate's avatar
Pietro Abate committed
488 489
    let opos = List.fold_left
		 (fun accu x ->
490 491 492 493 494 495 496 497 498 499 500
		    (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
501
  List.map line (Rec.get r)
502

503 504 505 506 507
(* 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)
508
let cap_product any_left any_right l =
Pietro Abate's avatar
Pietro Abate committed
509
  List.fold_left
510
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
511
    (any_left,any_right)
512
    l
513
let any_pair = { empty with times = any.times }
514

515 516 517
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

518
exception NotEmpty
519

520 521 522 523 524 525 526 527 528
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
529
    | WAbstract of Abstracts.elem option
530 531 532 533 534 535 536

    | 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
537
  and witness_slot =
538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
      { 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
553
	| WAbstract (Some t) -> 7 + 17 * Abstracts.T.hash t
Pietro Abate's avatar
Pietro Abate committed
554
	| WPair (_,_,s)
555 556 557 558 559 560
	| 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
561
	| WRecord (r,o,_) ->
562 563 564
	    (if o then 2 else 3) + 257 * LabelMap.hash hash_small r
	| WFun (f,_) ->
	    4 + 257 *
Pietro Abate's avatar
Pietro Abate committed
565 566
	      (Hashtbl.hash
		 (List.map
567
		    (function (x,None) -> 17 * hash_small x
Pietro Abate's avatar
Pietro Abate committed
568
		       | (x,Some y) ->
569 570 571 572 573 574 575 576 577 578 579 580 581 582 583
			   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
584
	| WAbstract (Some t1), WAbstract (Some t2) -> Abstracts.T.equal t1 t2
585 586 587
	| _ -> w1 == w2

      let equal w1 w2 = match w1,w2 with
Pietro Abate's avatar
Pietro Abate committed
588 589
	| WPair (p1,q1,_), WPair (p2,q2,_)
	| WXml (p1,q1,_), WXml (p2,q2,_) ->
590 591 592 593 594 595 596 597
	    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
598
					   | Some y1, Some y2 ->
599 600 601 602 603 604 605 606 607
					       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
608
  let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty;
609 610
		   wnodes_out = NodeSet.empty }

611 612 613 614
  let () =
    Stats.register Stats.Summary
      (fun ppf -> Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)

615
  let rec pp ppf = function
616 617 618 619 620 621 622 623 624 625
    | 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
626
    | WPair (w1,w2,_) ->
627
	Format.fprintf ppf "(%a,%a)" pp w1 pp w2
Pietro Abate's avatar
Pietro Abate committed
628
    | WXml (w1,w2,_) ->
629
	Format.fprintf ppf "XML(%a,%a)" pp w1 pp w2
630 631 632
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
Pietro Abate's avatar
Pietro Abate committed
633
	  (fun l w -> Format.fprintf ppf " %a=%a"
634
	     Label.print_attr l pp w)
635 636 637 638 639 640
	  ws;
	if o then Format.fprintf ppf " ..";
	Format.fprintf ppf " }"
    | WFun (f,_) ->
	Format.fprintf ppf "FUN{";
	List.iter (fun (x,y) ->
641
		     Format.fprintf ppf " %a->" pp x;
642 643
		     match y with
		       | None -> Format.fprintf ppf "#"
644
		       | Some y -> pp ppf y) f;
645 646 647 648 649 650 651
	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
652

653 654
  let printf = pp Format.std_formatter

655 656
  let wmk w =  (* incr wuid; w *)  (* hash-consing disabled *)
    try WHash.find wmemo w
Pietro Abate's avatar
Pietro Abate committed
657 658
    with Not_found ->
      incr wuid;
659
      WHash.add wmemo w w;
Pietro Abate's avatar
Pietro Abate committed
660
(*      Format.fprintf Format.std_formatter "W:%a@."
661
	pp w; *)
662 663 664 665 666 667 668
      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()))

669
  let bool_pair f =
Pietro Abate's avatar
Pietro Abate committed
670 671 672
    Pair.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
673 674 675
      ~atom:f

  let bool_rec f =
Pietro Abate's avatar
Pietro Abate committed
676 677 678
    Rec.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
679 680
      ~atom:f

681
  let rec node_has n = function
682 683 684 685 686 687 688 689 690
    | 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

691 692
  (* type_has checks if a witness is contained in the union of
   * the leafs of a bdd, ignoring all variables. *)
693
  and type_has t = function
694 695 696
    | 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
697 698 699
    | WPair (w1,w2,_) ->
	bool_pair
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
700
	  (BoolPair.leafconj t.times)
701
    | WXml (w1,w2,_) ->
Pietro Abate's avatar
Pietro Abate committed
702
	bool_pair
703
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
704
	  (BoolPair.leafconj t.xml)
705
    | WFun (f,_) ->
Pietro Abate's avatar
Pietro Abate committed
706
	bool_pair
707 708 709 710 711 712
	  (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
713
	       f)
714
	  (BoolPair.leafconj t.arrow)
715
    | WRecord (f,o,_) ->
Pietro Abate's avatar
Pietro Abate committed
716
	bool_rec
717 718 719
	  (fun (o',f') ->
	     ((not o) || o') && (
	       let checked = ref 0 in
Pietro Abate's avatar
Pietro Abate committed
720 721
	       try
		 LabelMap.iteri
722
		   (fun l n ->
Pietro Abate's avatar
Pietro Abate committed
723
		      let w =
724 725 726
			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
727
		   ) f';
728 729 730 731 732
		 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))
733
	  (BoolRec.leafconj t.record)
734
    | WAbsent -> t.absent
735
    | WAbstract a -> Abstracts.contains_sample a (BoolAbstracts.leafconj t.abstract)
736 737
end

Pietro Abate's avatar
Pietro Abate committed
738
type slot = { mutable status : status;
739 740
	       mutable notify : notify;
	       mutable active : bool }
741 742
and status = Empty | NEmpty of Witness.witness | Maybe
and notify = Nothing | Do of slot * (Witness.witness -> unit) * notify
743 744

let slot_empty = { status = Empty; active = false; notify = Nothing }
745 746
let slot_nempty w = { status = NEmpty w;
		     active = false; notify = Nothing }
747

748
let rec notify w = function
749
  | Nothing -> ()
Pietro Abate's avatar
Pietro Abate committed
750
  | Do (n,f,rem) ->
751 752
      if n.status == Maybe then (try f w with NotEmpty -> ());
      notify w rem
753 754 755 756 757

let rec iter_s s f = function
  | [] -> ()
  | arg::rem -> f arg s; iter_s s f rem

758 759 760
let set s w =
  s.status <- NEmpty w;
  notify w s.notify;
Pietro Abate's avatar
Pietro Abate committed
761
  s.notify <- Nothing;
762 763
  raise NotEmpty

764
let rec big_conj f l n w =
765
  match l with
766 767
    | [] -> set n w
    | [arg] -> f w arg n
768
    | arg::rem ->
Pietro Abate's avatar
Pietro Abate committed
769 770
	let s =
	  { status = Maybe; active = false;
771
	    notify = Do (n,(big_conj f rem n), Nothing) } in
Pietro Abate's avatar
Pietro Abate committed
772
	try
773
	  f w arg s;
774
	  if s.active then n.active <- true
775
	with NotEmpty when n.status == Empty || n.status == Maybe -> ()
776

777
let memo = DescrHash.create 8191
Pietro Abate's avatar
Pietro Abate committed
778
let marks = ref []
779

Pietro Abate's avatar
Pietro Abate committed
780
let count_subtype = Stats.Counter.create "Subtyping internal loop"
781

782 783
let complex = ref 0

784
let rec slot d =
785
  incr complex;
Pietro Abate's avatar
Pietro Abate committed
786
  Stats.Counter.incr count_subtype;
787
  (* XXX here I call leafconj a zilliontime. REWRITE !!! *)
788
  if d.absent then slot_nempty Witness.WAbsent
Pietro Abate's avatar
Pietro Abate committed
789
  else if not (Intervals.is_empty (BoolIntervals.leafconj d.ints))
790
  then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.leafconj d.ints)))
Pietro Abate's avatar
Pietro Abate committed
791
  else if not (Atoms.is_empty (BoolAtoms.leafconj d.atoms))
792
  then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.leafconj d.atoms)))
Pietro Abate's avatar
Pietro Abate committed
793
  else if not (Chars.is_empty (BoolChars.leafconj d.chars))
794
  then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
795 796
  else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
  then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
797 798
  else try
         DescrHash.find memo d
799 800 801 802
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
803
       iter_s s check_times (Pair.get (BoolPair.leafconj d.times));
Pietro Abate's avatar
Pietro Abate committed
804
       iter_s s check_xml (Pair.get (BoolPair.leafconj d.xml));
805 806
       iter_s s check_arrow (Pair.get (BoolPair.leafconj d.arrow));
       iter_s s check_record (get_record (BoolRec.leafconj d.record));
807
       if s.active then marks := s :: !marks else s.status <- Empty;
808
     with NotEmpty -> ());
809 810
    s

811 812 813 814 815
and guard n t f = match (slot t) with
  | { status = Empty } -> ()
  | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
  | { status = NEmpty v } -> f v

816
and check_times (left,right) s =
817 818 819 820
  let rec aux w1 w2 accu1 accu2 seen = function
    (* Find a product in right which contains (w1,w2) *)
    | [] -> (* no such product: the current witness is in the difference. *)
	set s (Witness.wpair w1 w2)
Pietro Abate's avatar
Pietro Abate committed
821
    | (n1,n2) :: rest