patterns.ml 40 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
81
82
let print_node ppf n =
  Format.fprintf ppf "P%i" n.id;
  to_print := n :: !to_print;
  dump_print ppf

83

84
85
let counter = State.ref "Patterns.counter" 0

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


131
132
133
134
135
136
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

137
  let check n = ()
138
  let dump = print_node
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
192
193
194
195
196

  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;
197
      let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in
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
229
230
231
232
233
      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
234
235
236
237
238


(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
239
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
240
241
let times_res v1 v2 = Types.Positive.times v1 v2

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

let memo_filter = ref MemoFilter.empty

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

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


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

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
301
  IdMap.get (IdMap.map Types.Positive.solve r)
302
303


304
305
(* Normal forms for patterns and compilation *)

306
307
let min (a:int) (b:int) = if a < b then a else b

308
309
310
let any_basic = Types.Record.or_absent Types.non_constructed


311
module Normal = struct
312

313
  type source = 
314
315
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
316
  type result = source id_map
317

318
319
320
321
322
323
324
  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
325
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
326
327
328
329
330
331

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
332
    | SConst c -> Types.Const.hash c
333
334
335
336
337
338
339
340
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


341
342
343
344
345
  let print_result ppf r = Format.fprintf ppf "<result>"
  let print_result_option ppf = function
    | Some x -> Format.fprintf ppf "Some(%a)" print_result x
    | None -> Format.fprintf ppf "None"

346
  module NodeSet = 
347
348
    SortedList.Make(Node)

349

350
  type nnf = NodeSet.t * Types.t (* pl,t;   t <= \accept{pl} *)
351

352
353
354
355
356
357
358
359
  let check_nnf (pl,t) =
    List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
      (NodeSet.get pl)

  let print_nnf ppf (pl,t) =
    Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t
			    

360
361
  let compare_nnf (l1,t1) (l2,t2) =
    let c = NodeSet.compare l1 l2 in if c <> 0 then c
362
    else Types.compare t1 t2
363
364

  let hash_nnf (l,t) =
365
    (NodeSet.hash l) + 17 * (Types.hash t)
366
367
368
369

  module NLineBasic = 
    SortedList.Make(
      struct
370
	include Custom.Dummy
371
	let serialize s _ = failwith "Patterns.NLineBasic.serialize"
372
	type t = result * Types.t
373
374
	let compare (r1,t1) (r2,t2) =
	  let c = compare_result r1 r2 in if c <> 0 then c
375
	  else Types.compare t1 t2
376
	let equal x y = compare x y == 0
377
	let hash (r,t) = hash_result r + 17 * Types.hash t
378
379
380
381
382
383
      end
    )

  module NLineProd = 
    SortedList.Make(
      struct
384
(*	include Custom.Dummy*)
385
	let serialize s _ = failwith "Patterns.NLineProd.serialize"
386
387
388
389
390
391
392
	let deserialize s = failwith "Patterns.NLineProd.deserialize"
	let check x = ()
	let dump ppf (r,x,y) =
	  Format.fprintf ppf "@[(result=%a;x=%a;y=%a)@]" 
	    print_result r
	    print_nnf x
	    print_nnf y
393
	type t = result * nnf * nnf
394
395
396
397
	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
398
	let equal x y = compare x y == 0
399
400
401
402
403
	let hash (r,x,y) =
	  hash_result r + 17 * (hash_nnf x) + 267 * (hash_nnf y)
      end
    )

404
  type record =
405
    | RecNolabel of result option * result option
406
    | RecLabel of label * NLineProd.t
407
  type t = {
408
    nfv    : fv;
409
    ncatchv: fv;
410
411
412
413
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
414
    nrecord: record
415
416
  }

417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
  let print_record ppf = function
    | RecLabel (lab,l) ->
	Format.fprintf ppf "RecLabel(@[%a@],@ @[%a@])"
	  Label.print (LabelPool.value lab)
	  NLineProd.dump l
    | RecNolabel (a,b) -> 
	Format.fprintf ppf "RecNolabel(@[%a@],@[%a@])" 
	  print_result_option a
	  print_result_option b
  let print ppf nf =
    Format.fprintf ppf "@[NF{na=%a;@[nrecord=@ @[%a@]@]}@]" 
      Types.Print.print nf.na
      print_record nf.nrecord
      

432
433
434
435
436
437
  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
438
      else let c = Types.compare t1.na t2.na in if c <> 0 then c
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
      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
460

461
  let fus = IdMap.union_disj
462

463
464
465
  let nempty lab = 
    { nfv = IdSet.empty; ncatchv = IdSet.empty; 
      na = Types.empty;
466
467
468
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
469
      nrecord = (match lab with 
470
		   | Some l -> RecLabel (l,NLineProd.empty)
471
		   | None -> RecNolabel (None,None))
472
    }
473
  let dummy = nempty None
474
475
476
477
478
479


  let ncup nf1 nf2 = 
    (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
    (* assert (nf1.nfv = nf2.nfv); *)
    { nfv = nf1.nfv;
480
      ncatchv = IdSet.cap nf1.ncatchv nf2.ncatchv;
481
      na      = Types.cup nf1.na nf2.na;
482
483
484
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
485
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
486
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
487
		       (* assert (l1 = l2); *) RecLabel (l1, NLineProd.cup r1 r2)
488
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
489
490
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
491
		   | _ -> assert false)
492
493
494
    }

  let double_fold f l1 l2 =
495
496
497
498
499
500
    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)
501
502
	 
  let ncap nf1 nf2 =
503
    let prod accu (res1,(pl1,t1),(ql1,s1)) (res2,(pl2,t2),(ql2,s2)) =
504
505
506
507
      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
508
509
	  (fus res1 res2, (NodeSet.cup pl1 pl2,t),(NodeSet.cup ql1 ql2,s)) 
	  :: accu
510
511
512
513
514
515
    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
516
    let record r1 r2 = match r1,r2 with
517
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
518
	  (* assert (l1 = l2); *)
519
	  RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
520
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
521
522
523
524
525
526
	  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
527
	  RecNolabel (x,y)
528
      | _ -> assert false
529
    in
530
531
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
      ncatchv = IdSet.cup nf1.ncatchv nf2.ncatchv;
532
      na = Types.cap nf1.na nf2.na;
533
534
535
536
537
538
      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;
539
540
    }

541
542
543
544
  let nnode p = NodeSet.singleton p, Types.descr p.accept
  let nc t = NodeSet.empty, t
  let ncany = nc Types.any

545
  let empty_res = IdMap.empty
546

547
  let ntimes lab acc p q = 
548
549
550
    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 
551
    { nempty lab with 
552
	nfv = IdSet.cup p.fv q.fv; 
553
	na = acc;
554
	nprod = NLineProd.singleton (src, nnode p, nnode q);
555
556
    }

557
  let nxml lab acc p q = 
558
559
560
    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 
561
    { nempty lab with 
562
	nfv = IdSet.cup p.fv q.fv; 
563
	na = acc;
564
	nxml =  NLineProd.singleton (src, nnode p, nnode q);
565
566
    }
    
567
568
569
570
571
572
573
574
575
576
  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;
577
		nrecord = RecLabel(label, 
578
				 NLineProd.singleton (src,nnode p, ncany))}
579
580
581
582
583
584
585
586
	  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;
587
588
589
590
		nrecord = 
		      RecLabel(label,
		        NLineProd.singleton(src,nc Types.Record.any_or_absent, 
 			 nnode p') )}
591
592
593
	  

  let nconstr lab t =
594
595
    let aux l = NLineProd.from_list
		(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
596
597
598
599
    let record = 
      match lab with
	| None ->
	    let (x,y) = Types.Record.empty_cases t in
600
	    RecNolabel ((if x then Some empty_res else None), 
601
602
		      (if y then Some empty_res else None))
	| Some l ->
603
604
605
606
607
608
609
610
611
612
(*
	    let ppf = Format.std_formatter in
	    Format.fprintf ppf "Constr record t=%a l=%a@."
	      Types.Print.print t Label.print (LabelPool.value l);
	    let sp = Types.Record.split_normal t l in
	    List.iter (fun (t1,t2) ->
			 Format.fprintf ppf "t1=%a t2=%a@."
			   Types.Print.print t1
			   Types.Print.print t2) sp;
*)
613
	    RecLabel (l,aux (Types.Record.split_normal t l))
614
615
    in	      
    { nempty lab with
616
	na = t;
617
	nbasic = NLineBasic.singleton (empty_res, Types.cap t any_basic);
618
619
620
	nprod = aux (Types.Product.normal t);
	nxml  = aux (Types.Product.normal ~kind:`XML t);
	nrecord = record
621
622
    }

623
  let nconstant lab x c = 
624
625
626
    let l = IdMap.singleton x (SConst c) in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.empty;
627
      na = Types.any;
628
629
630
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
631
      nrecord = match lab with
632
	| None -> RecNolabel (Some l, Some l)
633
	| Some lab -> 
634
635
636
	    RecLabel (lab, NLineProd.singleton 
			(l,nc Types.Record.any_or_absent,
				 ncany))
637
638
    }

639
  let ncapture lab x = 
640
641
642
    let l = IdMap.singleton x SCatch in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.singleton x;
643
      na = Types.any;
644
645
646
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
647
      nrecord = match lab with
648
	| None -> RecNolabel (Some l, Some l)
649
	| Some lab -> 
650
651
652
	    RecLabel (lab, NLineProd.singleton 
			(l,nc Types.Record.any_or_absent,
			         ncany))
653
654
    }

655
  let rec nnormal lab (acc,fv,d) =
656
    if Types.is_empty acc 
657
    then nempty lab
658
    else match d with
659
660
      | Constr t -> nconstr lab t
      | Cap (p,q) -> ncap (nnormal lab p) (nnormal lab q)
661
      | Cup ((acc1,_,_) as p,q) -> 
662
663
664
665
666
667
668
	  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
669
      | Dummy -> assert false
670
671
672
673
674
675

(*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 
676
    then LabelPool.dummy_max
677
678
679
680
681
682
    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
683
      | _ -> LabelPool.dummy_max
684

685
686
687
   
  let remove_catchv n =
    let ncv = n.ncatchv in
688
689
690
691
    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
692
    { nfv     = IdSet.diff n.nfv ncv;
693
694
      ncatchv = n.ncatchv;
      na      = n.na;
695
696
697
      nbasic  = nlinesbasic n.nbasic;
      nprod   = nlinesprod n.nprod;
      nxml    = nlinesprod n.nxml;
698
      nrecord = (match n.nrecord with
699
		   | RecNolabel (x,y) ->
700
701
702
703
704
705
		       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
706
		       RecNolabel (x,y)
707
		   | RecLabel (lab,l) -> RecLabel (lab, nlinesprod l))
708
709
    }

710
711
712
  let print_node_list ppf pl =
    List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl

713
  let normal l t pl =
714
    remove_catchv
715
716
717
718
      (List.fold_left 
	 (fun a p -> ncap a (nnormal l (descr p))) 
	 (nconstr l t) 
	 pl)
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736

(*
  let normal l t pl =
    let nf = normal l t pl in
    (match l with Some l ->
      Format.fprintf Format.std_formatter
	"normal(l=%a;t=%a;pl=%a)=%a@." 
	Label.print (LabelPool.value l)
	Types.Print.print t
	print_node_list pl
	print nf
      | None -> Format.fprintf Format.std_formatter
	"normal(t=%a;pl=%a)=%a@." 
	Types.Print.print t
	print_node_list pl
	print nf);
    nf
*)
737
end
738
739


740
741
module Compile = 
struct
742
  type actions =
743
744
    | AIgnore of result
    | AKind of actions_kind
745
  and actions_kind = {
746
    basic: (Types.t * result) list;
747
748
    atoms: result Atoms.map;
    chars: result Chars.map;
749
    prod: result dispatch dispatch;
750
    xml: result dispatch dispatch;
751
752
753
    record: record option;
  }
  and record = 
754
    | RecLabel of label * result dispatch dispatch
755
    | RecNolabel of result option * result option
756
      
757
  and 'a dispatch =
758
759
760
761
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible
762
763

  and result = int * source array
764
  and source = 
765
766
    | Catch | Const of Types.const 
    | Left of int | Right of int | Recompose of int * int
767
768
      
  and return_code = 
769
      Types.t * int *   (* accepted type, arity *)
770
      (int * int id_map) list
771
772

  and interface =
773
774
    [ `Result of int
    | `Switch of interface * interface
775
776
777
778
    | `None ]

  and dispatcher = {
    id : int;
779
    t  : Types.t;
780
    pl : Normal.t array;
781
    label : label option;
782
783
    interface : interface;
    codes : return_code array;
784
785
    mutable actions : actions option;
    mutable printed : bool
786
  }
787

788
789
790
791
792
793
794
  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
795
      | Const x, Const y -> Types.Const.equal x y 
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
      | 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


812
813
  let array_for_all f a =
    let rec aux f a i =
814
      if i == Array.length a then true
815
816
817
818
819
820
      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 =
821
      if i == Array.length a then true
822
823
824
825
      else f i a.(i) && (aux f a (succ i))
    in
    aux f a 0

826
  let combine_kind basic prod xml record =
827
828
829
830
831
832
833
    try (
      let rs = [] in
      let rs = match basic with
	| [_,r] -> r :: rs
	| [] -> rs
	| _ -> raise Exit in
      let rs = match prod with
834
835
	| Impossible -> rs
	| Ignore (Ignore r) -> r :: rs
836
	| _ -> raise Exit in
837
      let rs = match xml with
838
839
	| Impossible -> rs
	| Ignore (Ignore r) -> r :: rs
840
	| _ -> raise Exit in
841
842
      let rs = match record with
	| None -> rs
843
844
	| Some (RecLabel (_,Ignore (Ignore r))) -> r :: rs
	| Some (RecNolabel (Some r1, Some r2)) -> r1 :: r2 :: rs
845
846
	| _ -> raise Exit in
      match rs with
847
	| ((_, ret) as r) :: rs when 
848
	    List.for_all ( equal_result r ) rs 
849
	    && array_for_all 
850
851
	      (function Catch | Const _ -> true | _ -> false) ret
	    -> AIgnore r
852
853
	| _ -> raise Exit
    )
854
855
856
857
    with Exit -> 
      AKind 
      { basic = basic;
	atoms = 
858
	  Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
859
	chars = 
860
	  Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
861
862
	prod = prod; 
	xml = xml; 
863
864
	record = record;
      }
865
      
866
867
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
868
    else
869
870
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
	 && (array_for_all ( f act.(0) ) act) then
871
	   Ignore act.(0)
872
      else
873
	Dispatch (disp, act)
874
875
876


  let detect_right_tail_call = function
877
    | Dispatch (disp,branches) 
878
879
880
	when
	  array_for_all_i
	    (fun i (code,ret) ->
881
	       (i == code) && 
882
883
	       (array_for_all_i 
		  (fun pos -> 
884
		     function Right j when pos == j -> true | _ -> false)
885
886
887
		  ret
	       )
	    ) branches
888
	  -> TailCall disp
889
890
891
    | x -> x

  let detect_left_tail_call = function
892
    | Dispatch (disp,branches)
893
894
895
896
	when
	  array_for_all_i
	    (fun i -> 
	       function 
897
		 | Ignore (code,ret) ->
898
		     (i == code) &&
899
900
		     (array_for_all_i 
			(fun pos -> 
901
			   function Left j when pos == j -> true | _ -> false)
902
903
904
905
906
			ret
	       )
		 | _ -> false
	    ) branches
 	  ->
907
	 TailCall disp
908
909
    | x -> x
   
910
911
  let cur_id = State.ref "Patterns.cur_id" 0
		 (* TODO: save dispatchers ? *)
912
		 
913
914
915
916
917
918
  module NfMap = Map.Make(
    struct 
      type t = Normal.t
      let compare = Normal.compare_nf
    end)

919
920
  module DispMap = Map.Make(
    struct
921
      type t = Types.t * Normal.t array
922
923
924
925
926
927
928
929

      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) =
930
	let c = Types.compare t1 t2 in if c <> 0 then c 
931
932
933
	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)
934
935
    end
  )
936
937

    (* Try with a hash-table ! *)
938
    
939
  let dispatchers = ref DispMap.empty
940
941
		
  let timer_disp = Stats.Timer.create "Patterns.dispatcher loop"
942
943
944
945
946
947

  let rec print_iface ppf = function
    | `Result i -> Format.fprintf ppf "Result(%i)" i
    | `Switch (yes,no) -> Format.fprintf ppf "Switch(%a,%a)"
	print_iface yes print_iface no
    |