types.ml 134 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

30 31
type service_params =
  | TProd of service_params * service_params
Pietro Abate's avatar
Pietro Abate committed
32
  | TOption of service_params
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
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
45
  | TCoordv of service_params * string
Pietro Abate's avatar
Pietro Abate committed
46
  | TESuffix of string
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
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
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;
  }

150 151 152 153 154 155 156
module type VarType =
  sig
    include Bool.V
    type descr
    val inj : t -> descr
    val proj : descr -> t
  end
157

158 159 160 161 162 163 164 165 166
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 }
167

Pietro Abate's avatar
Pietro Abate committed
168
module rec Descr :
169
sig
170
  include Custom.T with
171 172
	    type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolTimes.t,
		      BoolXml.t, BoolArrow.t, BoolRec.t, BoolAbstracts.t) descr_
173
  val empty: t
174
  val any : t
Julien Lopez's avatar
Julien Lopez committed
175
  val is_empty : t -> bool
176 177
end =
struct
178

179 180
  type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolTimes.t,
	    BoolXml.t, BoolArrow.t, BoolRec.t, BoolAbstracts.t) descr_
181

182
  let dump ppf d =
183 184 185 186 187
    Format.fprintf ppf "@[<v 1>types:@\n\
@<1>    atoms: %a@\n\
@<1>     ints: %a@\n\
@<1>    chars: %a@\n\
@<1>    times: %a@\n\
188
@<1>      xml: %a@\n\
189 190 191 192
@<1>    arrow: %a@\n\
@<1>   record: %a@\n\
@<1> abstract: %a@\n\
@<1>   absent: %b@]@\n"
193
      BoolAtoms.dump d.atoms
194 195
      BoolIntervals.dump d.ints
      BoolChars.dump d.chars
196 197 198
      BoolTimes.dump d.times
      BoolXml.dump d.xml
      BoolArrow.dump d.arrow
199
      BoolRec.dump d.record
200
      BoolAbstracts.dump d.abstract
201
      d.absent
202

203
  let empty = empty_descr_
204

205 206 207 208
  let any =  {
    ints  = BoolIntervals.full;
    atoms = BoolAtoms.full;
    chars = BoolChars.full;
209 210 211 212
    times = BoolTimes.full;
    xml   = BoolXml.full;
    arrow = BoolArrow.full;
    record = BoolRec.full;
213
    abstract = BoolAbstracts.full;
214
    absent = false;
215 216
  }

217 218 219 220
  let check a =
    BoolChars.check a.chars;
    BoolIntervals.check a.ints;
    BoolAtoms.check a.atoms;
221 222 223
    BoolTimes.check a.times;
    BoolXml.check a.xml;
    BoolArrow.check a.arrow;
224
    BoolRec.check a.record;
225
    BoolAbstracts.check a.abstract;
226 227
    ()

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

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

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

265
  let hash a =
266 267 268
    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
269 270 271
    let accu = 17 * accu + BoolTimes.hash a.times in
    let accu = 17 * accu + BoolXml.hash a.xml in
    let accu = 17 * accu + BoolArrow.hash a.arrow in
272
    let accu = 17 * accu + BoolRec.hash a.record in
273
    let accu = 17 * accu + BoolAbstracts.hash a.abstract in
274 275
    let accu = if a.absent then accu+5 else accu in
    accu
276

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

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

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



302
end
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
and BoolAtoms : VarType with type Atom.t = Atoms.t
			 and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Atoms)
     type descr = Descr.t
     let inj t = { empty_descr_ with atoms = t }
     let proj t = t.atoms
   end

and BoolIntervals : VarType with type Atom.t = Intervals.t
			     and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Intervals)
     type descr = Descr.t
     let inj t = { empty_descr_ with ints = t }
     let proj t = t.ints
   end

and BoolChars : VarType with type Atom.t = Chars.t
			 and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Chars)
     type descr = Descr.t
     let inj t = { empty_descr_ with chars = t }
     let proj t = t.chars
   end

and BoolAbstracts : VarType with type Atom.t = Abstracts.t
			     and type descr = Descr.t
 =
   struct
     include Bool.MakeVar(Abstracts)
     type descr = Descr.t
     let inj t = { empty_descr_ with abstract = t }
     let proj t = t.abstract
   end
342

343 344
and Pair : Bool.S with type elem = (Node.t * Node.t) =
  Bool.Make(Custom.Pair(Node)(Node))
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371

and BoolTimes : VarType with module Atom = Pair
                              and type descr = Descr.t
=
  struct include Bool.MakeVar(Pair)
  type descr = Descr.t
  let inj (t : t) : descr = { empty_descr_ with times = t }
  let proj (t : descr) : t = t.times
end

and BoolXml : VarType with module Atom = Pair
                       and type descr = Descr.t
=
  struct include Bool.MakeVar(Pair)
  type descr = Descr.t
  let inj (t : t) : descr = { empty_descr_ with xml = t }
  let proj (t : descr) : t = t.xml
end

and BoolArrow : VarType with module Atom = Pair
                       and type descr = Descr.t
=
  struct include Bool.MakeVar(Pair)
  type descr = Descr.t
  let inj (t : t) : descr = { empty_descr_ with arrow = t }
  let proj (t : descr) : t = t.arrow
end
372

373 374 375
(* 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" *)
376

377 378
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
  Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
379

380 381 382 383 384 385 386 387
and BoolRec : VarType with module Atom = Rec
                       and type descr = Descr.t
=
  struct include Bool.MakeVar(Rec)
  type descr = Descr.t
  let inj (t : t) : descr = { empty_descr_ with record = t }
  let proj (t : descr) : t = t.record
end
388

389 390
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
391 392
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
393

394 395 396
type descr = Descr.t
type node = Node.t
include Descr
397

398 399
let dummy_print = (fun _ _ -> assert false)
let forward_print = ref dummy_print
400

Pietro Abate's avatar
Pietro Abate committed
401 402
let make () =
  incr count;
403 404
  Node.mk !count empty

Pietro Abate's avatar
Pietro Abate committed
405
let define n d =
406 407
  n.Node.descr <- d

Pietro Abate's avatar
Pietro Abate committed
408 409
let cons d =
  incr count;
410 411
  Node.mk !count d

412 413 414 415
let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id

416
let non_constructed =
Pietro Abate's avatar
Pietro Abate committed
417
  { any with
418
      times = empty.times; xml = empty.xml; record = empty.record }
Pietro Abate's avatar
Pietro Abate committed
419 420

let non_constructed_or_absent =
421
  { non_constructed with absent = true }
422

Pietro Abate's avatar
Pietro Abate committed
423
(* Descr.t type constructors *)
424 425 426
let times x y = { empty with times = BoolTimes.atom (`Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolXml.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolArrow.atom (`Atm (Pair.atom (x,y))) }
427

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

431
let record_fields x =
432
  { empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
433

434
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
435 436

(* Atm = Any ^ a *)
437 438 439 440 441
let var a =
  {
  ints  = BoolIntervals.var a;
  atoms = BoolAtoms.var a;
  chars = BoolChars.var a;
442 443 444 445
  times = BoolTimes.var a;
  xml   = BoolXml.var a;
  arrow = BoolArrow.var a;
  record= BoolRec.var a;
446
  abstract = BoolAbstracts.var a;
447
  absent = false;
448 449
}

450 451
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
452
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) }
453

Pietro Abate's avatar
Pietro Abate committed
454
let cup x y =
455
  if x == y then x else
456
    {
457 458 459
      ints  = BoolIntervals.cup x.ints  y.ints;
      atoms = BoolAtoms.cup x.atoms y.atoms;
      chars = BoolChars.cup x.chars y.chars;
460 461 462 463
      times = BoolTimes.cup x.times y.times;
      xml   = BoolXml.cup x.xml y.xml;
      arrow = BoolArrow.cup x.arrow y.arrow;
      record= BoolRec.cup x.record y.record;
464
      abstract = BoolAbstracts.cup x.abstract y.abstract;
465 466
      absent = x.absent || y.absent;
    }
467

Pietro Abate's avatar
Pietro Abate committed
468
let cap x y =
469
  if x == y then x else
470
    {
471
      atoms = BoolAtoms.cap x.atoms y.atoms;
472
      ints  = BoolIntervals.cap x.ints y.ints;
473
      chars = BoolChars.cap x.chars y.chars;
474 475 476 477
      times = BoolTimes.cap x.times y.times;
      xml   = BoolXml.cap x.xml y.xml;
      arrow = BoolArrow.cap x.arrow y.arrow;
      record = BoolRec.cap x.record y.record;
478
      abstract = BoolAbstracts.cap x.abstract y.abstract;
479
      absent= x.absent && y.absent;
480
    }
481

Pietro Abate's avatar
Pietro Abate committed
482
let diff x y =
483
  if x == y then empty else
484
    {
485
      atoms = BoolAtoms.diff x.atoms y.atoms;
486
      ints  = BoolIntervals.diff x.ints y.ints;
487
      chars = BoolChars.diff x.chars y.chars;
488 489 490 491
      times = BoolTimes.diff x.times y.times;
      xml   = BoolXml.diff x.xml y.xml;
      arrow = BoolArrow.diff x.arrow y.arrow;
      record= BoolRec.diff x.record y.record;
492
      abstract = BoolAbstracts.diff x.abstract y.abstract;
493
      absent= x.absent && not y.absent;
494
    }
Pietro Abate's avatar
Pietro Abate committed
495

496 497
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
498 499 500
  (BoolChars.trivially_disjoint a.chars b.chars) &&
  (BoolIntervals.trivially_disjoint a.ints b.ints) &&
  (BoolAtoms.trivially_disjoint a.atoms b.atoms) &&
501 502 503
  (BoolTimes.trivially_disjoint a.times b.times) &&
  (BoolXml.trivially_disjoint a.xml b.xml) &&
  (BoolArrow.trivially_disjoint a.arrow b.arrow) &&
504
  (BoolRec.trivially_disjoint a.record b.record) &&
505
  (BoolAbstracts.trivially_disjoint a.abstract b.abstract) &&
506
  (not (a.absent && b.absent))
507

508
let rec constant = function
509 510 511
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
512
  | Pair (x,y) -> times (const_node x) (const_node y)
513
  | Xml (x,y) -> xml (const_node x) (const_node y)
514
  | Record x -> record_fields (false ,LabelMap.map const_node x)
515 516
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
Pietro Abate's avatar
Pietro Abate committed
517
      else
518 519 520
	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)
521

522 523
let neg x = diff any x

524
let any_node = cons any
525
let empty_node = cons empty
526

527
module LabelS = Set.Make(Label)
528

Pietro Abate's avatar
Pietro Abate committed
529
let any_or_absent = { any with absent = true }
530
let only_absent = { empty with absent = true }
531

532
let get_record r =
Pietro Abate's avatar
Pietro Abate committed
533 534
  let labs accu (_,r) =
    List.fold_left
535
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
536
  let extend descrs labs (o,r) =
537 538 539 540 541
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
Pietro Abate's avatar
Pietro Abate committed
542
	      | (l2,x)::r when l1 == l2 ->
543 544 545
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
Pietro Abate's avatar
Pietro Abate committed
546
		  if not o then
547
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
548 549
		  aux (i+1) labs r
    in
550
    aux 0 labs (LabelMap.get r);
551 552 553
    o
  in
  let line (p,n) =
Pietro Abate's avatar
Pietro Abate committed
554
    let labels =
555 556
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
557
    let nlab = List.length labels in
558
    let mk () = Array.create nlab any_or_absent in
559 560

    let pos = mk () in
Pietro Abate's avatar
Pietro Abate committed
561 562
    let opos = List.fold_left
		 (fun accu x ->
563 564 565 566 567 568 569 570 571 572 573
		    (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
574
  List.map line (Rec.get r)
575

576 577 578 579 580
(* 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)
581
let cap_product any_left any_right l =
Pietro Abate's avatar
Pietro Abate committed
582
  List.fold_left
583
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
584
    (any_left,any_right)
585
    l
586
let any_pair = { empty with times = any.times }
587

588 589 590
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

591
exception NotEmpty
592

593 594 595 596 597 598 599 600 601
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
602
    | WAbstract of Abstracts.elem option
603 604 605 606 607 608 609

    | 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
610
  and witness_slot =
611 612 613 614 615 616 617 618 619 620 621 622 623 624 625
      { 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
626
	| WAbstract (Some t) -> 7 + 17 * Abstracts.T.hash t
Pietro Abate's avatar
Pietro Abate committed
627
	| WPair (_,_,s)
628 629 630 631 632 633
	| 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
634
	| WRecord (r,o,_) ->
635 636 637
	    (if o then 2 else 3) + 257 * LabelMap.hash hash_small r
	| WFun (f,_) ->
	    4 + 257 *
Pietro Abate's avatar
Pietro Abate committed
638 639
	      (Hashtbl.hash
		 (List.map
640
		    (function (x,None) -> 17 * hash_small x
Pietro Abate's avatar
Pietro Abate committed
641
		       | (x,Some y) ->
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656
			   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
657
	| WAbstract (Some t1), WAbstract (Some t2) -> Abstracts.T.equal t1 t2
658 659 660
	| _ -> w1 == w2

      let equal w1 w2 = match w1,w2 with
Pietro Abate's avatar
Pietro Abate committed
661 662
	| WPair (p1,q1,_), WPair (p2,q2,_)
	| WXml (p1,q1,_), WXml (p2,q2,_) ->
663 664 665 666 667 668 669 670
	    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
671
					   | Some y1, Some y2 ->
672 673 674 675 676 677 678 679 680
					       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
681
  let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty;
682 683
		   wnodes_out = NodeSet.empty }

684 685 686 687
  let () =
    Stats.register Stats.Summary
      (fun ppf -> Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)

688
  let rec pp ppf = function
689 690 691 692 693 694 695 696 697 698
    | 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
699
    | WPair (w1,w2,_) ->
700
	Format.fprintf ppf "(%a,%a)" pp w1 pp w2
Pietro Abate's avatar
Pietro Abate committed
701
    | WXml (w1,w2,_) ->
702
	Format.fprintf ppf "XML(%a,%a)" pp w1 pp w2
703 704 705
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
Pietro Abate's avatar
Pietro Abate committed
706
	  (fun l w -> Format.fprintf ppf " %a=%a"
707
	     Label.print_attr l pp w)
708 709 710 711 712 713
	  ws;
	if o then Format.fprintf ppf " ..";
	Format.fprintf ppf " }"
    | WFun (f,_) ->
	Format.fprintf ppf "FUN{";
	List.iter (fun (x,y) ->
714
		     Format.fprintf ppf " %a->" pp x;
715 716
		     match y with
		       | None -> Format.fprintf ppf "#"
717
		       | Some y -> pp ppf y) f;
718 719 720 721 722 723 724
	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
725

726 727
  let printf = pp Format.std_formatter

728 729
  let wmk w =  (* incr wuid; w *)  (* hash-consing disabled *)
    try WHash.find wmemo w
Pietro Abate's avatar
Pietro Abate committed
730 731
    with Not_found ->
      incr wuid;
732
      WHash.add wmemo w w;
Pietro Abate's avatar
Pietro Abate committed
733
(*      Format.fprintf Format.std_formatter "W:%a@."
734
	pp w; *)
735 736 737 738 739 740 741
      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()))

742
  let bool_pair f =
Pietro Abate's avatar
Pietro Abate committed
743 744 745
    Pair.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
746 747 748
      ~atom:f

  let bool_rec f =
Pietro Abate's avatar
Pietro Abate committed
749 750 751
    Rec.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
752 753
      ~atom:f

754
  let rec node_has n = function
755 756 757 758 759 760 761 762 763
    | 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

764 765
  (* type_has checks if a witness is contained in the union of
   * the leafs of a bdd, ignoring all variables. *)
766
  and type_has t = function
767 768 769
    | 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
770 771 772
    | WPair (w1,w2,_) ->
	bool_pair
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
773
	  (BoolTimes.leafconj t.times)
774
    | WXml (w1,w2,_) ->
Pietro Abate's avatar
Pietro Abate committed
775
	bool_pair
776
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
777
	  (BoolXml.leafconj t.xml)
778
    | WFun (f,_) ->
Pietro Abate's avatar
Pietro Abate committed
779
	bool_pair
780 781 782 783 784 785
	  (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
786
	       f)
787
	  (BoolArrow.leafconj t.arrow)
788
    | WRecord (f,o,_) ->
Pietro Abate's avatar
Pietro Abate committed
789
	bool_rec
790 791 792
	  (fun (o',f') ->
	     ((not o) || o') && (
	       let checked = ref 0 in
Pietro Abate's avatar
Pietro Abate committed
793 794
	       try
		 LabelMap.iteri
795
		   (fun l n ->
Pietro Abate's avatar
Pietro Abate committed
796
		      let w =
797 798 799
			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
800
		   ) f';
801 802 803 804 805
		 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))
806
	  (BoolRec.leafconj t.record)
807
    | WAbsent -> t.absent
808
    | WAbstract a -> Abstracts.contains_sample a (BoolAbstracts.leafconj t.abstract)
809 810
end

Pietro Abate's avatar
Pietro Abate committed
811
type slot = { mutable status : status;
812 813
	       mutable notify : notify;
	       mutable active : bool }
814 815
and status = Empty | NEmpty of Witness.witness | Maybe
and notify = Nothing | Do of slot * (Witness.witness -> unit) * notify
816 817

let slot_empty = { status = Empty; active = false; notify = Nothing }
818 819
let slot_nempty w = { status = NEmpty w;
		     active = false; notify = Nothing }
820

821
let rec notify w = function
822
  | Nothing -> ()
Pietro Abate's avatar
Pietro Abate committed
823
  | Do (n,f,rem) ->
824 825
      if n.status == Maybe then (try f w with NotEmpty -> ());
      notify w rem
826 827 828 829 830

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

831 832 833
let set s w =
  s.status <- NEmpty w;
  notify w s.notify;
Pietro Abate's avatar
Pietro Abate committed
834
  s.notify <- Nothing;
835 836
  raise NotEmpty

837
let rec big_conj f l n w =
838
  match l with
839 840
    | [] -> set n w
    | [arg] -> f w arg n
841
    | arg::rem ->
Pietro Abate's avatar
Pietro Abate committed
842 843
	let s =
	  { status = Maybe; active = false;
844
	    notify = Do (n,(big_conj f rem n), Nothing) } in
Pietro Abate's avatar
Pietro Abate committed
845
	try
846
	  f w arg s;
847
	  if s.active then n.active <- true
848
	with NotEmpty when n.status == Empty || n.status == Maybe -> ()
849

850
let memo = DescrHash.create 8191
Pietro Abate's avatar
Pietro Abate committed
851
let marks = ref []
852

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

855 856
let complex = ref 0

857
let rec slot d =
858
  incr complex;
Pietro Abate's avatar
Pietro Abate committed
859
  Stats.Counter.incr count_subtype;
860
  (* XXX here I call leafconj a zilliontime. REWRITE !!! *)
861
  if d.absent then slot_nempty Witness.WAbsent
Pietro Abate's avatar
Pietro Abate committed
862
  else if not (Intervals.is_empty (BoolIntervals.leafconj d.ints))
863
  then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.leafconj d.ints)))
Pietro Abate's avatar
Pietro Abate committed
864
  else if not (Atoms.is_empty (BoolAtoms.leafconj d.atoms))
865
  then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.leafconj d.atoms)))
Pietro Abate's avatar
Pietro Abate committed
866
  else if not (Chars.is_empty (BoolChars.leafconj d.chars))
867
  then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
868 869
  else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
  then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
870 871
  else try
         DescrHash.find memo d
872 873 874 875
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
876 877 878
       iter_s s check_times (Pair.get (BoolTimes.leafconj d.times));
       iter_s s check_xml (Pair.get (BoolXml.leafconj d.xml));
       iter_s s check_arrow (Pair.get (BoolArrow.leafconj d.arrow));
879
       iter_s s check_record (get_record (BoolRec.leafconj d.record));
880
       if s.active then marks := s :: !marks else s.status <- Empty;
881
     with NotEmpty -> ());
882 883
    s

884 885 886 887 888
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

889
and check_times (left,right) s =
890 891 892 893
  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
894
    | (n1,n2) :: rest
895 896
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
Pietro Abate's avatar
Pietro Abate committed
897
	let accu2' = diff accu2 (descr n2) in
898 899 900
	guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
	let accu1' = diff accu1 (descr n1) in
	guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
901
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
902
  in
903 904
  let (t1,t2) = cap_product any any left in
  guard s t1 (fun w1 -> guard s t2 (fun w2 -> aux w1 w2 t1 t2 [] right))
905 906

and check_xml (left,right) s =
907 908 909 910
  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.wxml w1 w2)
Pietro Abate's avatar
Pietro Abate committed
911
    | (n1,n2) :: rest
912 913
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
Pietro Abate's avatar
Pietro Abate committed
914
	let accu2' = diff accu2 (descr n2) in
915 916 917
	guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
	let accu1' = diff accu1 (descr n1) in
	guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
918
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
919
  in
920 921
  let (t1,t2) = cap_product any any_pair left in
  guard s t1 (fun w1 -> guard s t2 (fun w2 -> aux w1 w2 t1 t2 [] right))
922

923
and check_arrow (left,right) s =
924 925
  let single_right f (s1,s2) s =
    let rec aux w1 w2 accu1 accu2 left = match left with
926
      | (t1,t2)::left ->
Pietro Abate's avatar
Pietro Abate committed
927
          let accu1' = diff_t accu1 t1 in
928
          guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
929

Pietro Abate's avatar
Pietro Abate committed
930
          let accu2' = cap_t  accu2 t2 in
931
          guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
Pietro Abate's avatar
Pietro Abate committed
932
      | [] ->
933 934
	  let f = match f with Witness.WFun (f,_) -> f | _ -> assert false in
	  set s (Witness.wfun ((w1,w2)::f))
935 936
    in
    let accu1 = descr s1 in
937
    guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
938
  in
939
  big_conj single_right right s (Witness.wfun [])
940

941
and check_record (labels,(oleft,left),rights) s =
942 943
  let rec aux ws accus seen = function
    | [] ->
944 945
	let rec aux w i = function
	  | [] -> assert (i == Array.length ws); w
Pietro Abate's avatar
Pietro Abate committed
946 947
	  | l::labs ->
	      let w = match ws.(i) with
948
              | Witness.WAbsent -> w
Pietro Abate's avatar
Pietro Abate committed
949
              | wl -> LabelMap.add l wl w
950 951 952
            in
	      aux w (succ i) labs
      in
953 954
	set s (Witness.wrecord (aux LabelMap.empty 0 labels) oleft)
    | (false,_) :: rest when oleft -> aux ws accus seen rest
Pietro Abate's avatar
Pietro Abate committed
955
    | (_,f) :: rest
956 957 958 959 960 961
	when not (exists (Array.length left)
		    (fun i -> not (Witness.type_has f.(i) ws.(i)))) ->
	(* TODO: a version f get_record which keeps nodes in neg records. *)
	let right = seen @ rest in
	for i = 0 to Array.length left - 1 do
	  let di = diff accus.(i) f.(i) in
Pietro Abate's avatar
Pietro Abate committed
962
	  guard s di (fun wi ->
963 964 965 966 967
			let accus' = Array.copy accus in accus'.(i) <- di;
			let ws' = Array.copy ws in ws'.(i) <- wi;
			aux ws' accus' [] right);
	done
    | k :: rest -> aux ws accus (k::seen) rest
968
  in
969
  let rec start wl i =
970
    if (i < 0) then aux (Array.of_list wl) left [] rights
971
    else guard s left.(i) (fun w -> start (w::wl) (i - 1))
972
  in
973
  start [] (Array.length left - 1)
974

975
let timer_subtype = Stats.Timer.create "Types.is_empty"
976

977
let is_empty d =
978
  Stats.Timer.start timer_subtype;
979
  let s = slot d in
Pietro Abate's avatar
Pietro Abate committed
980 981 982
  List.iter
    (fun s' ->
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing)
983 984
    !marks;
  marks := [];
985
  Stats.Timer.stop timer_subtype
986
    (s.status == Empty)
987

988 989 990 991
let getwit t = match (slot t).status with NEmpty w -> w | _ -> assert false
  (* Assumes that is_empty has been called on t before. *)

let witness t = if is_empty t then raise Not_found else getwit t
992

993
let non_empty d = not (is_empty d)
994

995 996 997
let disjoint d1 d2 = is_empty (cap d1 d2)

let subtype d1 d2 = is_empty (diff d1 d2)
998

999 1000
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

1001

1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014
(* perform some semantic simplifications around type constructors *)
let atom a =
  let atm =
  if Atoms.(is_empty (diff full a)) then
    BoolAtoms.full
  else BoolAtoms.atom (`Atm a)
  in
  { empty with atoms = atm }

let times x y =
  if subtype any x.Node.descr
    && subtype any y.Node.descr
  then
1015
    { empty with times = BoolTimes.full }
1016 1017 1018 1019 1020 1021
  else times x y

let xml x y =
  if subtype any x.Node.descr
    && subtype any y.Node.descr
  then
1022
    { empty with xml = BoolXml.full }
1023 1024
  else xml x y

1025 1026 1027 1028 1029 1030 1031 1032
module Cache = struct

  type 'a cache =
    | Empty
    | Type of t * 'a
    | Split of Witness.witness * 'a cache * 'a cache

  let rec find f t = function
Pietro Abate's avatar
Pietro Abate committed
1033
    | Empty ->
1034 1035
	let r = f t in Type (t,r), r
    | Split (w,yes,no) ->
Pietro Abate's avatar
Pietro Abate committed
1036
	if Witness.type_has t w
1037 1038 1039
	then let yes,r = find f t yes in Split (w,yes,no), r
	else let no,r = find f t no in Split (w,yes,no), r
    | Type (s,rs) as c ->
Pietro Abate's avatar
Pietro Abate committed
1040 1041 1042
	let f1 ()=
	  let w = witness (diff t s) in
	  let rt = f t in
1043 1044
	  Split (w, Type (t,rt), c), rt
	and f2 () =
Pietro Abate's avatar
Pietro Abate committed
1045
	  let w = witness (diff s t) in
1046 1047 1048 1049 1050 1051 1052 1053
	  let rt = f t in
	  Split (w, c, Type (t,rt)), rt in

	if Random.int 2 = 0 then
	  try f1 () with Not_found -> try f2 () with Not_found -> c, rs
	else
	  try f2 () with Not_found -> try f1 () with Not_found -> c, rs

1054 1055 1056 1057 1058
  let rec lookup t = function
    | Empty -> None
    | Split (w,yes,no) -> lookup t (if Witness.type_has t w then yes else no)
    | Type (s,rs) -> if equiv s t then Some rs else None

1059 1060 1061 1062 1063 1064 1065
  let emp = Empty


  let rec dump_cache f ppf = function
    | Empty -> Format.fprintf ppf "Empty"
    | Type (_,s) -> Format.fprintf ppf "*%a" f s
    | Split (w,c1,c2) -> Format.fprintf ppf "?(%a,%a)"
1066
	(*Witness.pp w *)(dump_cache f) c1 (dump_cache f) c2
Pietro Abate's avatar