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

4
let get_opt = function Some x -> x | None -> assert false
5

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

15

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

35
let id x = x.id
36
let descr x = x.descr
37
38
let fv x = x.fv
let accept x = Types.internalize x.accept
39
40
41

let printed = ref []
let to_print = ref []
42
let rec print ppf (a,_,d) = 
43
  match d with
44
    | Constr t -> Types.Print.print ppf t
45
46
47
48
49
50
51
52
53
    | 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) -> 
54
	Format.fprintf ppf "{ %a =  P%i }" Label.print_attr l n.id;
55
56
	to_print := n :: !to_print
    | Capture x ->
57
	Format.fprintf ppf "%a" Ident.print x
58
    | Constant (x,c) ->
59
	Format.fprintf ppf "(%a := %a)" Ident.print x
60
	  Types.Print.print_const c
61
62
    | Dummy ->
	Format.fprintf ppf "*DUMMY*"
63

64
let dump_print ppf =
65
  while !to_print != [] do
66
67
68
69
70
71
72
73
74
75
76
    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
77

78
79
80
81
82
let print_node ppf n =
  Format.fprintf ppf "P%i" n.id;
  to_print := n :: !to_print;
  dump_print ppf

83

84
let counter = ref 0
85

86
let dummy = (Types.empty,IdSet.empty,Dummy)
87
88
let make fv =
  incr counter;
89
  { id = !counter; descr = dummy; accept = Types.make (); fv = fv }
90
91

let define x ((accept,fv,_) as d) =
92
  (* assert (x.fv = fv); *)
93
  Types.define x.accept accept;
94
  x.descr <- d
95

96
97
98
99
100
let cons fv d =
  let q = make fv in
  define q d;
  q

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

131

132
133
let print_node = ref (fun _ _ -> assert false)

134
135
136
137
138
139
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

140
  let check n = ()
141
  let dump ppf x = !print_node ppf x
142
end
143

144
145
(* Pretty-print *)

146
module Pat = struct
147
  type t = descr
148
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
    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) ->
166
	  let c = Label.compare x1 x2 in if c <> 0 then c
167
168
169
170
171
172
173
174
175
176
177
178
179
	  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
180
181
182
183
184
185
186
187
188

  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
189
    | Record (l,q) -> 6 + 17 * (Label.hash l) + 257 * q.id
190
191
192
    | Capture x -> 7 + (Id.hash x)
    | Constant (x,c) -> 8 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
    | Dummy -> assert false
193
194
195

  let check _ = assert false
  let dump _ = assert false
196
197
198
end

module Print = struct
199
200
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236

  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)) }) ->
237
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q3.descr
238
239
    | Xml _ -> assert false
    | Record (l,q) ->
240
	Format.fprintf ppf "{%a=%a}" Label.print_attr l print q.descr
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
    | 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
264
265
266
267
268
269
270
271
272
273
274


  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 "}"
275
276
end

277
let () = print_node := (fun ppf n -> Print.print ppf (descr n))
278

279
280
281
282

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
283
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
284
285
let times_res v1 v2 = Types.Positive.times v1 v2

286
(* Try with a hash-table *)
287
module MemoFilter = Map.Make 
288
  (struct 
289
     type t = Types.t * node 
290
291
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
292
       Types.compare t1 t2
293
   end)
294
295
296

let memo_filter = ref MemoFilter.empty

297
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
298
(* TODO: avoid is_empty t when t is not changing (Cap) *)
Pietro Abate's avatar
WIP    
Pietro Abate committed
299
  if Types.is_empty t then empty_res fv
300
301
  else
    match d with
Pietro Abate's avatar
WIP    
Pietro Abate committed
302
303
304
      | Constr t0 ->
          if Types.subtype t t0 then IdMap.empty 
          else (empty_res fv) (* omega *)
305
      | Cup ((a,_,_) as d1,d2) ->
306
	  IdMap.merge cup_res
307
308
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
309
      | Cap (d1,d2) ->
310
	  IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
311
312
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
313
314
315
      | Record (l,p) ->
	  filter_node (Types.Record.project t l) p
      | Capture c ->
316
	  IdMap.singleton c (Types.Positive.ty t)
317
      | Constant (c, cst) ->
318
	  IdMap.singleton c (Types.Positive.ty (Types.constant cst))
319
      | Dummy -> assert false
320

321
322
323
324
and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
325
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
326
       in
327
       IdMap.merge cup_res accu term
328
329
330
331
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)

332
and filter_node t p : Types.Positive.v id_map =
333
334
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
335
    let (_,fv,_) = descr p in
336
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
337
338
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
339
    IdMap.collide Types.Positive.define res r;
340
341
342
343
344
    r

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
345
  IdMap.map Types.Positive.solve r
Pietro Abate's avatar
WIP    
Pietro Abate committed
346

347
348
349
350
351
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

352
353
354
(* Factorization of capture variables and constant patterns *)

module Factorize = struct
355
356
  module NodeTypeSet = Set.Make(Custom.Pair(Node)(Types))

357
358
359
360
361
362
363
364
  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)
*)
365
  let rec approx_var seen (a,fv,d) t xs =
366
367
368
369
370
(*    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) ->
371
	  approx_var seen p2 (Types.diff t a1)
372
	    (approx_var seen p1 (Types.cap t a1) xs) 
373
374
375
      | Cap ((_,fv1,d1) as p1,((_,fv2,d2) as p2)) ->
	(match d1 with
	  | Capture(_, name) when Str.string_match (Str.regexp "pat[0-9]+:") name 0 ->
376
	    (match d2 with | Constr _ -> fv2 | _ -> approx_var seen p2 t xs)
377
	  | _ -> IdSet.cup
378
	    (approx_var seen p1 t (IdSet.cap fv1 xs))
379
	    (approx_var seen p2 t (IdSet.cap fv2 xs)))
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
      | 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 =
398
    if (NodeTypeSet.mem (q,t) seen) 
399
    then xs
400
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
401
      
402
403

(* Obviously not complete ! *)      
404
  let rec approx_nil seen (a,fv,d) t xs =
405
406
    assert (Types.subtype t a); 
    assert (IdSet.subset xs fv);
407
408
409
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
410
	  approx_nil seen p2 (Types.diff t a1)
411
412
413
414
415
416
417
418
419
420
421
422
	    (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 =
423
    if (NodeTypeSet.mem (q,t) seen) 
424
    then xs
425
    else approx_nil (NodeTypeSet.add (q,t) seen) q.descr t xs
426

427
(*
428
429
430
431
432
433
434
435
436
437
438
  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))
439
*)
440
441
	
  let var ((a,_,_) as p) t = 
442
    approx_var NodeTypeSet.empty p (Types.cap t a)
443
444

  let nil ((a,_,_) as p) t = 
445
    approx_nil NodeTypeSet.empty p (Types.cap t a)
446
447
448
449
450
end




451
(* Normal forms for patterns and compilation *)
452

453
454
let min (a:int) (b:int) = if a < b then a else b

455
456
let any_basic = Types.Record.or_absent Types.non_constructed

457
458
let rec first_label (acc,fv,d) =
  if Types.is_empty acc 
459
  then Label.dummy
460
461
  else match d with
    | Constr t -> Types.Record.first_label t
462
463
    | Cap (p,q) -> Label.min (first_label p) (first_label q)
    | Cup ((acc1,_,_) as p,q) -> Label.min (first_label p) (first_label q)
464
    | Record (l,p) -> l
465
    | _ -> Label.dummy
466

467
module Normal = struct
468

469
  type source = SCatch | SConst of Types.const 
470
  type result = source id_map
471

472
473
474
475
  let compare_source s1 s2 =
    if s1 == s2 then 0 
    else match (s1,s2) with
      | SCatch, _ -> -1 | _, SCatch -> 1
476
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
477

478
(*
479
480
  let hash_source = function
    | SCatch -> 1
481
    | SConst c -> Types.Const.hash c
482
*)
483
484
485
486
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

487
488
489
490
491
  module ResultMap = Map.Make(struct
				type t = result
				let compare = compare_result
			      end)

492
  module NodeSet = SortedList.Make(Node)
493

494
  module Nnf = struct
495
496
    include Custom.Dummy

497
498
499
500
501
502
    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) =
503
504
505
      Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]" 
	NodeSet.dump pl Types.Print.print t
	IdSet.dump xs
506
507
508
509
510
511
512
    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
513
514
515
516


    let first_label (pl,t,xs) = 
      List.fold_left
517
	(fun l p -> Label.min l (first_label (descr p)))
518
519
	(Types.Record.first_label t)
	pl
520
521


522
  end
523

524
525
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
526

527
528
529
530
531
    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
532

533
  module NLineProd = Set.Make(NProd)
534

535
  type record =
536
    | RecNolabel of result option * result option
537
    | RecLabel of label * NLineProd.t
538
  type t = {
539
540
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
541
    nrecord: record
542
  }
543

544
  let fus = IdMap.union_disj
545

546
  let nempty lab = 
547
    { nprod = NLineProd.empty; 
548
      nxml = NLineProd.empty;
549
      nrecord = (match lab with 
550
		   | Some l -> RecLabel (l,NLineProd.empty)
551
		   | None -> RecNolabel (None,None))
552
    }
553
  let dummy = nempty None
554
555
556


  let ncup nf1 nf2 = 
557
    { nprod   = NLineProd.union nf1.nprod nf2.nprod;
558
      nxml    = NLineProd.union nf1.nxml nf2.nxml;
559
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
560
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
561
		       (* assert (l1 = l2); *) 
562
		       RecLabel (l1, NLineProd.union r1 r2)
563
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
564
565
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
566
		   | _ -> assert false)
567
568
    }

569
  let double_fold_prod f l1 l2 =
570
571
572
573
    NLineProd.fold
      (fun x1 accu -> NLineProd.fold (fun x2 accu -> f accu x1 x2) l2 accu)
      l1 NLineProd.empty

574
  let ncap nf1 nf2 =
575
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
576
577
578
579
      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
580
	  NLineProd.add (fus res1 res2, 
581
582
	   (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
	   (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) 
583
	  accu
584
    in
585
    let record r1 r2 = match r1,r2 with
586
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
587
	  (* assert (l1 = l2); *)
588
	  RecLabel(l1, double_fold_prod prod r1 r2)
589
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
590
591
592
593
594
595
	  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
596
	  RecNolabel (x,y)
597
      | _ -> assert false
598
    in
599
    { nprod = double_fold_prod prod nf1.nprod nf2.nprod;
600
      nxml = double_fold_prod prod nf1.nxml nf2.nxml;
601
      nrecord = record nf1.nrecord nf2.nrecord;
602
603
    }

604
605
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
606
  let ncany = nc Types.any
607
  let ncany_abs = nc Types.Record.any_or_absent
608

609
  let empty_res = IdMap.empty
610

611
612
613
614
  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
615
    { (nempty lab) with 
616
	nprod = single_prod empty_res (nnode p xsp) (nnode q xsq)
617
618
    }

619
620
  let nxml lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
621
    { (nempty lab) with 
622
	nxml =  single_prod empty_res (nnode p xsp) (nnode q xsq)
623
624
    }
    
625
626
627
628
629
630
631
632
633
634
635
636
637
  let nrecord (lab : Label.t option) acc (l : Label.t) p xs =
    let label = get_opt lab in
(*    Format.fprintf
      Format.std_formatter "label=%a l=%a@."
      Label.print label Label.print l; *)
    assert (Label.compare label l <= 0);
    let lft,rgt =
      if Label.equal l label
      then nnode p xs, ncany
      else ncany_abs, nnode (cons p.fv (record l p)) xs
    in
    { (nempty lab) with
	nrecord = RecLabel(label, single_prod empty_res lft rgt) }
638
639

  let nconstr lab t =
640
641
642
643
    let aux l =
      List.fold_left (fun accu (t1,t2) -> 
			NLineProd.add (empty_res, nc t1,nc t2) accu)
	NLineProd.empty l in
644
645
646
647
    let record = match lab with
      | None ->
	  let (x,y) = Types.Record.empty_cases t in
	  RecNolabel ((if x then Some empty_res else None), 
648
		      (if y then Some empty_res else None))
649
      | Some l ->
650
	  RecLabel (l,aux (Types.Record.split_normal t l)) in
651
652
653
    {  nprod = aux (Types.Product.clean_normal (Types.Product.normal t));
       nxml  = 
	aux (Types.Product.clean_normal (Types.Product.normal ~kind:`XML t));
654
       nrecord = record
655
656
    }

657
  let nany lab res =
658
    { nprod  = single_prod res ncany ncany;
659
      nxml   = single_prod res ncany ncany;
660
      nrecord = match lab with
661
662
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
663
664
    }

665
666
667
  let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
  let ncapture lab x = nany lab (IdMap.singleton x SCatch)

668
  let rec nnormal lab (acc,fv,d) xs =
669
670
671
    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
672
    else match d with
673
674
      | Constr t -> assert false
      | Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
675
      | Cup ((acc1,_,_) as p,q) -> 
676
677
678
679
680
	  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
681
682
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
683
      | Record (l,p) -> nrecord lab acc l p xs
684
      | Dummy -> assert false
685
686
687
688
689

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


690
  let facto f t xs pl =
691
    List.fold_left 
692
693
      (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
      IdSet.empty
694
      pl
695

696
697
698
699
700
  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
701
    let xs = IdSet.diff xs vs_nil in
702
703
    (vs_var,vs_nil,(pl,t,xs))

704
  let normal l t pl xs =
705
706
    List.fold_left 
      (fun a p -> ncap a (nnormal l (descr p) xs)) (nconstr l t) pl
707

708
  let nnf lab t0 (pl,t,xs) = 
709
(*    assert (not (Types.disjoint t t0)); *)
710
711
    let t = if Types.subtype t t0 then t else Types.cap t t0 in
    normal lab t (NodeSet.get pl) xs
712

713
714
715
716
717
718
719
720
721
722
723
  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 -> 
724
	  if (IdSet.disjoint xp xs) 
725
	  then aux_check more s accu (Types.cap t tp) res r
726
	  else match d with
727
728
729
730
731
732
733
734
735
736
737
	    | 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
738
    in
739
740
    aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic) 
      IdMap.empty (List.map descr pl)
741

742
(*
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
  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)
784
*)
785
end
786
787


788
789
module Compile = struct
  open Auto_pat
790
      
791
  type return_code = 
792
      Types.t * int *   (* accepted type, arity *)
793
      int id_map option array
794

795
  type interface =
796
797
    [ `Result of int
    | `Switch of interface * interface
798
799
    | `None ]

800
  type dispatcher = {
801
    id : int;
802
    t  : Types.t;
803
    pl : Normal.Nnf.t array;
804
    label : label option;
805
806
    interface : interface;
    codes : return_code array;
807
    state : state;
808
  }
809

810
  let dispatcher_of_state = Hashtbl.create 1024
811

812
813
814
815
816
  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))

817
818
819
820
821
822
823
824
  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)

825
826
  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
827
      | Const x, Const y -> Types.Const.equal x y 
828
      | Stack x, Stack y -> x == y
829
830
831
      | Recompose (x1,x2), Recompose (y1,y2) -> (x1 == y1) && (x2 == y2)
      | _ -> false

832
833
  let equal_result (r1,s1,l1) (r2,s2,l2) =
    (r1 == r2) && (equal_array equal_source s1 s2) && (l1 == l2)
834

835
836
837
838
839
840
841
842
  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 =
843
    let res : result option ref = ref None in
844
    let chk = function Catch | Const _ -> true | _ -> false in
845
    let f ((_,ret,_) as r) =
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
      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;
862
863
    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.BoolAtoms.leafconj (Types.Atom.get t), r) basic);
    chars = Chars.mk_map (List.map (fun (t,r) -> Types.BoolChars.leafconj (Types.Char.get t), r) basic);
864
865
866
867
    prod = prod; 
    xml = xml; 
    record = record
  }
868

869
  let combine_kind basic prod xml record =
870
871
    try AIgnore (immediate_res basic prod xml record)
    with Exit -> AKind (split_kind basic prod xml record)
872
      
873
874
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
875
    else
876
877
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
	 && (array_for_all ( f act.(0) ) act) then
878
	   Ignore act.(0)
879
      else
880
	Dispatch (disp.state, act)
881

882
883
  let detect_tail_call f = function
    | Dispatch (disp,branches) when array_for_all_i f branches -> TailCall disp
884
885
    | x -> x

886
887
  let detect_right_tail_call =
    detect_tail_call
888
      (fun i (code,ret,_) ->
889
	 (i == code) && 
890
	   let ar = Array.length ret in
891
892
	   (array_for_all_i 
	      (fun pos -> 
893
		 function Stack j when pos + j == ar -> true | _ ->