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

4
5
6
7
8
9
10
11
12
13
(*
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


14
15
16
17
18
19
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
20
21


22
23
24
25
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
26

27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
let compare_const c1 c2 =
  match (c1,c2) with
    | Integer x, Integer y -> Intervals.vcompare x y
    | Integer _, _ -> -1
    | _, Integer _ -> 1
    | Atom x, Atom y -> Atoms.vcompare x y
    | Atom _, _ -> -1
    | _, Atom _ -> 1
    | Char x, Char y -> Chars.vcompare x y

let hash_const = function
  | Integer x -> Intervals.vhash x
  | Atom x -> Atoms.vhash x
  | Char x -> Chars.vhash x

42
43
let equal_const c1 c2 = compare_const c1 c2 = 0

44
45
type pair_kind = [ `Normal | `XML ]

46
47
48
49
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
50
51
52
  let dump ppf (x,y) =
    Format.fprintf ppf "(%i,%i)" x.id y.id
  let compare (y1,x1) (y2,x2) =
53
54
55
56
57
58
59
    if x1.id < x2.id then -1
    else if x1.id > x2.id then 1
    else y1.id - y2.id
  let equal (x1,y1) (x2,y2) = (x1==x2) && (y1==y2)
  let hash (x,y) = x.id + 17 * y.id
end 

60
61
62
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
63
64
  let dump ppf (o,r) = ()

65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
  let rec compare_rec r1 r2 =
    if r1 == r2 then 0
    else match (r1,r2) with
      | (l1,x1)::r1,(l2,x2)::r2 ->
	  if ((l1:int) < l2) then -1 
	  else if (l1 > l2) then 1 
	  else if x1.id < x2.id then -1
	  else if x1.id > x2.id then 1
	  else compare_rec r1 r2
      | ([],_) -> -1
      | _ -> 1

  let compare (o1,r1) (o2,r2) =
    if o1 && not o2 then -1 
    else if o2 && not o1 then 1
    else compare_rec (LabelMap.get r1) (LabelMap.get r2)

  let rec equal_rec r1 r2 =
    (r1 == r2) ||
    match (r1,r2) with
      | (l1,x1)::r1,(l2,x2)::r2 ->
	  (x1.id == x2.id) && (l1 == l2) && (equal_rec r1 r2)
      | _ -> false

  let equal (o1,r1) (o2,r2) =
    (o1 == o2) && (equal_rec (LabelMap.get r1) (LabelMap.get r2))

  let rec hash_rec accu = function
    | (l,x)::rem -> hash_rec (257 * accu + 17 * l + x.id) rem
    | [] -> accu + 5
      
  let hash (o,r) = hash_rec (if o then 2 else 1) (LabelMap.get r)
end

99
100
(* It is also possible to use Boolean insteand of Bool here;
   need to analyze when each one is more efficient *)
101
102
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
103

104
type descr = {
105
  atoms : Atoms.t;
106
107
  ints  : Intervals.t;
  chars : Chars.t;
108
109
110
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
111
  record: descr BoolRec.t;
112
  absent: bool
113
} and node = descr node0
114

115
	       
116
let empty = { 
117
118
119
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
120
  record= BoolRec.empty;
121
122
123
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
124
  absent= false;
125
126
127
}
	      
let any =  {
128
129
130
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
131
  record= BoolRec.full; 
132
133
134
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
135
  absent= false;
136
}
137
138
139
140

let non_constructed =
  { any with times = empty.times; xml = empty.xml; record = empty.record }
     
141
142
	     
let interval i = { empty with ints = i }
143
144
145
let times x y = { empty with times = BoolPair.atom (x,y) }
let xml x y = { empty with xml = BoolPair.atom (x,y) }
let arrow x y = { empty with arrow = BoolPair.atom (x,y) }
146
let record label t = 
147
148
149
  { empty with record = BoolRec.atom (true,LabelMap.singleton label t) }
let record' (x : bool * node Ident.label_map) =
  { empty with record = BoolRec.atom x }
150
151
152
153
154
155
let atom a = { empty with atoms = a }
let char c = { empty with chars = c }
let constant = function
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
156
      
157
158
let cup x y = 
  if x == y then x else {
159
160
161
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
162
    record= BoolRec.cup x.record y.record;
163
164
165
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
166
    absent= x.absent || y.absent;
167
168
169
170
  }
    
let cap x y = 
  if x == y then x else {
171
172
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
173
    record= BoolRec.cap x.record y.record;
174
    arrow = BoolPair.cap x.arrow y.arrow;
175
176
177
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
178
    absent= x.absent && y.absent;
179
180
181
182
  }
    
let diff x y = 
  if x == y then empty else {
183
184
185
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
186
    record= BoolRec.diff x.record y.record;
187
188
189
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
190
    absent= x.absent && not y.absent;
191
192
  }
    
193

194
let equal_descr a b =
195
196
197
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
198
199
200
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
201
  (BoolRec.equal a.record b.record) &&
202
  (a.absent == b.absent)
203
204

let compare_descr a b =
205
206
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
207
208
  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
209
210
211
  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
212
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
213
214
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
215
216
  else 0

217
let hash_descr a =
218
219
220
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
221
222
223
  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
224
  let accu = 17 * accu + BoolRec.hash a.record in
225
  let accu = if a.absent then accu+5 else accu in
226
  accu
227

228
229
230
231
232
233
234
235
(* 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) &&
236
237
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
238

239

240
241
242
243
244
245
246
247
248
module Descr =
struct 
  type t = descr
  let hash = hash_descr
  let equal = equal_descr
  let compare = compare_descr
end
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
249
module DescrSet = Set.Make(Descr)
250
251
252
253
254
255
256
257
258

module Descr1 =
struct 
  type 'a t = descr
  let hash = hash_descr
  let equal = equal_descr
  let compare = compare_descr
end
module DescrSList = SortedList.Make(Descr1)
259

260
(* let hash_cons = DescrHash.create 17000 *)
261

262
let count = State.ref "Types.count" 0
263
264
265
266
267
let make () = incr count; { id = !count; descr = empty }
let define n d = 
(*  DescrHash.add hash_cons d n; *)
  n.descr <- d
let cons d = 
268
(*   try DescrHash.find hash_cons d with Not_found ->
269
  incr count; let n = { id = !count; descr = d } in
270
  DescrHash.add hash_cons d n; n  *)
271
272
273
274
275
276
277
278
  incr count; { id = !count; descr = d }
let descr n = n.descr
let internalize n = n
let id n = n.id




279
280
let neg x = diff any x

281
282
let any_node = cons any

283
module LabelS = Set.Make(LabelPool)
284
285
286

let get_record r =
  let labs accu (_,r) = 
287
288
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
289
  let extend descrs labs (o,r) =
290
291
292
293
294
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
295
	      | (l2,x)::r when l1 == l2 -> 
296
297
298
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
299
		  if not o then descrs.(i) <- 
300
		    cap descrs.(i) { empty with absent = true }; (* TODO:OPT *)
301
302
		  aux (i+1) labs r
    in
303
    aux 0 labs (LabelMap.get r);
304
305
306
307
    o
  in
  let line (p,n) =
    let labels = 
308
309
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
310
    let nlab = List.length labels in
311
    let mk () = Array.create nlab { any with absent = true } in
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326

    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
327
  List.map line (BoolRec.get r)
328
   
329

330

331
332
333
334
335
336
337


(* 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)
338
let cap_product any_left any_right l =
339
340
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
341
    (any_left,any_right)
342
    l
343
344
let any_pair = { empty with times = any.times }

345

346
347
348
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

349
exception NotEmpty
350

351
352
353
354
355
356
357
358
359
360
361
362
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) -> 
363
      if n.status == Maybe then (try f n with NotEmpty -> ());
364
365
366
367
368
369
370
371
372
373
      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;
374
  s.notify <- Nothing; 
375
376
377
378
379
380
381
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
382
383
384
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
385
386
387
	try 
	  f arg s;
	  if s.active then n.active <- true
388
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
389

390
391
let guard a f n =
  match a with
392
    | { status = Empty } -> ()
393
394
395
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
396
    | { status = NEmpty } -> f n
397

398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499

(* 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) 

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

let rec slot d =
500
501
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
502
503
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
504
505
506
507
508
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
509
       iter_s s check_times (BoolPair.get d.times);  
510
       iter_s s check_xml (BoolPair.get d.xml); 
511
       iter_s s check_arrow (BoolPair.get d.arrow);
512
513
514
515
516
517
518
519
520
       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 ->
521
522
523
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
524
525
	     aux accu1 accu2 right s )
	else (
526
          let accu1' = diff accu1 t1 in 
527
	  guard (slot accu1') (aux accu1' accu2 right) s;
528
529

          let accu2' = diff accu2 t2 in 
530
	  guard (slot accu2') (aux accu1 accu2' right) s  
531
	)
532
533
    | [] -> set s
  in
534
  let (accu1,accu2) = cap_product any any left in
535
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
536
537
538
539
540

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
541
	if clearly_disjoint accu1 t1 || 
542
543
544
545
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
546
	  guard (slot accu1') (aux accu1' accu2 right) s;
547
548

          let accu2' = diff accu2 t2 in 
549
	  guard (slot accu2') (aux accu1 accu2' right) s  
550
551
552
553
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
554
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
555

556
557
558
559
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 ->
560
          let accu1' = diff_t accu1 t1 in 
561
	  guard (slot accu1') (aux accu1' accu2 left) s;
562
563

          let accu2' = cap_t  accu2 t2 in 
564
	  guard (slot accu2') (aux accu1 accu2' left) s
565
566
567
      | [] -> set s
    in
    let accu1 = descr s1 in
568
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
569
570
  in
  big_conj single_right right s
571

572
and check_record (labels,(oleft,left),rights) s =
573
574
  let rec aux rights s = match rights with
    | [] -> set s
575
    | (oright,right)::rights ->
576
	let next =
577
	  (oleft && (not oright)) ||
578
	  exists (Array.length left)
579
	    (fun i -> trivially_disjoint left.(i) right.(i))
580
581
582
583
584
585
	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
586
587
	    guard (slot di) (fun s ->
			left.(i) <- di;
588
589
590
			aux rights s;
			left.(i) <- back;
		     ) s
591
(* TODO: are side effects correct ? *)
592
593
594
595
596
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
597
      guard (slot left.(i)) (start (i - 1)) s
598
599
600
601
602
603
604
  in
  start (Array.length left - 1) s


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

611
(*
612
let is_empty d =
613
614
615
616
617
618
619
(*  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
*)  
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639

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
      | `Normal -> { d with times = empty.times }
      | `XML -> { d with xml = empty.xml }

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

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

640
641
642
643
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

644
645
646
647
648
649
650
    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*) 
651
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
	      
	      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)

676
*)
677
  let get_aux any_right d =
678
679
    let accu = ref [] in
    let line (left,right) =
680
      let (d1,d2) = cap_product any any_right left in
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
      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
696
    List.iter line (BoolPair.get d);
697
    !accu
698
699
700
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
701

702

703
704
  let get ?(kind=`Normal) d = 
    match kind with
705
706
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
707
708
709

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
710
711
712
713
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
714
715

  let restrict_1 rects pi1 =
716
717
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
718
719
720
721
    List.fold_left aux [] rects
  
  type normal = t

722
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
723

724
725
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
726
  let memo = ref Memo.empty
727
  let normal_times d = 
728
729
730
    try Memo.find d !memo 
    with
	Not_found ->
731
	  let gd = get_aux any d in
732
	  let n = normal_aux gd in
733
734
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
735
736
	  memo := Memo.add d n !memo;
	  n
737

738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
  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


754
755
756
757
758
759
760
761
762
763
  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 []
	 

764
765
766
767
768
769
770
  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

771
772
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
773
  let is_empty d = d == []
774
end
775

776
module Record = 
777
struct
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
  let has_record d = not (is_empty { empty with record = d.record })
  let or_absent d = { d with absent = true }
  let any_or_absent = or_absent any
  let has_absent d = d.absent

  let only_absent = {empty with absent = true}
  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
    let any = { empty with record = any.record }
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module TR = Normal.Make(T)(R)

  let any_record = { empty with record = BoolRec.full }

  let atom o l = 
    if o && LabelMap.is_empty l then any_record else
    { empty with record = BoolRec.atom (o,l) }

  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
	    Pair (any_or_absent, { empty with record = BoolRec.atom (o,r) })
	else
	  Pair (only_absent,
		{ empty with record = BoolRec.atom (o,r) })
    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
    { t with absent = false }

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

864
865
866
867
868
(* 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)
869

870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
  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 
	    then cup t1 { t2 with absent = false } 
	    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

  let any = { empty with record = any.record }

  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 
943
944
945
	  (fun accu (t1,t2) -> 
	     let x = (t1.absent, { t1 with absent = false }) in
	     aux ((l,x)::r) accu t2)
946
947
948
949
950
951
952
953
954
	  accu
	  (split d l)
    in
    aux [] [] d
end


module Print = 
struct
955
  let print_const ppf = function
956
957
958
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
959

960
  let nil_atom = Atoms.mk_ascii "nil"
961
962
963
964
965
966
967
968
969
  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

970
971
972
  module S = struct
  type t = { id : int; 
	     mutable def : d list; 
973
	     mutable state : [ `Expand | `None | `Marked | `Named of U.t ] }
974
  and  d =
975
    | Name of U.t
976
977
978
979
    | Regexp of t Pretty.regexp
    | Atomic of (Format.formatter -> unit)
    | Pair of t * t
    | Char of Chars.v
980
    | Xml of [ `Tag of (Format.formatter -> unit) | `Type of t ] * t * t
981
982
    | Record of (bool * t) label_map * bool * bool
    | Arrows of (t * t) list * (t * t) list
983
    | Neg of t
984
985
986
987
  let compare x y = x.id - y.id
  end
  module Decompile = Pretty.Decompile(DescrHash)(S)
  open S
988
989
990
991
992
993
994
995
996
997
998
999

  module DescrPairMap = 
    Map.Make(
      struct
	type t = descr * descr
	let compare (x1,y1) (x2,y2) =
	  let c = compare_descr x1 x2 in 
	  if c = 0 then compare_descr y1 y2 else c
      end)

  let named = State.ref "Types.Print.named" DescrMap.empty
  let named_xml = State.ref "Types.Print.named_xml"  DescrPairMap.empty
1000
  let register_global (name : U.t) d = 
1001
1002
1003
1004
1005
    if equal_descr { d with xml = BoolPair.empty } empty then 
      (let l = (*Product.merge_same_2*) (Product.get ~kind:`XML d) in
      match l with
	| [(t1,t2)] -> named_xml := DescrPairMap.add (t1,t2) name !named_xml
	| _ -> ());
1006
    named := DescrMap.add d name !named
1007

1008
  let memo = DescrHash.create 63
1009
1010
  let counter = ref 0
  let alloc def = { id = (incr counter; !counter); def = def; state = `None }
1011

1012
1013
1014
  let count_name = ref 0
  let name () =
    incr count_name;
1015
    U.mk ("X" ^ (string_of_int !count_name))
1016

1017
1018
  let to_print = ref []

1019
1020
1021
  let trivial_rec b = 
    b == BoolRec.empty || 
    (is_empty { empty with record = BoolRec.diff BoolRec.full b})
1022

1023
  let trivial_pair b = b == BoolPair.empty || b == BoolPair.full
1024
1025

  let worth_abbrev d = 
1026
1027
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
1028

1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
  let worth_complement d =
    let aux f x y = if f x y = 0 then 1 else 0 in
    let n = 
      aux Atoms.compare d.atoms any.atoms +
      aux Chars.compare d.chars any.chars +
      aux Intervals.compare d.ints any.ints +
      aux BoolPair.compare d.times any.times +
      aux BoolPair.compare d.xml any.xml +
      aux BoolPair.compare d.arrow any.arrow +
      aux BoolRec.compare d.record any.record in
    n >= 4

1041
  let rec prepare d =
1042
    try DescrHash.find memo d
1043
    with Not_found ->
1044
1045
      try 
	let n = DescrMap.find d !named in
1046
1047
	let s = alloc [] in
	s.state <- `Named n;
1048
1049
1050
	DescrHash.add memo d s;
	s
      with Not_found ->
1051
	if worth_complement d then 
1052
	  alloc [Neg (prepare (neg d))]
1053
	else
1054
1055
1056
	let slot = alloc [] in
	if not (worth_abbrev d) then slot.state <- `Expand;
	DescrHash.add memo d slot;
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
	let (seq,not_seq) =
	  if (subtype { empty with times = d.times } seqs_descr) then
	    (cap d seqs_descr, diff d seqs_descr)
	  else
	    (empty, d) in

	let add u = slot.def <- u :: slot.def in
	if (non_empty seq) then
	  add (Regexp (decompile seq));  
	List.iter
	  (fun (t1,t2) -> add (Pair (prepare t1, prepare t2)))
	  (Product.get not_seq);
	List.iter
	  (fun (t1,t2) ->
	     try 
	       let n = DescrPairMap.find (t1,t2) !named_xml in
	       add (Name n)
	     with
		 Not_found ->
	     let tag = 
1077
	       match Atoms.print_tag t1.atoms with
1078
		 | Some a when is_empty { t1 with atoms = Atoms.empty } -> `Tag a
1079
		 | _ -> `Type (prepare t1) in
1080
	     assert (equal_descr { t2 with times = empty.times } empty);
1081
1082
1083
	     List.iter
	       (fun (ta,tb) -> add (Xml (tag, prepare ta, prepare tb)))
	       (Product.get t2)
1084
	  )
1085
1086
1087
	  ((*Product.merge_same_2*) (Product.get ~kind:`XML not_seq));
	List.iter
	  (fun (r,some,none) -> 
1088
	     let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
	     add (Record (r,some,none)))
	  (Record.get not_seq);
	(match Chars.is_char not_seq.chars with
	  | Some c -> add (Char c)
	  | None ->
	      List.iter (fun x -> add (Atomic x)) (Chars.print not_seq.chars));
	List.iter (fun x -> add (Atomic x)) (Intervals.print not_seq.ints);
	List.iter (fun x -> add (Atomic x)) (Atoms.print not_seq.atoms);
	List.iter
	  (fun (p,n) ->
	     let aux (t,s) = prepare (descr t), prepare (descr s) in
	     let p = List.map aux p and n = List.map aux n in
	     add (Arrows (p,n)))
	  (BoolPair.get not_seq.arrow);
	slot.def <- List.rev slot.def;
	slot
	

  and decompile d =
    Decompile.decompile 
      (fun t -> 
	 let tr = Product.get t in
	 let tr = List.map (fun (l,t) -> prepare l, t) tr in
	 tr, Atoms.contains nil_atom t.atoms)
      d

1115
1116
  let gen = ref 0

1117
  let rec assign_name s =
1118
    incr gen;
1119
    match s.state with
1120
1121
1122
1123
1124
      | `None ->  
	  let g = !gen in
	  s.state <- `Marked; 
	  List.iter assign_name_rec s.def;
	  if (s.state == `Marked) && (!gen == g) then s.state <- `None
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
      | `Marked -> s.state <- `Named (name ()); to_print := s :: !to_print
      | _ -> ()
  and assign_name_rec = function
    | Neg t -> assign_name t
    | Name _ | Char _ | Atomic _ -> ()
    | Regexp r -> assign_name_regexp r
    | Pair (t1,t2) -> assign_name t1; assign_name t2
    | Xml (tag,t2,t3) -> 
	(match tag with `Type t -> assign_name t | _ -> ());
	assign_name t2;
	assign_name t3
    | Record (r,_,_) ->
	List.iter (fun (_,(_,t)) -> assign_name t) (LabelMap.get r)
    | Arrows (p,n) ->
	List.iter (fun (t1,t2) -> assign_name t1; assign_name t2) p;
	List.iter (fun (t1,t2) -> assign_name t1; assign_name t2) n
  and assign_name_regexp = function
    | Pretty.Epsilon | Pretty.Empty -> ()
    | Pretty.Alt (r1,r2) 
    | Pretty.Seq (r1,r2) -> assign_name_regexp r1; assign_name_regexp r2
    | Pretty.Star r | Pretty.Plus r -> assign_name_regexp r
    | Pretty.Trans t -> assign_name t

1148
  let rec do_print_slot pri ppf s =
1149
    match s.state with
1150
      | `Named n -> Format.fprintf ppf "%a" U.print n
1151
      | _ -> do_print_slot_real pri ppf s.def
1152
1153
1154
1155
1156
  and do_print_slot_real pri ppf def =
    let rec aux ppf = function
      | [] -> Format.fprintf ppf "Empty"
      | [ h ] -> do_print ppf h
      | h :: t -> Format.fprintf ppf "%a |@ %a" do_print h aux t
1157
    in
1158
1159
1160
1161
    if (pri >= 2) && (List.length def >= 2) 
    then Format.fprintf ppf "@[(%a)@]" aux def
    else aux ppf def
  and do_print ppf = function
1162
    | Neg t -> Format.fprintf ppf "Any \\ (@[%a@])" (do_print_slot 0) t
1163
    | Name n -> Format.fprintf ppf "%a" U.print n
1164
1165
1166
1167
1168
1169
1170
    | Char c -> Chars.print_v ppf c
    | Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r
    | Atomic a -> a ppf
    | Pair (t1,t2) -> 
	Format.fprintf ppf "@[(%a,%a)@]" 
	  (do_print_slot 0) t1 
	  (do_print_slot 0) t2
1171
    | Xml (tag,attr,t) -> 
1172
1173
	Format.fprintf ppf "<%a%a>%a" 
	  do_print_tag tag
1174
1175
	  do_print_attr attr
	  (do_print_slot 0) t
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
    | Record (r,some,none) ->
	if some then Format.fprintf ppf "@[{"
	else Format.fprintf ppf "@[{|";
	do_print_record ppf r;
	if not none then  Format.fprintf ppf ";@ ...";
	if some then Format.fprintf ppf " }@]"
	else Format.fprintf ppf " |}@]"
    | Arrows (p,n) ->
	(match p with
	   | [] -> Format.fprintf ppf "Arrow"
	   | (t,s)::l ->
	       Format.fprintf ppf "%a" do_print_arrow (t,s);
	       List.iter 
		 (fun (t,s) ->
		    Format.fprintf ppf " &@ %a" do_print_arrow (t,s)
		 ) l);
	List.iter 
	  (fun (t,s) ->
	     Format.fprintf ppf " \\@ %a" do_print_arrow (t,s)
	  ) n
  and do_print_arrow ppf (t,s) =
    Format.fprintf ppf "%a -> %a"
      (do_print_slot 0) t
      (do_print_slot 0) s
  and do_print_tag ppf = function
1201
    | `Tag s -> s ppf
1202
1203
    | `Type t -> Format.fprintf ppf "(%a)" (do_print_slot 0) t
  and do_print_attr ppf = function
1204
1205
    | { state = `Marked|`Expand; 
	def = [ Record (r,true,true) ] } -> do_print_record ppf r