aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-07 15:37:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-07 15:37:59 +0000
commit0a2738fe2e171cc6661824cd6525ee5d5c317334 (patch)
tree41c4eaff941fa572f46236197e087037cb0c158e /plugins/extraction
parent654f4e0f4dfae3073f8af5ccf54636f927191276 (diff)
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
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml4
-rw-r--r--plugins/extraction/extraction.ml16
-rw-r--r--plugins/extraction/modutil.ml4
-rw-r--r--plugins/extraction/table.ml27
-rw-r--r--plugins/extraction/table.mli5
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 *)