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


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

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

15
module LabelPool = Pool.Make(HashedString)
16

17
type label = LabelPool.t
18

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

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

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

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
  let compare (x1,y1) (x2,y2) =
    if x1.id < x2.id then -1
    else if x1.id > x2.id then 1
    else y1.id - y2.id
  let equal (x1,y1) (x2,y2) = (x1==x2) && (y1==y2)
  let hash (x,y) = x.id + 17 * y.id
end 

module BoolPair = Boolean.Make(NodePair)

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

50
	       
51
let empty = { 
52
53
54
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
55
56
57
58
59
60
61
  record= Boolean.empty;
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
}
	      
let any =  {
62
63
64
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
65
66
67
68
69
70
71
72
  record= Boolean.full; 
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
}
	     
	     
let interval i = { empty with ints = i }
73
74
75
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) }
76
77
78
79
80
81
82
83
84
85
let record label opt t = 
  { empty with record = Boolean.atom (true,[label,(opt,t)]) }
let record' x =
  { empty with record = Boolean.atom x }
let atom a = { empty with atoms = a }
let char c = { empty with chars = c }
let constant = function
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
86
      
87
88
let cup x y = 
  if x == y then x else {
89
90
91
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
92
93
94
95
96
97
98
99
    record= Boolean.cup x.record y.record;
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
  }
    
let cap x y = 
  if x == y then x else {
100
101
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
102
    record= Boolean.cap x.record y.record;
103
    arrow = BoolPair.cap x.arrow y.arrow;
104
105
106
107
108
109
110
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
  }
    
let diff x y = 
  if x == y then empty else {
111
112
113
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
114
115
116
117
118
119
120
121
122
123
124
125
126
    record= Boolean.diff x.record y.record;
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
  }
    
let count = ref 0
let make () = incr count; { id = !count; descr = empty }
let define n d = n.descr <- d
let cons d = incr count; { id = !count; descr = d }
let descr n = n.descr
let internalize n = n
let id n = n.id
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183

let rec compare_rec r1 r2 =
  if r1 == r2 then 0
  else match (r1,r2) with
    | (l1,(o1,x1))::r1,(l2,(o2,x2))::r2 ->
	if ((l1:int) < l2) then -1 
	else if (l1 > l2) then 1 
	else if o2 && not o1 then -1
	else if o1 && not o2 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
184
185
186
187
	     
let rec equal_rec r1 r2 =
  (r1 == r2) ||
  match (r1,r2) with
188
    | (l1,(o1,x1))::r1,(l2,(o2,x2))::r2 ->
189
	(x1.id = x2.id) && (l1 == l2) && (o1 == o2) && (equal_rec r1 r2)
190
    | _ -> false
191
192
193
194
195
	
let rec equal_rec_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
196
197
	(o1 == o2) &&
	(equal_rec r1 r2) && (equal_rec_list l1 l2)
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
    | _ -> 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 =
228
229
230
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
231
232
233
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
234
  (equal_rec_bool a.record b.record)
235
236
237
238
239

let compare_descr a b =
  let c = compare a.atoms b.atoms in if c <> 0 then c
  else let c = compare a.chars b.chars in if c <> 0 then c
  else let c = compare a.ints b.ints in if c <> 0 then c
240
241
242
  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
243
244
245
246
247
248
249
250
251
252
253
  else let c = compare_rec_bool a.record b.record in if c <> 0 then c
  else 0

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


254
255
256
257
258
259
260
261
262
263
264
265
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
  | (l,(o,x))::rem ->
266
      let accu = if o then accu else accu + 5 in
267
268
269
270
271
      hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
  | [] -> accu + 5
      
let rec hash_rec_list accu = function
  | (o,r)::l ->
272
      hash_rec_list (hash_rec (if o then accu*3 else accu) r) l
273
274
275
276
277
278
279
280
281
  | [] -> 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 =
282
283
284
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
285
286
287
  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
288
289
  let accu = hash_rec_bool accu a.record in
  accu
290

291
292
293
294
295
296
297
298
299
module DescrHash = 
  Hashtbl.Make(
    struct 
      type t = descr
      let hash = hash_descr
      let equal = equal_descr
    end
  )

300
301
let print_descr = ref (fun _ _  -> assert false)

302
303
let neg x = diff any x

304
305
let any_node = cons any

306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
module LabelSet = Set.Make(LabelPool)

let get_record r =
  let labs accu (_,r) = 
    List.fold_left (fun accu (l,_) -> LabelSet.add l accu) accu r in
  let extend (opts,descrs) labs (o,r) =
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
	      | (l2,(o,x))::r when l1 = l2 -> 
		  descrs.(i) <- cap descrs.(i) (descr x);
		  opts.(i) <- opts.(i) && o;
		  aux (i+1) labs r
	      | r ->
		  if not o then descrs.(i) <- empty;
		  aux (i+1) labs r
    in
    aux 0 labs r;
    o
  in
  let line (p,n) =
    let labels = 
      List.fold_left labs (List.fold_left labs LabelSet.empty p) n in
    let labels = LabelSet.elements labels in
    let nlab = List.length labels in
    let mk () = Array.create nlab true, Array.create nlab any in

    let pos = mk () in
    let opos = List.fold_left 
		 (fun accu x -> 
		    (extend pos labels x) && accu)
		 true p in
    let p = (opos, pos) in

    let n = List.map (fun x ->
			let neg = mk () in
			let o = extend neg labels x in
			(o,neg)
		     ) n in
    (labels,p,n)
  in
  List.map line r
   
351

352
module DescrMap = Map.Make(struct type t = descr let compare = compare end)
353
354

let check d =
355
356
357
  BoolPair.check d.times;
  BoolPair.check d.xml;
  BoolPair.check d.arrow;
358
359
360
  Boolean.check d.record;
  ()

361
362
363
364
365
366
367
368
369
370
371
372
373


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

374
375
376
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

377
let trivially_empty d = equal_descr d empty
378

379
exception NotEmpty
380

381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
type slot = { mutable status : status; 
	       mutable notify : notify;
	       mutable active : bool }
and status = Empty | NEmpty | Maybe
and notify = Nothing | Do of slot * (slot -> unit) * notify

let memo = DescrHash.create 33000

let marks = ref [] 
let slot_empty = { status = Empty; active = false; notify = Nothing }
let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }

let rec notify = function
  | Nothing -> ()
  | Do (n,f,rem) -> 
      if n.status = Maybe then (try f n with NotEmpty -> ());
      notify rem

let rec iter_s s f = function
  | [] -> ()
  | arg::rem -> f arg s; iter_s s f rem


let set s =
  s.status <- NEmpty;
  notify s.notify;
  raise NotEmpty

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

420

421
let rec guard a f n =
422
423
424
425
  match slot a with
    | { status = Empty } -> ()
    | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
    | { status = NEmpty } -> f n
426
427
428
429
430
431
432
433
434
435

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars)) then slot_not_empty 
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
436
437
438
       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);
439
440
441
442
443
444
445
446
447
448
449
450
451
452
       iter_s s check_record (get_record d.record);
       if s.active then marks := s :: !marks else s.status <- Empty;
     with
	 NotEmpty -> ());
    s

and check_times (left,right) s =
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
	     aux accu1 accu2 right s
	else
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
453
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
454
455
456
457
    | [] -> set s
  in
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
458

459
460
461
462
463
464
465
466
467
468
469
470
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
471

472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
and check_record (labels,(oleft,(left_opt,left)),rights) s =
  let rec aux rights s = match rights with
    | [] -> set s
    | (oright,(right_opt,right))::rights ->
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
	       (not (left_opt.(i) && right_opt.(i))) &&
	       (trivially_empty (cap left.(i) right.(i))))
	in
	if next then aux rights s
	else
	  for i = 0 to Array.length left - 1 do
	    let back = left.(i) in
	    let oback = left_opt.(i) in
	    let odi = oback && (not right_opt.(i)) in
	    let di = diff back right.(i) in
	    if odi then (
	      left.(i) <- diff back right.(i);
	      left_opt.(i) <- odi;
	      aux rights s;
	      left.(i) <- back;
	      left_opt.(i) <- oback;
	    ) else
	      guard di (fun s ->
			  left.(i) <- diff back right.(i);
			  left_opt.(i) <- odi;
			  aux rights s;
			  left.(i) <- back;
			  left_opt.(i) <- oback;
		       ) s
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
      if left_opt.(i) then start (i - 1) s
      else guard left.(i) (start (i - 1)) s
  in
  start (Array.length left - 1) s


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

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

528
let rec empty_rec d =
529
  if not (Intervals.is_empty d.ints) then false
530
531
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
532
533
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
534
535
  else (
    let backup = !memo in
536
    memo := Assumptions.add d backup;
537
    if 
538
539
540
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
541
542
543
544
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
545
      DescrHash.add cache_false d ();
546
547
548
549
550
551
552
553
554
555
      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 ->
556
557
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
558
559
560
561
562
	  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
563
	  if not (empty_rec accu2') then aux accu1 accu2' right
564
565
566
567
568
    | [] -> 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)
569

570
571
572
573
574
575
576
577
578

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
579
          if not (empty_rec accu1') then aux accu1' accu2 left;
580
          let accu2' = cap_t accu2 t2 in
581
          if not (empty_rec accu2') then aux accu1 accu2' left
582
583
584
585
586
587
588
589
      | [] -> 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

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

623
and empty_rec_record c =
624
  List.for_all empty_rec_record_aux (get_record c)
625

626
627
(*
let is_empty d =
628
  empty_rec d
629
*)  
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657

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*) 
658
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
	      
	      let i = cap t1 d1 in
	      if is_empty i then loop t1 t2 l
	      else (
		r := (i, cup t2 d2);
		let k = diff d1 t1 in 
		if non_empty k then res := (ref (k,d2)) :: !res;
		
		let j = diff t1 d1 in 
		if non_empty j then loop j t2 l
	      )
      in
      loop t1 t2 !res
    in
    List.iter add d;
    List.map (!) !res

676
(*
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
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)

705
*)
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
  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
    List.iter line d;
    !accu
727
728
729
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
730

731

732
733
  let get ?(kind=`Normal) d = 
    match kind with
734
735
      | `Normal -> get_aux (BoolPair.get d.times)
      | `XML -> get_aux (BoolPair.get d.xml)
736
737
738
739
740
741
742
743
744
745
746

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty

  let restrict_1 rects pi1 =
    let aux accu (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in
    List.fold_left aux [] rects
  
  type normal = t

747
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
748
749
750
751
752
753
754
755


  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 ->
756
	  let gd = get_aux (BoolPair.get d) in
757
	  let n = normal_aux gd in
758
759
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
760
761
	  memo := Memo.add d n !memo;
	  n
762

763
764
765
766
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
767

768
769
module Print = 
struct
770
771
772
773
774
775
776
  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
777
778
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
779

780
  let print_const ppf = function
781
782
783
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
784

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

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

  let trivial b = b = Boolean.empty || b = Boolean.full
799
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
800
801

  let worth_abbrev d = 
802
    not (trivial_pair d.times && trivial_pair d.xml && trivial_pair d.arrow && trivial d.record) 
803
804
805

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
806
    if not (DescrMap.mem d !named) then
807
808
809
810
811
812
813
814
      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);
815
816
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
817
818
	  (fun (n1,n2) -> mark n1; mark n2
(*
819
820
821
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
822
823
824
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
825
		  let l = get_record d1.record in
826
827
828
829
830
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
831
832
	       )
	       (Product.normal (descr n2))
833
*)
834
	  ) d.xml;
835
836
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
    	Boolean.iter (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) d.record
837
838
839
840
841

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

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

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

   let print ppf n = print_descr ppf (descr n)

end

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

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


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

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

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

  let solve v = internalize (make_node v)
end




(* Sample value *)
module Sample =
struct

981

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

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

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

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


and sample_rec_times memo c = 
  find (sample_rec_times_aux memo) c

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

and sample_rec_arrow c =
  find sample_rec_arrow_aux c

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

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

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


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

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

	    


1096

1097
let get x = try sample_rec Assumptions.empty x with Not_found -> Other
1098

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



module Record = 
struct
1138
1139
1140
1141
1142
  type atom = bool * (label, (bool * node)) SortedMap.t
  type t = atom Boolean.t

  let get d = d.record

1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
  module T = struct
    type t = descr
    let any = any
    let cap = cap
    let cup = cup
    let diff = diff
    let empty = is_empty
  end
  module R = struct
    (*Note: Boolean.cap,cup,diff would be ok,
      but we add here the simplification rules:
      { } & r --> r    ; { } | r -> { }
      r \ { } --> Empty *)

    type t = atom Boolean.t
    let any = Boolean.full
    let cap =  Boolean.cap
    let cup = Boolean.cup
    let diff = Boolean.diff
    let empty x = is_empty { empty with record = x }
  end
  module TR = Normal.Make(T)(R)

  let atom = function
    | (true,[]) -> Boolean.full
    | (o,l) -> Boolean.atom (o,l)

1170
1171
1172
1173
1174
1175
  let somefield_possible t =
    not (R.empty (R.diff t (Boolean.atom (false,[]))))

  let nofield_possible t =    
    not (R.empty (R.cap t (Boolean.atom (false,[]))))

1176
1177
  let restrict_label_absent t l =
    Boolean.compute_bool
1178
      (fun ((o,r) as x) ->
1179
1180
	 try
	   let (lo,_) = List.assoc l r in
1181
	   if lo then atom (o,SortedMap.diff r [l])
1182
1183
1184
1185
1186
1187
1188
1189
1190
	   else Boolean.empty
	 with Not_found -> Boolean.atom x
      )
      t

  let restrict_field t l d =
    (* Is it correct ?  Do we need to keep track of "first component"
       (value of l) as in label_present, then filter at the end ... ? *)
    Boolean.compute_bool
1191
      (fun ((o,r) as x) ->
1192
1193
1194
	 try
	   let (lo,lt) = List.assoc l r in
	   if (not lo) && (is_empty (cap d (descr lt))) then Boolean.empty
1195
	   else atom (o, SortedMap.diff r [l])
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
	 with Not_found -> 
	   if o then Boolean.atom x else Boolean.empty
      )
      t



  let label_present (t:t) l : (descr * t) list =
    let x =
      Boolean.compute_bool
1206
	(fun ((o,r) as x) ->
1207
1208
	   try
	     let (_,lt) = List.assoc l r in
1209
	     Boolean.atom (descr lt, atom (o, SortedMap.diff r [l]))
1210
1211
1212
1213
1214
1215
1216
1217
	   with Not_found -> 
	     if o then Boolean.atom (any, Boolean.atom x) else Boolean.empty
	)
	t
    in
    TR.boolean x

  let restrict_label_present t l =
1218
    Boolean.compute_bool
1219
      (fun ((o,r) as x) ->
1220
1221
1222
1223
1224
1225
1226
1227
	 try
	   Boolean.atom (o, SortedMap.change_exists l (fun (_,lt) -> (false,lt)) r)
	 with Not_found -> 
	   if o then Boolean.atom 
	     (true, SortedMap.union_disj [l, (false,any_node)] r)
	   else Boolean.empty
      )
      t
1228
1229
1230
1231
1232
1233
1234

  let project_field t l =
    let r = label_present t l in
    List.fold_left (fun accu (d,_) -> cup accu d) empty r

  let project t l =
    let t = get t in
1235
1236
1237
    let r = label_present t l in
    if r = [] then raise Not_found else
      List.fold_left (fun accu (d,_) -> cup accu d) empty r
1238
1239
1240
1241
	   
  type normal = 
      [ `Success
      | `Fail
1242
1243
      | `NoField
      | `SomeField
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
      | `Label of label * (descr * normal) list * normal ]

  let first_label t =
    let min = ref None in
    let lab l = match !min with 
      | Some l' when l >= l' -> () 
      | _ -> min := Some l in
    let aux = function
      | _,[] -> ()
      | _,(l,_)::_ -> lab l in
    Boolean.iter aux t;
    match !min with
      | Some l -> `Label l
      | None -> 
	  let n = 
	    Boolean.compute
	      ~empty:0
	      ~full:3
	      ~cup:(lor)
	      ~cap:(land)
	      ~diff:(fun a b -> a land lnot b)
	      ~atom:(function (true,[]) -> 3 | (false,[]) -> 1 | _ -> assert false)
	      t in
	  match n with
	    | 0 -> `Fail
	    | 1 -> `NoField
	    | 2 -> `SomeField
	    | _ -> `Success


1274
1275
1276
1277
1278
  let normal' t l = 
    let present = label_present t l
    and absent = restrict_label_absent t l in
    List.map (fun (d,t) -> d,t) present, absent

1279
1280
1281
1282
1283
1284
1285
1286
1287
  let rec normal_aux t =
    match first_label t with
      | `Label l ->
	  let present = label_present t l
	  and absent = restrict_label_absent t l in
	  `Label (l, List.map (fun (d,t) -> d, normal_aux t) present,
		  normal_aux absent)
      | `Fail -> `Fail
      | `Success -> `Success
1288
1289
      | `NoField -> `NoField
      | `SomeField -> `SomeField
1290
1291
1292
1293
1294
1295
1296
1297
1298

  let normal t = normal_aux (get t)
    


  let descr x = { empty with record = x }
  let is_empty x = is_empty (descr x)
(*

1299
1300
1301
1302
1303
1304
1305
  type t = (label, (bool * descr)) SortedMap.t list

  let get d =
    let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in
    List.filter line (get_record d.record)

  let restrict_label_present t l =
1306
1307
1308
1309
1310
1311
1312
    let restr = function 
      | (true, d) -> if non_empty d then (false,d) else raise Exit 
      | x -> x in
    let aux accu r =  
      try SortedMap.change l restr (false,any) r :: accu
      with Exit -> accu in
    List.fold_left aux [] t
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337

  let restrict_label_absent t l =
    let restr = function (true, _) -> (true,empty) | _ -> raise Exit in
    let aux accu r =  
      try SortedMap.change l restr (true,empty) r :: accu
      with Exit -> accu in
    List.fold_left aux [] t

  let restrict_field t l d =
    let restr (_,d1) = 
      let d1 = cap d d1 in 
      if is_empty d1 then raise Exit else (false,d1) in
    let aux accu r = 
      try SortedMap.change l restr (false,d) r :: accu 
      with Exit -> accu in
    List.fold_left aux [] t

  let project_field t l =
    let aux accu x =
      match List.assoc l x with
	| (false,t) -> cup accu t
	| _ -> raise Not_found
    in
    List.fold_left aux empty t

1338
1339
1340
  let project d l =
    project_field (get_record d.record) l

1341
1342
1343
1344
1345
1346
1347
1348
1349
  type normal = 
      [ `Success
      | `Fail
      | `Label of label * (descr * normal) list * normal ]

  let rec merge_record n r =
    match (n, r) with
      | (`Success, _) | (_, []) -> `Success
      | (`Fail, r) ->
1350
1351
	  let aux (l,(o,t)) n = 
	    `Label (l, [t,n], if o then n else `Fail) in
1352
1353
1354
1355
	  List.fold_right aux r `Success
      | (`Label (l1,present,absent), (l2,(o,t2))::r') ->
	  if (l1 < l2) then
	    let pr =  List.map (fun (t,x) -> (t, merge_record x r)) present in
1356
1357
1358
1359
	    let t = List.fold_left (fun a (t,_) -> diff a t) any present in
	    let pr = 
	      if non_empty t then (t, merge_record `Fail r) :: pr
	      else pr in
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
	    `Label (l1,pr,merge_record absent r)
	  else if (l2 < l1) then
	    let n' = merge_record n r' in
	    `Label (l2, [t2, n'], if o then n' else n)
	  else
	    let res = ref [] in
	    let aux a (t,x) = 
	      (let t = diff t t2 in 
	       if non_empty t then res := (t,x) :: !res);
	      (let t = cap t t2 in
	       if non_empty t then res := (t, merge_record x r') :: !res);
	      diff a t 
	    in
	    let t2 = List.fold_left aux t2 present in
	    let () = 
	      if non_empty t2 then 
	      res := (t2, merge_record `Fail r') :: !res in
	    let abs = if o then merge_record absent r' else absent in
	    `Label (l1, !res, abs)

1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
  module Unify = Map.Make(struct type t = normal let compare = compare end)

  let repository = ref Unify.empty

  let rec canonize = function
    | `Label (l,pr,ab) as x ->
	(try Unify.find x !repository 
	 with Not_found -> 
	   let pr = List.map (fun (t,n) -> canonize n,t) pr in
	   let pr = SortedMap.from_list cup pr in
	   let pr = List.map (fun (n,t) -> (t,n)) pr in
	   let x = `Label (l, pr, canonize ab) in
	   try Unify.find x !repository
	   with Not_found -> repository := Unify.add x x !repository; x
	)
    | x -> x
1396
1397

  let normal d =
1398
1399
1400
    let r = canonize (List.fold_left merge_record `Fail (get d)) in
    repository := Unify.empty;
    r
1401

1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
  type normal' =
      [ `Success
      | `Label of label * (descr * descr) list * descr option ] option

(* NOTE: this function relies on the fact that generic order
         makes smallest labels appear first *)

  let first_label d =
    let d = d.record in
    let min = ref None in
    let lab (l,o,t) = match !min with 
      | Some l' when l >= l' -> () 
      | _ -> if o && (descr t = any) then () else min := Some l in
    let line (p,n) =
      (match p with f::_ -> lab f | _ -> ());
      (match n with f::_ -> lab f | _ -> ()) in
    List.iter line d;
    match !min with
      | None -> if d = [] then `Empty else `Any
      | Some l -> `Label l

  let normal' (d : descr) l =
    let ab = ref empty in
    let rec extract f = function
      | (l',o,t) :: rem when l = l' -> 
	  f o (descr t); extract f rem
      | x :: rem -> x :: (extract f rem)
      | [] -> [] in
    let line (p,n) =
      let ao = ref true and ad = ref any in
      let p = 
	extract (fun o d -> ao := !ao && o; ad := cap !ad d) p
      and n = 
	extract (fun o d -> ao := !ao && not o; ad := diff !ad d) n
      in
      (* Note: p and n are still sorted *)
      let d = { empty with record = [(p,n)] } in
      if !ao then ab := cup d !ab;
      (!ad, d) in
    let pr = List.map line d.record in
    let pr = Product.normal_aux pr in
    let ab = if is_empty !ab then None else Some !ab in
    (pr, ab)
	    
1446
*)
1447
1448

  let any = { empty with record = any.record }
1449
(*
1450
  let is_empty d = d = []
1451
1452
1453
  let descr l =
    let line l = map_sort (fun (l,(o,d)) -> (l,o,cons d)) l, [] in 
    { empty with record = map_sort line l }
1454
*)
1455
1456
1457
1458
end



1459
let memo_normalize = ref DescrMap.empty
1460
1461
1462


let rec rec_normalize d =
1463
  try DescrMap.find d !memo_normalize
1464
1465
  with Not_found ->
    let n = make () in
1466
    memo_normalize := DescrMap.add d n !memo_normalize;
1467
    let times = 
1468
1469
1470
      List.fold_left 
	(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
	BoolPair.empty (Product.normal d)
1471
    in
1472
    let xml = 
1473
1474
1475
      List.fold_left 
	(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
	BoolPair.empty (Product.normal ~kind:`XML d)
1476
    in
1477
1478
    let record = d.record
(*