Refonte complete de la génération des types ML

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 261 insertions, 390 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index cfd4e33faa..ad0f6053df 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -31,7 +31,7 @@ open Nametab
 
 (*S Extraction results. *)
 
-(* The flag [type_var] gives us information about an identifier
+(* The type [flag] 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],
@@ -50,59 +50,43 @@ 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)
+type flag = info * arity
 
 (* 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 *)
+(* Convention: outmost lambda/product gives the head of the list, 
+   and [true] means that the argument is to be kept. *)
 
-type signature = type_var list
+type signature = 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 dummy type, denoting either: 
-   \begin{itemize} 
-   \item a CIC arity, without counterpart in ML
-   \item a non-informative type, which will receive special treatment
-   \end{itemize}
-   \end{itemize} *)
+(* The [extraction_result] is the result of the [extract_constr]
+   function that extracts any CIC object. It is either a ML type or 
+   a ML object. An ML type contains also a signature (saying how to 
+   translate its coq arity into a ML arity) and a type variable list. *)
 
-type type_extraction_result =
-  | Tmltype of ml_type * identifier list
-  | Tdum
+type extraction_result =
+  | Emltype of ml_type * signature * identifier list
+  | Emlterm of ml_ast
 
-(* The [indutive_extraction_result] is the dual of [type_extraction_result], 
-   but for inductive types. *)
+(* The [indutive_extraction_result] is used to save the extraction of 
+   an inductive type. It tells whether this inductive is informative 
+   or not, and in the informative case, stores a signature and a type 
+   variable list. *)
 
 type inductive_extraction_result = 
   | Iml of signature * identifier list
   | Iprop
 
-(* For an informative constructor, the [constructor_extraction_result] contains
-   the list of the types of its arguments, a signature, and the number of 
-   parameters to discard. *)
+(* For an informative constructor, the [constructor_extraction_result] 
+   contains the list of the types of its arguments, a signature, and 
+   the number of parameters to discard. *)
 
 type constructor_extraction_result = 
   | Cml of ml_type list * signature * int
   | Cprop
 
-(* The [extraction_result] is the result of the [extract_constr]
-   function that extracts any CIC object. It is either a ML type or 
-   a ML object. *)
-
-type extraction_result =
-  | Emltype of ml_type * signature * identifier list
-  | Emlterm of ml_ast
-
 (*S Tables to keep the extraction results. *)
 
 let inductive_table = 
@@ -139,7 +123,18 @@ let _ = declare_summary "Extraction tables"
 	    init_function = (fun () -> ());
 	    survive_section = true }
 
-(*S Utility functions. *)
+(*S Error messages. *)
+
+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 Generation of flags and signatures. *)
 
 let none = Evd.empty
 
@@ -149,71 +144,74 @@ let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
 let is_axiom sp = (Global.lookup_constant sp).const_body = None
 
-type lamprod = Lam | Product
-
-let dummy_arrow = function 
-  | Tmltype (mld,vl) -> Tmltype (Tarr (Tdummy, mld), vl)
-  | Tdum -> Tdum
-
-(*s [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] and [arity] parts. *)
+(* TODO: Could we export the one inside reductionops *)
 
-let rec list_of_ml_arrows = function
-  | Tarr (Tdummy, 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
-    | Sort s -> Some (family_of_sort s)
-    | _ -> None
-
-(*s [v_of_t] transforms a type [t] into a [type_var] flag. 
+let rec find_conclusion env c =
+  let t = whd_betadeltaiota env none c in
+  match kind_of_term t with
+    | Prod (x,t,c0) -> find_conclusion (push_rel (x,None,t) env) c0
+    | t -> t
+	  
+(*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
 
-let v_of_t env t = match get_arity env t with
-  | Some InProp -> logic_arity
-  | Some _ -> info_arity
-  | None when (sort_of env t) = InProp -> logic
-  | None -> default
+let flag_of_type env t = match find_conclusion env t with
+  | Sort (Prop Null) -> (Logic,Arity)
+  | Sort _ -> (Info,Arity)
+  | _ -> if (sort_of env t) = InProp then (Logic,NotArity)
+    else (Info,NotArity)
 
-(*S Operations on binders. *)
+(*s [is_default] is a particular case of the last function. *)
 
-type binders = (name * constr) list
+let is_default env t = 
+  not (is_arity env none t) && (sort_of env t) <> InProp
 
-(* Convention: right binders give [Rel 1] at the head, like those answered by 
-   [decompose_prod]. Left binders are the converse, like [signature]. *)
+(*s [term_sign] gernerates a signature aimed at treating a term 
+  application at the ML term level. *)
 
-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)
+let rec term_sign env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) -> 
+	(is_default env t) :: (term_sign (push_rel_assum (n,t) env) d)
+    | _ -> []
 
-(*s [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. *)
+(*s [type_sign] gernerates a signature aimed at treating a term 
+  application at the ML type level. It also produce a type var list. *)
 
-let sign_of_lbinders = lbinders_fold (fun _ _ v a -> v::a) [] 
+let rec type_sign env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) -> 
+	let s,vl = type_sign (push_rel_assum (n,t) env) d in 
+	let b = flag_of_type env t = (Info,Arity) in
+	let vl = if not b then vl
+	else (next_ident_away (id_of_name n) vl) :: vl 
+	in b::s, vl
+    | Sort _ -> [],[]
+    | _ -> assert false
 
-let sign_of_arity env c = 
-  sign_of_lbinders env (List.rev (fst (decompose_prod c)))
+(*s [app_sign] is used to generate a long enough signature.
+   Precondition: the head [f] is [Info].
+   Postcondition: the output signature is at least as long as the arguments. *)
+    
+let rec app_sign env f t a =
+  let s = term_sign env t in
+  let na = Array.length a in	
+  let ns = List.length s in 
+  if ns >= na then s
+  else 
+    (* This case can really occur. Cf [test_extraction.v]. *)
+    let f' = mkApp (f, Array.sub a 0 ns) in 
+    let a' = Array.sub a ns (na-ns) in 
+    s @ app_sign env f' (type_of env f') a'
+  
+(*s Function recording signatures of section paths. *)
 
-(*s [vl_of_arity] returns the list of the lambda variables tagged [info_arity]
-   in an arity. Renaming is done. *)
+let signature_of_sp sp typ = 
+  try lookup_signature sp
+  with Not_found -> 
+    let s = term_sign (Global.env()) typ in 
+    add_signature sp s; s
 
-let vl_of_lbinders = 
-  let f n _ v a = if v <> info_arity then a 
-  else (next_ident_away (id_of_name n) a) :: a
-  in lbinders_fold f [] 
-  
-let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c)))
-	 
 (*S Modification of the signature of terms. *)
 
 (* We sometimes want to suppress [prop] and [arity] in the signature 
@@ -233,8 +231,8 @@ let expansion_prop_eta s (ids,c) =
     | [] -> 
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
 	in ids, MLapp (ml_lift (i-1) c, a) 
-    | (Info,NotArity) :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
-    | _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
+    | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
+    | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
   in abs ids [] 1 s
 
 let kill_all_prop_lams_eta e s = 
@@ -242,7 +240,7 @@ let kill_all_prop_lams_eta e s =
   let n = nb_lams e in 
   let p = if m <= n then collect_n_lams m e 
   else expansion_prop_eta (snd (list_chop n s)) (collect_lams e) in 
-  kill_some_lams (List.rev_map ((=) default) s) p
+  kill_some_lams (List.rev s) p
 
 let kill_prop_lams_eta e s =
   if s = [] then e 
@@ -256,230 +254,156 @@ let kill_prop_lams_eta e s =
 let prop_abstract f  = 
   let rec abs rels i = function 
     | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels)
-    | ((_,Arity)|(Logic,_)) :: l -> MLlam (dummy_name, abs rels (succ i) l)
-    | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
+    | true :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
+    | false :: l -> MLlam (dummy_name, abs rels (succ i) l)
   in abs [] 1  
 
 (*s Abstraction of an constant. *)
 
 let abstract_constant sp s = 
-  if List.for_all ((=) default) s then MLglob (ConstRef sp) 
-  else 
+  if List.mem false s then  
     let f a = 
-      if List.mem default s then MLapp (MLglob (ConstRef sp), a)
+      if List.mem true s then MLapp (MLglob (ConstRef sp), a)
       else MLapp (MLglob (ConstRef sp), [MLdummy])
     in prop_abstract f s
-
-(*S Error messages. *)
-
-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.")
+  else MLglob (ConstRef sp) 
+
+(*S Management of type variable contexts. *)
+
+(*s From a signature toward a type variable context (ctx). *)
+
+let ctx_from_sign s = 
+  let rec make i = function 
+    | [] -> [] 
+    | true :: l -> i :: (make (i+1) l)
+    | false :: l -> 0 :: (make i l)
+  in make 1 (List.rev s)
+
+(*s Create a type variable context from indications taken from 
+  an inductive type (see just below). *) 
+
+let ctx_from_ind rels n d = 
+  let rec make i = 
+    if i > n then [] 
+    else try 
+      (Intmap.find (i+d) rels) :: (make (i+1))
+    with Not_found -> 0 :: (make (i+1))
+  in make 1
+
+(*s [parse_ind_args] is the function used for generating ad-hoc
+  translation of de Bruijn indices for extraction of inductive type. *)
+
+let parse_ind_args si args = 
+  let rec parse i k = function 
+    | [] -> Intmap.empty
+    | false :: s -> parse (i-1) k s
+    | true :: s -> 
+      (match kind_of_term args.(i) with 
+	 | Rel j -> Intmap.add j k (parse (i-1) (k+1) s)
+	 | _ -> parse (i-1) (k+1) s)
+  in parse ((Array.length args)-1) 1 (List.rev si) 
 
 (*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]. *)
+(*s [extract_type env c args ctx] is used to produce an ML type from the 
+   coq term [(c args)], which is supposed to be a Coq type on an informative 
+   sort. *)
 
-(* 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 = Tdum], then [v_of_t env t = _,Arity]
-   or [Logic,NotArity].
-   \end{itemize} *)
+(* [ctx] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-(* 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 -> Tdum 
-    | Some _ -> extract_type_rec_info env c vl args
-	  
-and extract_type_rec_info env c vl args = 
-  match (kind_of_term (whd_betaiotazeta c)) with
+let rec extract_type env c args ctx = 
+  match kind_of_term (whd_betaiotazeta c) with
     | Sort _ ->
-	assert (args = []); (* A sort can't be applied. *)
-	Tdum 
+	Tdummy 
     | 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
+	let mld = extract_type (push_rel_assum (n,t) env) d [] (0::ctx) in 
+	if mld = Tdummy then Tdummy 
+	else if not (is_default env t) then Tarr (Tdummy, mld)
+	else Tarr (extract_type env t [] ctx, mld)
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
-	extract_type_rec_info env d vl (Array.to_list args' @ args)
+	extract_type env d (Array.to_list args' @ args) ctx
     | 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)
+	   | (_,Some t,_) -> 
+	       extract_type env (lift n t) args ctx
+	   | _ -> 
+	       let n' = List.nth ctx (n-1) in 
+	       if n' = 0 then Tunknown else Tvar n')
+    | Const sp when is_ml_extraction (ConstRef sp) ->
+	Tglob (ConstRef sp)
     | Const sp when is_axiom sp -> 
-	let id = next_ident_away (basename sp) (dummy_name::vl) in 
-	Tmltype (Tvar id,  id :: vl)
+	Tunknown
     | Const sp ->
 	let t = constant_type env sp in 
 	if is_arity env none t then
-	  (match extract_constant sp with 
-	     | Emltype (Tdummy,_,_) -> Tdum
-	     | Emltype (_, sc, vlc) ->  
-		 extract_type_app env (ConstRef sp,sc,vlc) vl args 
-	     | Emlterm _ -> assert false) 
+	  match extract_constant sp with 
+	    | Emltype (mlt, sc, _) -> 
+		if mlt = Tdummy then Tdummy
+		else extract_type_app env (ConstRef sp,sc) args ctx
+	    | Emlterm _ -> assert false
 	else 
-	  (* We can't keep as ML type abbreviation a CIC constant *)
+	  (* We can't keep as ML type abbreviation a Coq 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 []
+	  extract_type env (applist (cvalue, args)) [] ctx
     | 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 flex_name (dummy_name::vl) in
-	Tmltype (Tvar id,  id :: vl)
-	  (* Type without counterpart in ML: we generate a 
-	     new flexible type variable. *) 
+	   | Iml (si,vli) -> extract_type_app env (IndRef spi,si) args ctx
+	   | Iprop -> assert false (* Cf. initial tests *))
+    | Case _ | Fix _ | CoFix _ -> Tunknown
     | Var _ -> section_message ()
     | _ -> assert false
 
-(*s 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), Lam -> 
-	(* 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) vl in 
-	let env' = push_rel_assum (Name id', t) env in
-	extract_type_rec_info env' d (id'::vl) []
-    | _, Lam ->
-	extract_type_rec_info  env' d vl []
-    | (Info, Arity), Product -> 
-	(* 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) vl in 
-	let env' = push_rel_assum (Name id', t) env in
-	dummy_arrow (extract_type_rec_info env' d (id'::vl) [])
-    | (Logic,_), Product -> 
-	dummy_arrow (extract_type_rec_info env' d vl [])
-    | (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
-		  | Tdum -> assert false 
-			(* Cf. relation between [extract_type] and [v_of_t] *)
-		  | Tmltype (mlt,vl'') -> Tmltype (Tarr(mlt,mld), vl''))
-	   | et -> et)
-	
 (*s Auxiliary function dealing with type application. 
-  Precondition: [r] is of type an arity. *)
+  Precondition: [r] is of type an arity represented by the signature [s], 
+  and is completely applied: [List.length args = List.length s]. *)
 		  
-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
-	     | Tdum -> (Tdummy :: args, vl) 
-  	           (* we pass a dummy type [arity] as argument *)
-	     | 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'' = 
+and extract_type_app env (r,s) args ctx =
+  let ml_args = 
     List.fold_right 
-      (fun id l -> (next_ident_away id (dummy_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. *)
+      (fun (b,t) a -> if b then (extract_type env t [] ctx) :: a else a)
+      (List.combine s args) []
+  in Tapp ((Tglob r) :: ml_args)
 
-(* Precondition:  [c] is of type an arity. 
-   This function is built on the [extract_type] model. *)
+(*s [extract_type_arity env c ctx p] works on a Coq term [c] whose type 
+  is an informative arity. It means that [c] is not a Coq type, but will 
+  be when applied to sufficiently many arguments ([p] in fact).  
+  This function decomposes p lambdas, with eta-expansion if needed. *)
 
-and signature env c =
-  signature_rec env c []
+(* [ctx] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-and signature_rec env c args = 
-  match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) 
-    | Lambda (n,t,d) -> 
+and extract_type_arity env c ctx p = 
+  if p=0 then extract_type env c [] ctx 
+  else 
+    let c = whd_betaiotazeta c in 
+    match kind_of_term c with 
+      | Lambda (n,t,d) -> 
+	  extract_type_arity (push_rel_assum (n,t) env) d ctx (p-1)
+      | _ ->  
+	  let rels = fst (splay_prod env none (type_of env c)) in
+	  let env = push_rels_assum rels env in  
+	  let eta_args = List.rev_map mkRel (interval 1 p) in 
+	  extract_type env (lift p c) eta_args ctx
+
+(*s [extract_type_ind] extracts the type of an informative inductive 
+  constructor toward the corresponding list of ML types. *)
+
+(* [p] is the number of product in [c] and [ctx] is a context for 
+  translating Coq [Rel] into ML type [Tvar] and [db] is a translation 
+  map (produced by a call to [parse_in_args]). *)
+
+and extract_type_ind env c ctx db p = 
+  match kind_of_term (whd_betadeltaiota env none c) with 
+    | Prod (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,_) -> signature_rec env (lift n t) args
-	   | _ -> [])
-    | 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 _ -> []
-    | Const sp -> assert (is_axiom sp); [] 
-    | Var _ -> section_message ()
-    | _ -> assert false
-
-(*s signature of a section path *)
-
-and signature_of_sp sp typ = 
-  try lookup_signature sp
-  with Not_found -> 
-    let s = signature (Global.env()) typ in 
-    add_signature sp s; s
+	let ctx' = (try Intmap.find p db with Not_found -> 0) :: ctx in
+	let l = extract_type_ind env' d ctx' db (p-1) in 
+	if is_default env t then
+	  let mlt = extract_type env t [] ctx in 
+	  if mlt = Tdummy then l else mlt :: l 
+	else l 
+    | _ -> [] 
 
 (*S Extraction of a term. *)
 
@@ -497,13 +421,13 @@ and extract_term_wt env c t =
 	 let id = id_of_name n in 
 	 (* If [d] was of type an arity, [c] too would be so *)
 	 let d' = extract_term (push_rel_assum (Name id,t) env) d in
-	 if (v_of_t env t) = default then MLlam (id, d')
+	 if is_default env t then MLlam (id, d')
 	 else MLlam (dummy_name, d')
      | LetIn (n, c1, t1, c2) ->
 	 let id = id_of_name n in 
 	 (* If [c2] was of type an arity, [c] too would be so *)
 	 let c2' = extract_term (push_rel (Name id,Some c1,t1) env) c2 in
-	 if (v_of_t env t1) = default then 
+	 if is_default env t1 then 
 	   let c1' = extract_term_wt env c1 t1 in 
 	   MLletin (id,c1',c2')
 	 else MLletin (dummy_name, MLdummy, c2')
@@ -558,13 +482,12 @@ and extract_case env ip c br =
     (* than an [extract_term]. See exemples in [test_extraction.v] *)
     let e = extract_constr_to_term env b in 
     let cp = (ip,succ j) in
-    let (s,_) = signature_of_constructor cp in
+    let s = fst (signature_of_constructor cp) in
     assert (List.length s = ni.(j));
     let ids,e = kill_all_prop_lams_eta e s in
     (ConstructRef cp, List.rev ids, e)
   in
-  if br = [||] then 
-    MLexn "absurd case"
+  if br = [||] then MLexn "absurd case"
   else 
     (* [c] has an inductive type, not an arity type. *)
     let t = type_of env c in 
@@ -575,7 +498,7 @@ and extract_case env ip c br =
 	(* [match c with C i j k -> t] becomes [t'] *)
 	assert (Array.length br = 1);
 	let e = extract_constr_to_term env br.(0) in 
-	let s = iterate (fun l -> logic :: l) ni.(0) [] in
+	let s = iterate (fun l -> false :: l) ni.(0) [] in
 	snd (kill_all_prop_lams_eta e s)
       end 
     else 
@@ -611,40 +534,17 @@ and extract_fix env i (fi,ti,ci as recd) =
 and extract_app env 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  
+  let sf = app_sign 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) -> MLdummy :: args
-	 | (Logic,NotArity) -> MLdummy :: args
-	 | (Info,NotArity) -> 
-	     (* We can't trust tag [default], so we use [extract_constr]. *)
-	     (extract_constr_to_term env a) :: args)
-      (List.combine (list_firstn nargs sf) args)
-      []
+    List.map 
+      (* We can't trust tag [default], so we use [extract_constr]. *)
+      (fun (b,a) -> if b then extract_constr_to_term env a else MLdummy)
+      (List.combine (list_firstn nargs sf) (Array.to_list args))
   in
   (* [f : arity] implies [(f args):arity], that can't be *)
-  let f' = extract_term_wt env f tyf in 
-  MLapp (f', mlargs)
-
-(*s [signature_of_application] is used to generate a long enough signature.
-   Precondition: the head [f] is [Info].
-   Postcondition: the output signature is at least as long as the arguments. *)
-    
-and signature_of_application env f t a =
-  let s = signature env t in
-  let nargs = Array.length a in	
-  let ns = List.length s in 
-  if ns >= nargs then s
-  else 
-    (* This case can really occur. Cf [test_extraction.v]. *)
-    let f' = mkApp (f, Array.sub a 0 ns) in 
-    let a' = Array.sub a ns (nargs-ns) in 
-    let t' = type_of env f' in
-    s @ signature_of_application env f' t' a'
+  MLapp (extract_term_wt env f tyf, mlargs)
 
 (*s Extraction of a constr seen as a term. *)
 
@@ -654,10 +554,7 @@ and extract_constr_to_term env c =
 (* Same, but With Type (wt). *)
 
 and extract_constr_to_term_wt env c t = 
-  match v_of_t env t with
-    | (_, Arity) -> MLdummy 
-    | (Logic, NotArity) -> MLdummy
-    | (Info, NotArity) -> extract_term_wt env c t
+  if is_default env t then extract_term_wt env c t else MLdummy
 
 (*S Extraction of a constr. *)
 
@@ -667,15 +564,15 @@ and extract_constr env c =
 (* Same, but With Type (wt). *)
 
 and extract_constr_wt env c t =
-  match v_of_t env t with
+  match flag_of_type env t with
     | (Logic, Arity) -> Emltype (Tdummy, [], [])
-    | (Logic, NotArity) -> Emlterm MLdummy
     | (Info, Arity) -> 
-	(match extract_type env c with
-	   | Tdum -> Emltype (Tdummy, [], [])
-	   | Tmltype (t, vl) -> Emltype (t, (signature env c), vl))
-    | (Info, NotArity) -> 
-	Emlterm (extract_term_wt env c t)
+	let s,vl = type_sign env t in 
+	let ctx = ctx_from_sign s in 
+	let mlt = extract_type_arity env c ctx (List.length s) in 
+	Emltype (mlt, s, vl)
+    | (Logic, NotArity) -> Emlterm MLdummy
+    | (Info, NotArity) -> Emlterm (extract_term_wt env c t)
 	  
 (*S Extraction of a constant. *)
 		
@@ -687,7 +584,7 @@ and extract_constant sp =
     let typ = cb.const_type in
     match cb.const_body with
       | None ->
-          (match v_of_t env typ with
+          (match flag_of_type env typ with
              | (Info,_) -> axiom_message sp (* We really need some code here *)
              | (Logic,NotArity) -> Emlterm MLdummy (* Axiom? I don't mind! *)
              | (Logic,Arity) -> Emltype (Tdummy,[],[]))  (* Idem *)
@@ -739,70 +636,45 @@ and extract_mib sp =
     let params_nb = mip.mind_nparams in
     let params_env = push_rel_context mip.mind_params_ctxt env 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 ip Iprop; vl
-	   end else begin
-	     let arity = mip.mind_nf_arity in
-	     let vla = List.rev (vl_of_arity env arity) in 
-	     add_inductive ip 
-	       (Iml (sign_of_arity env 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 (ip,j) Cprop
-	     done;
-	     vl
-	   end else 
-	     iterate_for 1 (Array.length mip.mind_consnames)
-	       (fun j vl -> 
-		  let t = type_of_constructor env (ip,j) in
-		  let t = snd (decompose_prod_n params_nb t) in
-		  match extract_type_rec_info params_env t vl [] with
-		    | Tdum -> assert false
-		    | Tmltype (mlt, v) -> 
-			let l = list_of_ml_arrows mlt
-			and s = signature params_env t in 
-			add_constructor (ip,j) (Cml (l,s,params_nb));
-			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 
+    (* their type var list. *)
+    for i = 0 to mib.mind_ntypes - 1 do
       let ip = (sp,i) in 
-      match lookup_inductive ip with 
-	| Iprop -> ()
-	| Iml (s,l) -> add_inductive ip (Iml (s,vl@l));
+      let (mib,mip) = Global.lookup_inductive ip in 
+      if mip.mind_sort = (Prop Null) then 
+	add_inductive ip Iprop
+      else
+	let arity = mip.mind_nf_arity in
+	let s,vl = type_sign env arity in 
+	add_inductive ip (Iml (s,vl))
     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 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 cp (Cml (t',s, n))
-      done
+    (* Second pass: we extract constructors *)
+    for i = 0 to mib.mind_ntypes - 1 do
+      let ip = (sp,i) in
+      let (mib,mip) = Global.lookup_inductive ip in
+      match lookup_inductive ip with 
+	| Iprop -> 
+	    for j = 1 to Array.length mip.mind_consnames do
+	      add_constructor (ip,j) Cprop
+	    done
+	| Iml (si,_) ->  
+	    for j = 1 to Array.length mip.mind_consnames do 
+	      let cp = (ip,j) in 
+	      let t = type_of_constructor env cp in
+	      let t = snd (decompose_prod_n params_nb t) in
+	      let s = term_sign params_env t in
+	      let n = List.length s in 
+	      let db,ctx = 
+		if si=[] then Intmap.empty,[]
+		else match find_conclusion params_env t with 
+		  | App (f, args) -> 
+		      (*i assert (kind_of_term f = Ind ip); i*)
+		      let db = parse_ind_args si args in 
+		      db, ctx_from_ind db params_nb n 
+		  | _ -> assert false 
+	      in 
+	      let l = extract_type_ind params_env t ctx db n in	      
+	      add_constructor cp (Cml (l,s,params_nb))
+	    done
     done
   end	      
 
@@ -836,8 +708,7 @@ and extract_inductive_declaration sp =
 	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
 	   match lookup_inductive ip with
 	     | Iprop -> acc
-	     | Iml (_,vl) -> 
-		 (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
+	     | Iml (_,vl) -> (vl, IndRef ip, one_ind ip nc) :: acc)
 	[] 
     in
     Dtype (l, not mib.mind_finite)
@@ -849,7 +720,7 @@ and extract_inductive_declaration sp =
 let extract_declaration r = match r with
   | ConstRef sp -> 
       (match extract_constant sp with
-	 | Emltype (mlt, s, vl) -> Dabbrev (r, List.rev vl, mlt)
+	 | Emltype (mlt, s, vl) -> Dabbrev (r, vl, mlt)
 	 | Emlterm t -> Dglob (r, t))
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp