aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ExtrHaskellString.v2
-rw-r--r--plugins/extraction/ExtrOcamlString.v1
-rw-r--r--plugins/extraction/common.ml11
-rw-r--r--plugins/extraction/common.mli3
-rw-r--r--plugins/extraction/extract_env.ml29
-rw-r--r--plugins/extraction/extract_env.mli11
-rw-r--r--plugins/extraction/extraction.ml22
-rw-r--r--plugins/extraction/g_extraction.mlg (renamed from plugins/extraction/g_extraction.ml4)81
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/miniml.ml25
-rw-r--r--plugins/extraction/miniml.mli25
-rw-r--r--plugins/extraction/mlutil.ml26
-rw-r--r--plugins/extraction/mlutil.mli5
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/modutil.mli7
-rw-r--r--plugins/extraction/plugin_base.dune5
-rw-r--r--plugins/extraction/table.ml64
-rw-r--r--plugins/extraction/table.mli77
18 files changed, 207 insertions, 195 deletions
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index ac1f6f9130..a4a40d3c5a 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -35,6 +35,8 @@ Extract Inductive ascii => "Prelude.Char"
(Data.Bits.testBit (Data.Char.ord a) 6)
(Data.Bits.testBit (Data.Char.ord a) 7))".
Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
Extract Inlined Constant String.string_dec => "(Prelude.==)".
+Extract Inlined Constant String.eqb => "(Prelude.==)".
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 030b486b26..a2a6a8fe67 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -33,6 +33,7 @@ Extract Constant shift =>
"fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
Extract Inlined Constant ascii_dec => "(=)".
+Extract Inlined Constant Ascii.eqb => "(=)".
Extract Inductive string => "char list" [ "[]" "(::)" ].
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/common.mli b/plugins/extraction/common.mli
index 78545c8bdf..07237d7504 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Globnames
open Miniml
(** By default, in module Format, you can do horizontal placing of blocks
@@ -54,7 +53,7 @@ val opened_libraries : unit -> ModPath.t list
type kind = Term | Type | Cons | Mod
-val pp_global : kind -> global_reference -> string
+val pp_global : kind -> GlobRef.t -> string
val pp_module : ModPath.t -> string
val top_visible_mp : unit -> ModPath.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 397cb29208..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
@@ -79,7 +79,7 @@ module type VISIT = sig
(* Add reference / ... in the visit lists.
These functions silently add the mp of their arg in the mp list *)
- val add_ref : global_reference -> unit
+ val add_ref : GlobRef.t -> unit
val add_kn : KerName.t -> unit
val add_decl_deps : ml_decl -> unit
val add_spec_deps : ml_spec -> unit
@@ -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. *)
@@ -596,19 +596,18 @@ let warns () =
let rec locate_ref = function
| [] -> [],[]
- | r::l ->
- let q = qualid_of_reference r in
- let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None
+ | qid::l ->
+ let mpo = try Some (Nametab.locate_module qid) with Not_found -> None
and ro =
- try Some (Smartlocate.global_with_alias r)
+ try Some (Smartlocate.global_with_alias qid)
with Nametab.GlobalizationError _ | UserError _ -> None
in
match mpo, ro with
- | None, None -> Nametab.error_global_not_found q
+ | None, None -> Nametab.error_global_not_found qid
| 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_ambiguous_name (q.CAst.v,mp,r);
+ warning_ambiguous_name (qid,mp,r);
let refs,mps = locate_ref l in refs,mp::mps
(*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -646,7 +645,7 @@ let separate_extraction lr =
is \verb!Extraction! [qualid]. *)
let simple_extraction r =
- Vernacentries.dump_global CAst.(make (Misctypes.AN r));
+ Vernacentries.dump_global CAst.(make (Constrexpr.AN r));
match locate_ref [r] with
| ([], [mp]) as p -> full_extr None p
| [r],[] ->
@@ -711,10 +710,10 @@ let structure_for_compute env sg c =
init false false ~compute:true;
let ast, mlt = Extraction.extract_constr env sg c in
let ast = Mlutil.normalize ast in
- let refs = ref Refset.empty in
- let add_ref r = refs := Refset.add r !refs in
+ let refs = ref GlobRef.Set.empty in
+ let add_ref r = refs := GlobRef.Set.add r !refs in
let () = ast_iter_references add_ref add_ref add_ref ast in
- let refs = Refset.elements !refs in
+ let refs = GlobRef.Set.elements !refs in
let struc = optimize_struct (refs,[]) (mono_environment refs []) in
(flatten_structure struc), ast, mlt
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 591d3bb86e..54fde2ca46 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -12,21 +12,20 @@
open Names
open Libnames
-open Globnames
-val simple_extraction : reference -> unit
-val full_extraction : string option -> reference list -> unit
-val separate_extraction : reference list -> unit
+val simple_extraction : qualid -> unit
+val full_extraction : string option -> qualid list -> unit
+val separate_extraction : qualid list -> unit
val extraction_library : bool -> Id.t -> unit
(* For the test-suite : extraction to a temporary file + ocamlc on it *)
-val extract_and_compile : reference list -> unit
+val extract_and_compile : qualid list -> unit
(* For debug / external output via coqtop.byte + Drop : *)
val mono_environment :
- global_reference list -> ModPath.t list -> Miniml.ml_structure
+ GlobRef.t list -> ModPath.t list -> Miniml.ml_structure
(* Used by the Relation Extraction plugin *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f25f636249..67c605ea1d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -431,7 +431,7 @@ and extract_really_ind env kn mib =
let packets =
Array.mapi
(fun i mip ->
- let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
+ let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in
let ar = Inductive.type_of_inductive env ((mib,mip),u) in
let ar = EConstr.of_constr ar in
let info = (fst (flag_of_type env sg ar) = Info) in
@@ -488,7 +488,7 @@ and extract_really_ind env kn mib =
Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
then raise (I Singleton);
if List.is_empty l then raise (I Standard);
- if Option.is_empty mib.mind_record then raise (I Standard);
+ if mib.mind_record == Declarations.NotRecord then raise (I Standard);
(* Now we're sure it's a record. *)
(* First, we find its field names. *)
let rec names_prod t = match Constr.kind t with
@@ -1065,9 +1065,14 @@ let extract_constant env kn cb =
(match cb.const_body with
| Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
- (match cb.const_proj with
+ (match Recordops.find_primitive_projection kn with
| None -> mk_typ (get_body c)
- | Some pb -> mk_typ (EConstr.of_constr pb.proj_body))
+ | Some p ->
+ let p = Projection.make p false in
+ let ind = Projection.inductive p in
+ let bodies = Inductiveops.legacy_match_projection env ind in
+ let body = bodies.(Projection.arg p) in
+ mk_typ (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_typ (get_opaque env c)
@@ -1076,9 +1081,14 @@ let extract_constant env kn cb =
(match cb.const_body with
| Undef _ -> warn_info (); mk_ax ()
| Def c ->
- (match cb.const_proj with
+ (match Recordops.find_primitive_projection kn with
| None -> mk_def (get_body c)
- | Some pb -> mk_def (EConstr.of_constr pb.proj_body))
+ | Some p ->
+ let p = Projection.make p false in
+ let ind = Projection.inductive p in
+ let bodies = Inductiveops.legacy_match_projection env ind in
+ let body = bodies.(Projection.arg p) in
+ mk_def (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
if access_opaque () then mk_def (get_opaque env c)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.mlg
index 93909f3e64..1445dffefa 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.mlg
@@ -8,14 +8,19 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Pcoq.Prim
+}
+
DECLARE PLUGIN "extraction_plugin"
+{
+
(* ML names *)
open Ltac_plugin
-open Genarg
open Stdarg
open Pp
open Names
@@ -24,23 +29,31 @@ open Extract_env
let pr_mlname _ _ _ s = spc () ++ qs s
+}
+
ARGUMENT EXTEND mlname
TYPED AS string
- PRINTED BY pr_mlname
-| [ preident(id) ] -> [ id ]
-| [ string(s) ] -> [ s ]
+ PRINTED BY { pr_mlname }
+| [ preident(id) ] -> { id }
+| [ string(s) ] -> { s }
END
+{
+
let pr_int_or_id _ _ _ = function
| ArgInt i -> int i
| ArgId id -> Id.print id
+}
+
ARGUMENT EXTEND int_or_id
- PRINTED BY pr_int_or_id
-| [ preident(id) ] -> [ ArgId (Id.of_string id) ]
-| [ integer(i) ] -> [ ArgInt i ]
+ PRINTED BY { pr_int_or_id }
+| [ preident(id) ] -> { ArgId (Id.of_string id) }
+| [ integer(i) ] -> { ArgInt i }
END
+{
+
let pr_language = function
| Ocaml -> str "OCaml"
| Haskell -> str "Haskell"
@@ -52,117 +65,119 @@ let warn_deprecated_ocaml_spelling =
(fun () ->
strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+}
+
VERNAC ARGUMENT EXTEND language
-PRINTED BY pr_language
-| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
-| [ "OCaml" ] -> [ Ocaml ]
-| [ "Haskell" ] -> [ Haskell ]
-| [ "Scheme" ] -> [ Scheme ]
-| [ "JSON" ] -> [ JSON ]
+PRINTED BY { pr_language }
+| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml }
+| [ "OCaml" ] -> { Ocaml }
+| [ "Haskell" ] -> { Haskell }
+| [ "Scheme" ] -> { Scheme }
+| [ "JSON" ] -> { JSON }
END
(* Extraction commands *)
VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
(* Extraction in the Coq toplevel *)
-| [ "Extraction" global(x) ] -> [ simple_extraction x ]
-| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
+| [ "Extraction" global(x) ] -> { simple_extraction x }
+| [ "Recursive" "Extraction" ne_global_list(l) ] -> { full_extraction None l }
(* Monolithic extraction to a file *)
| [ "Extraction" string(f) ne_global_list(l) ]
- -> [ full_extraction (Some f) l ]
+ -> { full_extraction (Some f) l }
(* Extraction to a temporary file and OCaml compilation *)
| [ "Extraction" "TestCompile" ne_global_list(l) ]
- -> [ extract_and_compile l ]
+ -> { extract_and_compile l }
END
VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
(* Same, with content splitted in several files *)
| [ "Separate" "Extraction" ne_global_list(l) ]
- -> [ separate_extraction l ]
+ -> { separate_extraction l }
END
(* Modular extraction (one Coq library = one ML module) *)
VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY
| [ "Extraction" "Library" ident(m) ]
- -> [ extraction_library false m ]
+ -> { extraction_library false m }
END
VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY
| [ "Recursive" "Extraction" "Library" ident(m) ]
- -> [ extraction_library true m ]
+ -> { extraction_library true m }
END
(* Target Language *)
VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF
| [ "Extraction" "Language" language(l) ]
- -> [ extraction_language l ]
+ -> { extraction_language l }
END
VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF
(* Custom inlining directives *)
| [ "Extraction" "Inline" ne_global_list(l) ]
- -> [ extraction_inline true l ]
+ -> { extraction_inline true l }
END
VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF
| [ "Extraction" "NoInline" ne_global_list(l) ]
- -> [ extraction_inline false l ]
+ -> { extraction_inline false l }
END
VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Inline" ]
- -> [Feedback. msg_info (print_extraction_inline ()) ]
+ -> {Feedback. msg_info (print_extraction_inline ()) }
END
VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
| [ "Reset" "Extraction" "Inline" ]
- -> [ reset_extraction_inline () ]
+ -> { reset_extraction_inline () }
END
VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF
(* Custom implicit arguments of some csts/inds/constructors *)
| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ]
- -> [ extraction_implicit r l ]
+ -> { extraction_implicit r l }
END
VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF
(* Force Extraction to not use some filenames *)
| [ "Extraction" "Blacklist" ne_ident_list(l) ]
- -> [ extraction_blacklist l ]
+ -> { extraction_blacklist l }
END
VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Blacklist" ]
- -> [ Feedback.msg_info (print_extraction_blacklist ()) ]
+ -> { Feedback.msg_info (print_extraction_blacklist ()) }
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
| [ "Reset" "Extraction" "Blacklist" ]
- -> [ reset_extraction_blacklist () ]
+ -> { reset_extraction_blacklist () }
END
(* Overriding of a Coq object by an ML one *)
VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF
| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
- -> [ extract_constant_inline false x idl y ]
+ -> { extract_constant_inline false x idl y }
END
VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF
| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
- -> [ extract_constant_inline true x [] y ]
+ -> { extract_constant_inline true x [] y }
END
VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
| [ "Extract" "Inductive" global(x) "=>"
mlname(id) "[" mlname_list(idl) "]" string_opt(o) ]
- -> [ extract_inductive x id idl o ]
+ -> { extract_inductive x id idl o }
END
(* Show the extraction of the current proof *)
VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
| [ "Show" "Extraction" ]
- -> [ show_extraction () ]
+ -> { show_extraction () }
END
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/miniml.ml b/plugins/extraction/miniml.ml
index e1e49d9269..ce920ad6a0 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -11,7 +11,6 @@
(*s Target language for extraction: a core ML called MiniML. *)
open Names
-open Globnames
(* The [signature] type is used to know how many arguments a CIC
object expects, and what these arguments will become in the ML
@@ -26,7 +25,7 @@ open Globnames
type kill_reason =
| Ktype
| Kprop
- | Kimplicit of global_reference * int (* n-th arg of a cst or construct *)
+ | Kimplicit of GlobRef.t * int (* n-th arg of a cst or construct *)
type sign = Keep | Kill of kill_reason
@@ -39,7 +38,7 @@ type signature = sign list
type ml_type =
| Tarr of ml_type * ml_type
- | Tglob of global_reference * ml_type list
+ | Tglob of GlobRef.t * ml_type list
| Tvar of int
| Tvar' of int (* same as Tvar, used to avoid clash *)
| Tmeta of ml_meta (* used during ML type reconstruction *)
@@ -60,7 +59,7 @@ type inductive_kind =
| Singleton
| Coinductive
| Standard
- | Record of global_reference option list (* None for anonymous field *)
+ | Record of GlobRef.t option list (* None for anonymous field *)
(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
If the inductive is logical ([ip_logical = false]), then all other fields
@@ -118,8 +117,8 @@ and ml_ast =
| MLapp of ml_ast * ml_ast list
| MLlam of ml_ident * ml_ast
| MLletin of ml_ident * ml_ast * ml_ast
- | MLglob of global_reference
- | MLcons of ml_type * global_reference * ml_ast list
+ | MLglob of GlobRef.t
+ | MLcons of ml_type * GlobRef.t * ml_ast list
| MLtuple of ml_ast list
| MLcase of ml_type * ml_ast * ml_branch array
| MLfix of int * Id.t array * ml_ast array
@@ -129,24 +128,24 @@ and ml_ast =
| MLmagic of ml_ast
and ml_pattern =
- | Pcons of global_reference * ml_pattern list
+ | Pcons of GlobRef.t * ml_pattern list
| Ptuple of ml_pattern list
| Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
| Pwild
- | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+ | Pusual of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
(*s ML declarations. *)
type ml_decl =
| Dind of MutInd.t * ml_ind
- | Dtype of global_reference * Id.t list * ml_type
- | Dterm of global_reference * ml_ast * ml_type
- | Dfix of global_reference array * ml_ast array * ml_type array
+ | Dtype of GlobRef.t * Id.t list * ml_type
+ | Dterm of GlobRef.t * ml_ast * ml_type
+ | Dfix of GlobRef.t array * ml_ast array * ml_type array
type ml_spec =
| Sind of MutInd.t * ml_ind
- | Stype of global_reference * Id.t list * ml_type option
- | Sval of global_reference * ml_type
+ | Stype of GlobRef.t * Id.t list * ml_type option
+ | Sval of GlobRef.t * ml_type
type ml_specif =
| Spec of ml_spec
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index e1e49d9269..ce920ad6a0 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -11,7 +11,6 @@
(*s Target language for extraction: a core ML called MiniML. *)
open Names
-open Globnames
(* The [signature] type is used to know how many arguments a CIC
object expects, and what these arguments will become in the ML
@@ -26,7 +25,7 @@ open Globnames
type kill_reason =
| Ktype
| Kprop
- | Kimplicit of global_reference * int (* n-th arg of a cst or construct *)
+ | Kimplicit of GlobRef.t * int (* n-th arg of a cst or construct *)
type sign = Keep | Kill of kill_reason
@@ -39,7 +38,7 @@ type signature = sign list
type ml_type =
| Tarr of ml_type * ml_type
- | Tglob of global_reference * ml_type list
+ | Tglob of GlobRef.t * ml_type list
| Tvar of int
| Tvar' of int (* same as Tvar, used to avoid clash *)
| Tmeta of ml_meta (* used during ML type reconstruction *)
@@ -60,7 +59,7 @@ type inductive_kind =
| Singleton
| Coinductive
| Standard
- | Record of global_reference option list (* None for anonymous field *)
+ | Record of GlobRef.t option list (* None for anonymous field *)
(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
If the inductive is logical ([ip_logical = false]), then all other fields
@@ -118,8 +117,8 @@ and ml_ast =
| MLapp of ml_ast * ml_ast list
| MLlam of ml_ident * ml_ast
| MLletin of ml_ident * ml_ast * ml_ast
- | MLglob of global_reference
- | MLcons of ml_type * global_reference * ml_ast list
+ | MLglob of GlobRef.t
+ | MLcons of ml_type * GlobRef.t * ml_ast list
| MLtuple of ml_ast list
| MLcase of ml_type * ml_ast * ml_branch array
| MLfix of int * Id.t array * ml_ast array
@@ -129,24 +128,24 @@ and ml_ast =
| MLmagic of ml_ast
and ml_pattern =
- | Pcons of global_reference * ml_pattern list
+ | Pcons of GlobRef.t * ml_pattern list
| Ptuple of ml_pattern list
| Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
| Pwild
- | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+ | Pusual of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
(*s ML declarations. *)
type ml_decl =
| Dind of MutInd.t * ml_ind
- | Dtype of global_reference * Id.t list * ml_type
- | Dterm of global_reference * ml_ast * ml_type
- | Dfix of global_reference array * ml_ast array * ml_type array
+ | Dtype of GlobRef.t * Id.t list * ml_type
+ | Dterm of GlobRef.t * ml_ast * ml_type
+ | Dfix of GlobRef.t array * ml_ast array * ml_type array
type ml_spec =
| Sind of MutInd.t * ml_ind
- | Stype of global_reference * Id.t list * ml_type option
- | Sval of global_reference * ml_type
+ | Stype of GlobRef.t * Id.t list * ml_type option
+ | Sval of GlobRef.t * ml_type
type ml_specif =
| Spec of ml_spec
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 0656d487ad..9f5c1f1a17 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -59,7 +59,7 @@ let rec eq_ml_type t1 t2 = match t1, t2 with
| Tarr (tl1, tr1), Tarr (tl2, tr2) ->
eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2
| Tglob (gr1, t1), Tglob (gr2, t2) ->
- eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2
+ GlobRef.equal gr1 gr2 && List.equal eq_ml_type t1 t2
| Tvar i1, Tvar i2 -> Int.equal i1 i2
| Tvar' i1, Tvar' i2 -> Int.equal i1 i2
| Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2
@@ -120,7 +120,7 @@ let rec mgu = function
| None -> m.contents <- Some t)
| Tarr(a, b), Tarr(a', b') ->
mgu (a, a'); mgu (b, b')
- | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
+ | Tglob (r,l), Tglob (r',l') when GlobRef.equal r r' ->
List.iter mgu (List.combine l l')
| Tdummy _, Tdummy _ -> ()
| Tvar i, Tvar j when Int.equal i j -> ()
@@ -270,7 +270,7 @@ let rec var2var' = function
| Tglob (r,l) -> Tglob (r, List.map var2var' l)
| a -> a
-type abbrev_map = global_reference -> ml_type option
+type abbrev_map = GlobRef.t -> ml_type option
(*s Delta-reduction of type constants everywhere in a ML type [t].
[env] is a function of type [ml_type_env]. *)
@@ -381,9 +381,9 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
eq_ml_ident na1 na2 && eq_ml_ast t1 t2
| MLletin (na1, c1, t1), MLletin (na2, c2, t2) ->
eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2
-| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2
+| MLglob gr1, MLglob gr2 -> GlobRef.equal gr1 gr2
| MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) ->
- eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2
+ eq_ml_type t1 t2 && GlobRef.equal gr1 gr2 && List.equal eq_ml_ast c1 c2
| MLtuple t1, MLtuple t2 ->
List.equal eq_ml_ast t1 t2
| MLcase (t1, c1, p1), MLcase (t2, c2, p2) ->
@@ -398,13 +398,13 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
and eq_ml_pattern p1 p2 = match p1, p2 with
| Pcons (gr1, p1), Pcons (gr2, p2) ->
- eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2
+ GlobRef.equal gr1 gr2 && List.equal eq_ml_pattern p1 p2
| Ptuple p1, Ptuple p2 ->
List.equal eq_ml_pattern p1 p2
| Prel i1, Prel i2 ->
Int.equal i1 i2
| Pwild, Pwild -> true
-| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2
+| Pusual gr1, Pusual gr2 -> GlobRef.equal gr1 gr2
| _ -> false
and eq_ml_branch (id1, p1, t1) (id2, p2, t2) =
@@ -541,24 +541,24 @@ let dump_unused_vars a =
| MLcase (t,e,br) ->
let e' = ren env e in
- let br' = Array.smartmap (ren_branch env) br in
+ let br' = Array.Smart.map (ren_branch env) br in
if e' == e && br' == br then a else MLcase (t,e',br')
| MLfix (i,ids,v) ->
let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in
- let v' = Array.smartmap (ren env') v in
+ let v' = Array.Smart.map (ren env') v in
if v' == v then a else MLfix (i,ids,v')
| MLapp (b,l) ->
- let b' = ren env b and l' = List.smartmap (ren env) l in
+ let b' = ren env b and l' = List.Smart.map (ren env) l in
if b' == b && l' == l then a else MLapp (b',l')
| MLcons(t,r,l) ->
- let l' = List.smartmap (ren env) l in
+ let l' = List.Smart.map (ren env) l in
if l' == l then a else MLcons (t,r,l')
| MLtuple l ->
- let l' = List.smartmap (ren env) l in
+ let l' = List.Smart.map (ren env) l in
if l' == l then a else MLtuple l'
| MLmagic b ->
@@ -984,7 +984,7 @@ let rec iota_red i lift br ((typ,r,a) as cons) =
if i >= Array.length br then raise Impossible;
let (ids,p,c) = br.(i) in
match p with
- | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons
+ | Pusual r' | Pcons (r',_) when not (GlobRef.equal r' r) -> iota_red (i+1) lift br cons
| Pusual r' ->
let c = named_lams (List.rev ids) c in
let c = ast_lift lift c
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 55a1ee893e..d23fdb3d53 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Globnames
open Miniml
open Table
@@ -59,7 +58,7 @@ val type_recomp : ml_type list * ml_type -> ml_type
val var2var' : ml_type -> ml_type
-type abbrev_map = global_reference -> ml_type option
+type abbrev_map = GlobRef.t -> ml_type option
val type_expand : abbrev_map -> ml_type -> ml_type
val type_simpl : ml_type -> ml_type
@@ -117,7 +116,7 @@ val dump_unused_vars : ml_ast -> ml_ast
val normalize : ml_ast -> ml_ast
val optimize_fix : ml_ast -> ml_ast
-val inline : global_reference -> ml_ast -> bool
+val inline : GlobRef.t -> ml_ast -> bool
val is_basic_pattern : ml_pattern -> bool
val has_deep_pattern : ml_branch array -> bool
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index f33a59edf9..b398bc07a0 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -76,7 +76,7 @@ let struct_iter do_decl do_spec do_mp s =
(*s Apply some fonctions upon all references in [ml_type], [ml_ast],
[ml_decl], [ml_spec] and [ml_structure]. *)
-type do_ref = global_reference -> unit
+type do_ref = GlobRef.t -> unit
let record_iter_references do_term = function
| Record l -> List.iter (Option.iter do_term) l
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 6a81f27054..f45773f095 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Globnames
open Miniml
(*s Functions upon ML modules. *)
@@ -17,7 +16,7 @@ open Miniml
val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
-type do_ref = global_reference -> unit
+type do_ref = GlobRef.t -> unit
val type_iter_references : do_ref -> ml_type -> unit
val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
@@ -30,7 +29,7 @@ val mtyp_of_mexpr : ml_module_expr -> ml_module_type
val msid_of_mt : ml_module_type -> ModPath.t
-val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
+val get_decl_in_structure : GlobRef.t -> ml_structure -> ml_decl
(* Some transformations of ML terms. [optimize_struct] simplify
all beta redexes (when the argument does not occur, it is just
@@ -39,5 +38,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
optimizations. The first argument is the list of objects we want to appear.
*)
-val optimize_struct : global_reference list * ModPath.t list ->
+val optimize_struct : GlobRef.t list * ModPath.t list ->
ml_structure -> ml_structure
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune
new file mode 100644
index 0000000000..037b0d5053
--- /dev/null
+++ b/plugins/extraction/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name extraction_plugin)
+ (public_name coq.plugins.extraction)
+ (synopsis "Coq's extraction plugin")
+ (libraries num coq.plugins.ltac))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 54c6d9d729..16890ea260 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -22,16 +22,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 *)
-module Refmap' = Refmap_env
-module Refset' = Refset_env
+module Refmap' = GlobRef.Map_env
+module Refset' = GlobRef.Set_env
(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
@@ -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
@@ -213,12 +208,12 @@ let is_recursor = function
(* NB: here, working modulo name equivalence is ok *)
-let projs = ref (Refmap.empty : (inductive*int) Refmap.t)
-let init_projs () = projs := Refmap.empty
-let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs
-let is_projection r = Refmap.mem r !projs
-let projection_arity r = snd (Refmap.find r !projs)
-let projection_info r = Refmap.find r !projs
+let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t)
+let init_projs () = projs := GlobRef.Map.empty
+let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs
+let is_projection r = GlobRef.Map.mem r !projs
+let projection_arity r = snd (GlobRef.Map.find r !projs)
+let projection_info r = GlobRef.Map.find r !projs
(*s Table of used axioms *)
@@ -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
@@ -451,7 +446,7 @@ let error_MPfile_as_mod mp b =
let argnames_of_global r =
let env = Global.env () in
- let typ, _ = Global.type_of_global_in_context env r in
+ let typ, _ = Typeops.type_of_global_in_context env r in
let rels,_ =
decompose_prod (Reduction.whd_all env typ) in
List.rev_map fst rels
@@ -505,7 +500,7 @@ let info_file f =
let my_bool_option name initval =
let flag = ref initval in
let access = fun () -> !flag in
- let _ = declare_bool_option
+ let () = declare_bool_option
{optdepr = false;
optname = "Extraction "^name;
optkey = ["Extraction"; name];
@@ -577,14 +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
+let () = declare_bool_option
{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
+let () = declare_int_option
{ optdepr = false;
optname = "Extraction Flag";
optkey = ["Extraction";"Flag"];
@@ -598,7 +593,7 @@ let _ = declare_int_option
let conservative_types_ref = ref false
let conservative_types () = !conservative_types_ref
-let _ = declare_bool_option
+let () = declare_bool_option
{optdepr = false;
optname = "Extraction Conservative Types";
optkey = ["Extraction"; "Conservative"; "Types"];
@@ -610,7 +605,7 @@ let _ = declare_bool_option
let file_comment_ref = ref ""
let file_comment () = !file_comment_ref
-let _ = declare_string_option
+let () = declare_string_option
{optdepr = false;
optname = "Extraction File Comment";
optkey = ["Extraction"; "File"; "Comment"];
@@ -652,14 +647,13 @@ let add_inline_entries b l =
(* Registration of operations for rollback. *)
-let inline_extraction : bool * global_reference list -> obj =
+let inline_extraction : bool * GlobRef.t list -> obj =
declare_object
{(default_object "Extraction Inline") with
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)))
}
@@ -736,7 +730,7 @@ let add_implicits r l =
(* Registration of operations for rollback. *)
-let implicit_extraction : global_reference * int_or_id list -> obj =
+let implicit_extraction : GlobRef.t * int_or_id list -> obj =
declare_object
{(default_object "Extraction Implicit") with
cache_function = (fun (_,(r,l)) -> add_implicits r 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. *)
@@ -857,7 +851,7 @@ let find_custom_match pv =
(* Registration of operations for rollback. *)
-let in_customs : global_reference * string list * string -> obj =
+let in_customs : GlobRef.t * string list * string -> obj =
declare_object
{(default_object "ML extractions") with
cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
@@ -867,7 +861,7 @@ let in_customs : global_reference * string list * string -> obj =
(fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
}
-let in_custom_matchs : global_reference * string -> obj =
+let in_custom_matchs : GlobRef.t * string -> obj =
declare_object
{(default_object "ML extractions custom matchs") with
cache_function = (fun (_,(r,s)) -> add_custom_match r s);
@@ -884,7 +878,7 @@ let extract_constant_inline inline r ids s =
match g with
| ConstRef kn ->
let env = Global.env () in
- let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
+ let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in
let typ = Reduction.whd_all env typ in
if Reduction.is_arity env typ
then begin
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 906dfd96ec..acc1bfee8a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -10,31 +10,30 @@
open Names
open Libnames
-open Globnames
open Miniml
open Declarations
-module Refset' : CSig.SetS with type elt = global_reference
-module Refmap' : CSig.MapS with type key = global_reference
+module Refset' : CSig.SetS with type elt = GlobRef.t
+module Refmap' : CSig.MapS with type key = GlobRef.t
-val safe_basename_of_global : global_reference -> Id.t
+val safe_basename_of_global : GlobRef.t -> Id.t
(*s Warning and Error messages. *)
val warning_axioms : unit -> unit
val warning_opaques : bool -> unit
-val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * GlobRef.t -> unit
val warning_id : string -> unit
-val error_axiom_scheme : global_reference -> int -> 'a
-val error_constant : global_reference -> 'a
-val error_inductive : global_reference -> 'a
+val error_axiom_scheme : GlobRef.t -> int -> 'a
+val error_constant : GlobRef.t -> 'a
+val error_inductive : GlobRef.t -> 'a
val error_nb_cons : unit -> 'a
val error_module_clash : ModPath.t -> ModPath.t -> 'a
val error_no_module_expr : ModPath.t -> 'a
-val error_singleton_become_prop : Id.t -> global_reference option -> 'a
+val error_singleton_become_prop : Id.t -> GlobRef.t option -> 'a
val error_unknown_module : qualid -> 'a
val error_scheme : unit -> 'a
-val error_not_visible : global_reference -> 'a
+val error_not_visible : GlobRef.t -> 'a
val error_MPfile_as_mod : ModPath.t -> bool -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
@@ -44,12 +43,12 @@ val err_or_warn_remaining_implicit : kill_reason -> unit
val info_file : string -> unit
-(*s utilities about [module_path] and [kernel_names] and [global_reference] *)
+(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
-val occur_kn_in_ref : MutInd.t -> global_reference -> bool
-val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t
-val modpath_of_r : global_reference -> ModPath.t
-val label_of_r : global_reference -> Label.t
+val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
+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
val is_modfile : ModPath.t -> bool
val string_of_modfile : ModPath.t -> string
@@ -61,7 +60,7 @@ val prefixes_mp : ModPath.t -> MPset.t
val common_prefix_from_list :
ModPath.t -> ModPath.t list -> ModPath.t option
val get_nth_label_mp : int -> ModPath.t -> Label.t
-val labels_of_ref : global_reference -> ModPath.t * Label.t list
+val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list
(*s Some table-related operations *)
@@ -83,27 +82,27 @@ val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option
val add_inductive_kind : MutInd.t -> inductive_kind -> unit
-val is_coinductive : global_reference -> bool
+val is_coinductive : GlobRef.t -> bool
val is_coinductive_type : ml_type -> bool
(* What are the fields of a record (empty for a non-record) *)
val get_record_fields :
- global_reference -> global_reference option list
-val record_fields_of_type : ml_type -> global_reference option list
+ GlobRef.t -> GlobRef.t option list
+val record_fields_of_type : ml_type -> GlobRef.t option list
val add_recursors : Environ.env -> MutInd.t -> unit
-val is_recursor : global_reference -> bool
+val is_recursor : GlobRef.t -> bool
val add_projection : int -> Constant.t -> inductive -> unit
-val is_projection : global_reference -> bool
-val projection_arity : global_reference -> int
-val projection_info : global_reference -> inductive * int (* arity *)
+val is_projection : GlobRef.t -> bool
+val projection_arity : GlobRef.t -> int
+val projection_info : GlobRef.t -> inductive * int (* arity *)
-val add_info_axiom : global_reference -> unit
-val remove_info_axiom : global_reference -> unit
-val add_log_axiom : global_reference -> unit
+val add_info_axiom : GlobRef.t -> unit
+val remove_info_axiom : GlobRef.t -> unit
+val add_log_axiom : GlobRef.t -> unit
-val add_opaque : global_reference -> unit
-val remove_opaque : global_reference -> unit
+val add_opaque : GlobRef.t -> unit
+val remove_opaque : GlobRef.t -> unit
val reset_tables : unit -> unit
@@ -172,22 +171,22 @@ val is_extrcompute : unit -> bool
(*s Table for custom inlining *)
-val to_inline : global_reference -> bool
-val to_keep : global_reference -> bool
+val to_inline : GlobRef.t -> bool
+val to_keep : GlobRef.t -> bool
(*s Table for implicits arguments *)
-val implicits_of_global : global_reference -> Int.Set.t
+val implicits_of_global : GlobRef.t -> Int.Set.t
(*s Table for user-given custom ML extractions. *)
(* UGLY HACK: registration of a function defined in [extraction.ml] *)
val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
-val is_custom : global_reference -> bool
-val is_inline_custom : global_reference -> bool
-val find_custom : global_reference -> string
-val find_type_custom : global_reference -> string list * string
+val is_custom : GlobRef.t -> bool
+val is_inline_custom : GlobRef.t -> bool
+val find_custom : GlobRef.t -> string
+val find_type_custom : GlobRef.t -> string list * string
val is_custom_match : ml_branch array -> bool
val find_custom_match : ml_branch array -> string
@@ -195,17 +194,17 @@ val find_custom_match : ml_branch array -> string
(*s Extraction commands. *)
val extraction_language : lang -> unit
-val extraction_inline : bool -> reference list -> unit
+val extraction_inline : bool -> qualid list -> unit
val print_extraction_inline : unit -> Pp.t
val reset_extraction_inline : unit -> unit
val extract_constant_inline :
- bool -> reference -> string list -> string -> unit
+ bool -> qualid -> string list -> string -> unit
val extract_inductive :
- reference -> string -> string list -> string option -> unit
+ qualid -> string -> string list -> string option -> unit
type int_or_id = ArgInt of int | ArgId of Id.t
-val extraction_implicit : reference -> int_or_id list -> unit
+val extraction_implicit : qualid -> int_or_id list -> unit
(*s Table of blacklisted filenames *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:04:38 +0000