viewcvs.cgi/types/patterns.ml

exception Error of string
open Ident

(*
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 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 q2.descr
    | Xml _ -> assert false
    | Record (l,q) ->
        Format.fprintf ppf "{%a=%a}" Label.print (LabelPool.value l) print q.descr
    | Capture x ->
        Format.fprintf ppf "%a" Ident.print x
    | Constant (x,c) ->
        Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.print_const c
    | Dummy -> assert false
      
  let print ppf p =
    mark S.empty p;
    print ppf p;
    let first = ref true in
    (try while true do
       let p = Queue.pop toprint in
       if not (S.mem p !printed) then 
         ( printed := S.add p !printed;
           Format.fprintf ppf " %s@ @[%a=%a@]"
             (if !first then (first := false; "where") else "and")
             print p
             real_print p
        );
     done with Queue.Empty -> ());
    id := 0;
    names := M.empty;
    printed := S.empty


  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


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)


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

  let check_nnf (pl,t) =
    List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
      (NodeSet.get pl)

  let print_nnf ppf (pl,t) =
    Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t
                            

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

  let hash_nnf (l,t) =
    (NodeSet.hash l) + 17 * (Types.hash t)

  module NLineBasic = 
    SortedList.Make(
      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 NLineProd = 
    SortedList.Make(
      struct
(*      include Custom.Dummy*)
        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
            print_nnf x
            print_nnf y
        type t = result * nnf * nnf
        let compare (r1,x1,y1) (r2,x2,y2) =
          let c = compare_result r1 r2 in if c <> 0 then c
          else let c = compare_nnf x1 x2 in if c <> 0 then c
          else compare_nnf y1 y2
        let equal x y = compare x y == 0
        let hash (r,x,y) =
          hash_result r + 17 * (hash_nnf x) + 267 * (hash_nnf y)
      end
    )

  type record =
    | RecNolabel of result option * result option
    | RecLabel of label * NLineProd.t
  type t = {
    nfv    : fv;
    ncatchv: 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
      

  let compare_nf t1 t2 =
    if t1 == t2 then 0
    else
      (* TODO: reorder; remove comparison of nfv ? *)
      let c = IdSet.compare t1.nfv t2.nfv in if c <> 0 then c 
      else let c = IdSet.compare t1.ncatchv t2.ncatchv in if c <> 0 then c
      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 match t1.nrecord, t2.nrecord with
        | RecNolabel (s1,n1), RecNolabel (s2,n2) ->
            let c = match (s1,s2) with
              | None,None -> 0
              | Some r1, Some r2 -> compare_result r1 r2
              | None, _ -> -1
              | _, None -> 1 in
            if c <> 0 then c 
            else (match (n1,n2) with
              | None,None -> 0
              | Some r1, Some r2 -> compare_result r1 r2
              | None, _ -> -1
              | _, None -> 1)
        | RecNolabel (_,_), _ -> -1
        | _, RecNolabel (_,_) -> 1
        | RecLabel (l1,p1), RecLabel (l2,p2) ->
            let c = LabelPool.compare l1 l2 in if c <> 0 then c
            else NLineProd.compare p1 p2

  let fus = IdMap.union_disj

  let nempty lab = 
    { nfv = IdSet.empty; ncatchv = 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;
      ncatchv = IdSet.cap nf1.ncatchv nf2.ncatchv;
      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),(ql1,s1)) (res2,(pl2,t2),(ql2,s2)) =
      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),(NodeSet.cup ql1 ql2,s)) 
          :: 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;
      ncatchv = IdSet.cup nf1.ncatchv nf2.ncatchv;
      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 = NodeSet.singleton p, Types.descr p.accept
  let nc t = NodeSet.empty, t
  let ncany = nc Types.any

  let empty_res = IdMap.empty

  let ntimes lab acc p q = 
    let src_p = IdMap.constant SLeft p.fv
    and src_q = IdMap.constant SRight q.fv in
    let src = IdMap.merge_elem SRecompose src_p src_q in 
    { nempty lab with 
        nfv = IdSet.cup p.fv q.fv; 
        na = acc;
        nprod = NLineProd.singleton (src, nnode p, nnode q);
    }

  let nxml lab acc p q = 
    let src_p = IdMap.constant SLeft p.fv
    and src_q = IdMap.constant SRight q.fv in
    let src = IdMap.merge_elem SRecompose src_p src_q in 
    { nempty lab with 
        nfv = IdSet.cup p.fv q.fv; 
        na = acc;
        nxml =  NLineProd.singleton (src, nnode p, nnode q);
    }
    
  let nrecord lab acc l p =
    match lab with
      | None -> assert false
      | Some label ->
          assert (label <= l);
          if l == label then
            let src = IdMap.constant SLeft p.fv in
            { nempty lab with
                nfv = p.fv;
                na = acc;
                nrecord = RecLabel(label, 
                                 NLineProd.singleton (src,nnode p, ncany))}
          else
            let src = IdMap.constant SRight p.fv in
            let p' = make p.fv in  (* optimize this ... *)
              (* cache the results to avoid looping ... *)
            define p' (record l p);
            { nempty lab with
                nfv = p.fv;
                na = acc;
                nrecord = 
                      RecLabel(label,
                        NLineProd.singleton(src,nc Types.Record.any_or_absent, 
                         nnode p') )}
          

  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 ->
(*
            let ppf = Format.std_formatter in
            Format.fprintf ppf "Constr record t=%a l=%a@."
              Types.Print.print t Label.print (LabelPool.value l);
            let sp = Types.Record.split_normal t l in
            List.iter (fun (t1,t2) ->
                         Format.fprintf ppf "t1=%a t2=%a@."
                           Types.Print.print t1
                           Types.Print.print t2) sp;
*)
            RecLabel (l,aux (Types.Record.split_normal t l))
    in        
    { nempty lab with
        na = t;
        nbasic = NLineBasic.singleton (empty_res, Types.cap t any_basic);
        nprod = aux (Types.Product.normal t);
        nxml  = aux (Types.Product.normal ~kind:`XML t);
        nrecord = record
    }

  let nconstant lab x c = 
    let l = IdMap.singleton x (SConst c) in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.empty;
      na = Types.any;
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
      nrecord = match lab with
        | None -> RecNolabel (Some l, Some l)
        | Some lab -> 
            RecLabel (lab, NLineProd.singleton 
                        (l,nc Types.Record.any_or_absent,
                                 ncany))
    }

  let ncapture lab x = 
    let l = IdMap.singleton x SCatch in
    { nfv = IdSet.singleton x;
      ncatchv = IdSet.singleton x;
      na = Types.any;
      nbasic = NLineBasic.singleton (l,any_basic); 
      nprod  = NLineProd.singleton (l,ncany,ncany);
      nxml   = NLineProd.singleton (l,ncany,ncany);
      nrecord = match lab with
        | None -> RecNolabel (Some l, Some l)
        | Some lab -> 
            RecLabel (lab, NLineProd.singleton 
                        (l,nc Types.Record.any_or_absent,
                                 ncany))
    }

  let rec nnormal lab (acc,fv,d) =
    if Types.is_empty acc 
    then nempty lab
    else match d with
      | Constr t -> nconstr lab t
      | Cap (p,q) -> ncap (nnormal lab p) (nnormal lab q)
      | Cup ((acc1,_,_) as p,q) -> 
          ncup (nnormal lab p) (ncap (nnormal lab q) 
                                  (nconstr lab (Types.neg acc1)))
      | Times (p,q) -> ntimes lab acc p q
      | Xml (p,q) -> nxml lab acc p q
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
      | Record (l,p) -> nrecord lab acc l p
      | Dummy -> assert false

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

  let rec first_label (acc,fv,d) =
    if Types.is_empty acc 
    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)
            (* should "first_label_type acc1" ? *)
      | Record (l,p) -> l
      | _ -> LabelPool.dummy_max

   
  let remove_catchv n =
    let ncv = n.ncatchv in
    let nlinesbasic l = 
      NLineBasic.map (fun (res,x) -> (IdMap.diff res ncv,x)) l in
    let nlinesprod l  = 
      NLineProd.map (fun (res,x,y) -> (IdMap.diff res ncv,x,y)) l in
    { nfv     = IdSet.diff n.nfv ncv;
      ncatchv = n.ncatchv;
      na      = n.na;
      nbasic  = nlinesbasic n.nbasic;
      nprod   = nlinesprod n.nprod;
      nxml    = nlinesprod n.nxml;
      nrecord = (match n.nrecord with
                   | RecNolabel (x,y) ->
                       let x = match x with 
                         | Some res -> Some (IdMap.diff res ncv) 
                         | None -> None in
                       let y = match y with 
                         | Some res -> Some (IdMap.diff res ncv) 
                         | None -> None in
                       RecNolabel (x,y)
                   | RecLabel (lab,l) -> RecLabel (lab, nlinesprod l))
    }

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

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

(*
  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 * int id_map) list

  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 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 array_for_all f a =
    let rec aux f a i =
      if i == Array.length a then true
      else f a.(i) && (aux f a (succ i))
    in
    aux f a 0

  let array_for_all_i f a =
    let rec aux f a i =
      if i == Array.length a then true
      else f i a.(i) && (aux f a (succ i))
    in
    aux f a 0

  let combine_kind basic prod xml record =
    try (
      let rs = [] in
      let rs = match basic with
        | [_,r] -> r :: rs
        | [] -> rs
        | _ -> raise Exit in
      let rs = match prod with
        | Impossible -> rs
        | Ignore (Ignore r) -> r :: rs
        | _ -> raise Exit in
      let rs = match xml with
        | Impossible -> rs
        | Ignore (Ignore r) -> r :: rs
        | _ -> raise Exit in
      let rs = match record with
        | None -> rs
        | Some (RecLabel (_,Ignore (Ignore r))) -> r :: rs
        | Some (RecNolabel (Some r1, Some r2)) -> r1 :: r2 :: rs
        | _ -> raise Exit in
      match rs with
        | ((_, ret) as r) :: rs when 
            List.for_all ( equal_result r ) rs 
            && array_for_all 
              (function Catch | Const _ -> true | _ -> false) ret
            -> AIgnore r
        | _ -> raise Exit
    )
    with Exit -> 
      AKind 
      { 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 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_right_tail_call = function
    | Dispatch (disp,branches) 
        when
          array_for_all_i
            (fun i (code,ret) ->
               (i == code) && 
               (array_for_all_i 
                  (fun pos -> 
                     function Right j when pos == j -> true | _ -> false)
                  ret
               )
            ) branches
          -> TailCall disp
    | x -> x

  let detect_left_tail_call = function
    | Dispatch (disp,branches)
        when
          array_for_all_i
            (fun i -> 
               function 
                 | Ignore (code,ret) ->
                     (i == code) &&
                     (array_for_all_i 
                        (fun pos -> 
                           function Left j when pos == j -> true | _ -> false)
                        ret
               )
                 | _ -> false
            ) branches
          ->
         TailCall disp
    | x -> x
   
  let cur_id = State.ref "Patterns.cur_id" 0
                 (* TODO: save dispatchers ? *)
                 
  module NfMap = Map.Make(
    struct 
      type t = Normal.t
      let compare = Normal.compare_nf
    end)

  module DispMap = Map.Make(
    struct
      type t = Types.t * Normal.t array

      let rec compare_rec a1 a2 i =
        if i < 0 then 0 
        else
          let c = Normal.compare_nf a1.(i) a2.(i) in
          if c <> 0 then c else compare_rec a1 a2 (i - 1)
          
      let compare (t1,a1) (t2,a2) =
        let c = Types.compare t1 t2 in if c <> 0 then c 
        else let l1 = Array.length a1 and l2 = Array.length a2 in
        if l1 < l2 then -1 else if l1 > l2 then 1
        else compare_rec a1 a2 (l1 - 1)
    end
  )

    (* 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 ppf = Format.std_formatter in
      Format.fprintf ppf "dispatcher %i:" !cur_id;
      Array.iter (fun x -> Format.fprintf ppf "%a;" Normal.print x) pl;
      Format.fprintf ppf "@."; *)
      let nb = ref 0 in
      let codes = ref [] in
      let rec aux t arity i accu = 
        if i == Array.length pl 
        then (incr nb; codes := (t,arity,accu)::!codes; `Result (!nb - 1))
        else
          let p = pl.(i) in
          let tp = p.Normal.na in
(*        let tp = Types.normalize tp in *) 

          let a1 = Types.cap t tp in
          if Types.is_empty a1 then
            `Switch (`None,aux t arity (i+1) accu)
          else
            let v = p.Normal.nfv in
            let a2 = Types.diff t tp in
            let accu' = (i,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) 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
(*
      Array.iteri (fun i p ->
                     Format.fprintf Format.std_formatter
                       "Pattern %i/%i accepts %a@." i (Array.length pl)
                       Types.Print.print p.Normal.na) pl; 
*)
      
      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 ();
(*      Format.fprintf Format.std_formatter "iface=%a@." print_iface iface;*)
      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
(*
    let ppf = Format.std_formatter in
    Format.fprintf ppf "find_code iface=%a [ "
      print_iface d.interface;
    for i = 0 to Array.length a - 1 do
      if (a.(i) != None) then
        Format.fprintf ppf "+ "
      else
        Format.fprintf ppf "- "
    done;
    Format.fprintf ppf "]@.";
*)
    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 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;
            
            let aux_final res = IdMap.map_to_list conv_source_basic res in
            accu := (t, return disp selected aux_final) :: !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 get_tests pl f t d post =
    let accu = ref [] in
    let aux i x = 
      let (pl,ty), info = f x in
      let pl = Normal.NodeSet.get pl in
      accu := (ty,pl,i,info) :: !accu in
    Array.iteri (fun i -> List.iter (aux i)) pl;

    let lab =
      List.fold_left 
        (fun l (ty,pl,_,_) ->
           List.fold_left
             (fun l p -> min l (Normal.first_label (descr p)))
             (min l (Types.Record.first_label ty))
             pl
        ) LabelPool.dummy_max !accu in
    let lab = if lab == LabelPool.dummy_max then None else Some lab in


    let pats = ref NfMap.empty in
    let nb_p = ref 0 in
    List.iter
      (fun (ty,pl,i,info) -> 
         let p = Normal.normal lab ty pl in
         let x = (i, p.Normal.ncatchv, info) in
         try 
           let s = NfMap.find p !pats in
           s := x :: !s
         with Not_found ->
           pats := NfMap.add p (ref [x]) !pats;
           incr nb_p
      ) !accu;
    let infos = Array.make !nb_p [] in
    let ps = Array.make !nb_p Normal.dummy in
    let count = ref 0 in
    NfMap.iter (fun p l ->
                  let i = !count in
                  infos.(i) <- !l;
                  ps.(i) <- p;
                  count := succ i) !pats;
    assert( !nb_p == !count );
    let disp = dispatcher t ps lab in

    let result (t,_,m) =
(*    Format.fprintf Format.std_formatter "Result=%a@." Types.Print.print t;*)
      let selected = Array.create (Array.length pl) [] in
      let add r (i, ncv, inf) = selected.(i) <- (r,ncv,inf) :: selected.(i) in
      List.iter (fun (j,r) -> List.iter (add r) infos.(j)) m;
      d t selected
    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 (_,brs) = 
      List.fold_left
        (fun (t,brs) (p,e) ->
           let p' = (Normal.NodeSet.singleton p,t) in
(*         let td = Types.descr (accept p) in
           let t' = 
             if Types.is_empty (Types.cap t td) then t else
               Types.diff t td in*)
           let t' = Types.diff t (Types.descr (accept p)) in
           (t', (p',(fv p, e)) :: brs)
        ) (t,[]) brs in
        
    let pl = Array.map (fun x -> [x]) (Array.of_list brs) in
    get_tests 
      pl 
      (fun x -> x)
      t
      (fun _ pl ->
         let r = ref Fail in
         let aux = function 
           | [(res,catchv,(fvl,e))] -> assert (!r == Fail); 
               let catchv = IdMap.constant (-1) catchv in
               let m = IdMap.union_disj catchv res in
               let m = List.map (fun x -> (x,IdMap.assoc x m)) fvl in
               r := Match (m,e)
           | [] -> () | _ -> assert false in
         Array.iter aux pl;
         !r
      )
      (fun x -> x)


  let rec dispatch_prod ?(kind=`Normal) disp =
    let pl = 
      match kind with
        | `Normal ->  
            Array.map (fun p -> Normal.NLineProd.get p.Normal.nprod) disp.pl
        | `XML -> 
            Array.map (fun p -> Normal.NLineProd.get p.Normal.nxml) disp.pl
    in
    let t = Types.Product.get ~kind disp.t in
    dispatch_prod0 disp t 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, ncatchv, (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, ncatchv, (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 =
              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 ->
(*          Format.fprintf Format.std_formatter "lab=%a Split:@." Label.print (LabelPool.value lab);*)
            let t = Types.Record.split t lab in
(*          List.iter (fun (t1,t2) ->
                         Format.fprintf Format.std_formatter "t1=%a t2=%a@."
                           Types.Print.print t1
                           Types.Print.print t2) t; *)
            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))
(* soucis avec les ncatchv ?? *)

      
  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 (Normal.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]) pl) in

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


(* New compilation procedure *)

module Compile2 = struct

  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 t = Types.Product.pi1 (Types.Product.get t)
  let pi2 t = Types.Product.pi2 (Types.Product.get 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