types.ml 39.5 KB
Newer Older
1
open Ident
2

3
4
5
6
7
8
9
10
11
12
(*
To be sure not to use generic comparison ...
*)
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1


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


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

26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
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

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

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

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

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

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

64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
  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

98
99
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
100

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

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

188
let equal_descr a b =
189
190
191
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
192
193
194
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
195
  (BoolRec.equal a.record b.record) &&
196
  (a.absent == b.absent)
197
198

let compare_descr a b =
199
200
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
201
202
  else let c = Chars.compare a.chars b.chars in if c <> 0 then c
  else let c = Intervals.compare a.ints b.ints in if c <> 0 then c
203
204
205
  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
206
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
207
208
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
209
210
  else 0

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

222
223
224
225
226
227
228
229
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
  (Chars.disjoint a.chars b.chars) &&
  (Intervals.disjoint a.ints b.ints) &&
  (Atoms.disjoint a.atoms b.atoms) &&
  (BoolPair.trivially_disjoint a.times b.times) &&
  (BoolPair.trivially_disjoint a.xml b.xml) &&
  (BoolPair.trivially_disjoint a.arrow b.arrow) &&
230
231
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
232

233

234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
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)
252

253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
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




272
273
let print_descr = ref (fun _ _  -> assert false)

274
275
let neg x = diff any x

276
277
let any_node = cons any

278
module LabelS = Set.Make(LabelPool)
279
280
281

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

    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
322
  List.map line (BoolRec.get r)
323
   
324

325

326
327
328
329
330
331
332
333
334
335
336
337


(* Subtyping algorithm *)

let diff_t d t = diff d (descr t)
let cap_t d t = cap d (descr t)
let cup_t d t = cup d (descr t)
let cap_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
    (any,any)
    l
338
339
340
341
342
let cup_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
    (empty,empty)
    l
343

344
345
346
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

347
let trivially_empty d = equal_descr d empty
348

349
exception NotEmpty
350

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

380
let count_slot = ref 0
381
382
383
384
385
386
387
388
389
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
390
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
391
392

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

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
401
402
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
403
404
  else try DescrHash.find memo d
  with Not_found ->
405
406
    (*    incr count_slot;
    Printf.eprintf "%i;" !count_slot; *)
407
(*    Format.fprintf Format.std_formatter "Empty:%a@\n" !print_descr d; *)
408
409
410
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
411
412
413
414
415
(*       Format.fprintf Format.std_formatter "check_times_bool:@[%a@]@\n"
	 BoolPair.dump d.times;  *)
(*       check_times_bool any any d.times s; *)
       iter_s s check_times (BoolPair.get d.times);  
       iter_s s check_times (BoolPair.get d.xml); 
416
       iter_s s check_arrow (BoolPair.get d.arrow);
417
418
419
420
421
422
423
       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 =
424
(*  Printf.eprintf "[%i]" (List.length right);
425
  flush stderr;  *)
426
427
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
428
429
430
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
431
432
	     aux accu1 accu2 right s )
	else (
433
434
435
436
437
438
439
440
441
          let accu1' = diff accu1 t1 in 
	  guard accu1' (aux accu1' accu2 right) s;

          let accu2' = diff accu2 t2 in 
	    guard accu2' (aux accu1 accu2' right) s  
(*	  let accu1 = cap accu1 t1 in (* TODO: approximation of cap ... *)
          let accu2' = diff accu2 t2 in 
	  guard accu1 (guard accu2' (aux accu1 accu2' right)) s *)

442
	)
443
444
    | [] -> set s
  in
445
446
447
  let (accu1,accu2) = cap_product left in
(*  if List.length right > 6 then (
    Printf.eprintf "HEURISTIC\n"; flush stderr; 
448
449
450
451
    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;
452
453
    Printf.eprintf "HEURISTIC failed\n"; flush stderr; 
  );  *)
454
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
455

456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482

(*
and check_times_bool accu1 accu2 b s =
  match b with
    | BoolPair.True -> guard accu1 (guard accu2 set) s
    | BoolPair.False -> ()
    | BoolPair.Split (_, (t1,t2), p,i,n) ->
	check_times_bool accu1 accu2 i s;
	let t1 = descr t1 and t2 = descr t2 in
	if (trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2)
	then check_times_bool accu1 accu2 n s else
	  (
	    if p <> BoolPair.False then
	      (let accu1 = cap accu1 t1 
	       and accu2 = cap accu2 t2 in
	       if not (trivially_empty accu1 || trivially_empty accu2) then
		 check_times_bool accu1 accu2 p s);
	    
	    if n <> BoolPair.False then
	      (let accu1' = diff accu1 t1 in 
	       check_times_bool accu1' accu2 n s;
               let accu2' = diff accu2 t2 in 
	       check_times_bool accu1 accu2' n s)
	  )
*)


483
484
485
486
487
488
489
490
491
492
493
494
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
495

496
and check_record (labels,(oleft,left),rights) s =
497
498
  let rec aux rights s = match rights with
    | [] -> set s
499
    | (oright,right)::rights ->
500
	let next =
501
	  (oleft && (not oright)) ||
502
	  exists (Array.length left)
503
	    (fun i -> trivially_disjoint left.(i) right.(i))
504
505
506
507
508
509
	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
510
511
512
513
514
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
515
516
517
518
519
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
520
      guard left.(i) (start (i - 1)) s
521
522
523
524
525
  in
  start (Array.length left - 1) s


let is_empty d =
526
(*  Printf.eprintf "is_empty: start\n"; flush stderr; *)
527
528
  let s = slot d in
  List.iter 
529
530
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
531
532
    !marks;
  marks := [];
533
(*  Printf.eprintf "is_empty: done\n"; flush stderr; *)
534
  s.status == Empty
535
536
  

537
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
538
539
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
540

541
let rec empty_rec d =
542
  if not (Intervals.is_empty d.ints) then false
543
544
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
545
  else if d.absent then false
546
547
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
548
549
  else (
    let backup = !memo in
550
    memo := Assumptions.add d backup;
551
    if 
552
553
554
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
555
556
557
558
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
559
      DescrHash.add cache_false d ();
560
561
562
563
564
565
566
567
568
569
      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 ->
570
571
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
572
573
574
575
576
	  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
577
	  if not (empty_rec accu2') then aux accu1 accu2' right
578
579
580
581
582
    | [] -> 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)
583

584
585
586
587
588
589
590
591
592

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
593
          if not (empty_rec accu1') then aux accu1' accu2 left;
594
          let accu2' = cap_t accu2 t2 in
595
          if not (empty_rec accu2') then aux accu1 accu2' left
596
597
598
599
600
601
602
603
      | [] -> 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

604
and empty_rec_record_aux (labels,(oleft,left),rights) =
605
606
  let rec aux = function
    | [] -> raise NotEmpty
607
    | (oright,right)::rights ->
608
609
610
611
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
612
	       trivially_empty (cap left.(i) right.(i)))
613
614
615
616
617
618
	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
619
	    if not (empty_rec di) then (
620
621
622
623
624
625
626
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
627
    (fun i -> empty_rec left.(i))
628
629
630
631
  ||
  (try aux rights; true with NotEmpty -> false)
	    

632
and empty_rec_record c =
633
  List.for_all empty_rec_record_aux (get_record c)
634

635
636
(*
let is_empty d =
637
  empty_rec d
638
  *)
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658

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

659
660
661
662
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

663
664
665
666
667
668
669
    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*) 
670
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
	      
	      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

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

717
*)
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
  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
737
    List.iter line (BoolPair.get d);
738
    !accu
739
740
741
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
742

743

744
745
  let get ?(kind=`Normal) d = 
    match kind with
746
747
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
748
749
750

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
751
752
753
754
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
755
756

  let restrict_1 rects pi1 =
757
758
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
759
760
761
762
    List.fold_left aux [] rects
  
  type normal = t

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

765
766
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
767
768
769
770
771
772
  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 ->
773
	  let gd = get_aux d in
774
	  let n = normal_aux gd in
775
776
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
777
778
	  memo := Memo.add d n !memo;
	  n
779

780
781
782
783
784
785
786
  let constraint_on_2 n t1 =
    List.fold_left 
      (fun accu (d1,d2) ->
	 if is_empty (cap d1 t1) then accu else cap accu d2)
      any
      n

787
788
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
789
  let is_empty d = d == []
790
end
791

792
793
module Print = 
struct
794
795
796
797
798
799
800
  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
801
802
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
803

804
  let print_const ppf = function
805
806
807
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
808

809
810
811
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
812
813
814
815
816
817
818
819
820
821

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

822
823
  let trivial_rec b = b == BoolRec.empty || b == BoolRec.full
  let trivial_pair b = b == BoolPair.empty || b == BoolPair.full
824
825

  let worth_abbrev d = 
826
827
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
828
829
830

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
831
    if not (DescrMap.mem d !named) then
832
833
      try 
	let r = DescrHash.find marks d in
834
	if (!r == None) && (worth_abbrev d) then 
835
836
837
838
839
	  let na = name () in 
	  r := Some na;
	  wh := (na,d) :: !wh
      with Not_found -> 
	DescrHash.add marks d (ref None);
840
841
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
842
843
	  (fun (n1,n2) -> mark n1; mark n2
(*
844
845
846
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
847
848
849
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
850
		  let l = get_record d1.record in
851
852
853
854
855
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
856
857
	       )
	       (Product.normal (descr n2))
858
*)
859
	  ) d.xml;
860
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
861
862
863
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
864
865
866
867
868

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
869
      let name = DescrMap.find d !named in
870
871
872
873
874
875
876
      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
877
	  Not_found -> assert false
878
  and real_print_descr ppf d = 
879
    if equal_descr d any then Format.fprintf ppf "Any" else
880
881
882
883
884
885
886
887
888
      (
	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 @
889
	   BoolRec.print "Record" print_record d.record
890
891
	  )
      )
892
893
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
894
  and print_xml ppf (t1,t2) =
895
896
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
897
898
899
900
901
902
903
904
905
    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
906
*)
907
908
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
909
910
911
912
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
913
    List.iter (fun (l,t) ->
914
		 let sep = if !first then (first := false; "") else ";" in
915
916
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
917
	      ) (LabelMap.get r);
918
919
    Format.fprintf ppf " %s}@]" o
(*
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
  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
937
*)
938
939
940

	  
  let end_print ppf =
941
    Format.fprintf ppf "@]";
942
943
944
945
946
947
948
949
950
951
    (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 "@]"
    );
952
(*    Format.fprintf ppf "@]"; *)
953
954
955
956
957
958
959
960
961
962
963
964
965
    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

966
let () = print_descr := Print.print_descr
967

968
969
module Positive =
struct
970
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
971
972
973
974
975
976
977
978
979
980
981
982
  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)
983
	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000

  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))
1001
  let xml d1 d2 = cons (`Xml (d1,d2))
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
  let define v1 v2 = def v1 (`Cup [v2]) 

  let solve v = internalize (make_node v)
end




(* Sample value *)
module Sample =
struct

1014

1015
1016
1017
1018
1019
let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
1020
1021
1022
  | Int of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
1023
1024
  | Pair of (t * t)
  | Xml of (t * t)
1025
  | Record of (bool * (label * t) list)
1026
  | Fun of (node * node) list
1027
  | Other
1028
 exception FoundSampleRecord of bool * (label * t) list
1029
1030
1031
1032
1033

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 ->
1034
    try Atom (Atoms.sample d.atoms) with 
1035
1036
	Not_found ->
(* Here: could create a fresh atom ... *)
1037
    try Char (Chars.sample d.chars) with Not_found ->
1038
    try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
1039
1040

    let memo = Assumptions.add d memo in
1041
1042
    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 ->
1043
    try sample_rec_record memo d.record with Not_found ->  
1044
1045
1046
1047
1048
1049
1050
1051
1052
    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 ->
1053
1054
(*TODO: check: is this correct ?  non_empty could return true
  but because of coinduction, the call to aux may raise Not_found, no ? *)
1055
1056
1057
1058
1059
        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
1060
    | [] -> (sample_rec memo accu1, sample_rec memo accu2)
1061
1062
1063
1064
1065
1066
1067
1068
  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

1069
1070
1071
1072
1073
1074
1075
1076
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
1077
  in
1078
1079
1080
1081
1082
1083
1084
1085
1086
  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
1087
1088
1089
1090
1091
1092
  else Fun left


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

1093
and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1094
1095
1096
1097
  let rec aux = function
    | [] -> 
	let l = ref labels and fields = ref [] in
	for i = 0 to Array.length left - 1 do
1098
	  fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1099
1100
	  l := List.tl !l
	done;
1101
	raise (FoundSampleRecord (oleft, List.rev !fields))
1102
    | (oright,right)::rights ->
1103
1104
1105
1106
1107
1108
	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
1109
	    if not (is_empty di) then (
1110
1111
1112
1113
1114
1115
1116
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  if exists (Array.length left) 
1117
    (fun i -> is_empty left.(i)) then raise Not_found;
1118
  try aux rights; raise Not_found
1119
  with FoundSampleRecord (o,r) -> (o,r)
1120
1121
1122
1123

	    


1124

1125
let get x = try sample_rec Assumptions.empty x with Not_found -> Other
1126

1127
1128
1129
1130
1131
1132
1133
  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
1134
1135
1136
    | Int i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
1137
    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
1138
    | Xml (Atom tag, Pair (attr, child)) -> 
1139
	Format.fprintf ppf "<%s %a>%a" (Atoms.value tag) print attr print child