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

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

13

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


34

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 (LabelPool.value l) n.id;
55
56
	to_print := n :: !to_print
    | Capture x ->
57
	Format.fprintf ppf "%a" U.print (Id.value x)
58
    | Constant (x,c) ->
59
	Format.fprintf ppf "(%a := %a)" U.print (Id.value 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
let counter = State.ref "Patterns.counter" 0

81
let dummy = (Types.empty,IdSet.empty,Dummy)
82
83
let make fv =
  incr counter;
84
  { id = !counter; descr = dummy; accept = Types.make (); fv = fv }
85
86

let define x ((accept,fv,_) as d) =
87
  (* assert (x.fv = fv); *)
88
  Types.define x.accept accept;
89
  x.descr <- d
90

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


126
127
128
129
130
131
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

132
133
134
  let check n = ()
  let dump ppf _ = Format.fprintf ppf "<Patterns.Node>"

135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191

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

  module DMemo = Map.Make(Custom.Int)
  let memo = Serialize.Get.mk_property (fun t -> ref DMemo.empty)
  let rec deserialize t = 
    let l = Serialize.Get.get_property memo t in
    let id = Serialize.Get.int t in
    try DMemo.find id !l
    with Not_found ->
      let accept = Types.Node.deserialize t in
      let fv = IdSet.deserialize t in
      incr counter;
192
      let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
      l := DMemo.add id n !l;
      n.descr <- deserialize_descr t;
      n
  and deserialize_descr s =
    match Serialize.Get.bits 3 s with
      | 0 -> constr (Types.deserialize s)
      | 1 ->
	  (* Avoid unnecessary tests *)
	  let (acc1,fv1,_) as x1 = deserialize_descr s in
	  let (acc2,fv2,_) as x2 = deserialize_descr s in
	  (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
      | 2 ->
	  let (acc1,fv1,_) as x1 = deserialize_descr s in
	  let (acc2,fv2,_) as x2 = deserialize_descr s in
	  (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2))
      | 3 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  times x y
      | 4 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  xml x y
      | 5 ->
	  let l = LabelPool.deserialize s in
	  let x = deserialize s in
	  record l x
      | 6 -> capture (Id.deserialize s)
      | 7 ->
	  let x = Id.deserialize s in
	  let c = Types.Const.deserialize s in
	  constant x c
      | _ -> assert false


end
229
230
231
232
233


(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
234
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
235
236
let times_res v1 v2 = Types.Positive.times v1 v2

237
(* Try with a hash-table *)
238
module MemoFilter = Map.Make 
239
  (struct 
240
     type t = Types.t * node 
241
242
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
243
       Types.compare t1 t2
244
   end)
245
246
247

let memo_filter = ref MemoFilter.empty

248
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
249
(* TODO: avoid is_empty t when t is not changing (Cap) *)
250
251
252
253
  if Types.is_empty t 
  then empty_res fv
  else
    match d with
254
      | Constr _ -> IdMap.empty
255
      | Cup ((a,_,_) as d1,d2) ->
256
	  IdMap.merge cup_res
257
258
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
259
      | Cap (d1,d2) ->
260
	  IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
261
262
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
263
264
265
      | Record (l,p) ->
	  filter_node (Types.Record.project t l) p
      | Capture c ->
266
	  IdMap.singleton c (Types.Positive.ty t)
267
      | Constant (c, cst) ->
268
	  IdMap.singleton c (Types.Positive.ty (Types.constant cst))
269
      | Dummy -> assert false
270

271
272
273
274
and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
275
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
276
       in
277
       IdMap.merge cup_res accu term
278
279
280
281
282
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)


283
and filter_node t p : Types.Positive.v id_map =
284
285
286
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
    let (_,fv,_) as d = descr p in
287
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
288
289
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
290
    IdMap.collide Types.Positive.define res r;
291
292
293
294
295
    r

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
296
  IdMap.get (IdMap.map Types.Positive.solve r)
297
298


299
300
(* Normal forms for patterns and compilation *)

301
302
let min (a:int) (b:int) = if a < b then a else b

303
304
305
let any_basic = Types.Record.or_absent Types.non_constructed


306
module Normal = struct
307

308
  type source = 
309
310
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
311
  type result = source id_map
312

313
314
315
316
317
318
319
  let compare_source s1 s2 =
    if s1 == s2 then 0 
    else match (s1,s2) with
      | SCatch, _ -> -1 | _, SCatch -> 1
      | SLeft, _ -> -1 | _, SLeft -> 1
      | SRight, _ -> -1 | _, SRight -> 1
      | SRecompose, _ -> -1 | _, SRecompose -> 1
320
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
321
322
323
324
325
326

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
327
    | SConst c -> Types.Const.hash c
328
329
330
331
332
333
334
335
336
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


  module NodeSet = 
337
338
    SortedList.Make(Node)

339

340
  type nnf = NodeSet.t * Types.t (* pl,t;   t <= \accept{pl} *)
341
342
343

  let compare_nnf (l1,t1) (l2,t2) =
    let c = NodeSet.compare l1 l2 in if c <> 0 then c
344
    else Types.compare t1 t2
345
346

  let hash_nnf (l,t) =
347
    (NodeSet.hash l) + 17 * (Types.hash t)
348
349
350
351

  module NLineBasic = 
    SortedList.Make(
      struct
352
	include Custom.Dummy
353
	let serialize s _ = failwith "Patterns.NLineBasic.serialize"
354
	type t = result * Types.t
355
356
	let compare (r1,t1) (r2,t2) =
	  let c = compare_result r1 r2 in if c <> 0 then c
357
	  else Types.compare t1 t2
358
	let equal x y = compare x y == 0
359
	let hash (r,t) = hash_result r + 17 * Types.hash t
360
361
362
363
364
365
      end
    )

  module NLineProd = 
    SortedList.Make(
      struct
366
	include Custom.Dummy
367
	let serialize s _ = failwith "Patterns.NLineProd.serialize"
368
	type t = result * nnf * nnf
369
370
371
372
	let compare (r1,x1,y1) (r2,x2,y2) =
	  let c = compare_result r1 r2 in if c <> 0 then c
	  else let c = compare_nnf x1 x2 in if c <> 0 then c
	  else compare_nnf y1 y2
373
	let equal x y = compare x y == 0
374
375
376
377
378
	let hash (r,x,y) =
	  hash_result r + 17 * (hash_nnf x) + 267 * (hash_nnf y)
      end
    )

379
  type record =
380
    | RecNolabel of result option * result option
381
    | RecLabel of label * NLineProd.t
382
  type t = {
383
    nfv    : fv;
384
    ncatchv: fv;
385
386
387
388
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
389
    nrecord: record
390
391
  }

392
393
394
395
396
397
  let compare_nf t1 t2 =
    if t1 == t2 then 0
    else
      (* TODO: reorder; remove comparison of nfv ? *)
      let c = IdSet.compare t1.nfv t2.nfv in if c <> 0 then c 
      else let c = IdSet.compare t1.ncatchv t2.ncatchv in if c <> 0 then c
398
      else let c = Types.compare t1.na t2.na in if c <> 0 then c
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
      else let c = NLineBasic.compare t1.nbasic t2.nbasic in if c <> 0 then c
      else let c = NLineProd.compare t1.nprod t2.nprod in if c <> 0 then c
      else let c = NLineProd.compare t1.nxml t2.nxml in if c <> 0 then c
      else match t1.nrecord, t2.nrecord with
	| RecNolabel (s1,n1), RecNolabel (s2,n2) ->
	    let c = match (s1,s2) with
	      | None,None -> 0
	      | Some r1, Some r2 -> compare_result r1 r2
	      | None, _ -> -1
	      | _, None -> 1 in
	    if c <> 0 then c 
	    else (match (n1,n2) with
	      | None,None -> 0
	      | Some r1, Some r2 -> compare_result r1 r2
	      | None, _ -> -1
	      | _, None -> 1)
	| RecNolabel (_,_), _ -> -1
	| _, RecNolabel (_,_) -> 1
	| RecLabel (l1,p1), RecLabel (l2,p2) ->
	    let c = LabelPool.compare l1 l2 in if c <> 0 then c
	    else NLineProd.compare p1 p2
420

421
  let fus = IdMap.union_disj
422

423
424
425
  let nempty lab = 
    { nfv = IdSet.empty; ncatchv = IdSet.empty; 
      na = Types.empty;
426
427
428
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
429
      nrecord = (match lab with 
430
		   | Some l -> RecLabel (l,NLineProd.empty)
431
		   | None -> RecNolabel (None,None))
432
    }
433
  let dummy = nempty None
434
435
436
437
438
439


  let ncup nf1 nf2 = 
    (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
    (* assert (nf1.nfv = nf2.nfv); *)
    { nfv = nf1.nfv;
440
      ncatchv = IdSet.cap nf1.ncatchv nf2.ncatchv;
441
      na      = Types.cup nf1.na nf2.na;
442
443
444
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
445
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
446
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
447
		       (* assert (l1 = l2); *) RecLabel (l1, NLineProd.cup r1 r2)
448
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
449
450
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
451
		   | _ -> assert false)
452
453
454
    }

  let double_fold f l1 l2 =
455
456
457
458
459
460
    List.fold_left 
      (fun accu x1 -> List.fold_left (fun accu x2 -> f accu x1 x2) accu l2)
      [] l1

  let double_fold_prod f l1 l2 =
    double_fold f (NLineProd.get l1) (NLineProd.get l2)
461
462
	 
  let ncap nf1 nf2 =
463
    let prod accu (res1,(pl1,t1),(ql1,s1)) (res2,(pl2,t2),(ql2,s2)) =
464
465
466
467
      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
468
469
	  (fus res1 res2, (NodeSet.cup pl1 pl2,t),(NodeSet.cup ql1 ql2,s)) 
	  :: accu
470
471
472
473
474
475
    in
    let basic accu (res1,t1) (res2,t2) =
      let t = Types.cap t1 t2 in
      if Types.is_empty t then accu else
	(fus res1 res2, t) :: accu
    in
476
    let record r1 r2 = match r1,r2 with
477
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
478
	  (* assert (l1 = l2); *)
479
	  RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
480
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
481
482
483
484
485
486
	  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
487
	  RecNolabel (x,y)
488
      | _ -> assert false
489
    in
490
491
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
      ncatchv = IdSet.cup nf1.ncatchv nf2.ncatchv;
492
      na = Types.cap nf1.na nf2.na;
493
494
495
496
497
498
      nbasic = NLineBasic.from_list (double_fold basic 
				       (NLineBasic.get nf1.nbasic) 
				       (NLineBasic.get nf2.nbasic));
      nprod = NLineProd.from_list (double_fold_prod prod nf1.nprod nf2.nprod);
      nxml = NLineProd.from_list (double_fold_prod prod nf1.nxml nf2.nxml);
      nrecord = record nf1.nrecord nf2.nrecord;
499
500
    }

501
502
503
504
  let nnode p = NodeSet.singleton p, Types.descr p.accept
  let nc t = NodeSet.empty, t
  let ncany = nc Types.any

505
  let empty_res = IdMap.empty
506

507
  let ntimes lab acc p q = 
508
509
510
    let src_p = IdMap.constant SLeft p.fv
    and src_q = IdMap.constant SRight q.fv in
    let src = IdMap.merge_elem SRecompose src_p src_q in 
511
    { nempty lab with 
512
	nfv = IdSet.cup p.fv q.fv; 
513
	na = acc;
514
	nprod = NLineProd.singleton (src, nnode p, nnode q);
515
516
    }

517
  let nxml lab acc p q = 
518
519
520
    let src_p = IdMap.constant SLeft p.fv
    and src_q = IdMap.constant SRight q.fv in
    let src = IdMap.merge_elem SRecompose src_p src_q in 
521
    { nempty lab with 
522
	nfv = IdSet.cup p.fv q.fv; 
523
	na = acc;
524
	nxml =  NLineProd.singleton (src, nnode p, nnode q);
525
526
    }
    
527
528
529
530
531
532
533
534
535
536
  let nrecord lab acc l p =
    match lab with
      | None -> assert false
      | Some label ->
	  assert (label <= l);
	  if l == label then
	    let src = IdMap.constant SLeft p.fv in
	    { nempty lab with
		nfv = p.fv;
		na = acc;
537
		nrecord = RecLabel(label, 
538
				 NLineProd.singleton (src,nnode p, ncany))}
539
540
541
542
543
544
545
546
	  else
	    let src = IdMap.constant SRight p.fv in
	    let p' = make p.fv in  (* optimize this ... *)
	      (* cache the results to avoid looping ... *)
	    define p' (record l p);
	    { nempty lab with
		nfv = p.fv;
		na = acc;
547
548
549
550
		nrecord = 
		      RecLabel(label,
		        NLineProd.singleton(src,nc Types.Record.any_or_absent, 
 			 nnode p') )}
551
552
553
	  

  let nconstr lab t =
554
555
    let aux l = NLineProd.from_list
		(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
556
557
558
559
    let record = 
      match lab with
	| None ->
	    let (x,y) = Types.Record.empty_cases t in
560
	    RecNolabel ((if x then Some empty_res else None), 
561
562
		      (if y then Some empty_res else None))
	| Some l ->
563
	    RecLabel (l,aux (Types.Record.split_normal t l))
564
565
    in	      
    { nempty lab with
566
	na = t;
567
	nbasic = NLineBasic.singleton (empty_res, Types.cap t any_basic);
568
569
570
	nprod = aux (Types.Product.normal t);
	nxml  = aux (Types.Product.normal ~kind:`XML t);
	nrecord = record
571
572
    }

573
  let nconstant lab x c = 
574
575
576
    let l = IdMap.singleton x (SConst c) in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.empty;
577
      na = Types.any;
578
579
580
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
581
      nrecord = match lab with
582
	| None -> RecNolabel (Some l, Some l)
583
	| Some lab -> 
584
585
586
	    RecLabel (lab, NLineProd.singleton 
			(l,nc Types.Record.any_or_absent,
				 ncany))
587
588
    }

589
  let ncapture lab x = 
590
591
592
    let l = IdMap.singleton x SCatch in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.singleton x;
593
      na = Types.any;
594
595
596
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
597
      nrecord = match lab with
598
	| None -> RecNolabel (Some l, Some l)
599
	| Some lab -> 
600
601
602
	    RecLabel (lab, NLineProd.singleton 
			(l,nc Types.Record.any_or_absent,
			         ncany))
603
604
    }

605
  let rec nnormal lab (acc,fv,d) =
606
    if Types.is_empty acc 
607
    then nempty lab
608
    else match d with
609
610
      | Constr t -> nconstr lab t
      | Cap (p,q) -> ncap (nnormal lab p) (nnormal lab q)
611
      | Cup ((acc1,_,_) as p,q) -> 
612
613
614
615
616
617
618
	  ncup (nnormal lab p) (ncap (nnormal lab q) 
				  (nconstr lab (Types.neg acc1)))
      | Times (p,q) -> ntimes lab acc p q
      | Xml (p,q) -> nxml lab acc p q
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
      | Record (l,p) -> nrecord lab acc l p
619
      | Dummy -> assert false
620
621
622
623
624
625

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

  let rec first_label (acc,fv,d) =
    if Types.is_empty acc 
626
    then LabelPool.dummy_max
627
628
629
630
631
632
    else match d with
      | Constr t -> Types.Record.first_label t
      | Cap (p,q) -> min (first_label p) (first_label q)
      | Cup ((acc1,_,_) as p,q) -> min (first_label p) (first_label q)
	    (* should "first_label_type acc1" ? *)
      | Record (l,p) -> l
633
      | _ -> LabelPool.dummy_max
634

635
636
637
   
  let remove_catchv n =
    let ncv = n.ncatchv in
638
639
640
641
    let nlinesbasic l = 
      NLineBasic.map (fun (res,x) -> (IdMap.diff res ncv,x)) l in
    let nlinesprod l  = 
      NLineProd.map (fun (res,x,y) -> (IdMap.diff res ncv,x,y)) l in
642
    { nfv     = IdSet.diff n.nfv ncv;
643
644
      ncatchv = n.ncatchv;
      na      = n.na;
645
646
647
      nbasic  = nlinesbasic n.nbasic;
      nprod   = nlinesprod n.nprod;
      nxml    = nlinesprod n.nxml;
648
      nrecord = (match n.nrecord with
649
		   | RecNolabel (x,y) ->
650
651
652
653
654
655
		       let x = match x with 
			 | Some res -> Some (IdMap.diff res ncv) 
			 | None -> None in
		       let y = match y with 
			 | Some res -> Some (IdMap.diff res ncv) 
			 | None -> None in
656
		       RecNolabel (x,y)
657
		   | RecLabel (lab,l) -> RecLabel (lab, nlinesprod l))
658
659
    }

660
  let normal l t pl =
661
    remove_catchv
662
663
664
665
      (List.fold_left 
	 (fun a p -> ncap a (nnormal l (descr p))) 
	 (nconstr l t) 
	 pl)
666
end
667
668


669
670
module Compile = 
struct
671
  type actions =
672
673
    | AIgnore of result
    | AKind of actions_kind
674
  and actions_kind = {
675
    basic: (Types.t * result) list;
676
677
    atoms: result Atoms.map;
    chars: result Chars.map;
678
    prod: result dispatch dispatch;
679
    xml: result dispatch dispatch;
680
681
682
    record: record option;
  }
  and record = 
683
    | RecLabel of label * result dispatch dispatch
684
    | RecNolabel of result option * result option
685
      
686
  and 'a dispatch =
687
688
689
690
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible
691
692

  and result = int * source array
693
  and source = 
694
695
    | Catch | Const of Types.const 
    | Left of int | Right of int | Recompose of int * int
696
697
      
  and return_code = 
698
      Types.t * int *   (* accepted type, arity *)
699
      (int * int id_map) list
700
701

  and interface =
702
703
    [ `Result of int
    | `Switch of interface * interface
704
705
706
707
    | `None ]

  and dispatcher = {
    id : int;
708
    t  : Types.t;
709
    pl : Normal.t array;
710
    label : label option;
711
712
    interface : interface;
    codes : return_code array;
713
714
    mutable actions : actions option;
    mutable printed : bool
715
  }
716

717
718
719
720
721
722
723
  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))

  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
724
      | Const x, Const y -> Types.Const.equal x y 
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
      | Left x, Left y -> x == y
      | Right x, Right y -> x == y
      | Recompose (x1,x2), Recompose (y1,y2) -> (x1 == y1) && (x2 == y2)
      | _ -> false

  let equal_result (r1,s1) (r2,s2) =
    (r1 == r2) && (equal_array equal_source s1 s2)

  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


741
742
  let array_for_all f a =
    let rec aux f a i =
743
      if i == Array.length a then true
744
745
746
747
748
749
      else f a.(i) && (aux f a (succ i))
    in
    aux f a 0

  let array_for_all_i f a =
    let rec aux f a i =
750
      if i == Array.length a then true
751
752
753
754
      else f i a.(i) && (aux f a (succ i))
    in
    aux f a 0

755
  let combine_kind basic prod xml record =
756
757
758
759
760
761
762
    try (
      let rs = [] in
      let rs = match basic with
	| [_,r] -> r :: rs
	| [] -> rs
	| _ -> raise Exit in
      let rs = match prod with
763
764
	| Impossible -> rs
	| Ignore (Ignore r) -> r :: rs
765
	| _ -> raise Exit in
766
      let rs = match xml with
767
768
	| Impossible -> rs
	| Ignore (Ignore r) -> r :: rs
769
	| _ -> raise Exit in
770
771
      let rs = match record with
	| None -> rs
772
773
	| Some (RecLabel (_,Ignore (Ignore r))) -> r :: rs
	| Some (RecNolabel (Some r1, Some r2)) -> r1 :: r2 :: rs
774
775
	| _ -> raise Exit in
      match rs with
776
	| ((_, ret) as r) :: rs when 
777
	    List.for_all ( equal_result r ) rs 
778
	    && array_for_all 
779
780
	      (function Catch | Const _ -> true | _ -> false) ret
	    -> AIgnore r
781
782
	| _ -> raise Exit
    )
783
784
785
786
    with Exit -> 
      AKind 
      { basic = basic;
	atoms = 
787
	  Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
788
	chars = 
789
	  Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
790
791
	prod = prod; 
	xml = xml; 
792
793
	record = record;
      }
794
      
795
796
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
797
    else
798
799
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
	 && (array_for_all ( f act.(0) ) act) then
800
	   Ignore act.(0)
801
      else
802
	Dispatch (disp, act)
803
804
805


  let detect_right_tail_call = function
806
    | Dispatch (disp,branches) 
807
808
809
	when
	  array_for_all_i
	    (fun i (code,ret) ->
810
	       (i == code) && 
811
812
	       (array_for_all_i 
		  (fun pos -> 
813
		     function Right j when pos == j -> true | _ -> false)
814
815
816
		  ret
	       )
	    ) branches
817
	  -> TailCall disp
818
819
820
    | x -> x

  let detect_left_tail_call = function
821
    | Dispatch (disp,branches)
822
823
824
825
	when
	  array_for_all_i
	    (fun i -> 
	       function 
826
		 | Ignore (code,ret) ->
827
		     (i == code) &&
828
829
		     (array_for_all_i 
			(fun pos -> 
830
			   function Left j when pos == j -> true | _ -> false)
831
832
833
834
835
			ret
	       )
		 | _ -> false
	    ) branches
 	  ->
836
	 TailCall disp
837
838
    | x -> x
   
839
840
  let cur_id = State.ref "Patterns.cur_id" 0
		 (* TODO: save dispatchers ? *)
841
		 
842
843
844
845
846
847
  module NfMap = Map.Make(
    struct 
      type t = Normal.t
      let compare = Normal.compare_nf
    end)

848
849
  module DispMap = Map.Make(
    struct
850
      type t = Types.t * Normal.t array
851
852
853
854
855
856
857
858

      let rec compare_rec a1 a2 i =
	if i < 0 then 0 
	else
	  let c = Normal.compare_nf a1.(i) a2.(i) in
	  if c <> 0 then c else compare_rec a1 a2 (i - 1)
	  
      let compare (t1,a1) (t2,a2) =
859
	let c = Types.compare t1 t2 in if c <> 0 then c 
860
861
862
	else let l1 = Array.length a1 and l2 = Array.length a2 in
	if l1 < l2 then -1 else if l1 > l2 then 1
	else compare_rec a1 a2 (l1 - 1)
863
864
    end
  )
865
866

    (* Try with a hash-table ! *)
867
    
868
  let dispatchers = ref DispMap.empty
869
870
871
		
  let timer_disp = Stats.Timer.create "Patterns.dispatcher loop"
      
872
  let dispatcher t pl lab : dispatcher =
873
874
    try DispMap.find (t,pl) !dispatchers
    with Not_found ->
875
      let nb = ref 0 in
876
877
      let codes = ref [] in
      let rec aux t arity i accu = 
878
879
	if i == Array.length pl 
	then (incr nb; codes := (t,arity,accu)::!codes; `Result (!nb - 1))
880
	else
881
882
883
884
885
886
887
	  let p = pl.(i) in
	  let tp = p.Normal.na in
(*	  let tp = Types.normalize tp in *)

	  let a1 = Types.cap t tp in
	  if Types.is_empty a1 then
	    `Switch (`None,aux t arity (i+1) accu)
888
	  else
889
	    let v = p.Normal.nfv in
890
	    let a2 = Types.diff t tp in
891
	    let accu' = (i,IdMap.num arity v) :: accu in
892
893
894
895
896
897
898
	    if Types.is_empty a2 then
	      `Switch (aux t (arity + (IdSet.length v)) (i+1) accu',`None)
	    else
	      `Switch (aux a1 (arity + (IdSet.length v)) (i+1) accu',
		       aux a2 arity (i+1) accu)

(* Unopt version:
899
	    `Switch 
900
	      (
901
	       aux (Types.cap t tp) (arity + (IdSet.length v)) (i+1) accu',
902
	       aux (Types.diff t tp) arity (i+1) accu
903
	      )
904
905
*)

906
      in
907
908
909
910
911
912
913
914
915
(*      Array.iteri (fun i p ->
		     Format.fprintf Format.std_formatter
		       "Pattern %i/%i accepts %a@." i (Array.length pl)
		       Types.Print.print p.Normal.na) pl; *)
      
      Stats.Timer.start timer_disp;
      let iface = 
	if Types.is_empty t then `None else aux t 0 0 [] in
      Stats.Timer.stop timer_disp ();
916
917
      let res = { id = !cur_id; 
		  t = t;
918
		  label = lab;
919
		  pl = pl;
920
		  interface = iface;
921
		  codes = Array.of_list (List.rev !codes);
922
		  actions = None; printed = false } in
923
924
925
926
      incr cur_id;
      dispatchers := DispMap.add (t,pl) res !dispatchers;
      res
    
927
928
  let find_code d a =
    let rec aux i = function
929
930
      | `Result code -> code
      | `None -> assert false
931
      | `Switch (yes,_) when a.(i) != None -> aux (i + 1) yes
932
      | `Switch (_,no) -> aux (i + 1) no
933
934
935
936
    in
    aux 0 d.interface

  let create_result pl =