viewcvs.cgi/types/patterns.ml

exception Error of string
open Ident

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

(*
To be sure not to use generic comparison ...
*)
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1


(* Syntactic algebra *)
(* Constraint: any node except Constr has fv<>[] ... *)
type d =
  | Constr of Types.t
  | Cup of descr * descr
  | Cap of descr * descr
  | Times of node * node
  | Xml of node * node
  | Record of label * node
  | Capture of id
  | Constant of id * Types.const
  | Dummy
and node = {
  id : int;
  mutable descr : descr;
  accept : Types.Node.t;
  fv : fv
} and descr = Types.t * fv * d


let id x = x.id
let descr x = x.descr
let fv x = x.fv
let accept x = Types.internalize x.accept

let printed = ref []
let to_print = ref []
let rec print ppf (a,_,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 (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) -> 
        Format.fprintf ppf "{ %a =  P%i }" Label.print (LabelPool.value l) n.id;
        to_print := n :: !to_print
    | Capture x ->
        Format.fprintf ppf "%a" U.print (Id.value x)
    | Constant (x,c) ->
        Format.fprintf ppf "(%a := %a)" U.print (Id.value x) 
          Types.Print.print_const c
    | Dummy ->
        Format.fprintf ppf "*DUMMY*"

let dump_print ppf =
  while !to_print != [] do
    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

let print_node ppf n =
  Format.fprintf ppf "P%i" n.id;
  to_print := n :: !to_print;
  dump_print ppf


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

let dummy = (Types.empty,IdSet.empty,Dummy)
let make fv =
  incr counter;
  { id = !counter; descr = dummy; accept = Types.make (); fv = fv }

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

let cons fv d =
  let q = make fv in
  define q d;
  q

let constr x = (x,IdSet.empty,Constr x)
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
  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
    in
    raise 
      (Error 
         ("The capture variable " ^ (U.to_string (Id.value x)) ^ 
          " should appear on both side of this | pattern"))
  );
  (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
  if not (IdSet.disjoint fv1 fv2) then (
    match IdSet.pick (IdSet.cap fv1 fv2) with
      | Some x -> 
          raise 
          (Error 
             ("The capture variable " ^ (U.to_string (Id.value x)) ^ 
              " cannot appear on both side of this & pattern"))
      | None -> assert false
  );
  (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2))
let times x y =
  (Types.times x.accept y.accept, IdSet.cup x.fv y.fv, Times (x,y))
let xml x y =
  (Types.xml x.accept y.accept, IdSet.cup x.fv y.fv, Xml (x,y))
let record l x = 
  (Types.record l x.accept, x.fv, Record (l,x))
let capture x = (Types.any, IdSet.singleton x, Capture x)
let constant x c = (Types.any, IdSet.singleton x, Constant (x,c))


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

  let check n = ()
  let dump = print_node


  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;
      let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in
      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

(* Pretty-print *)

module Pat = struct
  type t = descr
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
    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

  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
end

module Print = struct
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)

  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 q3.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


  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 "}"
end


(* Static semantics *)

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

(* Try with a hash-table *)
module MemoFilter = Map.Make 
  (struct 
     type t = Types.t * node 
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
       Types.compare t1 t2
   end)

let memo_filter = ref MemoFilter.empty

let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
(* TODO: avoid is_empty t when t is not changing (Cap) *)
  if Types.is_empty t 
  then empty_res fv
  else
    match d with
      | Constr _ -> IdMap.empty
      | Cup ((a,_,_) as d1,d2) ->
          IdMap.merge cup_res
            (filter_descr (Types.cap t a) d1)
            (filter_descr (Types.diff t a) d2)
      | Cap (d1,d2) ->
          IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
      | Record (l,p) ->
          filter_node (Types.Record.project t l) p
      | Capture c ->
          IdMap.singleton c (Types.Positive.ty t)
      | Constant (c, cst) ->
          IdMap.singleton c (Types.Positive.ty (Types.constant cst))
      | Dummy -> assert false

and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
         IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
       in
       IdMap.merge cup_res accu term
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)


and filter_node t p : Types.Positive.v id_map =
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
    let (_,fv,_) as d = descr p in
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
    IdMap.collide Types.Positive.define res r;
    r

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

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


(* Normal forms for patterns and compilation *)

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

let any_basic = Types.Record.or_absent Types.non_constructed

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

module Normal = struct

  type source = 
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
  type result = source id_map

  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
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
    | SConst c -> Types.Const.hash c
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


  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"

  module NodeSet = SortedList.Make(Node)

  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


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

  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


  module NProd = struct
    type t = result * Nnf.t * Nnf.t

    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

    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

  module NLineBasic = SortedList.Make(NBasic)
  module NLineProd = SortedList.Make(NProd)

  type record =
    | RecNolabel of result option * result option
    | RecLabel of label * NLineProd.t
  type t = {
    nfv    : fv;
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
    nrecord: record
  }

  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
      

  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 =
    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 = Types.compare t1.na t2.na in if c <> 0 then c
      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 compare_record t1.nrecord t2.nrecord

  let fus = IdMap.union_disj

  let nempty lab = 
    { nfv = IdSet.empty; 
      na = Types.empty;
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
      nrecord = (match lab with 
                   | Some l -> RecLabel (l,NLineProd.empty)
                   | None -> RecNolabel (None,None))
    }
  let dummy = nempty None


  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;
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
                   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
                       (* assert (l1 = l2); *) RecLabel (l1, NLineProd.cup r1 r2)
                   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
                       RecNolabel((if x1 == None then x2 else x1),
                                (if y1 == None then y2 else y1))
                   | _ -> assert false)
    }

  let double_fold f l1 l2 =
    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)
         
  let ncap nf1 nf2 =
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
      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
          (fus res1 res2, 
           (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
           (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) 
          :: accu
    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
    let record r1 r2 = match r1,r2 with
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
          (* assert (l1 = l2); *)
          RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
          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
          RecNolabel (x,y)
      | _ -> assert false
    in
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
      na = Types.cap nf1.na nf2.na;
      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;
    }

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

  let empty_res = IdMap.empty

  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
    let src = IdMap.merge_elem SRecompose src_p src_q in 
    { nempty lab with 
        nfv = xs;
        na = acc;
        nprod = single_prod src (nnode p xsp) (nnode q xsq)
    }

  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
    let src = IdMap.merge_elem SRecompose src_p src_q in 
    { nempty lab with 
        nfv = xs;
        na = acc;
        nxml =  single_prod src (nnode p xsp) (nnode q xsq)
    }
    
  let nrecord lab acc l p xs =
    assert (IdSet.equal xs (fv p));
    match lab with
      | None -> assert false
      | Some label ->
          assert (label <= l);
          let src,lft,rgt =
            if l == label
            then SLeft, nnode p xs, ncany
            else SRight, ncany_abs, nnode (cons p.fv (record l p)) xs
          in
          let src = IdMap.constant src xs in
          { nempty lab with
              nfv = xs;
              na = acc;
              nrecord = RecLabel(label, single_prod src lft rgt) }

  let nconstr lab t =
    let aux l = NLineProd.from_list
                (List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
    let record = match lab with
      | None ->
          let (x,y) = Types.Record.empty_cases t in
          RecNolabel ((if x then Some empty_res else None), 
                      (if y then Some empty_res else None))
      | Some l ->
          RecLabel (l,aux (Types.Record.split_normal t l)) in
    { nempty lab with
        na = t;
        nbasic = single_basic empty_res (Types.cap t any_basic);
        nprod = aux (Types.Product.normal t);
        nxml  = aux (Types.Product.normal ~kind:`XML t);
        nrecord = record
    }

  let nany lab res =
    { nfv = IdMap.domain res;
      na = Types.any;
      nbasic = single_basic res any_basic;
      nprod  = single_prod res ncany ncany;
      nxml   = single_prod res ncany ncany;
      nrecord = match lab with
        | None -> RecNolabel (Some res, Some res)
        | Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
    }

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

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

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


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

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

  let nnf lab (pl,t,xs) =
    let pl = NodeSet.get pl in
    normal lab t pl xs
    

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


module Compile = 
struct
  type actions =
    | AIgnore of result
    | AKind of actions_kind
  and actions_kind = {
    basic: (Types.t * result) list;
    atoms: result Atoms.map;
    chars: result Chars.map;
    prod: result dispatch dispatch;
    xml: result dispatch dispatch;
    record: record option;
  }
  and record = 
    | RecLabel of label * result dispatch dispatch
    | RecNolabel of result option * result option
      
  and 'a dispatch =
    | Dispatch of dispatcher * 'a array
    | TailCall of dispatcher
    | Ignore of 'a
    | Impossible

  and result = int * source array
  and source = 
    | Catch | Const of Types.const 
    | Left of int | Right of int | Recompose of int * int
      
  and return_code = 
      Types.t * int *   (* accepted type, arity *)
      int id_map option array

  and interface =
    [ `Result of int
    | `Switch of interface * interface
    | `None ]

  and dispatcher = {
    id : int;
    t  : Types.t;
    pl : Normal.t array;
    label : label option;
    interface : interface;
    codes : return_code array;
    mutable actions : actions option;
    mutable printed : bool
  }

  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 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)

  let equal_source s1 s2 =
    (s1 == s2) || match (s1,s2) with
      | Const x, Const y -> Types.Const.equal x y 
      | 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

  let immediate_res basic prod xml record =
    let res = ref None in
    let chk = function Catch | Const _ -> true | _ -> false in
    let f ((_,ret) as r) =
      match !res with
        | Some r0 when equal_result r r0 -> ()
        | None when array_for_all chk ret -> res := Some r
        | _ -> raise Exit in
    (match basic with [_,r] -> f r | [] -> () | _ -> raise Exit);
    (match prod with Ignore (Ignore r) -> f r |Impossible ->()| _->raise Exit);
    (match xml with Ignore (Ignore r) -> f r |Impossible ->()| _->raise Exit);
    (match record with
      | None -> ()
      | Some (RecLabel (_,Ignore (Ignore r))) -> f r
      | Some (RecNolabel (Some r1, Some r2)) -> f r1; f r2
      | _ -> raise Exit);
    match !res with Some r -> r | None -> raise Exit
          
  let split_kind basic prod xml record = {
    basic = basic;
    atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
    chars = Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
    prod = prod; 
    xml = xml; 
    record = record
  }

  let combine_kind basic prod xml record =
    try AIgnore (immediate_res basic prod xml record)
    with Exit -> AKind (split_kind basic prod xml record)
      
  let combine f (disp,act) =
    if Array.length act == 0 then Impossible
    else
      if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes) 
         && (array_for_all ( f act.(0) ) act) then
           Ignore act.(0)
      else
        Dispatch (disp, act)

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

  let detect_right_tail_call =
    detect_tail_call
      (fun i (code,ret) ->
         (i == code) && 
           (array_for_all_i 
              (fun pos -> 
                 function Right j when pos == j -> true | _ -> false)
              ret
           )
      )

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

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

    (* Try with a hash-table ! *)
    
  let dispatchers = ref DispMap.empty
                
  let timer_disp = Stats.Timer.create "Patterns.dispatcher loop"

  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"
      
  let dispatcher t pl lab : dispatcher =
    try DispMap.find (t,pl) !dispatchers
    with Not_found ->
      let nb = ref 0 in
      let codes = ref [] in
      let rec aux t arity i accu = 
        if i == Array.length pl 
        then (incr nb; let r = Array.of_list (List.rev accu) in 
              codes := (t,arity,r)::!codes; `Result (!nb - 1))
        else
          let p = pl.(i) in
          let tp = p.Normal.na in

          let a1 = Types.cap t tp in
          if Types.is_empty a1 then
            `Switch (`None,aux t arity (i+1) (None::accu))
          else
            let v = p.Normal.nfv in
            let a2 = Types.diff t tp in
            let accu' = Some (IdMap.num arity v) :: accu in
            if Types.is_empty a2 then
              `Switch (aux t (arity + (IdSet.length v)) (i+1) accu',`None)
            else
              `Switch (aux a1 (arity + (IdSet.length v)) (i+1) accu',
                       aux a2 arity (i+1) (None::accu))

(* Unopt version:
            `Switch 
              (
               aux (Types.cap t tp) (arity + (IdSet.length v)) (i+1) accu',
               aux (Types.diff t tp) arity (i+1) accu
              )
*)

      in
      Stats.Timer.start timer_disp;
      let iface = if Types.is_empty t then `None else aux t 0 0 [] in
      Stats.Timer.stop timer_disp ();
      let res = { 
        id = !cur_id; 
        t = t;
        label = lab;
        pl = pl;
        interface = iface;
        codes = Array.of_list (List.rev !codes);
        actions = None; printed = false 
      } in
      incr cur_id;
      dispatchers := DispMap.add (t,pl) res !dispatchers;
      res
    
  let find_code d a =
    let rec aux i = function
      | `Result code -> code
      | `None -> assert false
      | `Switch (yes,_) when a.(i) != None -> aux (i + 1) yes
      | `Switch (_,no) -> aux (i + 1) no in
    aux 0 d.interface

  let create_result pl =
    let aux x accu = match x with Some b -> b @ accu | None -> accu in
    Array.of_list (Array.fold_right aux pl [])

  let return disp pl f =
    let aux = function [x] -> Some (f x) | [] -> None | _ -> assert false in
    let final = Array.map aux pl in
    (find_code disp final, create_result final)
    
  let conv_source_basic s = match s with
    | Normal.SCatch -> Catch
    | Normal.SConst c -> Const c
    | _ -> assert false

  let return_basic disp selected =
    let aux_final res = IdMap.map_to_list conv_source_basic res in
    return disp selected aux_final

  let assoc v l =
    try IdMap.assoc v l with Not_found -> -1

  let conv_source_prod left right v s = match s with
    | Normal.SCatch -> Catch
    | Normal.SConst c -> Const c
    | Normal.SLeft -> Left (assoc v left)
    | Normal.SRight -> Right (assoc v right)
    | Normal.SRecompose -> Recompose (assoc v left, assoc v right)

  module TypeList = SortedList.Make(Types)
  let dispatch_basic disp : (Types.t * result) list =
(* TODO: try other algo, using disp.codes .... *)
    let pl = Array.map (fun p -> p.Normal.nbasic) disp.pl in
    let tests =
      let accu = ref [] in
      let aux i (res,x) = accu := (x, [i,res]) :: !accu in
      Array.iteri (fun i -> Normal.NLineBasic.iter (aux i)) pl;
      TypeList.Map.get (TypeList.Map.from_list (@) !accu) in

    let t = Types.cap any_basic disp.t in
    let accu = ref [] in
    let rec aux (success : (int * Normal.result) list) t l = 
      if Types.non_empty t 
      then match l with
        | [] ->
            let selected = Array.create (Array.length pl) [] in
            let add (i,res) = selected.(i) <- res :: selected.(i) in
            List.iter add success;
            accu := (t, return_basic disp selected) :: !accu
        | (ty,i) :: rem -> 
            aux (i @ success) (Types.cap t ty) rem; 
            aux success (Types.diff t ty) rem
    in
    aux [] t tests;
    !accu


  let first_lab pl =
    let aux l (req,_) = min l (Normal.Nnf.first_label req) in
    let lab = Array.fold_left (List.fold_left aux) LabelPool.dummy_max pl in
    if lab == LabelPool.dummy_max then None else Some lab


  let get_tests pl f t d post =
    let pl = Array.map (List.map f) pl in
    let lab = first_lab pl in
    let pl = Array.map (List.map (fun (x,info) -> (Normal.nnf lab x,info))) pl
    in
    (* Collect all subrequests *)
    let aux reqs (req,_) = NfSet.add req reqs in
    let reqs = Array.fold_left (List.fold_left aux) NfSet.empty pl in
    let reqs = Array.of_list (NfSet.elements reqs) in
    (* Map subrequest -> idx in reqs *)
    let idx = ref NfMap.empty in
    Array.iteri (fun i req -> idx := NfMap.add req i !idx) reqs;
    let idx = !idx in

    (* Build dispatcher *)
    let disp = dispatcher t reqs lab in
    
    (* Build continuation *)
    let result (t,_,m) =
      let get a (req,info) =
        match m.(NfMap.find req idx) with Some res -> (res,info)::a | _ -> a in
      let pl = Array.map (List.fold_left get []) pl in
      d t pl
    in
    let res = Array.map result disp.codes in
    post (disp,res)


  type 'a rhs = Match of (id * int) list * 'a | Fail
  let make_branches t brs =
    let t0 = ref t in
    let aux (p,e) = 
      let xs = fv p in
      let nnf = (Normal.NodeSet.singleton p, !t0, xs) in
      t0 := Types.diff !t0 (Types.descr (accept p));
      [(nnf, (xs, e))] in
    let res _ pl =
      let aux r = function 
        | [(res, (xs,e))] -> assert (r == Fail); 
            let m = List.map (fun x -> (x,IdMap.assoc x res)) xs in
            Match (m,e)
        | [] -> r | _ -> assert false in
      Array.fold_left aux Fail pl in
    let pl = Array.map aux (Array.of_list brs) in
    get_tests pl (fun x -> x) t res (fun x -> x)


  let rec dispatch_prod ?(kind=`Normal) disp =
    let extr = match kind with
        | `Normal ->  fun p -> Normal.NLineProd.get p.Normal.nprod
        | `XML -> fun p -> Normal.NLineProd.get p.Normal.nxml in
    let t = Types.Product.get ~kind disp.t in
    dispatch_prod0 disp t (Array.map extr disp.pl)
  and dispatch_prod0 disp t pl =
    get_tests pl
      (fun (res,p,q) -> p, (res,q))
      (Types.Product.pi1 t)
      (dispatch_prod1 disp t)
      (fun x -> detect_left_tail_call (combine equal_result_dispatch x))
  and dispatch_prod1 disp t t1 pl =
    get_tests pl
      (fun (ret1, (res,q)) -> q, (ret1,res) ) 
      (Types.Product.pi2_restricted t1 t)
      (dispatch_prod2 disp)
      (fun x -> detect_right_tail_call (combine equal_result x))
  and dispatch_prod2 disp t2 pl =
    let aux_final (ret2, (ret1, res)) =  
      IdMap.mapi_to_list (conv_source_prod ret1 ret2) res in
    return disp pl aux_final


  let dispatch_record disp : record option =
    let t = disp.t in
    if not (Types.Record.has_record t) then None 
    else
      match disp.label with
        | None -> 
            let (some,none) = Types.Record.empty_cases t in
            let some = aux some 
              if some then 
                let pl = Array.map (fun p -> match p.Normal.nrecord with
                                      | Normal.RecNolabel (Some x,_) -> [x]
                                      | Normal.RecNolabel (None,_) -> []
                                      | _ -> assert false) disp.pl in
                Some (return disp pl (IdMap.map_to_list conv_source_basic))
              else None
            in
            let none =
              if none then 
                let pl = Array.map (fun p -> match p.Normal.nrecord with
                                      | Normal.RecNolabel (_,Some x) -> [x]
                                      | Normal.RecNolabel (_,None) -> []
                                      | _ -> assert false) disp.pl in
                Some (return disp pl (IdMap.map_to_list conv_source_basic))
              else None
            in        
            Some (RecNolabel (some,none))
        | Some lab ->
            let t = Types.Record.split t lab in
            let pl = Array.map (fun p -> match p.Normal.nrecord with
                                  | Normal.RecLabel (_,l) -> 
                                      Normal.NLineProd.get l
                                  | _ -> assert false) disp.pl in
            Some (RecLabel (lab,dispatch_prod0 disp t pl))
      
  let actions disp =
    match disp.actions with
      | Some a -> a
      | None ->
          let a = combine_kind
                    (dispatch_basic disp)
                    (dispatch_prod disp)
                    (dispatch_prod ~kind:`XML disp)
                    (dispatch_record disp)
          in
          disp.actions <- Some a;
          a

  let to_print = ref []

  module DSET = Set.Make (struct type t = int let compare (x:t) (y:t) = x - y end)
  let printed = ref DSET.empty

  let queue d =
    if not d.printed then (
      d.printed <- true;
      to_print := d :: !to_print
    )

  let rec print_source ppf = function
    | Catch  -> Format.fprintf ppf "v"
    | Const c -> Types.Print.print_const ppf c
    | Left (-1) -> Format.fprintf ppf "v1"
    | Right (-1) -> Format.fprintf ppf "v2"
    | Left i -> Format.fprintf ppf "l%i" i
    | Right j -> Format.fprintf ppf "r%i" j
    | Recompose (i,j) -> 
        Format.fprintf ppf "(%a,%a)" 
          print_source (Left i)
          print_source (Right j)

  let print_result ppf =
    Array.iteri 
      (fun i s ->
         if i > 0 then Format.fprintf ppf ",";
         print_source ppf s; 
      )

  let print_ret ppf (code,ret) = 
    Format.fprintf ppf "$%i" code;
    if Array.length ret <> 0 then 
      Format.fprintf ppf "(%a)" print_result ret

  let print_ret_opt ppf = function
    | None -> Format.fprintf ppf "*"
    | Some r -> print_ret ppf r

  let print_kind ppf actions =
    let print_lhs ppf (code,prefix,d) =
      let arity = match d.codes.(code) with (_,a,_) -> a in
      Format.fprintf ppf "$%i(" code;
      for i = 0 to arity - 1 do
        if i > 0 then Format.fprintf ppf ",";
        Format.fprintf ppf "%s%i" prefix i;
      done;
      Format.fprintf ppf ")" in
    let print_basic (t,ret) =
      Format.fprintf ppf " | %a -> %a@\n"
        Types.Print.print t
        print_ret ret
    in
    let print_prod2 = function
      | Impossible -> assert false
      | Ignore r ->
          Format.fprintf ppf "        %a\n" 
            print_ret r
      | TailCall d ->
          queue d;
          Format.fprintf ppf "        disp_%i v2@\n" d.id
      | Dispatch (d, branches) ->
          queue d;
          Format.fprintf ppf "        match v2 with disp_%i@\n" d.id;
          Array.iteri 
            (fun code r ->
               Format.fprintf ppf "        | %a -> %a\n" 
                 print_lhs (code, "r", d)
                 print_ret r;
            )
            branches
    in
    let print_prod prefix ppf = function
      | Impossible -> ()
      | Ignore d2 ->
          Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix;
          print_prod2 d2
      | TailCall d ->
          queue d;
          Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix;
          Format.fprintf ppf "      disp_%i v1@\n" d.id
      | Dispatch (d,branches) ->
          queue d;
          Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix;
          Format.fprintf ppf "      match v1 with disp_%i@\n" d.id;
          Array.iteri 
            (fun code d2 ->
               Format.fprintf ppf "      | %a -> @\n"
               print_lhs (code, "l", d);
               print_prod2 d2;
            )
            branches
    in
    let rec print_record_opt ppf = function
      | None -> ()
      | Some (RecLabel (l,d)) ->
          let l = LabelPool.value l in
          print_prod ("record:"^(Label.to_string l)) ppf d
      | Some (RecNolabel (r1,r2)) ->
          Format.fprintf ppf " | Record -> @\n";
          Format.fprintf ppf "     SomeField:%a;NoField:%a@\n" 
           print_ret_opt r1 print_ret_opt r2
   in
    
    List.iter print_basic actions.basic;
    print_prod "" ppf actions.prod;
    print_prod "XML" ppf actions.xml;
    print_record_opt ppf actions.record

  let print_actions ppf = function
    | AKind k -> print_kind ppf k
    | AIgnore r -> Format.fprintf ppf "v -> %a@\n" print_ret r

  let print_dispatcher ppf d =
    Format.fprintf ppf "Dispatcher %i accepts [%a]@\n" 
      d.id Types.Print.print (Types.normalize d.t); 
    let print_code code (t, arity, m) =
      Format.fprintf ppf "  Returns $%i(arity=%i) for [%a]" 
        code arity
        Types.Print.print (Types.normalize t);
(*      
      List.iter
        (fun (i,b) ->
           Format.fprintf ppf "[%i:" i;
           List.iter 
             (fun (v,i) ->  Format.fprintf ppf "%s=>%i;" v i)
             b;
           Format.fprintf ppf "]"
        ) m;  *)
      
      Format.fprintf ppf "@\n";
    in
    Array.iteri print_code d.codes;   
    Format.fprintf ppf "let disp_%i = function@\n" d.id;
    print_actions ppf (actions d);
    Format.fprintf ppf "====================================@\n"


  let rec print_dispatchers ppf =
    match !to_print with
      | [] -> ()
      | d :: rem -> 
          to_print := rem; 
          print_dispatcher ppf d; 
          print_dispatchers ppf


  let show ppf t pl lab =
    let disp = dispatcher t pl lab in
    queue disp;
    print_dispatchers ppf

  let debug_compile ppf t pl =
    let t = Types.descr t in
    let lab =
      List.fold_left
        (fun l p -> min l (first_label (descr p)))
        (Types.Record.first_label t) pl in
    let lab = if lab == LabelPool.dummy_max then None else Some lab in
    
    let pl = Array.of_list 
               (List.map (fun p -> Normal.normal lab (*t*) Types.Record.any_or_absent [p] (fv p)) pl) in

    show ppf t pl lab;
    Format.fprintf ppf "# compiled dispatchers: %i@\n" !cur_id
end


(* New compilation procedure *)

module Compile2 = struct

  let any_or_abs = Types.Record.any_or_absent

  module PatList = SortedList.Make(struct include Custom.Dummy include Pat end)
  module TypesFv = Custom.Pair(Types)(IdSet)
  module Req = PatList.MakeMap(TypesFv)
    (* Invariant for (p |-> (t,X)):
       i)  t != Empty
       ii) X \subset fv(p) *)

  let empty_reqs = PatList.Map.empty

  let merge_reqs =
    PatList.Map.merge 
      (fun (t1,xs1) (t2,xs2) -> Types.cup t1 t2, IdSet.cup xs1 xs2)

  let add_req reqs p t xs =
    merge_reqs reqs (PatList.Map.singleton p (t,xs))

  module NodeSet = Set.Make(Node)

  let pi1 ~kind t = Types.Product.pi1 (Types.Product.get ~kind t)
  let pi2 ~kind t = Types.Product.pi2 (Types.Product.get ~kind t)

  module Approx = struct

(* 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) ->
            IdSet.cap
              (approx_var seen p1 (Types.cap t a1) xs) 
              (approx_var seen p2 (Types.diff 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 =
      if (NodeSet.mem q seen) 
      then xs
      else approx_var (NodeSet.add q seen) q.descr t xs
        

    let approx_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 approx_var ((a,_,_) as p) t = 
      approx_var NodeSet.empty p (Types.cap t a)
  end

  module TargExpr = struct

    type t = source IdMap.map
    and source =
      | SrcCapture
      | SrcLeft | SrcRight
      | SrcCst of Types.const
      | SrcPair of source * source
      | SrcFetchLeft of int
      | SrcFetchRight of int
      | SrcLocal of int

(*
    let rec equal_src s1 s2 = (s1 == s2) || match (s1,s2) with
      | SrcCst c1, SrcCst c2 -> Types.Const.equal c1 c2
      | SrcPair (s1,ss1), SrcPair (s2,ss2) -> 
          equal_src s1 s2 && equal_src ss1 ss2
      | SrcFetchLeft i, SrcFetchLeft j
      | SrcFetchRight i, SrcFetchRight j
      | SrcLocal i, SrcLocal j when i == j -> true
      | _ -> false

    let equal = IdMap.equal equal_src
*)


    type push = PushConst of Types.const | PushField | PushCapture

    let capture x = IdMap.singleton x SrcCapture
    let captures xs = IdMap.constant SrcCapture xs
    let cst x c = IdMap.singleton x (SrcCst c)
    let constants cs = IdMap.map (fun c -> SrcCst c) cs
    let fetch_left f = SrcFetchLeft f
    let fetch_right f = SrcFetchRight f
    let fetch_local ofs i = SrcLocal (ofs + i)
    let empty = IdMap.empty
    let merge e1 e2 = IdMap.merge (fun s1 s2 -> SrcPair (s1,s2)) e1 e2
    let captures_left xs = IdMap.constant SrcLeft xs
    let captures_right xs = IdMap.constant SrcRight xs

    let rec print_src ppf = function
      | SrcCapture -> Format.fprintf ppf "v"
      | SrcLeft -> Format.fprintf ppf "v1"
      | SrcRight -> Format.fprintf ppf "v2"
      | SrcCst c -> Types.Print.print_const ppf c
      | SrcPair (s1,s2) -> 
          Format.fprintf ppf "(%a,%a)" print_src s1 print_src s2
      | SrcFetchLeft x -> Format.fprintf ppf "x%i" x
      | SrcFetchRight x -> Format.fprintf ppf "y%i" x
      | SrcLocal x -> Format.fprintf ppf "local(%i)" x

    let print ppf r =
      Format.fprintf ppf "{ "; 
      List.iter (fun (x,s) -> 
                   Format.fprintf ppf "%a:=%a "
                     U.print (Id.value x)
                     print_src s) (IdMap.get r);
      Format.fprintf ppf "}";
  end

  module Derivation = struct

    type t =
      | TSucceed
      | TFail
      | TConstr of Types.t * Types.t
      | TCapt of TargExpr.t * t
      | TAlt of descr * Types.t * t * t
      | TConj of Types.t * fv * t * t
      | TTimes of Types.pair_kind * int * descr * Types.t * fv * node * node 
      | TRecord of int * descr * Types.t * fv * label * node

(*
    let rec same p1 p2 = (p1 == p2) || match (p1,p2) with
        | TConstr (t1,s1), TConstr (t2,s2) ->
            Types.equiv s1 s2 &&
            Types.equiv (Types.cap t1 s1) (Types.cap t2 s2)
        | TCapt (pr1,p1), TCapt (pr2,p2) ->
            TargExpr.equal pr1 pr2 && same p1 p2
        | TAlt (p1,_,a1,b1), TAlt (p2,_,a2,b2) ->
            (p1 == p2) && (same a1 a2) && (same b1 b2)
        | TConj (_,_,a1,b1), TConj (_,_,a2,b2) ->
            same a1 a2 && same b1 b2
        | TTimes (k1,uid1,p1,t1,xs1,a1,b1),
          TTimes (k2,uid2,p2,t2,xs2,a2,b2) ->
            assert false
        | TRecord (uid1,_,t1,_,_,_),
          TRecord (uid2,_,t2,_,_,_) ->
            (uid1 == uid2) && (Types.equiv t1 t2)
        | _ -> false
*)

  (* TODO: allocate the stack locations by sorting the ids
       (to allow  ({ l = (x,y) } | (x:=1)&(y:=2))) *)
    let push_csts pushes locals =
      let push x = 
        pushes := x :: !pushes;
        let loc = TargExpr.SrcLocal !locals in
        incr locals; loc in
      let reloc = function
        | TargExpr.SrcCst c -> push (TargExpr.PushConst c)
        | TargExpr.SrcLeft -> push TargExpr.PushField
        | TargExpr.SrcCapture -> push TargExpr.PushCapture
        | TargExpr.SrcLocal _ as s -> s
        | _ -> assert false
      in
      let rec aux = function
        | TCapt (pr,p) -> TCapt (IdMap.map reloc pr, p)
        | TAlt (p,a1,p1,p2) -> TAlt (p,a1,aux p1,aux p2)
        | TConj (a1,fv1,p1,p2) -> TConj (a1,fv1,aux p1, aux p2)
        | p -> p
      in
      aux

    let capt pr p = 
      if IdMap.is_empty pr then p else match p with
        | TCapt (pr2,p) -> TCapt (TargExpr.merge pr pr2,p)
        | TFail -> TFail
        | p ->  TCapt (pr,p)

    let success pr =
      capt pr TSucceed

    let success_if_present pr =
      capt pr (TConstr (Types.any,any_or_abs))

    let rec conj a1 fv1 r1 r2 = match (r1,r2) with
      | TSucceed,r | r,TSucceed -> r
      | TFail,r | r,TFail -> TFail
      | TCapt (f,r1), r2 | r2, TCapt (f,r1) -> capt f (conj a1 fv1 r1 r2)
      | r1,r2 -> TConj (a1,fv1,r1,r2)

    let constrain a t = 
      if Types.disjoint a t then TFail
      else if Types.subtype t a then (
(*      Format.fprintf Format.std_formatter
          "Optimize constraint -> Succeed  a=%a t=%a@."
          Types.Print.print a
          Types.Print.print t; *)
        TSucceed
      )
      else TConstr (a,t)

    let alt p a1 r1 r2 = match (r1,r2) with
      | TFail,r | r,TFail -> r
      | TSucceed, _ -> assert false
          (* Note: this cannot happen because if the lhs succeeds,
             then the rhs must fail (it is evaluated under
             the assumption that the lhs fails, so the static
             assumption is empty in this case). *)
      | r1,r2 -> TAlt (p,a1,r1,r2)

    let rec print ppf = function
      | TSucceed -> Format.fprintf ppf "Succeed"
      | TFail -> Format.fprintf ppf "Fail"
      | TConstr (t,s) -> 
          Format.fprintf ppf "%a/%a" 
            Types.Print.print t
            Types.Print.print s
      | TCapt (pr,r) ->
          Format.fprintf ppf "{%a}(%a)" TargExpr.print pr print r
      | TAlt (_,_,l,r) -> 
          Format.fprintf ppf "(%a | %a)" print l print r
      | TConj (_,_,l,r) -> 
          Format.fprintf ppf "(%a & %a)" print l print r
      | TRecord (_,_,t,xs,l,q) -> 
          Format.fprintf ppf "<t=%a;xs=%a;{%a=%a}>"
            Types.Print.print t
            Print.print_xs xs
            Label.print (LabelPool.value l)
            Print.print q.descr
      | TTimes (kind,_,_,t,xs,q1,q2) ->
          Format.fprintf ppf "<t=%a;xs=%a;(%a,%a)>"
            Types.Print.print t
            Print.print_xs xs
            Print.print q1.descr
            Print.print q2.descr

    exception NotAResult

    let get_result = function
      | TSucceed -> Some TargExpr.empty
      | TCapt (r,TSucceed) -> Some r
      | TFail -> None
      | r -> raise NotAResult
(*
          Format.fprintf Format.std_formatter "ERR: %a@." print r;
*)

          
    let print_result ppf = function
      | None -> Format.fprintf ppf "Fail"
      | Some r -> TargExpr.print ppf r


    let uid = ref 0
    let rec mk ((a,fv,d) as p) = match d with
      | Constr t -> TConstr (t, any_or_abs)
      | Cup ((a1,_,_) as p1,p2) -> TAlt (p, a1,mk p1, mk p2)
      | Cap ((a1,fv1,_) as p1,p2) -> TConj (a1,fv1,mk p1,mk p2)
      | Capture x -> success_if_present (TargExpr.capture x)
      | Constant (x,c) -> success_if_present (TargExpr.cst x c)
      | Times (q1,q2) -> 
          TTimes (`Normal,(incr uid; !uid), p, any_or_abs,fv,q1,q2)
      | Xml (q1,q2) -> 
          TTimes (`XML,(incr uid; !uid), p,any_or_abs,fv,q1,q2)
      | Record (l,q) -> 
          TRecord ((incr uid; !uid),p, any_or_abs,fv,l,q)
      | Dummy -> assert false

 
    let approx_var p t xs f =
      let vs = Approx.approx_var p t xs in
      let xs = IdSet.diff xs vs in
      let pr = f vs in
      (pr,xs)

    let approx_cst p t xs f =
      let vs = Approx.approx_cst p t xs in
      let xs = IdSet.diff xs (IdMap.domain vs) in
      let pr = f vs in
      (pr,xs)

   let factorize ((a,_,_) as p) t xs f =
      if Types.disjoint a t then TFail
      else
(*      let () = Format.fprintf Format.std_formatter
          "Factorize p=%a t=%a a=%a@."
          Print.print p
          Types.Print.print t
          Types.Print.print a in *)
        let pr,xs = approx_var p t xs TargExpr.captures in
        let pr',xs = approx_cst p t xs TargExpr.constants in
        let pr = TargExpr.merge pr pr' in
        capt pr (if (IdSet.is_empty xs) then constrain a t else f xs)


    let rec optimize t xs = function
      | TCapt (pr,p) ->
          let pr = IdMap.restrict pr xs in
          capt pr (optimize t (IdSet.diff xs (IdMap.domain pr)) p)
      | TAlt (p,a1,p1,p2) ->
          factorize p t xs 
            (fun xs ->
               alt p a1 (optimize t xs p1) (optimize (Types.diff t a1) xs p2))
      | TConj (a1,fv1,p1,p2) ->
          (* We don't factorize above a & pattern eagerly, because
             if factorization would occur, it would also
             occur below and be lifted by the conj function, which
             produces the same effect. *)
          conj a1 fv1
            (optimize t (IdSet.cap xs fv1) p1)
            (optimize (Types.cap t a1) (IdSet.diff xs fv1) p2)
      | TConstr (a,_) -> constrain a t
      | TTimes (kind,uid, p,_,_,q1,q2) ->
          factorize p t xs (fun xs -> TTimes (kind,uid, p,t,xs,q1,q2))
      | TRecord (uid,p,_,_,l,q) ->
          factorize p t xs (fun xs -> TRecord (uid,p,t,xs,l,q))
      | TSucceed -> if Types.is_empty t then TFail else TSucceed
      | TFail -> TFail

(*
    let optimize t xs p =
      let p' = optimize t xs p in
      Format.fprintf Format.std_formatter
        "Optimize %a // (t=%a) ===> %a@."
        print p
        Types.Print.print t
        print p';
      p'
*)

    let fold f accu = function
      | TCapt (_,p) -> f accu p
      | TAlt (_,_,p1,p2) | TConj (_,_,p1,p2) -> f (f accu p1) p2
      | _ -> accu

    let iter f = function
      | TCapt (_,p) -> f p
      | TAlt (_,_,p1,p2) | TConj (_,_,p1,p2) -> f p1; f p2
      | _ -> ()

    let map f = function
      | TCapt (pr,p) -> capt pr (f p)
      | TAlt (p,a1,p1,p2) -> alt p a1 (f p1) (f p2)
      | TConj (a1,fv1,p1,p2) -> conj a1 fv1 (f p1) (f p2)
      | x -> x

    let iter_constr f = 
      let rec aux = function
        | TConstr (t,s) -> f (t,s)
        | p -> iter aux p 
      in aux

    let iter_times k f =
      let rec aux = function
        | TTimes (kind,uid,_,t,xs,q1,q2) when k == kind -> f (uid,t,xs,q1,q2)
        | p -> iter aux p
      in aux

    let iter_records f =
      let rec aux = function
        | TRecord (uid,_,t,xs,l,q) -> f (uid,t,xs,l,q)
        | p -> iter aux p
      in aux

    let iter_field l f =
      let rec aux = function
        | TRecord (uid,_,t,xs,l',q) when l == l' -> f (uid,t,xs,q)
        | p -> iter aux p
      in aux

    let opt_all t0 =
      List.map 
        (fun (p,t,xs) -> 
           if Types.subtype t t0 then (p,t,xs) 
           else let t = Types.cap t t0 in (optimize t xs p, t, xs))

    let get_results reqs =
      List.map (fun (p,_,_) -> get_result p) reqs

    let iter_all f g reqs =
      List.iter (fun (p,_,_) -> f g p) reqs

    let get_all pi get sel extract iter side reqs =
      let extra = ref [] in
      let res = ref empty_reqs in
      let aux3 s1 t12 = 
        let t1 = sel t12 in
        if not ((Types.subtype s1 t1) || (Types.disjoint s1 t1)) 
        then res := add_req !res (constr t1) s1 IdSet.empty in
      let aux2 (t,s) = List.iter (aux3 (pi s)) (get (Types.cap t s)) in
      let aux z =
        let uid,t,xs,q = extract z in
        let xs = IdSet.cap xs q.fv and p = q.descr and t = pi t in

(*      let p = cap p (constr Types.any) in *)
        let pr,xs = approx_var p t xs side in
        let pr',xs = approx_cst p t xs TargExpr.constants in
        let pr = TargExpr.merge pr pr' in

        extra := (uid,pr)::!extra;
        if not ((IdSet.is_empty xs) 
                && (Types.subtype t (Types.descr q.accept))) then
        res := add_req !res p t xs in
      iter_all iter aux reqs;
      iter_all iter_constr aux2 reqs;
      !extra,!res

    let prod_all k side pi sel selq reqs = 
      get_all pi (fun t -> Types.Product.clean_normal (Types.Product.normal ~kind:k t)) sel
        (fun (uid,t,xs,q1,q2) -> uid,t,xs,selq (q1,q2))
        (iter_times k)
        side
        reqs

    let all_labels reqs =
      let res = ref LabelSet.empty in
      let aux2 (t,_) = res := LabelSet.cup !res (Types.Record.all_labels t) in
      let aux (_,_,_,l,_) = res := LabelSet.add l !res in
      iter_all iter_records aux reqs;
      iter_all iter_constr aux2 reqs;
      LabelSet.get !res

    let record_all l reqs =
      let extra,res =
        get_all (Types.Record.pi l) (fun t -> Types.Record.split_normal t l) fst
          (fun z -> z)
          (iter_field l)
          TargExpr.captures_left
          reqs in
      extra,res

   let rec find_binds q reqs binds fetch =
      match (reqs,binds) with
        | (p2,_)::_, Some b::_ when Pat.equal q.descr p2 ->
            IdMap.map fetch b
        | _::reqs, _::binds -> find_binds q reqs binds fetch
        | _ -> raise Not_found
    let find_binds q reqs binds fetch uid extra =
      let r = List.assq uid extra in
      try TargExpr.merge r (find_binds q (PatList.Map.get reqs) binds fetch)
      with Not_found -> r

    let pair swap l r = let (l,r) = swap (l,r) in  TargExpr.SrcPair (l,r) 
    let rec set_times k swap swap' extra1 extra2 reqs1 reqs2 binds1 binds2 = 
      let rec aux = function
        | TTimes (kind,uid,_,t,xs,q1,q2) when k == kind->
            let (q1,q2) = swap (q1,q2) in
            let r1 = find_binds q1 reqs1 binds1 TargExpr.fetch_left uid extra1
            and r2 = find_binds q2 reqs2 binds2 TargExpr.fetch_right uid extra2
            in
            let r = IdMap.merge (pair swap') r1 r2 in
            success (IdMap.restrict r xs)
        | x -> map aux x
      in
      aux

    let rec set_field l locals extra1 reqs1 binds1 =
      let rec aux = function
        | TRecord (uid,_,t,xs,l',q) when l == l' ->
            let r = find_binds q reqs1 binds1 
              (TargExpr.fetch_local locals) uid extra1
            in
            success (IdMap.restrict r xs)
        | x -> map aux x
      in
      aux


    let mkopt p t xs = optimize t xs (mk p)

    let demo ppf ((_,fv,_) as p) t =
      let p = mk p in
(*       Format.fprintf ppf "%a@." print p; *)
      let p = optimize t fv p in
      Format.fprintf ppf "%a@." print p;
      Format.fprintf ppf "@.Fields:@.";
      iter_records
        (fun (_,t,xs,l,q) -> 
           Format.fprintf ppf "(%a=%a) / %a@."
             print_lab l
             Print.print q.descr
             Types.Print.print (Types.Record.project_opt t l)
        ) p

  end

  type output = Types.t * int * int id_map option list
      (* Obtained type, arity, bindings *)

  type rescode =
    | RFail
    | RCode of int
    | RSwitch of rescode * rescode
    | RIgnore of rescode
        
  type result = int * TargExpr.source array
  type actions = 
    | AResult of result
    | AKind of actions_kind
  and actions_kind = {
    basic: (Types.t * result) list;
    atoms: result Atoms.map;