patterns.ml 70.2 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" Ident.print x
63
    | Constant (x,c) ->
64
	Format.fprintf ppf "(%a := %a)" Ident.print 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 " ^ (Ident.to_string 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 " ^ (Ident.to_string 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
297
298

  let serialize _ _ = assert false
  let deserialize _ = assert false
  let check _ = assert false
  let dump _ = assert false
299
300
301
end

module Print = struct
302
303
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
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
335
336
337
338
339

  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)) }) ->
340
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q3.descr
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
    | 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
367
368
369
370
371
372
373
374
375
376
377


  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 "}"
378
379
380
end


381
382
383
384

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
385
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
386
387
let times_res v1 v2 = Types.Positive.times v1 v2

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

let memo_filter = ref MemoFilter.empty

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

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


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

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
447
  IdMap.map Types.Positive.solve r
448
449
450
451
452
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

453

454
455
456
(* Factorization of capture variables and constant patterns *)

module Factorize = struct
457
458
  module NodeTypeSet = Set.Make(Custom.Pair(Node)(Types))

459
460
461
462
463
464
465
466
467
468
469
470
471
472
  let pi1 ~kind t = Types.Product.pi1 (Types.Product.get ~kind t)
  let pi2 ~kind t = Types.Product.pi2 (Types.Product.get ~kind t)

(* Note: this is incomplete because of non-atomic constant patterns:
# debug approx (_,(x:=(1,2))) (1,2);;
[DEBUG:approx]
x=(1,2)
*)
  let rec approx_var seen ((a,fv,d) as p) t xs =
(*    assert (Types.subtype t a); 
      assert (IdSet.subset xs fv); *)
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
473
	  approx_var seen p2 (Types.diff t a1)
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
	    (approx_var seen p1 (Types.cap t a1) xs) 
      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
	  IdSet.cup
	    (approx_var seen p1 t (IdSet.cap fv1 xs))
	    (approx_var seen p2 t (IdSet.cap fv2 xs))
      | Capture _ ->
	  xs
      | Constant (_,c) -> 
	  if (Types.subtype t (Types.constant c)) then xs else IdSet.empty
      | Times (q1,q2) ->
	  let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
	  IdSet.cap
	    (approx_var_node seen q1 (pi1 ~kind:`Normal t) xs)
	    (approx_var_node seen q2 (pi2 ~kind:`Normal t) xs)
      | Xml (q1,q2) ->
	  let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
	  IdSet.cap
	    (approx_var_node seen q1 (pi1 ~kind:`XML t) xs)
	    (approx_var_node seen q2 (pi2 ~kind:`XML t) xs)
      | Record _ -> IdSet.empty
      | _ -> assert false
	  
  and approx_var_node seen q t xs =
497
    if (NodeTypeSet.mem (q,t) seen) 
498
    then xs
499
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
500
      
501
502

(* Obviously not complete ! *)      
503
  let rec approx_nil seen ((a,fv,d) as p) t xs =
504
505
    assert (Types.subtype t a); 
    assert (IdSet.subset xs fv);
506
507
508
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
509
	  approx_nil seen p2 (Types.diff t a1)
510
511
512
513
514
515
516
517
518
519
520
521
	    (approx_nil seen p1 (Types.cap t a1) xs) 
      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
	  IdSet.cup
	    (approx_nil seen p1 t (IdSet.cap fv1 xs))
	    (approx_nil seen p2 t (IdSet.cap fv2 xs))
      | Constant (_,c) when Types.Const.equal c Sequence.nil_cst -> xs
      | Times (q1,q2) ->
	  let xs = IdSet.cap q2.fv (IdSet.diff xs q1.fv) in
	  approx_nil_node seen q2 (pi2 ~kind:`Normal t) xs
      | _ -> IdSet.empty
	  
  and approx_nil_node seen q t xs =
522
    if (NodeTypeSet.mem (q,t) seen) 
523
    then xs
524
    else approx_nil (NodeTypeSet.add (q,t) seen) q.descr t xs
525
526
527
528
529
530
531
532
533
534
535
536
537
538

  let cst ((a,_,_) as p) t xs =
    if IdSet.is_empty xs then IdMap.empty
    else
      let rec aux accu (x,t) =
	if (IdSet.mem xs x) then
	  match Sample.single_opt (Types.descr t) with
	    | Some c -> (x,c)::accu
	    | None -> accu
	else accu in
      let t = Types.cap t a in
      IdMap.from_list_disj (List.fold_left aux [] (filter_descr t p))
	
  let var ((a,_,_) as p) t = 
539
    approx_var NodeTypeSet.empty p (Types.cap t a)
540
541

  let nil ((a,_,_) as p) t = 
542
    approx_nil NodeTypeSet.empty p (Types.cap t a)
543
544
545
546
547
end




548
549
(* Normal forms for patterns and compilation *)

550
551
let min (a:int) (b:int) = if a < b then a else b

552
553
let any_basic = Types.Record.or_absent Types.non_constructed

554
555
556
557
558
559
560
561
562
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
563

564
module Normal = struct
565

566
  type source = 
567
568
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
569
  type result = source id_map
570

571
572
573
574
575
576
577
  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
578
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
579
580
581
582
583
584

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
585
    | SConst c -> Types.Const.hash c
586
587
588
589
590
591
592
593
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


594
595
596
597
598
  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"

599
  module NodeSet = SortedList.Make(Node)
600

601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
  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
616
617
618
619
620
621
622


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

625
626
627
628
629
630
631
632
633
634
  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
635
636


637
638
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
639

640
641
642
643
644
645
    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
646

647
648
649
650
651
652
653
    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
654

655
656
  module NLineBasic = SortedList.Make(NBasic)
  module NLineProd = SortedList.Make(NProd)
657

658
  type record =
659
    | RecNolabel of result option * result option
660
    | RecLabel of label * NLineProd.t
661
  type t = {
662
    nfv    : fv;
663
664
665
666
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
667
    nrecord: record
668
669
  }

670
671
672
673
674
675
676
677
678
679
  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 =
680
    Format.fprintf ppf "@[NF{na=%a;@ @[nprod=@ @[%a@]@]};@ @[nrecord=@ @[%a@]@]}@]" 
681
      Types.Print.print nf.na
682
      NLineProd.dump nf.nprod
683
684
685
      print_record nf.nrecord
      

686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
  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 =
703
704
705
706
    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 
707
      else let c = Types.compare t1.na t2.na in if c <> 0 then c
708
709
710
      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
711
      else compare_record t1.nrecord t2.nrecord
712

713
  let fus = IdMap.union_disj
714

715
  let nempty lab = 
716
    { nfv = IdSet.empty; 
717
      na = Types.empty;
718
719
720
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
721
      nrecord = (match lab with 
722
		   | Some l -> RecLabel (l,NLineProd.empty)
723
		   | None -> RecNolabel (None,None))
724
    }
725
  let dummy = nempty None
726
727
728
729
730
731
732


  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;
733
734
735
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
736
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
737
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
738
739
		       (* assert (l1 = l2); *) 
		       RecLabel (l1, NLineProd.cup r1 r2)
740
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
741
742
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
743
		   | _ -> assert false)
744
745
746
    }

  let double_fold f l1 l2 =
747
748
749
750
751
752
    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)
753
754
	 
  let ncap nf1 nf2 =
755
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
756
757
758
759
      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
760
761
762
	  (fus res1 res2, 
	   (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
	   (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) 
763
	  :: accu
764
765
766
767
768
769
    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
770
    let record r1 r2 = match r1,r2 with
771
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
772
	  (* assert (l1 = l2); *)
773
	  RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
774
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
775
776
777
778
779
780
	  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
781
	  RecNolabel (x,y)
782
      | _ -> assert false
783
    in
784
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
785
      na = Types.cap nf1.na nf2.na;
786
787
788
789
790
791
      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;
792
793
    }

794
795
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
796
  let ncany = nc Types.any
797
  let ncany_abs = nc Types.Record.any_or_absent
798

799
  let empty_res = IdMap.empty
800

801
802
803
804
805
806
807
  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
808
    let src = IdMap.merge_elem SRecompose src_p src_q in 
809
    { (nempty lab) with 
810
	nfv = xs;
811
	na = acc;
812
	nprod = single_prod src (nnode p xsp) (nnode q xsq)
813
814
    }

815
816
817
818
  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
819
    let src = IdMap.merge_elem SRecompose src_p src_q in 
820
    { (nempty lab) with 
821
	nfv = xs;
822
	na = acc;
823
	nxml =  single_prod src (nnode p xsp) (nnode q xsq)
824
825
    }
    
826
  let nrecord lab acc l p xs =
827
828
829
830
    match lab with
      | None -> assert false
      | Some label ->
	  assert (label <= l);
831
832
833
834
835
836
	  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
837
	  { (nempty lab) with
838
839
840
	      nfv = xs;
	      na = acc;
	      nrecord = RecLabel(label, single_prod src lft rgt) }
841
842

  let nconstr lab t =
843
844
    let aux l = NLineProd.from_list
		(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
845
846
847
848
    let record = match lab with
      | None ->
	  let (x,y) = Types.Record.empty_cases t in
	  RecNolabel ((if x then Some empty_res else None), 
849
		      (if y then Some empty_res else None))
850
      | Some l ->
851
	  RecLabel (l,aux (Types.Record.split_normal t l)) in
852
    { (nempty lab) with
853
	na = t;
854
	nbasic = single_basic empty_res (Types.cap t any_basic);
855
856
857
	nprod = aux (Types.Product.normal t);
	nxml  = aux (Types.Product.normal ~kind:`XML t);
	nrecord = record
858
859
    }

860
861
  let nany lab res =
    { nfv = IdMap.domain res;
862
      na = Types.any;
863
864
865
      nbasic = single_basic res any_basic;
      nprod  = single_prod res ncany ncany;
      nxml   = single_prod res ncany ncany;
866
      nrecord = match lab with
867
868
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
869
870
    }

871
872
873
874
875
  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
876
(*
877
878
879
880
    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);
881
*)
882
883
    if Types.is_empty acc then nempty lab
    else if IdSet.is_empty xs then nconstr lab acc
884
    else match d with
885
886
      | Constr t -> assert false
      | Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
887
      | Cup ((acc1,_,_) as p,q) -> 
888
889
890
891
892
	  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
893
894
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
895
      | Record (l,p) -> nrecord lab acc l p xs
896
      | Dummy -> assert false
897
898
899
900
901

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


902
   
903
904
905
  let print_node_list ppf pl =
    List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl

906
  let facto f t xs pl =
907
    List.fold_left 
908
909
      (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
      IdSet.empty
910
      pl
911

912
  let normal f l t pl xs =
913
914
    let a = nconstr l t in

915
916
917
918
919
920
921
    let vs_var = facto Factorize.var t xs pl in
    let xs = IdSet.diff xs vs_var in
    let vs_var,a =
      if f then vs_var,a
      else
	IdSet.empty,
	List.fold_left (fun a x -> ncap a (ncapture l x)) a vs_var in
922

923
924
925
926
927
928
929
930
    let vs_nil = facto Factorize.nil t xs pl in
    let xs = IdSet.diff xs vs_nil in
    let vs_nil,a =
      if f then vs_nil,a
      else
	IdSet.empty,
	List.fold_left 
	  (fun a x -> ncap a (nconstant l x Sequence.nil_cst)) a vs_nil in
931

932
    vs_var,vs_nil,
933
934
    List.fold_left (fun a p -> ncap a (nnormal l (descr p) xs)) a pl

935
  let nnf facto lab t0 (pl,t,xs) = 
936
937
938
939
    let t =
      if Types.subtype t t0 then t else Types.cap t t0 in
(*    let ppf = Format.std_formatter in
     Format.fprintf ppf "normal nnf=%a@." Nnf.print (pl,t,xs); *)
940
    normal facto lab t (NodeSet.get pl) xs
941
942
    

943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
(*
  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
*)
960
end
961
962


963
964
module Compile = 
struct
965
  type actions =
966
967
    | AIgnore of result
    | AKind of actions_kind
968
  and actions_kind = {
969
    basic: (Types.t * result) list;
970
971
    atoms: result Atoms.map;
    chars: result Chars.map;
972
    prod: result dispatch dispatch;
973
    xml: result dispatch dispatch;
974
975
976
    record: record option;
  }
  and record = 
977
    | RecLabel of label * result dispatch dispatch
978
    | RecNolabel of result option * result option
979
      
980
  and 'a dispatch =
981
982
983
984
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible
985

986
  and result = int * source array * int
987
  and source = 
988
    | Catch | Const of Types.const 
989
    | Stack of int | Left | Right | Nil | Recompose of int * int
990
991
      
  and return_code = 
992
      Types.t * int *   (* accepted type, arity *)
993
      int id_map option array
994
995

  and interface =
996
997
    [ `Result of int
    | `Switch of interface * interface
998
999
1000
1001
    | `None ]

  and dispatcher = {
    id : int;
1002
    t  : Types.t;
1003
    pl : Normal.t array;
1004
    label : label option;
1005
1006
    interface : interface;
    codes : return_code array;
1007
1008
    mutable actions : actions option;
    mutable printed : bool
1009
  }
1010

1011
1012
  let types_of_codes d = Array.map (fun (t,ar,_) -> t) d.codes

1013
1014
1015
1016
1017
  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))

1018
1019
1020
1021
1022
1023
1024
1025
  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)