diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/extract_env.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 16 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 27 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 5 |
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 *) |