aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml11
-rw-r--r--checker/mod_checking.ml10
-rw-r--r--checker/mod_checking.mli2
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_print.ml2
-rw-r--r--kernel/opaqueproof.ml27
-rw-r--r--kernel/opaqueproof.mli28
-rw-r--r--library/global.ml8
-rw-r--r--library/global.mli4
-rw-r--r--library/library.ml7
-rw-r--r--library/library.mli3
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--printing/prettyp.ml6
-rw-r--r--stm/stm.ml4
-rw-r--r--vernac/assumptions.ml4
-rw-r--r--vernac/lemmas.ml2
18 files changed, 60 insertions, 68 deletions
diff --git a/checker/check.ml b/checker/check.ml
index cc5ad0af4c..76f40dbac2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -100,16 +100,7 @@ let access_opaque_table dp i =
assert (i < Array.length t);
t.(i)
-let access_opaque_univ_table dp i =
- try
- let t = LibraryMap.find dp !opaque_univ_tables in
- assert (i < Array.length t);
- Some t.(i)
- with Not_found -> None
-
-let () =
- Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
- Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
+let () = Mod_checking.set_indirect_accessor access_opaque_table
let check_one_lib admit senv (dir,m) =
let md = m.library_compiled in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index a3f151ef86..1cf07e7cc7 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,6 +8,14 @@ open Environ
(** {6 Checking constants } *)
+let get_proof = ref (fun _ _ -> assert false)
+let set_indirect_accessor f = get_proof := f
+
+let indirect_accessor = {
+ Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+ Opaqueproof.access_constraints = (fun _ _ -> assert false);
+}
+
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn);
(* Locally set the oracle for further typechecking *)
@@ -33,7 +41,7 @@ let check_constant_declaration env kn cb =
let body = match cb.const_body with
| Undef _ | Primitive _ -> None
| Def c -> Some (Mod_subst.force_constr c)
- | OpaqueDef o -> Some (Opaqueproof.force_proof otab o)
+ | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o)
in
let () =
match body with
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 6cff3e6b8c..dbc81c8507 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,4 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+
val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
index cfc38ff9c9..22a0163fbb 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_print.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -11,7 +11,7 @@ let simple_body_access gref =
failwith "constructors are not covered in this example"
| Globnames.ConstRef cst ->
let cb = Environ.lookup_constant cst (Global.env()) in
- match Global.body_of_constant_body cb with
+ match Global.body_of_constant_body Library.indirect_accessor cb with
| Some(e, _) -> e
| None -> failwith "This term has no value"
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f148ee248..75f96da3eb 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,6 +16,11 @@ open Mod_subst
type work_list = (Instance.t * Id.t array) Cmap.t *
(Instance.t * Id.t array) Mindmap.t
+type indirect_accessor = {
+ access_proof : DirPath.t -> int -> constr option;
+ access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+
type cooking_info = {
modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
@@ -36,23 +41,9 @@ let empty_opaquetab = {
opaque_dir = DirPath.initial;
}
-(* hooks *)
-let default_get_opaque dp _ =
- CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
-let default_get_univ dp _ =
- CErrors.user_err (Pp.pr_sequence Pp.str [
- "Cannot access universe constraints of opaque proofs in library ";
- DirPath.to_string dp])
let not_here () =
CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
-
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-(* /hooks *)
-
let create cu = Direct ([],cu)
let turn_indirect dp o tab = match o with
@@ -97,26 +88,26 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
let fp = snd (Int.Map.find i prfs) in
join except fp
-let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) ->
fst(Future.force cu)
| Indirect (l,dp,i) ->
let pt =
if DirPath.equal dp odp
then Future.chain (snd (Int.Map.find i prfs)) fst
- else match !get_opaque dp i with
+ else match access.access_proof dp i with
| None -> not_here ()
| Some v -> Future.from_val v
in
let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
-let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
then snd (Future.force (snd (Int.Map.find i prfs)))
- else match !get_univ dp i with
+ else match access.access_constraints dp i with
| None -> Univ.ContextSet.empty
| Some u -> u
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3b61ec71ef..4646206e55 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -35,10 +35,19 @@ val create : proofterm -> opaque
used so far *)
val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
+type indirect_accessor = {
+ access_proof : DirPath.t -> int -> constr option;
+ access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+(** When stored indirectly, opaque terms are indexed by their library
+ dirpath and an integer index. The two functions above activate
+ this indirect storage, by telling how to retrieve terms.
+*)
+
(** From a [opaque] back to a [constr]. This might use the
- indirect opaque accessor configured below. *)
-val force_proof : opaquetab -> opaque -> constr
-val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+ indirect opaque accessor given as an argument. *)
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
val subst_opaque : substitution -> opaque -> opaque
@@ -64,16 +73,3 @@ val dump : ?except:Future.UUIDSet.t -> opaquetab ->
Univ.ContextSet.t option array *
cooking_info list array *
int Future.UUIDMap.t
-
-(** When stored indirectly, opaque terms are indexed by their library
- dirpath and an integer index. The following two functions activate
- this indirect storage, by telling how to store and retrieve terms.
- Default creator always returns [None], preventing the creation of
- any indirect link, and default accessor always raises an error.
-*)
-
-val set_indirect_opaque_accessor :
- (DirPath.t -> int -> constr option) -> unit
-val set_indirect_univ_accessor :
- (DirPath.t -> int -> Univ.ContextSet.t option) -> unit
-
diff --git a/library/global.ml b/library/global.ml
index 827b062725..d5ffae7716 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -132,7 +132,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
let opaque_tables () = Environ.opaque_tables (env ())
-let body_of_constant_body env cb =
+let body_of_constant_body access env cb =
let open Declarations in
let otab = Environ.opaque_tables env in
match cb.const_body with
@@ -141,11 +141,11 @@ let body_of_constant_body env cb =
| Def c ->
Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
| OpaqueDef o ->
- Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
+ Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
-let body_of_constant_body ce = body_of_constant_body (env ()) ce
+let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
-let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let body_of_constant access cst = body_of_constant_body access (lookup_constant cst)
(** Operations on kernel names *)
diff --git a/library/global.mli b/library/global.mli
index 984d8c666c..aa9fc18477 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -100,13 +100,13 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
val opaque_tables : unit -> Opaqueproof.opaquetab
-val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
(** Returns the body of the constant if it has any, and the polymorphic context
it lives in. For monomorphic constant, the latter is empty, and for
polymorphic constants, the term contains De Bruijn universe variables that
need to be instantiated. *)
-val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
(** {6 Compiled libraries } *)
diff --git a/library/library.ml b/library/library.ml
index 3bc2e84054..039124635e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -318,9 +318,10 @@ let access_univ_table dp i =
access_table what univ_tables dp i
with Not_found -> None
-let () =
- Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
- Opaqueproof.set_indirect_univ_accessor access_univ_table
+let indirect_accessor = {
+ Opaqueproof.access_proof = access_opaque_table;
+ Opaqueproof.access_constraints = access_univ_table;
+}
(************************************************************************)
(* Internalise libraries *)
diff --git a/library/library.mli b/library/library.mli
index d2b0c4f202..2c0673c3b1 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -73,3 +73,6 @@ val overwrite_library_filenames : string -> unit
(** {6 Native compiler. } *)
val native_name_from_filename : string -> string
+
+(** {6 Opaque accessors} *)
+val indirect_accessor : Opaqueproof.indirect_accessor
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 9db7c8d8d3..051d1f8e0f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr)
let get_opaque env c =
EConstr.of_constr
- (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+ (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c)
let applistc c args = EConstr.mkApp (c, Array.of_list args)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index cffe8a3e78..f2b9ba2ec6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -951,7 +951,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst evd f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
+ let (f_body, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in
let f_body = EConstr.of_constr f_body in
let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1082,7 +1082,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
}
in
let get_body const =
- match Global.body_of_constant const with
+ match Global.body_of_constant Library.indirect_accessor const with
| Some (body, _) ->
let env = Global.env () in
let sigma = Evd.from_env env in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f51c6dc6be..2c107d39d9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -413,7 +413,7 @@ let get_funs_constant mp =
in
function const ->
let find_constant_body const =
- match Global.body_of_constant const with
+ match Global.body_of_constant Library.indirect_accessor const with
| Some (body, _) ->
let body = Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ce7d149ae1..a6b088de0c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -851,7 +851,7 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
end
| _ -> raise (UserError (None, str "Not a function reference") )
in
- (match Global.body_of_constant_body c_body with
+ (match Global.body_of_constant_body Library.indirect_accessor c_body with
| None -> error "Cannot build a graph over an axiom!"
| Some (body, _) ->
let env = Global.env () in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9541ea5882..fca33a24bf 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -549,7 +549,7 @@ let print_instance sigma cb =
let print_constant with_values sep sp udecl =
let cb = Global.lookup_constant sp in
- let val_0 = Global.body_of_constant_body cb in
+ let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in
let typ = cb.const_type in
let univs =
let open Univ in
@@ -557,7 +557,7 @@ let print_constant with_values sep sp udecl =
match cb.const_body with
| Undef _ | Def _ | Primitive _ -> cb.const_universes
| OpaqueDef o ->
- let body_uctxs = Opaqueproof.force_constraints otab o in
+ let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in
match cb.const_universes with
| Monomorphic ctx ->
Monomorphic (ContextSet.union body_uctxs ctx)
@@ -717,7 +717,7 @@ let print_full_pure_context env sigma =
| OpaqueDef lc ->
str "Theorem " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
- str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
+ str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
diff --git a/stm/stm.ml b/stm/stm.ml
index 30cf8a0622..660dc27211 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1839,11 +1839,11 @@ end = struct (* {{{ *)
| _ -> assert false in
(* No need to delay the computation, the future has been forced by
the call to [check_task_aux] above. *)
- let uc = Opaqueproof.force_constraints (Global.opaque_tables ()) o in
+ let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in
let uc = Univ.hcons_universe_context_set uc in
(* We only manipulate monomorphic terms here. *)
let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
- let pr = map (Option.get (Global.body_of_constant_body c)) in
+ let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
let pr = discharge pr in
let pr = Constr.hcons pr in
u.(bucket) <- Some uc;
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 445f10ecc1..9353ef3902 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
traverse_object accu body (VarRef id)
| Const (kn, _) ->
- let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
+ let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
traverse_object accu body (ConstRef kn)
| Ind ((mind, _) as ind, _) ->
traverse_inductive accu mind (IndRef ind)
@@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with
| Lambda(_,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
- let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
+ let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
| _ ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 317cf487cc..740b9031cc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -57,7 +57,7 @@ let retrieve_first_recthm uctx = function
let uctx = UState.context uctx in
let inst = Univ.UContext.instance uctx in
let map (c, ctx) = Vars.subst_instance_constr inst c in
- (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
+ (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
| _ -> assert false
let adjust_guardness_conditions const = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:43:30 +0000