Extraction: a warning when an opaque constant is enterred

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

5 files changed, 51 insertions, 5 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index cb873f2e5..04d1f2a8d 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -513,6 +513,7 @@ let full_extr f (refs,mps) =
   init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
   let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  warning_opaques ();
   warning_axioms ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
@@ -526,6 +527,7 @@ let separate_extraction lr =
   init true false;
   let refs,mps = locate_ref lr in
   let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  warning_opaques ();
   warning_axioms ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
@@ -544,6 +546,7 @@ let simple_extraction r = match locate_ref [r] with
       init false false;
       let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
+      warning_opaques ();
       warning_axioms ();
       if is_custom r then msgnl (str "(** User defined extraction *)");
       print_one_decl struc (modpath_of_r r) d;
@@ -570,6 +573,7 @@ let extraction_library is_rec m =
   in
   let struc = List.fold_left select [] l in
   let struc = optimize_struct ([],[]) struc in
+  warning_opaques ();
   warning_axioms ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5131704a7..450aa8710 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -904,16 +904,24 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 let extract_constant env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
+  let warn_info_none () =
+    if not (is_custom r) then begin
+      add_info_axiom r;
+      if not !Flags.load_proofs && cb.const_opaque then add_opaque_ko r
+    end
+  in
+  let warn_info_some () = if cb.const_opaque then add_opaque_ok r
+  in
   match cb.const_body with
-    | None -> (* A logical axiom is risky, an informative one is fatal. *)
+    | None ->
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) ->
-	       if not (is_custom r) then add_info_axiom r;
+	       warn_info_none ();
 	       let n = type_scheme_nb_args env typ in
 	       let ids = iterate (fun l -> anonymous_name::l) n [] in
 	       Dtype (r, ids, Taxiom)
            | (Info,Default) ->
-	       if not (is_custom r) then add_info_axiom r;
+	       warn_info_none ();
 	       let t = snd (record_constant_type env kn (Some typ)) in
 	       Dterm (r, MLaxiom, type_expunge env t)
            | (Logic,TypeScheme) ->
@@ -925,9 +933,11 @@ let extract_constant env kn cb =
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
 	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
 	   | (Info, Default) ->
+	       warn_info_some ();
 	       let e,t = extract_std_constant env kn (force body) typ in
 	       Dterm (r,e,t)
 	   | (Info, TypeScheme) ->
+	       warn_info_some ();
 	       let s,vl = type_sign_vl env typ in
                let db = db_from_sign s in
                let t = extract_type_scheme env db (force body) (List.length s)
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 21dfee666..027b24787 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -332,7 +332,9 @@ let rec depcheck_se = function
     let refs = declared_refs d in
     let refs' = List.filter is_needed refs in
     if refs' = [] then
-      (List.iter remove_info_axiom refs; se')
+      (List.iter remove_info_axiom refs;
+       List.iter remove_opaque refs;
+       se')
     else begin
       List.iter found_needed refs';
       (* Hack to avoid extracting unused part of a Dfix *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6d4f06e14..8c9fdf37d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,6 +175,15 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
 let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
+let opaques_ok = ref Refset'.empty
+let opaques_ko = ref Refset'.empty
+let init_opaques () = opaques_ok := Refset'.empty; opaques_ko := Refset'.empty
+let add_opaque_ok r = opaques_ok := Refset'.add r !opaques_ok
+let add_opaque_ko r = opaques_ko := Refset'.add r !opaques_ko
+let remove_opaque r =
+  opaques_ok := Refset'.remove r !opaques_ok;
+  opaques_ko := Refset'.remove r !opaques_ko
+
 (*s Extraction modes: modular or monolithic, library or minimal ?
 
 Nota:
@@ -256,6 +265,22 @@ let warning_axioms () =
        fnl ())
   end
 
+let warning_opaques () =
+  let opaques_ok = Refset'.elements !opaques_ok in
+  if opaques_ok = [] then ()
+  else msg_warning
+    (str "Extraction is accessing the body of the following opaque constants:"
+     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ok)
+     ++ str "." ++ fnl ()
+     ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ());
+  let opaques_ko = Refset'.elements !opaques_ko in
+  if opaques_ko = [] then ()
+  else msg_warning
+    (str "Extraction cannot access the body of the following opaque constants:"
+     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ko)
+     ++ fnl () ++ str "due to option -dont-load-proofs. "
+     ++ str "These constants are treated as axioms." ++ fnl ())
+
 let warning_both_mod_and_cst q mp r =
  msg_warning
    (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
@@ -778,4 +803,4 @@ let extract_inductive r s l optstr =
 
 let reset_tables () =
   init_terms (); init_types (); init_inductives (); init_recursors ();
-  init_projs (); init_axioms (); reset_modfile ()
+  init_projs (); init_axioms (); init_opaques (); reset_modfile ()
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 8c009c662..158e33ec9 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -19,6 +19,7 @@ val safe_basename_of_global : global_reference -> identifier
 (*s Warning and Error messages. *)
 
 val warning_axioms : unit -> unit
+val warning_opaques : unit -> unit
 val warning_both_mod_and_cst :
  qualid -> module_path -> global_reference -> unit
 val warning_id : string -> unit
@@ -83,6 +84,10 @@ val add_info_axiom : global_reference -> unit
 val remove_info_axiom : global_reference -> unit
 val add_log_axiom : global_reference -> unit
 
+val add_opaque_ok : global_reference -> unit
+val add_opaque_ko : global_reference -> unit
+val remove_opaque : global_reference -> unit
+
 val reset_tables : unit -> unit
 
 (*s AutoInline parameter *)