types.ml 37.6 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
21
22
23
24
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
25
26


27
28
29
30
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
31

32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
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

47
48
type pair_kind = [ `Normal | `XML ]

49
50
51
52
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
53
54
55
  let dump ppf (x,y) =
    Format.fprintf ppf "(%i,%i)" x.id y.id
  let compare (y1,x1) (y2,x2) =
56
57
58
59
60
61
62
    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 

63
64
65
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
66
67
  let dump ppf (o,r) = ()

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
99
100
101
  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

102
103
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
104

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

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

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

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

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

226

227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
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)

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

246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
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




265
266
let print_descr = ref (fun _ _  -> assert false)

267
268
let neg x = diff any x

269
270
let any_node = cons any

271
module LabelS = Set.Make(LabelPool)
272
273
274

let get_record r =
  let labs accu (_,r) = 
275
276
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
277
  let extend descrs labs (o,r) =
278
279
280
281
282
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
283
	      | (l2,x)::r when l1 == l2 -> 
284
285
286
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
287
288
		  if not o then descrs.(i) <- 
		    cap descrs.(i) { empty with absent = true };
289
290
		  aux (i+1) labs r
    in
291
    aux 0 labs (LabelMap.get r);
292
293
294
295
    o
  in
  let line (p,n) =
    let labels = 
296
297
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
298
    let nlab = List.length labels in
299
    let mk () = Array.create nlab { any with absent = true } in
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314

    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
315
  List.map line (BoolRec.get r)
316
   
317

318

319
320
321
322
323
324
325
326
327
328
329
330


(* 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
331
332
333
334
335
let cup_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
    (empty,empty)
    l
336

337
338
339
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

340
let trivially_empty d = equal_descr d empty
341

342
exception NotEmpty
343

344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
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;
370
  s.notify <- Nothing; 
371
372
373
374
375
376
377
378
379
380
381
382
383
384
  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

let rec guard a f n =
385
386
  match slot a with
    | { status = Empty } -> ()
387
    | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
388
    | { status = NEmpty } -> f n
389
390
391
392

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
393
394
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
395
396
  else try DescrHash.find memo d
  with Not_found ->
397
(*    Format.fprintf Format.std_formatter "Empty:%a@\n" !print_descr d; *)
398
399
400
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
401
402
403
       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);
404
405
406
407
408
409
410
       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 =
411
(*  Printf.eprintf "[%i]" (List.length right);
412
  flush stderr;  *)
413
414
415
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	if trivially_empty (cap_t accu1 t1) || 
416
417
418
	   trivially_empty (cap_t accu2 t2) then (
	     aux accu1 accu2 right s )
	else (
419
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
420
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
421
	)
422
423
    | [] -> set s
  in
424
425
426
427
428
429
430
431
432
(*
  if List.length right > 6 then (
    Printf.eprintf "HEURISTIC\n"; flush stderr;
    let (n1,n2) = cup_product right in
    let n1 = diff accu1 n1 and n2 = diff accu2 n2 in
    guard n1 set s;
    guard n2 set s;
    Printf.eprintf "HEURISTIC failed\n"; flush stderr;
  ); *)
433
434
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
435

436
437
438
439
440
441
442
443
444
445
446
447
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
448

449
and check_record (labels,(oleft,left),rights) s =
450
451
  let rec aux rights s = match rights with
    | [] -> set s
452
    | (oright,right)::rights ->
453
	let next =
454
	  (oleft && (not oright)) || (* ggg... why ???  check this line *)
455
456
	  exists (Array.length left)
	    (fun i ->
457
	       trivially_empty (cap left.(i) right.(i)))
458
459
460
461
462
463
	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
464
465
466
467
468
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
469
470
471
472
473
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
474
      guard left.(i) (start (i - 1)) s
475
476
477
478
479
  in
  start (Array.length left - 1) s


let is_empty d =
480
(*  Printf.eprintf "is_empty: start\n"; flush stderr; *)
481
482
483
484
485
  let s = slot d in
  List.iter 
    (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing) 
    !marks;
  marks := [];
486
(*  Printf.eprintf "is_empty: done\n"; flush stderr; *)
487
488
489
  s.status = Empty
  

490
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
491
492
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
493

494
let rec empty_rec d =
495
  if not (Intervals.is_empty d.ints) then false
496
497
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
498
  else if d.absent then false
499
500
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
501
502
  else (
    let backup = !memo in
503
    memo := Assumptions.add d backup;
504
    if 
505
506
507
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
508
509
510
511
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
512
      DescrHash.add cache_false d ();
513
514
515
516
517
518
519
520
521
522
      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 ->
523
524
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
525
526
527
528
529
	  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
530
	  if not (empty_rec accu2') then aux accu1 accu2' right
531
532
533
534
535
    | [] -> 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)
536

537
538
539
540
541
542
543
544
545

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
546
          if not (empty_rec accu1') then aux accu1' accu2 left;
547
          let accu2' = cap_t accu2 t2 in
548
          if not (empty_rec accu2') then aux accu1 accu2' left
549
550
551
552
553
554
555
556
      | [] -> 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

557
and empty_rec_record_aux (labels,(oleft,left),rights) =
558
559
  let rec aux = function
    | [] -> raise NotEmpty
560
    | (oright,right)::rights ->
561
562
563
564
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
565
	       trivially_empty (cap left.(i) right.(i)))
566
567
568
569
570
571
	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
572
	    if not (empty_rec di) then (
573
574
575
576
577
578
579
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
580
    (fun i -> empty_rec left.(i))
581
582
583
584
  ||
  (try aux rights; true with NotEmpty -> false)
	    

585
and empty_rec_record c =
586
  List.for_all empty_rec_record_aux (get_record c)
587

588
589
(*
let is_empty d =
590
  empty_rec d
591
  *)
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619

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*) 
620
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
	      
	      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

638
(*
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
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)

667
*)
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
  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
687
    List.iter line (BoolPair.get d);
688
    !accu
689
690
691
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
692

693

694
695
  let get ?(kind=`Normal) d = 
    match kind with
696
697
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
698
699
700

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
701
702
703
704
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
705
706

  let restrict_1 rects pi1 =
707
708
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
709
710
711
712
    List.fold_left aux [] rects
  
  type normal = t

713
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
714
715
716
717
718
719
720
721


  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 ->
722
	  let gd = get_aux d in
723
	  let n = normal_aux gd in
724
725
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
726
727
	  memo := Memo.add d n !memo;
	  n
728

729
730
731
732
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
733

734
735
module Print = 
struct
736
737
738
739
740
741
742
  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
743
744
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
745

746
  let print_const ppf = function
747
748
749
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
750

751
752
753
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
754
755
756
757
758
759
760
761
762
763

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

764
  let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
765
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
766
767

  let worth_abbrev d = 
768
769
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
770
771
772

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
773
    if not (DescrMap.mem d !named) then
774
775
776
777
778
779
780
781
      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);
782
783
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
784
785
	  (fun (n1,n2) -> mark n1; mark n2
(*
786
787
788
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
789
790
791
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
792
		  let l = get_record d1.record in
793
794
795
796
797
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
798
799
	       )
	       (Product.normal (descr n2))
800
*)
801
	  ) d.xml;
802
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
803
804
805
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
806
807
808
809
810

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
811
      let name = DescrMap.find d !named in
812
813
814
815
816
817
818
      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
819
	  Not_found -> assert false
820
821
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
822
823
824
825
826
827
828
829
830
      (
	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 @
831
	   BoolRec.print "Record" print_record d.record
832
833
	  )
      )
834
835
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
836
  and print_xml ppf (t1,t2) =
837
838
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
839
840
841
842
843
844
845
846
847
    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
848
*)
849
850
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
851
852
853
854
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
855
    List.iter (fun (l,t) ->
856
		 let sep = if !first then (first := false; "") else ";" in
857
858
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
859
	      ) (LabelMap.get r);
860
861
    Format.fprintf ppf " %s}@]" o
(*
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
  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
879
*)
880
881
882

	  
  let end_print ppf =
883
    Format.fprintf ppf "@]";
884
885
886
887
888
889
890
891
892
893
    (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 "@]"
    );
894
(*    Format.fprintf ppf "@]"; *)
895
896
897
898
899
900
901
902
903
904
905
906
907
    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

908
let () = print_descr := Print.print_descr
909

910
911
module Positive =
struct
912
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
913
  and v = { mutable def : rhs; mutable node : node option }
914
915


916
917
918
919
920
921
922
923
924
  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)
925
	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
926

927
928
929
930
931
932
933
934
935
  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
936

937
938
939
940
941
942
  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))
943
  let xml d1 d2 = cons (`Xml (d1,d2))
944
  let define v1 v2 = def v1 (`Cup [v2]) 
945

946
947
  let solve v = internalize (make_node v)
end
948

949

950

951

952
953
954
(* Sample value *)
module Sample =
struct
955

956

957
958
959
960
961
let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
962
963
964
  | Int of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
965
966
  | Pair of (t * t)
  | Xml of (t * t)
967
  | Record of (bool * (label * t) list)
968
  | Fun of (node * node) list
969
  | Other
970
 exception FoundSampleRecord of bool * (label * t) list
971
972
973
974
975

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 ->
976
    try Atom (Atoms.sample d.atoms) with 
977
978
	Not_found ->
(* Here: could create a fresh atom ... *)
979
    try Char (Chars.sample d.chars) with Not_found ->
980
    try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
981
982

    let memo = Assumptions.add d memo in
983
984
    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 ->
985
986
987
988
989
990
991
992
993
994
    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 ->
995
996
(*TODO: check: is this correct ?  non_empty could return true
  but because of coinduction, the call to aux may raise Not_found, no ? *)
997
998
999
1000
1001
        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
1002
    | [] -> (sample_rec memo accu1, sample_rec memo accu2)
1003
1004
1005
1006
  in
  let (accu1,accu2) = cap_product left in
  if (is_empty accu1) || (is_empty accu2) then raise Not_found;
  aux accu1 accu2 right
1007

1008
1009
and sample_rec_arrow c =
  find sample_rec_arrow_aux c
1010

1011
1012
1013
1014
1015
1016
1017
1018
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
1019
  in
1020
1021
1022
1023
1024
1025
1026
1027
1028
  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
1029
1030
1031
1032
1033
  else Fun left


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

1035
and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1036
1037
1038
1039
  let rec aux = function
    | [] -> 
	let l = ref labels and fields = ref [] in
	for i = 0 to Array.length left - 1 do
1040
	  fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1041
1042
	  l := List.tl !l
	done;
1043
	raise (FoundSampleRecord (oleft, List.rev !fields))
1044
    | (oright,right)::rights ->
1045
1046
1047
1048
1049
1050
	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
1051
	    if not (is_empty di) then (
1052
1053
1054
1055
1056
1057
1058
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  if exists (Array.length left) 
1059
    (fun i -> is_empty left.(i)) then raise Not_found;
1060
  try aux rights; raise Not_found
1061
  with FoundSampleRecord (o,r) -> (o,r)
1062
1063
1064
1065

	    


1066

1067
let get x = try sample_rec Assumptions.empty x with Not_found -> Other
1068

1069
1070
1071
1072
1073
1074
1075
  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
1076
1077
1078
    | Int i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
1079
    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
1080
1081
    | Xml (Atom tag, Pair (attr, child)) -> 
	Format.fprintf ppf "<%s>%a" (Atoms.value tag) (*print attr*) print child
1082
    | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
1083
1084
    | Record (o,r) ->
	Format.fprintf ppf "{ %a%s }"
1085
1086
1087
	  (print_sep 
	     (fun ppf (l,x) -> 
		Format.fprintf ppf "%s = %a"
1088
		(LabelPool.value l)
1089
1090
1091
1092
		print x
	     )
	     " ; "
	  ) r
1093
	  (if o then "; ..." else "")
1094
1095
1096
1097
1098
1099
1100
1101
1102
    | 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
1103
1104
    | Other ->
	Format.fprintf ppf "[cannot determine value]"
1105
1106
end

1107
1108


1109
module Record = 
1110
struct
1111
1112
1113
1114
  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
1115