(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(*i $Id$ i*)

open Pp
open Util
open Names
open Nameops
open Term
open Termops
open Declarations
open Environ
open Reductionops
open Inductive
open Inductiveops
open Instantiate
open Miniml
open Table
open Mlutil
open Closure
open Summary
open Nametab

(*s Extraction results. *)

(* The flag [type_var] gives us information about an identifier
   coming from a Lambda or a Product:
   \begin{itemize}
   \item [Arity] denotes identifiers of type an arity of some sort [Set],
     [Prop] or [Type], that is $(x_1:X_1)\ldots(x_n:X_n)s$ with [s = Set],
     [Prop] or [Type] 
   \item [NotArity] denotes the other cases. It may be inexact after 
   instanciation. For example [(X:Type)X] is [NotArity] and may give [Set]
   after instanciation, which is rather [Arity]
   \item [Logic] denotes identifiers of type an arity of sort [Prop], 
     or of type of type [Prop]
   \item [Info] is the opposite. The same example [(X:Type)X] shows 
     that an [Info] term might in fact be [Logic] later on. 
   \end{itemize} *)

type info = Logic | Info

type arity = Arity | NotArity

type type_var = info * arity

let logic_arity = (Logic, Arity)
let info_arity = (Info, Arity)
let logic = (Logic, NotArity)
let default = (Info, NotArity)

(* The [signature] type is used to know how many arguments a CIC
   object expects, and what these arguments will become in the ML
   object. *)
   
(* Convention: outmost lambda/product gives the head of the list *)

type signature = type_var list

(* When dealing with CIC contexts, we maintain corresponding contexts 
   telling whether a variable will be kept or will disappear.
   Cf. [renum_db]. *)

(* Convention: innermost ([Rel 1]) is at the head of the list *)

type extraction_context = bool list

(* The [type_extraction_result] is the result of the [extract_type] function
   that extracts a CIC object into an ML type. It is either: 
   \begin{itemize}
   \item a real ML type, followed by its list of type variables (['a],\ldots)
   \item a CIC arity, without counterpart in ML
   \item a non-informative type, which will receive special treatment
   \end{itemize} *)

type type_extraction_result =
  | Tmltype of ml_type * identifier list
  | Tarity
  | Tprop

(* The [term_extraction_result] is the result of the [extract_term]
   function that extracts a CIC object into an ML term *)

type term_extraction_result = 
  | Rmlterm of ml_ast
  | Rprop

(* The [extraction_result] is the result of the [extract_constr]
   function that extracts any CIC object. It is either a ML type, a ML
   object or something non-informative. *)

type extraction_result =
  | Emltype of ml_type * signature * identifier list
  | Emlterm of ml_ast

(*s Utility functions. *)

let none = Evd.empty

let type_of env c = Retyping.get_type_of env Evd.empty (strip_outer_cast c)

let sort_of env c = 
  Retyping.get_sort_family_of env Evd.empty (strip_outer_cast c)

open RedFlags
let whd_betaiotalet = clos_norm_flags (mkflags [fBETA;fIOTA;fZETA])

let is_axiom sp = (Global.lookup_constant sp).const_body = None

type lamprod = Lam | Product

let flexible_name = id_of_string "flex"

let id_of_name = function
  | Anonymous -> id_of_string "x"
  | Name id   -> id

(* [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t]
   returns the list [[a;b;...;z]]. It is used when making the ML types
   of inductive definitions. We also suppress [Prop] parts. *)

let rec list_of_ml_arrows = function
  | Tarr (Miniml.Tarity, b) -> assert false
  | Tarr (Miniml.Tprop, b) -> list_of_ml_arrows b
  | Tarr (a, b) -> a :: list_of_ml_arrows b
  | t -> []

(*s [get_arity c] returns [Some s] if [c] is an arity of sort [s], 
   and [None] otherwise. *)

let rec get_arity env c =
  match kind_of_term (whd_betadeltaiota env none c) with
    | Prod (x,t,c0) -> get_arity (push_rel (x,None,t) env) c0
    | Cast (t,_) -> get_arity env t
    | Sort s -> Some (family_of_sort s)
    | _ -> None

(* idem, but goes through [Lambda] as well. Cf. [find_conclusion]. *)

let rec get_lam_arity env c =
  match kind_of_term (whd_betadeltaiota env none c) with
    | Lambda (x,t,c0) -> get_lam_arity (push_rel (x,None,t) env) c0
    | Prod (x,t,c0) -> get_lam_arity (push_rel (x,None,t) env) c0
    | Cast (t,_) -> get_lam_arity env t
    | Sort s -> Some (family_of_sort s)
    | _ -> None

(*s Detection of non-informative parts. *)

let is_non_info_sort env s = is_Prop (whd_betadeltaiota env none s)

let is_non_info_type env t = 
  (sort_of env t) = InProp  || (get_arity env t) = Some InProp

(*i This one is not used, left only to precise what we call a non-informative 
   term.

let is_non_info_term env c = 
  let t = type_of env c in
  let s = sort_of env t in
  (s <> InProp) ||
  match get_arity env t with 
    | Some InProp -> true
    | Some InType -> (get_lam_arity env c = Some InProp)
    | _ -> false
i*)

(* [v_of_t] transforms a type [t] into a [type_var] flag. *)

let v_of_t env t = match get_arity env t with
  | Some InProp -> logic_arity
  | Some _ -> info_arity
  | _ -> if is_non_info_type env t then logic else default

(*s Operations on binders *)

type binders = (name * constr) list

(* Convention: right binders give [Rel 1] at the head, like those answered by 
   [decompose_prod]. Left binders are the converse. *)

let rec lbinders_fold f acc env = function 
  | [] -> acc
  | (n,t) as b :: l -> 
      f n t (v_of_t env t)
        (lbinders_fold f acc (push_rel_assum b env) l)

(* [sign_of_arity] transforms an arity into a signature. It is used 
   for example with the types of inductive definitions, which are known
   to be already in arity form. *)

let sign_of_lbinders = lbinders_fold (fun _ _ v a -> v::a) [] 

let sign_of_arity env c = 
  sign_of_lbinders env (List.rev (fst (decompose_prod c)))

(* [vl_of_arity] returns the list of the lambda variables tagged [info_arity]
   in an arity. Renaming is done. *)

let vl_of_lbinders = 
  lbinders_fold 
    (fun n _ v a -> 
       if v = info_arity 
       then (next_ident_away (id_of_name n) (prop_name::a))::a 
       else a) []
  
let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c)))
	 
(*s [renum_db] gives the new de Bruijn indices for variables in an ML
   term.  This translation is made according to an [extraction_context]. *)
	
let renum_db ctx n = 
  let rec renum = function
    | (1, true  :: _) -> 1
    | (n, true  :: s) -> succ (renum (pred n, s))
    | (n, false :: s) -> renum (pred n, s)
    | _ -> assert false
  in
  renum (n, ctx)

(*s Decomposition of a function expecting n arguments at least. We eta-expanse
   if needed *)

let force_n_prod n env c = 
  if nb_prod c < n then whd_betadeltaiota env none c else c

let decompose_lam_eta n env c = 
  let dif = n - (nb_lam c) in 
  if dif <= 0 then 
    decompose_lam_n n c
  else
    let t = type_of env c in
    let (trb,_) = decompose_prod_n n (force_n_prod n env t) in
    let (rb, e) = decompose_lam c in 
    let rb = (list_firstn dif trb) @ rb in 
    let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in
    (rb, e)

(*s TODO commentaires *)

let prop_abstract_1 f  = 
  let rec abs rels i = function 
    | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels)
    | (_,Arity) :: l -> abs rels i l
    | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
    | (Logic,_) :: l -> MLlam (prop_name, abs rels (succ i) l)
  in abs [] 1  
  
let prop_abstract_2 f = 
  let rec abs rels i = function 
    | [] -> f i (List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels)
    | (_,Arity) :: l -> abs rels i l
    | (Info,_) :: l -> MLlam (anonymous, abs (MLrel i :: rels) (succ i) l)
    | (Logic,_) :: l -> MLlam (prop_name, abs (MLprop :: rels) (succ i) l)
  in abs [] 1 


(*s Abstraction of an constant. *)

let abstract_const sp s = 
  if List.mem default s then 
    prop_abstract_1 (fun a -> MLapp(MLglob (ConstRef sp), a)) s
  else MLglob (ConstRef sp)

(*s The opposite function. *)

let eta_expanse_w_prop e s = 
  let s = List.filter (function (_,NotArity) -> true | _ -> false) s in
  let ids,e = collect_lams e in
  let m = List.length ids in 
  assert (m <= (List.length s)); 
  let _,s = list_chop m s in 
  let core = if s <> [] then 
    prop_abstract_2 (fun i a -> MLapp (ml_lift (i-1) e,a)) s 
  else e 
  in let new_e = named_lams core ids in 
  try 
    let new_e,_,_ = kill_prop_aux new_e in new_e 
  with Impossible -> new_e

(*s Error message when extraction ends on an axiom. *)

let axiom_message sp =
  errorlabstrm "axiom_message"
    (str "You must specify an extraction for axiom" ++ spc () ++ 
       pr_sp sp ++ spc () ++ str "first.")

let section_message () = 
  errorlabstrm "section_message"
    (str "You can't extract within a section. Close it and try again.")

(*s Tables to keep the extraction of inductive types and constructors. *)

type inductive_extraction_result = 
  | Iml of signature * identifier list
  | Iprop
   
let inductive_extraction_table = 
  ref (Gmap.empty : (inductive, inductive_extraction_result) Gmap.t)

let add_inductive_extraction i e = 
  inductive_extraction_table := Gmap.add i e !inductive_extraction_table

let lookup_inductive_extraction i = Gmap.find i !inductive_extraction_table

type constructor_extraction_result = 
  | Cml of ml_type list * signature * int
  | Cprop

let constructor_extraction_table = 
  ref (Gmap.empty : (constructor, constructor_extraction_result) Gmap.t)

let add_constructor_extraction c e = 
  constructor_extraction_table := Gmap.add c e !constructor_extraction_table

let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table

let constant_table = 
  ref (Gmap.empty : (section_path, extraction_result) Gmap.t)

let signature_table = 
  ref (Gmap.empty : (section_path, signature) Gmap.t)

(* Tables synchronization. *)

let freeze () =
  !inductive_extraction_table, !constructor_extraction_table, 
  !constant_table, !signature_table

let unfreeze (it,cst,ct,st) =
  inductive_extraction_table := it;
  constructor_extraction_table := cst;
  constant_table := ct;
  signature_table := st

let _ = declare_summary "Extraction tables"
	  { freeze_function = freeze;
	    unfreeze_function = unfreeze;
	    init_function = (fun () -> ());
	    survive_section = true }


(*s Extraction of a type. *)

(* When calling [extract_type] we suppose that the type of [c] is an
   arity. This is for example checked in [extract_constr]. *)

(* Relation with [v_of_t]: it is less precise, since we do not 
   delta-reduce in [extract_type] in general.
   \begin{itemize}
   \item If [v_of_t env t = NotArity,_], 
   then [extract_type env t] is a [Tmltype].
   \item If [extract_type env t = Tarity], then [v_of_t env t = Arity,_]
   \end{itemize} *)

(* Generation of type variable list (['a] in caml).
   In Coq [(a:Set)(a:Set)a] is legal, but in ML we have only a flat list 
   of type variable, so we must take care of renaming now, in order to get 
   something like [type ('a,'a0) foo = 'a0].  The list [vl] is used to 
   accumulate those type variables and to do renaming on the fly. 
   Convention: the last elements of this list correspond to external products.
   This is used when dealing with applications *)

let rec extract_type env c =
  extract_type_rec env c [] [] 

and extract_type_rec env c vl args = 
  (* We accumulate the context, arguments and generated variables list *)
  let t = type_of env (applist (c, args)) in
    (* Since [t] is an arity, there is two non-informative case: 
       [t] is an arity of sort [Prop], or 
       [c] has a non-informative head symbol *)
    match get_arity env t with 
      | None -> 
	  assert false (* Cf. precondition. *)
      | Some InProp ->
	  Tprop 
      | Some _ -> extract_type_rec_info env c vl args
	    
and extract_type_rec_info env c vl args = 
  match (kind_of_term (whd_betaiotalet env none c)) with
    | Sort _ ->
	assert (args = []); (* A sort can't be applied. *)
	Tarity 
    | Prod (n,t,d) ->
	assert (args = []); (* A product can't be applied. *)
	extract_prod_lam env (n,t,d) vl Product
    | Lambda (n,t,d) ->
	assert (args = []); (* [c] is now in head normal form. *)
	extract_prod_lam env (n,t,d) vl Lam
    | App (d, args') ->
	(* We just accumulate the arguments. *)
	extract_type_rec_info env d vl (Array.to_list args' @ args)
    | Rel n -> 
	(match lookup_rel n env with
	   | (_,Some t,_) -> 
	       extract_type_rec_info env (lift n t) vl args  
	   | (id,_,_) ->
	       Tmltype (Tvar (id_of_name id), vl))
    | Const sp when args = [] && is_ml_extraction (ConstRef sp) ->
	Tmltype (Tglob (ConstRef sp), vl)
    | Const sp when is_axiom sp -> 
	let id = next_ident_away (basename sp) (prop_name::vl) in 
	Tmltype (Tvar id,  id :: vl)
    | Const sp ->
	let t = constant_type env sp in 
	if is_arity env none t then
	  (match extract_constant sp with 
	     | Emltype (Miniml.Tarity,_,_) -> Tarity
	     | Emltype (Miniml.Tprop,_,_) -> Tprop
	     | Emltype (_, sc, vlc) ->  
		 extract_type_app env (ConstRef sp,sc,vlc) vl args 
	     | Emlterm _ -> assert false) 
	else 
	  (* We can't keep as ML type abbreviation a CIC constant *)
	  (* which type is not an arity: we reduce this constant. *)
	  let cvalue = constant_value env sp in
	  extract_type_rec_info env (applist (cvalue, args)) vl []
    | Ind spi ->
	(match extract_inductive spi with 
	   |Iml (si,vli) -> 
	       extract_type_app env (IndRef spi,si,vli) vl args 
	   |Iprop -> assert false (* Cf. initial tests *))
    | Case _ | Fix _ | CoFix _ ->
	let id = next_ident_away flexible_name (prop_name::vl) in
	Tmltype (Tvar id,  id :: vl)
	  (* Type without counterpart in ML: we generate a 
	     new flexible type variable. *) 
    | Cast (c, _) ->
	extract_type_rec_info env c vl args
    | Var _ -> section_message ()
    | _ -> 
	assert false

(* Auxiliary function used to factor code in lambda and product cases *)

and extract_prod_lam env (n,t,d) vl flag = 
  let tag = v_of_t env t in
  let env' = push_rel_assum (n,t) env in
  match tag,flag with
    | (Info, Arity), _ -> 
	(* We rename before the [push_rel], to be sure that the corresponding*)
	(* [lookup_rel] will be correct. *)
	let id' = next_ident_away (id_of_name n) (prop_name::vl) in 
	let env' = push_rel_assum (Name id', t) env in
	extract_type_rec_info env' d (id'::vl) []
    | (Logic, Arity), _ | _, Lam ->
      extract_type_rec_info  env' d vl []
    | (Logic, NotArity), Product ->
      (match extract_type_rec_info env' d vl [] with 
         | Tmltype (mld, vl') -> Tmltype (Tarr (Miniml.Tprop, mld), vl')
         | et -> et)
    | (Info, NotArity), Product ->
	(* It is important to treat [d] first and [t] in second. *)
	(* This ensures that the end of [vl] correspond to external binders. *)
	(match extract_type_rec_info env' d vl [] with 
	   | Tmltype (mld, vl') -> 
	       (match extract_type_rec_info env t vl' [] with
		  | Tprop | Tarity -> assert false 
			(* Cf. relation between [extract_type] and [v_of_t] *)
		  | Tmltype (mlt,vl'') -> Tmltype (Tarr(mlt,mld), vl''))
	   | et -> et)
	
 (* Auxiliary function dealing with type application. 
    Precondition: [r] is of type an arity. *)
		  
and extract_type_app env (r,sc,vlc) vl args =
  let diff = (List.length args - List.length sc ) in
  let args = if diff > 0 then begin
    (* This can (normally) only happen when r is a flexible type. 
       We discard the remaining arguments *)
    (*i    wARN (hov 0 (str ("Discarding " ^
		 (string_of_int diff) ^ " type(s) argument(s)."))); i*)
    list_firstn (List.length sc) args
  end else args in
  let nargs = List.length args in
  (* [r] is of type an arity, so it can't be applied to more than n args, 
     where n is the number of products in this arity type. *)
  (* But there are flexibles ... *)
  let sign_args = list_firstn nargs sc in
  let (mlargs,vl') = 
    List.fold_right 
      (fun (v,a) ((args,vl) as acc) -> match v with
	 | _, NotArity -> acc
	 | Logic, Arity -> acc
	 | Info, Arity -> match extract_type_rec_info env a vl [] with
	     | Tarity -> (Miniml.Tarity :: args, vl) 
  	           (* we pass a dummy type [arity] as argument *)
	     | Tprop -> (Miniml.Tprop :: args, vl)
	     | Tmltype (mla,vl') -> (mla :: args, vl'))
      (List.combine sign_args args) 
      ([],vl)
  in
  (* The type variable list is [vl'] plus those variables of [c] not 
     corresponding to arguments. There is [nvlargs] such variables of [c] *)
  let nvlargs = List.length vlc - List.length mlargs in 
  assert (nvlargs >= 0);
  let vl'' = 
    List.fold_right 
      (fun id l -> (next_ident_away id (prop_name::l)) :: l) 
      (list_firstn nvlargs vlc) vl'
  in
  (* We complete the list of arguments of [c] by variables *)
  let vlargs = 
    List.rev_map (fun i -> Tvar i) (list_firstn nvlargs vl'') in
  Tmltype (Tapp ((Tglob r) :: mlargs @ vlargs), vl'')


(*s Signature of a type. *)

(* Precondition:  [c] is of type an arity. 
   This function is built on the [extract_type] model. *)

and signature env c =
  signature_rec env (whd_betaiotalet env none c) []

and signature_rec env c args = 
  match kind_of_term c with
    | Prod (n,t,d) 
    | Lambda (n,t,d) -> 
	let env' = push_rel_assum (n,t) env in
	(v_of_t env t) :: (signature_rec env' d [])
    | App (d, args') ->
	signature_rec env d (Array.to_list args' @ args)
    | Rel n -> 
	(match lookup_rel n env with
	   | (_,Some t,_) -> 
	       let c' = whd_betaiotalet env none (lift n t) in 
	       signature_rec env c' args
	   | _ -> [])
    | Const sp when args = [] && is_ml_extraction (ConstRef sp) -> []
    | Const sp when is_axiom sp -> []
    | Const sp ->
	let t = constant_type env sp in 
	if is_arity env none t then
	  (match extract_constant sp with 
	     | Emltype (Miniml.Tarity,_,_) -> []
	     | Emltype (Miniml.Tprop,_,_) -> []
	     | Emltype (_,sc,_) ->  
		 let d = List.length sc - List.length args in 
		 if d <= 0 then [] else list_lastn d sc
	     | Emlterm _ -> assert false) 
	else 
	  let cvalue = constant_value env sp in
	  let c' = whd_betaiotalet env none (applist (cvalue, args)) in
	  signature_rec env c' [] 
    | Ind spi ->
	(match extract_inductive spi with 
	   |Iml (si,_) -> 
	       let d = List.length si - List.length args in 
	       if d <= 0 then [] else list_lastn d si
	   |Iprop -> [])
    | Sort _ | Case _ | Fix _ | CoFix _ -> []
    | Cast (c, _) -> signature_rec env c args
    | Var _ -> section_message ()
    | _ -> assert false

(*s signature of a section path *)

and signature_of_sp sp typ = 
  try 
    Gmap.find sp !signature_table 
  with Not_found -> 
    let s = signature (Global.env()) typ in
    signature_table := Gmap.add sp s !signature_table; s 

(*s Extraction of a term. 
    Precondition: [c] has a type which is not an arity. 
    This is normaly checked in [extract_constr]. *)

and extract_term env ctx c = 
  extract_term_wt env ctx c (type_of env c)

(* Same, but With Type (wt). *)

and extract_term_wt env ctx c t =
  let s = sort_of env t in
  (* The only non-informative case: [s] is [Prop] *)
  if (s = InProp) then
    Rprop
  else 
    Rmlterm (extract_term_info_wt env ctx c t)

(* Variants with a stronger precondition: [c] is informative. 
   We directly return a [ml_ast], not a [term_extraction_result] *)

and extract_term_info env ctx c = 
  extract_term_info_wt env ctx c (type_of env c)

(* Same, but With Type (wt). *)

and extract_term_info_wt env ctx c t = 
   match kind_of_term c with
     | Lambda (n, t, d) ->
	 let v = v_of_t env t in 
	 let id = id_of_name n in 
	 let id = if id=prop_name then anonymous else id in 
	 let env' = push_rel_assum (Name id,t) env in
	 let ctx' = (snd v = NotArity) :: ctx in
	 let d' = extract_term_info env' ctx' d in
	 (* If [d] was of type an arity, [c] too would be so *)
	 (match v with
	    | _,Arity -> d'
            | Logic,NotArity -> MLlam (prop_name, d')
            | Info,NotArity -> MLlam (id, d'))
     | LetIn (n, c1, t1, c2) ->
	 let v = v_of_t env t1 in
	 let id = id_of_name n in 
	 let id = if id=prop_name then anonymous else id in 
	 let env' = push_rel (Name id,Some c1,t1) env in
	 (match v with
	    | (Info, NotArity) -> 
		let c1' = extract_term_info_wt env ctx c1 t1 in
		let c2' = extract_term_info env' (true :: ctx) c2 in
		(* If [c2] was of type an arity, [c] too would be so *)
		MLletin (id,c1',c2')
	    | _ -> extract_term_info env' (false :: ctx) c2)
     | Rel n ->
	 MLrel (renum_db ctx n)
     | Const sp ->
	 abstract_const sp (signature_of_sp sp t)
     | App (f,a) ->
      	 extract_app env ctx f a 
     | Construct cp ->
	 abstract_constructor cp (signature_of_constructor cp)
     | Case ({ci_ind=ip},_,c,br) ->
	 extract_case env ctx ip c br
     | Fix ((_,i),recd) -> 
	 extract_fix env ctx i recd
     | CoFix (i,recd) -> 
	 extract_fix env ctx i recd  
     | Cast (c, _) ->
	 extract_term_info_wt env ctx c t
     | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ ->
	 assert false 
     | Var _ -> section_message ()

(*s Abstraction of an inductive constructor: 
   \begin{itemize}
   \item In ML, contructor arguments are uncurryfied. 
   \item We managed to suppress logical parts inside inductive definitions,
   but they must appears outside (for partial applications for instance)
   \item We also suppressed all Coq parameters to the inductives, since
   they are fixed, and thus are not used for the computation.
   \end{itemize}

   The following code deals with those 3 questions: from constructor [C], it 
   produces: 

   [fun ]$p_1 \ldots p_n ~ x_1 \ldots x_n $[-> C(]$x_{i_1},\ldots, x_{i_k}$[)].
   This ML term will be reduced later on when applied, see [mlutil.ml].

   In the special case of a informative singleton inductive, [C] is identity *)

and abstract_constructor cp (s,n) =
  let f = if is_singleton_constructor cp then 
    function [x] -> x | _ -> assert false
  else
    fun a -> MLcons (ConstructRef cp, a)
  in anonym_lams (ml_lift n (prop_abstract_1 f s)) n

(* Extraction of a case *)

and extract_case env ctx ip c br = 
  let ni = mis_constr_nargs ip in
  (* [ni]: number of arguments without parameters in each branch *)
  (* [br]: bodies of each branch (in functional form) *)
  let extract_branch j b = 	  
    let cp = (ip,succ j) in
    let (s,_) = signature_of_constructor cp in
    assert (List.length s = ni.(j));
    let (rb,e) = decompose_lam_eta ni.(j) env b in
    let lb = List.rev rb in
    (* We suppose that [sign_of_lbinders env lb] gives back [s] *) 
    (* So we trust [s] when making [ctx'] *)
    let ctx' = List.fold_left (fun l v -> (v = default)::l) ctx s in 
    (* Some pathological cases need an [extract_constr] here rather *)
    (* than an [extract_term]. See exemples in [test_extraction.v] *)
    let env' = push_rel_context (List.map (fun (x,t) -> (x,None,t)) rb) env in
    let e' = extract_constr_to_term env' ctx' e in
    let ids = 
      List.fold_right 
	(fun (v,(n,_)) a -> if v = default then (id_of_name n :: a) else a)
	(List.combine s lb) []
    in
    (ConstructRef cp, ids, e')
  in
  if br = [||] then 
    MLexn "absurd case"
  else 
    (* [c] has an inductive type, not an arity type *)
    match extract_term env ctx c with
      | Rmlterm a when is_singleton_inductive ip -> 
          (* Informative singleton case: *)
          (* [match c with C i -> t] becomes [let i = c' in t'] *)
          assert (Array.length br = 1);
          let (_,ids,e') = extract_branch 0 br.(0) in
          assert (List.length ids = 1);
          MLletin (List.hd ids,a,e')
      | Rmlterm a -> 
          (* Standard case: we apply [extract_branch]. *)
          MLcase (a, Array.mapi extract_branch br)
      | Rprop -> 
	  (* Logical singleton case: *)
	  (* [match c with C i j k -> t] becomes [t'] *)
	  assert (Array.length br = 1);
	  let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in
	  let env' = push_rels_assum rb env in 
	  (* We know that all arguments are logic. *)
	  let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in 
	  extract_constr_to_term env' ctx' e
	    
  
(* Extraction of a (co)-fixpoint *)

and extract_fix env ctx i (fi,ti,ci as recd) = 
  let n = Array.length ti in
  let ti' = Array.mapi lift ti in 
  let lb = Array.to_list (array_map2 (fun a b -> (a,b)) fi ti') in
  let env' = push_rels_assum (List.rev lb) env in
  let ctx' = 
    (List.rev_map (fun (_,a) -> a = NotArity) (sign_of_lbinders env lb)) @ ctx
  in
  let extract_fix_body c t = 
    extract_constr_to_term_wt env' ctx' c (lift n t) in
  let ei = array_map2 extract_fix_body ci ti in
  MLfix (i, Array.map id_of_name fi, ei)

(* Auxiliary function dealing with term application. 
   Precondition: the head [f] is [Info]. *)

and extract_app env ctx f args =
  let tyf = type_of env f in
  let nargs = Array.length args in
  let sf = signature_of_application env f tyf args in  
  assert (List.length sf >= nargs); 
  (* Cf. postcondition of [signature_of_application]. *)
  let args = Array.to_list args in 
  let mlargs = 
    List.fold_right 
      (fun (v,a) args -> match v with
	 | (_,Arity) -> args
	 | (Logic,NotArity) -> MLprop :: args
	 | (Info,NotArity) -> 
	     (* We can't trust tag [default], so we use [extract_constr]. *)
	     (extract_constr_to_term env ctx a) :: args)
      (List.combine (list_firstn nargs sf) args)
      []
  in
  (* [f : arity] implies [(f args):arity], that can't be *)
  let f' = extract_term_info_wt env ctx f tyf in 
  MLapp (f', mlargs)

(* [signature_of_application] is used to generate a long enough signature.
   Precondition: the head [f] is [Info].
   Postcondition: the returned signature is longer than the arguments *)
    
and signature_of_application env f t a =
  let nargs = Array.length a in	 	
  let t = force_n_prod nargs env t in 
  (* It does not really ensure that [t] start by [n] products, 
     but it reduces as much as possible *)
  let nbp = nb_prod t in
  let s = signature env t in
  if nbp >= nargs then 
    s
  else 
    (* This case can really occur. Cf [test_extraction.v]. *)
    let f' = mkApp (f, Array.sub a 0 nbp) in 
    let a' = Array.sub a nbp (nargs-nbp) in 
    let t' = type_of env f' in
    s @ signature_of_application env f' t' a'


(*s Extraction of a constr seen as a term. *)

and extract_constr_to_term env ctx c =
  extract_constr_to_term_wt env ctx c (type_of env c)

(* Same, but With Type (wt). *)

and extract_constr_to_term_wt env ctx c t = 
  match v_of_t env t with
    | (_, Arity) -> MLarity 
    | (Logic, NotArity) -> MLprop
    | (Info, NotArity) -> extract_term_info_wt env ctx c t

(* Extraction of a constr. *)

and extract_constr env c = 
  extract_constr_wt env c (type_of env c)

(* Same, but With Type (wt). *)

and extract_constr_wt env c t =
  match v_of_t env t with
    | (Logic, Arity) -> Emltype (Miniml.Tarity, [], [])
    | (Logic, NotArity) -> Emlterm MLprop
    | (Info, Arity) -> 
	(match extract_type env c with
	   | Tprop -> Emltype (Miniml.Tprop, [], [])
	   | Tarity -> Emltype (Miniml.Tarity, [], [])
	   | Tmltype (t, vl) -> Emltype (t, (signature env c), vl))
    | (Info, NotArity) -> 
	Emlterm (extract_term_info_wt env [] c t)
	  
(*s Extraction of a constant. *)
		
and extract_constant sp =
  try
    Gmap.find sp !constant_table
  with Not_found ->
    let env = Global.env() in    
    let cb = Global.lookup_constant sp in
    let typ = cb.const_type in
    match cb.const_body with
      | None ->
          (match v_of_t env typ with
             | (Info,_) -> axiom_message sp (* We really need some code here *)
             | (Logic,NotArity) -> Emlterm MLprop (* Axiom? I don't mind! *)
             | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[]))  (* Idem *)
      | Some body ->
	  let e = match extract_constr_wt env body typ with 
	    | Emlterm MLprop as e -> e
	    | Emlterm MLarity as e -> e
	    | Emlterm a -> 
		Emlterm (eta_expanse_w_prop a (signature_of_sp sp typ))
	    | e -> e 
	  in constant_table := Gmap.add sp e !constant_table;
          e

(*s Extraction of an inductive. *)
    
and extract_inductive ((sp,_) as i) =
  extract_mib sp;
  lookup_inductive_extraction i
			     
and extract_constructor (((sp,_),_) as c) =
  extract_mib sp;
  lookup_constructor_extraction c

and signature_of_constructor cp = match extract_constructor cp with
  | Cprop -> assert false
  | Cml (_,s,n) -> (s,n)

(* Looking for informative singleton case, i.e. an inductive with one 
   constructor which has one informative argument. This dummy case will 
   be simplified. *)
 
and is_singleton_inductive ind = 
  let (mib,mip) = Global.lookup_inductive ind in 
  mib.mind_finite &&
  (mib.mind_ntypes = 1) &&
  (Array.length mip.mind_consnames = 1) && 
  match extract_constructor (ind,1) with 
    | Cml ([mlt],_,_)-> not (type_mem_sp (fst ind) mlt)
    | _ -> false
          
and is_singleton_constructor ((sp,i),_) = 
  is_singleton_inductive (sp,i) 

and extract_mib sp =
  let ind = (sp,0) in
  if not (Gmap.mem ind !inductive_extraction_table) then begin
    let (mib,mip) = Global.lookup_inductive ind in
    let genv = Global.env () in 
    (* Everything concerning parameters. 
       We do that first, since they are common to all the [mib]. *)
    let nb = mip.mind_nparams in
    let rb = mip.mind_params_ctxt in 
    let env = push_rel_context rb genv in
    let lb = List.rev_map (fun (n,s,t)->(n,t)) rb in 
    let nbtokeep = 
      lbinders_fold 
	(fun _ _ (_,j) a -> if j = NotArity then a+1 else a) 0 genv lb in
    let vl = vl_of_lbinders genv lb in
    (* First pass: we store inductive signatures together with 
       an initial type var list. *)
    let vl0 = iterate_for 0 (mib.mind_ntypes - 1)
	(fun i vl -> 
	   let ip = (sp,i) in 
	   let (mib,mip) = Global.lookup_inductive ip in 
	   if mip.mind_sort = (Prop Null) then begin
	     add_inductive_extraction ip Iprop; vl
	   end else begin
	     let arity = mip.mind_nf_arity in
	     let vla = List.rev (vl_of_arity genv arity) in 
	     add_inductive_extraction ip 
	       (Iml (sign_of_arity genv arity, vla));
	     vla @ vl 
	   end
	) []
    in
    (* Second pass: we extract constructors arities and we accumulate
       type variables. Thanks to on-the-fly renaming in [extract_type],
       the [vl] list should be correct. *)
    let vl = 
      iterate_for 0 (mib.mind_ntypes - 1)
	(fun i vl -> 
	   let ip = (sp,i) in
           let (mib,mip) = Global.lookup_inductive ip in
	   if mip.mind_sort = Prop Null then begin
	     for j = 1 to Array.length mip.mind_consnames do
	       add_constructor_extraction (ip,j) Cprop
	     done;
	     vl
	   end else 
	     iterate_for 1 (Array.length mip.mind_consnames)
	       (fun j vl -> 
		  let t = type_of_constructor genv (ip,j) in
		  let t = snd (decompose_prod_n nb t) in
		  match extract_type_rec_info env t vl [] with
		    | Tarity | Tprop -> assert false
		    | Tmltype (mlt, v) -> 
			let l = list_of_ml_arrows mlt
			and s = signature env t in 
			add_constructor_extraction (ip,j) (Cml (l,s,nbtokeep));
			v)
	       vl)
	vl0
    in
    let vl = list_firstn (List.length vl - List.length vl0) vl in
    (* Third pass: we update the type variables list in the inductives table *)
    for i = 0 to mib.mind_ntypes-1 do 
      let ip = (sp,i) in 
      match lookup_inductive_extraction ip with 
	| Iprop -> ()
	| Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l));
    done;
    (* Fourth pass: we also update the constructors table *)
    for i = 0 to mib.mind_ntypes-1 do 
      let ip = (sp,i) in 
      for j = 1 to Array.length mib.mind_packets.(i).mind_consnames do
	let cp = (ip,j) in 
	match lookup_constructor_extraction cp  with 
	  | Cprop -> ()
	  | Cml (t,s,n) -> 
	      let vl = List.rev_map (fun i -> Tvar i) vl in
	      let t' = List.map (update_args sp vl) t in 
	      add_constructor_extraction cp (Cml (t',s, n))
      done
    done
  end	      

and extract_inductive_declaration sp =
  extract_mib sp;
  let ip = (sp,0) in 
  if is_singleton_inductive ip then
    let t = match lookup_constructor_extraction (ip,1) with 
      | Cml ([t],_,_)-> t
      | _ -> assert false
    in
    let vl = match lookup_inductive_extraction ip with 
       | Iml (_,vl) -> vl
       | _ -> assert false
     in 
    Dabbrev (IndRef ip,vl,t)
  else
    let mib = Global.lookup_mind sp in
    let one_ind ip n = 
      iterate_for (-n) (-1)
	(fun j l -> 
	   let cp = (ip,-j) in 
	   match lookup_constructor_extraction cp with 
	     | Cprop -> assert false
	     | Cml (t,_,_) -> (ConstructRef cp, t)::l) []
    in
    let l = 
      iterate_for (1 - mib.mind_ntypes) 0
	(fun i acc -> 
	   let ip = (sp,-i) in
	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
	   match lookup_inductive_extraction ip with
	     | Iprop -> acc
	     | Iml (_,vl) -> 
		 (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
	[] 
    in
    Dtype (l, not mib.mind_finite)
      
(*s Extraction of a global reference i.e. a constant or an inductive. *)

let extract_declaration r = match r with
  | ConstRef sp -> 
      (match extract_constant sp with
	 | Emltype (mlt, s, vl) -> Dabbrev (r, List.rev vl, mlt)
	 | Emlterm t -> Dglob (r, t))
  | IndRef (sp,_) -> extract_inductive_declaration sp
  | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
  | VarRef _ -> assert false

(*s Check if a global reference corresponds to a logical inductive. *)

let decl_is_logical_ind = function 
  | IndRef ip -> extract_inductive ip = Iprop 
  | ConstructRef cp -> extract_constructor cp  = Cprop
  | _ -> false

(*s Check if a global reference corresponds to the constructor of 
  a singleton inductive. *)

let decl_is_singleton = function 
  | ConstructRef cp -> is_singleton_constructor cp 
  | _ -> false