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

4
5
6
7
8
let print_lab ppf l = 
  if (l == LabelPool.dummy_max) 
  then Format.fprintf ppf "<dummy_max>"
  else Label.print ppf (LabelPool.value l)

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

18

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


39

40
let id x = x.id
41
let descr x = x.descr
42
43
let fv x = x.fv
let accept x = Types.internalize x.accept
44
45
46

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

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

83
84
85
86
87
let print_node ppf n =
  Format.fprintf ppf "P%i" n.id;
  to_print := n :: !to_print;
  dump_print ppf

88

89
90
let counter = State.ref "Patterns.counter" 0

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

let define x ((accept,fv,_) as d) =
97
  (* assert (x.fv = fv); *)
98
  Types.define x.accept accept;
99
  x.descr <- d
100

101
102
103
104
105
let cons fv d =
  let q = make fv in
  define q d;
  q

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

140

141
142
143
144
145
146
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

147
  let check n = ()
148
  let dump = print_node
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
197
198
199
200
201
202
203
204
205
206

  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;
207
      let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in
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
239
240
241
242
243
      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
244

245
246
(* Pretty-print *)

247
module Pat = struct
248
  type t = descr
249
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
    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) ->
	  let c = LabelPool.compare x1 x2 in if c <> 0 then c
	  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
281
282
283
284
285
286
287
288
289
290
291
292
293

  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
    | Record (l,q) -> 6 + 17 * (LabelPool.hash l) + 257 * q.id
    | Capture x -> 7 + (Id.hash x)
    | Constant (x,c) -> 8 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
    | Dummy -> assert false
294
295
296
end

module Print = struct
297
298
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334

  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)) }) ->
335
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q3.descr
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
    | Xml _ -> assert false
    | Record (l,q) ->
	Format.fprintf ppf "{%a=%a}" Label.print (LabelPool.value l) print q.descr
    | 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
362
363
364
365
366
367
368
369
370
371
372


  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 "}"
373
374
375
end


376
377
378
379

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
380
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
381
382
let times_res v1 v2 = Types.Positive.times v1 v2

383
(* Try with a hash-table *)
384
module MemoFilter = Map.Make 
385
  (struct 
386
     type t = Types.t * node 
387
388
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
389
       Types.compare t1 t2
390
   end)
391
392
393

let memo_filter = ref MemoFilter.empty

394
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
395
(* TODO: avoid is_empty t when t is not changing (Cap) *)
396
397
398
399
  if Types.is_empty t 
  then empty_res fv
  else
    match d with
400
      | Constr _ -> IdMap.empty
401
      | Cup ((a,_,_) as d1,d2) ->
402
	  IdMap.merge cup_res
403
404
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
405
      | Cap (d1,d2) ->
406
	  IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
407
408
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
409
410
411
      | Record (l,p) ->
	  filter_node (Types.Record.project t l) p
      | Capture c ->
412
	  IdMap.singleton c (Types.Positive.ty t)
413
      | Constant (c, cst) ->
414
	  IdMap.singleton c (Types.Positive.ty (Types.constant cst))
415
      | Dummy -> assert false
416

417
418
419
420
and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
421
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
422
       in
423
       IdMap.merge cup_res accu term
424
425
426
427
428
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)


429
and filter_node t p : Types.Positive.v id_map =
430
431
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
432
    let (_,fv,_) as d = descr p in
433
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
434
435
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
436
    IdMap.collide Types.Positive.define res r;
437
438
439
440
441
    r

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

444
445
446
447
448
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

449

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
458
459
460
461
462
463
464
let rec first_label (acc,fv,d) =
  if Types.is_empty acc 
  then LabelPool.dummy_max
  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)
    | Record (l,p) -> l
    | _ -> LabelPool.dummy_max
465

466
module Normal = struct
467

468
  type source = 
469
470
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
471
  type result = source id_map
472

473
474
475
476
477
478
479
  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
480
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
481
482
483
484
485
486

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
487
    | SConst c -> Types.Const.hash c
488
489
490
491
492
493
494
495
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


496
497
498
499
500
  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"

501
  module NodeSet = SortedList.Make(Node)
502

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


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

527
528
529
530
531
532
533
534
535
536
  module NBasic = struct
    include Custom.Dummy
    let serialize s _ = failwith "Patterns.NLineBasic.serialize"
    type t = result * Types.t
    let compare (r1,t1) (r2,t2) =
      let c = compare_result r1 r2 in if c <> 0 then c
      else Types.compare t1 t2
    let equal x y = compare x y == 0
    let hash (r,t) = hash_result r + 17 * Types.hash t
  end
537
538


539
540
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
541

542
543
544
545
546
547
    let serialize s _ = failwith "Patterns.NLineProd.serialize"
    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 Nnf.print x Nnf.print y
548

549
550
551
552
553
554
555
    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
    let equal x y = compare x y == 0
    let hash (r,x,y) = hash_result r + 17 * (Nnf.hash x) + 267 * (Nnf.hash y)
  end
556

557
558
  module NLineBasic = SortedList.Make(NBasic)
  module NLineProd = SortedList.Make(NProd)
559

560
  type record =
561
    | RecNolabel of result option * result option
562
    | RecLabel of label * NLineProd.t
563
  type t = {
564
    nfv    : fv;
565
566
567
568
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
569
    nrecord: record
570
  }
571

572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
  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
      

587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
  include Custom.Dummy
  let compare_record t1 t2 = match t1,t2 with
    | RecNolabel (s1,n1), RecNolabel (s2,n2) ->
	(match (s1,s2,n1,n2) with
	   | Some r1, Some r2, _, _ -> compare_result r1 r2
	   | None, Some _, _, _ -> -1
	   | Some _, None, _, _ -> 1
	   | None,None,Some r1, Some r2 -> compare_result r1 r2
	   | None,None,None, Some _ -> -1
	   | None,None, Some _, None -> 1
	   | None,None, None, None -> 0)
    | 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
  let compare t1 t2 =
604
605
606
607
    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 
608
      else let c = Types.compare t1.na t2.na in if c <> 0 then c
609
610
611
      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
612
      else compare_record t1.nrecord t2.nrecord
613

614
  let fus = IdMap.union_disj
615

616
  let nempty lab = 
617
    { nfv = IdSet.empty; 
618
      na = Types.empty;
619
620
621
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
622
      nrecord = (match lab with 
623
		   | Some l -> RecLabel (l,NLineProd.empty)
624
		   | None -> RecNolabel (None,None))
625
    }
626
  let dummy = nempty None
627
628
629
630
631
632
633


  let ncup nf1 nf2 = 
    (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
    (* assert (nf1.nfv = nf2.nfv); *)
    { nfv = nf1.nfv;
      na      = Types.cup nf1.na nf2.na;
634
635
636
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
637
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
638
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
639
		       (* assert (l1 = l2); *) RecLabel (l1, NLineProd.cup r1 r2)
640
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
641
642
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
643
		   | _ -> assert false)
644
645
646
    }

  let double_fold f l1 l2 =
647
648
649
650
651
652
    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)
653
654
	 
  let ncap nf1 nf2 =
655
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
656
657
658
659
      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
660
661
662
	  (fus res1 res2, 
	   (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
	   (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) 
663
	  :: accu
664
665
666
667
668
669
    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
670
    let record r1 r2 = match r1,r2 with
671
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
672
	  (* assert (l1 = l2); *)
673
	  RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
674
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
675
676
677
678
679
680
	  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
681
	  RecNolabel (x,y)
682
      | _ -> assert false
683
    in
684
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
685
      na = Types.cap nf1.na nf2.na;
686
687
688
689
690
691
      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;
692
693
    }

694
695
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
696
  let ncany = nc Types.any
697
  let ncany_abs = nc Types.Record.any_or_absent
698

699
  let empty_res = IdMap.empty
700

701
702
703
704
705
706
707
  let single_basic src t = NLineBasic.singleton (src, t)
  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
    let src_p = IdMap.constant SLeft xsp
    and src_q = IdMap.constant SRight xsq in
708
    let src = IdMap.merge_elem SRecompose src_p src_q in 
709
    { nempty lab with 
710
	nfv = xs;
711
	na = acc;
712
	nprod = single_prod src (nnode p xsp) (nnode q xsq)
713
714
    }

715
716
717
718
  let nxml lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
    let src_p = IdMap.constant SLeft xsp
    and src_q = IdMap.constant SRight xsq in
719
    let src = IdMap.merge_elem SRecompose src_p src_q in 
720
    { nempty lab with 
721
	nfv = xs;
722
	na = acc;
723
	nxml =  single_prod src (nnode p xsp) (nnode q xsq)
724
725
    }
    
726
727
  let nrecord lab acc l p xs =
    assert (IdSet.equal xs (fv p));
728
729
730
731
    match lab with
      | None -> assert false
      | Some label ->
	  assert (label <= l);
732
733
734
735
736
737
738
739
740
741
	  let src,lft,rgt =
	    if l == label
	    then SLeft, nnode p xs, ncany
	    else SRight, ncany_abs, nnode (cons p.fv (record l p)) xs
	  in
	  let src = IdMap.constant src xs in
	  { nempty lab with
	      nfv = xs;
	      na = acc;
	      nrecord = RecLabel(label, single_prod src lft rgt) }
742
743

  let nconstr lab t =
744
745
    let aux l = NLineProd.from_list
		(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
746
747
748
749
    let record = match lab with
      | None ->
	  let (x,y) = Types.Record.empty_cases t in
	  RecNolabel ((if x then Some empty_res else None), 
750
		      (if y then Some empty_res else None))
751
752
      | Some l ->
	  RecLabel (l,aux (Types.Record.split_normal t l)) in
753
    { nempty lab with
754
	na = t;
755
	nbasic = single_basic empty_res (Types.cap t any_basic);
756
757
758
	nprod = aux (Types.Product.normal t);
	nxml  = aux (Types.Product.normal ~kind:`XML t);
	nrecord = record
759
760
    }

761
762
  let nany lab res =
    { nfv = IdMap.domain res;
763
      na = Types.any;
764
765
766
      nbasic = single_basic res any_basic;
      nprod  = single_prod res ncany ncany;
      nxml   = single_prod res ncany ncany;
767
      nrecord = match lab with
768
769
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
770
771
    }

772
773
774
775
776
777
778
779
780
781
782
  let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
  let ncapture lab x = nany lab (IdMap.singleton x SCatch)

  let rec nnormal lab ((acc,fv,d) as p) xs =
    let xs = IdSet.cap xs fv in
    if not (IdSet.equal xs fv) then
      (Format.fprintf Format.std_formatter
	 "ERR: p=%a  xs=%a  fv=%a@." Print.print p Print.print_xs xs Print.print_xs fv;
       exit 1);
    if Types.is_empty acc then nempty lab
    else if IdSet.is_empty xs then nconstr lab acc
783
    else match d with
784
785
      | Constr t -> assert false
      | Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
786
      | Cup ((acc1,_,_) as p,q) -> 
787
788
789
790
791
	  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
792
793
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
794
      | Record (l,p) -> nrecord lab acc l p xs
795
      | Dummy -> assert false
796
797
798
799
800

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


801
   
802
803
804
  let print_node_list ppf pl =
    List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl

805
806
807
808
809
  let normal l t pl xs =
    List.fold_left 
      (fun a p -> ncap a (nnormal l (descr p) xs)) 
      (nconstr l t) 
      pl
810

811
812
813
814
815
  let nnf lab (pl,t,xs) =
    let pl = NodeSet.get pl in
    normal lab t pl xs
    

816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
(*
  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
*)
833
end
834
835


836
837
module Compile = 
struct
838
  type actions =
839
840
    | AIgnore of result
    | AKind of actions_kind
841
  and actions_kind = {
842
    basic: (Types.t * result) list;
843
844
    atoms: result Atoms.map;
    chars: result Chars.map;
845
    prod: result dispatch dispatch;
846
    xml: result dispatch dispatch;
847
848
849
    record: record option;
  }
  and record = 
850
    | RecLabel of label * result dispatch dispatch
851
    | RecNolabel of result option * result option
852
      
853
  and 'a dispatch =
854
855
856
857
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible
858
859

  and result = int * source array
860
  and source = 
861
862
    | Catch | Const of Types.const 
    | Left of int | Right of int | Recompose of int * int
863
864
      
  and return_code = 
865
      Types.t * int *   (* accepted type, arity *)
866
      int id_map option array
867
868

  and interface =
869
870
    [ `Result of int
    | `Switch of interface * interface
871
872
873
874
    | `None ]

  and dispatcher = {
    id : int;
875
    t  : Types.t;
876
    pl : Normal.t array;
877
    label : label option;
878
879
    interface : interface;
    codes : return_code array;
880
881
    mutable actions : actions option;
    mutable printed : bool
882
  }
883

884
885
886
887
888
  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))

889
890
891
892
893
894
895
896
  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)

897
898
  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
899
      | Const x, Const y -> Types.Const.equal x y 
900
901
902
903
904
905
906
907
      | 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)

908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
  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 =
    let res = ref None in
    let chk = function Catch | Const _ -> true | _ -> false in
    let f ((_,ret) as r) =
      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;
    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
    chars = Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
    prod = prod; 
    xml = xml; 
    record = record
  }
941

942
  let combine_kind basic prod xml record =
943
944
    try AIgnore (immediate_res basic prod xml record)
    with Exit -> AKind (split_kind basic prod xml record)
945
      
946
947
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
948
    else
949
950
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
	 && (array_for_all ( f act.(0) ) act) then
951
	   Ignore act.(0)
952
      else
953
	Dispatch (disp, act)
954

955
956
  let detect_tail_call f = function
    | Dispatch (disp,branches) when array_for_all_i f branches -> TailCall disp
957
958
    | x -> x

959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
  let detect_right_tail_call =
    detect_tail_call
      (fun i (code,ret) ->
	 (i == code) && 
	   (array_for_all_i 
	      (fun pos -> 
		 function Right j when pos == j -> true | _ -> false)
	      ret
	   )
      )

  let detect_left_tail_call =
    detect_tail_call
      (fun i -> 
	 function 
	   | Ignore (code,ret) when (i == code) ->
	       array_for_all_i 
		 (fun pos -> 
		    function Left j when pos == j -> true | _ -> false)
		 ret
	   | _ -> false
      )
981
   
982
983
  let cur_id = State.ref "Patterns.cur_id" 0
		 (* TODO: save dispatchers ? *)
984
		 
985
  module NfMap = Map.Make(Normal)
986
  module NfSet = Set.Make(Normal)
987
988

  module DispMap = Map.Make(Custom.Pair(Types)(Custom.Array(Normal)))
989
990

    (* Try with a hash-table ! *)
991
    
992
  let dispatchers = ref DispMap.empty
993
994
		
  let timer_disp = Stats.Timer.create "Patterns.dispatcher loop"
995
996
997
998
999
1000

  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
    | `None -> Format.fprintf ppf "None"
1001
      
1002
  let dispatcher t pl lab : dispatcher =
1003
1004
    try DispMap.find (t,pl) !dispatchers
    with Not_found ->
1005
      let nb = ref 0 in
1006
1007
      let codes = ref [] in
      let rec aux t arity i accu = 
1008
	if i == Array.length pl 
1009
1010
	then (incr nb; let r = Array.of_list (List.rev accu) in 
	      codes := (t,arity,r)::!codes; `Result (!nb - 1))
1011
	else
1012
1013
1014
1015
1016
	  let p = pl.(i) in
	  let tp = p.Normal.na in

	  let a1 = Types.cap t tp in
	  if Types.is_empty a1 then
1017
	    `Switch (`None,aux t arity (i+1) (None::accu))
1018
	  else
1019
	    let v = p.Normal.nfv in
1020
	    let a2 = Types.diff t tp in
1021
	    let accu' = Some (IdMap.num arity v) :: accu in
1022
1023
1024
1025
	    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',
1026
		       aux a2 arity (i+1) (None::accu))
1027