patterns.ml 69 KB
Newer Older
1
exception Error of string
2
open Ident
3

4
5
6
7
8
let print_lab ppf l = 
  if (l == LabelPool.dummy_max) 
  then Format.fprintf ppf "<dummy_max>"
  else Label.print ppf (LabelPool.value l)

9
10
11
(*
To be sure not to use generic comparison ...
*)
12
13
14
15
16
17
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1

18

19
(* Syntactic algebra *)
20
(* Constraint: any node except Constr has fv<>[] ... *)
21
type d =
22
  | Constr of Types.t
23
  | Cup of descr * descr
24
  | Cap of descr * descr
25
  | Times of node * node
26
  | Xml of node * node
27
  | Record of label * node
28
29
  | Capture of id
  | Constant of id * Types.const
30
  | Dummy
31
32
and node = {
  id : int;
33
  mutable descr : descr;
34
  accept : Types.Node.t;
35
  fv : fv
36
37
38
} and descr = Types.t * fv * d


39

40
let id x = x.id
41
let descr x = x.descr
42
43
let fv x = x.fv
let accept x = Types.internalize x.accept
44
45
46

let printed = ref []
let to_print = ref []
47
let rec print ppf (a,_,d) = 
48
  match d with
49
    | Constr t -> Types.Print.print ppf t
50
51
52
53
54
55
56
57
58
    | Cup (p1,p2) -> Format.fprintf ppf "(%a | %a)" print p1 print p2
    | Cap (p1,p2) -> Format.fprintf ppf "(%a & %a)" print p1 print p2
    | Times (n1,n2) -> 
	Format.fprintf ppf "(P%i,P%i)" n1.id n2.id;
	to_print := n1 :: n2 :: !to_print
    | Xml (n1,n2) -> 
	Format.fprintf ppf "XML(P%i,P%i)" n1.id n2.id;
	to_print := n1 :: n2 :: !to_print
    | Record (l,n) -> 
59
	Format.fprintf ppf "{ %a =  P%i }" Label.print (LabelPool.value l) n.id;
60
61
	to_print := n :: !to_print
    | Capture x ->
62
	Format.fprintf ppf "%a" Ident.print x
63
    | Constant (x,c) ->
64
	Format.fprintf ppf "(%a := %a)" Ident.print x
65
	  Types.Print.print_const c
66
67
    | Dummy ->
	Format.fprintf ppf "*DUMMY*"
68

69
let dump_print ppf =
70
  while !to_print != [] do
71
72
73
74
75
76
77
78
79
80
81
    let p = List.hd !to_print in
    to_print := List.tl !to_print;
    if not (List.mem p.id !printed) then
      ( printed := p.id :: !printed;
	Format.fprintf ppf "P%i:=%a\n" p.id print (descr p)
      )
  done

let print ppf d =
  Format.fprintf ppf "%a@\n" print d;
  dump_print ppf
82

83
84
85
86
87
let print_node ppf n =
  Format.fprintf ppf "P%i" n.id;
  to_print := n :: !to_print;
  dump_print ppf

88

89
90
let counter = State.ref "Patterns.counter" 0

91
let dummy = (Types.empty,IdSet.empty,Dummy)
92
93
let make fv =
  incr counter;
94
  { id = !counter; descr = dummy; accept = Types.make (); fv = fv }
95
96

let define x ((accept,fv,_) as d) =
97
  (* assert (x.fv = fv); *)
98
  Types.define x.accept accept;
99
  x.descr <- d
100

101
102
103
104
105
let cons fv d =
  let q = make fv in
  define q d;
  q

106
let constr x = (x,IdSet.empty,Constr x)
107
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
108
109
110
111
112
  if not (IdSet.equal fv1 fv2) then (
    let x = match IdSet.pick (IdSet.diff fv1 fv2) with
      | Some x -> x
      | None -> match IdSet.pick (IdSet.diff fv2 fv1) with Some x -> x 
	  | None -> assert false
113
114
115
    in
    raise 
      (Error 
116
	 ("The capture variable " ^ (Ident.to_string x) ^ 
117
118
	  " should appear on both side of this | pattern"))
  );
119
  (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
120
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
121
122
123
  if not (IdSet.disjoint fv1 fv2) then (
    match IdSet.pick (IdSet.cap fv1 fv2) with
      | Some x -> 
124
125
	  raise 
	  (Error 
126
	     ("The capture variable " ^ (Ident.to_string x) ^ 
127
	      " cannot appear on both side of this & pattern"))
128
      | None -> assert false
129
  );
130
  (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2))
131
let times x y =
132
  (Types.times x.accept y.accept, IdSet.cup x.fv y.fv, Times (x,y))
133
let xml x y =
134
  (Types.xml x.accept y.accept, IdSet.cup x.fv y.fv, Xml (x,y))
135
let record l x = 
136
  (Types.record l x.accept, x.fv, Record (l,x))
137
138
let capture x = (Types.any, IdSet.singleton x, Capture x)
let constant x c = (Types.any, IdSet.singleton x, Constant (x,c))
139
140


141
142
let print_node = ref (fun _ _ -> assert false)

143
144
145
146
147
148
module Node = struct
  type t = node
  let compare n1 n2 = n1.id - n2.id
  let equal n1 n2 = n1.id == n2.id
  let hash n = n.id

149
  let check n = ()
150
  let dump ppf x = !print_node ppf x
151

152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208

  module SMemo = Set.Make(Custom.Int)
  let memo = Serialize.Put.mk_property (fun t -> ref SMemo.empty)
  let rec serialize t n = 
    let l = Serialize.Put.get_property memo t in
    Serialize.Put.int t n.id;
    if not (SMemo.mem n.id !l) then (
      l := SMemo.add n.id !l;
      Types.Node.serialize t n.accept;
      IdSet.serialize t n.fv;
      serialize_descr t n.descr
    )
  and serialize_descr s (_,_,d) =
    serialize_d s d
  and serialize_d s = function
    | Constr t ->
	Serialize.Put.bits 3 s 0;
	Types.serialize s t
    | Cup (p1,p2) ->
	Serialize.Put.bits 3 s 1;
	serialize_descr s p1; 
	serialize_descr s p2
    | Cap (p1,p2) ->
	Serialize.Put.bits 3 s 2;
	serialize_descr s p1; 
	serialize_descr s p2
    | Times (p1,p2) ->
	Serialize.Put.bits 3 s 3;
	serialize s p1;
	serialize s p2
    | Xml (p1,p2) ->
	Serialize.Put.bits 3 s 4;
	serialize s p1;
	serialize s p2
    | Record (l,p) ->
	Serialize.Put.bits 3 s 5;
	LabelPool.serialize s l;
	serialize s p
    | Capture x ->
	Serialize.Put.bits 3 s 6;
	Id.serialize s x
    | Constant (x,c) ->
	Serialize.Put.bits 3 s 7;
	Id.serialize s x;
	Types.Const.serialize s c
    | Dummy -> assert false

  module DMemo = Map.Make(Custom.Int)
  let memo = Serialize.Get.mk_property (fun t -> ref DMemo.empty)
  let rec deserialize t = 
    let l = Serialize.Get.get_property memo t in
    let id = Serialize.Get.int t in
    try DMemo.find id !l
    with Not_found ->
      let accept = Types.Node.deserialize t in
      let fv = IdSet.deserialize t in
      incr counter;
209
      let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
      l := DMemo.add id n !l;
      n.descr <- deserialize_descr t;
      n
  and deserialize_descr s =
    match Serialize.Get.bits 3 s with
      | 0 -> constr (Types.deserialize s)
      | 1 ->
	  (* Avoid unnecessary tests *)
	  let (acc1,fv1,_) as x1 = deserialize_descr s in
	  let (acc2,fv2,_) as x2 = deserialize_descr s in
	  (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
      | 2 ->
	  let (acc1,fv1,_) as x1 = deserialize_descr s in
	  let (acc2,fv2,_) as x2 = deserialize_descr s in
	  (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2))
      | 3 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  times x y
      | 4 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  xml x y
      | 5 ->
	  let l = LabelPool.deserialize s in
	  let x = deserialize s in
	  record l x
      | 6 -> capture (Id.deserialize s)
      | 7 ->
	  let x = Id.deserialize s in
	  let c = Types.Const.deserialize s in
	  constant x c
      | _ -> assert false


end
246

247
248
(* Pretty-print *)

249
module Pat = struct
250
  type t = descr
251
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
    match (d1,d2) with
      | Constr t1, Constr t2 -> Types.compare t1 t2
      | Constr _, _ -> -1 | _, Constr _ -> 1

      | Cup (x1,y1), Cup (x2,y2) | Cap (x1,y1), Cap (x2,y2) ->
	  let c = compare x1 x2 in if c <> 0 then c 
	  else compare y1 y2
      | Cup _, _ -> -1 | _, Cup _ -> 1
      | Cap _, _ -> -1 | _, Cap _ -> 1

      | Times (x1,y1), Times (x2,y2) | Xml (x1,y1), Xml (x2,y2) ->
	  let c = Node.compare x1 x2 in if c <> 0 then c
	  else Node.compare y1 y2
      | Times _, _ -> -1 | _, Times _ -> 1
      | Xml _, _ -> -1 | _, Xml _ -> 1

      | Record (x1,y1), Record (x2,y2) ->
	  let c = LabelPool.compare x1 x2 in if c <> 0 then c
	  else Node.compare y1 y2
      | Record _, _ -> -1 | _, Record _ -> 1

      | Capture x1, Capture x2 ->
	  Id.compare x1 x2
      | Capture _, _ -> -1 | _, Capture _ -> 1

      | Constant (x1,y1), Constant (x2,y2) ->
	  let c = Id.compare x1 x2 in if c <> 0 then c
	  else Types.Const.compare y1 y2
      | Constant _, _ -> -1 | _, Constant _ -> 1

      | Dummy, Dummy -> assert false
283
284
285
286
287
288
289
290
291
292
293
294
295

  let equal p1 p2 = compare p1 p2 == 0

  let rec hash (_,_,d) = match d with
    | Constr t -> 1 + 17 * (Types.hash t)
    | Cup (p1,p2) -> 2 + 17 * (hash p1) + 257 * (hash p2)
    | Cap (p1,p2) -> 3 + 17 * (hash p1) + 257 * (hash p2)
    | Times (q1,q2) -> 4 + 17 * q1.id + 257 * q2.id
    | Xml (q1,q2) -> 5 + 17 * q1.id + 257 * q2.id
    | Record (l,q) -> 6 + 17 * (LabelPool.hash l) + 257 * q.id
    | Capture x -> 7 + (Id.hash x)
    | Constant (x,c) -> 8 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
    | Dummy -> assert false
296
297
298
299
300

  let serialize _ _ = assert false
  let deserialize _ = assert false
  let check _ = assert false
  let dump _ = assert false
301
302
303
end

module Print = struct
304
305
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
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

  let names = ref M.empty
  let printed = ref S.empty
  let toprint = Queue.create ()
  let id = ref 0

  let rec mark seen ((_,_,d) as p) =
    if (M.mem p !names) then ()
    else if (S.mem p seen) then
      (incr id;
       names := M.add p !id !names;
       Queue.add p toprint)
    else 
      let seen = S.add p seen in
      match d with
	| Cup (p1,p2) | Cap (p1,p2) -> mark seen p1; mark seen p2
	| Times (q1,q2) | Xml (q1,q2) -> mark seen q1.descr; mark seen q2.descr
	| Record (_,q) -> mark seen q.descr
	| _ -> ()

  let rec print ppf p =
    try 
      let i = M.find p !names in
      Format.fprintf ppf "P%i" i
    with Not_found ->
      real_print ppf p
  and real_print ppf (_,_,d) =  match d with
    | Constr t ->
	Types.Print.print ppf t
    | Cup (p1,p2) ->
	Format.fprintf ppf "(%a | %a)" print p1 print p2
    | Cap (p1,p2) ->
	Format.fprintf ppf "(%a & %a)" print p1 print p2
    | Times (q1,q2) ->
	Format.fprintf ppf "(%a,%a)" print q1.descr print q2.descr
    | Xml (q1,{ descr = (_,_,Times(q2,q3)) }) ->
342
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q3.descr
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
    | Xml _ -> assert false
    | Record (l,q) ->
	Format.fprintf ppf "{%a=%a}" Label.print (LabelPool.value l) print q.descr
    | Capture x ->
	Format.fprintf ppf "%a" Ident.print x
    | Constant (x,c) ->
	Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.print_const c
    | Dummy -> assert false
      
  let print ppf p =
    mark S.empty p;
    print ppf p;
    let first = ref true in
    (try while true do
       let p = Queue.pop toprint in
       if not (S.mem p !printed) then 
	 ( printed := S.add p !printed;
	   Format.fprintf ppf " %s@ @[%a=%a@]"
	     (if !first then (first := false; "where") else "and")
	     print p
	     real_print p
	);
     done with Queue.Empty -> ());
    id := 0;
    names := M.empty;
    printed := S.empty
369
370
371
372
373
374
375
376
377
378
379


  let print_xs ppf xs =
    Format.fprintf ppf "{";
    let rec aux = function
      | [] -> ()
      | [x] -> Ident.print ppf x
      | x::q -> Ident.print ppf x; Format.fprintf ppf ","; aux q
    in
    aux xs;
    Format.fprintf ppf "}"
380
381
end

382
let () = print_node := (fun ppf n -> Print.print ppf (descr n))
383

384
385
386
387

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
388
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
389
390
let times_res v1 v2 = Types.Positive.times v1 v2

391
(* Try with a hash-table *)
392
module MemoFilter = Map.Make 
393
  (struct 
394
     type t = Types.t * node 
395
396
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
397
       Types.compare t1 t2
398
   end)
399
400
401

let memo_filter = ref MemoFilter.empty

402
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
403
(* TODO: avoid is_empty t when t is not changing (Cap) *)
404
405
406
407
  if Types.is_empty t 
  then empty_res fv
  else
    match d with
408
      | Constr _ -> IdMap.empty
409
      | Cup ((a,_,_) as d1,d2) ->
410
	  IdMap.merge cup_res
411
412
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
413
      | Cap (d1,d2) ->
414
	  IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
415
416
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
417
418
419
      | Record (l,p) ->
	  filter_node (Types.Record.project t l) p
      | Capture c ->
420
	  IdMap.singleton c (Types.Positive.ty t)
421
      | Constant (c, cst) ->
422
	  IdMap.singleton c (Types.Positive.ty (Types.constant cst))
423
      | Dummy -> assert false
424

425
426
427
428
and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
429
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
430
       in
431
       IdMap.merge cup_res accu term
432
433
434
435
436
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)


437
and filter_node t p : Types.Positive.v id_map =
438
439
440
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
    let (_,fv,_) as d = descr p in
441
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
442
443
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
444
    IdMap.collide Types.Positive.define res r;
445
446
447
448
449
    r

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
450
  IdMap.map Types.Positive.solve r
451
452
453
454
455
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

456

457
458
459
(* Factorization of capture variables and constant patterns *)

module Factorize = struct
460
461
  module NodeTypeSet = Set.Make(Custom.Pair(Node)(Types))

462
463
464
465
466
467
468
469
470
471
472
473
474
475
  let pi1 ~kind t = Types.Product.pi1 (Types.Product.get ~kind t)
  let pi2 ~kind t = Types.Product.pi2 (Types.Product.get ~kind t)

(* Note: this is incomplete because of non-atomic constant patterns:
# debug approx (_,(x:=(1,2))) (1,2);;
[DEBUG:approx]
x=(1,2)
*)
  let rec approx_var seen ((a,fv,d) as p) t xs =
(*    assert (Types.subtype t a); 
      assert (IdSet.subset xs fv); *)
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
476
	  approx_var seen p2 (Types.diff t a1)
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
	    (approx_var seen p1 (Types.cap t a1) xs) 
      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
	  IdSet.cup
	    (approx_var seen p1 t (IdSet.cap fv1 xs))
	    (approx_var seen p2 t (IdSet.cap fv2 xs))
      | Capture _ ->
	  xs
      | Constant (_,c) -> 
	  if (Types.subtype t (Types.constant c)) then xs else IdSet.empty
      | Times (q1,q2) ->
	  let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
	  IdSet.cap
	    (approx_var_node seen q1 (pi1 ~kind:`Normal t) xs)
	    (approx_var_node seen q2 (pi2 ~kind:`Normal t) xs)
      | Xml (q1,q2) ->
	  let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
	  IdSet.cap
	    (approx_var_node seen q1 (pi1 ~kind:`XML t) xs)
	    (approx_var_node seen q2 (pi2 ~kind:`XML t) xs)
      | Record _ -> IdSet.empty
      | _ -> assert false
	  
  and approx_var_node seen q t xs =
500
    if (NodeTypeSet.mem (q,t) seen) 
501
    then xs
502
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
503
      
504
505

(* Obviously not complete ! *)      
506
  let rec approx_nil seen ((a,fv,d) as p) t xs =
507
508
    assert (Types.subtype t a); 
    assert (IdSet.subset xs fv);
509
510
511
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
512
	  approx_nil seen p2 (Types.diff t a1)
513
514
515
516
517
518
519
520
521
522
523
524
	    (approx_nil seen p1 (Types.cap t a1) xs) 
      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
	  IdSet.cup
	    (approx_nil seen p1 t (IdSet.cap fv1 xs))
	    (approx_nil seen p2 t (IdSet.cap fv2 xs))
      | Constant (_,c) when Types.Const.equal c Sequence.nil_cst -> xs
      | Times (q1,q2) ->
	  let xs = IdSet.cap q2.fv (IdSet.diff xs q1.fv) in
	  approx_nil_node seen q2 (pi2 ~kind:`Normal t) xs
      | _ -> IdSet.empty
	  
  and approx_nil_node seen q t xs =
525
    if (NodeTypeSet.mem (q,t) seen) 
526
    then xs
527
    else approx_nil (NodeTypeSet.add (q,t) seen) q.descr t xs
528
529
530
531
532
533
534
535
536
537
538
539
540
541

  let cst ((a,_,_) as p) t xs =
    if IdSet.is_empty xs then IdMap.empty
    else
      let rec aux accu (x,t) =
	if (IdSet.mem xs x) then
	  match Sample.single_opt (Types.descr t) with
	    | Some c -> (x,c)::accu
	    | None -> accu
	else accu in
      let t = Types.cap t a in
      IdMap.from_list_disj (List.fold_left aux [] (filter_descr t p))
	
  let var ((a,_,_) as p) t = 
542
    approx_var NodeTypeSet.empty p (Types.cap t a)
543
544

  let nil ((a,_,_) as p) t = 
545
    approx_nil NodeTypeSet.empty p (Types.cap t a)
546
547
548
549
550
end




551
552
(* Normal forms for patterns and compilation *)

553
554
let min (a:int) (b:int) = if a < b then a else b

555
556
let any_basic = Types.Record.or_absent Types.non_constructed

557
558
559
560
561
562
563
564
565
let rec first_label (acc,fv,d) =
  if Types.is_empty acc 
  then LabelPool.dummy_max
  else match d with
    | Constr t -> Types.Record.first_label t
    | Cap (p,q) -> min (first_label p) (first_label q)
    | Cup ((acc1,_,_) as p,q) -> min (first_label p) (first_label q)
    | Record (l,p) -> l
    | _ -> LabelPool.dummy_max
566

567
module Normal = struct
568

569
  type source = SCatch | SConst of Types.const 
570
  type result = source id_map
571

572
573
574
575
  let compare_source s1 s2 =
    if s1 == s2 then 0 
    else match (s1,s2) with
      | SCatch, _ -> -1 | _, SCatch -> 1
576
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
577

578
(*
579
580
  let hash_source = function
    | SCatch -> 1
581
    | SConst c -> Types.Const.hash c
582
*)
583
584
585
586
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

587
588
589
590
591
  module ResultMap = Map.Make(struct
				type t = result
				let compare = compare_result
			      end)

592
  module NodeSet = SortedList.Make(Node)
593

594
  module Nnf = struct
595
596
    include Custom.Dummy

597
598
599
600
601
602
603
604
605
606
607
608
609
610
    type t = NodeSet.t * Types.t * IdSet.t (* pl,t;   t <= \accept{pl} *)
	
    let check (pl,t,xs) =
      List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
	(NodeSet.get pl)
    let print ppf (pl,t,xs) =
      Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t
    let compare (l1,t1,xs1) (l2,t2,xs2) =
      let c = NodeSet.compare l1 l2 in if c <> 0 then c
      else let c = Types.compare t1 t2 in if c <> 0 then c
      else IdSet.compare xs1 xs2
    let hash (l,t,xs) = 
      (NodeSet.hash l) + 17 * (Types.hash t) + 257 * (IdSet.hash xs)
    let equal x y = compare x y == 0
611
612
613
614
615
616
617


    let first_label (pl,t,xs) = 
      List.fold_left
	(fun l p -> min l (first_label (descr p)))
	(Types.Record.first_label t)
	pl
618
619


620
  end
621

622
623
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
624

625
626
627
628
629
    let compare (r1,x1,y1) (r2,x2,y2) =
      let c = compare_result r1 r2 in if c <> 0 then c
      else let c = Nnf.compare x1 x2 in if c <> 0 then c
      else Nnf.compare y1 y2
  end
630

631
  module NLineProd = Set.Make(NProd)
632

633
  type record =
634
    | RecNolabel of result option * result option
635
    | RecLabel of label * NLineProd.t
636
  type t = {
637
638
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
639
    nrecord: record
640
641
  }

642
  let fus = IdMap.union_disj
643

644
  let nempty lab = 
645
    { nprod = NLineProd.empty; 
646
      nxml = NLineProd.empty;
647
      nrecord = (match lab with 
648
		   | Some l -> RecLabel (l,NLineProd.empty)
649
		   | None -> RecNolabel (None,None))
650
    }
651
  let dummy = nempty None
652
653
654


  let ncup nf1 nf2 = 
655
    { nprod   = NLineProd.union nf1.nprod nf2.nprod;
656
      nxml    = NLineProd.union nf1.nxml nf2.nxml;
657
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
658
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
659
		       (* assert (l1 = l2); *) 
660
		       RecLabel (l1, NLineProd.union r1 r2)
661
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
662
663
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
664
		   | _ -> assert false)
665
666
    }

667
  let double_fold_prod f l1 l2 =
668
669
670
671
    NLineProd.fold
      (fun x1 accu -> NLineProd.fold (fun x2 accu -> f accu x1 x2) l2 accu)
      l1 NLineProd.empty

672
  let ncap nf1 nf2 =
673
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
674
675
676
677
      let t = Types.cap t1 t2 in
      if Types.is_empty t then accu else
	let s = Types.cap s1 s2  in
	if Types.is_empty s then accu else
678
	  NLineProd.add (fus res1 res2, 
679
680
	   (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
	   (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) 
681
	  accu
682
    in
683
    let record r1 r2 = match r1,r2 with
684
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
685
	  (* assert (l1 = l2); *)
686
	  RecLabel(l1, double_fold_prod prod r1 r2)
687
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
688
689
690
691
692
693
	  let x = match x1,x2 with 
	    | Some res1, Some res2 -> Some (fus res1 res2) 
	    | _ -> None
	  and y = match y1,y2 with
	    | Some res1, Some res2 -> Some (fus res1 res2)
	    | _ -> None in
694
	  RecNolabel (x,y)
695
      | _ -> assert false
696
    in
697
    { nprod = double_fold_prod prod nf1.nprod nf2.nprod;
698
      nxml = double_fold_prod prod nf1.nxml nf2.nxml;
699
      nrecord = record nf1.nrecord nf2.nrecord;
700
701
    }

702
703
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
704
  let ncany = nc Types.any
705
  let ncany_abs = nc Types.Record.any_or_absent
706

707
  let empty_res = IdMap.empty
708

709
710
711
712
  let single_prod src p q = NLineProd.singleton (src, p,q)

  let ntimes lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
713
    { (nempty lab) with 
714
	nprod = single_prod empty_res (nnode p xsp) (nnode q xsq)
715
716
    }

717
718
  let nxml lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
719
    { (nempty lab) with 
720
	nxml =  single_prod empty_res (nnode p xsp) (nnode q xsq)
721
722
    }
    
723
  let nrecord lab acc l p xs =
724
725
726
727
    match lab with
      | None -> assert false
      | Some label ->
	  assert (label <= l);
728
	  let lft,rgt =
729
	    if l == label
730
731
	    then nnode p xs, ncany
	    else ncany_abs, nnode (cons p.fv (record l p)) xs
732
	  in
733
	  { (nempty lab) with
734
	      nrecord = RecLabel(label, single_prod empty_res lft rgt) }
735
736

  let nconstr lab t =
737
738
739
740
    let aux l =
      List.fold_left (fun accu (t1,t2) -> 
			NLineProd.add (empty_res, nc t1,nc t2) accu)
	NLineProd.empty l in
741
742
743
744
    let record = match lab with
      | None ->
	  let (x,y) = Types.Record.empty_cases t in
	  RecNolabel ((if x then Some empty_res else None), 
745
		      (if y then Some empty_res else None))
746
      | Some l ->
747
	  RecLabel (l,aux (Types.Record.split_normal t l)) in
748
    {  nprod = aux (Types.Product.normal t);
749
750
       nxml  = aux (Types.Product.normal ~kind:`XML t);
       nrecord = record
751
752
    }

753
  let nany lab res =
754
    { nprod  = single_prod res ncany ncany;
755
      nxml   = single_prod res ncany ncany;
756
      nrecord = match lab with
757
758
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
759
760
    }

761
762
763
764
765
766
767
  let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
  let ncapture lab x = nany lab (IdMap.singleton x SCatch)

  let rec nnormal lab ((acc,fv,d) as p) xs =
    let xs = IdSet.cap xs fv in
    if Types.is_empty acc then nempty lab
    else if IdSet.is_empty xs then nconstr lab acc
768
    else match d with
769
770
      | Constr t -> assert false
      | Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
771
      | Cup ((acc1,_,_) as p,q) -> 
772
773
774
775
776
	  ncup 
	    (nnormal lab p xs) 
	    (ncap (nnormal lab q xs) (nconstr lab (Types.neg acc1)))
      | Times (p,q) -> ntimes lab acc p q xs
      | Xml (p,q) -> nxml lab acc p q xs
777
778
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
779
      | Record (l,p) -> nrecord lab acc l p xs
780
      | Dummy -> assert false
781
782
783
784
785

(*TODO: when an operand of Cap has its first_label > lab,
  directly shift it*)


786
  let facto f t xs pl =
787
    List.fold_left 
788
789
      (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
      IdSet.empty
790
      pl
791

792
793
794
795
796
  let factorize t0 (pl,t,xs) =
    let t0 = if Types.subtype t t0 then t else Types.cap t t0 in
    let vs_var = facto Factorize.var t0 xs pl in
    let xs = IdSet.diff xs vs_var in
    let vs_nil = facto Factorize.nil t0 xs pl in
797
    let xs = IdSet.diff xs vs_nil in
798
799
    (vs_var,vs_nil,(pl,t,xs))

800
  let normal l t pl xs =
801
802
    List.fold_left 
      (fun a p -> ncap a (nnormal l (descr p) xs)) (nconstr l t) pl
803

804
  let nnf lab t0 (pl,t,xs) = 
805
(*    assert (not (Types.disjoint t t0)); *)
806
807
    let t = if Types.subtype t t0 then t else Types.cap t t0 in
    normal lab t (NodeSet.get pl) xs
808

809
810
811
812
813
814
815
816
817
818
819
  let basic_tests f (pl,t,xs) =
    let rec aux more s accu t res = function
	(* Invariant: t and s disjoint, t not empty *)
      | [] -> 
	  let accu =
	    try 
	      let t' = ResultMap.find res accu in
	      ResultMap.add res (Types.cup t t') accu
	    with Not_found -> ResultMap.add res t accu in
	  cont (Types.cup t s) accu more
      | (tp,xp,d) :: r -> 
820
	  if (IdSet.disjoint xp xs) 
821
	  then aux_check more s accu (Types.cap t tp) res r
822
	  else match d with
823
824
825
826
827
828
829
830
831
832
833
	    | Cup (p1,p2) -> aux ((t,res,p2::r)::more) s accu t res (p1::r)
	    | Cap (p1,p2) -> aux more s accu t res (p1 :: p2 :: r)
	    | Capture x -> aux more s accu t (IdMap.add x SCatch res) r
	    | Constant (x,c) -> 
		aux more s accu t (IdMap.add x (SConst c) res) r
	    | _ -> cont s accu more
    and aux_check more s accu t res pl =
      if Types.is_empty t then cont s accu more else aux more s accu t res pl
    and cont s accu = function
      | [] -> ResultMap.iter f accu
      | (t,res,pl)::tl -> aux_check tl s accu (Types.diff t s) res pl
834
    in
835
836
    aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic) 
      IdMap.empty (List.map descr pl)
837

838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
(*
  let prod_tests (pl,t,xs) =
    let rec aux accu q1 q2 res = function
      | [] -> (res,q1,q2) :: accu
      | (tp,xp,d) :: r -> 
	  if (IdSet.disjoint xp xs) 
	  then aux_check accu q1 q2 res tp r
	  else match d with
	    | Cup (p1,p2) -> aux (aux accu q1 q2 res (p2::r)) q1 q2 res (p1::r)
	    | Cap (p1,p2) -> aux accu q1 q2 res (p1 :: p2 :: r)
	    | Capture x -> aux accu q1 q2 (IdMap.add x SCatch res) r
	    | Constant (x,c) -> aux accu q1 q2 (IdMap.add x (SConst c) res) r
	    | Times (p1,p2) -> 
		let (pl1,t1,xs1) = q1 and (pl2,t2,xs2) = q2 in
		let t1 = Types.cap t1 (Types.descr (accept p1)) in
		if Types.is_empty t1 then accu
		else let t2 = Types.cap t2 (Types.descr (accept p2)) in
		if Types.is_empty t2 then accu
		else
		  let q1 =
		    let xs1' = IdSet.cap (fv p1) xs in
		    if IdSet.is_empty xs1' then (pl1,t1,xs1)
		    else (NodeSet.add p1 pl1, t1, IdSet.cup xs1 xs1')
		  and q2 = 
		    let xs2' = IdSet.cap (fv p2) xs in
		    if IdSet.is_empty xs2' then (pl2,t2,xs2)
		    else (NodeSet.add p2 pl2, t2, IdSet.cup xs2 xs2')
		  in
		  aux accu q1 q2 res r
	    | _ -> accu
    and aux_check accu q1 q2 res t r =
      List.fold_left
	(fun accu (t1',t2') ->
	   let (pl1,t1,xs1) = q1 and (pl2,t2,xs2) = q2 in
	   let t1 = Types.cap t1 t1' in
	   if Types.is_empty t1 then accu
	   else let t2 = Types.cap t2 t2' in
	   if Types.is_empty t2 then accu
	   else aux accu (pl1,t1,xs1) (pl2,t2,xs2) res r)
	accu (Types.Product.clean_normal (Types.Product.normal t))
    in
    aux_check [] ncany ncany IdMap.empty t (List.map descr pl)
*)
881

882
end
883
884


885
886
module Compile = 
struct
887
  type actions =
888
889
    | AIgnore of result
    | AKind of actions_kind
890
  and actions_kind = {
891
    basic: (Types.t * result) list;
892
893
    atoms: result Atoms.map;
    chars: result Chars.map;
894
    prod: result dispatch dispatch;
895
    xml: result dispatch dispatch;
896
897
898
    record: record option;
  }
  and record = 
899
    | RecLabel of label * result dispatch dispatch
900
    | RecNolabel of result option * result option
901
      
902
  and 'a dispatch =
903
904
905
906
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible
907

908
  and result = int * source array * int
909
  and source = 
910
    | Catch | Const of Types.const 
911
    | Stack of int | Left | Right | Nil | Recompose of int * int
912
913
      
  and return_code = 
914
      Types.t * int *   (* accepted type, arity *)
915
      int id_map option array
916
917

  and interface =
918
919
    [ `Result of int
    | `Switch of interface * interface
920
921
922
923
    | `None ]

  and dispatcher = {
    id : int;
924
    t  : Types.t;
925
    pl : Normal.Nnf.t array;
926
    label : label option;
927
928
    interface : interface;
    codes : return_code array;
929
930
    mutable actions : actions option;
    mutable printed : bool
931
  }
932

933
934
  let types_of_codes d = Array.map (fun (t,ar,_) -> t) d.codes

935
936
937
938
939
  let equal_array f a1 a2 =
    let rec aux i = (i < 0) || ((f a1.(i) a2.(i)) && (aux (i - 1))) in
    let l1 = Array.length a1 and l2 = Array.length a2 in
    (l1 == l2) && (aux (l1 - 1))

940
941
942
943
944
945
946
947
  let array_for_all f a =
    let rec aux f a i = (i < 0) || (f a.(i) && (aux f a (pred i))) in
    aux f a (Array.length a - 1)

  let array_for_all_i f a =
    let rec aux f a i = (i < 0) || (f i a.(i) && (aux f a (pred i))) in
    aux f a (Array.length a - 1)

948
949
  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
950
      | Const x, Const y -> Types.Const.equal x y 
951
      | Stack x, Stack y -> x == y
952
953
954
      | Recompose (x1,x2), Recompose (y1,y2) -> (x1 == y1) && (x2 == y2)
      | _ -> false

955
956
  let equal_result (r1,s1,l1) (r2,s2,l2) =
    (r1 == r2) && (equal_array equal_source s1 s2) && (l1 == l2)
957

958
959
960
961
962
963
964
965
  let equal_result_dispatch d1 d2 = (d1 == d2) || match (d1,d2) with
    | Dispatch (d1,a1), Dispatch (d2,a2) -> 
	(d1 == d2) && (equal_array equal_result a1 a2)
    | TailCall d1, TailCall d2 -> d1 == d2
    | Ignore a1, Ignore a2 -> equal_result a1 a2
    | _ -> false

  let immediate_res basic prod xml record =
966
    let res : result option ref = ref None in
967
    let chk = function Catch | Const _ -> true | _ -> false in
968
    let f ((_,ret,_) as r) =
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
      match !res with
	| Some r0 when equal_result r r0 -> ()
	| None when array_for_all chk ret -> res := Some r
	| _ -> raise Exit in
    (match basic with [_,r] -> f r | [] -> () | _ -> raise Exit);
    (match prod with Ignore (Ignore r) -> f r |Impossible ->()| _->raise Exit);
    (match xml with Ignore (Ignore r) -> f r |Impossible ->()| _->raise Exit);
    (match record with
      | None -> ()
      | Some (RecLabel (_,Ignore (Ignore r))) -> f r
      | Some (RecNolabel (Some r1, Some r2)) -> f r1; f r2
      | _ -> raise Exit);
    match !res with Some r -> r | None -> raise Exit
	  
  let split_kind basic prod xml record = {
    basic = basic;
    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
    chars = Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
    prod = prod; 
    xml = xml; 
    record = record
  }
991

992
  let combine_kind basic prod xml record =
993
994
    try AIgnore (immediate_res basic prod xml record)
    with Exit -> AKind (split_kind basic prod xml record)
995
      
996
997
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
998
    else
999
1000
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
	 && (array_for_all ( f act.(0) ) act) then
1001
	   Ignore act.(0)
1002
      else
1003
	Dispatch (disp, act)
1004

1005
1006
  let detect_tail_call f = function
    | Dispatch (disp,branches) when array_for_all_i f branches -> TailCall disp
1007
1008
    | x -> x

1009
1010
  let detect_right_tail_call =
    detect_tail_call
1011
      (fun i (code,ret,_) ->
1012
	 (i == code) && 
1013
	   let ar = Array.length ret in
1014
1015
	   (array_for_all_i