aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml18
-rw-r--r--plugins/extraction/common.mli2
-rw-r--r--plugins/extraction/extract_env.ml9
-rw-r--r--plugins/extraction/extraction.ml33
-rw-r--r--plugins/extraction/extraction_plugin.mlpack (renamed from plugins/extraction/extraction_plugin.mllib)1
-rw-r--r--plugins/extraction/g_extraction.ml43
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/json.ml3
-rw-r--r--plugins/extraction/modutil.ml4
-rw-r--r--plugins/extraction/ocaml.ml93
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/extraction/table.ml134
-rw-r--r--plugins/extraction/table.mli3
13 files changed, 148 insertions, 159 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 3c5f6cb720..de97ba97c3 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -145,7 +145,7 @@ type env = Id.t list * Id.Set.t
(*s Generic renaming issues for local variable names. *)
let rec rename_id id avoid =
- if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
+ if Id.Set.mem id avoid then rename_id (increment_subscript id) avoid else id
let rec rename_vars avoid = function
| [] ->
@@ -308,15 +308,16 @@ end
module DupMap = Map.Make(DupOrd)
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
let index = ref 0 and dups = ref DupMap.empty in
register_cleanup (fun () -> index := 0; dups := DupMap.empty);
let add mp l =
incr index;
let ren = "Coq__" ^ string_of_int !index in
dups := DupMap.add (mp,l) ren !dups
- and check mp l = DupMap.find (mp, l) !dups
- in (add,check)
+ and get mp l =
+ try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+ in (add,get)
type reset_kind = AllButExternal | Everything
@@ -510,10 +511,11 @@ let pp_duplicate k' prefix mp rls olab =
(* Here rls=s::rls', we search the label for s inside mp *)
List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
in
- try dottify (check_duplicate prefix lbl :: rls')
- with Not_found ->
- assert (get_phase () == Pre); (* otherwise it's too late *)
- add_duplicate prefix lbl; dottify rls
+ match get_duplicate prefix lbl with
+ | Some ren -> dottify (ren :: rls')
+ | None ->
+ assert (get_phase () == Pre); (* otherwise it's too late *)
+ add_duplicate prefix lbl; dottify rls
let fstlev_ks k = function
| [] -> assert false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 2f5601964e..b8e95afb38 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path
val push_visible : module_path -> module_path list -> unit
val pop_visible : unit -> unit
-val check_duplicate : module_path -> Label.t -> string
+val get_duplicate : module_path -> Label.t -> string option
type reset_kind = AllButExternal | Everything
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a03be5743f..e019bb3c2a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -13,7 +13,7 @@ open Names
open Libnames
open Globnames
open Pp
-open Errors
+open CErrors
open Util
open Table
open Extraction
@@ -507,8 +507,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
in
(* First, a dry run, for computing objects to rename or duplicate *)
set_phase Pre;
- let devnull = formatter true None in
- pp_with devnull (d.pp_struct struc);
+ ignore (d.pp_struct struc);
let opened = opened_libraries () in
(* Print the implementation *)
let cout = if dry then None else Option.map open_out fn in
@@ -583,8 +582,8 @@ let rec locate_ref = function
| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
| Some mp, Some r ->
- warning_both_mod_and_cst q mp r;
- let refs,mps = locate_ref l in refs,mp::mps
+ warning_ambiguous_name (q,mp,r);
+ let refs,mps = locate_ref l in refs,mp::mps
(*s Recursive extraction in the Coq toplevel. The vernacular command is
\verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e40621965f..2b19c2805f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -36,7 +36,7 @@ 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
+ [SingletonInductiveBecomeProp]. This exception will be caught
in late wrappers around the exported functions of this file,
in order to display the location of the issue. *)
@@ -74,7 +74,7 @@ type flag = info * scheme
Really important function. *)
let rec flag_of_type env t : flag =
- let t = whd_betadeltaiota env none t in
+ let t = whd_all env none t in
match kind_of_term t with
| Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
| Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
@@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with
(*s [type_sign] gernerates a signature aimed at treating a type application. *)
let rec type_sign env c =
- match kind_of_term (whd_betadeltaiota env none c) with
+ match kind_of_term (whd_all env none c) with
| Prod (n,t,d) ->
(if is_info_scheme env t then Keep else Kill Kprop)
:: (type_sign (push_rel_assum (n,t) env) d)
| _ -> []
let rec type_scheme_nb_args env c =
- match kind_of_term (whd_betadeltaiota env none c) with
+ match kind_of_term (whd_all env none c) with
| Prod (n,t,d) ->
let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
if is_info_scheme env t then n+1 else n
@@ -135,7 +135,7 @@ let make_typvar n vl =
next_ident_away id' vl
let rec type_sign_vl env c =
- match kind_of_term (whd_betadeltaiota env none c) with
+ match kind_of_term (whd_all env none c) with
| Prod (n,t,d) ->
let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -143,7 +143,7 @@ let rec type_sign_vl env c =
| _ -> [],[]
let rec nb_default_params env c =
- match kind_of_term (whd_betadeltaiota env none c) with
+ match kind_of_term (whd_all env none c) with
| Prod (n,t,d) ->
let n = nb_default_params (push_rel_assum (n,t) env) d in
if is_default env t then n+1 else n
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
| Const (kn,u as c) ->
let r = ConstRef kn in
let cb = lookup_constant kn env in
- let typ,_ = Typeops.type_of_constant env c in
+ let typ = Typeops.type_of_constant_in env c in
(match flag_of_type env typ with
| (Logic,_) -> assert false (* Cf. logical cases above *)
| (Info, TypeScheme) ->
@@ -371,8 +371,7 @@ and extract_really_ind env kn mib =
let packets =
Array.mapi
(fun i mip ->
- let (ind,u), ctx =
- Universes.fresh_inductive_instance env (kn,i) in
+ let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
let ar = Inductive.type_of_inductive env ((mib,mip),u) in
let info = (fst (flag_of_type env ar) = Info) in
let s,v = if info then type_sign_vl env ar else [],[] in
@@ -489,7 +488,7 @@ and extract_really_ind env kn mib =
*)
and extract_type_cons env db dbmap c i =
- match kind_of_term (whd_betadeltaiota env none c) with
+ match kind_of_term (whd_all env none c) with
| Prod (n,t,d) ->
let env' = push_rel_assum (n,t) env in
let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
@@ -591,10 +590,10 @@ let rec extract_term env mle mlt c args =
with NotDefault d ->
let mle' = Mlenv.push_std_type mle (Tdummy d) in
ast_pop (extract_term env' mle' mlt c2 args'))
- | Const (kn,u) ->
- extract_cst_app env mle mlt kn u args
- | Construct (cp,u) ->
- extract_cons_app env mle mlt cp u args
+ | Const (kn,_) ->
+ extract_cst_app env mle mlt kn args
+ | Construct (cp,_) ->
+ extract_cons_app env mle mlt cp args
| Proj (p, c) ->
let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
extract_term env mle mlt term args
@@ -645,7 +644,7 @@ and make_mlargs env e s args typs =
(*s Extraction of a constant applied to arguments. *)
-and extract_cst_app env mle mlt kn u args =
+and extract_cst_app env mle mlt kn args =
(* First, the [ml_schema] of the constant, in expanded version. *)
let nb,t = record_constant_type env kn None in
let schema = nb, expand env t in
@@ -684,7 +683,7 @@ and extract_cst_app env mle mlt kn u args =
let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
else mla
- with e when Errors.noncritical e -> mla
+ with e when CErrors.noncritical e -> mla
in
(* For strict languages, purely logical signatures lead to a dummy lam
(except when [Kill Ktype] everywhere). So a [MLdummy] is left
@@ -718,7 +717,7 @@ and extract_cst_app env mle mlt kn u args =
they are fixed, and thus are not used for the computation.
\end{itemize} *)
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
(* First, we build the type of the constructor, stored in small pieces. *)
let mi = extract_ind env kn in
let params_nb = mi.ind_nparams in
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack
index ad32124347..9184f65017 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mlpack
@@ -9,4 +9,3 @@ Scheme
Json
Extract_env
G_extraction
-Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 0a8cb0ccd3..e1d6bb4a84 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,11 +8,12 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+DECLARE PLUGIN "extraction_plugin"
+
(* ML names *)
open Genarg
open Stdarg
-open Constrarg
open Pcoq.Prim
open Pp
open Names
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 764223621e..0692c88cd1 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -9,7 +9,7 @@
(*s Production of Haskell syntax. *)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 8874afef33..e43c47d050 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -142,7 +142,8 @@ let rec json_expr env = function
("what", json_str "fix:item");
("name", json_id fi);
("body", json_function env' ti)
- ]) (Array.map2 (fun a b -> a,b) ids' defs)))
+ ]) (Array.map2 (fun a b -> a,b) ids' defs)));
+ ("for", json_int i);
]
| MLexn s -> json_dict [
("what", json_str "expr:exception");
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index bd48311308..60fe8e7620 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -8,7 +8,7 @@
open Names
open Globnames
-open Errors
+open CErrors
open Util
open Miniml
open Table
@@ -310,7 +310,7 @@ let base_r = function
let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
let needed = ref Refset'.empty
and needed_mps = ref MPset.empty in
- ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty),
+ ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty),
(fun r -> needed := Refset'.add (base_r r) !needed),
(fun mp -> needed_mps := MPset.add mp !needed_mps),
(fun r -> needed := Refset'.remove (base_r r) !needed),
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3cb3810cbc..d89bf95ee8 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -9,7 +9,7 @@
(*s Production of Ocaml syntax. *)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -203,7 +203,7 @@ let rec pp_expr par env args =
let args = List.skipn (projection_arity r) args in
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
- with e when Errors.noncritical e -> apply (pp_global Term r))
+ with e when CErrors.noncritical e -> apply (pp_global Term r))
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -555,24 +555,6 @@ let pp_decl = function
| Dfix (rv,defs,typs) ->
pp_Dfix (rv,defs,typs)
-let pp_alias_decl ren = function
- | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
- | Dtype (r, l, _) ->
- let name = pp_global Type r in
- let l = rename_tvars keywords l in
- let ids = pp_parameters l in
- hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
- str (ren^".") ++ name)
- | Dterm (r, a, t) ->
- let name = pp_global Term r in
- hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
- | Dfix (rv, _, _) ->
- prvecti (fun i r -> if is_inline_custom r then mt () else
- let name = pp_global Term r in
- hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
- fnl ())
- rv
-
let pp_spec = function
| Sval (r,_) when is_inline_custom r -> mt ()
| Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,42 +579,32 @@ let pp_spec = function
in
hov 2 (str "type " ++ ids ++ name ++ def)
-let pp_alias_spec ren = function
- | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
- | Stype (r,l,_) ->
- let name = pp_global Type r in
- let l = rename_tvars keywords l in
- let ids = pp_parameters l in
- hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
- str (ren^".") ++ name)
- | Sval _ -> assert false
-
let rec pp_specif = function
| (_,Spec (Sval _ as s)) -> pp_spec s
| (l,Spec s) ->
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> pp_spec s
+ | Some ren ->
hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
fnl () ++ str "end" ++ fnl () ++
- pp_alias_spec ren s
- with Not_found -> pp_spec s)
+ str ("include module type of struct include "^ren^" end"))
| (l,Smodule mt) ->
let def = pp_module_type [] mt in
- let def' = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
- with Not_found -> Pp.mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> Pp.mt ()
+ | Some ren ->
+ fnl () ++
+ hov 1 (str ("module "^ren^" :") ++ spc () ++
+ str "module type of struct include " ++ name ++ str " end"))
| (l,Smodtype mt) ->
let def = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module type "^ren^" = ") ++ name
- with Not_found -> Pp.mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> Pp.mt ()
+ | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_type params = function
| MTident kn ->
@@ -653,8 +625,10 @@ and pp_module_type params = function
let l = List.rev l in
pop_visible ();
str "sig" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
- fnl () ++ str "end"
+ (if List.is_empty l then mt ()
+ else
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+ ++ str "end"
| MTwith(mt,ML_With_type(idl,vl,typ)) ->
let ids = pp_parameters (rename_tvars keywords vl) in
let mp_mt = msid_of_mt mt in
@@ -681,12 +655,11 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false
let rec pp_structure_elem = function
| (l,SEdecl d) ->
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> pp_decl d
+ | Some ren ->
hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
- fnl () ++ str "end" ++ fnl () ++
- pp_alias_decl ren d
- with Not_found -> pp_decl d)
+ fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
| (l,SEmodule m) ->
let typ =
(* virtual printing of the type, in order to have a correct mli later*)
@@ -699,18 +672,16 @@ let rec pp_structure_elem = function
hov 1
(str "module " ++ name ++ typ ++ str " =" ++
(if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module "^ren^" = ") ++ name
- with Not_found -> mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+ | None -> mt ())
| (l,SEmodtype m) ->
let def = pp_module_type [] m in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module type "^ren^" = ") ++ name
- with Not_found -> mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> mt ()
+ | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_expr params = function
| MEident mp -> pp_modname mp
@@ -732,8 +703,10 @@ and pp_module_expr params = function
let l = List.rev l in
pop_visible ();
str "struct" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
- fnl () ++ str "end"
+ (if List.is_empty l then mt ()
+ else
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+ ++ str "end"
let rec prlist_sep_nonempty sep f = function
| [] -> mt ()
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 7b0f14dff7..a6309e61f9 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -9,7 +9,7 @@
(*s Production of Scheme syntax. *)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Miniml
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 560fe5aea8..5e7d810c93 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -15,7 +15,7 @@ open Libobject
open Goptions
open Libnames
open Globnames
-open Errors
+open CErrors
open Util
open Pp
open Miniml
@@ -293,83 +293,96 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
(*S Warning and Error messages. *)
-let err s = errorlabstrm "Extraction" s
+let err s = user_err ~hdr:"Extraction" s
+
+let warn_extraction_axiom_to_realize =
+ CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction"
+ (fun axioms ->
+ let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in
+ strbrk ("The following "^s^" must be realized in the extracted code:")
+ ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms)
+ ++ str "." ++ fnl ())
+
+let warn_extraction_logical_axiom =
+ CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction"
+ (fun axioms ->
+ let s =
+ if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were"
+ in
+ (strbrk ("The following logical "^s^" encountered:") ++
+ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n")
+ ++ strbrk "Having invalid logical axiom in the environment when extracting"
+ ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++
+ fnl ()))
let warning_axioms () =
let info_axioms = Refset'.elements !info_axioms in
- if List.is_empty info_axioms then ()
- else begin
- let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
- Feedback.msg_warning
- (str ("The following "^s^" must be realized in the extracted code:")
- ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
- ++ str "." ++ fnl ())
- end;
+ if not (List.is_empty info_axioms) then
+ warn_extraction_axiom_to_realize info_axioms;
let log_axioms = Refset'.elements !log_axioms in
- if List.is_empty log_axioms then ()
- else begin
- let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
- in
- Feedback.msg_warning
- (str ("The following logical "^s^" encountered:") ++
- hov 1
- (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
- ++
- str "Having invalid logical axiom in the environment when extracting" ++
- spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
- fnl ())
- end
+ if not (List.is_empty log_axioms) then
+ warn_extraction_logical_axiom log_axioms
+
+let warn_extraction_opaque_accessed =
+ CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction"
+ (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++
+ strbrk "the following opaque constant bodies have been accessed :" ++
+ lst ++ str "." ++ fnl ())
+
+let warn_extraction_opaque_as_axiom =
+ CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction"
+ (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++
+ strbrk "the following opaque constants have been extracted as axioms :" ++
+ lst ++ str "." ++ fnl () ++
+ strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+ ++ fnl ())
let warning_opaques accessed =
let opaques = Refset'.elements !opaques in
- if List.is_empty opaques then ()
- else
+ if not (List.is_empty opaques) then
let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
- if accessed then
- Feedback.msg_warning
- (str "The extraction is currently set to bypass opacity,\n" ++
- str "the following opaque constant bodies have been accessed :" ++
- lst ++ str "." ++ fnl ())
- else
- Feedback.msg_warning
- (str "The extraction now honors the opacity constraints by default,\n" ++
- str "the following opaque constants have been extracted as axioms :" ++
- lst ++ str "." ++ fnl () ++
- str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
- ++ fnl ())
-
-let warning_both_mod_and_cst q mp r =
- Feedback.msg_warning
- (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
- str "do you mean module " ++
- pr_long_mp mp ++
- str " or object " ++
- pr_long_global r ++ str " ?" ++ fnl () ++
- str "First choice is assumed, for the second one please use " ++
- str "fully qualified name." ++ fnl ())
+ if accessed then warn_extraction_opaque_accessed lst
+ else warn_extraction_opaque_as_axiom lst
+
+let warning_ambiguous_name =
+ CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction"
+ (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++
+ strbrk "do you mean module " ++
+ pr_long_mp mp ++
+ strbrk " or object " ++
+ pr_long_global r ++ str " ?" ++ fnl () ++
+ strbrk "First choice is assumed, for the second one please use " ++
+ strbrk "fully qualified name." ++ fnl ())
let error_axiom_scheme r i =
err (str "The type scheme axiom " ++ spc () ++
safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
str " type variable(s).")
+let warn_extraction_inside_module =
+ CWarnings.create ~name:"extraction-inside-module" ~category:"extraction"
+ (fun () -> strbrk "Extraction inside an opened module is experimental." ++
+ strbrk "In case of problem, close it first.")
+
+
let check_inside_module () =
if Lib.is_modtype () then
err (str "You can't do that within a Module Type." ++ fnl () ++
str "Close it and try again.")
else if Lib.is_module () then
- Feedback.msg_warning
- (str "Extraction inside an opened module is experimental.\n" ++
- str "In case of problem, close it first.\n")
+ warn_extraction_inside_module ()
let check_inside_section () =
if Lib.sections_are_opened () then
err (str "You can't do that within a section." ++ fnl () ++
str "Close it and try again.")
-let warning_id s =
- Feedback.msg_warning (str ("The identifier "^s^
- " contains __ which is reserved for the extraction"))
+let warn_extraction_reserved_identifier =
+ CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction"
+ (fun s -> strbrk ("The identifier "^s^
+ " contains __ which is reserved for the extraction"))
+
+let warning_id s = warn_extraction_reserved_identifier s
let error_constant r =
err (safe_pr_global r ++ str " is not a constant.")
@@ -428,7 +441,7 @@ let error_MPfile_as_mod mp b =
let argnames_of_global r =
let typ = Global.type_of_global_unsafe r in
let rels,_ =
- decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
+ decompose_prod (Reduction.whd_all (Global.env ()) typ) in
List.rev_map fst rels
let msg_of_implicit = function
@@ -447,12 +460,15 @@ let error_remaining_implicit k =
str "You might also try Unset Extraction SafeImplicits to force" ++
fnl() ++ str "the extraction of unsafe code and review it manually.")
+let warn_extraction_remaining_implicit =
+ CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction"
+ (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
+ strbrk "Extraction SafeImplicits is unset, extracting nonetheless,"
+ ++ strbrk "but this code is potentially unsafe, please review it manually.")
+
let warning_remaining_implicit k =
let s = msg_of_implicit k in
- Feedback.msg_warning
- (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
- str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl ()
- ++ str "but this code is potentially unsafe, please review it manually.")
+ warn_extraction_remaining_implicit s
let check_loaded_modfile mp = match base_mp mp with
| MPfile dp ->
@@ -864,7 +880,7 @@ let extract_constant_inline inline r ids s =
| ConstRef kn ->
let env = Global.env () in
let typ = Global.type_of_global_unsafe (ConstRef kn) in
- let typ = Reduction.whd_betadeltaiota env typ in
+ let typ = Reduction.whd_all env typ in
if Reduction.is_arity env typ
then begin
let nargs = Hook.get use_type_scheme_nb_args env typ in
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 62c20bd3a7..15a08756c0 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t
val warning_axioms : unit -> unit
val warning_opaques : bool -> unit
-val warning_both_mod_and_cst :
- qualid -> module_path -> global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit
val warning_id : string -> unit
val error_axiom_scheme : global_reference -> int -> 'a
val error_constant : global_reference -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 19:04:20 +0000