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

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

Jérôme Maloberti's avatar
Jérôme Maloberti 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

19
20
21
22
23
module Vars = struct
  module V = struct include Custom.String end
  include Bool.Make(V)
end

24
type const = 
25
  | Integer of Intervals.V.t
26
  | Atom of Atoms.V.t
27
  | Var of Vars.V.t
28
  | Char of Chars.V.t
29
30
31
32
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
33

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

58
59
60
module Const = struct
  type t = const

61
62
  let check _ = ()
  let dump ppf _ = Format.fprintf ppf "<Types.Const.t>"
63
64

  let rec compare c1 c2 = match (c1,c2) with
65
    | Integer x, Integer y -> Intervals.V.compare x y
66
67
    | Integer _, _ -> -1
    | _, Integer _ -> 1
68
    | Atom x, Atom y -> Atoms.V.compare x y
69
70
    | Atom _, _ -> -1
    | _, Atom _ -> 1
71
    | Var x, Var y -> Vars.V.compare x y
72
73
74
    | Var _, _ -> -1
    | _, Var _ -> 1

75
    | Char x, Char y -> Chars.V.compare x y
76
77
78
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
79
80
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
81
82
83
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
84
85
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
86
87
88
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
89
	LabelMap.compare compare x y
90
91
92
93
94
95
96
    | Record _, _ -> -1
    | _, Record _ -> 1
    | String (i1,j1,s1,r1), String (i2,j2,s2,r2) ->
	let c = Pervasives.compare i1 i2 in if c <> 0 then c 
	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 *)
97
98
99
100
101
102
103
104
105
106
	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
107
    | Var x -> 7 + 17 * (Vars.V.hash x)
108
      (* Note: improve hash for String *)
109

110
111
  let equal c1 c2 = compare c1 c2 = 0
end
112

113
114
module Abstract =
struct
115
  module T = Custom.String
116
117
118
119
120
121
122
123
124
125
  type abs = T.t

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

  include SortedList.FiniteCofinite(T)

  let print = function
126
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
127
128
129
130
131
    | Cofinite l ->       
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]
132

133
134
135
136
137
  let contains_sample s t = match s,t with
    | None, Cofinite _ -> true
    | None, Finite _ -> false
    | Some s, t -> contains s t
    
138
139
end

140
141
type pair_kind = [ `Normal | `XML ]

142
143
144
145
146
147
148
149
150
151
152
153

module BoolAtoms : BoolVar.S with 
  type bt = Atoms.t and
  type elem = Atoms.t Custom.pairvar = BoolVar.Make(Atoms)
module BoolIntervals : BoolVar.S with 
  type bt = Intervals.t and
  type elem = Intervals.t Custom.pairvar = BoolVar.Make(Intervals)
module BoolChars : BoolVar.S with 
  type bt = Chars.t and
  type elem = Chars.t Custom.pairvar = BoolVar.Make(Chars)
module BoolVars : BoolVar.S with type elem = Vars.t Custom.pairvar = BoolVar.Make(Vars)

154
155
module rec Descr : 
sig
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
  (* each kind is represented as a union of itersection of types 
   * the type is a union of all kinds
   *
   * we add a new field that contains only variables.
   * Inv : 
     * if the bdd of ANY kind is composed only of variables,
       the we move it in vars:
     * From a bdd we move all variables to vars: that belong to
     * to a path in the bdd that contains only variables and end in
     * true
     * A bdd never contains a path that ends in 1 and contains only variables
     *
     * (t1 v a ) ^ ( t2 v b )
     * we need to distribute variables for the intersection
     * (t1 ^ t2) v (t1 ^ b) v (t2 ^ a) v (a ^ b)
     * before we were doing only t1 ^ t2
   *)
173
  type s = {
174
175
176
177
    atoms : BoolAtoms.t;
    vars  : BoolVars.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
178
179
180
181
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
182
    abstract: Abstract.t;
183
184
185
    (* this is used in record to flag the fact that the type of a label is
     * absent . It is used for optional arguments in functions as ?Int
     * is the union of Int ^ undef where undef is a type with absent : true *)
186
187
    absent: bool
  }
188
  include Custom.T with type t = s
189
  val empty: t
190
191
end =
struct
192
  type s = {
193
194
195
196
    atoms : BoolAtoms.t;
    vars  : BoolVars.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
197
198
199
200
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
201
    abstract: Abstract.t;
202
203
    absent: bool
  }
204
  type t = s
205

206
207
208
209
  let print_lst ppf =
    List.iter (fun f -> f ppf; Format.fprintf ppf " |")

  let dump ppf d =
210
211
212
    Format.fprintf ppf "<types atoms(%a) vars(%a) times(%a) record(%a) xml(%a)>"
      BoolAtoms.dump d.atoms
      BoolVars.dump d.vars
213
214
215
      BoolPair.dump d.times
      BoolRec.dump d.record
      BoolPair.dump d.xml
216

217
218
219
220
221
  let empty = { 
    times = BoolPair.empty; 
    xml   = BoolPair.empty; 
    arrow = BoolPair.empty; 
    record= BoolRec.empty;
222
223
224
225
    ints  = BoolIntervals.empty;
    atoms = BoolAtoms.empty;
    vars = BoolVars.empty;
    chars = BoolChars.empty;
226
    abstract = Abstract.empty;
227
228
229
    absent= false;
  }

230
  let equal a b =
231
    (a == b) || (
232
233
234
235
      (BoolAtoms.equal a.atoms b.atoms) &&
      (BoolChars.equal a.chars b.chars) &&
      (BoolIntervals.equal a.ints  b.ints) &&
      (BoolVars.equal a.vars b.vars) &&
236
237
238
239
      (BoolPair.equal a.times b.times) &&
      (BoolPair.equal a.xml b.xml) &&
      (BoolPair.equal a.arrow b.arrow) &&
      (BoolRec.equal a.record b.record) &&
240
      (Abstract.equal a.abstract b.abstract) &&
241
242
      (a.absent == b.absent)
    )
243
244
245

  let compare a b =
    if a == b then 0 
246
247
248
249
    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
    else let c = BoolVars.compare a.vars b.vars in if c <> 0 then c
250
251
252
253
    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
254
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
255
256
257
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
258
      
259
  let hash a =
260
261
262
263
    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
    let accu = 17 * accu + BoolVars.hash a.vars in
264
265
266
267
268
269
270
    let accu = 17 * accu + BoolPair.hash a.times in
    let accu = 17 * accu + BoolPair.hash a.xml in
    let accu = 17 * accu + BoolPair.hash a.arrow in
    let accu = 17 * accu + BoolRec.hash a.record in
    let accu = 17 * accu + Abstract.hash a.abstract in
    let accu = if a.absent then accu+5 else accu in
    accu
271

272
  let check a =
273
274
275
276
    BoolChars.check a.chars;
    BoolIntervals.check a.ints;
    BoolAtoms.check a.atoms;
    BoolVars.check a.vars;
277
278
279
280
    BoolPair.check a.times;
    BoolPair.check a.xml;
    BoolPair.check a.arrow;
    BoolRec.check a.record;
281
    Abstract.check a.abstract;
282
283
    ()

284
285
286
end
and Node :
sig
287
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
288
289
290
291
292
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
293
  val mk: int -> Descr.t -> t
294
end =
295

296
struct
297
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
298
  let check n = ()
299
  let dump ppf n = Format.fprintf ppf "X%i" n.id
300
  let hash x = x.id + Compunit.hash x.cu
301
  let compare x y = 
302
303
304
    let c = x.id - y.id in if c = 0 then Compunit.compare x.cu y.cu else c
  let equal x y = x==y || (x.id == y.id && (Compunit.equal x.cu y.cu))
  let mk id d = { id = id; cu = Compunit.current (); descr = d }
305
306
end

307
308
309
310
and Pair : Bool.S with type elem = (Node.t * Node.t) =
  Bool.Make(Custom.Pair(Node)(Node))
and BoolPair : BoolVar.S with type bt = Pair.t and type elem = Pair.t Custom.pairvar =
  BoolVar.Make(Pair)
311

312
313
314
315
316
317
318
(* bool = true means that the record is open that is, that
 * the labels that are not in the domain of the map are
 * equal to "any" *)
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
  Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
and BoolRec : BoolVar.S with type bt = Rec.t and type elem = Rec.t Custom.pairvar =
  BoolVar.Make(Rec)
319

320
321
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
322
323
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
324

325
326
327
type descr = Descr.t
type node = Node.t
include Descr
328

329
330
let forward_print = ref (fun _ _ -> assert false)

331
332
333
334
let make () = 
  incr count; 
  Node.mk !count empty

335
336
337
338
339
340
341
let define n d = 
  n.Node.descr <- d

let cons d = 
  incr count; 
  Node.mk !count d

342
let any =  {
343
344
345
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
346
  record= BoolRec.full; 
347
348
349
350
  ints  = BoolIntervals.any;
  atoms = BoolAtoms.any;
  vars = BoolVars.any;
  chars = BoolChars.any;
351
  abstract = Abstract.any;
352
  absent= false;
353
}
354
355

let non_constructed =
356
357
  { any with  
      times = empty.times; xml = empty.xml; record = empty.record }
358
     
359
let non_constructed_or_absent = 
360
  { non_constructed with absent = true }
361
	     
362
363
364
let times x y = { empty with times = BoolPair.atom (Custom.Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolPair.atom (Custom.Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolPair.atom (Custom.Atm (Pair.atom (x,y))) }
365
let record label t = 
366
  { empty with 
367
368
369
      record = BoolRec.atom (Custom.Atm (Rec.atom (true,LabelMap.singleton label t))) }
let record_fields x =
  { empty with record = BoolRec.atom (Custom.Atm (Rec.atom x)) }
370
let atom a = { empty with atoms = a }
371
let vars a = { empty with vars = a }
372
let char c = { empty with chars = c }
373
let interval i = { empty with ints = i }
374
let abstract a = { empty with abstract = a }
375
376

let get_abstract t = t.abstract
377
      
378
379
let cup x y = 
  if x == y then x else {
380
381
382
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
383
    record= BoolRec.cup x.record y.record;
384
385
386
387
    ints  = BoolIntervals.cup x.ints  y.ints;
    atoms = BoolAtoms.cup x.atoms y.atoms;
    vars  = BoolVars.cup x.vars y.vars;
    chars = BoolChars.cup x.chars y.chars;
388
    abstract = Abstract.cup x.abstract y.abstract;
389
    absent= x.absent || y.absent;
390
391
392
393
  }
    
let cap x y = 
  if x == y then x else {
394
395
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
396
    record= BoolRec.cap x.record y.record;
397
    arrow = BoolPair.cap x.arrow y.arrow;
398
399
400
401
    ints  = BoolIntervals.cap x.ints  y.ints;
    atoms = BoolAtoms.cap x.atoms y.atoms;
    vars  = BoolVars.cap x.vars y.vars;
    chars = BoolChars.cap x.chars y.chars;
402
    abstract = Abstract.cap x.abstract y.abstract;
403
    absent= x.absent && y.absent;
404
405
406
407
  }
    
let diff x y = 
  if x == y then empty else {
408
409
410
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
411
    record= BoolRec.diff x.record y.record;
412
413
414
415
    ints  = BoolIntervals.diff x.ints  y.ints;
    atoms = BoolAtoms.diff x.atoms y.atoms;
    vars  = BoolVars.diff x.vars y.vars;
    chars = BoolChars.diff x.chars y.chars;
416
    abstract = Abstract.diff x.abstract y.abstract;
417
    absent= x.absent && not y.absent;
418
419
  }
    
420
421
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
422
423
424
425
  (BoolChars.trivially_disjoint a.chars b.chars) &&
  (BoolIntervals.trivially_disjoint a.ints b.ints) &&
  (BoolAtoms.trivially_disjoint a.atoms b.atoms) &&
  (BoolVars.trivially_disjoint a.vars b.vars) &&
426
427
428
  (BoolPair.trivially_disjoint a.times b.times) &&
  (BoolPair.trivially_disjoint a.xml b.xml) &&
  (BoolPair.trivially_disjoint a.arrow b.arrow) &&
429
  (BoolRec.trivially_disjoint a.record b.record) &&
430
  (Abstract.disjoint a.abstract b.abstract) &&
431
  (not (a.absent && b.absent))
432

433
let descr n = n.Node.descr
434
let internalize n = n
435
let id n = n.Node.id
436

437
let rec constant = function
438
439
440
441
  | Integer i -> interval (BoolIntervals.atom (Custom.Atm (Intervals.atom i)))
  | Atom a -> atom (BoolAtoms.atom (Custom.Atm (Atoms.atom a)))
  | Var a -> vars (BoolVars.atom (Custom.Var a))
  | Char c -> char (BoolChars.atom (Custom.Atm (Chars.atom c)))
442
  | Pair (x,y) -> times (const_node x) (const_node y)
443
  | Xml (x,y) -> xml (const_node x) (const_node y)
444
  | Record x -> record_fields (false ,LabelMap.map const_node x)
445
446
447
448
449
450
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
      else 
	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)
451

452
453
let neg x = diff any x

454
let any_node = cons any
455
let empty_node = cons empty
456

457
module LabelS = Set.Make(Label)
458

459
460
let any_or_absent = { any with absent = true } 
let only_absent = { empty with absent = true }
461

462
463
let get_record r =
  let labs accu (_,r) = 
464
465
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
466
  let extend descrs labs (o,r) =
467
468
469
470
471
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
472
	      | (l2,x)::r when l1 == l2 -> 
473
474
475
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
476
477
		  if not o then 
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
478
479
		  aux (i+1) labs r
    in
480
    aux 0 labs (LabelMap.get r);
481
482
483
484
    o
  in
  let line (p,n) =
    let labels = 
485
486
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
487
    let nlab = List.length labels in
488
    let mk () = Array.create nlab any_or_absent in
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503

    let pos = mk () in
    let opos = List.fold_left 
		 (fun accu x -> 
		    (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
504
  List.map line (Rec.get r)
505
   
506
507
508
509
510
(* 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)
511
let cap_product any_left any_right l =
512
513
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
514
    (any_left,any_right)
515
    l
516
let any_pair = { empty with times = any.times }
517

518
519
520
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

521
exception NotEmpty
522

523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
module Witness = struct

  module NodeSet = Set.Make(Node)

  type witness =
    | WInt of Intervals.V.t
    | WAtom of Atoms.sample
    | WChar of Chars.V.t
    | WAbsent
    | WAbstract of Abstract.elem option

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

    | WFun of (witness * witness option) list * witness_slot
  and witness_slot = 
      { mutable wnodes_in: NodeSet.t;
	mutable wnodes_out: NodeSet.t;
	mutable wuid: int }

  module WHash = Hashtbl.Make(
    struct
      type t = witness
      let hash_small = function
	| WInt i -> 17 * Intervals.V.hash i
	| WChar c -> 1 + 17 * Chars.V.hash c
	| WAtom None -> 2
	| WAtom (Some (ns,None)) -> 3 + 17 * Ns.Uri.hash ns
	| WAtom (Some (_,Some t)) -> 4 + 17 * Ns.Label.hash t
	| WAbsent -> 5
	| WAbstract None -> 6
	| WAbstract (Some t) -> 7 + 17 * Abstract.T.hash t
	| WPair (_,_,s) 
	| 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
	| WRecord (r,o,_) -> 
	    (if o then 2 else 3) + 257 * LabelMap.hash hash_small r
	| WFun (f,_) ->
	    4 + 257 *
	      (Hashtbl.hash 
		 (List.map 
		    (function (x,None) -> 17 * hash_small x
		       | (x,Some y) -> 
			   1 + 17 * hash_small x + 257 * hash_small y)
		    f)
	      )
	| _ -> assert false

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

      let equal w1 w2 = match w1,w2 with
	| WPair (p1,q1,_), WPair (p2,q2,_) 
592
	| WXml (p1,q1,_), WXml (p2,q2,_) -> 
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
	    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
					   | Some y1, Some y2 -> 
					       equal_small y1 y2
					   | None, None -> true
					   | _ -> false)
		) f1 f2
	| _ -> false
    end)

  let wmemo = WHash.create 1024
  let wuid = ref 0
  let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty; 
		   wnodes_out = NodeSet.empty }

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

618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
  let rec print_witness ppf = function
    | WInt i ->
	Format.fprintf ppf "%a" Intervals.V.print i
    | WChar c ->
	Format.fprintf ppf "%a" Chars.V.print c
    | WAtom None ->
	Format.fprintf ppf "`#:#"
    | WAtom (Some (ns,None)) ->
	Format.fprintf ppf "`%a" Ns.InternalPrinter.print_any_ns ns
    | WAtom (Some (_,Some t)) ->
	Format.fprintf ppf "`%a" Ns.Label.print_attr t
    | WPair (w1,w2,_) -> 
	Format.fprintf ppf "(%a,%a)" print_witness w1 print_witness w2
    | WXml (w1,w2,_) -> 
	Format.fprintf ppf "XML(%a,%a)" print_witness w1 print_witness w2
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
	  (fun l w -> Format.fprintf ppf " %a=%a" 
	     Label.print_attr l print_witness w)
	  ws;
	if o then Format.fprintf ppf " ..";
	Format.fprintf ppf " }"
    | WFun (f,_) ->
	Format.fprintf ppf "FUN{";
	List.iter (fun (x,y) ->
		     Format.fprintf ppf " %a->" print_witness x;
		     match y with
		       | None -> Format.fprintf ppf "#"
		       | Some y -> print_witness ppf y) f;
	Format.fprintf ppf " }"
    | WAbstract None ->
	Format.fprintf ppf "Abstract(..)"
    | WAbstract (Some s) ->
	Format.fprintf ppf "Abstract(%s)" s
    | WAbsent ->
	Format.fprintf ppf "Absent"
	  
656
657
658
659
660
661
662
663
664
665
666
667
668
669
  let wmk w =  (* incr wuid; w *)  (* hash-consing disabled *)
    try WHash.find wmemo w
    with Not_found -> 
      incr wuid; 
      WHash.add wmemo w w;
(*      Format.fprintf Format.std_formatter "W:%a@." 
	print_witness w; *)
      w

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

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

  let bool_rec f =
677
    Rec.compute 
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
      ~empty:false ~full:true 
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y) 
      ~atom:f

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

  and type_has t = function
693
694
695
    | WInt i -> Intervals.contains i (BoolIntervals.get t.ints)
    | WChar c -> Chars.contains c (BoolChars.get t.chars)
    | WAtom a -> Atoms.contains_sample a (BoolAtoms.get t.atoms)
696
697
698
    | WPair (w1,w2,_) -> 
	bool_pair 
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2) 
699
	  (BoolPair.get t.times)
700
701
702
    | WXml (w1,w2,_) ->
	bool_pair 
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
703
	  (BoolPair.get t.xml)
704
705
706
707
708
709
710
711
712
    | WFun (f,_) ->
	bool_pair 
	  (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))
	       f) 
713
	  (BoolPair.get t.arrow)
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
    | WRecord (f,o,_) ->
	bool_rec 
	  (fun (o',f') ->
	     ((not o) || o') && (
	       let checked = ref 0 in
	       try 
		 LabelMap.iteri 
		   (fun l n ->
		      let w = 
			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
		   ) f'; 
		 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))
732
	  (BoolRec.get t.record)
733
734
735
736
    | WAbsent -> t.absent
    | WAbstract a -> Abstract.contains_sample a t.abstract
end

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

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

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

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

757
758
759
let set s w =
  s.status <- NEmpty w;
  notify w s.notify;
760
  s.notify <- Nothing; 
761
762
  raise NotEmpty

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

776
let memo = DescrHash.create 8191
777
778
let marks = ref [] 

779
780
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

781
782
let complex = ref 0

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

808
809
810
811
812
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

813
and check_times (left,right) s =
814
815
816
817
818
819
820
821
  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)
    | (n1,n2) :: rest 
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
	let accu2' = diff accu2 (descr n2) in 
822
823
824
	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)
825
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
826
  in
827
828
  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))
829
830

and check_xml (left,right) s =
831
832
833
834
835
836
837
838
  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)
    | (n1,n2) :: rest 
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
	let accu2' = diff accu2 (descr n2) in 
839
840
841
	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)
842
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
843
  in
844
845
  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))
846

847
and check_arrow (left,right) s =
848
849
  let single_right f (s1,s2) s =
    let rec aux w1 w2 accu1 accu2 left = match left with
850
      | (t1,t2)::left ->
851
          let accu1' = diff_t accu1 t1 in 
852
	  guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
853
854

          let accu2' = cap_t  accu2 t2 in 
855
	  guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
856
857
858
      | [] -> 
	  let f = match f with Witness.WFun (f,_) -> f | _ -> assert false in
	  set s (Witness.wfun ((w1,w2)::f))
859
860
    in
    let accu1 = descr s1 in
861
    guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
862
  in
863
  big_conj single_right right s (Witness.wfun [])
864

865
and check_record (labels,(oleft,left),rights) s =
866
867
  let rec aux ws accus seen = function
    | [] ->
868
869
	let rec aux w i = function
	  | [] -> assert (i == Array.length ws); w
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
	  | l::labs -> 
	      let w = match ws.(i) with 
		| Witness.WAbsent -> w
		| wl -> LabelMap.add l wl w in
	      aux w (succ i) labs in
	set s (Witness.wrecord (aux LabelMap.empty 0 labels) oleft)
    | (false,_) :: rest when oleft -> aux ws accus seen rest
    | (_,f) :: rest 
	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
	  guard s di (fun wi -> 
			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
890
  in
891
  let rec start wl i =
892
    if (i < 0) then aux (Array.of_list wl) left [] rights
893
    else guard s left.(i) (fun w -> start (w::wl) (i - 1))
894
  in
895
  start [] (Array.length left - 1)
896

897
let timer_subtype = Stats.Timer.create "Types.is_empty"
898

899
let is_empty d =
900
  Stats.Timer.start timer_subtype;
901
902
  let s = slot d in
  List.iter 
903
904
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
905
906
    !marks;
  marks := [];
907
  Stats.Timer.stop timer_subtype
908
    (s.status == Empty)
909

910
911
912
913
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
914

915
916
917
let non_empty d = 
  not (is_empty d)

918
919
920
let disjoint d1 d2 = is_empty (cap d1 d2)

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

922
923
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953

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
    | Empty -> 
	let r = f t in Type (t,r), r
    | Split (w,yes,no) ->
	if Witness.type_has t w 
	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 ->
	let f1 ()= 
	  let w = witness (diff t s) in 
	  let rt = f t in 
	  Split (w, Type (t,rt), c), rt
	and f2 () =
	  let w = witness (diff s t) in 
	  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

954
955
956
957
958
  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

959
960
961
962
963
964
965
966
967
968
969
970
  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)"
	(*Witness.print_witness w *)(dump_cache f) c1 (dump_cache f) c2

  let memo f =
    let c = ref emp in
    fun t ->
971
972
973
       let c',r = find f t !c in
       c := c';
       r
974
975
976

end

977
978
979
980
981
982
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
983
984
      | `Normal -> { d with times = empty.times }
      | `XML -> { d with xml = empty.xml }
985
986
987
988
989

  let is_product ?kind d = is_empty (other ?kind d)

  let need_second = function _::_::_ -> true | _ -> false

990
991
992
993
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

994
995
996
997
998
999
1000
    let res = ref [] in

    let add (t1,t2) =
      let rec loop t1 t2 = function
	| [] -> res := (ref (t1,t2)) :: !res
	| ({contents = (d1,d2)} as r)::l ->
	    (*OPT*) 
1001
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
	      
	      let i = cap t1 d1 in
	      if is_empty i then loop t1 t2 l
	      else (
		r := (i, cup t2 d2);
		let k = diff d1 t1 in 
		if non_empty k then res := (ref (k,d2)) :: !res;
		
		let j = diff t1 d1 in 
		if non_empty j then loop j t2 l
	      )
      in
      loop t1 t2 !res
    in
    List.iter add d;
    List.map (!) !res


(* Partitioning:

(t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
=
(t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)

1026
*)
1027
  let get_aux any_right d =
1028
1029
    let accu = ref [] in
    let line (left,right) =
1030
      let (d1,d2) = cap_product any any_right left in
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
      if (non_empty d1) && (non_empty d2) then
	let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
	let right = normal_aux right in
	let resid1 = ref d1 in
	let () = 
	  List.iter
	    (fun (t1,t2) ->
	       let t1 = cap d1 t1 in
	       if (non_empty t1) then
		 let () = resid1 := diff !resid1 t1 in
		 let t2 = diff d2 t2 in
		 if (non_empty t2) then accu := (t1,t2) :: !accu
	    ) right in
	if non_empty !resid1 then accu := (!resid1, d2) :: !accu 
    in
1046
    List.iter line (Pair.get (BoolPair.get d));
1047
    !accu
1048
1049
1050
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
1051

1052

Pietro Abate's avatar