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

4
let get_opt = function Some x -> x | None -> assert false
5

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

15

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

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.pp_type ppf t
45 46
    | Cup (p1,p2) -> Format.fprintf ppf "(%a | %a)" print p1 print p2
    | Cap (p1,p2) -> Format.fprintf ppf "(%a & %a)" print p1 print p2
47
    | Times (n1,n2) ->
48 49
	Format.fprintf ppf "(P%i,P%i)" n1.id n2.id;
	to_print := n1 :: n2 :: !to_print
50
    | Xml (n1,n2) ->
51 52
	Format.fprintf ppf "XML(P%i,P%i)" n1.id n2.id;
	to_print := n1 :: n2 :: !to_print
53
    | Record (l,n) ->
54
	Format.fprintf ppf "{ %a =  P%i }" Label.print_attr l n.id;
55 56
	to_print := n :: !to_print
    | Capture x ->
57
	Format.fprintf ppf "%a" Ident.print x
58
    | Constant (x,c) ->
59
	Format.fprintf ppf "(%a := %a)" Ident.print x
60
	  Types.Print.pp_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

Julien Lopez's avatar
Julien Lopez committed
83 84 85
let pp_v ppf (id, name) =
  Format.fprintf ppf "(%d,%s)" (Upool.int id) (Encodings.Utf8.to_string name)

Pietro Abate's avatar
Pietro Abate committed
86
let pp_fv ppf fv = Utils.pp_list ~delim:("","") pp_v ppf fv
Julien Lopez's avatar
Julien Lopez committed
87 88 89 90 91 92

let pp_node ppf node =
  Format.fprintf ppf "id:%d; descr:[%a]; accept:[id:%d; descr:%a]; fv:[%a]"
    node.id
    print node.descr
    (Types.id node.accept)
93
    Types.Print.pp_type (Types.descr node.accept)
94
    pp_fv (node.fv :> Id.t list)
95

96
let counter = ref 0
97

98
let dummy = (Types.empty,IdSet.empty,Dummy)
99 100
let make fv =
  incr counter;
101
  { id = !counter; descr = dummy; accept = Types.make (); fv = fv }
102 103

let define x ((accept,fv,_) as d) =
104
  (* assert (x.fv = fv); *)
105
  Types.define x.accept accept;
106
  x.descr <- d
107

108 109 110 111 112
let cons fv d =
  let q = make fv in
  define q d;
  q

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

143

144 145
let print_node = ref (fun _ _ -> assert false)

146 147 148 149 150 151
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

152
  let check n = ()
153
  let dump ppf x = !print_node ppf x
154
end
155

156 157
(* Pretty-print *)

158
module Pat = struct
159
  type t = descr
160
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
161 162 163 164 165
    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) ->
166
	  let c = compare x1 x2 in if c <> 0 then c
167 168 169 170 171 172 173 174 175 176 177
	  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) ->
178
	  let c = Label.compare x1 x2 in if c <> 0 then c
179 180 181 182 183 184 185 186 187 188 189 190 191
	  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
192 193 194 195 196 197 198 199 200

  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
201
    | Record (l,q) -> 6 + 17 * (Label.hash l) + 257 * q.id
202 203 204
    | Capture x -> 7 + (Id.hash x)
    | Constant (x,c) -> 8 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
    | Dummy -> assert false
205 206 207

  let check _ = assert false
  let dump _ = assert false
208 209 210
end

module Print = struct
211 212
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
213 214 215 216 217 218 219 220 221 222 223 224

  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)
225
    else
226 227 228 229 230 231 232 233
      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 =
234
    try
235 236 237 238 239 240
      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 ->
241
	Types.Print.pp_type ppf t
242 243 244 245 246 247 248
    | 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)) }) ->
249
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q3.descr
250 251
    | Xml _ -> assert false
    | Record (l,q) ->
252
	Format.fprintf ppf "{%a=%a}" Label.print_attr l print q.descr
253 254 255
    | Capture x ->
	Format.fprintf ppf "%a" Ident.print x
    | Constant (x,c) ->
256
	Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.pp_const c
257
    | Dummy -> assert false
258

259
  let pp ppf p =
260 261 262 263 264
    mark S.empty p;
    print ppf p;
    let first = ref true in
    (try while true do
       let p = Queue.pop toprint in
265
       if not (S.mem p !printed) then
266 267 268 269 270 271 272 273 274 275
	 ( 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
276 277 278 279 280 281 282 283 284 285

  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 "}"
286 287 288

  let printf = pp Format.std_formatter
  let string_of_pattern t = Utils.string_of_formatter pp t
289 290
end

291
let () = print_node := (fun ppf n -> Print.print ppf (descr n))
292

293 294 295 296

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
297
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
298 299
let times_res v1 v2 = Types.Positive.times v1 v2

300
(* Try with a hash-table *)
301 302 303 304
module MemoFilter = Map.Make
  (struct
     type t = Types.t * node
     let compare (t1,n1) (t2,n2) =
305
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
306
       Types.compare t1 t2
307
   end)
308 309 310

let memo_filter = ref MemoFilter.empty

311
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
312
(* TODO: avoid is_empty t when t is not changing (Cap) *)
Pietro Abate's avatar
Pietro Abate committed
313
  if Types.is_empty t then empty_res fv
314 315
  else
    match d with
Pietro Abate's avatar
Pietro Abate committed
316
      | Constr t0 ->
317
          if Types.subtype t t0 then IdMap.empty
Pietro Abate's avatar
Pietro Abate committed
318
          else (empty_res fv) (* omega *)
319
      | Cup ((a,_,_) as d1,d2) ->
320
	  IdMap.merge cup_res
321 322
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
323
      | Cap (d1,d2) ->
324
	  IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
325 326
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
327 328 329
      | Record (l,p) ->
	  filter_node (Types.Record.project t l) p
      | Capture c ->
330
	  IdMap.singleton c (Types.Positive.ty t)
331
      | Constant (c, cst) ->
332
	  IdMap.singleton c (Types.Positive.ty (Types.constant cst))
333
      | Dummy -> assert false
334

335
and filter_prod ?kind fv p1 p2 t =
336
  List.fold_left
337
    (fun accu (d1,d2) ->
338
       let term =
339
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
340
       in
341
       IdMap.merge cup_res accu term
342 343 344 345
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)

346
and filter_node t p : Types.Positive.v id_map =
347 348
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
349
    let (_,fv,_) = descr p in
350
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
351 352
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
353
    IdMap.collide Types.Positive.define res r;
354 355 356 357 358
    r

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
359
  IdMap.map Types.Positive.solve r
Pietro Abate's avatar
Pietro Abate committed
360

361 362 363 364 365
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

366 367 368
(* Factorization of capture variables and constant patterns *)

module Factorize = struct
369 370
  module NodeTypeSet = Set.Make(Custom.Pair(Node)(Types))

371 372 373 374 375 376 377 378
  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)
*)
379
  let rec approx_var seen (a,fv,d) t xs =
380
(*    assert (Types.subtype t a);
381 382 383 384
      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) ->
385
	  approx_var seen p2 (Types.diff t a1)
386
	    (approx_var seen p1 (Types.cap t a1) xs)
387 388 389 390
      | 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))
391 392
      | Capture _ ->
	  xs
393
      | Constant (_,c) ->
394 395 396 397 398 399 400 401 402 403 404 405 406
	  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
407

408
  and approx_var_node seen q t xs =
409
    if (NodeTypeSet.mem (q,t) seen)
410
    then xs
411
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
412

413 414

(* Obviously not complete ! *)
415
  let rec approx_nil seen (a,fv,d) t xs =
416
    assert (Types.subtype t a);
417
    assert (IdSet.subset xs fv);
418 419 420
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
421
	  approx_nil seen p2 (Types.diff t a1)
422
	    (approx_nil seen p1 (Types.cap t a1) xs)
423 424 425 426 427 428 429 430 431
      | 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
432

433
  and approx_nil_node seen q t xs =
434
    if (NodeTypeSet.mem (q,t) seen)
435
    then xs
436
    else approx_nil (NodeTypeSet.add (q,t) seen) q.descr t xs
437

438
(*
439 440 441 442 443 444 445 446 447 448 449
  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))
450
*)
451 452

  let var ((a,_,_) as p) t =
453
    approx_var NodeTypeSet.empty p (Types.cap t a)
454

455
  let nil ((a,_,_) as p) t =
456
    approx_nil NodeTypeSet.empty p (Types.cap t a)
457 458 459 460 461
end




462
(* Normal forms for patterns and compilation *)
463

464 465
let min (a:int) (b:int) = if a < b then a else b

466 467
let any_basic = Types.Record.or_absent Types.non_constructed

468
let rec first_label (acc,fv,d) =
469
  if Types.is_empty acc
470
  then Label.dummy
471 472
  else match d with
    | Constr t -> Types.Record.first_label t
473 474
    | Cap (p,q) -> Label.min (first_label p) (first_label q)
    | Cup ((acc1,_,_) as p,q) -> Label.min (first_label p) (first_label q)
475
    | Record (l,p) -> l
476
    | _ -> Label.dummy
477

478
module Normal = struct
479

480
  type source = SCatch | SConst of Types.const
481
  type result = source id_map
482

483
  let compare_source s1 s2 =
484
    if s1 == s2 then 0
485 486
    else match (s1,s2) with
      | SCatch, _ -> -1 | _, SCatch -> 1
487
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
488

489
(*
490 491
  let hash_source = function
    | SCatch -> 1
492
    | SConst c -> Types.Const.hash c
493
*)
494

495 496 497
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

498 499 500 501 502
  module ResultMap = Map.Make(struct
				type t = result
				let compare = compare_result
			      end)

503
  module NodeSet = SortedList.Make(Node)
504

505
  module Nnf = struct
506 507
    include Custom.Dummy

508
    type t = NodeSet.t * Types.t * IdSet.t (* pl,t;   t <= \accept{pl} *)
509

510
    let check ((pl,t,xs) : t) =
511
      List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
512
	(pl :> Node.t list)
513
    let print ppf (pl,t,xs) =
514
      Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]"
515
	NodeSet.dump pl Types.Print.pp_type t
516
	IdSet.dump xs
517 518 519 520
    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
521
    let hash (l,t,xs) =
522 523
      (NodeSet.hash l) + 17 * (Types.hash t) + 257 * (IdSet.hash xs)
    let equal x y = compare x y == 0
524 525


526
    let first_label ((pl,t,xs) : t) =
527
      List.fold_left
528
	(fun l p -> Label.min l (first_label (descr p)))
529
	(Types.Record.first_label t)
530
	(pl :> Node.t list)
531 532


533
  end
534

535 536
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
537

538 539 540 541 542
    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
  end
543

544
  module NLineProd = Set.Make(NProd)
545

546
  type record =
547
    | RecNolabel of result option * result option
548
    | RecLabel of label * NLineProd.t
549
  type t = {
550 551
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
552
    nrecord: record
553
  }
554

555
  let fus = IdMap.union_disj
556

557 558
  let nempty lab =
    { nprod = NLineProd.empty;
559
      nxml = NLineProd.empty;
560
      nrecord = (match lab with
561
		   | Some l -> RecLabel (l,NLineProd.empty)
562
		   | None -> RecNolabel (None,None))
563
    }
564
  let dummy = nempty None
565 566


567
  let ncup nf1 nf2 =
568
    { nprod   = NLineProd.union nf1.nprod nf2.nprod;
569
      nxml    = NLineProd.union nf1.nxml nf2.nxml;
570
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
571 572
		   | RecLabel (l1,r1), RecLabel (l2,r2) ->
		       (* assert (l1 = l2); *)
573
		       RecLabel (l1, NLineProd.union r1 r2)
574
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
575 576
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
577
		   | _ -> assert false)
578 579
    }

580
  let double_fold_prod f l1 l2 =
581 582 583 584
    NLineProd.fold
      (fun x1 accu -> NLineProd.fold (fun x2 accu -> f accu x1 x2) l2 accu)
      l1 NLineProd.empty

585
  let ncap nf1 nf2 =
586
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
587 588 589 590
      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
591
	  NLineProd.add (fus res1 res2,
592
	   (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
593
	   (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2))
594
	  accu
595
    in
596
    let record r1 r2 = match r1,r2 with
597
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
598
	  (* assert (l1 = l2); *)
599
	  RecLabel(l1, double_fold_prod prod r1 r2)
600
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
601 602
	  let x = match x1,x2 with
	    | Some res1, Some res2 -> Some (fus res1 res2)
603 604 605 606
	    | _ -> None
	  and y = match y1,y2 with
	    | Some res1, Some res2 -> Some (fus res1 res2)
	    | _ -> None in
607
	  RecNolabel (x,y)
608
      | _ -> assert false
609
    in
610
    { nprod = double_fold_prod prod nf1.nprod nf2.nprod;
611
      nxml = double_fold_prod prod nf1.nxml nf2.nxml;
612
      nrecord = record nf1.nrecord nf2.nrecord;
613 614
    }

615 616
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
617
  let ncany = nc Types.any
618
  let ncany_abs = nc Types.Record.any_or_absent
619

620
  let empty_res = IdMap.empty
621

622 623
  let single_prod src p q = NLineProd.singleton (src, p,q)

624
  let ntimes lab acc p q xs =
625
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
626
    { (nempty lab) with
627
	nprod = single_prod empty_res (nnode p xsp) (nnode q xsq)
628 629
    }

630
  let nxml lab acc p q xs =
631
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
632
    { (nempty lab) with
633
	nxml =  single_prod empty_res (nnode p xsp) (nnode q xsq)
634
    }
635

636 637 638 639 640 641 642 643 644 645 646 647 648
  let nrecord (lab : Label.t option) acc (l : Label.t) p xs =
    let label = get_opt lab in
(*    Format.fprintf
      Format.std_formatter "label=%a l=%a@."
      Label.print label Label.print l; *)
    assert (Label.compare label l <= 0);
    let lft,rgt =
      if Label.equal l label
      then nnode p xs, ncany
      else ncany_abs, nnode (cons p.fv (record l p)) xs
    in
    { (nempty lab) with
	nrecord = RecLabel(label, single_prod empty_res lft rgt) }
649 650

  let nconstr lab t =
651
    let aux l =
652
      List.fold_left (fun accu (t1,t2) ->
653 654
			NLineProd.add (empty_res, nc t1,nc t2) accu)
	NLineProd.empty l in
655 656 657
    let record = match lab with
      | None ->
	  let (x,y) = Types.Record.empty_cases t in
658
	  RecNolabel ((if x then Some empty_res else None),
659
		      (if y then Some empty_res else None))
660
      | Some l ->
661
	  RecLabel (l,aux (Types.Record.split_normal t l)) in
662
    {  nprod = aux (Types.Product.clean_normal (Types.Product.normal t));
663
       nxml  =
664
	aux (Types.Product.clean_normal (Types.Product.normal ~kind:`XML t));
665
       nrecord = record
666 667
    }

668
  let nany lab res =
669
    { nprod  = single_prod res ncany ncany;
670
      nxml   = single_prod res ncany ncany;
671
      nrecord = match lab with
672 673
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
674 675
    }

676 677 678
  let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
  let ncapture lab x = nany lab (IdMap.singleton x SCatch)

679
  let rec nnormal lab (acc,fv,d) xs =
680 681 682
    let xs = IdSet.cap xs fv in
    if Types.is_empty acc then nempty lab
    else if IdSet.is_empty xs then nconstr lab acc
683
    else match d with
684 685
      | Constr t -> assert false
      | Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
686 687 688
      | Cup ((acc1,_,_) as p,q) ->
	  ncup
	    (nnormal lab p xs)
689 690 691
	    (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
692 693
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
694
      | Record (l,p) -> nrecord lab acc l p xs
695
      | Dummy -> assert false
696 697 698 699 700

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


701
  let facto f t xs pl =
702
    List.fold_left
703 704
      (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
      IdSet.empty
705
      pl
706

707 708
  let factorize t0 (pl,t,xs) =
    let t0 = if Types.subtype t t0 then t else Types.cap t t0 in
709
    let vs_var = facto Factorize.var t0 xs (NodeSet.get pl) in
710
    let xs = IdSet.diff xs vs_var in
711
    let vs_nil = facto Factorize.nil t0 xs (NodeSet.get pl) in
712
    let xs = IdSet.diff xs vs_nil in
713 714
    (vs_var,vs_nil,(pl,t,xs))

715
  let normal l t pl xs =
716
    List.fold_left
717
      (fun a p -> ncap a (nnormal l (descr p) xs)) (nconstr l t) pl
718

719
  let nnf lab t0 (pl,t,xs) =
720
(*    assert (not (Types.disjoint t t0)); *)
721 722
    let t = if Types.subtype t t0 then t else Types.cap t t0 in
    normal lab t (NodeSet.get pl) xs
723

724 725 726
  let basic_tests f (pl,t,xs) =
    let rec aux more s accu t res = function
	(* Invariant: t and s disjoint, t not empty *)
727
      | [] ->
728
	  let accu =
729
	    try
730 731 732 733
	      let t' = ResultMap.find res accu in
	      ResultMap.add res (Types.cup t t') accu
	    with Not_found -> ResultMap.add res t accu in
	  cont (Types.cup t s) accu more
734 735
      | (tp,xp,d) :: r ->
	  if (IdSet.disjoint xp xs)
736
	  then aux_check more s accu (Types.cap t tp) res r
737
	  else match d with
738 739 740
	    | Cup (p1,p2) -> aux ((t,res,p2::r)::more) s accu t res (p1::r)
	    | Cap (p1,p2) -> aux more s accu t res (p1 :: p2 :: r)
	    | Capture x -> aux more s accu t (IdMap.add x SCatch res) r
741
	    | Constant (x,c) ->
742 743 744 745 746 747 748
		aux more s accu t (IdMap.add x (SConst c) res) r
	    | _ -> cont s accu more
    and aux_check more s accu t res pl =
      if Types.is_empty t then cont s accu more else aux more s accu t res pl
    and cont s accu = function
      | [] -> ResultMap.iter f accu
      | (t,res,pl)::tl -> aux_check tl s accu (Types.diff t s) res pl
749
    in
750
    aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic)
751
      IdMap.empty (List.map descr (NodeSet.get pl))
752

753
(*
754 755 756
  let prod_tests (pl,t,xs) =
    let rec aux accu q1 q2 res = function
      | [] -> (res,q1,q2) :: accu
757 758
      | (tp,xp,d) :: r ->
	  if (IdSet.disjoint xp xs)
759 760 761 762 763 764
	  then aux_check accu q1 q2 res tp r
	  else match d with
	    | Cup (p1,p2) -> aux (aux accu q1 q2 res (p2::r)) q1 q2 res (p1::r)
	    | Cap (p1,p2) -> aux accu q1 q2 res (p1 :: p2 :: r)
	    | Capture x -> aux accu q1 q2 (IdMap.add x SCatch res) r
	    | Constant (x,c) -> aux accu q1 q2 (IdMap.add x (SConst c) res) r
765
	    | Times (p1,p2) ->
766 767 768 769 770 771 772 773 774 775
		let (pl1,t1,xs1) = q1 and (pl2,t2,xs2) = q2 in
		let t1 = Types.cap t1 (Types.descr (accept p1)) in
		if Types.is_empty t1 then accu
		else let t2 = Types.cap t2 (Types.descr (accept p2)) in
		if Types.is_empty t2 then accu
		else
		  let q1 =
		    let xs1' = IdSet.cap (fv p1) xs in
		    if IdSet.is_empty xs1' then (pl1,t1,xs1)
		    else (NodeSet.add p1 pl1, t1, IdSet.cup xs1 xs1')
776
		  and q2 =
777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794
		    let xs2' = IdSet.cap (fv p2) xs in
		    if IdSet.is_empty xs2' then (pl2,t2,xs2)
		    else (NodeSet.add p2 pl2, t2, IdSet.cup xs2 xs2')
		  in
		  aux accu q1 q2 res r
	    | _ -> accu
    and aux_check accu q1 q2 res t r =
      List.fold_left
	(fun accu (t1',t2') ->
	   let (pl1,t1,xs1) = q1 and (pl2,t2,xs2) = q2 in
	   let t1 = Types.cap t1 t1' in
	   if Types.is_empty t1 then accu
	   else let t2 = Types.cap t2 t2' in
	   if Types.is_empty t2 then accu
	   else aux accu (pl1,t1,xs1) (pl2,t2,xs2) res r)
	accu (Types.Product.clean_normal (Types.Product.normal t))
    in
    aux_check [] ncany ncany IdMap.empty t (List.map descr pl)
795
*)
796
end
797 798


799 800
module Compile = struct
  open Auto_pat
801 802

  type return_code =
803
      Types.t * int *   (* accepted type, arity *)
804
      int id_map option array
805

806
  type interface =
807 808
    [ `Result of int
    | `Switch of interface * interface
809 810
    | `None ]

811
  type dispatcher = {
812
    id : int;
813
    t  : Types.t;
814
    pl : Normal.Nnf.t array;
815
    label : label option;
816 817
    interface : interface;
    codes : return_code array;
818
    state : state;
819
  }
820

821
  let dispatcher_of_state = Hashtbl.create 1024
822

823 824 825 826 827
  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))

828 829 830 831 832 833 834 835
  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)

836 837
  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
838
      | Const x, Const y -> Types.Const.equal x y
839
      | Stack x, Stack y -> x == y
840 841 842
      | Recompose (x1,x2), Recompose (y1,y2) -> (x1 == y1) && (x2 == y2)
      | _ -> false

843 844
  let equal_result (r1,s1,l1) (r2,s2,l2) =
    (r1 == r2) && (equal_array equal_source s1 s2) && (l1 == l2)
845

846
  let equal_result_dispatch d1 d2 = (d1 == d2) || match (d1,d2) with
847
    | Dispatch (d1,a1), Dispatch (d2,a2) ->
848 849 850 851 852 853
	(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 =
854
    let res : result option ref = ref None in
855
    let chk = function Catch | Const _ -> true | _ -> false in
856
    let f ((_,ret,_) as r) =
857 858 859 860 861 862 863 864 865 866 867 868 869
      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
870

871 872
  let split_kind basic prod xml record = {
    basic = basic;
873 874
    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.VarAtoms.leafconj (Types.Atom.get t), r) basic);
    chars = Chars.mk_map (List.map (fun (t,r) -> Types.VarChars.leafconj (Types.Char.get t), r) basic);
875 876
    prod = prod;
    xml = xml;
877 878
    record = record
  }
879

880
  let combine_kind basic prod xml record =
881 882
    try AIgnore (immediate_res basic prod xml record)
    with Exit -> AKind (split_kind basic prod xml record)
883

884 885
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
886
    else
887
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes)
888
	 && (array_for_all ( f act.(0) ) act) then
889
	   Ignore act.(0)
890
      else
891
	Dispatch (disp.state, act)
892

893 894
  let detect_tail_call f = function
    | Dispatch (disp,branches) when array_for_all_i f branches -> TailCall disp
895 896
    | x -> x

897 898
  let detect_right_tail_call =
    detect_tail_call
899
      (fun i (code,ret,_) ->
900
	 (i == code) &&
901
	   let ar = Array.length ret in
902 903
	   (array_for_all_i
	      (fun pos ->
904
		 function Stack j when pos + j == ar -> true | _ -> false)
905 906 907 908 909 910
	      ret
	   )
      )

  let detect_left_tail_call =
    detect_tail_call
911 912
      (fun i ->
	 function
913 914
	   | Ignore (code,ret,_) when (i == code) ->
	       let ar = Array.length ret in
915 916
	       array_for_all_i
		 (fun pos ->
917
		    function Stack j when pos + j == ar -> true | _ -> false)
918 919 920
		 ret
	   | _ -> false
      )
921

922
  let cur_id = ref 0
923

924 925
  module NfMap = Map.Make(Normal.Nnf)
  module NfSet = Set.Make(Normal.Nnf)
926

927
  module DispMap = Map.Make(Custom.Pair(Types)(Custom.Array(Normal.Nnf)))
928 929

    (* Try with a hash-table ! *)
930

931
  let dispatchers = ref DispMap.empty
932 933 934 935 936 937

  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"
938

939 940
  let dump_disp disp =
    let ppf = Format.std_formatter in
941
    Format.fprintf ppf "Dispatcher t=%a@." Types.Print.pp_type disp.t;
942
    Array.iter (fun p ->
943
		 Format.fprintf ppf "  pat %a@." Normal.Nnf.print p;
944
	      ) disp.pl
945

946
  let first_lab t (reqs : Normal.Nnf.t array) =
947
    let aux l req = Label.min l (Normal.Nnf.first_label req) in
948
    let lab =
949
      Array.fold_left aux (Types.Record.first_label t) reqs in
950 951 952 953 954
    if lab == Label.dummy then None else Some lab

  let dummy_actions = AIgnore ((-1),[||],(-1))

  let compute_actions = ref (fun _ -> assert false)
955

956
  let dispatcher t (pl : Normal.Nnf.t array) : dispatcher =
957 958
    try DispMap.find (t,pl) !dispatchers
    with Not_found ->
959
      let lab = first_lab t pl in
960
      let nb = ref 0 in
961
      let codes = ref [] in
962 963 964
      let rec aux t arity i accu =
	if i == Array.length pl
	then (incr nb; let r = Array.of_list (List.rev accu) in
965
	      codes := (t,arity,r)::!codes; `Result (!nb - 1))
966
	else
967
	  let (_,tp,v) = pl.(i) in
968 969
	  let a1 = Types.cap t tp in
	  if Types.is_empty a1 then
970
	    `Switch (`None,aux t arity (i+1) (None::accu))
971
	  else