Extraction with implicits: perform the occur-check after optimisations

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

6 files changed, 46 insertions, 27 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c11a8f1285..c0097d492a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -135,6 +135,17 @@ let sign_with_implicits r s =
   in
   add_impl 1 s
 
+(* Enriching a exception message *)
+
+let rec handle_exn r n fn_name = function
+  | MLexn s ->
+      (try Scanf.sscanf s "UNBOUND %d"
+	 (fun i ->
+	    assert ((0 < i) && (i <= n));
+	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
+       with _ -> MLexn s)
+  | a -> ast_map (handle_exn r n fn_name) a
+
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
@@ -761,13 +772,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
-	try
-	  let ids,e = case_expunge s e in
-	  (r, List.rev ids, e)
-	with Occurs i ->
-	  let n = List.length s in
-	  assert ((0<i) && (i <= n));
-	  error_non_implicit r (n-i+1) None
+	let ids,e = case_expunge s e in
+	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
+	(r, List.rev ids, e')
       in
       if mi.ind_info = Singleton then
 	begin
@@ -849,11 +856,10 @@ let extract_std_constant env kn body typ =
   (* The real extraction: *)
   let e = extract_term env mle t' c [] in
   (* Expunging term and type from dummy lambdas. *)
-  try
-    term_expunge s (ids,e), type_expunge_from_sign env s t
-  with Occurs i ->
-    assert ((0 < i) && (i <= n));
-    error_non_implicit (ConstRef kn) (n-i+1) (Some (fst (List.nth rels (i-1))))
+  let trm = term_expunge s (ids,e) in
+  let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm
+  in
+  trm, type_expunge_from_sign env s t
 
 let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 1cef86ee59..034baad955 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -497,8 +497,6 @@ let ast_subst e =
    [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies
    to [Rel] greater than [Array.length v]. *)
 
-exception Occurs of int
-
 let gen_subst v d t =
   let rec subst n = function
     | MLrel i as a ->
@@ -506,7 +504,7 @@ let gen_subst v d t =
 	if i' < 1 then a
 	else if i' <= Array.length v then
 	  match v.(i'-1) with
-	    | None -> raise (Occurs i')
+	    | None -> MLexn ("UNBOUND " ^ string_of_int i')
 	    | Some u -> ast_lift n u
 	else MLrel (i+d)
     | a -> ast_map_lift subst n a
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 7e9cfbeed1..3466f22d3a 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -112,8 +112,6 @@ val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
 
-exception Occurs of int
-
 (* Classification of signatures *)
 
 type sign_kind =
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 7e8127fb3e..4ed6e9a084 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -346,12 +346,24 @@ let rec depcheck_struct = function
       let lse' = depcheck_se lse in
       (mp,lse')::struc'
 
+let check_implicits = function
+  | MLexn s ->
+      if String.length s > 8 && (s.[0] = 'U' || s.[0] = 'I') then
+	begin
+	  if String.sub s 0 7 = "UNBOUND" then assert false;
+	  if String.sub s 0 8 = "IMPLICIT" then
+	    error_non_implicit (String.sub s 9 (String.length s - 9));
+	end;
+      false
+  | _ -> false
+
 let optimize_struct to_appear struc =
   let subst = ref (Refmap.empty : ml_ast Refmap.t) in
   let opt_struc =
     List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
   in
   let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
+  ignore (struct_ast_search check_implicits opt_struc);
   try
     if modular () then raise NoDepCheck;
     reset_needed ();
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index df61375c58..3cac73998d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -207,9 +207,11 @@ let safe_basename_of_global = function
       (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
-let safe_pr_global r =
- try Printer.pr_global r
- with _ -> pr_id (safe_basename_of_global r)
+let string_of_global r =
+ try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
+ with _ -> string_of_id (safe_basename_of_global r)
+
+let safe_pr_global r = str (string_of_global r)
 
 (* idem, but with qualification, and only for constants. *)
 
@@ -321,13 +323,15 @@ let error_record r =
   err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
        fnl () ++ str "To help extraction, please use an explicit name.")
 
-let error_non_implicit r n oid =
-  let name = match oid with
-    | None -> mt ()
-    | Some id -> str "(" ++ pr_name id ++ str ") "
+let msg_non_implicit r n id =
+  let name = match id with
+    | Anonymous -> ""
+    | Name id -> "(" ^ string_of_id id ^ ") "
   in
-  err (str ("The "^(ordinal n)^" argument ") ++ name ++ str "of " ++
-       safe_pr_global r ++ str " still occurs after extraction." ++
+  "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
+
+let error_non_implicit msg =
+  err (str (msg ^ " still occurs after extraction.") ++
        fnl () ++ str "Please check the Extraction Implicit declarations.")
 
 let check_loaded_modfile mp = match base_mp mp with
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 49108cf522..04d90b8815 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -31,7 +31,8 @@ val error_record : global_reference -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
-val error_non_implicit : global_reference -> int -> name option -> 'a
+val msg_non_implicit : global_reference -> int -> name -> string
+val error_non_implicit : string -> 'a
 
 val info_file : string -> unit