Extraction : add a location in the error message about polyprop

3 files changed, 56 insertions, 24 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index bdf01e73b..0ac8e3c4c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -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 catched
+   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. *)
 
@@ -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
@@ -934,11 +946,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,7 +982,8 @@ 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) ->
@@ -995,11 +1010,14 @@ let extract_constant env kn cb =
 	    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) ->
@@ -1014,26 +1032,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
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index d7842e127..5f83d2949 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -391,9 +391,15 @@ let error_no_module_expr mp =
        ++ str "some Declare Module outside any Module Type.\n"
        ++ str "This situation is currently unsupported by the extraction.")
 
-let error_singleton_become_prop id =
+let error_singleton_become_prop id og =
+  let loc =
+    match og with
+    | Some g -> fnl () ++ str "in " ++ safe_pr_global g ++
+                str " (or in its mutual block)"
+    | None -> mt ()
+  in
   err (str "The informative inductive type " ++ pr_id id ++
-       str " has a Prop instance.\n" ++
+       str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++
        str "This happens when a sort-polymorphic singleton inductive type\n" ++
        str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
        str "The Ocaml extraction cannot handle this situation yet.\n" ++
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 2b163610e..62c20bd3a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
-val error_singleton_become_prop : Id.t -> 'a
+val error_singleton_become_prop : Id.t -> global_reference option -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a