aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/Extraction.v0
-rw-r--r--plugins/extraction/common.ml37
-rw-r--r--plugins/extraction/common.mli3
-rw-r--r--plugins/extraction/extract_env.ml19
-rw-r--r--plugins/extraction/extract_env.mli1
-rw-r--r--plugins/extraction/extraction.ml46
-rw-r--r--plugins/extraction/extraction.mli1
-rw-r--r--plugins/extraction/g_extraction.ml46
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/json.ml1
-rw-r--r--plugins/extraction/miniml.mli1
-rw-r--r--plugins/extraction/mlutil.ml1
-rw-r--r--plugins/extraction/mlutil.mli1
-rw-r--r--plugins/extraction/modutil.ml5
-rw-r--r--plugins/extraction/modutil.mli1
-rw-r--r--plugins/extraction/ocaml.ml97
-rw-r--r--plugins/extraction/scheme.ml11
-rw-r--r--plugins/extraction/table.ml35
-rw-r--r--plugins/extraction/table.mli1
-rw-r--r--plugins/extraction/vo.itarget1
20 files changed, 140 insertions, 134 deletions
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
deleted file mode 100644
index e69de29bb2..0000000000
--- a/plugins/extraction/Extraction.v
+++ /dev/null
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 3c5f6cb720..9c3f97696f 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Pp
open Util
open Names
@@ -67,7 +68,9 @@ let pp_boxed_tuple f = function
blocks is less that a line length. To avoid this awkward situation,
we attach a big virtual size to [fnl] newlines. *)
-let fnl () = stras (1000000,"") ++ fnl ()
+(* EG: This looks quite suspicious... but beware of bugs *)
+(* let fnl () = stras (1000000,"") ++ fnl () *)
+let fnl () = fnl ()
let fnl2 () = fnl () ++ fnl ()
@@ -91,10 +94,7 @@ let begins_with_CoqXX s =
let unquote s =
if lang () != Scheme then s
- else
- let s = String.copy s in
- for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
- s
+ else String.map (fun c -> if c == '\'' then '~' else c) s
let rec qualify delim = function
| [] -> assert false
@@ -110,12 +110,17 @@ let pseudo_qualify = qualify "__"
let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
-let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id))
+[@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+let uncapitalize = String.uncapitalize
+[@@@ocaml.warning "+3"]
+
+let lowercase_id id = Id.of_string (uncapitalize (ascii_of_id id))
let uppercase_id id =
let s = ascii_of_id id in
assert (not (String.is_empty s));
if s.[0] == '_' then Id.of_string ("Coq_"^s)
- else Id.of_string (String.capitalize s)
+ else Id.of_string (capitalize s)
type kind = Term | Type | Cons | Mod
@@ -145,7 +150,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 +313,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 +516,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..4c9b1e1a5a 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Globnames
open Miniml
@@ -62,7 +63,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 52f22ee603..688bcd025c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Miniml
open Term
open Declarations
@@ -41,7 +42,7 @@ let toplevel_env () =
| "MODULE TYPE" ->
let modtype = Global.lookup_modtype (MPdot (mp, l)) in
Some (l, SFBmodtype modtype)
- | "INCLUDE" -> error "No extraction of toplevel Include yet."
+ | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.")
| _ -> None
end
| _ -> None
@@ -435,7 +436,7 @@ let mono_filename f =
else
try Id.of_string (Filename.basename f)
with UserError _ ->
- error "Extraction: provided filename is not a valid identifier"
+ user_err Pp.(str "Extraction: provided filename is not a valid identifier")
in
Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
@@ -472,13 +473,14 @@ let formatter dry file =
if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
else
match file with
- | Some f -> Pp_control.with_output_to f
+ | Some f -> Topfmt.with_output_to f
| None -> Format.formatter_of_buffer buf
in
+ (* XXX: Fixme, this shouldn't depend on Topfmt *)
(* We never want to see ellipsis ... in extracted code *)
Format.pp_set_max_boxes ft max_int;
(* We reuse the width information given via "Set Printing Width" *)
- (match Pp_control.get_margin () with
+ (match Topfmt.get_margin () with
| None -> ()
| Some i ->
Format.pp_set_margin ft i;
@@ -507,8 +509,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
@@ -519,8 +520,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
set_phase Impl;
pp_with ft (d.preamble mo comment opened unsafe_needs);
pp_with ft (d.pp_struct struc);
+ Format.pp_print_flush ft ();
Option.iter close_out cout;
with reraise ->
+ Format.pp_print_flush ft ();
Option.iter close_out cout; raise reraise
end;
if not dry then Option.iter info_file fn;
@@ -533,8 +536,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
set_phase Intf;
pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
pp_with ft (d.pp_sig (signature_of_structure struc));
+ Format.pp_print_flush ft ();
close_out cout;
with reraise ->
+ Format.pp_print_flush ft ();
close_out cout; raise reraise
end;
info_file si)
@@ -653,7 +658,7 @@ let extraction_library is_rec m =
let l = List.rev (environment_until (Some dir_m)) in
let select l (mp,struc) =
if Visit.needed_mp mp
- then (mp, extract_structure env mp no_delta true struc) :: l
+ then (mp, extract_structure env mp no_delta ~all:true struc) :: l
else l
in
let struc = List.fold_left select [] l in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 90f4f911b7..1e7a6ba5bd 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -8,6 +8,7 @@
(*s This module declares the extraction commands. *)
+open API
open Names
open Libnames
open Globnames
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a980a43f53..f1a50e7eba 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,6 +7,7 @@
(************************************************************************)
(*i*)
+open API
open Util
open Names
open Term
@@ -42,11 +43,11 @@ let none = Evd.empty
let type_of env c =
let polyprop = (lang() == Haskell) in
- Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
+ EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)))
let sort_of env c =
let polyprop = (lang() == Haskell) in
- Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
+ Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
(*S Generation of flags and signatures. *)
@@ -70,11 +71,17 @@ type scheme = TypeScheme | Default
type flag = info * scheme
+let whd_all env t =
+ EConstr.Unsafe.to_constr (whd_all env none (EConstr.of_constr t))
+
+let whd_betaiotazeta t =
+ EConstr.Unsafe.to_constr (whd_betaiotazeta none (EConstr.of_constr t))
+
(*s [flag_of_type] transforms a type [t] into a [flag].
Really important function. *)
let rec flag_of_type env t : flag =
- let t = whd_all env none t in
+ let t = whd_all env 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)
@@ -99,17 +106,20 @@ let is_info_scheme env t = match flag_of_type env t with
| (Info, TypeScheme) -> true
| _ -> false
+let push_rel_assum (n, t) env =
+ Environ.push_rel (LocalAssum (n, t)) env
+
(*s [type_sign] gernerates a signature aimed at treating a type application. *)
let rec type_sign env c =
- match kind_of_term (whd_all env none c) with
+ match kind_of_term (whd_all env 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_all env none c) with
+ match kind_of_term (whd_all env 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 +145,7 @@ let make_typvar n vl =
next_ident_away id' vl
let rec type_sign_vl env c =
- match kind_of_term (whd_all env none c) with
+ match kind_of_term (whd_all env 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 +153,7 @@ let rec type_sign_vl env c =
| _ -> [],[]
let rec nb_default_params env c =
- match kind_of_term (whd_all env none c) with
+ match kind_of_term (whd_all env 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
@@ -214,7 +224,7 @@ let parse_ind_args si args relmax =
let rec extract_type env db j c args =
- match kind_of_term (whd_betaiotazeta Evd.empty c) with
+ match kind_of_term (whd_betaiotazeta c) with
| App (d, args') ->
(* We just accumulate the arguments. *)
extract_type env db j d (Array.to_list args' @ args)
@@ -258,7 +268,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) ->
@@ -297,7 +307,7 @@ and extract_type_app env db (r,s) args =
let ml_args =
List.fold_right
(fun (b,c) a -> if b == Keep then
- let p = List.length (fst (splay_prod env none (type_of env c))) in
+ let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in
let db = iterate (fun l -> 0 :: l) p db in
(extract_type_scheme env db c p) :: a
else a)
@@ -316,12 +326,13 @@ and extract_type_app env db (r,s) args =
and extract_type_scheme env db c p =
if Int.equal p 0 then extract_type env db 0 c []
else
- let c = whd_betaiotazeta Evd.empty c in
+ let c = whd_betaiotazeta c in
match kind_of_term c with
| Lambda (n,t,d) ->
extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
| _ ->
- let rels = fst (splay_prod env none (type_of env c)) in
+ let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in
+ let rels = List.map (on_snd EConstr.Unsafe.to_constr) rels in
let env = push_rels_assum rels env in
let eta_args = List.rev_map mkRel (List.interval 1 p) in
extract_type env db 0 (lift p c) eta_args
@@ -488,7 +499,7 @@ and extract_really_ind env kn mib =
*)
and extract_type_cons env db dbmap c i =
- match kind_of_term (whd_all env none c) with
+ match kind_of_term (whd_all env 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
@@ -595,7 +606,8 @@ let rec extract_term env mle mlt c 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
+ let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in
+ let term = EConstr.Unsafe.to_constr term in
extract_term env mle mlt term args
| Rel n ->
(* As soon as the expected [mlt] for the head is known, *)
@@ -846,8 +858,8 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
let decomp_lams_eta_n n m env c t =
- let rels = fst (splay_prod_n env none n t) in
- let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
+ let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) in
+ let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,EConstr.Unsafe.to_constr c)) rels in
let rels',c = decompose_lam c in
let d = n - m in
(* we'd better keep rels' as long as possible. *)
@@ -887,7 +899,7 @@ let extract_std_constant env kn body typ =
break user's clever let-ins and partial applications). *)
let rels, c =
let n = List.length s
- and m = nb_lam body in
+ and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in
if n <= m then decompose_lam_n n body
else
let s,s' = List.chop m s in
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index cdda777a6c..2b4b05a957 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -8,6 +8,7 @@
(*s Extraction from Coq terms to Miniml. *)
+open API
open Names
open Term
open Declarations
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 19fda4aead..6cba83ef91 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,14 +8,16 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+open API
+open Grammar_API.Pcoq.Prim
+
DECLARE PLUGIN "extraction_plugin"
(* ML names *)
+open Ltac_plugin
open Genarg
open Stdarg
-open Constrarg
-open Pcoq.Prim
open Pp
open Names
open Nameops
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0692c88cd1..8cdfb34992 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -8,6 +8,7 @@
(*s Production of Haskell syntax. *)
+open API
open Pp
open CErrors
open Util
@@ -20,9 +21,10 @@ open Mlutil
open Common
(*s Haskell renaming issues. *)
-
+[@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
let pr_upper_id id = str (String.capitalize (Id.to_string id))
+[@@@ocaml.warning "+3"]
let keywords =
List.fold_right (fun s -> Id.Set.add (Id.of_string s))
@@ -185,7 +187,7 @@ let rec pp_expr par env args =
pp_boxed_tuple (pp_expr true env []) l
| MLcase (_,t, pv) when is_custom_match pv ->
if not (is_regular_match pv) then
- error "Cannot mix yet user-given match and general patterns.";
+ user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
let mkfun (ids,_,e) =
if not (List.is_empty ids) then named_lams (List.rev ids) e
else dummy_lams (ast_lift 1 e) 1
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index e43c47d050..1bf19f186b 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,3 +1,4 @@
+open API
open Pp
open Util
open Names
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index db33615228..28226f225f 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -8,6 +8,7 @@
(*s Target language for extraction: a core ML called MiniML. *)
+open API
open Pp
open Names
open Globnames
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 402fe4ffe6..5a50899c66 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,6 +7,7 @@
(************************************************************************)
(*i*)
+open API
open Util
open Names
open Libnames
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index c667552490..2655dfc897 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Globnames
open Miniml
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 60fe8e7620..2b1e810604 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Globnames
open CErrors
@@ -19,7 +20,7 @@ open Mlutil
let rec msid_of_mt = function
| MTident mp -> mp
| MTwith(mt,_)-> msid_of_mt mt
- | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name")
+ | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.")
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
@@ -231,7 +232,7 @@ let get_decl_in_structure r struc =
| _ -> error_not_visible r
in go ll sel
with Not_found ->
- anomaly (Pp.str "reference not found in extracted structure")
+ anomaly (Pp.str "reference not found in extracted structure.")
(*s Optimization of a [ml_structure]. *)
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index dc8708249a..45e890be0f 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Globnames
open Miniml
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 5d10cb939d..83abaf508e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -8,6 +8,7 @@
(*s Production of Ocaml syntax. *)
+open API
open Pp
open CErrors
open Util
@@ -66,7 +67,7 @@ let pp_header_comment = function
| None -> mt ()
| Some com -> pp_comment com ++ fnl2 ()
-let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
let pp_tdummy usf =
if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
@@ -246,7 +247,7 @@ let rec pp_expr par env args =
pp_boxed_tuple (pp_expr true env []) l
| MLcase (_, t, pv) when is_custom_match pv ->
if not (is_regular_match pv) then
- error "Cannot mix yet user-given match and general patterns.";
+ user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
let mkfun (ids,_,e) =
if not (List.is_empty ids) then named_lams (List.rev ids) e
else dummy_lams (ast_lift 1 e) 1
@@ -555,24 +556,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,43 +580,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 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
+ (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")
- with Not_found -> Pp.mt ())
+ 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 ->
@@ -647,15 +619,17 @@ and pp_module_type params = function
push_visible mp params;
let try_pp_specif l x =
let px = pp_specif x in
- if Pp.is_empty px then l else px::l
+ if Pp.ismt px then l else px::l
in
(* We cannot use fold_right here due to side effects in pp_specif *)
let l = List.fold_left try_pp_specif [] sign in
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
@@ -682,12 +656,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*)
@@ -700,18 +673,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
@@ -726,15 +697,17 @@ and pp_module_expr params = function
push_visible mp params;
let try_pp_structure_elem l x =
let px = pp_structure_elem x in
- if Pp.is_empty px then l else px::l
+ if Pp.ismt px then l else px::l
in
(* We cannot use fold_right here due to side effects in pp_structure_elem *)
let l = List.fold_left try_pp_structure_elem [] sel in
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 ()
@@ -742,7 +715,7 @@ let rec prlist_sep_nonempty sep f = function
| h::t ->
let e = f h in
let r = prlist_sep_nonempty sep f t in
- if Pp.is_empty e then r
+ if Pp.ismt e then r
else e ++ sep () ++ r
let do_struct f s =
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a6309e61f9..55168cc297 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -8,6 +8,7 @@
(*s Production of Scheme syntax. *)
+open API
open Pp
open CErrors
open Util
@@ -40,11 +41,7 @@ let preamble _ comment _ usf =
(if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
let pr_id id =
- let s = Id.to_string id in
- for i = 0 to String.length s - 1 do
- if s.[i] == '\'' then s.[i] <- '~'
- done;
- str s
+ str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id)
let paren = pp_par true
@@ -100,9 +97,9 @@ let rec pp_expr env args =
prlist_with_sep spc (pp_cons_args env) args')
in
if is_coinductive r then paren (str "delay " ++ st) else st
- | MLtuple _ -> error "Cannot handle tuples in Scheme yet."
+ | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.")
| MLcase (_,_,pv) when not (is_regular_match pv) ->
- error "Cannot handle general patterns in Scheme yet."
+ user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
| MLcase (_,t,pv) when is_custom_match pv ->
let mkfun (ids,_,e) =
if not (List.is_empty ids) then named_lams (List.rev ids) e
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ff66d915f5..607ca1b3a9 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Term
open Declarations
@@ -20,6 +21,11 @@ open Util
open Pp
open Miniml
+[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+[@@@ocaml.warning "+3"]
+
+
(** Sets and maps for [global_reference] that use the "user" [kernel_name]
instead of the canonical one *)
@@ -55,7 +61,7 @@ let is_modfile = function
| _ -> false
let raw_string_of_modfile = function
- | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
+ | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f)))
| _ -> assert false
let is_toplevel mp =
@@ -256,7 +262,7 @@ let safe_basename_of_global r =
let last_chance r =
try Nametab.basename_of_global r
with Not_found ->
- anomaly (Pp.str "Inductive object unknown to extraction and not globally visible")
+ anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.")
in
match r with
| ConstRef kn -> Label.to_id (con_label kn)
@@ -293,7 +299,7 @@ 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"
@@ -494,8 +500,7 @@ let my_bool_option name initval =
let flag = ref initval in
let access = fun () -> !flag in
let _ = declare_bool_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction "^name;
optkey = ["Extraction"; name];
optread = access;
@@ -567,16 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
let optims () = !opt_flag_ref
let _ = declare_bool_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction Optimize";
optkey = ["Extraction"; "Optimize"];
optread = (fun () -> not (Int.equal !int_flag_ref 0));
optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
let _ = declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Extraction Flag";
optkey = ["Extraction";"Flag"];
optread = (fun _ -> Some !int_flag_ref);
@@ -590,8 +593,7 @@ let conservative_types_ref = ref false
let conservative_types () = !conservative_types_ref
let _ = declare_bool_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction Conservative Types";
optkey = ["Extraction"; "Conservative"; "Types"];
optread = (fun () -> !conservative_types_ref);
@@ -603,8 +605,7 @@ let file_comment_ref = ref ""
let file_comment () = !file_comment_ref
let _ = declare_string_option
- {optsync = true;
- optdepr = false;
+ {optdepr = false;
optname = "Extraction File Comment";
optkey = ["Extraction"; "File"; "Comment"];
optread = (fun () -> !file_comment_ref);
@@ -773,13 +774,11 @@ let file_of_modfile mp =
| MPfile f -> Id.to_string (List.hd (DirPath.repr f))
| _ -> assert false
in
- let s = String.copy (string_of_modfile mp) in
- if s.[0] != s0.[0] then s.[0] <- s0.[0];
- s
+ String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp)
let add_blacklist_entries l =
blacklist_table :=
- List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
+ List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s)))
l !blacklist_table
(* Registration of operations for rollback. *)
@@ -894,7 +893,7 @@ let extract_constant_inline inline r ids s =
let extract_inductive r s l optstr =
check_inside_section ();
let g = Smartlocate.global_with_alias r in
- Dumpglob.add_glob (loc_of_reference r) g;
+ Dumpglob.add_glob ?loc:(loc_of_reference r) g;
match g with
| IndRef ((kn,i) as ip) ->
let mib = Global.lookup_mind kn in
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 15a08756c0..cd1667bdb0 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Libnames
open Globnames
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 3563f71dfc..9c30c5eb3e 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,3 @@
-Extraction.vo
ExtrHaskellBasic.vo
ExtrHaskellNatNum.vo
ExtrHaskellNatInt.vo
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 07:53:31 +0000