types.ml 36.6 KB
Newer Older
1
2
3
4
open Recursive
open Printf


5
6
let map_sort f l =
  SortedList.from_list (List.map f l)
7

8
9
10
11
12
13
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
14

15
16
module LabelPool = Pool.Make(SortedList.String)
module X = SortedList.Make(SortedList.Lift(LabelPool))
17

18
type label = LabelPool.t
19

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

25
26
type pair_kind = [ `Normal | `XML ]

27
28
29
30
31
32
33
34
35
36
37
38
39
40
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
  let compare (x1,y1) (x2,y2) =
    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 

module BoolPair = Boolean.Make(NodePair)

41
type descr = {
42
  atoms : Atoms.t;
43
44
  ints  : Intervals.t;
  chars : Chars.t;
45
46
47
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
48
49
  record: (bool * (label, node) SortedMap.t) Boolean.t;
  absent: bool
50
} and node = descr node0
51

52
	       
53
let empty = { 
54
55
56
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
57
58
59
60
  record= Boolean.empty;
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
61
  absent= false;
62
63
64
}
	      
let any =  {
65
66
67
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
68
69
70
71
  record= Boolean.full; 
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
72
  absent= false;
73
74
75
76
}
	     
	     
let interval i = { empty with ints = i }
77
78
79
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) }
80
81
let record label t = 
  { empty with record = Boolean.atom (true,[label,t]) }
82
83
84
85
86
87
88
89
let record' x =
  { empty with record = Boolean.atom x }
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)
90
      
91
92
let cup x y = 
  if x == y then x else {
93
94
95
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
96
97
98
99
    record= Boolean.cup x.record y.record;
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
100
    absent= x.absent || y.absent;
101
102
103
104
  }
    
let cap x y = 
  if x == y then x else {
105
106
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
107
    record= Boolean.cap x.record y.record;
108
    arrow = BoolPair.cap x.arrow y.arrow;
109
110
111
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
112
    absent= x.absent && y.absent;
113
114
115
116
  }
    
let diff x y = 
  if x == y then empty else {
117
118
119
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
120
121
122
123
    record= Boolean.diff x.record y.record;
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
124
    absent= x.absent && not y.absent;
125
126
127
128
129
130
131
132
133
  }
    
let count = ref 0
let make () = incr count; { id = !count; descr = empty }
let define n d = n.descr <- d
let cons d = incr count; { id = !count; descr = d }
let descr n = n.descr
let internalize n = n
let id n = n.id
134
135
136
137

let rec compare_rec r1 r2 =
  if r1 == r2 then 0
  else match (r1,r2) with
138
    | (l1,x1)::r1,(l2,x2)::r2 ->
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
	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 rec compare_rec_list l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
	if o2 && not o1 then -1
	else if o1 && not o2 then 1
	else let c = compare_rec r1 r2 in if c <> 0 then c 
	else compare_rec_list l1 l2
    | ([],_) -> -1
    | _ -> 1

let rec compare_rec_bool l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 ->
	let c = compare_rec_list p1 p2 in if c <> 0 then c 
	else let c = compare_rec_list n1 n2 in if c <> 0 then c 
	else compare_rec_bool l1 l2
    | ([],_) -> -1
    | _ -> 1

let rec compare_times_list l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (x1,y1)::l1, (x2,y2)::l2 ->
	if (x1.id < x2.id) then -1
	else if (x1.id > x2.id) then 1 
	else if (y1.id < y2.id) then -1
	else if (y1.id > y2.id) then 1 
	else compare_times_list l1 l2
    | ([],_) -> -1
    | _ -> 1

let rec compare_times_bool l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 ->
	let c = compare_times_list p1 p2 in if c <> 0 then c 
	else let c = compare_times_list n1 n2 in if c <> 0 then c 
	else compare_times_bool l1 l2
    | ([],_) -> -1
    | _ -> 1
189
190
191
192
	     
let rec equal_rec r1 r2 =
  (r1 == r2) ||
  match (r1,r2) with
193
194
    | (l1,x1)::r1,(l2,x2)::r2 ->
	(x1.id = x2.id) && (l1 == l2) && (equal_rec r1 r2)
195
    | _ -> false
196
197
198
199
200
	
let rec equal_rec_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
201
202
	(o1 == o2) &&
	(equal_rec r1 r2) && (equal_rec_list l1 l2)
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
    | _ -> false
	
let rec equal_rec_bool l1 l2 =
  (l1 == l2) ||
  match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 -> 
	(equal_rec_list p1 p2) &&
	(equal_rec_list n1 n2) &&
        (equal_rec_bool l1 l2)
    | _ -> false
	
let rec equal_times_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (x1,y1)::l1, (x2,y2)::l2 -> 
	(x1.id = x2.id) &&
	(y1.id = y2.id) &&
	(equal_times_list l1 l2)
    | _ -> false
	
let rec equal_times_bool l1 l2 =
  (l1 == l2) ||
  match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 -> 
	(equal_times_list p1 p2) &&
	(equal_times_list n1 n2) &&
        (equal_times_bool l1 l2)
    | _ -> false
	
let equal_descr a b =
233
234
235
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
236
237
238
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
239
240
  (equal_rec_bool a.record b.record) &&
  (a.absent == b.absent)
241
242
243
244
245

let compare_descr a b =
  let c = compare a.atoms b.atoms in if c <> 0 then c
  else let c = compare a.chars b.chars in if c <> 0 then c
  else let c = compare a.ints b.ints in if c <> 0 then c
246
247
248
  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
249
  else let c = compare_rec_bool a.record b.record in if c <> 0 then c
250
251
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
252
253
254
255
256
257
258
259
260
261
  else 0

(*
let compare_descr a b =
  let c = compare_descr a b in
  assert (c = compare a b);
  c
*)


262
263
264
265
266
267
268
269
270
271
272
let rec hash_times_list accu = function
  | (x,y)::l ->
      hash_times_list (accu * 257 + x.id * 17 + y.id) l
  | [] -> accu + 17
      
let rec hash_times_bool accu = function
  | (p,n)::l -> 
      hash_times_bool (hash_times_list (hash_times_list accu p) n) l
  | [] -> accu + 3
      
let rec hash_rec accu = function
273
  | (l,x)::rem ->
274
275
276
277
278
      hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
  | [] -> accu + 5
      
let rec hash_rec_list accu = function
  | (o,r)::l ->
279
      hash_rec_list (hash_rec (if o then accu*3 else accu) r) l
280
281
282
283
284
285
286
287
288
  | [] -> accu + 17
      
let rec hash_rec_bool accu = function
  | (p,n)::l -> 
      hash_rec_bool (hash_rec_list (hash_rec_list accu p) n) l
  | [] -> accu + 3
      
      
let hash_descr a =
289
290
291
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
292
293
294
  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
295
  let accu = hash_rec_bool accu a.record in
296
  let accu = if a.absent then accu+5 else accu in
297
  accu
298

299
300
301
302
303
304
305
306
307
module DescrHash = 
  Hashtbl.Make(
    struct 
      type t = descr
      let hash = hash_descr
      let equal = equal_descr
    end
  )

308
309
let print_descr = ref (fun _ _  -> assert false)

310
311
let neg x = diff any x

312
313
let any_node = cons any

314
315
316
317
318
module LabelSet = Set.Make(LabelPool)

let get_record r =
  let labs accu (_,r) = 
    List.fold_left (fun accu (l,_) -> LabelSet.add l accu) accu r in
319
  let extend descrs labs (o,r) =
320
321
322
323
324
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
325
	      | (l2,x)::r when l1 == l2 -> 
326
327
328
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
329
330
		  if not o then descrs.(i) <- 
		    cap descrs.(i) { empty with absent = true };
331
332
333
334
335
336
337
338
339
340
		  aux (i+1) labs r
    in
    aux 0 labs r;
    o
  in
  let line (p,n) =
    let labels = 
      List.fold_left labs (List.fold_left labs LabelSet.empty p) n in
    let labels = LabelSet.elements labels in
    let nlab = List.length labels in
341
    let mk () = Array.create nlab { any with absent = true } in
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358

    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
  List.map line r
   
359

360
module DescrMap = Map.Make(struct type t = descr let compare = compare end)
361
362

let check d =
363
364
365
  BoolPair.check d.times;
  BoolPair.check d.xml;
  BoolPair.check d.arrow;
366
367
368
  Boolean.check d.record;
  ()

369
370
371
372
373
374
375
376
377
378
379
380
381


(* 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)
let cap_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
    (any,any)
    l

382
383
384
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

385
let trivially_empty d = equal_descr d empty
386

387
exception NotEmpty
388

389
390
391
392
393
394
395
396
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
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 memo = DescrHash.create 33000

let marks = ref [] 
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) -> 
      if n.status = Maybe then (try f n with NotEmpty -> ());
      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;
  raise NotEmpty

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

428

429
let rec guard a f n =
430
431
  match slot a with
    | { status = Empty } -> ()
432
433
    | { status = Maybe } as s -> 
	n.active <- true; s.notify <- Do (n,f,s.notify)
434
    | { status = NEmpty } -> f n
435
436
437
438

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
439
440
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
441
442
443
444
445
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
446
447
448
       iter_s s check_times (BoolPair.get d.times);
       iter_s s check_times (BoolPair.get d.xml);
       iter_s s check_arrow (BoolPair.get d.arrow);
449
450
451
452
453
454
455
456
457
458
459
460
461
462
       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 ->
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
	     aux accu1 accu2 right s
	else
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
463
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
464
465
466
467
    | [] -> set s
  in
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
468

469
470
471
472
473
474
475
476
477
478
479
480
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 ->
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 left) s;
          let accu2' = cap_t  accu2 t2 in guard accu2' (aux accu1 accu2' left) s
      | [] -> set s
    in
    let accu1 = descr s1 in
    guard accu1 (aux accu1 (neg (descr s2)) left) s
  in
  big_conj single_right right s
481

482
and check_record (labels,(oleft,left),rights) s =
483
484
  let rec aux rights s = match rights with
    | [] -> set s
485
    | (oright,right)::rights ->
486
	let next =
487
	  (oleft && (not oright)) || (* ggg... why ???  check this line *)
488
489
	  exists (Array.length left)
	    (fun i ->
490
	       trivially_empty (cap left.(i) right.(i)))
491
492
493
494
495
496
	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
497
498
499
500
501
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
502
503
504
505
506
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
507
      guard left.(i) (start (i - 1)) s
508
509
510
511
512
513
514
515
516
517
518
519
520
  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
  

521
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
522
523
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
524

525
let rec empty_rec d =
526
  if not (Intervals.is_empty d.ints) then false
527
528
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
529
  else if d.absent then false
530
531
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
532
533
  else (
    let backup = !memo in
534
    memo := Assumptions.add d backup;
535
    if 
536
537
538
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
539
540
541
542
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
543
      DescrHash.add cache_false d ();
544
545
546
547
548
549
550
551
552
553
      false
    )
  )

and empty_rec_times c =
  List.for_all empty_rec_times_aux c

and empty_rec_times_aux (left,right) =
  let rec aux accu1 accu2 = function
    | (t1,t2)::right ->
554
555
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
556
557
558
559
560
	  aux accu1 accu2 right
	else
          let accu1' = diff_t accu1 t1 in
          if not (empty_rec accu1') then aux accu1' accu2 right;
          let accu2' = diff_t accu2 t2 in
561
	  if not (empty_rec accu2') then aux accu1 accu2' right
562
563
564
565
566
    | [] -> raise NotEmpty
  in
  let (accu1,accu2) = cap_product left in
  (empty_rec accu1) || (empty_rec accu2) ||
    (try aux accu1 accu2 right; true with NotEmpty -> false)
567

568
569
570
571
572
573
574
575
576

and empty_rec_arrow c =
  List.for_all empty_rec_arrow_aux c

and empty_rec_arrow_aux (left,right) =
  let single_right (s1,s2) =
    let rec aux accu1 accu2 = function
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
577
          if not (empty_rec accu1') then aux accu1' accu2 left;
578
          let accu2' = cap_t accu2 t2 in
579
          if not (empty_rec accu2') then aux accu1 accu2' left
580
581
582
583
584
585
586
587
      | [] -> raise NotEmpty
    in
    let accu1 = descr s1 in
    (empty_rec accu1) ||
    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
  in
  List.exists single_right right

588
and empty_rec_record_aux (labels,(oleft,left),rights) =
589
590
  let rec aux = function
    | [] -> raise NotEmpty
591
    | (oright,right)::rights ->
592
593
594
595
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
596
	       trivially_empty (cap left.(i) right.(i)))
597
598
599
600
601
602
	in
	if next then aux rights 
	else
	  for i = 0 to Array.length left - 1 do
	    let back = left.(i) in
	    let di = diff back right.(i) in
603
	    if not (empty_rec di) then (
604
605
606
607
608
609
610
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
611
    (fun i -> empty_rec left.(i))
612
613
614
615
  ||
  (try aux rights; true with NotEmpty -> false)
	    

616
and empty_rec_record c =
617
  List.for_all empty_rec_record_aux (get_record c)
618

619
620
(*
let is_empty d =
621
  empty_rec d
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

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

  let normal_aux d =
    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
	      
	      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

669
(*
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
This version explodes when dealing with
   Any - [ t1? t2? t3? ... tn? ]
==> need partitioning 
*)
  let get_aux d =
    let line accu (left,right) =
      let rec aux accu d1 d2 = function
	| (t1,t2)::right ->
	    let accu = 
	      let d1 = diff_t d1 t1 in
              if is_empty d1 then accu else aux accu d1 d2 right in
	    let accu =
              let d2 = diff_t d2 t2 in
              if is_empty d2 then accu else aux accu d1 d2 right in
	    accu
	| [] -> (d1,d2) :: accu
      in
      let (d1,d2) = cap_product left in
      if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
    in
    List.fold_left line [] d

(* Partitioning:

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

698
*)
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
  let get_aux d =
    let accu = ref [] in
    let line (left,right) =
      let (d1,d2) = cap_product left in
      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
718
    List.iter line (BoolPair.get d);
719
    !accu
720
721
722
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
723

724

725
726
  let get ?(kind=`Normal) d = 
    match kind with
727
728
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
729
730
731

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
732
733
734
735
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
736
737

  let restrict_1 rects pi1 =
738
739
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
740
741
742
743
    List.fold_left aux [] rects
  
  type normal = t

744
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
745
746
747
748
749
750
751
752


  let memo = ref Memo.empty
  let normal ?(kind=`Normal) d = 
    let d = match kind with `Normal -> d.times | `XML -> d.xml in
    try Memo.find d !memo 
    with
	Not_found ->
753
	  let gd = get_aux d in
754
	  let n = normal_aux gd in
755
756
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
757
758
	  memo := Memo.add d n !memo;
	  n
759

760
761
762
763
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
764

765
766
module Print = 
struct
767
768
769
770
771
772
773
  let rec print_union ppf = function
    | [] -> Format.fprintf ppf "Empty"
    | [h] -> h ppf
    | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t

  let print_tag ppf a =
    match Atoms.is_atom a with
774
775
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
776

777
  let print_const ppf = function
778
779
780
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
781

782
783
784
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
785
786
787
788
789
790
791
792
793
794
795

  let marks = DescrHash.create 63
  let wh = ref []
  let count_name = ref 0
  let name () =
    incr count_name;
    "X" ^ (string_of_int !count_name)
(* TODO: 
   check that these generated names does not conflict with declared types *)

  let trivial b = b = Boolean.empty || b = Boolean.full
796
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
797
798

  let worth_abbrev d = 
799
    not (trivial_pair d.times && trivial_pair d.xml && trivial_pair d.arrow && trivial d.record) 
800
801
802

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
803
    if not (DescrMap.mem d !named) then
804
805
806
807
808
809
810
811
      try 
	let r = DescrHash.find marks d in
	if (!r = None) && (worth_abbrev d) then 
	  let na = name () in 
	  r := Some na;
	  wh := (na,d) :: !wh
      with Not_found -> 
	DescrHash.add marks d (ref None);
812
813
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
814
815
	  (fun (n1,n2) -> mark n1; mark n2
(*
816
817
818
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
819
820
821
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
822
		  let l = get_record d1.record in
823
824
825
826
827
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
828
829
	       )
	       (Product.normal (descr n2))
830
*)
831
	  ) d.xml;
832
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
833
    	Boolean.iter (fun (o,l) -> List.iter (fun (l,n) -> mark n) l) d.record
834
835
836
837
838

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
839
      let name = DescrMap.find d !named in
840
841
842
843
844
845
846
      Format.fprintf ppf "%s" name
    with Not_found ->
      try
      	match !(DescrHash.find marks d) with
      	  | Some n -> Format.fprintf ppf "%s" n
      	  | None -> real_print_descr ppf d
      with
847
	  Not_found -> assert false
848
849
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
850
851
852
853
854
855
856
857
858
859
860
861
      (
	if d.absent then Format.fprintf ppf "?";
	print_union ppf 
	  (Intervals.print d.ints @
	   Chars.print d.chars @
	   Atoms.print d.atoms @
	   BoolPair.print "Pair" print_times d.times @
	   BoolPair.print "XML" print_xml d.xml @
	   BoolPair.print "Arrow" print_arrow d.arrow @
	   Boolean.print "Record" print_record d.record
	  )
      )
862
863
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
864
  and print_xml ppf (t1,t2) =
865
866
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
867
868
869
870
871
872
873
874
875
    let l = Product.normal (descr t2) in
    let l = List.map
	      (fun (d1,d2) ppf ->
		 Format.fprintf ppf "@[<><%a%a>%a@]" 
		   print_tag (descr t1).atoms
		   print_attribs d1.record 
		   print_descr d2) l
    in
    print_union ppf l
876
*)
877
878
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
879
880
881
882
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
883
    List.iter (fun (l,t) ->
884
		 let sep = if !first then (first := false; "") else ";" in
885
886
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
887
888
889
	      ) r;
    Format.fprintf ppf " %s}@]" o
(*
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
  and print_attribs ppf r =
    let l = get_record r in
    if l <> [ [] ] then 
    let l = List.map 
      (fun att ppf ->
	 let first = ref true in
	 Format.fprintf ppf "{" ;
	 List.iter (fun (l,(o,d)) ->
		      Format.fprintf ppf "%s%s=%s%a" 
		        (if !first then "" else " ")
		        (LabelPool.value l) (if o then "?" else "")
		        print_descr d; 
		      first := false
		   ) att;
	   Format.fprintf ppf "}"
      ) l in
    print_union ppf l
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

	  
  let end_print ppf =
    (match List.rev !wh with
       | [] -> ()
       | (na,d)::t ->
	   Format.fprintf ppf " where@ @[%s = %a" na real_print_descr d;
	   List.iter 
	     (fun (na,d) -> 
		Format.fprintf ppf " and@ %s = %a" na real_print_descr d)
	     t;
	   Format.fprintf ppf "@]"
    );
    Format.fprintf ppf "@]";
    count_name := 0;
    wh := [];
    DescrHash.clear marks

  let print_descr ppf d =
    mark_descr d;
    Format.fprintf ppf "@[%a" print_descr d;
    end_print ppf

   let print ppf n = print_descr ppf (descr n)

end

935
let () = print_descr := Print.print_descr
936

937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
module Positive =
struct
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
  and v = { mutable def : rhs; mutable node : node option }


  let rec make_descr seen v =
    if List.memq v seen then empty
    else
      let seen = v :: seen in
      match v.def with
	| `Type d -> d
	| `Cup vl -> 
	    List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
	| `Times (v1,v2) -> times (make_node v1) (make_node v2)

  and make_node v =
    match v.node with
      | Some n -> n
      | None ->
	  let n = make () in
	  v.node <- Some n;
	  let d = make_descr [] v in
	  define n d;
	  n

  let forward () = { def = `Cup []; node = None }
  let def v d = v.def <- d
  let cons d = let v = forward () in def v d; v
  let ty d = cons (`Type d)
  let cup vl = cons (`Cup vl)
  let times d1 d2 = cons (`Times (d1,d2))
  let define v1 v2 = def v1 (`Cup [v2]) 

  let solve v = internalize (make_node v)
end




(* Sample value *)
module Sample =
struct

981

982
983
984
985
986
let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
987
988
989
  | Int of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
990
991
  | Pair of (t * t)
  | Xml of (t * t)
992
993
  | Record of (label * t) list
  | Fun of (node * node) list
994
  | Other
995
  exception FoundSampleRecord of (label * t) list
996
997
998
999
1000

let rec sample_rec memo d =
  if (Assumptions.mem d memo) || (is_empty d) then raise Not_found 
  else 
    try Int (Intervals.sample d.ints) with Not_found ->
1001
    try Atom (Atoms.sample d.atoms) with 
1002
1003
	Not_found ->
(* Here: could create a fresh atom ... *)
1004
    try Char (Chars.sample d.chars) with Not_found ->
1005
    try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
1006
1007

    let memo = Assumptions.add d memo in
1008
1009
    try Pair (sample_rec_times memo (BoolPair.get d.times)) with Not_found ->
    try Xml (sample_rec_times memo (BoolPair.get d.xml)) with Not_found ->
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
    try sample_rec_record memo d.record with Not_found -> 
    raise Not_found


and sample_rec_times memo c = 
  find (sample_rec_times_aux memo) c

and sample_rec_times_aux memo (left,right) =
  let rec aux accu1 accu2 = function
    | (t1,t2)::right ->
1020
1021
(*TODO: check: is this correct ?  non_empty could return true
  but because of coinduction, the call to aux may raise Not_found, no ? *)
1022
1023
1024
1025
1026
        let accu1' = diff_t accu1 t1 in
        if non_empty accu1' then aux accu1' accu2 right else
          let accu2' = diff_t accu2 t2 in
          if non_empty accu2' then aux accu1 accu2' right else
	    raise Not_found
1027
    | [] -> (sample_rec memo accu1, sample_rec memo accu2)
1028
1029
1030
1031
1032
1033
1034
1035
  in
  let (accu1,accu2) = cap_product left in
  if (is_empty accu1) || (is_empty accu2) then raise Not_found;
  aux accu1 accu2 right

and sample_rec_arrow c =
  find sample_rec_arrow_aux c

1036
1037
1038
1039
1040
1041
1042
1043
and check_empty_simple_arrow_line left (s1,s2) = 
  let rec aux accu1 accu2 = function
    | (t1,t2)::left ->
        let accu1' = diff_t accu1 t1 in
        if non_empty accu1' then aux accu1 accu2 left;
        let accu2' = cap_t accu2 t2 in
        if non_empty accu2' then aux accu1 accu2 left
    | [] -> raise NotEmpty
1044
  in
1045
1046
1047
1048
1049
1050
1051
1052
1053
  let accu1 = descr s1 in
  (is_empty accu1) ||
  (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)

and check_empty_arrow_line left right = 
  List.exists (check_empty_simple_arrow_line left) right

and sample_rec_arrow_aux (left,right) =
  if (check_empty_arrow_line left right) then raise Not_found
1054
1055
1056
1057
1058
1059
  else Fun left


and sample_rec_record memo c =
  Record (find (sample_rec_record_aux memo) (get_record c))

1060
and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1061
1062
1063
1064
  let rec aux = function
    | [] -> 
	let l = ref labels and fields = ref [] in
	for i = 0 to Array.length left - 1 do
1065
	  fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1066
1067
1068
	  l := List.tl !l
	done;
	raise (FoundSampleRecord (List.rev !fields))
1069
    | (oright,right)::rights ->
1070
1071
1072
1073
1074
1075
	let next = (oleft && (not oright)) in
	if next then aux rights 
	else
	  for i = 0 to Array.length left - 1 do
	    let back = left.(i) in
	    let di = diff back right.(i) in
1076
	    if not (is_empty di) then (
1077
1078
1079
1080
1081
1082
1083
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  if exists (Array.length left) 
1084
    (fun i -> is_empty left.(i)) then raise Not_found;
1085
1086
1087
1088
1089
1090
  try aux rights; raise Not_found
  with FoundSampleRecord r -> r

	    


1091

1092
let get x = try sample_rec Assumptions.empty x with Not_found -> Other
1093

1094
1095
1096
1097
1098
1099
1100
  let rec print_sep f sep ppf = function
    | [] -> ()
    | [x] -> f ppf x
    | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem


  let rec print ppf = function
1101
1102
1103
    | Int i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
1104
    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
1105
    | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
1106
1107
1108
1109
1110
    | Record r ->
	Format.fprintf ppf "{ %a }"
	  (print_sep 
	     (fun ppf (l,x) -> 
		Format.fprintf ppf "%s = %a"
1111
		(LabelPool.value l)
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
		print x
	     )
	     " ; "
	  ) r
    | Fun iface ->
	Format.fprintf ppf "(fun ( %a ) x -> ...)"
	  (print_sep
	     (fun ppf (t1,t2) ->
		Format.fprintf ppf "%a -> %a; "
		Print.print t1 Print.print t2
	     )
	     " ; "
	  ) iface
1125
1126
    | Other ->
	Format.fprintf ppf "[cannot determine value]"
1127
1128
1129
1130
1131
1132
end



module Record = 
struct
1133
1134
1135
1136
  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
1137

1138
1139
  module T = struct
    type t = descr
1140
    let any = any_or_absent
1141
1142
1143
    let cap = cap
    let cup = cup
    let diff = diff
1144
1145
    let is_empty = is_empty
    let empty = empty
1146
1147
  end
  module R = struct
1148
1149
1150
1151
1152
1153
1154
    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
1155
1156
1157
1158
  end
  module TR = Normal.Make(T)(R)

  let atom = function
1159
1160
    | (true,[]) -> { empty with record = Boolean.full }
    | (o,l) -> { empty with record = Boolean.atom (o,l) }
1161

1162
  let aux d l=
1163
    Boolean.compute_bool
1164
      (fun ((o,r) as x) ->
1165
	 try
1166
1167
	   let lt = List.assoc l r in
	   Boolean.atom (descr lt, atom (o, SortedMap.diff r [l]))
1168
	 with Not_found -> 
1169
	   if o then Boolean.atom (or_absent any, atom x) 
1170
1171
	   else Boolean.empty
      )
1172
      d.record
1173

1174
1175
  let split (d : descr) l =
    TR.boolean (aux d l)
1176

1177
1178
  let split_normal d l =
    TR.boolean_normal (aux d l)
1179

1180

1181
  let project d l =
1182
1183
1184
    let t = TR.pi1 (split d l) in
    if t.absent then raise Not_found;
    t
1185
1186

  let first_label d =
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
    let min = ref LabelPool.dummy_max in
    let aux = 
      function _,(l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
    Boolean.iter aux d.record;
    !min

  let empty_cases d =
    let x = Boolean.compute
	      ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
	      ~diff:(fun a b -> a land lnot b)
	      ~atom:(function (true,[]) -> 3 | (false,[]) -> 1 
		       | _ -> assert false) d.record in
    (x land 2 <> 0, x land 1 <> 0)
    
1201
1202
1203
1204
1205
1206

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



1207
let memo_normalize = ref DescrMap.empty
1208
1209
1210


let rec rec_normalize d =
1211
  try DescrMap.find d !memo_normalize
1212
1213
  with Not_found ->
    let n = make () in
1214
    memo_normalize := DescrMap.add d n !memo_normalize;
1215
    let times = 
1216
1217
1218
      List.fold_left 
	(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
	BoolPair.empty (Product.normal d)
1219
    in
1220
    let xml = 
1221
1222
1223
      List.fold_left 
	(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
	BoolPair.empty (Product.normal ~kind:`XML d)
1224
    in
1225
1226
    let record = d.record
(*
1227
1228
1229
      map_sort
	(fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
	(Record.get d)
1230
*)