(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
open Errors
open Names
open Term
open Context
open Declarations
open Util
open Nativevalues
open Nativelambda
open Pre_env

(** This file defines the mllambda code generation phase of the native
compiler. mllambda represents a fragment of ML, and can easily be printed
to OCaml code. *)

(** Local names {{{**)

type lname = { lname : name; luid : int }

let dummy_lname = { lname = Anonymous; luid = -1 }

module LNord = 
  struct 
    type t = lname 
    let compare l1 l2 = l1.luid - l2.luid
  end
module LNmap = Map.Make(LNord)
module LNset = Set.Make(LNord)

let lname_ctr = ref (-1)

let reset_lname = lname_ctr := -1

let fresh_lname n = 
  incr lname_ctr;
  { lname = n; luid = !lname_ctr }
  (**}}}**)

(** Global names {{{ **)
type gname = 
  | Gind of string * inductive (* prefix, inductive name *)
  | Gconstruct of string * constructor (* prefix, constructor name *)
  | Gconstant of string * constant (* prefix, constant name *)
  | Gcase of label option * int
  | Gpred of label option * int
  | Gfixtype of label option * int
  | Gnorm of label option * int
  | Gnormtbl of label option * int
  | Ginternal of string
  | Grel of int
  | Gnamed of identifier

let eq_gname gn1 gn2 =
  match gn1, gn2 with
  | Gind (s1, ind1), Gind (s2, ind2) -> String.equal s1 s2 && eq_ind ind1 ind2
  | Gconstruct (s1, c1), Gconstruct (s2, c2) ->
      String.equal s1 s2 && eq_constructor c1 c2
  | Gconstant (s1, c1), Gconstant (s2, c2) ->
      String.equal s1 s2 && Constant.equal c1 c2
  | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2
  | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2
  | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2
  | Gpred (Some l1, i1), Gpred (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2
  | Gfixtype (None, i1), Gfixtype (None, i2) -> Int.equal i1 i2
  | Gfixtype (Some l1, i1), Gfixtype (Some l2, i2) ->
      Int.equal i1 i2 && Label.equal l1 l2
  | Gnorm (None, i1), Gnorm (None, i2) -> Int.equal i1 i2
  | Gnorm (Some l1, i1), Gnorm (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2
  | Gnormtbl (None, i1), Gnormtbl (None, i2) -> Int.equal i1 i2
  | Gnormtbl (Some l1, i1), Gnormtbl (Some l2, i2) ->
      Int.equal i1 i2 && Label.equal l1 l2
  | Ginternal s1, Ginternal s2 -> String.equal s1 s2
  | Grel i1, Grel i2 -> Int.equal i1 i2
  | Gnamed id1, Gnamed id2 -> Id.equal id1 id2
  | _ -> false

let case_ctr = ref (-1)

let reset_gcase () = case_ctr := -1

let fresh_gcase l =
  incr case_ctr;
  Gcase (l,!case_ctr)

let pred_ctr = ref (-1)

let reset_gpred () = pred_ctr := -1

let fresh_gpred l = 
  incr pred_ctr;
  Gpred (l,!pred_ctr)

let fixtype_ctr = ref (-1)

let reset_gfixtype () = fixtype_ctr := -1

let fresh_gfixtype l =
  incr fixtype_ctr;
  Gfixtype (l,!fixtype_ctr)

let norm_ctr = ref (-1)

let reset_norm () = norm_ctr := -1

let fresh_gnorm l =
  incr norm_ctr;
  Gnorm (l,!norm_ctr)

let normtbl_ctr = ref (-1)

let reset_normtbl () = normtbl_ctr := -1

let fresh_gnormtbl l =
  incr normtbl_ctr;
  Gnormtbl (l,!normtbl_ctr)
  (**}}}**)

(** Symbols (pre-computed values) {{{**)

type symbol =
  | SymbValue of Nativevalues.t
  | SymbSort of sorts
  | SymbName of name
  | SymbConst of constant
  | SymbMatch of annot_sw
  | SymbInd of inductive

let dummy_symb = SymbValue (dummy_value ())

let eq_symbol sy1 sy2 =
  match sy1, sy2 with
  | SymbValue v1, SymbValue v2 -> Pervasives.(=) v1 v2 (** FIXME: how is this even valid? *)
  | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2
  | SymbName n1, SymbName n2 -> Name.equal n1 n2
  | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
  | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
  | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
  | _, _ -> false

open Hashset.Combine

let hash_symbol symb =
  match symb with
  | SymbValue v -> combinesmall 1 (Hashtbl.hash v)
  | SymbSort s -> combinesmall 2 (Sorts.hash s)
  | SymbName name -> combinesmall 3 (Name.hash name)
  | SymbConst c -> combinesmall 4 (Constant.hash c)
  | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
  | SymbInd ind -> combinesmall 6 (ind_hash ind)

module HashedTypeSymbol = struct
  type t = symbol
  let equal = eq_symbol
  let hash = hash_symbol
end

module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)

let symb_tbl = HashtblSymbol.create 211

let clear_symb_tbl () = HashtblSymbol.clear symb_tbl

let get_value tbl i =
  match tbl.(i) with
    | SymbValue v -> v
    | _ -> anomaly (Pp.str "get_value failed")

let get_sort tbl i =
  match tbl.(i) with
    | SymbSort s -> s
    | _ -> anomaly (Pp.str "get_sort failed")

let get_name tbl i =
  match tbl.(i) with
    | SymbName id -> id
    | _ -> anomaly (Pp.str "get_name failed")

let get_const tbl i =
  match tbl.(i) with
    | SymbConst kn -> kn
    | _ -> anomaly (Pp.str "get_const failed")

let get_match tbl i =
  match tbl.(i) with
    | SymbMatch case_info -> case_info
    | _ -> anomaly (Pp.str "get_match failed")

let get_ind tbl i =
  match tbl.(i) with
    | SymbInd ind -> ind
    | _ -> anomaly (Pp.str "get_ind failed")

let push_symbol x =
  try HashtblSymbol.find symb_tbl x
  with Not_found ->
    let i = HashtblSymbol.length symb_tbl in
    HashtblSymbol.add symb_tbl x i; i

let symbols_tbl_name = Ginternal "symbols_tbl"

let get_symbols_tbl () =
  let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
  HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl(**}}}**)

(** Lambda to Mllambda {{{**)
  
type primitive =
  | Mk_prod
  | Mk_sort
  | Mk_ind
  | Mk_const
  | Mk_sw
  | Mk_fix of rec_pos * int 
  | Mk_cofix of int
  | Mk_rel of int
  | Mk_var of identifier
  | Is_accu
  | Cast_accu
  | Upd_cofix
  | Force_cofix

let eq_primitive p1 p2 =
  match p1, p2 with
  | Mk_prod, Mk_prod -> true
  | Mk_sort, Mk_sort -> true
  | Mk_ind, Mk_ind -> true
  | Mk_const, Mk_const -> true
  | Mk_sw, Mk_sw -> true
  | Mk_fix (rp1, i1), Mk_fix (rp2, i2) -> Int.equal i1 i2 && eq_rec_pos rp1 rp2
  | Mk_cofix i1, Mk_cofix i2 -> Int.equal i1 i2
  | Mk_rel i1, Mk_rel i2 -> Int.equal i1 i2
  | Mk_var id1, Mk_var id2 -> Id.equal id1 id2
  | Is_accu, Is_accu -> true
  | Cast_accu, Cast_accu -> true
  | Upd_cofix, Upd_cofix -> true
  | Force_cofix, Force_cofix -> true
  | _ -> false

type mllambda =
  | MLlocal        of lname 
  | MLglobal       of gname 
  | MLprimitive    of primitive
  | MLlam          of lname array * mllambda 
  | MLletrec       of (lname * lname array * mllambda) array * mllambda
  | MLlet          of lname * mllambda * mllambda
  | MLapp          of mllambda * mllambda array
  | MLif           of mllambda * mllambda * mllambda
  | MLmatch        of annot_sw * mllambda * mllambda * mllam_branches
                              (* argument, prefix, accu branch, branches *)
  | MLconstruct    of string * constructor * mllambda array
                   (* prefix, constructor name, arguments *)
  | MLint          of bool * int   (* true if the type sould be int *)
  | MLsetref       of string * mllambda
  | MLsequence     of mllambda * mllambda

and mllam_branches = ((constructor * lname option array) list * mllambda) array

let push_lnames n env lns =
  snd (Array.fold_left (fun (i,r) x -> (i+1, LNmap.add x i r)) (n,env) lns)

let opush_lnames n env lns =
  let oadd x i r = match x with Some ln -> LNmap.add ln i r | None -> r in
  snd (Array.fold_left (fun (i,r) x -> (i+1, oadd x i r)) (n,env) lns)

(* Alpha-equivalence on mllambda *)
(* eq_mllambda gn1 gn2 n env1 env2 t1 t2 tests if t1 = t2 modulo gn1 = gn2 *)
let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
  match t1, t2 with
  | MLlocal ln1, MLlocal ln2 ->
      Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2)
  | MLglobal gn1', MLglobal gn2' ->
      eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2')
  | MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2
  | MLlam (lns1, ml1), MLlam (lns2, ml2) ->
      Int.equal (Array.length lns1) (Array.length lns2) &&
      let env1 = push_lnames n env1 lns1 in
      let env2 = push_lnames n env2 lns2 in
      eq_mllambda gn1 gn2 (n+Array.length lns1) env1 env2 ml1 ml2
  | MLletrec (defs1, body1), MLletrec (defs2, body2) ->
      Int.equal (Array.length defs1) (Array.length defs2) &&
      let lns1 = Array.map (fun (x,_,_) -> x) defs1 in
      let lns2 = Array.map (fun (x,_,_) -> x) defs2 in
      let env1 = push_lnames n env1 lns1 in
      let env2 = push_lnames n env2 lns2 in
      let n = n + Array.length defs1 in
      eq_letrec gn1 gn2 n env1 env2 defs1 defs2 &&
      eq_mllambda gn1 gn2 n env1 env2 body1 body2
  | MLlet (ln1, def1, body1), MLlet (ln2, def2, body2) ->
      eq_mllambda gn1 gn2 n env1 env2 def1 def2 &&
      let env1 = LNmap.add ln1 n env1 in
      let env2 = LNmap.add ln2 n env2 in
      eq_mllambda gn1 gn2 (n+1) env1 env2 body1 body2
  | MLapp (ml1, args1), MLapp (ml2, args2) ->
      eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 &&
      Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
  | MLif (cond1,br1,br'1), MLif (cond2,br2,br'2) ->
      eq_mllambda gn1 gn2 n env1 env2 cond1 cond2 &&
      eq_mllambda gn1 gn2 n env1 env2 br1 br2 &&
      eq_mllambda gn1 gn2 n env1 env2 br'1 br'2
  | MLmatch (annot1, c1, accu1, br1), MLmatch (annot2, c2, accu2, br2) ->
      eq_annot_sw annot1 annot2 &&
      eq_mllambda gn1 gn2 n env1 env2 c1 c2 &&
      eq_mllambda gn1 gn2 n env1 env2 accu1 accu2 &&
      eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
  | MLconstruct (pf1, cs1, args1), MLconstruct (pf2, cs2, args2) ->
      String.equal pf1 pf2 &&
      eq_constructor cs1 cs2 &&
      Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
  | MLint (ty1,v1), MLint (ty2,v2) ->
      ty1 == ty2 && Int.equal v1 v2
  | MLsetref (id1, ml1), MLsetref (id2, ml2) ->
      String.equal id1 id2 &&
      eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
   | MLsequence (ml1, ml'1), MLsequence (ml2, ml'2) ->
       eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 &&
       eq_mllambda gn1 gn2 n env1 env2 ml'1 ml'2
   | _, _ -> false

and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
  let eq_def (_,args1,ml1) (_,args2,ml2) =
    Int.equal (Array.length args1) (Array.length args2) &&
    let env1 = push_lnames n env1 args1 in
    let env2 = push_lnames n env2 args2 in
    eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 ml1 ml2
  in
  Array.equal eq_def defs1 defs2

(* we require here that patterns have the same order, which may be too strong *)
and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
  let eq_cargs (cs1, args1) (cs2, args2) body1 body2 =
    Int.equal (Array.length args1) (Array.length args2) &&
    eq_constructor cs1 cs2 &&
    let env1 = opush_lnames n env1 args1 in
    let env2 = opush_lnames n env2 args2 in
    eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 body1 body2
  in
  let eq_branch (ptl1,body1) (ptl2,body2) =
   List.equal (fun pt1 pt2 -> eq_cargs pt1 pt2 body1 body2) ptl1 ptl2
  in
  Array.equal eq_branch br1 br2

(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *)
let rec hash_mllambda gn n env t =
  match t with
  | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
  | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else Hashtbl.hash gn')
  | MLprimitive prim -> combinesmall 3 (Hashtbl.hash prim)
  | MLlam (lns, ml) ->
      let env = push_lnames n env lns in
      combinesmall 4 (combine (Array.length lns) (hash_mllambda gn (n+1) env ml))
  | MLletrec (defs, body) ->
      let lns = Array.map (fun (x,_,_) -> x) defs in
      let env = push_lnames n env lns in
      let n = n + Array.length defs in
      let h = combine (hash_mllambda gn n env body) (Array.length defs) in
      combinesmall 5 (hash_mllambda_letrec gn n env h defs)
  | MLlet (ln, def, body) ->
      let hdef = hash_mllambda gn n env def in
      let env = LNmap.add ln n env in
      combinesmall 6 (combine hdef (hash_mllambda gn (n+1) env body))
  | MLapp (ml, args) ->
      let h = hash_mllambda gn n env ml in
      combinesmall 7 (hash_mllambda_array gn n env h args)
  | MLif (cond,br,br') ->
      let hcond = hash_mllambda gn n env cond in
      let hbr = hash_mllambda gn n env br in
      let hbr' = hash_mllambda gn n env br' in
      combinesmall 8 (combine3 hcond hbr hbr')
  | MLmatch (annot, c, accu, br) ->
      let hannot = Hashtbl.hash annot in
      let hc = hash_mllambda gn n env c in
      let haccu = hash_mllambda gn n env accu in
      combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
  | MLconstruct (pf, cs, args) ->
      let hpf = Hashtbl.hash pf in
      let hcs = Hashtbl.hash cs in
      combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args)
  | MLint (ty,v) ->
      combinesmall 11 (combine (Hashtbl.hash ty) v)
  | MLsetref (id, ml) ->
      let hid = Hashtbl.hash id in
      let hml = hash_mllambda gn n env ml in
      combinesmall 12 (combine hid hml)
  | MLsequence (ml, ml') ->
      let hml = hash_mllambda gn n env ml in
      let hml' = hash_mllambda gn n env ml' in
      combinesmall 13 (combine hml hml')

and hash_mllambda_letrec gn n env init defs =
  let hash_def (_,args,ml) =
    let env = push_lnames n env args in
    let nargs = Array.length args in
    combine nargs (hash_mllambda gn (n + nargs) env ml)
  in
  Array.fold_left (fun acc t -> combine (hash_def t) acc) init defs

and hash_mllambda_array gn n env init arr =
  Array.fold_left (fun acc t -> combine (hash_mllambda gn n env t) acc) init arr

and hash_mllam_branches gn n env init br =
  let hash_cargs (cs, args) body =
    let nargs = Array.length args in
    let hcs = Hashtbl.hash cs in
    let env = opush_lnames n env args in
    let hbody = hash_mllambda gn (n + nargs) env body in
    combine3 nargs hcs hbody
  in
  let hash_branch acc (ptl,body) =
    List.fold_left (fun acc t -> combine (hash_cargs t body) acc) acc ptl
  in
  Array.fold_left hash_branch init br

let fv_lam l =
  let rec aux l bind fv =
    match l with
    | MLlocal l ->
	if LNset.mem l bind then fv else LNset.add l fv
    | MLglobal _ | MLprimitive _  | MLint _ -> fv
    | MLlam (ln,body) ->
	let bind = Array.fold_right LNset.add ln bind in
	aux body bind fv
    | MLletrec(bodies,def) ->
	let bind = 
	  Array.fold_right (fun (id,_,_) b -> LNset.add id b) bodies bind in
	let fv_body (_,ln,body) fv =
	  let bind = Array.fold_right LNset.add ln bind in
	  aux body bind fv in
	Array.fold_right fv_body bodies (aux def bind fv)
    | MLlet(l,def,body) ->
	aux body (LNset.add l bind) (aux def bind fv)
    | MLapp(f,args) ->
	let fv_arg arg fv = aux arg bind fv in
	Array.fold_right fv_arg args (aux f bind fv)
    | MLif(t,b1,b2) ->
	aux t bind (aux b1 bind (aux b2 bind fv))
    | MLmatch(_,a,p,bs) ->
      let fv = aux a bind (aux p bind fv) in
      let fv_bs (cargs, body) fv =
	let bind = 
	  List.fold_right (fun (_,args) bind ->
	    Array.fold_right 
	      (fun o bind -> match o with 
	      | Some l -> LNset.add l bind 
	      | _ -> bind) args bind) 
	    cargs bind in
	aux body bind fv in
      Array.fold_right fv_bs bs fv
          (* argument, accu branch, branches *)
    | MLconstruct (_,_,p) ->
	Array.fold_right (fun a fv -> aux a bind fv) p fv
    | MLsetref(_,l) -> aux l bind fv
    | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) in
  aux l LNset.empty LNset.empty


let mkMLlam params body =
  if Array.is_empty params then body 
  else
    match body with
    | MLlam (params', body) -> MLlam(Array.append params params', body)
    | _ -> MLlam(params,body)

let mkMLapp f args =
  if Array.is_empty args then f
  else
    match f with
    | MLapp(f,args') -> MLapp(f,Array.append args' args)
    | _ -> MLapp(f,args)

let empty_params = [||]

let decompose_MLlam c =
  match c with
  | MLlam(ids,c) -> ids,c
  | _ -> empty_params,c

(*s Global declaration *)
type global =
(*  | Gtblname of gname * identifier array *)
  | Gtblnorm of gname * lname array * mllambda array 
  | Gtblfixtype of gname * lname array * mllambda array
  | Glet of gname * mllambda
  | Gletcase of 
      gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
  | Gopen of string
  | Gtype of inductive * int array
    (* ind name, arities of constructors *)
  | Gcomment of string

(* Alpha-equivalence on globals *)
let eq_global g1 g2 =
  match g1, g2 with
  | Gtblnorm (gn1,lns1,mls1), Gtblnorm (gn2,lns2,mls2)
  | Gtblfixtype (gn1,lns1,mls1), Gtblfixtype (gn2,lns2,mls2) ->
      Int.equal (Array.length lns1) (Array.length lns2) &&
      Int.equal (Array.length mls1) (Array.length mls2) &&
      let env1 = push_lnames 0 LNmap.empty lns1 in
      let env2 = push_lnames 0 LNmap.empty lns2 in
      Array.for_all2 (eq_mllambda gn1 gn2 (Array.length lns1) env1 env2) mls1 mls2
  | Glet (gn1, def1), Glet (gn2, def2) ->
      eq_mllambda gn1 gn2 0 LNmap.empty LNmap.empty def1 def2
  | Gletcase (gn1,lns1,annot1,c1,accu1,br1),
      Gletcase (gn2,lns2,annot2,c2,accu2,br2) ->
      Int.equal (Array.length lns1) (Array.length lns2) &&
      let env1 = push_lnames 0 LNmap.empty lns1 in
      let env2 = push_lnames 0 LNmap.empty lns2 in
      let t1 = MLmatch (annot1,c1,accu1,br1) in
      let t2 = MLmatch (annot2,c2,accu2,br2) in
      eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
  | Gopen s1, Gopen s2 -> String.equal s1 s2
  | Gtype (ind1, arr1), Gtype (ind2, arr2) ->
      eq_ind ind1 ind2 && Array.equal Int.equal arr1 arr2
  | Gcomment s1, Gcomment s2 -> String.equal s1 s2
  | _, _ -> false

let hash_global g =
  match g with
  | Gtblnorm (gn,lns,mls) ->
      let nlns = Array.length lns in
      let nmls = Array.length mls in
      let env = push_lnames 0 LNmap.empty lns in
      let hmls = hash_mllambda_array gn nlns env (combine nlns nmls) mls in
      combinesmall 1 hmls
  | Gtblfixtype (gn,lns,mls) ->
      let nlns = Array.length lns in
      let nmls = Array.length mls in
      let env = push_lnames 0 LNmap.empty lns in
      let hmls = hash_mllambda_array gn nlns env (combine nlns nmls) mls in
      combinesmall 2 hmls
  | Glet (gn, def) ->
      combinesmall 3 (hash_mllambda gn 0 LNmap.empty def)
  | Gletcase (gn,lns,annot,c,accu,br) ->
      let nlns = Array.length lns in
      let env = push_lnames 0 LNmap.empty lns in
      let t = MLmatch (annot,c,accu,br) in
      combinesmall 4 (combine nlns (hash_mllambda gn nlns env t))
  | Gopen s -> combinesmall 5 (Hashtbl.hash s)
  | Gtype (ind, arr) ->
      combinesmall 6 (combine (Hashtbl.hash ind) (Hashtbl.hash arr))
  | Gcomment s -> combinesmall 7 (Hashtbl.hash s)
  
let global_stack = ref ([] : global list)

module HashedTypeGlobal = struct
  type t = global
  let equal = eq_global
  let hash = hash_global
end

module HashtblGlobal = Hashtbl.Make(HashedTypeGlobal)

let global_tbl = HashtblGlobal.create 19991

let clear_global_tbl () = HashtblGlobal.clear global_tbl

let push_global gn t =
  try HashtblGlobal.find global_tbl t
  with Not_found ->
    (global_stack := t :: !global_stack;
    HashtblGlobal.add global_tbl t gn; gn)

let push_global_let gn body =
  push_global gn (Glet (gn,body))

let push_global_fixtype gn params body =
  push_global gn (Gtblfixtype (gn,params,body))

let push_global_norm gn params body =
  push_global gn (Gtblnorm (gn, params, body))

let push_global_case gn params annot a accu bs =
  push_global gn (Gletcase (gn, params, annot, a, accu, bs))

(*s Compilation environment *)

type env =
    { env_rel : mllambda list; (* (MLlocal lname) list *)
      env_bound : int; (* length of env_rel *)
      (* free variables *)
      env_urel : (int * mllambda) list ref; (* list of unbound rel *)
      env_named : (identifier * mllambda) list ref }

let empty_env () =
  { env_rel = [];
    env_bound = 0;
    env_urel = ref [];
    env_named = ref []
  }

let push_rel env id = 
  let local = fresh_lname id in
  local, { env with 
	   env_rel = MLlocal local :: env.env_rel;
	   env_bound = env.env_bound + 1
	 }

let push_rels env ids =
  let lnames, env_rel = 
    Array.fold_left (fun (names,env_rel) id ->
      let local = fresh_lname id in
      (local::names, MLlocal local::env_rel)) ([],env.env_rel) ids in
  Array.of_list (List.rev lnames), { env with 
			  env_rel = env_rel;
			  env_bound = env.env_bound + Array.length ids
			}

let get_rel env id i =
  if i <= env.env_bound then
    List.nth env.env_rel (i-1)
  else 
    let i = i - env.env_bound in
    try Int.List.assoc i !(env.env_urel)
    with Not_found ->
      let local = MLlocal (fresh_lname id) in
      env.env_urel := (i,local) :: !(env.env_urel);
      local

let get_var env id =
  try Id.List.assoc id !(env.env_named)
  with Not_found ->
    let local = MLlocal (fresh_lname (Name id)) in
    env.env_named := (id, local)::!(env.env_named);
    local
   
(*s Traduction of lambda to mllambda *)

let get_prod_name codom = 
  match codom with
  | MLlam(ids,_) -> ids.(0).lname
  | _ -> assert false

let get_lname (_,l) = 
  match l with
  | MLlocal id -> id
  | _ -> invalid_arg "Nativecode.get_lname"

let fv_params env = 
  let fvn, fvr = !(env.env_named), !(env.env_urel) in 
  let size = List.length fvn + List.length fvr in
  if Int.equal size 0 then empty_params 
  else begin
    let params = Array.make size dummy_lname in
    let fvn = ref fvn in
    let i = ref 0 in
    while not (List.is_empty !fvn) do
      params.(!i) <- get_lname (List.hd !fvn);
      fvn := List.tl !fvn;
      incr i
    done;
    let fvr = ref fvr in
    while not (List.is_empty !fvr) do
      params.(!i) <- get_lname (List.hd !fvr);
      fvr := List.tl !fvr;
      incr i
    done;
    params
  end

let generalize_fv env body = 
  mkMLlam (fv_params env) body

let empty_args = [||]

let fv_args env fvn fvr =
  let size = List.length fvn + List.length fvr in
  if Int.equal size 0 then empty_args 
  else 
    begin
      let args = Array.make size (MLint (false,0)) in
      let fvn = ref fvn in
      let i = ref 0 in
      while not (List.is_empty !fvn) do
	args.(!i) <- get_var env (fst (List.hd !fvn));
	fvn := List.tl !fvn;
	incr i
      done;
      let fvr = ref fvr in
      while not (List.is_empty !fvr) do
	let (k,_ as kml) = List.hd !fvr in
	let n = get_lname kml in 
	args.(!i) <- get_rel env n.lname k;
	fvr := List.tl !fvr;
	incr i
      done;
      args
    end

let get_value_code i =
  MLapp (MLglobal (Ginternal "get_value"), [|MLglobal symbols_tbl_name;MLint(true,i)|])

let get_sort_code i =
  MLapp (MLglobal (Ginternal "get_sort"), [|MLglobal symbols_tbl_name;MLint(true,i)|])

let get_name_code i =
  MLapp (MLglobal (Ginternal "get_name"), [|MLglobal symbols_tbl_name;MLint(true,i)|])

let get_const_code i =
  MLapp (MLglobal (Ginternal "get_const"), [|MLglobal symbols_tbl_name;MLint(true,i)|])

let get_match_code i =
  MLapp (MLglobal (Ginternal "get_match"), [|MLglobal symbols_tbl_name;MLint(true,i)|])

let get_ind_code i =
  MLapp (MLglobal (Ginternal "get_ind"), [|MLglobal symbols_tbl_name;MLint(true,i)|])

type rlist =
  | Rnil 
  | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' 
and rlist' = rlist ref

let rm_params fv params = 
  Array.map (fun l -> if LNset.mem l fv then Some l else None) params 

let rec insert cargs body rl =
 match !rl with
 | Rnil ->
     let fv = fv_lam body in
     let (c,params) = cargs in
     let params = rm_params fv params in
     rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
 | Rcons(l,fv,body',rl) ->
     if Pervasives.(=) body body' then (** FIXME *)
       let (c,params) = cargs in
       let params = rm_params fv params in
       l := (c,params)::!l
     else insert cargs body rl

let rec to_list rl =
  match !rl with
  | Rnil -> []
  | Rcons(l,_,body,tl) -> (!l,body)::to_list tl

let merge_branches t =
  let newt = ref Rnil in
  Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
  Array.of_list (to_list newt)

 let rec ml_of_lam env l t =
  match t with
  | Lrel(id ,i) -> get_rel env id i
  | Lvar id -> get_var env id
  | Lprod(dom,codom) ->
      let dom = ml_of_lam env l dom in
      let codom = ml_of_lam env l codom in
      let n = get_prod_name codom in
      let i = push_symbol (SymbName n) in
      MLapp(MLprimitive Mk_prod, [|get_name_code i;dom;codom|])
  | Llam(ids,body) ->
    let lnames,env = push_rels env ids in
    MLlam(lnames, ml_of_lam env l body)
  | Llet(id,def,body) ->
      let def = ml_of_lam env l def in
      let lname, env = push_rel env id in
      let body = ml_of_lam env l body in
      MLlet(lname,def,body)
  | Lapp(f,args) ->
      MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args)
  | Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c))
  | Lcase (annot,p,a,bs) ->
      (* let predicate_uid fv_pred = compilation of p 
         let rec case_uid fv a_uid = 
           match a_uid with
           | Accu _ => mk_sw (predicate_uid fv_pred) (case_uid fv) a_uid
           | Ci argsi => compilation of branches 
         compile case = case_uid fv (compilation of a) *)
      (* Compilation of the predicate *)
         (* Remark: if we do not want to compile the predicate we 
            should a least compute the fv, then store the lambda representation
            of the predicate (not the mllambda) *)
      let env_p = empty_env () in
      let pn = fresh_gpred l in
      let mlp = ml_of_lam env_p l p in
      let mlp = generalize_fv env_p mlp in
      let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in
      let pn = push_global_let pn mlp in
      (* Compilation of the case *)
      let env_c = empty_env () in
      let a_uid = fresh_lname Anonymous in
      let la_uid = MLlocal a_uid in
      (* compilation of branches *)
      let ml_br (c,params, body) = 
	let lnames, env = push_rels env_c params in
	(c, lnames, ml_of_lam env l body) in
      let bs = Array.map ml_br bs in
      let cn = fresh_gcase l in
      (* Compilation of accu branch *)
      let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in  
      let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in
      let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in
         (* remark : the call to fv_args does not add free variables in env_c *)
      let i = push_symbol (SymbMatch annot) in
      let accu =
	MLapp(MLprimitive Mk_sw,
	      [| get_match_code i; MLapp (MLprimitive Cast_accu, [|la_uid|]);
		 pred;
		 cn_fv |]) in
(*      let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
      let case = generalize_fv env_c body in *)
      let cn = push_global_case cn (Array.append (fv_params env_c) [|a_uid|])
        annot la_uid accu (merge_branches bs)
      in
      (* Final result *)
      let arg = ml_of_lam env l a in
      let force =
	if annot.asw_finite then arg
	else MLapp(MLprimitive Force_cofix, [|arg|]) in
      mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
  | Lif(t,bt,bf) -> 
      MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
  | Lfix ((rec_pos,start), (ids, tt, tb)) ->
      (* let type_f fvt = [| type fix |] 
         let norm_f1 fv f1 .. fn params1 = body1
	 ..
         let norm_fn fv f1 .. fn paramsn = bodyn
         let norm fv f1 .. fn = 
	    [|norm_f1 fv f1 .. fn; ..; norm_fn fv f1 .. fn|]
         compile fix = 
	   let rec f1 params1 = 
             if is_accu rec_pos.(1) then mk_fix (type_f fvt) (norm fv) params1
	     else norm_f1 fv f1 .. fn params1
           and .. and fn paramsn = 
	     if is_accu rec_pos.(n) then mk_fix (type_f fvt) (norm fv) paramsn
             else norm_fn fv f1 .. fv paramsn in
	   start
      *)
      (* Compilation of type *)
      let env_t = empty_env () in
      let ml_t = Array.map (ml_of_lam env_t l) tt in
      let params_t = fv_params env_t in
      let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
      let gft = fresh_gfixtype l in
      let gft = push_global_fixtype gft params_t ml_t in
      let mk_type = MLapp(MLglobal gft, args_t) in
      (* Compilation of norm_i *)
      let ndef = Array.length ids in
      let lf,env_n = push_rels (empty_env ()) ids in
      let t_params = Array.make ndef [||] in
      let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
      let mk_let envi (id,def) t = MLlet (id,def,t) in
      let mk_lam_or_let (params,lets,env) (id,def) =
        let ln,env' = push_rel env id in
        match def with
        | None -> (ln::params,lets,env')
        | Some lam -> (params, (ln,ml_of_lam env l lam)::lets,env')
      in
      let ml_of_fix i body =
        let varsi, bodyi = decompose_Llam_Llet body in
        let paramsi,letsi,envi = 
          Array.fold_left mk_lam_or_let ([],[],env_n) varsi
        in
        let paramsi,letsi =
          Array.of_list (List.rev paramsi), Array.of_list (List.rev letsi)
        in
        t_norm_f.(i) <- fresh_gnorm l;
        let bodyi = ml_of_lam envi l bodyi in
        t_params.(i) <- paramsi;
        let bodyi = Array.fold_right (mk_let envi) letsi bodyi in
        mkMLlam paramsi bodyi
      in
      let tnorm = Array.mapi ml_of_fix tb in
      let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in
      let fv_params = fv_params env_n in
      let fv_args' = Array.map (fun id -> MLlocal id) fv_params in
      let norm_params = Array.append fv_params lf in
      let t_norm_f = Array.mapi (fun i body ->
	push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in
      let norm = fresh_gnormtbl l in
      let norm = push_global_norm norm fv_params 
         (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in
      (* Compilation of fix *)
      let fv_args = fv_args env fvn fvr in      
      let lf, env = push_rels env ids in
      let lf_args = Array.map (fun id -> MLlocal id) lf in
      let mk_norm = MLapp(MLglobal norm, fv_args) in
      let mkrec i lname = 
	let paramsi = t_params.(i) in
	let reci = MLlocal (paramsi.(rec_pos.(i))) in
	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
	let body = 
	  MLif(MLapp(MLprimitive Is_accu,[|reci|]),
	       mkMLapp 
		 (MLapp(MLprimitive (Mk_fix(rec_pos,i)), 
			[|mk_type; mk_norm|]))
		 pargsi,
	       MLapp(MLglobal t_norm_f.(i), 
		     Array.concat [fv_args;lf_args;pargsi])) 
	in
	(lname, paramsi, body) in
      MLletrec(Array.mapi mkrec lf, lf_args.(start))
  | Lcofix (start, (ids, tt, tb)) -> 
      (* Compilation of type *)
      let env_t = empty_env () in
      let ml_t = Array.map (ml_of_lam env_t l) tt in
      let params_t = fv_params env_t in
      let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
      let gft = fresh_gfixtype l in
      let gft = push_global_fixtype gft params_t ml_t in
      let mk_type = MLapp(MLglobal gft, args_t) in
      (* Compilation of norm_i *) 
      let ndef = Array.length ids in
      let lf,env_n = push_rels (empty_env ()) ids in
      let t_params = Array.make ndef [||] in
      let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
      let ml_of_fix i body =
        let idsi,bodyi = decompose_Llam body in
        let paramsi, envi = push_rels env_n idsi in
        t_norm_f.(i) <- fresh_gnorm l;
        let bodyi = ml_of_lam envi l bodyi in
        t_params.(i) <- paramsi;
        mkMLlam paramsi bodyi in
      let tnorm = Array.mapi ml_of_fix tb in
      let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in
      let fv_params = fv_params env_n in
      let fv_args' = Array.map (fun id -> MLlocal id) fv_params in
      let norm_params = Array.append fv_params lf in
      let t_norm_f = Array.mapi (fun i body ->
	push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in
      let norm = fresh_gnormtbl l in
      let norm = push_global_norm norm fv_params
        (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in
      (* Compilation of fix *)
      let fv_args = fv_args env fvn fvr in      
      let mk_norm = MLapp(MLglobal norm, fv_args) in
      let lnorm = fresh_lname Anonymous in
      let ltype = fresh_lname Anonymous in
      let lf, env = push_rels env ids in
      let lf_args = Array.map (fun id -> MLlocal id) lf in
      let upd i lname cont =
	let paramsi = t_params.(i) in
	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
	let uniti = fresh_lname Anonymous in
	let body =
	  MLlam(Array.append paramsi [|uniti|],
		MLapp(MLglobal t_norm_f.(i),
		      Array.concat [fv_args;lf_args;pargsi])) in
	MLsequence(MLapp(MLprimitive Upd_cofix, [|lf_args.(i);body|]),
		   cont) in
      let upd = Array.fold_right_i upd lf lf_args.(start) in
      let mk_let i lname cont =
	MLlet(lname,
	      MLapp(MLprimitive(Mk_cofix i),[| MLlocal ltype; MLlocal lnorm|]),
	      cont) in
      let init = Array.fold_right_i mk_let lf upd in 
      MLlet(lnorm, mk_norm, MLlet(ltype, mk_type, init))
  (*    	    
      let mkrec i lname = 
	let paramsi = t_params.(i) in
	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
	let uniti = fresh_lname Anonymous in
	let body = 
	  MLapp( MLprimitive(Mk_cofix i),
		 [|mk_type;mk_norm; 
		   MLlam([|uniti|],
			 MLapp(MLglobal t_norm_f.(i),
			       Array.concat [fv_args;lf_args;pargsi]))|]) in
	(lname, paramsi, body) in
      MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
   
  | Lmakeblock (prefix,cn,_,args) ->
      MLconstruct(prefix,cn,Array.map (ml_of_lam env l) args)
  | Lconstruct (prefix, cn) ->
      MLglobal (Gconstruct (prefix, cn))
  | Lval v ->
      let i = push_symbol (SymbValue v) in get_value_code i
  | Lsort s ->
    let i = push_symbol (SymbSort s) in
    MLapp(MLprimitive Mk_sort, [|get_sort_code i|])
  | Lind (prefix, ind) -> MLglobal (Gind (prefix, ind))
  | Llazy -> MLglobal (Ginternal "lazy")
  | Lforce -> MLglobal (Ginternal "Lazy.force")

let mllambda_of_lambda auxdefs l t =
  let env = empty_env () in
  global_stack := auxdefs;
  let ml = ml_of_lam env l t in
  let fv_rel = !(env.env_urel) in
  let fv_named = !(env.env_named) in
  (* build the free variables *)
  let get_lname (_,t) = 
   match t with
   | MLlocal x -> x
   | _ -> assert false in
  let params = 
    List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in
  if List.is_empty params then
    (!global_stack, ([],[]), ml)
  (* final result : global list, fv, ml *)
  else
    (!global_stack, (fv_named, fv_rel), mkMLlam (Array.of_list params) ml)
    (**}}}**)

(** Code optimization {{{**)

(** Optimization of match and fix *)

let can_subst l = 
  match l with
  | MLlocal _ | MLint _ | MLglobal _ -> true
  | _ -> false

let subst s l =
  if LNmap.is_empty s then l 
  else
    let rec aux l =
      match l with
      | MLlocal id -> (try LNmap.find id s with Not_found -> l)
      | MLglobal _ | MLprimitive _ | MLint _ -> l
      | MLlam(params,body) -> MLlam(params, aux body)
      | MLletrec(defs,body) ->
	let arec (f,params,body) = (f,params,aux body) in
	MLletrec(Array.map arec defs, aux body)
      | MLlet(id,def,body) -> MLlet(id,aux def, aux body)
      | MLapp(f,args) -> MLapp(aux f, Array.map aux args)
      | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2)
      | MLmatch(annot,a,accu,bs) ->
	  let auxb (cargs,body) = (cargs,aux body) in
	  MLmatch(annot,a,aux accu, Array.map auxb bs)
      | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args)
      | MLsetref(s,l1) -> MLsetref(s,aux l1) 
      | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
    in
    aux l

let add_subst id v s =
  match v with
  | MLlocal id' when Int.equal id.luid id'.luid -> s
  | _ -> LNmap.add id v s

let subst_norm params args s =
  let len = Array.length params in
  assert (Int.equal (Array.length args) len && Array.for_all can_subst args);
  let s = ref s in
  for i = 0 to len - 1 do
    s := add_subst params.(i) args.(i) !s
  done;
  !s

let subst_case params args s =
  let len = Array.length params in
  assert (len > 0 && 
	  Int.equal (Array.length args) len && 
	  let r = ref true and i = ref 0 in
	  (* we test all arguments excepted the last *)
	  while !i < len - 1  && !r do r := can_subst args.(!i); incr i done;
	  !r);
  let s = ref s in
  for i = 0 to len - 2 do
    s := add_subst params.(i) args.(i) !s
  done;
  !s, params.(len-1), args.(len-1)
    
let empty_gdef = Int.Map.empty, Int.Map.empty
let get_norm (gnorm, _) i = Int.Map.find i gnorm
let get_case (_, gcase) i = Int.Map.find i gcase

let all_lam n bs = 
  let f (_, l) = 
    match l with
    | MLlam(params, _) -> Int.equal (Array.length params) n
    | _ -> false in
  Array.for_all f bs

let commutative_cut annot a accu bs args =
  let mkb (c,b) =
     match b with
     | MLlam(params, body) -> 
         (c, Array.fold_left2 (fun body x v -> MLlet(x,v,body)) body params args)
     | _ -> assert false in
  MLmatch(annot, a, mkMLapp accu args, Array.map mkb bs)

let optimize gdef l =   
  let rec optimize s l =
    match l with
    | MLlocal id -> (try LNmap.find id s with Not_found -> l)
    | MLglobal _ | MLprimitive _ | MLint _ -> l
    | MLlam(params,body) -> 
	MLlam(params, optimize s body)
    | MLletrec(decls,body) ->
	let opt_rec (f,params,body) = (f,params,optimize s body ) in 
	MLletrec(Array.map opt_rec decls, optimize s body)
    | MLlet(id,def,body) ->
	let def = optimize s def in
	if can_subst def then optimize (add_subst id def s) body 
	else MLlet(id,def,optimize s body)
    | MLapp(f, args) ->
	let args = Array.map (optimize s) args in
	begin match f with
	| MLglobal (Gnorm (_,i)) ->
	    (try
	      let params,body = get_norm gdef i in
	      let s = subst_norm params args s in
	      optimize s body	    
	    with Not_found -> MLapp(optimize s f, args))
	| MLglobal (Gcase (_,i)) ->
	    (try 
	      let params,body = get_case gdef i in
	      let s, id, arg = subst_case params args s in
	      if can_subst arg then optimize (add_subst id arg s) body
	      else MLlet(id, arg, optimize s body)
	    with Not_found ->  MLapp(optimize s f, args))
	| _ -> 
            let f = optimize s f in
            match f with
            | MLmatch (annot,a,accu,bs) ->
              if all_lam (Array.length args) bs then  
                commutative_cut annot a accu bs args 
              else MLapp(f, args)
            | _ -> MLapp(f, args)

	end
    | MLif(t,b1,b2) ->
	let t = optimize s t in
	let b1 = optimize s b1 in
	let b2 = optimize s b2 in
	begin match t, b2 with
	| MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
	    when Pervasives.(=) l1 l2 -> MLmatch(annot, l1, b1, bs) (** FIXME *)
        | _, _ -> MLif(t, b1, b2)
	end
    | MLmatch(annot,a,accu,bs) ->
	let opt_b (cargs,body) = (cargs,optimize s body) in
	MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
    | MLconstruct(prefix,c,args) ->
        MLconstruct(prefix,c,Array.map (optimize s) args)
    | MLsetref(r,l) -> MLsetref(r, optimize s l) 
    | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2)
  in
  optimize LNmap.empty l

let optimize_stk stk =
  let add_global gdef g =
    match g with
    | Glet (Gnorm (_,i), body) ->
	let (gnorm, gcase) = gdef in
	(Int.Map.add i (decompose_MLlam body) gnorm, gcase)
    | Gletcase(Gcase (_,i), params, annot,a,accu,bs) ->
	let (gnorm,gcase) = gdef in
	(gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase)
    | Gletcase _ -> assert false
    | _ -> gdef in
  let gdef = List.fold_left add_global empty_gdef stk in
  let optimize_global g = 
    match g with
    | Glet(Gconstant (prefix, c), body) ->
        Glet(Gconstant (prefix, c), optimize gdef body)
    | _ -> g in
  List.map optimize_global stk
  (**}}}**)

(** Printing to ocaml {{{**)
(* Redefine a bunch of functions in module Names to generate names
   acceptable to OCaml. *)
let string_of_id s = Unicode.ascii_of_ident (string_of_id s)
let string_of_label l = Unicode.ascii_of_ident (string_of_label l)

let string_of_dirpath = function
  | [] -> "_"
  | sl -> String.concat "_" (List.rev_map string_of_id sl)

(* The first letter of the file name has to be a capital to be accepted by *)
(* OCaml as a module identifier.                                           *)
let string_of_dirpath s = "N"^string_of_dirpath s

let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir)

let string_of_name x =
  match x with
    | Anonymous -> "anonymous" (* assert false *)
    | Name id -> string_of_id id

let string_of_label_def l =
  match l with
    | None -> ""
    | Some l -> string_of_label l

(* Relativization of module paths *)
let rec list_of_mp acc = function
  | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp
  | MPfile dp ->
      let dp = repr_dirpath dp in
      string_of_dirpath dp :: acc
  | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc

let list_of_mp mp = list_of_mp [] mp

let string_of_kn kn =
  let (mp,dp,l) = repr_kn kn in
  let mp = list_of_mp mp in
  String.concat "_" mp ^ "_" ^ string_of_label l

let string_of_con c = string_of_kn (user_con c)
let string_of_mind mind = string_of_kn (user_mind mind)

let string_of_gname g =
  match g with
  | Gind (prefix, (mind, i)) ->
      Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
  | Gconstruct (prefix, ((mind, i), j)) ->
      Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
  | Gconstant (prefix, c) ->
      Format.sprintf "%sconst_%s" prefix (string_of_con c)
  | Gcase (l,i) ->
      Format.sprintf "case_%s_%i" (string_of_label_def l) i
  | Gpred (l,i) ->
      Format.sprintf "pred_%s_%i" (string_of_label_def l) i
  | Gfixtype (l,i) ->
      Format.sprintf "fixtype_%s_%i" (string_of_label_def l) i
  | Gnorm (l,i) ->
      Format.sprintf "norm_%s_%i" (string_of_label_def l) i
  | Ginternal s -> Format.sprintf "%s" s
  | Gnormtbl (l,i) -> 
      Format.sprintf "normtbl_%s_%i" (string_of_label_def l) i
  | Grel i ->
      Format.sprintf "rel_%i" i
  | Gnamed id ->
      Format.sprintf "named_%s" (string_of_id id)

let pp_gname fmt g =
  Format.fprintf fmt "%s" (string_of_gname g)

let pp_lname fmt ln =
  let s = Unicode.ascii_of_ident (string_of_name ln.lname) in
  Format.fprintf fmt "x_%s_%i" s ln.luid

let pp_ldecls fmt ids =
  let len = Array.length ids in
  for i = 0 to len - 1 do
    Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i)
  done

let string_of_construct prefix ((mind,i),j) =
  let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in
  prefix ^ id
   
let pp_int fmt i =
  if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i

let pp_mllam fmt l =

  let rec pp_mllam fmt l =
    match l with
    | MLlocal ln -> Format.fprintf fmt "@[%a@]" pp_lname ln
    | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g
    | MLprimitive p -> Format.fprintf fmt "@[%a@]" pp_primitive p
    | MLlam(ids,body) ->
	Format.fprintf fmt "@[(fun%a@ ->@\n %a)@]"
	  pp_ldecls ids pp_mllam body
    | MLletrec(defs, body) ->
	Format.fprintf fmt "@[%a@ in@\n%a@]" pp_letrec defs 
	  pp_mllam body
    | MLlet(id,def,body) ->
	Format.fprintf fmt "@[(let@ %a@ =@\n %a@ in@\n%a)@]"
          pp_lname id pp_mllam def pp_mllam body
    | MLapp(f, args) ->
	Format.fprintf fmt "@[%a@ %a@]" pp_mllam f (pp_args true) args
    | MLif(t,l1,l2) ->
	Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
	  pp_mllam t pp_mllam l1 pp_mllam l2 
    | MLmatch (asw, c, accu_br, br) ->
	let mind,i = asw.asw_ind in
    let prefix = asw.asw_prefix in
	let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
	Format.fprintf fmt 
	  "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
	  pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br
	  
    | MLconstruct(prefix,c,args) ->
        Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" 
          (string_of_construct prefix c) pp_cargs args
    | MLint(int, i) ->
	if int then pp_int fmt i
	else Format.fprintf fmt "(val_of_int %a)" pp_int i
    | MLsetref (s, body) ->
	Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
    | MLsequence(l1,l2) ->
	Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2

  and pp_letrec fmt defs =
    let len = Array.length defs in
    let pp_one_rec i (fn, argsn, body) =
      Format.fprintf fmt "%a%a =@\n  %a"
	pp_lname fn 
	pp_ldecls argsn pp_mllam body in
    Format.fprintf fmt "@[let rec ";
    pp_one_rec 0 defs.(0);
    for i = 1 to len - 1 do
      Format.fprintf fmt "@\nand ";
      pp_one_rec i defs.(i)
    done;

  and pp_blam fmt l =
    match l with
    | MLprimitive (Mk_prod | Mk_sort) 
    | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
	Format.fprintf fmt "(%a)" pp_mllam l
    | MLconstruct(_,_,args) when Array.length args > 0 ->
	Format.fprintf fmt "(%a)" pp_mllam l
    | _ -> pp_mllam fmt l

  and pp_args sep fmt args =
    let sep = if sep then " " else "," in
    let len = Array.length args in
    if len > 0 then begin
      Format.fprintf fmt "%a" pp_blam args.(0);
      for i = 1 to len - 1 do
	Format.fprintf fmt "%s%a" sep pp_blam args.(i)
      done
    end 

  and pp_cargs fmt args =
    let len = Array.length args in
    match len with
    | 0 -> ()
    | 1 -> Format.fprintf fmt " %a" pp_blam args.(0)
    | _ -> Format.fprintf fmt "(%a)" (pp_args false) args

  and pp_cparam fmt param = 
    match param with
    | Some l -> pp_mllam fmt (MLlocal l)
    | None -> Format.fprintf fmt "_"

  and pp_cparams fmt params =
    let len = Array.length params in
    match len with
    | 0 -> ()
    | 1 -> Format.fprintf fmt " %a" pp_cparam params.(0)
    | _ -> 
	let aux fmt params =
	  Format.fprintf fmt "%a" pp_cparam params.(0);
	  for i = 1 to len - 1 do
	    Format.fprintf fmt ",%a" pp_cparam params.(i)
	  done in 
	Format.fprintf fmt "(%a)" aux params

  and pp_branches prefix fmt bs =
    let pp_branch (cargs,body) =
      let pp_c fmt (cn,args) = 
        Format.fprintf fmt "| %s%a " 
      (string_of_construct prefix cn) pp_cparams args in
      let rec pp_cargs fmt cargs =
        match cargs with
    | [] -> ()
    | cargs::cargs' -> 
        Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in
      Format.fprintf fmt "%a ->@\n  %a@\n" 
    pp_cargs cargs pp_mllam body
      in
    Array.iter pp_branch bs

  and pp_primitive fmt = function
    | Mk_prod -> Format.fprintf fmt "mk_prod_accu" 
    | Mk_sort -> Format.fprintf fmt "mk_sort_accu"
    | Mk_ind -> Format.fprintf fmt "mk_ind_accu"
    | Mk_const -> Format.fprintf fmt "mk_constant_accu"
    | Mk_sw -> Format.fprintf fmt "mk_sw_accu"
    | Mk_fix(rec_pos,start) -> 
	let pp_rec_pos fmt rec_pos = 
	  Format.fprintf fmt "@[[| %i" rec_pos.(0);
	  for i = 1 to Array.length rec_pos - 1 do
	    Format.fprintf fmt "; %i" rec_pos.(i) 
	  done;
	  Format.fprintf fmt " |]@]" in
	Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start
    | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start
    | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i
    | Mk_var id ->
        Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id)
    | Is_accu -> Format.fprintf fmt "is_accu"
    | Cast_accu -> Format.fprintf fmt "cast_accu"
    | Upd_cofix -> Format.fprintf fmt "upd_cofix"
    | Force_cofix -> Format.fprintf fmt "force_cofix"
  in
  Format.fprintf fmt "@[%a@]" pp_mllam l
  
let pp_array fmt t =
  let len = Array.length t in
  Format.fprintf fmt "@[[|";
  for i = 0 to len - 2 do
    Format.fprintf fmt "%a; " pp_mllam t.(i)
  done;
  if len > 0 then
    Format.fprintf fmt "%a" pp_mllam t.(len - 1);
  Format.fprintf fmt "|]@]"
  
let pp_global fmt g =
  match g with
  | Glet (gn, c) ->
      let ids, c = decompose_MLlam c in
      Format.fprintf fmt "@[let %a%a =@\n  %a@]@\n@." pp_gname gn 
	pp_ldecls ids
	pp_mllam c
  | Gopen s ->
      Format.fprintf fmt "@[open %s@]@." s
  | Gtype ((mind, i), lar) ->
      let l = string_of_mind mind in
      let rec aux s ar = 
	if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
      let pp_const_sig i fmt j ar =
        let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
        Format.fprintf fmt "  | Construct_%s_%i_%i %s@\n" l i j sig_str
      in
      let pp_const_sigs i fmt lar =
        Format.fprintf fmt "  | Accu_%s_%i of Nativevalues.t@\n" l i;
        Array.iteri (pp_const_sig i fmt) lar
      in
      Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar
  | Gtblfixtype (g, params, t) ->
      Format.fprintf fmt "@[let %a %a =@\n  %a@]@\n@." pp_gname g
	pp_ldecls params pp_array t
  | Gtblnorm (g, params, t) ->
      Format.fprintf fmt "@[let %a %a =@\n  %a@]@\n@." pp_gname g
	pp_ldecls params pp_array t 
  | Gletcase(gn,params,annot,a,accu,bs) ->
      Format.fprintf fmt "@[(* Hash = %i *)@\nlet rec %a %a =@\n  %a@]@\n@."
      (hash_global g)
	pp_gname gn pp_ldecls params 
	pp_mllam (MLmatch(annot,a,accu,bs))
  | Gcomment s ->
      Format.fprintf fmt "@[(* %s *)@]@." s(**}}}**)

(** Compilation of elements in environment {{{**)
let rec compile_with_fv env auxdefs l t =
  let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
  if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
  else apply_fv env (fv_named,fv_rel) auxdefs ml

and apply_fv env (fv_named,fv_rel) auxdefs ml =
  let get_rel_val (n,_) auxdefs =
    (*
    match !(lookup_rel_native_val n env) with
    | NVKnone ->
    *)
        compile_rel env auxdefs n
(*    | NVKvalue (v,d) -> assert false *)
  in
  let get_named_val (id,_) auxdefs =
    (*
    match !(lookup_named_native_val id env) with
    | NVKnone ->
        *)
        compile_named env auxdefs id
(*    | NVKvalue (v,d) -> assert false *)
  in
  let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
  let auxdefs = List.fold_right get_named_val fv_named auxdefs in
  let lvl = rel_context_length env.env_rel_context in
  let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
  let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
  let aux_name = fresh_lname Anonymous in
  auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))

and compile_rel env auxdefs n =
  let (_,body,_) = lookup_rel n env.env_rel_context in
  let n = rel_context_length env.env_rel_context - n in
  match body with
  | Some t ->
      let code = lambda_of_constr env t in
      let auxdefs,code = compile_with_fv env auxdefs None code in
      Glet(Grel n, code)::auxdefs
  | None -> 
      Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs

and compile_named env auxdefs id =
  let (_,body,_) = lookup_named id env.env_named_context in
  match body with
  | Some t ->
      let code = lambda_of_constr env t in
      let auxdefs,code = compile_with_fv env auxdefs None code in
      Glet(Gnamed id, code)::auxdefs
  | None -> 
      Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs

let compile_constant env prefix ~interactive con body =
  match body with
  | Def t ->
      let t = Lazyconstr.force t in
      let code = lambda_of_constr env t in
      let is_lazy = is_lazy t in
      let code = if is_lazy then mk_lazy code else code in
      let name =
        if interactive then LinkedInteractive (prefix, is_lazy)
        else Linked (prefix, is_lazy)
      in
      let l = con_label con in
      let auxdefs,code = compile_with_fv env [] (Some l) code in
      let code =
        optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
      in
      code, name
  | _ -> 
      let i = push_symbol (SymbConst con) in
      [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))],
      if interactive then LinkedInteractive (prefix, false)
      else Linked (prefix, false)

let loaded_native_files = ref ([] : string list)

let is_loaded_native_file s = String.List.mem s !loaded_native_files

let register_native_file s =
  if not (is_loaded_native_file s) then
    loaded_native_files := s :: !loaded_native_files

let is_code_loaded ~interactive name =
  match !name with
  | NotLinked -> false
  | LinkedInteractive (s,_) ->
      if (interactive && is_loaded_native_file s) then true
      else (name := NotLinked; false)
  | Linked (s,_) ->
      if is_loaded_native_file s then true
      else (name := NotLinked; false)

let param_name = Name (id_of_string "params")
let arg_name = Name (id_of_string "arg")

let compile_mind prefix ~interactive mb mind stack =
  let f i stack ob =
    let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
    let j = push_symbol (SymbInd (mind,i)) in
    let name = Gind ("", (mind, i)) in
    let accu =
      Glet(name, MLapp (MLprimitive Mk_ind, [|get_ind_code j|]))
    in
    let nparams = mb.mind_nparams in
    let params = 
      Array.init nparams (fun i -> {lname = param_name; luid = i}) in
    let add_construct j acc (_,arity) = 
      let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in 
      let c = (mind,i), (j+1) in
	  Glet(Gconstruct ("",c),
	     mkMLlam (Array.append params args)
	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
    in
    Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl
  in
  let name =
    if interactive then LinkedInteractive (prefix, false)
    else Linked (prefix, false)
  in
  let upd = (mb.mind_native_name, name) in
  Array.fold_left_i f stack mb.mind_packets, upd

type code_location_update =
    Declarations.native_name ref * Declarations.native_name
type code_location_updates =
  code_location_update Mindmap_env.t * code_location_update Cmap_env.t

type linkable_code = global list * code_location_updates

let empty_updates = Mindmap_env.empty, Cmap_env.empty

let compile_mind_deps env prefix ~interactive
    (comp_stack, (mind_updates, const_updates) as init) mind =
  let mib = lookup_mind mind env in
  if is_code_loaded ~interactive mib.mind_native_name
    || Mindmap_env.mem mind mind_updates
  then init
  else
    let comp_stack, upd = compile_mind prefix ~interactive mib mind comp_stack in
    let mind_updates = Mindmap_env.add mind upd mind_updates in
    (comp_stack, (mind_updates, const_updates))

(* This function compiles all necessary dependencies of t, and generates code in
   reverse order, as well as linking information updates *)
let rec compile_deps env prefix ~interactive init t =
  match kind_of_term t with
  | Meta _ -> invalid_arg "Nativecode.compile_deps: Meta"
  | Evar _ -> invalid_arg "Nativecode.compile_deps: Evar"
  | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind
  | Const c ->
      let c = get_allias env c in
      let cb = lookup_constant c env in
      let (_, (_, const_updates)) = init in
      if is_code_loaded ~interactive cb.const_native_name
        || (Cmap_env.mem c const_updates)
      then init
      else
      let comp_stack, (mind_updates, const_updates) = match cb.const_body with
        | Def t -> compile_deps env prefix ~interactive init (Lazyconstr.force t)
        | _ -> init
      in
      let code, name = compile_constant env prefix ~interactive c cb.const_body in
      let comp_stack = code@comp_stack in
      let const_updates = Cmap_env.add c (cb.const_native_name, name) const_updates in
      comp_stack, (mind_updates, const_updates)
  | Construct ((mind,_),_) -> compile_mind_deps env prefix ~interactive init mind
  | Case (ci, p, c, ac) ->
      let mind = fst ci.ci_ind in
      let init = compile_mind_deps env prefix ~interactive init mind in
      fold_constr (compile_deps env prefix ~interactive) init t
  | _ -> fold_constr (compile_deps env prefix ~interactive) init t

let compile_constant_field env prefix con (code, (mupds, cupds)) cb =
  let acc = (code, (mupds, cupds)) in
  match cb.const_body with
  | Def t ->
    let t = Lazyconstr.force t in
    let (code, (mupds, cupds)) =
      compile_deps env prefix ~interactive:false acc t
    in
    let (gl, name) =
      compile_constant ~interactive:false env prefix con cb.const_body
    in
    let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
    gl@code, (mupds, cupds)
  | _ ->
    let (gl, name) =
      compile_constant env prefix ~interactive:false con cb.const_body
    in
    let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
    gl@code, (mupds, cupds)

let compile_mind_field prefix mp l (code, (mupds, cupds)) mb =
  let mind = MutInd.make2 mp l in
  let code, upd = compile_mind prefix ~interactive:false mb mind code in
  let mupds = Mindmap_env.add mind upd mupds in
  code, (mupds, cupds)

let mk_open s = Gopen s

let mk_internal_let s code =
  Glet(Ginternal s, code)

(* ML Code for conversion function *)
let mk_conv_code env prefix t1 t2 =
  let gl, (mind_updates, const_updates) =
    let init = ([], empty_updates) in
    compile_deps env prefix ~interactive:true init t1
  in
  let gl, (mind_updates, const_updates) =
    let init = (gl, (mind_updates, const_updates)) in
    compile_deps env prefix ~interactive:true init t2
  in
  let code1 = lambda_of_constr env t1 in
  let code2 = lambda_of_constr env t2 in
  let (gl,code1) = compile_with_fv env gl None code1 in
  let (gl,code2) = compile_with_fv env gl None code2 in
  let t1 = mk_internal_let "t1" code1 in
  let t2 = mk_internal_let "t2" code2 in
  let g1 = MLglobal (Ginternal "t1") in
  let g2 = MLglobal (Ginternal "t2") in
  let setref1 = Glet(Ginternal "_", MLsetref("rt1",g1)) in
  let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
  let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
  let header = Glet(Ginternal "symbols_tbl",
    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
      [|MLglobal (Ginternal "()")|])) in
  header::gl, (mind_updates, const_updates)

let mk_norm_code env prefix t =
  let gl, (mind_updates, const_updates) =
    let init = ([], empty_updates) in
    compile_deps env prefix ~interactive:true init t
  in
  let code = lambda_of_constr env t in
  let (gl,code) = compile_with_fv env gl None code in
  let t1 = mk_internal_let "t1" code in
  let g1 = MLglobal (Ginternal "t1") in
  let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
  let gl = List.rev (setref :: t1 :: gl) in
  let header = Glet(Ginternal "symbols_tbl",
    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
      [|MLglobal (Ginternal "()")|])) in
  header::gl, (mind_updates, const_updates)

let mk_library_header dir =
  let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
  [Glet(Ginternal "symbols_tbl",
    MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
    [|MLglobal (Ginternal libname)|]))]

let update_location (r,v) = r := v

let update_locations (ind_updates,const_updates) =
  Mindmap_env.iter (fun _ -> update_location) ind_updates;
  Cmap_env.iter (fun _ -> update_location) const_updates

let add_header_comment mlcode s =
  Gcomment s :: mlcode
(** }}} **)

(* vim: set filetype=ocaml foldmethod=marker: *)