patterns.ml

type capture = string
type fv = capture SortedList.t

exception Error of string


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

let id x = x.id
let descr x = match x.descr with Some d -> d | None -> failwith "Patterns.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) = 
(*  Format.fprintf ppf "[%a]" Types.Print.print_descr a; *)
  match d with
    | Constr t -> Types.Print.print_descr 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 "{ %s =  P%i }" (Types.LabelPool.value l) n.id;
	to_print := n :: !to_print
    | Capture x ->
	Format.fprintf ppf "%s" x
    | Constant (x,c) ->
	Format.fprintf ppf "(%s := %a)" x Types.Print.print_const c

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 counter = State.ref "Patterns.counter" 0

let make fv =
  incr counter;
  { id = !counter; descr = None; accept = Types.make (); fv = fv }

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

let constr x = (x,[],Constr x)
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
  if fv1 <> fv2 then (
    let x = match SortedList.diff fv1 fv2 with
      | x::_ -> x
      | [] -> match SortedList.diff fv2 fv1 with x::_ -> x | _ -> assert false
    in
    raise 
      (Error 
	 ("The capture variable " ^ x ^ 
	  " should appear on both side of this | pattern"))
  );
  (Types.cup acc1 acc2, SortedList.cup fv1 fv2, Cup (x1,x2))
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
  if not (SortedList.disjoint fv1 fv2) then (
    match SortedList.cap fv1 fv2 with
      | x::_ -> 
	  raise 
	  (Error 
	     ("The capture variable " ^ x ^ 
	      " cannot appear on both side of this & pattern"))
      | _ -> assert false
  );
  (Types.cap acc1 acc2, SortedList.cup fv1 fv2, Cap (x1,x2))
let times x y =
  (Types.times x.accept y.accept, SortedList.cup x.fv y.fv, Times (x,y))
let xml x y =
  (Types.xml x.accept y.accept, SortedList.cup x.fv y.fv, Xml (x,y))
let record l x = 
  (Types.record l false x.accept, x.fv, Record (l,x))
let capture x = (Types.any, [x], Capture x)
let constant x c = (Types.any, [x], Constant (x,c))




(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
let empty_res fv = List.map (fun v -> (v, Types.Positive.ty Types.empty)) fv
let times_res v1 v2 = Types.Positive.times v1 v2

module MemoFilter = Map.Make 
  (struct type t = Types.descr * node let compare = compare end)

let memo_filter = ref MemoFilter.empty

let rec filter_descr t (_,fv,d) : (capture, Types.Positive.v) SortedMap.t =
(* 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 _ -> []
      | Cup ((a,_,_) as d1,d2) ->
	  SortedMap.union cup_res
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
      | Cap (d1,d2) ->
	  SortedMap.union 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 ->
	  [(c, Types.Positive.ty t)]
      | Constant (c, cst) ->
	  [(c, Types.Positive.ty (Types.constant cst))]

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


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

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
  List.map (fun (c,v) -> (c,Types.Positive.solve v)) r



(* Returns a pattern q equivalent to p when applied to a
   value of type t *)
(*
module Compiler = 
struct
  type dispatcher = {
    did      : int;
    nb_codes : int;
    results  : res;
    t        : Types.descr;
    pats     : (node option * Types.descr) SortedList.t;
    mutable actions  : actions option;
  }
  and bind = (capture, int) SortedMap.t
  and res = [ `Return of Types.descr * int 
	    | `Fail 
	    | `Branch of (bind * res * res) ]
  and 'a dispatch = dispatcher * 'a array
  and actions = { 
    act_basic: basic_actions;
    act_prod : prod_actions 
  }
  and prod_actions = (int * prod_src list) dispatch dispatch
  and basic_actions = (Types.descr * (int * basic_src list)) SortedList.t
  and prod_src = [ `Capture |  `Const of Types.const 
		 | `Combine of int * int | `Left of int | `Right of int ]
  and basic_src = [ `Capture |  `Const of Types.const ]



  module DispMap = Map.Make(
    struct
      type t = Types.descr * (node option * Types.descr) SortedList.t
      let compare = compare
    end
  )
    
  let dispatchers = ref DispMap.empty
  let nb_disp = ref 0		  

  let rec make_res codes pos t l =
    if Types.is_empty t then `Fail
    else match l with
      | [] -> 
	  incr codes; `Return (t, !codes - 1)
      | (p,restr)::rem ->
	  let (pos,bind,a) = match p with
	    | Some p -> 
		let pos = ref pos in
		let bind = List.map (fun v -> incr pos; (v,!pos-1)) (fv p) in
		(!pos,bind,Types.cap restr (Types.descr (accept p)))
	    | None -> (pos,[],restr)
	  in
(*	  assert (Types.subtype restr t);*)
	  let yes = make_res codes pos (Types.cap t a) rem
	  and no = make_res codes pos (Types.diff t a) rem in
	  `Branch (bind,yes,no)
	    
    
  let make_dispatcher t pats =
    try DispMap.find (t,pats) !dispatchers
    with Not_found ->
      incr nb_disp;
      let nbc = ref 0 in
      let res = make_res nbc 0 t pats in
      let d = { did = !nb_disp; 
		pats = pats;
		t = t;
		results = res; 
		nb_codes = !nbc; 
		actions = None } in
      dispatchers := DispMap.add (t,pats) d !dispatchers;
      d

  let rec find_code accu = function
    | (`Return (_,c),[]) -> 
	(c,List.rev accu)
    | (`Branch (_,_,no),None::rem) -> 
	find_code accu (no,rem)
    | (`Branch (_,yes,_),Some x::rem) -> 
	find_code (List.rev_append x accu) (yes,rem)
    | (`Fail,_) -> assert false
    | _ -> assert false 


  let dispatcher t (args : (node option * Types.descr * bind option ref) 
		      list) f =
(*    let args = 
      List.map
	(function 
	   | (`Pat p, s, r) -> (`Pat p, Types.cap t s, r)
	   | (`Typ c, s, r) -> 
	       let s = Types.cap t s in
	       (`Typ (Types.cap c s), s, r)) args in *)
    let args = List.map (fun (p,restr,flag) -> ((p,restr),[flag])) args in
    let args = SortedMap.from_list (@) args in
    let pats = List.map fst args in
    let d = make_dispatcher t pats in
    let res = Array.create d.nb_codes (Obj.magic 0) in
    let rec aux = function
      | (`Fail,_) -> ()
      | (`Return (t,c), []) -> res.(c) <- f t
      | (`Branch (bind,yes,no), (_,fls)::rem) ->
	  List.iter (fun r -> r := Some bind) fls; aux (yes,rem);
	  List.iter (fun r -> r := None) fls; aux (no,rem)
      | _ -> assert false
    in
    aux (d.results,args);
    (d,res)

	   

  let sort_list l =
    Array.of_list (SortedList.from_list l)

  type 'a pat =
    | One
    | Zero
    | Capt of Types.descr * capture
    | Const of Types.descr * capture * Types.const
    | Alt of 'a pat * 'a pat
    | And of 'a pat * 'a pat
    | Atom of 'a

  let rec print f ppf = function
    | One -> Format.fprintf ppf "One"
    | Zero -> Format.fprintf ppf "Zero"
    | Capt (t,x) -> 
	Format.fprintf ppf "[%a]%s" Types.Print.print_descr t x
    | Const (t,x,c) -> 
	Format.fprintf ppf "[%a](%s:=%a)" Types.Print.print_descr t 
	x Types.Print.print_const c
    | Alt (p1,p2) -> Format.fprintf ppf "(%a | %a)" (print f) p1 (print f) p2
    | And (p1,p2) -> Format.fprintf ppf "(%a & %a)" (print f) p1 (print f) p2
    | Atom a -> Format.fprintf ppf "%a" f a

  let alt = function
    | (Zero,p) | (p,Zero) -> p
    | (p1,p2) -> Alt (p1,p2)

  let and_ = function
    | (Zero,_) | (_,Zero) -> Zero
    | (One,p) | (p,One) -> p
    | (p1,p2) -> And (p1,p2)

(*
debug compile2 (Int,Int)|(Char,Char) (Int,x)|(x,Char);;
*)

(*
  let atom s a p =
    if Types.is_empty (Types.cap s a) then Zero else
      Atom (s, p)
*)

  let rec map f = function
    | One -> One
    | Zero -> Zero
    | Capt (t,x) -> Capt (t,x)
    | Const (t,x,c) -> Const (t,x,c)
    | Alt (p1,p2) -> alt (map f p1, map f p2)
    | And (p1,p2) -> and_ (map f p1, map f p2)
    | Atom a -> f a

  let rec get f (a,_,d) s =
    let s = Types.cap s a in
    if Types.is_empty s then Zero 
    else match d with
      | Cup ((a1,_,_) as d1,d2) ->
	  let p1 = get f d1 s in
	  let p2 = get f d2 (Types.diff s a1) in
	  alt (p1,p2)
      | Cap ((a1,_,_) as d1,d2) ->
	  let p1 = get f d1 s in
	  let p2 = get f d2 s in
	  and_ (p1,p2)
      | Capture x ->
	  Capt (s,x)
      | Constant (s,x,c) ->
	  Const (x,c)
      | d -> f d s

  let rec get_final f = function
    | Atom x -> f x
    | One -> Some []
    | Zero -> None
    | Capt (s,x) -> Some [x, `Capture]
    | Const (s,x,c) -> Some [x, `Const c]
    | Alt (p1,p2) ->
	(match get_final f p1 with
	  | Some _ as x -> x
	  | None -> get_final f p2)
    | And (p1,p2) ->
	(match get_final f p1 with
	  | Some x -> 
	      (match get_final f p2 with
		 | Some y -> Some (SortedMap.union_disj x y)
		 | None -> None)
	  | None -> None)

  let get_final f p =
    match get_final f t p with
      | None -> None
      | Some l -> Some (List.map snd l)


  let map_list f =
    List.map (map f)

  let pi1 d = Types.Product.pi1 (Types.Product.get d)
  let pi2 d d1 = Types.Product.pi2 (Types.Product.restrict_1
				      (Types.Product.get d) d1)

  let prepare_prod' =
    get (fun d r ->
	   match d with
	     | Times (n1,n2) ->
		 Atom (Some (n1,n2),r)
	     | Constr _ ->
		 Atom (None,r)
	     | _ -> Zero
	)

  let prepare_prod (p,restr) =
    match p with
      | Some p -> prepare_prod' (descr p) restr
      | None -> Atom (None, restr)
	  (* TODO: special case here ... restr<=t...*)

  let map_prod1 collect (p,r) =
    let (n1,n2) = match p with 
      | Some (n1,n2) -> Some n1, Some n2 
      | None -> None, None in
    let l =
      List.map 
	(fun (r1,r2) ->
	   let fl = ref None in
	   collect := (n1,r1,fl) :: !collect;
	   (fl,n2,r2)
	) (Types.Product.normal r) in
    Atom l


  let map_prod2 collect l =
    let l = 
      List.fold_left
	(fun accu (fl1,n2,r2) ->
	   match !fl1 with
	     | None -> accu
	     | Some bind ->
		 let fl2 = ref None in
		 collect := (n2, r2, fl2) :: !collect;
		 (bind,fl2)::accu
	) [] l in
    Atom l

  let rec prod_final = function
    | [] -> None
    | (bind1,{contents = Some bind2})::_ ->
	Some (SortedMap.combine	
		(fun x -> `Left x) (fun x -> `Right x)
		(fun x y -> `Combine (x,y))
		bind1 bind2)
    | _::rem -> prod_final rem


  let dispatch_prod (res:res) t (pats:(node option * Types.descr) list) : 
    prod_actions =
    let pats = List.map prepare_prod pats in
    let lefts = ref [] in
    let pats =  map_list (map_prod1 lefts) pats in
    dispatcher (pi1 t) !lefts
      (fun t1 ->
	 let rights = ref [] in
	 let pats = map_list (map_prod2 rights) pats in
	 dispatcher (pi2 t t1) !rights
	   (fun t2 ->
	    let pats = List.map (get_final (prod_final)) pats in
	    find_code [] (res,pats)
	   )
      )

  let any_basic = Types.neg (List.fold_left Types.cup Types.empty
			       [Types.Product.any_xml;
				Types.Product.any;
				Types.Record.any])

  let prepare_basic' =
    get (fun d r ->
	   match d with
	     | Constr _ -> Atom r
	     | _ -> Zero)

  let prepare_basic (p,restr) =
    match p with
      | Some p -> prepare_basic' (descr p) restr
      | None -> Atom restr
      
  let basic_final t =
    get_final (
      fun s ->
	if Types.subtype t s then Some []
	else (assert (Types.is_empty (Types.cap t s)); None)
    )

  let dispatch_basic res t pats : basic_actions =
    let types = ref [] in
    let rec aux = function
      | `Fail -> ()
      | `Branch (bind,yes,no) -> aux yes; aux no
      | `Return (t,c) -> 
(*	  Format.fprintf Format.std_formatter "<<<%a -> %i>>>@\n" 
	    Types.Print.print_descr t c; *)
	  let t = Types.cap t any_basic in
	  if not (Types.is_empty t) then types := t :: !types in
    aux res;
    let pats = List.map prepare_basic pats in
    Format.fprintf Format.std_formatter "BASIC:%i@\n" (List.length !types);
    List.iter (fun p -> 
		 Format.fprintf Format.std_formatter
		   "==> %a@\n"
		   (print Types.Print.print_descr) p
	      ) pats;
    List.map
      (fun t ->
	 let pats = List.map (basic_final t) pats in
	 Format.fprintf Format.std_formatter "BASIC:";
	 List.iter (function 
		      | Some _ -> 
			  Format.fprintf Format.std_formatter "YES"
		      | None -> 
			  Format.fprintf Format.std_formatter "NO "
		   ) pats;
	 Format.fprintf Format.std_formatter "@\n";
	 
	 (t, find_code [] (res,pats))
      ) !types


  let get_actions disp =
    match disp.actions with
      | Some a -> a
      | None ->
	  let a = {
	    act_basic = dispatch_basic disp.results disp.t disp.pats;
	    act_prod = dispatch_prod disp.results disp.t disp.pats
	  } in
	  disp.actions <- Some a;
	  a

  let to_print = ref ([] : dispatcher list)
  let printed = ref ([] : dispatcher list)


  let print_act_basic ppf b =
    List.iter 
      (fun (d,(code,bind)) ->
	 Format.fprintf ppf "| %a -> %i( " 
	 Types.Print.print_descr d
	 code;
	 List.iter 
	   (function
	      | `Capture -> 
		  Format.fprintf ppf "v "
	      | `Const c -> 
		  Format.fprintf ppf "%a " Types.Print.print_const c)
	   bind;
	 Format.fprintf ppf ")@\n" 
      ) b

  let print_act_prod ppf (disp1,b1) =
    Format.fprintf ppf "| (v1,v2) -> match v1 with disp%i@\n" disp1.did;
    to_print := disp1 :: !to_print;
    for i = 0 to Array.length b1 - 1 do
     let (disp2,b2) = b1.(i) in
     to_print := disp2 :: !to_print;
      Format.fprintf ppf " | %i(l) -> match v2 with disp%i@\n" i disp2.did;
      for j = 0 to Array.length b2 - 1 do
	let (code,bind) = b2.(j) in
	Format.fprintf ppf "  | %i(r) -> %i(" j code;
	List.iter 
	  (function
	     | `Capture -> 
		 Format.fprintf ppf "v "
	     | `Const c -> 
		 Format.fprintf ppf "%a " Types.Print.print_const c
	     | `Left x ->
		 Format.fprintf ppf "l%i " x
	     | `Right x ->
		 Format.fprintf ppf "r%i " x
	     | `Combine (x,y) ->
		 Format.fprintf ppf "(l%i,r%i) " x y
	  )
	  bind;
	Format.fprintf ppf ")@\n" 
      done;
    done
		 
  let rec print_disp ppf disp =
    Format.fprintf ppf "Dispatcher [%i]: 0..%i@\n" disp.did (disp.nb_codes - 1);
    let a = get_actions disp in
    print_act_basic ppf a.act_basic;
    print_act_prod ppf a.act_prod;

    let rec loop () = 
      match !to_print with
	| [] -> ()
	| d::q -> 
	    to_print := q;
	    if List.memq d !printed then loop ()
	    else (printed := d :: !printed; print_disp ppf d)
    in
    loop ()


(*
let rec collect typ f (a,_,d) s =
  if Types.is_empty (Types.cap s a) then () else
  match d with
    | Constr t -> if not (Types.subtype s a) then typ s (Types.cap s t)
    | Cup ((a1,_,_) as d1,d2) -> 
	collect typ f d1 s; collect typ f d2 (Types.diff s a1)
    | Cap ((a1,_,_) as d1,d2) ->
	collect typ f d1 s;
	collect typ f d2 (Types.cap s a1)
    | Capture _ | Constant (_,_) -> ()
    | d -> f s d

let get_prod =
  get (function Times (n1,n2) -> Some n1 | _ -> None)
let get_record =
  get (function Record (l,n) -> Some (l,n) | _ -> None)

let print_prod =
  print (fun ppf p1 ->
	   Format.fprintf ppf "(P%i)" p1.id
	)
let print_record =
  print (fun ppf (l,p) ->
	   Format.fprintf ppf "{ %s = P%i }" (Types.LabelPool.value l) p.id
	)

let demo ppf p t =
  collect 
    (fun w t -> 
       Format.fprintf ppf "TYP1:%a // %a@\n"
         Types.Print.print_descr t
         Types.Print.print_descr w;
       let n = Types.Product.normal t in
       let pi1 = Types.Product.pi1 (Types.Product.get w) in
       List.iter (fun (d1,d2) ->
		    Format.fprintf ppf "=> %a // %a@\n"
		    Types.Print.print_descr d1
		    Types.Print.print_descr pi1
		 ) n
    )
    (fun w -> function
       | Times (n1,n2) -> 
	   let pi1 = Types.Product.pi1 (Types.Product.get w) in
	   Format.fprintf ppf "PAT1:%i // %a@\n" n1.id 
	     Types.Print.print_descr pi1; 
	   to_print := n1 :: !to_print
       | _ -> ()) p t

*)
end

let demo ppf p t =
(*
  Compiler.demo ppf p t;
  dump_print ppf
*)
(*
  Format.fprintf ppf "PROD:%a@\n" Compiler.print_prod (Compiler.get_prod p (Types.cap Types.Product.any t));
  Format.fprintf ppf "REC :%a@\n" Compiler.print_record (Compiler.get_record p (Types.cap Types.Record.any t))
*)
  ()


let rec restrict ((a,fv,d) as p) t =
  (* TODO OPT: Don't call cup,cap .... *)
  match d with
    | Constr s ->
	constr (Types.cap t a)
	(* Could return any type  (t&s)|u  with u&t=0 *)
    | Cup (((a1,_,_) as p1),((a2,_,_) as p2)) ->
	let p1 = 
	  if Types.is_empty (Types.cap t a1) then None 
	  else Some (restrict p1 t) in
	let p2 =
	  let t' = Types.diff t a1 in
	  if Types.is_empty (Types.cap t' a2) then None 
	  else Some (restrict p2 t') in
	(match (p1,p2) with
	   | Some p1, Some p2 -> cup p1 p2
	   | Some p1, None -> p1
	   | None, Some p2 -> p2
	   | _ -> assert false)
    | Cap (p1,p2) -> cap (restrict p1 t) (restrict p2 t)
(*    | Capture _ | Constant (_,_) -> p *)
    | _ -> p (* (Types.cap a t, fv, d) *)
  
let restrict ((a,fv,_) as p) t =
  if Types.is_empty (Types.cap a t) then `Reject
  else if (fv = []) && (Types.subtype t a) then `Accept
  else `Pat (restrict p t)
*)


(* Normal forms for patterns and compilation *)

module Normal : sig 
  type 'a sl = 'a SortedList.t
  type ('a,'b) sm = ('a,'b) SortedMap.t

  type source = 
      [ `Catch | `Const of Types.const 
      | `Left | `Right | `Recompose 
      | `Field of Types.label 
      ]
  type result = (capture, source) sm

  type nnf = node sl * Types.descr
  type 'a nline = (result *  'a) list
  type record =
      [ `Success
      | `Fail
      | `Dispatch of (nnf * record) list
      | `Label of Types.label * (nnf * record) list * record ]
  type t = {
    nfv    : fv;
    ncatchv: fv;
    na     : Types.descr;
    nbasic : Types.descr nline;
    nprod  : (nnf * nnf) nline;
    nxml   : (nnf * nnf) nline;
    nrecord: record nline
  }

  val any_basic: Types.descr
  val normal: Types.descr -> node list -> t
end = 
struct
  type 'a sl = 'a SortedList.t
  type ('a,'b) sm = ('a,'b) SortedMap.t

  type source = 
      [ `Catch | `Const of Types.const 
      | `Left | `Right | `Recompose 
      | `Field of Types.label 
      ]
  type result = (capture, source) sm

  type 'a line = (result * 'a, Types.descr) sm
  type nf = {
    v     : fv;
    catchv: fv;  (* Variables catching the value *)
    a     : Types.descr;
    basic : unit line;
    prod  : (node sl * node sl) line;
    xml   : (node sl * node sl) line;
    record: ((Types.label, node sl) sm) line;

  }

  type nnf = node sl * Types.descr   (* pl,t;   t <= \accept{pl} *)
  type 'a nline = (result *  'a) sl
  type record =
      [ `Success
      | `Fail
      | `Dispatch of (nnf * record) list
      | `Label of Types.label * (nnf * record) list * record ]
  type t = {
    nfv    : fv;
    ncatchv: fv;
    na     : Types.descr;
    nbasic : Types.descr nline;
    nprod  : (nnf * nnf) nline;
    nxml   : (nnf * nnf) nline;
    nrecord: record nline
  }

  let nempty = { nfv = []; ncatchv = []; na = Types.empty;
		 nbasic = []; nprod = []; nxml = []; nrecord = [] }


  let ncup nf1 nf2 = 
    (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
    (* assert (nf1.nfv = nf2.nfv); *)
    { nfv = nf1.nfv;
      ncatchv = SortedList.cap nf1.ncatchv nf2.ncatchv;
      na      = Types.cup nf1.na nf2.na;
      nbasic  = SortedList.cup nf1.nbasic nf2.nbasic;
      nprod   = SortedList.cup nf1.nprod nf2.nprod;
      nxml    = SortedList.cup nf1.nxml nf2.nxml;
      nrecord = SortedList.cup nf1.nrecord nf2.nrecord;
    }

  let fus = SortedMap.union_disj
  let slcup = SortedList.cup

  let double_fold f l1 l2 =
    SortedList.from_list
      (List.fold_left 
	 (fun accu x1 ->
	    List.fold_left
	    (fun accu x2 ->
	       f accu x1 x2
	    )
	    accu l2
	 ) [] l1)
	 
  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, ((slcup pl1 pl2,t),(slcup 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
    { nfv = SortedList.cup nf1.nfv nf2.nfv;
      ncatchv = SortedList.cup nf1.ncatchv nf2.ncatchv;
      na = Types.cap nf1.na nf2.na;
      nbasic = double_fold basic nf1.nbasic nf2.nbasic;
      nprod = double_fold prod nf1.nprod nf2.nprod;
      nxml = double_fold prod nf1.nxml nf2.nxml;
      nrecord = []; (* TODO ... *)
    }

  let ntimes acc p q = 
    let src_p = List.map (fun v -> (v,`Left)) p.fv
    and src_q = List.map (fun v -> (v,`Right)) q.fv in
    let src = SortedMap.union (fun _ _ -> `Recompose) src_p src_q in 
    let rects = Types.Product.normal acc in
    let prod = List.map (fun (t1,t2) -> (src, (([p],t1),([q],t2)))) rects in
    { nempty with 
	nfv = SortedList.cup p.fv q.fv; 
	na = acc;
	nprod = SortedList.from_list prod
    }

    

  let empty = { v = []; catchv = []; 
		a = Types.empty; 
		basic = []; prod = []; xml = []; record = [] }
  let any_basic = Types.neg (List.fold_left Types.cup Types.empty
			       [Types.Product.any_xml;
				Types.Product.any;
				Types.Record.any])
  let restrict t nf =
    let rec filter = function
      | (key,acc) :: rem -> 
	  let acc = Types.cap t acc in
	  if Types.is_empty acc then filter rem else (key,acc) :: (filter rem)
      | [] -> []
    in
    {  v = nf.v;
       catchv = nf.catchv;
       a = Types.cap t nf.a;
       basic = filter nf.basic;
       prod = filter nf.prod;
       xml = filter nf.xml;
       record = filter nf.record;
    }


  let cap nf1 nf2 =
    let merge f lines1 lines2 =
      let m =
	List.fold_left 
	  (fun accu ((res1,x1),acc1) ->
	     List.fold_left
	     (fun accu ((res2,x2),acc2) ->
		let acc = Types.cap acc1 acc2 in
		if Types.is_empty acc then accu
		else ((fus res1 res2, f x1 x2),acc) :: accu
	     ) accu lines2
	  ) [] lines1 in
      SortedMap.from_list Types.cup m
    in
    let merge_basic () () = ()
    and merge_prod (p1,q1) (p2,q2) = slcup p1 p2, slcup q1 q2
    and merge_record r1 r2 = SortedMap.union slcup r1 r2 in
    { v = SortedList.cup nf1.v nf2.v;
      catchv = SortedList.cup nf1.catchv nf2.catchv;
      a = Types.cap nf1.a nf2.a;
      basic = merge merge_basic nf1.basic nf2.basic;
      prod = merge merge_prod nf1.prod nf2.prod;
      xml = merge merge_prod nf1.xml nf2.xml;
      record = merge merge_record nf1.record nf2.record;
    }


		  
  let cup acc1 nf1 nf2 =
    let nf2 = restrict (Types.neg acc1) nf2 in
    { v = nf1.v; (* = nf2.v *)
      catchv = SortedList.cap nf1.catchv nf2.catchv;
      a = Types.cup nf1.a nf2.a;
      basic = SortedMap.union Types.cup nf1.basic nf2.basic;
      prod  = SortedMap.union Types.cup nf1.prod nf2.prod;
      xml   = SortedMap.union Types.cup nf1.xml nf2.xml;
      record = SortedMap.union Types.cup nf1.record nf2.record;
    }

  let times acc p q = 
    let src_p = List.map (fun v -> (v,`Left)) p.fv
    and src_q = List.map (fun v -> (v,`Right)) q.fv in
    let src = SortedMap.union (fun _ _ -> `Recompose) src_p src_q in 
    { empty with 
	v = SortedList.cup p.fv q.fv; 
	a = acc;
	prod = [ (src, ([p], [q])), acc ] }

  let xml acc p q = 
    let src_p = List.map (fun v -> (v,`Left)) p.fv
    and src_q = List.map (fun v -> (v,`Right)) q.fv in
    let src = SortedMap.union (fun _ _ -> `Recompose) src_p src_q in 
    { empty with 
	v = SortedList.cup p.fv q.fv; 
	a = acc;
	xml = [ (src, ([p], [q])), acc ] }

  let record acc l p =
    let src = List.map (fun v -> (v, `Field l)) p.fv in
    { empty with
	v = p.fv;
	a = acc;
	record = [ (src, [l,[p]]), acc ] }

  let any =
    { v = []; 
      catchv = [];
      a = Types.any;
      basic = [ ([],()), any_basic ]; 
      prod  = [ ([],([],[])), Types.Product.any ];
      xml   = [ ([],([],[])), Types.Product.any_xml ];
      record = [ ([],[]), Types.Record.any ];
    }

  let capture x =
    let l = [x,`Catch] in
    { v = [x];
      catchv = [x];
      a = Types.any;
      basic = [ (l,()), any_basic ]; 
      prod  = [ (l,([],[])), Types.Product.any  ];
      xml  = [ (l,([],[])), Types.Product.any_xml  ];
      record = [ (l,[]), Types.Record.any ];
    }

  let constant x c =
    let l = [x,`Const c] in
    { v = [x];
      catchv = [];
      a = Types.any;
      basic = [ (l,()), any_basic ]; 
      prod  = [ (l,([],[])), Types.Product.any  ];
      xml   = [ (l,([],[])), Types.Product.any_xml  ];
      record = [ (l,[]), Types.Record.any ];
    }

  let constr t =
    { v = [];
      catchv = [];
      a = t;
      basic = [ ([],()), Types.cap t any_basic ];
      prod  = [ ([],([],[])), Types.cap t Types.Product.any ];
      xml   = [ ([],([],[])), Types.cap t Types.Product.any_xml ];
      record = [ ([],[]), Types.cap t Types.Record.any ];
    }

(* Put a pattern in normal form *)
  let rec nf (acc,fv,d) =
    if Types.is_empty acc 
    then empty
    else match d with
      | Constr t -> constr t
      | Cap (p,q) -> cap (nf p) (nf q)
      | Cup ((acc1,_,_) as p,q) -> cup acc1 (nf p) (nf q)
      | Times (p,q) -> times acc p q
      | Xml (p,q) -> xml acc p q
      | Capture x -> capture x
      | Constant (x,c) -> constant x c
      | Record (l,p) -> record acc l p

  let normal nf =
    let basic =
      List.map (fun ((res,()),acc) -> (res,acc)) 

    and prod ?kind l =
      let line accu (((res,(pl,ql)),acc)) =
	let aux accu (t1,t2) = (res,( (pl,t1), (ql,t2) ))::accu in
	let t = Types.Product.normal ?kind acc in
	List.fold_left aux accu t in
      List.fold_left line [] l
   

    and record =
      let rec aux nr fields = 
	match (nr,fields) with
	  | (`Success, []) -> `Success
	  | (`Fail,_) -> `Fail
	  | (`Success, (l2,pl)::fields) ->
	      `Label (l2, [(pl,Types.any), aux nr fields], `Fail)
	  | (`Label (l1, _, _), (l2,pl)::fields) when l2 < l1 ->
	      `Label (l2, [(pl,Types.any), aux nr fields], `Fail)
	  | (`Label (l1, pr, _), (l2,pl)::fields) when l1 = l2 ->
	      let pr = 
		List.map (fun (t,x) -> (((pl,t) : nnf), aux x fields)) pr in
	      `Label (l1, pr, `Fail)
	  | (`Label (l1, pr, ab),_) ->
	      let aux_ab = aux ab fields in
	      let pr = 
		List.map (fun (t,x) -> (([],t), 
(* Types.Record.normal enforce physical equility
   in case of a ? field *)
					if x==ab then aux_ab else
					aux x fields)) pr in
	      `Label (l1, pr, aux_ab)

(* TODO:!!!*)
	  | ((`NoField|`SomeField),_) -> aux `Success fields
      in

      let line accu ((res,fields),acc) =
	let nr = Types.Record.normal acc in
	let x = aux nr fields in
	match x with 
	  | `Fail -> accu 
	  | x -> (res,x) :: accu in
      List.fold_left line []
    in
    let nlines l = 
      List.map (fun (res,x) -> (SortedMap.diff res nf.catchv,x)) l in
    { nfv     = SortedList.diff nf.v nf.catchv; 
      ncatchv = nf.catchv;
      na      = nf.a;
      nbasic  = nlines (basic nf.basic);
      nprod   = nlines (prod nf.prod);
      nxml    = nlines (prod ~kind:`XML nf.xml);
      nrecord = nlines (record nf.record);
    }

  let normal t pl =
    normal (List.fold_left (fun a p -> cap a (nf (descr p))) (constr t) pl)

end


module Compile = 
struct
  type actions =
      [ `Ignore of result
      | `Kind of actions_kind ]
  and actions_kind = {
    basic: (Types.descr * result) list;
    prod: result dispatch dispatch;
    xml: result dispatch dispatch;
    record: record option;
  }
  and record = 
      [ `Label of Types.label * record dispatch * record option
      | `Result of result
      | `Absent ]
      
  and 'a dispatch =
      [ `Dispatch of dispatcher * 'a array
      | `TailCall of dispatcher
      | `Ignore of 'a
      | `None ]

  and result = int * source array
  and source = 
      [ `Catch | `Const of Types.const 
      | `Left of int | `Right of int | `Recompose of int * int
      | `Field of Types.label * int
      ]
      
  and return_code = 
      Types.descr * int *   (* accepted type, arity *)
      (int * (capture, int) SortedMap.t) list

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

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

  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
	| `None -> rs
	| `Ignore (`Ignore r) -> r :: rs
	| _ -> raise Exit in
      let rs = match xml with
	| `None -> rs
	| `Ignore (`Ignore r) -> r :: rs
	| _ -> raise Exit in
      let rs = match record with
	| None -> rs
	| Some (`Result r) -> r :: rs
	| _ -> raise Exit in
      match rs with
	| ((_, ret) as r) :: rs when 
	    List.for_all ( (=) r ) rs 
	    && array_for_all 
	      (function `Catch | `Const _ -> true | _ -> false) ret
	    -> `Ignore r
	| _ -> raise Exit
    )
    with Exit -> `Kind { basic = basic; prod = prod; xml = xml; record = record }

  let combine (disp,act) =
    if Array.length act = 0 then `None
    else
      if (array_for_all (fun (_,ar,_) -> ar = 0) disp.codes) 
	 && (array_for_all ( (=) act.(0) ) act) then
	   `Ignore act.(0)
      else
	`Dispatch (disp, act)

  let combine_record l present absent = 
    match (present,absent) with
      | (`Ignore r1, Some r2) when r1 = r2 -> r1
      | (`Ignore `Absent, Some r) -> r
      | (`Ignore r, None) -> r
      | _ -> `Label (l, present, absent)

  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 DispMap = Map.Make(
    struct
      type t = Types.descr * Normal.t array
      let compare = compare
    end
  )
    
  let dispatchers = ref DispMap.empty
		      
  let rec num i = function [] -> [] | h::t -> (h,i)::(num (i+1) t)

    
  let dispatcher t pl : 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 Types.is_empty t then `None
	else
	  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 v = SortedList.diff p.Normal.nfv p.Normal.ncatchv in
(*	    let tp = Types.normalize tp in *)
	    let accu' = (i,num arity v) :: accu in
	    `Switch 
	      (
	       aux (Types.cap t tp) (arity + (List.length v)) (i+1) accu',
	       aux (Types.diff t tp) arity (i+1) accu
	      )
      in
      let iface = aux t 0 0 [] in
      let res = { id = !cur_id; 
		  t = t;
		  pl = pl;
		  interface = iface;
		  codes = Array.of_list (List.rev !codes);
		  actions = None } 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 =
    Array.of_list (
      Array.fold_right
		     (fun x accu -> match x with
			| Some b -> b @ accu 
			| None -> accu)
		     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 (v,s) = match s with
    | (`Catch | `Const _) as x -> x
    | _ -> assert false

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

  let conv_source_prod left right (v,s) = match s with
    | (`Catch | `Const _) as x -> x
    | `Left -> `Left (assoc v left)
    | `Right -> `Right (assoc v right)
    | `Recompose -> `Recompose (assoc v left, assoc v right)
    | _ -> assert false

  let conv_source_record catch (v,s) = match s with
    | (`Catch | `Const _) as x -> x
    | `Field l -> `Field (l, try assoc v (List.assoc l catch) with Not_found -> -1)
    | _ -> assert false


  let dispatch_basic disp : (Types.descr * 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 -> List.iter (aux i)) pl;
      SortedMap.from_list SortedList.cup !accu in

    let t = Types.cap Normal.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 = List.map 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 unselect = Array.create (Array.length pl) [] in
    let aux i x = 
      let yes, no = f x in
      List.iter (fun ( (pl,ty), info) ->
		   let p = Normal.normal ty pl in
		   accu := (p,[i, p.Normal.ncatchv, info]) :: !accu;
		) yes;
      unselect.(i) <- no @ unselect.(i) in
    Array.iteri (fun i -> List.iter (aux i)) pl;

    let sorted = Array.of_list (SortedMap.from_list SortedList.cup !accu) in
    let infos = Array.map snd sorted in
    let disp = dispatcher t (Array.map fst sorted) in
    let result (t,_,m) =
      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 unselect
    in