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

5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* IDEAS for optimizations:

  * optimize lines of dnf for products and record;
    instead of
      (t1,s1) & ... & (tn,sn) \ ....
    use:
      (t1 & ... & tn, s1 & ... & sn) \ ....

    ---> more compact representation, more sharing, ...
 
  * re-consider using BDD-like representation instead of dnf
*)


19
20
let map_sort f l =
  SortedList.from_list (List.map f l)
21

22
23
24
25
26
27
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
28
29


30
31
32
33
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
34

35
36
type pair_kind = [ `Normal | `XML ]

37
38
39
40
41
42
43
44
45
46
47
48
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 

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
74
75
76
77
78
79
80
81
82
83
84
85
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
  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

86
module BoolPair = Boolean.Make(NodePair)
87
module BoolRec = Boolean.Make(RecArg)
88

89
type descr = {
90
  atoms : Atoms.t;
91
92
  ints  : Intervals.t;
  chars : Chars.t;
93
94
95
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
96
  record: descr BoolRec.t;
97
  absent: bool
98
} and node = descr node0
99

100
	       
101
let empty = { 
102
103
104
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
105
  record= BoolRec.empty;
106
107
108
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
109
  absent= false;
110
111
112
}
	      
let any =  {
113
114
115
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
116
  record= BoolRec.full; 
117
118
119
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
120
  absent= false;
121
122
123
124
}
	     
	     
let interval i = { empty with ints = i }
125
126
127
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) }
128
let record label t = 
129
130
131
  { empty with record = BoolRec.atom (true,LabelMap.singleton label t) }
let record' (x : bool * node Ident.label_map) =
  { empty with record = BoolRec.atom x }
132
133
134
135
136
137
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)
138
      
139
140
let cup x y = 
  if x == y then x else {
141
142
143
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
144
    record= BoolRec.cup x.record y.record;
145
146
147
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
148
    absent= x.absent || y.absent;
149
150
151
152
  }
    
let cap x y = 
  if x == y then x else {
153
154
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
155
    record= BoolRec.cap x.record y.record;
156
    arrow = BoolPair.cap x.arrow y.arrow;
157
158
159
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
160
    absent= x.absent && y.absent;
161
162
163
164
  }
    
let diff x y = 
  if x == y then empty else {
165
166
167
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
168
    record= BoolRec.diff x.record y.record;
169
170
171
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
172
    absent= x.absent && not y.absent;
173
174
  }
    
175
176
177
178

let rec compare_rec r1 r2 =
  if r1 == r2 then 0
  else match (r1,r2) with
179
    | (l1,x1)::r1,(l2,x2)::r2 ->
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
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
	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
230
231
232
233
	     
let rec equal_rec r1 r2 =
  (r1 == r2) ||
  match (r1,r2) with
234
235
    | (l1,x1)::r1,(l2,x2)::r2 ->
	(x1.id = x2.id) && (l1 == l2) && (equal_rec r1 r2)
236
    | _ -> false
237
238
239
240
241
	
let rec equal_rec_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
242
243
	(o1 == o2) &&
	(equal_rec r1 r2) && (equal_rec_list l1 l2)
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
    | _ -> 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 =
274
275
276
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
277
278
279
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
280
  (BoolRec.equal a.record b.record) &&
281
  (a.absent == b.absent)
282
283

let compare_descr a b =
284
285
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
286
287
  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
288
289
290
  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
291
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
292
293
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
294
295
296
297
298
299
300
301
302
303
  else 0

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


304
305
306
307
308
309
310
311
312
313
314
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
315
  | (l,x)::rem ->
316
317
318
319
320
      hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
  | [] -> accu + 5
      
let rec hash_rec_list accu = function
  | (o,r)::l ->
321
      hash_rec_list (hash_rec (if o then accu*3 else accu) r) l
322
323
324
325
326
327
328
329
330
  | [] -> 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 =
331
332
333
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
334
335
336
  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
337
  let accu = 17 * accu + BoolRec.hash a.record in
338
  let accu = if a.absent then accu+5 else accu in
339
  accu
340

341

342
343
344
345
346
347
348
349
350
module DescrHash = 
  Hashtbl.Make(
    struct 
      type t = descr
      let hash = hash_descr
      let equal = equal_descr
    end
  )

351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
let hash_cons = DescrHash.create 17000

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




370
371
let print_descr = ref (fun _ _  -> assert false)

372
373
let neg x = diff any x

374
375
let any_node = cons any

376
module LabelS = Set.Make(LabelPool)
377
378
379

let get_record r =
  let labs accu (_,r) = 
380
381
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
382
  let extend descrs labs (o,r) =
383
384
385
386
387
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
388
	      | (l2,x)::r when l1 == l2 -> 
389
390
391
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
392
393
		  if not o then descrs.(i) <- 
		    cap descrs.(i) { empty with absent = true };
394
395
		  aux (i+1) labs r
    in
396
    aux 0 labs (LabelMap.get r);
397
398
399
400
    o
  in
  let line (p,n) =
    let labels = 
401
402
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
403
    let nlab = List.length labels in
404
    let mk () = Array.create nlab { any with absent = true } in
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419

    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
420
  List.map line (BoolRec.get r)
421
   
422

423
module DescrMap = Map.Make(struct type t = descr let compare = compare end)
424
425

let check d =
426
427
428
  BoolPair.check d.times;
  BoolPair.check d.xml;
  BoolPair.check d.arrow;
429
  BoolRec.check d.record;
430
431
  ()

432
433
434
435
436
437
438
439
440
441
442
443
444


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

445
446
447
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

448
let trivially_empty d = equal_descr d empty
449

450
exception NotEmpty
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
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;
478
  s.notify <- Nothing; 
479
480
481
482
483
484
485
486
487
488
489
490
491
  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

492

493
let rec guard a f n =
494
495
  match slot a with
    | { status = Empty } -> ()
496
    | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
497
    | { status = NEmpty } -> f n
498
499
500
501

and slot d =
  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
510
511
       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);
512
513
514
515
516
517
518
       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 =
519
520
(*  Printf.eprintf "[%i]" (List.length right);
  flush stderr; *)
521
522
523
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	if trivially_empty (cap_t accu1 t1) || 
524
525
526
	   trivially_empty (cap_t accu2 t2) then (
	     aux accu1 accu2 right s )
	else (
527
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
528
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
529
	)
530
531
532
533
    | [] -> set s
  in
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
534

535
536
537
538
539
540
541
542
543
544
545
546
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
547

548
and check_record (labels,(oleft,left),rights) s =
549
550
  let rec aux rights s = match rights with
    | [] -> set s
551
    | (oright,right)::rights ->
552
	let next =
553
	  (oleft && (not oright)) || (* ggg... why ???  check this line *)
554
555
	  exists (Array.length left)
	    (fun i ->
556
	       trivially_empty (cap left.(i) right.(i)))
557
558
559
560
561
562
	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
563
564
565
566
567
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
568
569
570
571
572
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
573
      guard left.(i) (start (i - 1)) s
574
575
576
577
578
  in
  start (Array.length left - 1) s


let is_empty d =
579
(*  Printf.eprintf "is_empty: start\n"; flush stderr; *)
580
581
582
583
584
  let s = slot d in
  List.iter 
    (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing) 
    !marks;
  marks := [];
585
(*  Printf.eprintf "is_empty: done\n"; flush stderr; *)
586
587
588
  s.status = Empty
  

589
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
590
591
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
592

593
let rec empty_rec d =
594
  if not (Intervals.is_empty d.ints) then false
595
596
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
597
  else if d.absent then false
598
599
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
600
601
  else (
    let backup = !memo in
602
    memo := Assumptions.add d backup;
603
    if 
604
605
606
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
607
608
609
610
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
611
      DescrHash.add cache_false d ();
612
613
614
615
616
617
618
619
620
621
      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 ->
622
623
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
624
625
626
627
628
	  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
629
	  if not (empty_rec accu2') then aux accu1 accu2' right
630
631
632
633
634
    | [] -> 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)
635

636
637
638
639
640
641
642
643
644

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
645
          if not (empty_rec accu1') then aux accu1' accu2 left;
646
          let accu2' = cap_t accu2 t2 in
647
          if not (empty_rec accu2') then aux accu1 accu2' left
648
649
650
651
652
653
654
655
      | [] -> 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

656
and empty_rec_record_aux (labels,(oleft,left),rights) =
657
658
  let rec aux = function
    | [] -> raise NotEmpty
659
    | (oright,right)::rights ->
660
661
662
663
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
664
	       trivially_empty (cap left.(i) right.(i)))
665
666
667
668
669
670
	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
671
	    if not (empty_rec di) then (
672
673
674
675
676
677
678
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
679
    (fun i -> empty_rec left.(i))
680
681
682
683
  ||
  (try aux rights; true with NotEmpty -> false)
	    

684
and empty_rec_record c =
685
  List.for_all empty_rec_record_aux (get_record c)
686

687
688
(*
let is_empty d =
689
  empty_rec d
690
  *)
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718

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*) 
719
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
	      
	      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

737
(*
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
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)

766
*)
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
  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
786
    List.iter line (BoolPair.get d);
787
    !accu
788
789
790
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
791

792

793
794
  let get ?(kind=`Normal) d = 
    match kind with
795
796
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
797
798
799

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
800
801
802
803
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
804
805

  let restrict_1 rects pi1 =
806
807
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
808
809
810
811
    List.fold_left aux [] rects
  
  type normal = t

812
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
813
814
815
816
817
818
819
820


  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 ->
821
	  let gd = get_aux d in
822
	  let n = normal_aux gd in
823
824
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
825
826
	  memo := Memo.add d n !memo;
	  n
827

828
829
830
831
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
832

833
834
module Print = 
struct
835
836
837
838
839
840
841
  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
842
843
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
844

845
  let print_const ppf = function
846
847
848
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
849

850
851
852
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
853
854
855
856
857
858
859
860
861
862

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

863
  let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
864
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
865
866

  let worth_abbrev d = 
867
868
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
869
870
871

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
872
    if not (DescrMap.mem d !named) then
873
874
875
876
877
878
879
880
      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);
881
882
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
883
884
	  (fun (n1,n2) -> mark n1; mark n2
(*
885
886
887
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
888
889
890
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
891
		  let l = get_record d1.record in
892
893
894
895
896
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
897
898
	       )
	       (Product.normal (descr n2))
899
*)
900
	  ) d.xml;
901
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
902
903
904
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
905
906
907
908
909

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
910
      let name = DescrMap.find d !named in
911
912
913
914
915
916
917
      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
918
	  Not_found -> assert false
919
920
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
921
922
923
924
925
926
927
928
929
      (
	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 @
930
	   BoolRec.print "Record" print_record d.record
931
932
	  )
      )
933
934
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
935
  and print_xml ppf (t1,t2) =
936
937
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
938
939
940
941
942
943
944
945
946
    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
947
*)
948
949
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
950
951
952
953
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
954
    List.iter (fun (l,t) ->
955
		 let sep = if !first then (first := false; "") else ";" in
956
957
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
958
	      ) (LabelMap.get r);
959
960
    Format.fprintf ppf " %s}@]" o
(*
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
  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
978
*)
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005

	  
  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

1006
let () = print_descr := Print.print_descr
1007

1008
1009
module Positive =
struct
1010
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
  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)
1023
	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040

  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))
1041
  let xml d1 d2 = cons (`Xml (d1,d2))
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
  let define v1 v2 = def v1 (`Cup [v2]) 

  let solve v = internalize (make_node v)
end




(* Sample value *)
module Sample =
struct

1054

1055
1056
1057
1058
1059
let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
1060
1061
1062
  | Int of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
1063
1064
  | Pair of (t * t)
  | Xml of (t * t)
1065
  | Record of (bool * (label * t) list)
1066
  | Fun of (node * node) list
1067
  | Other
1068
 exception FoundSampleRecord of bool * (label * t) list
1069
1070
1071
1072
1073

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 ->
1074
    try Atom (Atoms.sample d.atoms) with 
1075
1076
	Not_found ->
(* Here: could create a fresh atom ... *)
1077
    try Char (Chars.sample d.chars) with Not_found ->
1078
    try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
1079
1080

    let memo = Assumptions.add d memo in
1081
1082
    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 ->
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
    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 ->
1093
1094
(*TODO: check: is this correct ?  non_empty could return true
  but because of coinduction, the call to aux may raise Not_found, no ? *)
1095
1096
1097
1098
1099
        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
1100
    | [] -> (sample_rec memo accu1, sample_rec memo accu2)
1101
1102
1103
1104
1105
1106
1107
1108
  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

1109
1110
1111
1112
1113
1114
1115
1116
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
1117
  in
1118
1119
1120
1121
1122
1123
1124
1125
1126
  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
1127
1128
1129
1130
1131
1132
  else Fun left


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

1133
and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1134
1135
1136
1137
  let rec aux = function
    | [] -> 
	let l = ref labels and fields = ref [] in
	for i = 0 to Array.length left - 1 do
1138
	  fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1139
1140
	  l := List.tl !l
	done;
1141
	raise (FoundSampleRecord (oleft, List.rev !fields))
1142
    | (oright,right)::rights ->
1143
1144
1145
1146
1147
1148
	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
1149
	    if not (is_empty di) then (
1150
1151
1152
1153
1154
1155
1156
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  if exists (Array.length left) 
1157
    (fun i -> is_empty left.(i)) then raise Not_found;
1158
  try aux rights; raise Not_found
1159
  with FoundSampleRecord (o,r) -> (o,r)
1160
1161
1162
1163

	    


1164

1165
let get x = try sample_rec Assumptions.empty x with Not_found -> Other
1166

1167
1168
1169
1170
1171
1172
1173
  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
1174
1175
1176
    | Int i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
1177
    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
1178
1179
    | Xml (Atom tag, Pair (attr, child)) -> 
	Format.fprintf ppf "<%s>%a" (Atoms.value tag) (*print attr*) print child
1180
    | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
1181
1182
    | Record (o,r) ->
	Format.fprintf ppf "{ %a%s }"
1183
1184
1185
	  (print_sep 
	     (fun ppf (l,x) -> 
		Format.fprintf ppf "%s = %a"
1186
		(LabelPool.value l)
1187
1188
1189
1190
		print x
	     )
	     " ; "
	  ) r
1191
	  (if o then "; ..." else "")
1192
1193
1194
1195
1196
1197
1198
1199
1200
    | 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
1201
1202
    | Other ->
	Format.fprintf ppf "[cannot determine value]"