open Util
open Names
open Esubst
open Term
open Constr
open Declarations
open Vmvalues
open Environ
open Pp

let pr_con sp = str(Names.Label.to_string (Constant.label sp))

type lambda =
  | Lrel          of Name.t * int
  | Lvar          of Id.t
  | Levar         of Evar.t * lambda array
  | Lprod         of lambda * lambda
  | Llam          of Name.t Context.binder_annot array * lambda
  | Llet          of Name.t Context.binder_annot * lambda * lambda
  | Lapp          of lambda * lambda array
  | Lconst        of pconstant
  | Lprim         of pconstant option * CPrimitives.t * lambda array
        (* No check if None *)
  | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
  | Lif           of lambda * lambda * lambda
  | Lfix          of (int array * int) * fix_decl
  | Lcofix        of int * fix_decl
  | Lint          of int
  | Lmakeblock    of int * lambda array
  | Luint         of Uint63.t
  | Lfloat        of Float64.t
  | Lval          of structured_values
  | Lsort         of Sorts.t
  | Lind          of pinductive
  | Lproj         of Projection.Repr.t * lambda

(* We separate branches for constant and non-constant constructors. If the OCaml
   limitation on non-constant constructors is reached, remaining branches are
   stored in [extra_branches]. *)
and lam_branches =
  { constant_branches : lambda array;
    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array }
(*    extra_branches : (name array * lambda) array } *)

and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array

(** Printing **)

let pr_annot x = Name.print x.Context.binder_name

let pp_names ids =
  prlist_with_sep (fun _ -> brk(1,1)) pr_annot (Array.to_list ids)

let pp_rel name n =
  Name.print name ++  str "##" ++ int n

let pp_sort s =
  match Sorts.family s with
  | InSet -> str "Set"
  | InProp -> str "Prop"
  | InSProp -> str "SProp"
  | InType -> str "Type"

let rec pp_lam lam =
  match lam with
  | Lrel (id,n) -> pp_rel id n
  | Lvar id -> Id.print id
  | Levar (evk, args) ->
    hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++
      prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")")
  | Lprod(dom,codom) -> hov 1
                          (str "forall(" ++
                           pp_lam dom ++
                           str "," ++ spc() ++
                           pp_lam codom ++
                           str ")")
  | Llam(ids,body) -> hov 1
                        (str "(fun " ++
                         pp_names ids ++
                         str " =>" ++
                         spc() ++
                         pp_lam body ++
                         str ")")
  | Llet(id,def,body) -> hov 0
                           (str "let " ++
                            pr_annot id ++
                            str ":=" ++
                            pp_lam def  ++
                            str " in" ++
                            spc() ++
                            pp_lam body)
  | Lapp(f, args) -> hov 1
                       (str "(" ++ pp_lam f ++ spc() ++
                        prlist_with_sep spc pp_lam (Array.to_list args) ++
                        str")")
  | Lconst (kn,_) -> pr_con kn
  | Lcase(_ci, _rtbl, t, a, branches) ->
    let ic = ref (-1) in
    let ib = ref 0 in
    v 0 (str"<" ++ pp_lam t ++ str">" ++ cut() ++
         str "Case" ++ spc () ++ pp_lam a ++ spc() ++ str "of" ++ cut() ++
         v 0
           ((prlist_with_sep (fun _ -> str "")
               (fun c ->
                  cut () ++ str "| " ++
                  int (incr ic; !ic) ++ str " => " ++ pp_lam c)
               (Array.to_list branches.constant_branches)) ++
            (prlist_with_sep (fun _ -> str "")
               (fun (ids,c) ->
                  cut () ++ str "| " ++
                  int (incr ib; !ib) ++ str " " ++
                  pp_names ids ++ str " => " ++ pp_lam c)
               (Array.to_list branches.nonconstant_branches)))
         ++ cut() ++ str "end")
  | Lif (t, bt, bf) ->
      v 0 (str "(if " ++ pp_lam t ++
             cut () ++ str "then " ++ pp_lam bt ++
             cut() ++ str "else " ++ pp_lam bf ++ str ")")
  | Lfix((t,i),(lna,tl,bl)) ->
    let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in
    hov 1
      (str"fix " ++ int i ++ spc() ++  str"{" ++
       v 0
         (prlist_with_sep spc
            (fun (na,i,ty,bd) ->
               pr_annot na ++ str"/" ++ int i ++ str":" ++
               pp_lam ty ++ cut() ++ str":=" ++
               pp_lam bd) (Array.to_list fixl)) ++
       str"}")

  | Lcofix (i,(lna,tl,bl)) ->
    let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
    hov 1
      (str"cofix " ++ int i ++ spc() ++  str"{" ++
       v 0
         (prlist_with_sep spc
            (fun (na,ty,bd) ->
               pr_annot na ++ str":" ++ pp_lam ty ++
               cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++
       str"}")
  | Lmakeblock(tag, args) ->
    hov 1
      (str "(makeblock " ++ int tag ++ spc() ++
       prlist_with_sep spc pp_lam (Array.to_list args) ++
       str")")
  | Luint i -> str (Uint63.to_string i)
  | Lfloat f -> str (Float64.to_string f)
  | Lval _ -> str "values"
  | Lsort s -> pp_sort s
  | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
  | Lprim(Some (kn,_u),_op,args) ->
     hov 1
         (str "(PRIM " ++ pr_con kn ++  spc() ++
            prlist_with_sep spc pp_lam  (Array.to_list args) ++
            str")")
  | Lprim(None,op,args) ->
     hov 1
         (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++  spc() ++
            prlist_with_sep spc pp_lam (Array.to_list args) ++
            str")")
  | Lproj(p,arg) ->
    hov 1
      (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
       ++ str ")")
  | Lint i ->
    Pp.(str "(int:" ++ int i ++ str ")")

(*s Constructors *)

let mkLapp f args =
  if Array.length args = 0 then f
  else
    match f with
    | Lapp(f', args') -> Lapp (f', Array.append args' args)
    | _ -> Lapp(f, args)

let mkLlam ids body =
  if Array.length ids = 0 then body
  else
    match body with
    | Llam(ids', body) -> Llam(Array.append ids ids', body)
    | _ -> Llam(ids, body)

let decompose_Llam lam =
  match lam with
  | Llam(ids,body) -> ids, body
  | _ -> [||], lam

(*s Operators on substitution *)
let subst_id = subs_id 0
let lift = subs_lift
let liftn = subs_liftn
let cons v subst = subs_cons([|v|], subst)
let shift subst = subs_shft (1, subst)

(* A generic map function *)

let map_lam_with_binders g f n lam =
  match lam with
  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _
  | Lfloat _ -> lam
  | Levar (evk, args) ->
    let args' = Array.Smart.map (f n) args in
    if args == args' then lam else Levar (evk, args')
  | Lprod(dom,codom) ->
    let dom' = f n dom in
    let codom' = f n codom in
    if dom == dom' && codom == codom' then lam else Lprod(dom',codom')
  | Llam(ids,body) ->
    let body' = f (g (Array.length ids) n) body in
    if body == body' then lam else mkLlam ids body'
  | Llet(id,def,body) ->
    let def' = f n def in
    let body' = f (g 1 n) body in
    if body == body' && def == def' then lam else Llet(id,def',body')
  | Lapp(fct,args) ->
    let fct' = f n fct in
    let args' = Array.Smart.map (f n) args in
    if fct == fct' && args == args' then lam else mkLapp fct' args'
  | Lcase(ci,rtbl,t,a,branches) ->
    let const = branches.constant_branches in
    let nonconst = branches.nonconstant_branches in
    let t' = f n t in
    let a' = f n a in
    let const' = Array.Smart.map (f n) const in
    let on_b b =
      let (ids,body) = b in
      let body' = f (g (Array.length ids) n) body in
      if body == body' then b else (ids,body') in
    let nonconst' = Array.Smart.map on_b nonconst in
    let branches' =
      if const == const' && nonconst == nonconst' then
        branches
      else
        { constant_branches = const';
          nonconstant_branches = nonconst' }
    in
    if t == t' && a == a' && branches == branches' then lam else
      Lcase(ci,rtbl,t',a',branches')
  | Lif(t,bt,bf) ->
      let t' = f n t in
      let bt' = f n bt in
      let bf' = f n bf in
      if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf')
  | Lfix(init,(ids,ltypes,lbodies)) ->
    let ltypes' = Array.Smart.map (f n) ltypes in
    let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
    if ltypes == ltypes' && lbodies == lbodies' then lam
    else Lfix(init,(ids,ltypes',lbodies'))
  | Lcofix(init,(ids,ltypes,lbodies)) ->
    let ltypes' = Array.Smart.map (f n) ltypes in
    let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
    if ltypes == ltypes' && lbodies == lbodies' then lam
    else Lcofix(init,(ids,ltypes',lbodies'))
  | Lmakeblock(tag,args) ->
    let args' = Array.Smart.map (f n) args in
    if args == args' then lam else Lmakeblock(tag,args')
  | Lprim(kn,op,args) ->
    let args' = Array.Smart.map (f n) args in
    if args == args' then lam else Lprim(kn,op,args')
  | Lproj(p,arg) ->
    let arg' = f n arg in
    if arg == arg' then lam else Lproj(p,arg')

(*s Lift and substitution *)


let rec lam_exlift el lam =
  match lam with
  | Lrel(id,i) ->
    let i' = reloc_rel i el in
    if i == i' then lam else Lrel(id,i')
  | _ -> map_lam_with_binders el_liftn lam_exlift el lam

let lam_lift k lam =
  if k = 0 then lam
  else lam_exlift (el_shft k el_id) lam

let lam_subst_rel lam id n subst =
  match expand_rel n subst with
  | Inl(k,v) -> lam_lift k v
  | Inr(n',_) ->
    if n == n' then lam
    else Lrel(id, n')

let rec lam_exsubst subst lam =
  match lam with
  | Lrel(id,i) -> lam_subst_rel lam id i subst
  | _ -> map_lam_with_binders liftn lam_exsubst subst lam

let lam_subst_args subst args =
  if is_subs_id subst then args
  else Array.Smart.map (lam_exsubst subst) args

(** Simplification of lambda expression *)

(* [simplify subst lam] simplify the expression [lam_subst subst lam] *)
(* that is :                                                          *)
(* - Reduce [let] is the definition can be substituted i.e:           *)
(*    - a variable (rel or identifier)                                *)
(*    - a constant                                                    *)
(*    - a structured constant                                         *)
(*    - a function                                                    *)
(* - Transform beta redex into [let] expression                       *)
(* - Move arguments under [let]                                       *)
(* Invariant : Terms in [subst] are already simplified and can be     *)
(*             substituted                                            *)

let can_subst lam =
  match lam with
  | Lrel _ | Lvar _ | Lconst _ | Luint _
  | Lval _ | Lsort _ | Lind _ -> true
  | _ -> false


let can_merge_if bt bf =
  match bt, bf with
  | Llam(_idst,_), Llam(_idsf,_) -> true
  | _ -> false

let merge_if t bt bf =
  let (idst,bodyt) = decompose_Llam bt in
  let (idsf,bodyf) = decompose_Llam bf in
  let nt = Array.length idst in
  let nf = Array.length idsf in
  let common,idst,idsf =
    if nt = nf then idst, [||], [||]
    else
      if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
      else idsf, Array.sub idst nf (nt - nf), [||] in
  Llam(common,
       Lif(lam_lift (Array.length common) t,
           mkLlam idst bodyt,
           mkLlam idsf bodyf))


let rec simplify subst lam =
  match lam with
  | Lrel(id,i) -> lam_subst_rel lam id i subst

  | Llet(id,def,body) ->
      let def' = simplify subst def in
      if can_subst def' then simplify (cons def' subst) body
      else
        let body' = simplify (lift subst) body in
        if def == def' && body == body' then lam
        else Llet(id,def',body')

  | Lapp(f,args) ->
      begin match simplify_app subst f subst args with
      | Lapp(f',args') when f == f' && args == args' -> lam
      | lam' -> lam'
      end

  | Lif(t,bt,bf) ->
      let t' = simplify subst t in
      let bt' = simplify subst bt in
      let bf' = simplify subst bf in
      if can_merge_if bt' bf' then merge_if t' bt' bf'
      else
        if t == t' && bt == bt' && bf == bf' then lam
        else Lif(t',bt',bf')
  | _ -> map_lam_with_binders liftn simplify subst lam

and simplify_app substf f substa args =
  match f with
  | Lrel(id, i) ->
    begin match lam_subst_rel f id i substf with
      | Llam(ids, body) ->
        reduce_lapp
          subst_id (Array.to_list ids) body
          substa (Array.to_list args)
      | f' -> mkLapp f' (simplify_args substa args)
    end
  | Llam(ids, body) ->
    reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args)
  | Llet(id, def, body) ->
    let def' = simplify substf def in
    if can_subst def' then
      simplify_app (cons def' substf) body substa args
    else
      Llet(id, def', simplify_app (lift substf) body (shift substa) args)
  | Lapp(f, args') ->
    let args = Array.append
        (lam_subst_args substf args') (lam_subst_args substa args) in
    simplify_app substf f subst_id args
  | _ -> mkLapp (simplify substf f) (simplify_args substa args)

and simplify_args subst args = Array.Smart.map (simplify subst) args

and reduce_lapp substf lids body substa largs =
  match lids, largs with
  | id::lids, a::largs ->
    let a = simplify substa a in
    if can_subst a then
      reduce_lapp (cons a substf) lids body substa largs
    else
      let body = reduce_lapp (lift substf) lids body (shift substa) largs in
      Llet(id, a, body)
  | [], [] -> simplify substf body
  | _::_, _ ->
    Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body)
  | [], _ -> simplify_app substf body substa (Array.of_list largs)




(* [occurrence kind k lam]:
   If [kind] is [true] return [true] if the variable [k] does not appear in
   [lam], return [false] if the variable appear one time and not
   under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
   If [kind] is [false] return [false] if the variable does not appear in [lam]
   else raise [Not_found]
*)

let rec occurrence k kind lam =
  match lam with
  | Lrel (_,n) ->
    if n = k then
      if kind then false else raise Not_found
    else kind
  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _
  | Lfloat _ -> kind
  | Levar (_, args) ->
    occurrence_args k kind args
  | Lprod(dom, codom) ->
    occurrence k (occurrence k kind dom) codom
  | Llam(ids,body) ->
    let _ = occurrence (k+Array.length ids) false body in kind
  | Llet(_,def,body) ->
    occurrence (k+1) (occurrence k kind def) body
  | Lapp(f, args) ->
    occurrence_args k (occurrence k kind f) args
  | Lprim(_,_,args) | Lmakeblock(_,args) ->
    occurrence_args k kind args
  | Lcase(_ci,_rtbl,t,a,branches) ->
    let kind = occurrence k (occurrence k kind t) a in
    let r = ref kind in
    Array.iter (fun c -> r := occurrence k kind c  && !r) branches.constant_branches;
    let on_b (ids,c) =
      r := occurrence (k+Array.length ids) kind c && !r
    in
    Array.iter on_b branches.nonconstant_branches;
    !r
  | Lif (t, bt, bf) ->
      let kind = occurrence k kind t in
      kind && occurrence k kind bt && occurrence k kind bf
  | Lfix(_,(ids,ltypes,lbodies))
  | Lcofix(_,(ids,ltypes,lbodies)) ->
    let kind = occurrence_args k kind ltypes in
    let _ = occurrence_args (k+Array.length ids) false lbodies in
    kind
  | Lproj(_,arg) ->
    occurrence k kind arg

and occurrence_args k kind args =
  Array.fold_left (occurrence k) kind args

let occur_once lam =
  try let _ = occurrence 1 true lam in true
  with Not_found -> false

(* [remove_let lam] remove let expression in [lam] if the variable is *)
(* used at most once time in the body, and does not appear under      *)
(* a lambda or a fix or a cofix                                       *)

let rec remove_let subst lam =
  match lam with
  | Lrel(id,i) -> lam_subst_rel lam id i subst
  | Llet(id,def,body) ->
    let def' = remove_let subst def in
    if occur_once body then remove_let (cons def' subst) body
    else
      let body' = remove_let (lift subst) body in
      if def == def' && body == body' then lam else Llet(id,def',body')
  | _ -> map_lam_with_binders liftn remove_let subst lam


(*s Translation from [constr] to [lambda] *)

(* Translation of constructor *)

(* Limitation due to OCaml's representation of non-constant
  constructors: limited to 245 + 1 (0 tag) cases. *)

exception TooLargeInductive of Pp.t

let max_nb_const = 0x1000000
let max_nb_block = 0x1000000 + Obj.last_non_constant_constructor_tag - 1

let str_max_constructors =
  Format.sprintf
    " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block

let check_compilable ib =

  if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then
    let msg =
      Pp.(str "Cannot compile code for virtual machine as it uses inductive "
          ++ Id.print ib.mind_typename ++ str str_max_constructors)
    in
    raise (TooLargeInductive msg)

let is_value lc =
  match lc with
  | Lval _ | Lint _ | Luint _ -> true
  | _ -> false

let get_value lc =
  match lc with
  | Luint i -> val_of_uint i
  | Lval v -> v
  | Lint i -> val_of_int i
  | _ -> raise Not_found

let make_args start _end =
  Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))

(* Translation of constructors *)
let expand_constructor tag nparams arity =
  let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
  let ids = Array.make (nparams + arity) anon in
  if arity = 0 then mkLlam ids (Lint tag)
  else
    let args = make_args arity 1 in
    Llam(ids, Lmakeblock (tag, args))

let makeblock tag nparams arity args =
  let nargs = Array.length args in
  if nparams > 0 || nargs < arity then
    mkLapp (expand_constructor tag nparams arity) args
  else
    (* The constructor is fully applied *)
  if arity = 0 then Lint tag
  else
  if Array.for_all is_value args then
    if tag < Obj.last_non_constant_constructor_tag then
      Lval(val_of_block tag (Array.map get_value args))
    else
      let args = Array.map get_value args in
      let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in
      Lval(val_of_block Obj.last_non_constant_constructor_tag args)
  else Lmakeblock(tag, args)

let makearray args def =
  try
    let p = Array.map get_value args in
    Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def))
  with Not_found ->
    let ar = Lmakeblock(0, args) in (* build the ocaml array *)
    let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *)
    Lmakeblock(0,[|kind|]) (* the reference *)

(* Compiling constants *)

let rec get_alias env kn =
  let cb = lookup_constant kn env in
  let tps = cb.const_body_code in
  match tps with
  | None -> kn
  | Some tps ->
    (match Cemitcodes.force tps with
     | Cemitcodes.BCalias kn' -> get_alias env kn'
     | _ -> kn)

(* Compilation of primitive *)

let prim kn p args =
  Lprim(Some kn, p, args)

let expand_prim kn op arity =
  (* primitives are always Relevant *)
  let ids = Array.make arity Context.anonR in
  let args = make_args arity 1 in
  Llam(ids, prim kn op args)

let lambda_of_prim kn op args =
  let arity = CPrimitives.arity op in
  match Int.compare (Array.length args) arity with
  | 0 -> prim kn op args
  | x when x > 0 ->
    let prim_args = Array.sub args 0 arity in
    let extra_args = Array.sub args arity (Array.length args - arity) in
    mkLapp(prim kn op prim_args) extra_args
  | _ -> mkLapp (expand_prim kn op arity) args

(*i Global environment *)

let get_names decl =
  let decl = Array.of_list decl in
  Array.map fst decl


(* Rel Environment *)
module Vect =
struct
  type 'a t = {
    mutable elems : 'a array;
    mutable size : int;
  }

  let make n a = {
    elems = Array.make n a;
    size = 0;
  }

  let extend (v : 'a t) =
    if v.size = Array.length v.elems then
      let new_size = min (2*v.size) Sys.max_array_length in
      if new_size <= v.size then raise (Invalid_argument "Vect.extend");
      let new_elems = Array.make new_size v.elems.(0) in
      Array.blit v.elems 0 new_elems 0 (v.size);
      v.elems <- new_elems

  let push v a =
    extend v;
    v.elems.(v.size) <- a;
    v.size <- v.size + 1

  let popn (v : 'a t) n =
    v.size <- max 0 (v.size - n)

  let pop v = popn v 1

  let get_last (v : 'a t) n =
    if v.size <= n then raise
        (Invalid_argument "Vect.get:index out of bounds");
    v.elems.(v.size - n - 1)

end

let dummy_lambda = Lrel(Anonymous, 0)

let empty_args = [||]

module Renv =
struct

  type constructor_info = tag * int * int (* nparam nrealargs *)

  type t = {
    global_env : env;
    name_rel : Name.t Vect.t;
    construct_tbl : (constructor, constructor_info) Hashtbl.t;
  }

  let make env = {
    global_env = env;
    name_rel = Vect.make 16 Anonymous;
    construct_tbl = Hashtbl.create 111
  }

  let push_rel env id = Vect.push env.name_rel id.Context.binder_name

  let push_rels env ids =
    Array.iter (push_rel env) ids

  let pop env = Vect.pop env.name_rel

  let popn env n =
    for _i = 1 to n do pop env done

  let get env n =
    Lrel (Vect.get_last env.name_rel (n-1), n)

  let get_construct_info env c =
    try Hashtbl.find env.construct_tbl c
    with Not_found ->
      let ((mind,j), i) = c in
      let oib = lookup_mind mind env.global_env in
      let oip = oib.mind_packets.(j) in
      check_compilable oip;
      let tag,arity = oip.mind_reloc_tbl.(i-1) in
      let nparams = oib.mind_nparams in
      let r = (tag, nparams, arity) in
      Hashtbl.add env.construct_tbl c r;
      r
end

open Renv

let rec lambda_of_constr env c =
  match Constr.kind c with
  | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
  | Evar (evk, args) ->
    let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
    Levar (evk, args)

  | Cast (c, _, _) -> lambda_of_constr env c

  | Rel i -> Renv.get env i

  | Var id -> Lvar id

  | Sort s -> Lsort s
  | Ind ind -> Lind ind

  | Prod(id, dom, codom) ->
    let ld = lambda_of_constr env dom in
    Renv.push_rel env id;
    let lc = lambda_of_constr env codom in
    Renv.pop env;
    Lprod(ld, Llam([|id|], lc))

  | Lambda _ ->
    let params, body = decompose_lam c in
    let ids = get_names (List.rev params) in
    Renv.push_rels env ids;
    let lb = lambda_of_constr env body in
    Renv.popn env (Array.length ids);
    mkLlam ids lb

  | LetIn(id, def, _, body) ->
    let ld = lambda_of_constr env def in
    Renv.push_rel env id;
    let lb = lambda_of_constr env body in
    Renv.pop env;
    Llet(id, ld, lb)

  | App(f, args) -> lambda_of_app env f args

  | Const _ -> lambda_of_app env c empty_args

  | Construct _ ->  lambda_of_app env c empty_args

  | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
    let ind = ci.ci_ind in
    let mib = lookup_mind (fst ind) env.global_env in
    let oib = mib.mind_packets.(snd ind) in
    let () = check_compilable oib in
    let rtbl = oib.mind_reloc_tbl in


    (* translation of the argument *)
    let la = lambda_of_constr env a in
    (* translation of the type *)
    let lt = lambda_of_constr env t in
    (* translation of branches *)
    let consts = Array.make oib.mind_nb_constant dummy_lambda in
    let blocks = Array.make oib.mind_nb_args ([||],dummy_lambda) in
    for i = 0 to Array.length rtbl - 1 do
      let tag, arity = rtbl.(i) in
      let b = lambda_of_constr env branches.(i) in
      if arity = 0 then consts.(tag) <- b
      else
        let b =
          match b with
          | Llam(ids, body) when Array.length ids = arity -> (ids, body)
          | _ ->
            let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
            let ids = Array.make arity anon in
            let args = make_args arity 1 in
            let ll = lam_lift arity b in
            (ids, mkLapp  ll args)
        in blocks.(tag-1) <- b
    done;
    let branches =
      { constant_branches = consts;
        nonconstant_branches = blocks }
    in
    Lcase(ci, rtbl, lt, la, branches)

  | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
    let ltypes = lambda_of_args env 0 type_bodies in
    Renv.push_rels env names;
    let lbodies = lambda_of_args env 0 rec_bodies in
    Renv.popn env (Array.length names);
    Lfix(rec_init, (names, ltypes, lbodies))

  | CoFix(init,(names,type_bodies,rec_bodies)) ->
    let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in
    let ltypes = lambda_of_args env 0 type_bodies in
    Renv.push_rels env names;
    let lbodies = lambda_of_args env 0 rec_bodies in
    Renv.popn env (Array.length names);
    Lcofix(init, (names, ltypes, lbodies))

  | Proj (p,c) ->
    let lc = lambda_of_constr env c in
    Lproj (Projection.repr p,lc)

  | Int i -> Luint i
  | Float f -> Lfloat f
  | Array(_u, t,def,_ty) ->
    let def = lambda_of_constr env def in
    makearray (lambda_of_args env 0 t) def

and lambda_of_app env f args =
  match Constr.kind f with
  | Const (kn,u as c) ->
      let kn = get_alias env.global_env kn in
      let cb = lookup_constant kn env.global_env in
      begin match cb.const_body with
      | Primitive op -> lambda_of_prim (kn,u) op (lambda_of_args env 0 args)
      | Def csubst when cb.const_inline_code ->
          lambda_of_app env (Mod_subst.force_constr csubst) args
      | Def _ | OpaqueDef _ | Undef _ -> mkLapp (Lconst c) (lambda_of_args env 0 args)
      end
  | Construct (c,_) ->
      let tag, nparams, arity = Renv.get_construct_info env c in
      let nargs = Array.length args in
      if nparams < nargs then (* got all parameters *)
        let args = lambda_of_args env nparams args in
        makeblock tag 0 arity args
      else makeblock tag (nparams - nargs) arity empty_args
  | _ ->
      let f = lambda_of_constr env f in
      let args = lambda_of_args env 0 args in
      mkLapp f args

and lambda_of_args env start args =
  let nargs = Array.length args in
  if start < nargs then
    Array.init (nargs - start)
      (fun i -> lambda_of_constr env args.(start + i))
  else empty_args

(*********************************)
let dump_lambda = ref false

let optimize_lambda lam =
  let lam = simplify subst_id lam in
  remove_let subst_id lam

let lambda_of_constr ~optimize genv c =
  let env = Renv.make genv in
  let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in
  Renv.push_rels env (Array.of_list ids);
  let lam = lambda_of_constr env c in
  let lam = if optimize then optimize_lambda lam else lam in
  if !dump_lambda then
    Feedback.msg_debug (pp_lam lam);
  lam