patterns.ml 41.5 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
35
} and descr = Types.t * fv * d


36

37
let id x = x.id
38
let descr x = x.descr
39
40
let fv x = x.fv
let accept x = Types.internalize x.accept
41
42
43

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

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

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

85

86
let counter = ref 0
87

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

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

98
99
100
101
102
let cons fv d =
  let q = make fv in
  define q d;
  q

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

133

134
135
let print_node = ref (fun _ _ -> assert false)

136
137
138
139
140
141
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

142
  let check n = ()
143
  let dump ppf x = !print_node ppf x
144
end
145

146
147
(* Pretty-print *)

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

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

  let check _ = assert false
  let dump _ = assert false
198
199
200
end

module Print = struct
201
202
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
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
237
238

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


  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 "}"
277
278
end

279
let () = print_node := (fun ppf n -> Print.print ppf (descr n))
280

281
282
283
284

(* Static semantics *)

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

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

let memo_filter = ref MemoFilter.empty

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

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

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

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

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

354
355
356
(* Factorization of capture variables and constant patterns *)

module Factorize = struct
357
358
  module NodeTypeSet = Set.Make(Custom.Pair(Node)(Types))

359
360
361
362
363
364
365
366
  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)
*)
367
  let rec approx_var seen (a,fv,d) t xs =
368
369
370
371
372
(*    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) ->
373
	  approx_var seen p2 (Types.diff t a1)
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
	    (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 =
397
    if (NodeTypeSet.mem (q,t) seen) 
398
    then xs
399
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
400
      
401
402

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

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

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




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

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

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

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

466
module Normal = struct
467

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

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

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

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

491
  module NodeSet = SortedList.Make(Node)
492

493
  module Nnf = struct
494
495
    include Custom.Dummy

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


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


521
  end
522

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

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

532
  module NLineProd = Set.Make(NProd)
533

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

543
  let fus = IdMap.union_disj
544

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


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

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

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

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

608
  let empty_res = IdMap.empty
609

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

618
619
  let nxml lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
620
    { (nempty lab) with 
621
	nxml =  single_prod empty_res (nnode p xsp) (nnode q xsq)
622
623
    }
    
624
625
626
627
628
629
630
631
632
633
634
635
636
  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) }
637
638

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

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

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

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

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


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

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

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

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

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

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
  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)
783
*)
784
end
785
786


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

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

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

809
  let dispatcher_of_state = Hashtbl.create 1024
810

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

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

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

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

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

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

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

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

  let detect_left_tail_call =
    detect_tail_call
      (fun i -> 
	 function 
901
902
	   | Ignore (code,ret,_) when (i == code) ->
	       let ar = Array.length ret in
903
904
	       array_for_all_i 
		 (fun pos ->