patterns.ml 42.1 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) 
Pietro Abate's avatar
Pietro Abate committed
373
374
375
376
377
      | 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))
(*
378
379
      | Cap ((_,fv1,d1) as p1,((_,fv2,d2) as p2)) ->
	(match d1 with
380
	  | Capture(_, name) when Str.string_match (Str.regexp "pat[0-9]+:") (Encodings.Utf8.get_str name) 0 ->
381
	    (match d2 with | Constr _ -> fv2 | _ -> approx_var seen p2 t xs)
382
	  | _ -> IdSet.cup
383
	    (approx_var seen p1 t (IdSet.cap fv1 xs))
384
	    (approx_var seen p2 t (IdSet.cap fv2 xs)))
Pietro Abate's avatar
Pietro Abate committed
385
*)
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
      | 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 =
404
    if (NodeTypeSet.mem (q,t) seen) 
405
    then xs
406
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
407
      
408
409

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

433
(*
434
435
436
437
438
439
440
441
442
443
444
  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))
445
*)
446
447
	
  let var ((a,_,_) as p) t = 
448
    approx_var NodeTypeSet.empty p (Types.cap t a)
449
450

  let nil ((a,_,_) as p) t = 
451
    approx_nil NodeTypeSet.empty p (Types.cap t a)
452
453
454
455
456
end




457
(* Normal forms for patterns and compilation *)
458

459
460
let min (a:int) (b:int) = if a < b then a else b

461
462
let any_basic = Types.Record.or_absent Types.non_constructed

463
464
let rec first_label (acc,fv,d) =
  if Types.is_empty acc 
465
  then Label.dummy
466
467
  else match d with
    | Constr t -> Types.Record.first_label t
468
469
    | Cap (p,q) -> Label.min (first_label p) (first_label q)
    | Cup ((acc1,_,_) as p,q) -> Label.min (first_label p) (first_label q)
470
    | Record (l,p) -> l
471
    | _ -> Label.dummy
472

473
module Normal = struct
474

475
  type source = SCatch | SConst of Types.const 
476
  type result = source id_map
477

478
479
480
481
  let compare_source s1 s2 =
    if s1 == s2 then 0 
    else match (s1,s2) with
      | SCatch, _ -> -1 | _, SCatch -> 1
482
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
483

484
(*
485
486
  let hash_source = function
    | SCatch -> 1
487
    | SConst c -> Types.Const.hash c
488
*)
489
490
491
492
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

493
494
495
496
497
  module ResultMap = Map.Make(struct
				type t = result
				let compare = compare_result
			      end)

498
  module NodeSet = SortedList.Make(Node)
499

500
  module Nnf = struct
501
502
    include Custom.Dummy

503
504
505
506
507
508
    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) =
509
510
511
      Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]" 
	NodeSet.dump pl Types.Print.print t
	IdSet.dump xs
512
513
514
515
516
517
518
    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
519
520
521
522


    let first_label (pl,t,xs) = 
      List.fold_left
523
	(fun l p -> Label.min l (first_label (descr p)))
524
525
	(Types.Record.first_label t)
	pl
526
527


528
  end
529

530
531
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
532

533
534
535
536
537
    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
538

539
  module NLineProd = Set.Make(NProd)
540

541
  type record =
542
    | RecNolabel of result option * result option
543
    | RecLabel of label * NLineProd.t
544
  type t = {
545
546
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
547
    nrecord: record
548
  }
549

550
  let fus = IdMap.union_disj
551

552
  let nempty lab = 
553
    { nprod = NLineProd.empty; 
554
      nxml = NLineProd.empty;
555
      nrecord = (match lab with 
556
		   | Some l -> RecLabel (l,NLineProd.empty)
557
		   | None -> RecNolabel (None,None))
558
    }
559
  let dummy = nempty None
560
561
562


  let ncup nf1 nf2 = 
563
    { nprod   = NLineProd.union nf1.nprod nf2.nprod;
564
      nxml    = NLineProd.union nf1.nxml nf2.nxml;
565
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
566
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
567
		       (* assert (l1 = l2); *) 
568
		       RecLabel (l1, NLineProd.union r1 r2)
569
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
570
571
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
572
		   | _ -> assert false)
573
574
    }

575
  let double_fold_prod f l1 l2 =
576
577
578
579
    NLineProd.fold
      (fun x1 accu -> NLineProd.fold (fun x2 accu -> f accu x1 x2) l2 accu)
      l1 NLineProd.empty

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

610
611
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
612
  let ncany = nc Types.any
613
  let ncany_abs = nc Types.Record.any_or_absent
614

615
  let empty_res = IdMap.empty
616

617
618
619
620
  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
621
    { (nempty lab) with 
622
	nprod = single_prod empty_res (nnode p xsp) (nnode q xsq)
623
624
    }

625
626
  let nxml lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
627
    { (nempty lab) with 
628
	nxml =  single_prod empty_res (nnode p xsp) (nnode q xsq)
629
630
    }
    
631
632
633
634
635
636
637
638
639
640
641
642
643
  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) }
644
645

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

663
  let nany lab res =
664
    { nprod  = single_prod res ncany ncany;
665
      nxml   = single_prod res ncany ncany;
666
      nrecord = match lab with
667
668
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
669
670
    }

671
672
673
  let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
  let ncapture lab x = nany lab (IdMap.singleton x SCatch)

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

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


696
  let facto f t xs pl =
697
    List.fold_left 
698
699
      (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
      IdSet.empty
700
      pl
701

702
703
704
705
706
  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
707
    let xs = IdSet.diff xs vs_nil in
708
709
    (vs_var,vs_nil,(pl,t,xs))

710
  let normal l t pl xs =
711
712
    List.fold_left 
      (fun a p -> ncap a (nnormal l (descr p) xs)) (nconstr l t) pl
713

714
  let nnf lab t0 (pl,t,xs) = 
715
(*    assert (not (Types.disjoint t t0)); *)
716
717
    let t = if Types.subtype t t0 then t else Types.cap t t0 in
    normal lab t (NodeSet.get pl) xs
718

719
720
721
722
723
724
725
726
727
728
729
  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 -> 
730
	  if (IdSet.disjoint xp xs) 
731
	  then aux_check more s accu (Types.cap t tp) res r
732
	  else match d with
733
734
735
736
737
738
739
740
741
742
743
	    | 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
744
    in
745
746
    aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic) 
      IdMap.empty (List.map descr pl)
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
784
785
786
787
788
789
  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)
790
*)
791
end
792
793


794
795
module Compile = struct
  open Auto_pat
796
      
797
  type return_code = 
798
      Types.t * int *   (* accepted type, arity *)
799
      int id_map option array
800

801
  type interface =
802
803
    [ `Result of int
    | `Switch of interface * interface
804
805
    | `None ]

806
  type dispatcher = {
807
    id : int;
808
    t  : Types.t;
809
    pl : Normal.Nnf.t array;
810
    label : label option;
811
812
    interface : interface;
    codes : return_code array;
813
    state : state;
814
  }
815

816
  let dispatcher_of_state = Hashtbl.create 1024
817

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

823
824
825
826
827
828
829
830
  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)

831
832
  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
833
      | Const x, Const y -> Types.Const.equal x y 
834
      | Stack x, Stack y -> x == y
835
836
837
      | Recompose (x1,x2), Recompose (y1,y2) -> (x1 == y1) && (x2 == y2)
      | _ -> false

838
839
  let equal_result (r1,s1,l1) (r2,s2,l2) =
    (r1 == r2) && (equal_array equal_source s1 s2) && (l1 == l2)
840

841
842
843
844
845
846
847
848
  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 =
849
    let res : result option ref = ref None in
850
    let chk = function Catch | Const _ -> true | _ -> false in
851
    let f ((_,ret,_) as r) =
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
      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;
868
869
    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);
870
871
872
873
    prod = prod; 
    xml = xml; 
    record = record
  }
874

875
  let combine_kind basic prod xml record =
876
877
    try AIgnore (immediate_res basic prod xml record)
    with Exit -> AKind (split_kind basic prod xml record)
878
      
879
880
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
881
    else
882
883
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
	 && (array_for_all ( f act.(0) ) act) then
884
	   Ignore act.(0)
885
      else
886
	Dispatch (disp.state, act)
887

888
889
  let detect_tail_call f = function
    | Dispatch (disp,branches) when array_for_all_i f branches -> TailCall disp
890
891
    | x -> x

892
893
  let detect_right_tail_call =
    detect_tail_call
894
      (fun i (code,ret,_) ->
895
	 (i == code) &&