aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml11
-rw-r--r--plugins/extraction/extract_env.ml8
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/table.ml26
-rw-r--r--plugins/extraction/table.mli2
5 files changed, 20 insertions, 33 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index f235bb8986..bdeb6fca60 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -112,17 +112,12 @@ 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
-[@@@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 lowercase_id id = Id.of_string (String.uncapitalize_ascii (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 (capitalize s)
+ else Id.of_string (String.capitalize_ascii s)
type kind = Term | Type | Cons | Mod
@@ -593,7 +588,7 @@ let pp_global k r =
let ls = ref_renaming (k,r) in
assert (List.length ls > 1);
let s = List.hd ls in
- let mp,_,l = repr_of_r r in
+ let mp,l = repr_of_r r in
if ModPath.equal mp (top_visible_mp ()) then
(* simpliest situation: definition of r (or use in the same context) *)
(* we update the visible environment *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5d3115d8d7..b0f6301192 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,7 +30,7 @@ open Common
let toplevel_env () =
let get_reference = function
| (_,kn), Lib.Leaf o ->
- let mp,_,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
begin match Libobject.object_tag o with
| "CONSTANT" ->
let constant = Global.lookup_constant (Constant.make1 kn) in
@@ -124,7 +124,7 @@ module Visit : VISIT = struct
end
let add_field_label mp = function
- | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab)
+ | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make mp lab)
| (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
let rec add_labels mp = function
@@ -208,10 +208,10 @@ let env_for_mtb_with_def env mp me reso idl =
Modops.add_structure mp before reso env
let make_cst resolver mp l =
- Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
+ Mod_subst.constant_of_delta_kn resolver (KerName.make mp l)
let make_mind resolver mp l =
- Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l)
+ Mod_subst.mind_of_delta_kn resolver (KerName.make mp l)
(* From a [structure_body] (i.e. a list of [structure_field_body])
to specifications. *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e6234c1452..97fe9f24d5 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,10 +21,8 @@ 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 pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
+let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
let keywords =
List.fold_right (fun s -> Id.Set.add (Id.of_string s))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e05e82af6f..7b4fd280bd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -22,11 +22,6 @@ 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 *)
@@ -41,16 +36,16 @@ let occur_kn_in_ref kn = function
| ConstRef _ | VarRef _ -> false
let repr_of_r = function
- | ConstRef kn -> Constant.repr3 kn
+ | ConstRef kn -> Constant.repr2 kn
| IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
+ | ConstructRef ((kn,_),_) -> MutInd.repr2 kn
| VarRef v -> KerName.repr (Lib.make_kn v)
let modpath_of_r r =
- let mp,_,_ = repr_of_r r in mp
+ let mp,_ = repr_of_r r in mp
let label_of_r r =
- let _,_,l = repr_of_r r in l
+ let _,l = repr_of_r r in l
let rec base_mp = function
| MPdot (mp,l) -> base_mp mp
@@ -61,7 +56,7 @@ let is_modfile = function
| _ -> false
let raw_string_of_modfile = function
- | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f)))
+ | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
| _ -> assert false
let is_toplevel mp =
@@ -100,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
let labels_of_ref r =
let mp_top = Lib.current_mp () in
- let mp,_,l = repr_of_r r in
+ let mp,l = repr_of_r r in
parse_labels2 [l] mp_top mp
@@ -194,7 +189,7 @@ let init_recursors () = recursors := KNset.empty
let add_recursors env ind =
let kn = MutInd.canonical ind in
let mk_kn id =
- KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id)
+ KerName.make (KerName.modpath kn) (Label.of_id id)
in
let mib = Environ.lookup_mind ind env in
Array.iter
@@ -292,7 +287,7 @@ let safe_pr_long_global r =
try Printer.pr_global r
with Not_found -> match r with
| ConstRef kn ->
- let mp,_,l = Constant.repr3 kn in
+ let mp,l = Constant.repr2 kn in
str ((ModPath.to_string mp)^"."^(Label.to_string l))
| _ -> assert false
@@ -658,8 +653,7 @@ let inline_extraction : bool * GlobRef.t list -> obj =
cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
classify_function = (fun o -> Substitute o);
- discharge_function =
- (fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
+ discharge_function = (fun (_,x) -> Some x);
subst_function =
(fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
}
@@ -784,7 +778,7 @@ let file_of_modfile mp =
let add_blacklist_entries l =
blacklist_table :=
- List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s)))
+ List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
l !blacklist_table
(* Registration of operations for rollback. *)
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a8baeaf1b6..acc1bfee8a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
-val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t
+val repr_of_r : GlobRef.t -> ModPath.t * Label.t
val modpath_of_r : GlobRef.t -> ModPath.t
val label_of_r : GlobRef.t -> Label.t
val base_mp : ModPath.t -> ModPath.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:36:12 +0000