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

28 29
type service_params =
  | TProd of service_params * service_params
Pietro Abate's avatar
Pietro Abate committed
30
  | TOption of service_params
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
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
43
  | TCoordv of service_params * string
Pietro Abate's avatar
Pietro Abate committed
44
  | TESuffix of string
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
49 50 51
  | TAny
  | TConst of string;;

52 53 54
module Const = struct
  type t = const

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

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

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

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

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

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

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

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

116
  let full = any
117 118

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

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

131 132
end

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

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

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

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

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

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

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

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

218
  let empty = empty_descr_
219

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

556 557
let neg x = diff any x

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

561
module LabelS = Set.Make(Label)
562

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

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

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

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

610 611 612 613 614
(* Subtyping algorithm *)

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

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

625
exception NotEmpty
626

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

  module NodeSet = Set.Make(Node)

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

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

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

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

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

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

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

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

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

760 761
  let printf = pp Format.std_formatter

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

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

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

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

788
  let rec node_has n = function
789 790 791 792 793 794 795 796 797
    | 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

798 799
  (* type_has checks if a witness is contained in the union of
   * the leafs of a bdd, ignoring all variables. *)
800
  and type_has t = function
801 802 803
    | WInt i -> Intervals.contains i (VarIntervals.leafconj t.ints)
    | WChar c -> Chars.contains c (VarChars.leafconj t.chars)
    | WAtom a -> Atoms.contains_sample a (VarAtoms.leafconj t.atoms)
Pietro Abate's avatar
Pietro Abate committed
804 805 806
    | WPair (w1,w2,_) ->
	bool_pair
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
807
	  (VarTimes.leafconj t.times)
808
    | WXml (w1,w2,_) ->
Pietro Abate's avatar
Pietro Abate committed
809
	bool_pair
810
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
811
	  (VarXml.leafconj t.xml)
812
    | WFun (f,_) ->
Pietro Abate's avatar
Pietro Abate committed
813
	bool_pair
814 815 816 817 818 819
	  (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
820
	       f)
821
	  (VarArrow.leafconj t.arrow)
822
    | WRecord (f,o,_) ->
Pietro Abate's avatar
Pietro Abate committed
823
	bool_rec
824 825 826
	  (fun (o',f') ->
	     ((not o) || o') && (
	       let checked = ref 0 in
Pietro Abate's avatar
Pietro Abate committed
827 828
	       try
		 LabelMap.iteri
829
		   (fun l n ->
Pietro Abate's avatar
Pietro Abate committed
830
		      let w =
831 832 833
			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
834
		   ) f';
835 836 837 838 839
		 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))
840
	  (VarRec.leafconj t.record)
841
    | WAbsent -> t.absent
842
    | WAbstract a -> Abstracts.contains_sample a (VarAbstracts.leafconj t.abstract)
843 844
end

Pietro Abate's avatar
Pietro Abate committed
845
type slot = { mutable status : status;
846 847
	       mutable notify : notify;
	       mutable active : bool }
848 849
and status = Empty | NEmpty of Witness.witness | Maybe
and notify = Nothing | Do of slot * (Witness.witness -> unit) * notify
850 851

let slot_empty = { status = Empty; active = false; notify = Nothing }
852 853
let slot_nempty w = { status = NEmpty w;
		     active = false; notify = Nothing }
854

855
let rec notify w = function
856
  | Nothing -> ()
Pietro Abate's avatar
Pietro Abate committed
857
  | Do (n,f,rem) ->
858 859
      if n.status == Maybe then (try f w with NotEmpty -> ());
      notify w rem
860 861 862 863 864

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

865 866 867
let set s w =
  s.status <- NEmpty w;
  notify w s.notify;
Pietro Abate's avatar
Pietro Abate committed
868
  s.notify <- Nothing;
869 870
  raise NotEmpty

871
let rec big_conj f l n w =
872
  match l with
873 874
    | [] -> set n w
    | [arg] -> f w arg n
875
    | arg::rem ->
Pietro Abate's avatar
Pietro Abate committed
876 877
	let s =
	  { status = Maybe; active = false;
878
	    notify = Do (n,(big_conj f rem n), Nothing) } in
Pietro Abate's avatar
Pietro Abate committed
879
	try
880
	  f w arg s;
881
	  if s.active then n.active <- true
882
	with NotEmpty when n.status == Empty || n.status == Maybe -> ()
883

884
let memo = DescrHash.create 8191
Pietro Abate's avatar
Pietro Abate committed
885
let marks = ref []
886

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

889 890
let complex = ref 0

891
let rec slot d =
892
  incr complex;
Pietro Abate's avatar
Pietro Abate committed
893
  Stats.Counter.incr count_subtype;
894
  (* XXX here I call leafconj a zilliontime. REWRITE !!! *)
895
  if d.absent then slot_nempty Witness.WAbsent
896 897 898 899 900 901 902 903
  else if not (Intervals.is_empty (VarIntervals.leafconj d.ints))
  then slot_nempty (Witness.WInt (Intervals.sample (VarIntervals.leafconj d.ints)))
  else if not (Atoms.is_empty (VarAtoms.leafconj d.atoms))
  then slot_nempty (Witness.WAtom (Atoms.sample (VarAtoms.leafconj d.atoms)))
  else if not (Chars.is_empty (VarChars.leafconj d.chars))
  then slot_nempty (Witness.WChar (Chars.sample (VarChars.leafconj d.chars)))
  else if not (Abstracts.is_empty (VarAbstracts.leafconj d.abstract))
  then slot_nempty (Witness.WAbstract (Abstracts.sample (VarAbstracts.leafconj d.abstract)))
904 905
  else try
         DescrHash.find memo d
906 907 908 909
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
910 911 912 913
       iter_s s check_times (Pair.get (VarTimes.leafconj d.times));
       iter_s s check_xml (Pair.get (VarXml.leafconj d.xml));
       iter_s s check_arrow (Pair.get (VarArrow.leafconj d.arrow));
       iter_s s check_record (get_record (VarRec.leafconj d.record));
914
       if s.active then marks := s :: !marks else s.status <- Empty;
915
     with NotEmpty -> ());
916 917
    s

918 919 920 921 922
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

923
and check_times (left,right) s =
924 925 926 927
  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
928
    | (n1,n2) :: rest
929 930
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
Pietro Abate's avatar
Pietro Abate committed
931
	let accu2' = diff accu2 (descr n2) in
932 933 934
	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)
935
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
936
  in
937 938
  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))
939 940

and check_xml (left,right) s =
941 942 943 944
  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
945
    | (n1,n2) :: rest
946 947
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
Pietro Abate's avatar
Pietro Abate committed
948
	let accu2' = diff accu2 (descr n2) in
949 950 951
	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)
952
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
953
  in
954 955
  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))
956

957
and check_arrow (left,right) s =
958 959
  let single_right f (s1,s2) s =
    let rec aux w1 w2 accu1 accu2 left = match left with
960
      | (t1,t2)::left ->
Pietro Abate's avatar
Pietro Abate committed
961
          let accu1' = diff_t accu1 t1 in
962
          guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
963

Pietro Abate's avatar
Pietro Abate committed
964
          let accu2' = cap_t  accu2 t2 in
965
          guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
Pietro Abate's avatar
Pietro Abate committed
966
      | [] ->
967 968
	  let f = match f with Witness.WFun (f,_) -> f | _ -> assert false in
	  set s (Witness.wfun ((w1,w2)::f))
969 970
    in
    let accu1 = descr s1 in
971
    guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
972
  in
973
  big_conj single_right right s (Witness.wfun [])
974

975
and check_record (labels,(oleft,left),rights) s =
976 977
  let rec aux ws accus seen = function
    | [] ->
978 979
	let rec aux w i = function
	  | [] -> assert (i == Array.length ws); w
Pietro Abate's avatar
Pietro Abate committed
980 981
	  | l::labs ->
	      let w = match ws.(i) with
982
              | Witness.WAbsent -> w
Pietro Abate's avatar
Pietro Abate committed
983
              | wl -> LabelMap.add l wl w
984 985 986
            in
	      aux w (succ i) labs
      in
987 988
	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
989
    | (_,f) :: rest
990 991 992 993 994 995
	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
996
	  guard s di (fun wi ->
997 998 999 1000 1001
			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
1002
  in
1003
  let rec start wl i =
1004
    if (i < 0) then aux (Array.of_list wl) left [] rights
1005
    else guard s left.(i) (fun w -> start (w::wl) (i - 1))
1006
  in
1007
  start [] (Array.length left - 1)
1008

1009
let timer_subtype = Stats.Timer.create "Types.is_empty"
1010

1011
let is_empty d =
1012
  Stats.Timer.start timer_subtype;
1013
  let s = slot d in
Pietro Abate's avatar
Pietro Abate committed
1014 1015 1016
  List.iter
    (fun s' ->
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing)
1017 1018
    !marks;
  marks := [];
1019
  Stats.Timer.stop timer_subtype
1020
    (s.status == Empty)
1021

1022 1023 1024 1025
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
1026

1027
let non_empty d = not (is_empty d)
1028

1029 1030 1031
let disjoint d1 d2 = is_empty (cap d1 d2)

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

1033 1034
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

1035 1036 1037 1038 1039 1040 1041 1042
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
1043
    | Empty ->
1044 1045
	let r = f t in Type (t,r), r
    | Split (w,yes,no) ->
Pietro Abate's avatar
Pietro Abate committed
1046
	if Witness.type_has t w
1047 1048 1049
	then let yes,r =