summaryrefslogtreecommitdiff
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.mli3
-rw-r--r--plugins/extraction/extract_env.ml15
-rw-r--r--plugins/extraction/extract_env.mli11
-rw-r--r--plugins/extraction/extraction.ml22
-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/table.ml8
-rw-r--r--plugins/extraction/table.mli77
14 files changed, 117 insertions, 112 deletions
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index ac1f6f91..a4a40d3c 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 030b486b..a2a6a8fe 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.mli b/plugins/extraction/common.mli
index 78545c8b..07237d75 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 397cb292..4ede11b5 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -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
@@ -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],[] ->
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 591d3bb8..54fde2ca 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 f25f6362..67c605ea 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/miniml.ml b/plugins/extraction/miniml.ml
index e1e49d92..ce920ad6 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 e1e49d92..ce920ad6 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 0656d487..9f5c1f1a 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 55a1ee89..d23fdb3d 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 f33a59ed..b398bc07 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 6a81f270..f45773f0 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/table.ml b/plugins/extraction/table.ml
index 54c6d9d7..c3f4cfe6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -652,7 +652,7 @@ 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);
@@ -736,7 +736,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);
@@ -857,7 +857,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 +867,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);
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 906dfd96..a8baeaf1 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 * DirPath.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.39.1) at 2024-12-26 06:57:09 +0000