patterns.ml 65.6 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
(* Pretty-print *)

237
module Pat = struct
238
  type t = descr
239
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
    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
271
272
273
274
275
276
277
278
279
280
281
282
283

  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
284
285
286
end

module Print = struct
287
288
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
289
290
291
292
293
294
295
296
297
298
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
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351

  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)) }) ->
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q2.descr
    | 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
352
353
354
355
356
357
358
359
360
361
362


  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 "}"
363
364
365
end


366
367
368
369

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
370
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
371
372
let times_res v1 v2 = Types.Positive.times v1 v2

373
(* Try with a hash-table *)
374
module MemoFilter = Map.Make 
375
  (struct 
376
     type t = Types.t * node 
377
378
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
379
       Types.compare t1 t2
380
   end)
381
382
383

let memo_filter = ref MemoFilter.empty

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

407
408
409
410
and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
411
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
412
       in
413
       IdMap.merge cup_res accu term
414
415
416
417
418
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)


419
and filter_node t p : Types.Positive.v id_map =
420
421
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
422
    let (_,fv,_) as d = descr p in
423
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
424
425
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
426
    IdMap.collide Types.Positive.define res r;
427
428
429
430
431
    r

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

434
435
436
437
438
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

439

440
(* Normal forms for patterns and compilation *)
441

442
443
let min (a:int) (b:int) = if a < b then a else b

444
445
446
let any_basic = Types.Record.or_absent Types.non_constructed


447
module Normal = struct
448

449
  type source = 
450
451
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
452
  type result = source id_map
453

454
455
456
457
458
459
460
  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
461
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
462
463
464
465
466
467

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
468
    | SConst c -> Types.Const.hash c
469
470
471
472
473
474
475
476
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


477
478
479
480
481
  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"

482
  module NodeSet = 
483
484
    SortedList.Make(Node)

485

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

488
489
490
491
492
493
494
495
  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
			    

496
497
  let compare_nnf (l1,t1) (l2,t2) =
    let c = NodeSet.compare l1 l2 in if c <> 0 then c
498
    else Types.compare t1 t2
499
500

  let hash_nnf (l,t) =
501
    (NodeSet.hash l) + 17 * (Types.hash t)
502
503
504
505

  module NLineBasic = 
    SortedList.Make(
      struct
506
	include Custom.Dummy
507
	let serialize s _ = failwith "Patterns.NLineBasic.serialize"
508
	type t = result * Types.t
509
510
	let compare (r1,t1) (r2,t2) =
	  let c = compare_result r1 r2 in if c <> 0 then c
511
	  else Types.compare t1 t2
512
	let equal x y = compare x y == 0
513
	let hash (r,t) = hash_result r + 17 * Types.hash t
514
515
516
517
518
519
      end
    )

  module NLineProd = 
    SortedList.Make(
      struct
520
(*	include Custom.Dummy*)
521
	let serialize s _ = failwith "Patterns.NLineProd.serialize"
522
523
524
525
526
527
528
	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
529
	type t = result * nnf * nnf
530
531
532
533
	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
534
	let equal x y = compare x y == 0
535
536
537
538
539
	let hash (r,x,y) =
	  hash_result r + 17 * (hash_nnf x) + 267 * (hash_nnf y)
      end
    )

540
  type record =
541
    | RecNolabel of result option * result option
542
    | RecLabel of label * NLineProd.t
543
  type t = {
544
    nfv    : fv;
545
    ncatchv: fv;
546
547
548
549
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
550
    nrecord: record
551
  }
552

553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
  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
      

568
569
570
571
572
573
  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
574
      else let c = Types.compare t1.na t2.na in if c <> 0 then c
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
      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
596

597
  let fus = IdMap.union_disj
598

599
600
601
  let nempty lab = 
    { nfv = IdSet.empty; ncatchv = IdSet.empty; 
      na = Types.empty;
602
603
604
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
605
      nrecord = (match lab with 
606
		   | Some l -> RecLabel (l,NLineProd.empty)
607
		   | None -> RecNolabel (None,None))
608
    }
609
  let dummy = nempty None
610
611
612
613
614
615


  let ncup nf1 nf2 = 
    (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
    (* assert (nf1.nfv = nf2.nfv); *)
    { nfv = nf1.nfv;
616
      ncatchv = IdSet.cap nf1.ncatchv nf2.ncatchv;
617
      na      = Types.cup nf1.na nf2.na;
618
619
620
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
621
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
622
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
623
		       (* assert (l1 = l2); *) RecLabel (l1, NLineProd.cup r1 r2)
624
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
625
626
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
627
		   | _ -> assert false)
628
629
630
    }

  let double_fold f l1 l2 =
631
632
633
634
635
636
    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)
637
638
	 
  let ncap nf1 nf2 =
639
    let prod accu (res1,(pl1,t1),(ql1,s1)) (res2,(pl2,t2),(ql2,s2)) =
640
641
642
643
      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
644
645
	  (fus res1 res2, (NodeSet.cup pl1 pl2,t),(NodeSet.cup ql1 ql2,s)) 
	  :: accu
646
647
648
649
650
651
    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
652
    let record r1 r2 = match r1,r2 with
653
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
654
	  (* assert (l1 = l2); *)
655
	  RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
656
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
657
658
659
660
661
662
	  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
663
	  RecNolabel (x,y)
664
      | _ -> assert false
665
    in
666
667
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
      ncatchv = IdSet.cup nf1.ncatchv nf2.ncatchv;
668
      na = Types.cap nf1.na nf2.na;
669
670
671
672
673
674
      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;
675
676
    }

677
678
679
680
  let nnode p = NodeSet.singleton p, Types.descr p.accept
  let nc t = NodeSet.empty, t
  let ncany = nc Types.any

681
  let empty_res = IdMap.empty
682

683
  let ntimes lab acc p q = 
684
685
686
    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 
687
    { nempty lab with 
688
	nfv = IdSet.cup p.fv q.fv; 
689
	na = acc;
690
	nprod = NLineProd.singleton (src, nnode p, nnode q);
691
692
    }

693
  let nxml lab acc p q = 
694
695
696
    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 
697
    { nempty lab with 
698
	nfv = IdSet.cup p.fv q.fv; 
699
	na = acc;
700
	nxml =  NLineProd.singleton (src, nnode p, nnode q);
701
702
    }
    
703
704
705
706
707
708
709
710
711
712
  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;
713
		nrecord = RecLabel(label, 
714
				 NLineProd.singleton (src,nnode p, ncany))}
715
716
717
718
719
720
721
722
	  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;
723
724
725
726
		nrecord = 
		      RecLabel(label,
		        NLineProd.singleton(src,nc Types.Record.any_or_absent, 
 			 nnode p') )}
727
728
729
	  

  let nconstr lab t =
730
731
    let aux l = NLineProd.from_list
		(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
732
733
734
735
    let record = 
      match lab with
	| None ->
	    let (x,y) = Types.Record.empty_cases t in
736
	    RecNolabel ((if x then Some empty_res else None), 
737
738
		      (if y then Some empty_res else None))
	| Some l ->
739
740
741
742
743
744
745
746
747
748
(*
	    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;
*)
749
	    RecLabel (l,aux (Types.Record.split_normal t l))
750
751
    in	      
    { nempty lab with
752
	na = t;
753
	nbasic = NLineBasic.singleton (empty_res, Types.cap t any_basic);
754
755
756
	nprod = aux (Types.Product.normal t);
	nxml  = aux (Types.Product.normal ~kind:`XML t);
	nrecord = record
757
758
    }

759
  let nconstant lab x c = 
760
761
762
    let l = IdMap.singleton x (SConst c) in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.empty;
763
      na = Types.any;
764
765
766
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
767
      nrecord = match lab with
768
	| None -> RecNolabel (Some l, Some l)
769
	| Some lab -> 
770
771
772
	    RecLabel (lab, NLineProd.singleton 
			(l,nc Types.Record.any_or_absent,
				 ncany))
773
774
    }

775
  let ncapture lab x = 
776
777
778
    let l = IdMap.singleton x SCatch in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.singleton x;
779
      na = Types.any;
780
781
782
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
783
      nrecord = match lab with
784
	| None -> RecNolabel (Some l, Some l)
785
	| Some lab -> 
786
787
788
	    RecLabel (lab, NLineProd.singleton 
			(l,nc Types.Record.any_or_absent,
			         ncany))
789
790
    }

791
  let rec nnormal lab (acc,fv,d) =
792
    if Types.is_empty acc 
793
    then nempty lab
794
    else match d with
795
796
      | Constr t -> nconstr lab t
      | Cap (p,q) -> ncap (nnormal lab p) (nnormal lab q)
797
      | Cup ((acc1,_,_) as p,q) -> 
798
799
800
801
802
803
804
	  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
805
      | Dummy -> assert false
806
807
808
809
810
811

(*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 
812
    then LabelPool.dummy_max
813
814
815
816
817
818
    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
819
      | _ -> LabelPool.dummy_max
820

821
822
823
   
  let remove_catchv n =
    let ncv = n.ncatchv in
824
825
826
827
    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
828
    { nfv     = IdSet.diff n.nfv ncv;
829
830
      ncatchv = n.ncatchv;
      na      = n.na;
831
832
833
      nbasic  = nlinesbasic n.nbasic;
      nprod   = nlinesprod n.nprod;
      nxml    = nlinesprod n.nxml;
834
      nrecord = (match n.nrecord with
835
		   | RecNolabel (x,y) ->
836
837
838
839
840
841
		       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
842
		       RecNolabel (x,y)
843
		   | RecLabel (lab,l) -> RecLabel (lab, nlinesprod l))
844
845
    }

846
847
848
  let print_node_list ppf pl =
    List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl

849
  let normal l t pl =
850
    remove_catchv
851
852
853
854
      (List.fold_left 
	 (fun a p -> ncap a (nnormal l (descr p))) 
	 (nconstr l t) 
	 pl)
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872

(*
  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
*)
873
end
874
875


876
877
module Compile = 
struct
878
  type actions =
879
880
    | AIgnore of result
    | AKind of actions_kind
881
  and actions_kind = {
882
    basic: (Types.t * result) list;
883
884
    atoms: result Atoms.map;
    chars: result Chars.map;
885
    prod: result dispatch dispatch;
886
    xml: result dispatch dispatch;
887
888
889
    record: record option;
  }
  and record = 
890
    | RecLabel of label * result dispatch dispatch
891
    | RecNolabel of result option * result option
892
      
893
  and 'a dispatch =
894
895
896
897
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible
898
899

  and result = int * source array
900
  and source = 
901
902
    | Catch | Const of Types.const 
    | Left of int | Right of int | Recompose of int * int
903
904
      
  and return_code = 
905
      Types.t * int *   (* accepted type, arity *)
906
      (int * int id_map) list
907
908

  and interface =
909
910
    [ `Result of int
    | `Switch of interface * interface
911
912
913
914
    | `None ]

  and dispatcher = {
    id : int;
915
    t  : Types.t;
916
    pl : Normal.t array;
917
    label : label option;
918
919
    interface : interface;
    codes : return_code array;
920
921
    mutable actions : actions option;
    mutable printed : bool
922
  }
923

924
925
926
927
928
929
930
  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
931
      | Const x, Const y -> Types.Const.equal x y 
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
      | 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


948
949
  let array_for_all f a =
    let rec aux f a i =
950
      if i == Array.length a then true
951
952
953
954
955
956
      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 =
957
      if i == Array.length a then true
958
959
960
961
      else f i a.(i) && (aux f a (succ i))
    in
    aux f a 0

962
  let combine_kind basic prod xml record =
963
964
965
966
967
968
969
    try (
      let rs = [] in
      let rs = match basic with
	| [_,r] -> r :: rs
	| [] -> rs
	| _ -> raise Exit in
      let rs = match prod with
970
971
	| Impossible -> rs
	| Ignore (Ignore r) -> r :: rs
972
	| _ -> raise Exit in
973
      let rs = match xml with
974
975
	| Impossible -> rs
	| Ignore (Ignore r) -> r :: rs
976
	| _ -> raise Exit in
977
978
      let rs = match record with
	| None -> rs
979
980
	| Some (RecLabel (_,Ignore (Ignore r))) -> r :: rs
	| Some (RecNolabel (Some r1, Some r2)) -> r1 :: r2 :: rs
981
982
	| _ -> raise Exit in
      match rs with
983
	| ((_, ret) as r) :: rs when 
984
	    List.for_all ( equal_result r ) rs 
985
	    && array_for_all 
986
987
	      (function Catch | Const _ -> true | _ -> false) ret
	    -> AIgnore r
988
989
	| _ -> raise Exit
    )
990
991
992
993
    with Exit -> 
      AKind 
      { basic = basic;
	atoms = 
994
	  Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
995
	chars = 
996
	  Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
997
998
	prod = prod; 
	xml = xml; 
999
1000
	record = record;
      }