1 files changed, 75 insertions, 44 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 10644da2..a980a43f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Environ
@@ -26,6 +25,7 @@ open Globnames
 open Miniml
 open Table
 open Mlutil
+open Context.Rel.Declaration
 (*i*)
 
 exception I of inductive_kind
@@ -35,17 +35,18 @@ let current_fixpoints = ref ([] : constant list)
 
 let none = Evd.empty
 
+(* NB: In OCaml, [type_of] and [get_of] might raise
+   [SingletonInductiveBecomeProp]. This exception will be caught
+   in late wrappers around the exported functions of this file,
+   in order to display the location of the issue. *)
+
 let type_of env c =
-  try
-    let polyprop = (lang() == Haskell) in
-    Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
-  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
+  let polyprop = (lang() == Haskell) in
+  Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
 
 let sort_of env c =
-  try
-    let polyprop = (lang() == Haskell) in
-    Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
-  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
+  let polyprop = (lang() == Haskell) in
+  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
 
 (*S Generation of flags and signatures. *)
 
@@ -73,9 +74,9 @@ type flag = info * scheme
   Really important function. *)
 
 let rec flag_of_type env t : flag =
-  let t = whd_betadeltaiota env none t in
+  let t = whd_all env none t in
   match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
+    | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
@@ -101,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -134,7 +135,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -142,7 +143,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -248,7 +249,7 @@ let rec extract_type env db j c args =
     | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
     | Rel n ->
 	(match lookup_rel n env with
-           | (_,Some t,_) -> extract_type env db j (lift n t) args
+           | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
 	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
@@ -285,7 +286,7 @@ let rec extract_type env db j c args =
     | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
-    | Case _ | Fix _ | CoFix _ -> Tunknown
+    | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown
     | _ -> assert false
 
 (*s Auxiliary function dealing with type application.
@@ -328,11 +329,22 @@ and extract_type_scheme env db c p =
 
 (*S Extraction of an inductive type. *)
 
+(* First, a version with cache *)
+
 and extract_ind env kn = (* kn is supposed to be in long form *)
   let mib = Environ.lookup_mind kn env in
   match lookup_ind kn mib with
   | Some ml_ind -> ml_ind
   | None ->
+     try
+       extract_really_ind env kn mib
+     with SingletonInductiveBecomesProp id ->
+       (* TODO : which inductive is concerned in the block ? *)
+       error_singleton_become_prop id (Some (IndRef (kn,0)))
+
+(* Then the real function *)
+
+and extract_really_ind env kn mib =
     (* First, if this inductive is aliased via a Module,
        we process the original inductive if possible.
        When at toplevel of the monolithic case, we cannot do much
@@ -359,8 +371,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     let packets =
       Array.mapi
 	(fun i mip ->
-	   let (ind,u), ctx = 
-	     Universes.fresh_inductive_instance env (kn,i) in
+	   let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
 	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
 	   let info = (fst (flag_of_type env ar) = Info) in
 	   let s,v = if info then type_sign_vl env ar else [],[] in
@@ -477,7 +488,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
@@ -561,7 +572,7 @@ let rec extract_term env mle mlt c args =
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
-	let env' = push_rel (Name id, Some c1, t1) env in
+	let env' = push_rel (LocalDef (Name id, c1, t1)) env in
 	(* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
@@ -579,10 +590,10 @@ let rec extract_term env mle mlt c args =
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const (kn,u) ->
-	extract_cst_app env mle mlt kn u args
-    | Construct (cp,u) ->
-	extract_cons_app env mle mlt cp u args
+    | Const (kn,_) ->
+	extract_cst_app env mle mlt kn args
+    | Construct (cp,_) ->
+	extract_cons_app env mle mlt cp args
     | Proj (p, c) ->
         let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
 	  extract_term env mle mlt term args
@@ -633,7 +644,7 @@ and make_mlargs env e s args typs =
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn u args =
+and extract_cst_app env mle mlt kn args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
   let nb,t = record_constant_type env kn None in
   let schema = nb, expand env t in
@@ -672,7 +683,7 @@ and extract_cst_app env mle mlt kn u args =
 	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
 	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
-      with e when Errors.noncritical e -> mla
+      with e when CErrors.noncritical e -> mla
   in
   (* For strict languages, purely logical signatures lead to a dummy lam
      (except when [Kill Ktype] everywhere). So a [MLdummy] is left
@@ -706,7 +717,7 @@ and extract_cst_app env mle mlt kn u args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   (* First, we build the type of the constructor, stored in small pieces. *)
   let mi = extract_ind env kn in
   let params_nb = mi.ind_nparams in
@@ -836,7 +847,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 
 let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in
+  let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
@@ -934,11 +945,13 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env ti.(i) != InProp then begin
-      let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
-      terms.(i) <- e;
-      types.(i) <- t;
-    end
+    if sort_of env ti.(i) != InProp then
+      try
+        let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
+        terms.(i) <- e;
+        types.(i) <- t;
+      with SingletonInductiveBecomesProp id ->
+        error_singleton_become_prop id (Some (ConstRef vkn.(i)))
   done;
   current_fixpoints := [];
   Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
@@ -968,13 +981,17 @@ let extract_constant env kn cb =
     let e,t = extract_std_constant env kn c typ in
     Dterm (r,e,t)
   in
-  match flag_of_type env typ with
+  try
+    match flag_of_type env typ with
     | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
     | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_typ (Mod_subst.force_constr c)
+	      | Some pb -> mk_typ pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
@@ -983,17 +1000,23 @@ let extract_constant env kn cb =
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_def (Mod_subst.force_constr c)
+	      | Some pb -> mk_def pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
               mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c)
             else mk_ax ())
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id (Some (ConstRef kn))
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
-  match flag_of_type env typ with
+  try
+    match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kprop)
     | (Info, TypeScheme) ->
@@ -1008,26 +1031,34 @@ let extract_constant_spec env kn cb =
     | (Info, Default) ->
 	let t = snd (record_constant_type env kn (Some typ)) in
 	Sval (r, type_expunge env t)
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id (Some (ConstRef kn))
 
 let extract_with_type env c =
-  let typ = type_of env c in
-  match flag_of_type env typ with
+  try
+    let typ = type_of env c in
+    match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign s in
 	let t = extract_type_scheme env db c (List.length s) in
 	Some (vl, t)
     | _ -> None
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id None
 
 let extract_constr env c =
   reset_meta_count ();
-  let typ = type_of env c in
-  match flag_of_type env typ with
+  try
+    let typ = type_of env c in
+    match flag_of_type env typ with
     | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype
     | (Logic,_) -> MLdummy Kprop, Tdummy Kprop
     | (Info,Default) ->
-      let mlt = extract_type env [] 1 typ [] in
-      extract_term env Mlenv.empty mlt c [], mlt
+       let mlt = extract_type env [] 1 typ [] in
+       extract_term env Mlenv.empty mlt c [], mlt
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id None
 
 let extract_inductive env kn =
   let ind = extract_ind env kn in