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

4
5
6
7
8
(* TODO:
   - I store hash in types to avoid computing it several times.
     Does not seem to help a lot.
*)

9
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
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
30
module Const = struct
  type t = const

31
32
33
34
35
36
37
38
39
40
41
  let rec check = function
    | Integer i -> Intervals.V.check i
    | Atom i -> Atoms.V.check i
    | Char i -> Chars.V.check i
    | Pair (x,y) | Xml (x,y) -> check x; check y
    | Record l -> LabelMap.iter check l
    | String (i,j,s,q) -> U.check s; check q

  let dump ppf _ =
    Format.fprintf ppf "<Types.Const.t>"

42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
  let rec serialize s = function
    | Integer x ->
	Serialize.Put.bits 3 s 0;
	Intervals.V.serialize s x
    | Atom x ->
	Serialize.Put.bits 3 s 1;
	Atoms.V.serialize s x
    | Char x ->
	Serialize.Put.bits 3 s 2;
	Chars.V.serialize s x
    | Pair (x,y) ->
	Serialize.Put.bits 3 s 3;
	serialize s x;
	serialize s y
    | Xml (x,y) ->
	Serialize.Put.bits 3 s 4;
	serialize s x;
	serialize s y
    | Record r ->
	Serialize.Put.bits 3 s 5;
	LabelMap.serialize serialize s r
    | String (i,j,st,q) ->
	Serialize.Put.bits 3 s 6;
	U.serialize_sub s st i j;
	serialize s q

  let rec deserialize s =
    match Serialize.Get.bits 3 s with
      | 0 ->
	  Integer (Intervals.V.deserialize s)
      | 1 ->
	  Atom (Atoms.V.deserialize s)
74
75
      | 2 ->
	  Char (Chars.V.deserialize s)
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
      | 3 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  Pair (x,y)
      | 4 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  Xml (x,y)
      | 5 ->
	  Record (LabelMap.deserialize deserialize s)
      | 6 ->
	  let st = U.deserialize s in
	  let q = deserialize s in
	  String (U.start_index st, U.end_index st, st, q)
      | _ ->
	  assert false

  let rec compare c1 c2 = match (c1,c2) with
94
    | Integer x, Integer y -> Intervals.V.compare x y
95
96
    | Integer _, _ -> -1
    | _, Integer _ -> 1
97
    | Atom x, Atom y -> Atoms.V.compare x y
98
99
    | Atom _, _ -> -1
    | _, Atom _ -> 1
100
    | Char x, Char y -> Chars.V.compare x y
101
102
103
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
104
105
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
106
107
108
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
109
110
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
111
112
113
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
114
	LabelMap.compare compare x y
115
116
117
118
119
120
121
    | 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 *)
122
123
124
125
126
127
128
129
130
131
	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
132
      (* Note: improve hash for String *)
133

134
135
  let equal c1 c2 = compare c1 c2 = 0
end
136

137
138
type pair_kind = [ `Normal | `XML ]

139
140
141
142
143
144
145
let count = State.ref "Types.count" 0
		
let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)
      

146
147
148
149
150
151
152
153
154
module rec Descr : 
sig
(*
  Want to write:
    type s = { ... }
    include Custom.T with type t = s
  but a  bug in OCaml 3.07+beta 2 makes it impossible
*)
  type t = {
155
    mutable hash: int;
156
157
158
159
160
161
162
163
164
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    absent: bool
  }
165
  val empty: t
166
167
168
169
170
171
172
173
174
175
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
  val serialize: t Serialize.Put.f
  val deserialize: t Serialize.Get.f
end =
struct
  type t = {
176
    mutable hash: int;
177
178
179
180
181
182
183
184
185
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    absent: bool
  }
186

187
188
189
  let dump ppf _ =
    Format.fprintf ppf "<Types.Descr.t>"

190
191
192
193
194
195
196
197
198
199
200
201
  let empty = { 
    hash = 0;
    times = BoolPair.empty; 
    xml   = BoolPair.empty; 
    arrow = BoolPair.empty; 
    record= BoolRec.empty;
    ints  = Intervals.empty;
    atoms = Atoms.empty;
    chars = Chars.empty;
    absent= false;
  }

202
  let equal a b =
203
204
205
206
207
208
209
210
211
212
    (a == b) || (
      (Atoms.equal a.atoms b.atoms) &&
      (Chars.equal a.chars b.chars) &&
      (Intervals.equal a.ints  b.ints) &&
      (BoolPair.equal a.times b.times) &&
      (BoolPair.equal a.xml b.xml) &&
      (BoolPair.equal a.arrow b.arrow) &&
      (BoolRec.equal a.record b.record) &&
      (a.absent == b.absent)
    )
213
214
215
216
217
218
219
220
221
222
223
224
225

  let compare a b =
    if a == b then 0 
    else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
    else let c = Chars.compare a.chars b.chars in if c <> 0 then c
    else let c = Intervals.compare a.ints b.ints in if c <> 0 then c
    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
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
226
      
227
  let hash a =
228
229
230
231
232
233
234
235
236
237
238
239
    if a.hash <> 0 then a.hash else (
      let accu = Chars.hash a.chars in
      let accu = 17 * accu + Intervals.hash a.ints in
      let accu = 17 * accu + Atoms.hash a.atoms in
      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 = if a.absent then accu+5 else accu in
      a.hash <- accu;
      accu
    )
240

241
242
243
244
245
246
247
248
249
250
251
  let check a =
    Chars.check a.chars;
    Intervals.check a.ints;
    Atoms.check a.atoms;
    BoolPair.check a.times;
    BoolPair.check a.xml;
    BoolPair.check a.arrow;
    BoolRec.check a.record;
    ()


252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
  let serialize t a =
    Chars.serialize t a.chars;
    Intervals.serialize t a.ints;
    Atoms.serialize t a.atoms;
    BoolPair.serialize t a.times;
    BoolPair.serialize t a.xml;
    BoolPair.serialize t a.arrow;
    BoolRec.serialize t a.record;
    Serialize.Put.bool t a.absent 

  let deserialize t =
    let chars = Chars.deserialize t in
    let ints = Intervals.deserialize t in
    let atoms = Atoms.deserialize t in
    let times = BoolPair.deserialize t in
    let xml = BoolPair.deserialize t in
    let arrow = BoolPair.deserialize t in
    let record = BoolRec.deserialize t in
    let absent = Serialize.Get.bool t in
271
    let d = { hash=0; 
272
      chars = chars; ints = ints; atoms = atoms; times = times; xml = xml;
273
274
275
      arrow = arrow; record = record; absent = absent } in
    check d;
    d
276
277
   
    
278
279
280
end
and Node :
sig
281

282
283
284
285
286
287
288
289
290
  type t = { id : int; mutable descr : Descr.t }
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
  val serialize: t Serialize.Put.f
  val deserialize: t Serialize.Get.f
end =
291

292
293
struct
  type t = { id : int; mutable descr : Descr.t }
294
295
  let check n = ()
  let dump ppf n = failwith "Types.Node.dump"
296
  let hash x = x.id
297
  let compare x y = x.id - y.id  (* ids are small enough ! *)
298
  let equal x y = x == y
299

300
301
302

  module SMemo = Set.Make(Custom.Int)
  let memo = Serialize.Put.mk_property (fun t -> ref SMemo.empty)
303
304
  let serialize t n = 
    Serialize.Put.int t n.id;
305
    let l = Serialize.Put.get_property memo t in
306
307
308
309
    if not (SMemo.mem n.id !l) then ( 
      l := SMemo.add n.id !l; 
      Descr.serialize t n.descr
    )
310

311
312
  module DMemo = Map.Make(Custom.Int)
  let memo = Serialize.Get.mk_property (fun t -> ref DMemo.empty)
313
  let deserialize t = 
314
    let l = Serialize.Get.get_property memo t in
315
    let id = Serialize.Get.int t in
316
317
318
319
320
321
322
323
    try DMemo.find id !l
    with Not_found ->
      (* TODO: hash-consing ? *)
      incr count; 
      let n = { id = !count; descr = Descr.empty } in
      l := DMemo.add id n !l;
      n.descr <- Descr.deserialize t;
      n
324
325
end

326
(* It is also possible to use Boolean instead of Bool here;
327
   need to analyze when each one is more efficient *)
328
329
330
331
332
333
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
Bool.Make(Custom.Pair(Node)(Node))

and BoolRec : Bool.S with type elem = bool * Node.t label_map =
Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))

334
335
336
337
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
338

339
340
341
type descr = Descr.t
type node = Node.t
include Descr
342
343
344
345
346
347
348
349
350
351
352
353
354
355

let hash_cons = DescrHash.create 17000  

let make () = incr count; { Node.id = !count; Node.descr = empty }
let define n d = 
  DescrHash.add hash_cons d n; 
  n.Node.descr <- d
let cons d = 
  try DescrHash.find hash_cons d 
  with Not_found ->
    incr count; 
    let n = { Node.id = !count; Node.descr = d } in
    DescrHash.add hash_cons d n; n  

356
let any =  {
357
  hash = 0;
358
359
360
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
361
  record= BoolRec.full; 
362
363
364
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
365
  absent= false;
366
}
367
368

let non_constructed =
369
370
371
  { any with  
      hash = 0;
      times = empty.times; xml = empty.xml; record = empty.record }
372
     
373
	     
374
375
376
377
let interval i = { empty with hash = 0; ints = i }
let times x y = { empty with hash = 0; times = BoolPair.atom (x,y) }
let xml x y = { empty with hash = 0; xml = BoolPair.atom (x,y) }
let arrow x y = { empty with hash = 0; arrow = BoolPair.atom (x,y) }
378
let record label t = 
379
380
  { empty with hash = 0; 
      record = BoolRec.atom (true,LabelMap.singleton label t) }
381
let record' (x : bool * node Ident.label_map) =
382
383
384
  { empty with hash = 0; record = BoolRec.atom x }
let atom a = { empty with hash = 0; atoms = a }
let char c = { empty with hash = 0; chars = c }
385
      
386
387
let cup x y = 
  if x == y then x else {
388
    hash = 0;
389
390
391
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
392
    record= BoolRec.cup x.record y.record;
393
394
395
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
396
    absent= x.absent || y.absent;
397
398
399
400
  }
    
let cap x y = 
  if x == y then x else {
401
    hash = 0;
402
403
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
404
    record= BoolRec.cap x.record y.record;
405
    arrow = BoolPair.cap x.arrow y.arrow;
406
407
408
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
409
    absent= x.absent && y.absent;
410
411
412
413
  }
    
let diff x y = 
  if x == y then empty else {
414
    hash = 0;
415
416
417
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
418
    record= BoolRec.diff x.record y.record;
419
420
421
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
422
    absent= x.absent && not y.absent;
423
424
  }
    
425

426

427

428
429
430
431
432
433
434
435
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
  (Chars.disjoint a.chars b.chars) &&
  (Intervals.disjoint a.ints b.ints) &&
  (Atoms.disjoint a.atoms b.atoms) &&
  (BoolPair.trivially_disjoint a.times b.times) &&
  (BoolPair.trivially_disjoint a.xml b.xml) &&
  (BoolPair.trivially_disjoint a.arrow b.arrow) &&
436
437
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
438

439

440

441
let descr n = n.Node.descr
442
let internalize n = n
443
let id n = n.Node.id
444
445


446
447
448
449
450
451
452
453
454
455
456
457
458
let rec constant = function
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
  | Pair (x,y) -> times (const_node x) (const_node y)
  | Xml (x,y) -> times (const_node x) (const_node y)
  | Record x -> record' (false ,LabelMap.map const_node x)
  | 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)
459

460
461
let neg x = diff any x

462
463
let any_node = cons any

464
module LabelS = Set.Make(LabelPool)
465

466
467
468
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

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

    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
511
  List.map line (BoolRec.get r)
512
   
513

514

515
516
517
518
519
520
521


(* 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)
522
let cap_product any_left any_right l =
523
524
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
525
    (any_left,any_right)
526
    l
527
let any_pair = { empty with hash = 0; times = any.times }
528

529

530
531
532
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

533
exception NotEmpty
534

535
536
537
538
539
540
541
542
543
544
545
546
type slot = { mutable status : status; 
	       mutable notify : notify;
	       mutable active : bool }
and status = Empty | NEmpty | Maybe
and notify = Nothing | Do of slot * (slot -> unit) * notify

let slot_empty = { status = Empty; active = false; notify = Nothing }
let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }

let rec notify = function
  | Nothing -> ()
  | Do (n,f,rem) -> 
547
      if n.status == Maybe then (try f n with NotEmpty -> ());
548
549
550
551
552
553
554
555
556
557
      notify rem

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


let set s =
  s.status <- NEmpty;
  notify s.notify;
558
  s.notify <- Nothing; 
559
560
561
562
563
564
565
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
566
567
568
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
569
570
571
	try 
	  f arg s;
	  if s.active then n.active <- true
572
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
573

574
575
let guard a f n =
  match a with
576
    | { status = Empty } -> ()
577
578
579
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
580
    | { status = NEmpty } -> f n
581

582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
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
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679

(* Fast approximation *)

module ClearlyEmpty = 
struct

let memo = DescrHash.create 33000
let marks = ref [] 

let rec slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
       iter_s s check_times (BoolPair.get d.times);  
       iter_s s check_xml (BoolPair.get d.xml); 
       iter_s s check_arrow (BoolPair.get d.arrow);
       iter_s s check_record (get_record d.record);
       if s.active then marks := s :: !marks else s.status <- Empty;
     with
	 NotEmpty -> ());
    s

and check_times (left,right) s =
  let (accu1,accu2) = cap_product any any left in
  let single_right (t1,t2) s =
    let t1 = descr t1 and t2 = descr t2 in
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s 
    else
      let accu1 = diff accu1 t1 in guard (slot accu1) set s;
      let accu2 = diff accu2 t2 in guard (slot accu2) set s in
  guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s

and check_xml (left,right) s =
  let (accu1,accu2) = cap_product any any_pair left in
  let single_right (t1,t2) s =
    let t1 = descr t1 and t2 = descr t2 in
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s 
    else
      let accu1 = diff accu1 t1 in guard (slot accu1) set s;
      let accu2 = diff accu2 t2 in guard (slot accu2) set s in
  guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s

and check_arrow (left,right) s =
  let single_right (s1,s2) s =
    let accu1 = descr s1 and accu2 = neg (descr s2) in
    let single_left (t1,t2) s =
      let accu1 = diff_t accu1 t1 in guard (slot accu1) set s;
      let accu2 = cap_t  accu2 t2 in guard (slot accu2) set s
    in
    guard (slot accu1) (big_conj single_left left) s
  in
  big_conj single_right right s

and check_record (labels,(oleft,left),rights) s =
  let rec single_right (oright,right) s = 
    let next =
      (oleft && (not oright)) ||
      exists (Array.length left)
	(fun i -> trivially_disjoint left.(i) right.(i))
    in
    if next then set s
    else
      for i = 0 to Array.length left - 1 do
	let di = diff left.(i) right.(i) in guard (slot di) set s
      done
  in
  let rec start i s =
    if (i < 0) then big_conj single_right rights s
    else guard (slot left.(i)) (start (i - 1)) s
  in
  start (Array.length left - 1) s


let is_empty d =
  let s = slot d in
  List.iter 
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
    !marks;
  marks := [];
  s.status == Empty
end

let clearly_disjoint t1 t2 =
(*
  if trivially_disjoint t1 t2 then true
  else
    if ClearlyEmpty.is_empty (cap t1 t2) then
      (Printf.eprintf "!\n"; true) else false
*)
  trivially_disjoint t1 t2 || ClearlyEmpty.is_empty (cap t1 t2) 

680
681
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

682
683
684
685
let memo = DescrHash.create 33000
let marks = ref [] 

let rec slot d =
686
687
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
688
689
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
690
691
692
693
694
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
695
       iter_s s check_times (BoolPair.get d.times);  
696
       iter_s s check_xml (BoolPair.get d.xml); 
697
       iter_s s check_arrow (BoolPair.get d.arrow);
698
699
700
701
702
703
704
705
706
       iter_s s check_record (get_record d.record);
       if s.active then marks := s :: !marks else s.status <- Empty;
     with
	 NotEmpty -> ());
    s

and check_times (left,right) s =
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
707
708
709
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
710
711
	     aux accu1 accu2 right s )
	else (
712
          let accu1' = diff accu1 t1 in 
713
	  guard (slot accu1') (aux accu1' accu2 right) s;
714
715

          let accu2' = diff accu2 t2 in 
716
	  guard (slot accu2') (aux accu1 accu2' right) s  
717
	)
718
719
    | [] -> set s
  in
720
  let (accu1,accu2) = cap_product any any left in
721
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
722
723
724
725
726

and check_xml (left,right) s =
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	let t1 = descr t1 and t2 = descr t2 in
727
	if clearly_disjoint accu1 t1 || 
728
729
730
731
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
732
	  guard (slot accu1') (aux accu1' accu2 right) s;
733
734

          let accu2' = diff accu2 t2 in 
735
	  guard (slot accu2') (aux accu1 accu2' right) s  
736
737
738
739
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
740
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
741

742
743
744
745
and check_arrow (left,right) s =
  let single_right (s1,s2) s =
    let rec aux accu1 accu2 left s = match left with
      | (t1,t2)::left ->
746
          let accu1' = diff_t accu1 t1 in 
747
	  guard (slot accu1') (aux accu1' accu2 left) s;
748
749

          let accu2' = cap_t  accu2 t2 in 
750
	  guard (slot accu2') (aux accu1 accu2' left) s
751
752
753
      | [] -> set s
    in
    let accu1 = descr s1 in
754
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
755
756
  in
  big_conj single_right right s
757

758
and check_record (labels,(oleft,left),rights) s =
759
760
  let rec aux rights s = match rights with
    | [] -> set s
761
    | (oright,right)::rights ->
762
	let next =
763
	  (oleft && (not oright)) ||
764
	  exists (Array.length left)
765
	    (fun i -> trivially_disjoint left.(i) right.(i))
766
767
768
769
770
771
	in
	if next then aux rights s
	else
	  for i = 0 to Array.length left - 1 do
	    let back = left.(i) in
	    let di = diff back right.(i) in
772
773
	    guard (slot di) (fun s ->
			left.(i) <- di;
774
775
776
			aux rights s;
			left.(i) <- back;
		     ) s
777
(* TODO: are side effects correct ? *)
778
779
780
781
782
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
783
      guard (slot left.(i)) (start (i - 1)) s
784
785
786
787
  in
  start (Array.length left - 1) s


788
789
let timer_subtype = Stats.Timer.create "Types.is_empty"

790
let is_empty d =
791
  Stats.Timer.start timer_subtype;
792
793
  let s = slot d in
  List.iter 
794
795
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
796
797
    !marks;
  marks := [];
798
799
  Stats.Timer.stop timer_subtype 
    (s.status == Empty)
800

801
(*
802
let is_empty d =
803
804
805
806
807
808
809
(*  let b1 = ClearlyEmpty.is_empty d in
  let b2 = is_empty d in
  assert (b2 || not b1);
  Printf.eprintf "b1 = %b; b2 = %b\n" b1 b2;
  b2  *)
  if ClearlyEmpty.is_empty d then (Printf.eprintf "!\n"; true) else is_empty d
*)  
810
811
812
813
814
815
816
817
818
819
820
821
822

let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
823
824
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
825
826
827
828
829

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

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

830
831
832
833
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

834
835
836
837
838
839
840
    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*) 
841
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
	      
	      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)

866
*)
867
  let get_aux any_right d =
868
869
    let accu = ref [] in
    let line (left,right) =
870
      let (d1,d2) = cap_product any any_right left in
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
      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
886
    List.iter line (BoolPair.get d);
887
    !accu
888
889
890
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
891

892

893
894
  let get ?(kind=`Normal) d = 
    match kind with
895
896
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
897
898
899

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
900
901
902
903
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
904
905

  let restrict_1 rects pi1 =
906
907
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
908
909
910
911
    List.fold_left aux [] rects
  
  type normal = t

912
  module Memo = Map.Make(BoolPair)
913

914
915
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
916
  let memo = ref Memo.empty
917
  let normal_times d = 
918
919
920
    try Memo.find d !memo 
    with
	Not_found ->
921
	  let gd = get_aux any d in
922
	  let n = normal_aux gd in
923
924
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
925
926
	  memo := Memo.add d n !memo;
	  n
927

928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
  let memo_xml = ref Memo.empty
  let normal_xml d = 
    try Memo.find d !memo_xml
    with
	Not_found ->
	  let gd = get_aux any_pair d in
	  let n = normal_aux gd in
	  memo_xml := Memo.add d n !memo_xml;
	  n

  let normal ?(kind=`Normal) d =
    match kind with 
      | `Normal -> normal_times d.times 
      | `XML -> normal_xml d.xml


944
945
946
947
948
949
950
951
952
953
  let merge_same_2 r =
    let r = 
      List.fold_left 
	(fun accu (t1,t2) ->
	   let t = try DescrMap.find t2 accu with Not_found -> empty in
	   DescrMap.add t2 (cup t t1) accu
	) DescrMap.empty r in
    DescrMap.fold (fun t2 t1 accu -> (t1,t2)::accu) r []
	 

954
955
956
957
958
959
960
  let constraint_on_2 n t1 =
    List.fold_left 
      (fun accu (d1,d2) ->
	 if is_empty (cap d1 t1) then accu else cap accu d2)
      any
      n

961
962
  let any = { empty with hash = 0; times = any.times }
  and any_xml = { empty with hash = 0; xml = any.xml }
963
  let is_empty d = d == []
964
end
965

966
module Record = 
967
struct
968
969
  let has_record d = not (is_empty { empty with hash= 0; record = d.record })
  let or_absent d = { d with hash = 0; absent = true }
970
971
972
  let any_or_absent = or_absent any
  let has_absent d = d.absent

973
  let only_absent = {empty with hash = 0; absent = true}
974
975
976
977
978
979
980
981
982
983
984
985
986
  let only_absent_node = cons only_absent

  module T = struct
    type t = descr
    let any = any_or_absent
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module R = struct
    type t = descr
987
    let any = { empty with hash = 0; record = any.record }
988
989
990
991
992
993
994
995
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module TR = Normal.Make(T)(R)

996
  let any_record = { empty with hash = 0; record = BoolRec.full }
997
998
999

  let atom o l = 
    if o && LabelMap.is_empty l then any_record else
1000
    { empty with hash = 0; record = BoolRec.atom (o,l) }
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011

  type zor = Pair of descr * descr | Any

  let aux_split d l=
    let f (o,r) =
      try
	let (lt,rem) = LabelMap.assoc_remove l r in
	Pair (descr lt, atom o rem)
      with Not_found -> 
	if o then
	  if LabelMap.is_empty r then Any else
1012
	    Pair (any_or_absent, { empty with hash=0; record = BoolRec.atom (o,r) })
1013
1014
	else
	  Pair (only_absent,
1015
		{ empty with hash = 0; record = BoolRec.atom (o,r) })
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
    in
    List.fold_left 
      (fun b (p,n) ->
	 let rec aux_p accu = function
	   | x::p -> 
	       (match f x with
		  | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
		  | Any -> aux_p accu p)
	   | [] -> aux_n accu [] n
	 and aux_n p accu = function
	   | x::n -> 
	       (match f x with
		  | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
		  | Any -> b)
	   | [] -> (p,accu) :: b in
	 aux_p [] p)
      []
      (BoolRec.get d.record)

  let split (d : descr) l =
    TR.boolean (aux_split d l)

  let split_normal d l =
    TR.boolean_normal (aux_split d l)


  let project d l =
    let t = TR.pi1 (split d l) in
    if t.absent then raise Not_found;
    t

  let project_opt d l =
    let t = TR.pi1 (split d l) in
1049
    { t with hash = 0; absent = false }
1050
1051
1052

  let condition d l t =
    TR.pi2_restricted t (split d l)
1053

1054
1055
1056
1057
1058
(* TODO: eliminate this cap ... (reord l only_absent_node) when
   not necessary. eg. {| ..... |} \ l *)

  let remove_field d l = 
    cap (TR.pi2 (split d l)) (record l only_absent_node)
1059

1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
  let first_label d =
    let min = ref LabelPool.dummy_max in
    let aux (_,r) = 
      match LabelMap.get r with
	  (l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
    BoolRec.iter aux d.record;
    !min

  let empty_cases d =
    let x = BoolRec.compute
	      ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
	      ~diff:(fun a b -> a land lnot b)
	      ~atom:(function (o,r) ->
		       assert (LabelMap.get r == []);
		       if o then 3 else 1
		    )
	      d.record in
    (x land 2 <> 0, x land 1 <> 0)

  let has_empty_record d =
    BoolRec.compute
      ~empty:false ~full:true ~cup:(||) ~cap:(&&)
      ~diff:(fun a b -> a && not b)
      ~atom:(function (o,r) ->
	       List.for_all 
	         (fun (l,t) -> (descr t).absent)
	         (LabelMap.get r)
	    )
      d.record
    

(*TODO: optimize merge
   - pre-compute the sequence of labels
   - remove empty or full { l = t }
*)

  let merge d1 d2 = 
    let res = ref empty in
    let rec aux accu d1 d2 =
      let l = min (first_label d1) (first_label d2) in
      if l = LabelPool.dummy_max then
	let (some1,none1) = empty_cases d1 
	and (some2,none2) = empty_cases d2 in
	let none = none1 && none2 and some = some1 || some2 in
	let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
	(* approx for the case (some && not none) ... *)
	res := cup !res (record' (some, accu))
      else
	let l1 = split d1 l and l2 = split d2 l in
	let loop (t1,d1) (t2,d2) =
	  let t = 
	    if t2.absent 
1112
	    then cup t1 { t2 with hash = 0; absent = false } 
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
	    else t2 
	  in
	  aux ((l,cons t)::accu) d1 d2
	in
	List.iter (fun x -> List.iter (loop x) l2) l1
	  
    in
    aux [] d1 d2;
    !res

1123
  let any = { empty with hash = 0; record = any.record }
1124
1125
1126
1127
1128
1129
1130
1131
1132

  let get d =
    let rec aux r accu d =
      let l = first_label d in
      if l == LabelPool.dummy_max then
	let (o1,o2) = empty_cases d in 
	if o1 || o2 then (LabelMap.from_list_disj r,o1,o2)::accu else accu
      else
	List.fold_left 
1133
	  (fun accu (t1,t2) -> 
1134
	     let x = (t1.absent, { t1 with hash = 0; absent = false }) in
1135
	     aux ((l,x)::r) accu t2)
1136
1137
1138
1139
1140
1141
1142
1143
1144
	  accu
	  (split d l)
    in
    aux [] [] d
end


module Print = 
struct
1145
  let rec print_const ppf = function
1146
1147
1148
    | Integer i -> Intervals.V.print ppf i
    | Atom a -> Atoms.V.print_quote ppf a
    | Char c -> Chars.V.print ppf c
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
    | Pair (x,y) -> Format.fprintf ppf "(%a,%a)" print_const x print_const y
    | Xml (x,y) -> Format.fprintf ppf "XML(%a,%a)" print_const x print_const y
    | Record r -> 
	Format.fprintf ppf "Record{";
	List.iter 
	  (fun (l,c) -> 
	     Format.fprintf ppf "%a : %a; " 
	     Label.print (LabelPool.value l)
	     print_const c)
	  (LabelMap.get r);
	Format.fprintf ppf "}"
    | String (i,j,s,c) ->
	Format.fprintf ppf "\"%a\" @ %a"
	U.print (U.mk (U.get_substr s i j))
	print_const c
1164

1165
  let nil_atom = Atoms.V.mk_ascii "nil"
1166
1167
1168
1169
1170
1171
1172
1173
1174
  let nil_type = atom (Atoms.atom nil_atom)
  let (seqs_node,seqs_descr) = 
    let n = make () in
    let d = cup nil_type (times any_node n) in
    define n d;
    (n, d)

  let is_regexp t = subtype t seqs_descr

1175
1176
1177
  module S = struct
  type t = { id : int; 
	     mutable def : d list; 
1178
	     mutable state : [ `Expand | `None | `Marked | `Named of U.t ] }
1179
  and  d =
1180
    | Name of U.t
1181
1182
1183
    | Regexp of t Pretty.regexp
    | Atomic of (Format.formatter -> unit)
    | Pair of t * t
1184
    | Char of Chars.V.t
1185
    | Xml of [ `Tag of (Format.formatter -> unit) | `Type of t ] * t * t
1186
1187
    | Record of (bool * t) label_map * bool * bool
    | Arrows of (t * t) list * (t * t) list