aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cooking.ml17
-rw-r--r--kernel/cooking.mli6
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/declareops.ml15
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/lazyconstr.ml134
-rw-r--r--kernel/mod_subst.ml3
-rw-r--r--kernel/mod_subst.mli4
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/modops.ml4
-rw-r--r--kernel/nativecode.ml4
-rw-r--r--kernel/nativelambda.ml4
-rw-r--r--kernel/opaqueproof.ml112
-rw-r--r--kernel/opaqueproof.mli (renamed from kernel/lazyconstr.mli)65
-rw-r--r--kernel/safe_typing.ml8
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml16
19 files changed, 194 insertions, 216 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index af6992252..58465849c 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -719,7 +719,7 @@ let compile env c =
let compile_constant_body env = function
| Undef _ | OpaqueDef _ -> BCconstant
| Def sb ->
- let body = Lazyconstr.force sb in
+ let body = Mod_subst.force_constr sb in
match kind_of_term body with
| Const kn' ->
(* we use the canonical name of the constant*)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 75642648d..f81bcceb3 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -109,7 +109,7 @@ let abstract_constant_type =
let abstract_constant_body =
List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
-type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
+type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool
type result =
@@ -118,21 +118,22 @@ type result =
let on_body ml hy f = function
| Undef _ as x -> x
- | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
- | OpaqueDef lc ->
- OpaqueDef (Lazyconstr.discharge_direct_lazy_constr ml hy f lc)
+ | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
+ | OpaqueDef o ->
+ OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
+ { Opaqueproof.modlist = ml; abstract = hy } o)
let constr_of_def = function
| Undef _ -> assert false
- | Def cs -> Lazyconstr.force cs
- | OpaqueDef lc -> Lazyconstr.force_opaque lc
+ | Def cs -> Mod_subst.force_constr cs
+ | OpaqueDef lc -> Opaqueproof.force_proof lc
-let cook_constr { Lazyconstr.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract } c =
let cache = Hashtbl.create 13 in
let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
abstract_constant_body (expmod_constr cache modlist c) hyps
-let cook_constant env { from = cb; info = { Lazyconstr.modlist; abstract } } =
+let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
let cache = Hashtbl.create 13 in
let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
let body = on_body modlist hyps
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 05c7a2040..8493b81d8 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -14,7 +14,7 @@ open Univ
(** {6 Cooking the constants. } *)
-type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
+type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool
@@ -23,9 +23,9 @@ type result =
* Context.section_context option
val cook_constant : env -> recipe -> result
-val cook_constr : Lazyconstr.cooking_info -> Term.constr -> Term.constr
+val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
(** {6 Utility functions used in module [Discharge]. } *)
-val expmod_constr : Lazyconstr.work_list -> constr -> constr
+val expmod_constr : Opaqueproof.work_list -> constr -> constr
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef56ae512..e6025790a 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -37,8 +37,8 @@ type inline = int option
type constant_def =
| Undef of inline
- | Def of Lazyconstr.constr_substituted
- | OpaqueDef of Lazyconstr.lazy_constr
+ | Def of constr Mod_subst.substituted
+ | OpaqueDef of Opaqueproof.opaque
(* some contraints are in constant_constraints, some other may be in
* the OpaueDef *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 21a961fc3..7c852a755 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -8,7 +8,6 @@
open Declarations
open Mod_subst
-open Lazyconstr
open Util
(** Operations concernings types in [Declarations] :
@@ -18,14 +17,14 @@ open Util
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
- | Def c -> Some (Lazyconstr.force c)
- | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
+ | Def c -> Some (force_constr c)
+ | OpaqueDef o -> Some (Opaqueproof.force_proof o)
let constraints_of_constant cb = Univ.union_constraints cb.const_constraints
(match cb.const_body with
| Undef _ -> Univ.empty_constraint
| Def c -> Univ.empty_constraint
- | OpaqueDef lc -> snd (Lazyconstr.force_opaque_w_constraints lc))
+ | OpaqueDef o -> Opaqueproof.force_constraints o)
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
@@ -57,8 +56,8 @@ let subst_const_type sub arity = match arity with
let subst_const_def sub def = match def with
| Undef _ -> def
- | Def c -> Def (subst_constr_subst sub c)
- | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+ | Def c -> Def (subst_constr sub c)
+ | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
let subst_const_body sub cb =
assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -104,7 +103,7 @@ let hcons_const_type = function
let hcons_const_def = function
| Undef inl -> Undef inl
| Def l_constr ->
- let constr = force l_constr in
+ let constr = force_constr l_constr in
Def (from_val (Term.hcons_constr constr))
| OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
@@ -238,7 +237,7 @@ let hcons_mind mib =
let join_constant_body cb =
match cb.const_body with
- | OpaqueDef d -> Lazyconstr.join_lazy_constr d
+ | OpaqueDef o -> Opaqueproof.join_opaque o
| _ -> ()
let string_of_side_effect = function
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 93677e5a9..15db39328 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -189,7 +189,7 @@ exception NotEvaluableConst of const_evaluation_result
let constant_value env kn =
let cb = lookup_constant kn env in
match cb.const_body with
- | Def l_body -> Lazyconstr.force l_body
+ | Def l_body -> Mod_subst.force_constr l_body
| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
| Undef _ -> raise (NotEvaluableConst NoBody)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 7d318add5..bcd366f1a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -12,7 +12,7 @@ Cbytecodes
Copcodes
Cemitcodes
Nativevalues
-Lazyconstr
+Opaqueproof
Declareops
Retroknowledge
Conv_oracle
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
deleted file mode 100644
index 23d6d559d..000000000
--- a/kernel/lazyconstr.ml
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Mod_subst
-
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-type cooking_info = { modlist : work_list; abstract : Context.named_context }
-
-(** [constr_substituted] are [constr] with possibly pending
- substitutions of kernel names. *)
-
-type constr_substituted = constr substituted
-
-let from_val = from_val
-
-let force = force subst_mps
-
-let subst_constr_subst = subst_substituted
-
-(** Opaque proof terms might be in some external tables.
- The [force_opaque] function below allows to access these tables,
- this might trigger the read of some extra parts of .vo files.
- In the [Indirect] case, we accumulate "manually" a substitution
- list, the younger one coming first. Nota: no [Direct] constructor
- should end in a .vo, this is checked by coqchk.
-*)
-
-type proofterm = (constr * Univ.constraints) Future.computation
-type lazy_constr =
- (* subst, lib, index *)
- | Indirect of substitution list * DirPath.t * int
- (* opaque in section or interactive session *)
- | Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation
-
-(* TODO : this hcons function could probably be improved (for instance
- hash the dir_path in the Indirect case) *)
-
-let subst_lazy_constr sub = function
- | Direct ([],cu) ->
- Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
- subst_constr_subst sub c, u))
- | Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged")
- | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
-
-let iter_direct_lazy_constr f = function
- | Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr")
- | Direct (d,cu) ->
- Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u))
-
-let discharge_direct_lazy_constr modlist abstract f = function
- | Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr")
- | Direct (d,cu) ->
- Direct ({ modlist; abstract }::d,
- Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
- from_val (f (force c)), u))
-
-let default_get_opaque dp _ =
- Errors.error
- ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
-let default_get_univ dp _ =
- Errors.error
- ("Cannot access universe constraints of opaque proofs in library " ^
- DirPath.to_string dp)
-
-let default_mk_indirect _ = None
-
-let default_join_indirect_local_opaque _ _ = ()
-let default_join_indirect_local_univ _ _ = ()
-
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
-let join_indirect_local_opaque = ref default_join_indirect_local_opaque
-let join_indirect_local_univ = ref default_join_indirect_local_univ
-
-let mk_indirect = ref default_mk_indirect
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-let set_indirect_creator f = (mk_indirect := f)
-let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
-let set_join_indirect_local_univ f = join_indirect_local_univ := f
-
-let reset_indirect_creator () = mk_indirect := default_mk_indirect
-
-let force_lazy_constr = function
- | Direct (_,c) -> Future.force c
- | Indirect (l,dp,i) ->
- let c = Future.force (!get_opaque dp i) in
- List.fold_right subst_constr_subst l (from_val c),
- Future.force
- (Option.default
- (Future.from_val Univ.empty_constraint)
- (!get_univ dp i))
-
-let join_lazy_constr = function
- | Direct (_,c) -> ignore(Future.force c)
- | Indirect (_,dp,i) ->
- !join_indirect_local_opaque dp i;
- !join_indirect_local_univ dp i
-
-let turn_indirect lc = match lc with
- | Indirect _ ->
- Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
- | Direct (d,cu) ->
- let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) ->
- (* this constr_substituted shouldn't have been substituted yet *)
- assert (fst (Mod_subst.repr_substituted c) == None);
- hcons_constr (force c),u) in
- match !mk_indirect (d,cu) with
- | None -> lc
- | Some (dp,i) -> Indirect ([],dp,i)
-
-let force_opaque lc =
- let c, _u = force_lazy_constr lc in force c
-let force_opaque_w_constraints lc =
- let c, u = force_lazy_constr lc in force c, u
-let get_opaque_future_constraints lc = match lc with
- | Indirect (_,dp,i) -> !get_univ dp i
- | Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu))
-let get_opaque_futures lc = match lc with
- | Indirect _ -> assert false
- | Direct (_,cu) ->
- let cu =
- Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in
- Future.split2 ~greedy:true cu
-
-let opaque_from_val cu =
- Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u))
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 009bcb770..f0d1aca4d 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -546,6 +546,9 @@ let force fsubst r = match r.subst_subst with
let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; }
+let force_constr = force subst_mps
+let subst_constr = subst_substituted
+
(* debug *)
let repr_substituted r = match r.subst_subst with
| [] -> None, r.subst_value
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index ddc05380a..34f10b31a 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -152,3 +152,7 @@ val occur_mbid : MBId.t -> substitution -> bool
- [Some s, a] when r is a delayed substitution [s] applied to [a] *)
val repr_substituted : 'a substituted -> substitution list option * 'a
+
+val force_constr : Term.constr substituted -> Term.constr
+val subst_constr :
+ substitution -> Term.constr substituted -> Term.constr substituted
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 6e656fad9..6c0f1b060 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,11 +80,11 @@ let rec check_with_def env struc (idl,c) mp equiv =
let cst = cb.const_constraints +++ cst1 +++ cst2 in
j.uj_val, cst
| Def cs ->
- let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
+ let cst1 = Reduction.conv env' c (Mod_subst.force_constr cs) in
let cst = cb.const_constraints +++ cst1 in
c, cst
in
- let def = Def (Lazyconstr.from_val c') in
+ let def = Def (Mod_subst.from_val c') in
let cb' =
{ cb with
const_body = def;
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2942412f0..2bd421bb3 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -345,7 +345,7 @@ let strengthen_const mp_from l cb resolver =
let kn = KerName.make2 mp_from l in
let con = constant_of_delta_kn resolver kn in
{ cb with
- const_body = Def (Lazyconstr.from_val (mkConst con));
+ const_body = Def (Mod_subst.from_val (mkConst con));
const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
let rec strengthen_mod mp_from mp_to mb =
@@ -407,7 +407,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
match constant.const_body with
| Undef _ | OpaqueDef _ -> l
| Def body ->
- let constr = Lazyconstr.force body in
+ let constr = Mod_subst.force_constr body in
add_inline_delta_resolver kn (lev, Some constr) l
with Not_found ->
error_no_such_label_sub (con_label con)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 7d542c107..99513319b 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1523,7 +1523,7 @@ and compile_named env sigma auxdefs id =
let compile_constant env sigma prefix ~interactive con body =
match body with
| Def t ->
- let t = Lazyconstr.force t in
+ let t = Mod_subst.force_constr t in
let code = lambda_of_constr env sigma t in
let is_lazy = is_lazy t in
let code = if is_lazy then mk_lazy code else code in
@@ -1628,7 +1628,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
else
let comp_stack, (mind_updates, const_updates) = match cb.const_body with
| Def t ->
- compile_deps env sigma prefix ~interactive init (Lazyconstr.force t)
+ compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
| _ -> init
in
let code, name =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 258f03efd..e6a579c5b 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -639,11 +639,11 @@ and lambda_of_app env sigma f args =
begin match cb.const_body with
| Def csubst ->
if cb.const_inline_code then
- lambda_of_app env sigma (Lazyconstr.force csubst) args
+ lambda_of_app env sigma (Mod_subst.force_constr csubst) args
else
let prefix = get_const_prefix !global_env kn in
let t =
- if is_lazy (Lazyconstr.force csubst) then
+ if is_lazy (Mod_subst.force_constr csubst) then
mkLapp Lforce [|Lconst (prefix, kn)|]
else Lconst (prefix, kn)
in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
new file mode 100644
index 000000000..50208e28a
--- /dev/null
+++ b/kernel/opaqueproof.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Term
+open Mod_subst
+
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context }
+type proofterm = (constr * Univ.constraints) Future.computation
+type opaque =
+ | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
+ | Direct of cooking_info list * proofterm
+ | NoIndirect of substitution list * proofterm
+
+(* hooks *)
+let default_get_opaque dp _ =
+ Errors.error
+ ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+let default_get_univ dp _ =
+ Errors.error
+ ("Cannot access universe constraints of opaque proofs in library " ^
+ DirPath.to_string dp)
+let default_mk_indirect _ = None
+let default_join_indirect_local_opaque _ _ = ()
+let default_join_indirect_local_univ _ _ = ()
+
+let get_opaque = ref default_get_opaque
+let get_univ = ref default_get_univ
+let join_indirect_local_opaque = ref default_join_indirect_local_opaque
+let join_indirect_local_univ = ref default_join_indirect_local_univ
+let mk_indirect = ref default_mk_indirect
+
+let set_indirect_opaque_accessor f = (get_opaque := f)
+let set_indirect_univ_accessor f = (get_univ := f)
+let set_indirect_creator f = (mk_indirect := f)
+let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
+let set_join_indirect_local_univ f = join_indirect_local_univ := f
+let reset_indirect_creator () = mk_indirect := default_mk_indirect
+(* /hooks *)
+
+let create cu = Direct ([],cu)
+
+let turn_indirect o = match o with
+ | Indirect _
+ | NoIndirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+ | Direct (d,cu) ->
+ let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
+ match !mk_indirect (d,cu) with
+ | None -> NoIndirect([],cu)
+ | Some (dp,i) -> Indirect ([],dp,i)
+
+let subst_opaque sub = function
+ | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
+ | NoIndirect (s,uc) -> NoIndirect (sub::s,uc)
+ | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque")
+
+let iter_direct_opaque f = function
+ | Indirect _
+ | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+ | Direct (d,cu) ->
+ Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
+
+let discharge_direct_opaque ~cook_constr ci = function
+ | Indirect _
+ | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+ | Direct (d,cu) ->
+ Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
+
+let join_opaque = function
+ | Direct (_,cu) -> ignore(Future.join cu)
+ | NoIndirect (_,cu) -> ignore(Future.join cu)
+ | Indirect (_,dp,i) ->
+ !join_indirect_local_opaque dp i;
+ !join_indirect_local_univ dp i
+
+let force_proof = function
+ | Direct (_,cu) ->
+ fst(Future.force cu)
+ | NoIndirect (l,cu) ->
+ let c, _ = Future.force cu in
+ force_constr (List.fold_right subst_substituted l (from_val c))
+ | Indirect (l,dp,i) ->
+ let c = Future.force (!get_opaque dp i) in
+ force_constr (List.fold_right subst_substituted l (from_val c))
+
+let force_constraints = function
+ | Direct (_,cu)
+ | NoIndirect(_,cu) -> snd(Future.force cu)
+ | Indirect (_,dp,i) ->
+ match !get_univ dp i with
+ | None -> Univ.empty_constraint
+ | Some u -> Future.force u
+
+let get_constraints = function
+ | Direct (_,cu)
+ | NoIndirect(_,cu) -> Some(Future.chain ~pure:true cu snd)
+ | Indirect (_,dp,i) -> !get_univ dp i
+
+let get_proof = function
+ | Direct (_,cu) -> Future.chain ~pure:true cu fst
+ | NoIndirect(l,cu) ->
+ Future.chain ~pure:true cu (fun (c,_) ->
+ force_constr (List.fold_right subst_substituted l (from_val c)))
+ | Indirect (l,dp,i) ->
+ Future.chain ~pure:true (!get_opaque dp i) (fun c ->
+ force_constr (List.fold_right subst_substituted l (from_val c)))
diff --git a/kernel/lazyconstr.mli b/kernel/opaqueproof.mli
index db4d8fb72..957889aa9 100644
--- a/kernel/lazyconstr.mli
+++ b/kernel/opaqueproof.mli
@@ -10,52 +10,45 @@ open Names
open Term
open Mod_subst
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-type cooking_info = { modlist : work_list; abstract : Context.named_context }
-
-(** [constr_substituted] are [constr] with possibly pending
- substitutions of kernel names. *)
-
-type constr_substituted
+(** This module implements the handling of opaque proof terms.
+ Opauqe proof terms are special since:
+ - they can be lazily computed and substituted
+ - they are stoked in an optionally loaded segment of .vo files
+ An [opaque] proof terms holds the real data until fully discharged.
+ In this case it is called [direct].
+ When it is [turn_indirect] the data is relocated to an opaque table
+ and the [opaque] is turned into an index. *)
-val from_val : constr -> constr_substituted
-val force : constr_substituted -> constr
-val subst_constr_subst :
- substitution -> constr_substituted -> constr_substituted
-
-(** Opaque proof terms might be in some external tables. The
- [force_opaque] function below allows to access these tables,
- this might trigger the read of some extra parts of .vo files *)
-
-type lazy_constr
type proofterm = (constr * Univ.constraints) Future.computation
+type opaque
-(** From a [constr] to some (immediate) [lazy_constr]. *)
-val opaque_from_val : proofterm -> lazy_constr
+(** From a [proofterm] to some [opaque]. *)
+val create : proofterm -> opaque
-(** Turn an immediate [lazy_constr] into an indirect one, thanks
- to the indirect opaque creator configured below. *)
-val turn_indirect : lazy_constr -> lazy_constr
+(** Turn a direct [opaque] into an indirect one, also hashconses constr *)
+val turn_indirect : opaque -> opaque
-(** From a [lazy_constr] back to a [constr]. This might use the
+(** From a [opaque] back to a [constr]. This might use the
indirect opaque accessor configured below. *)
-val force_opaque : lazy_constr -> constr
-val force_opaque_w_constraints : lazy_constr -> constr * Univ.constraints
-val get_opaque_future_constraints :
- lazy_constr -> Univ.constraints Future.computation option
-val get_opaque_futures :
- lazy_constr ->
- Term.constr Future.computation * Univ.constraints Future.computation
+val force_proof : opaque -> constr
+val force_constraints : opaque -> Univ.constraints
+val get_proof : opaque -> Term.constr Future.computation
+val get_constraints : opaque -> Univ.constraints Future.computation option
-val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
+val subst_opaque : substitution -> opaque -> opaque
+val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
-(* val hcons_lazy_constr : lazy_constr -> lazy_constr *)
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context }
-(* Used to discharge the proof term. *)
-val iter_direct_lazy_constr : (constr -> unit) -> lazy_constr -> lazy_constr
-val discharge_direct_lazy_constr : work_list -> Context.named_context -> (constr -> constr) -> lazy_constr -> lazy_constr
+(* The type has two caveats:
+ 1) cook_constr is defined after
+ 2) we have to store the input in the [opaque] in order to be able to
+ discharge it when turning a .vi into a .vo *)
+val discharge_direct_opaque :
+ cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
-val join_lazy_constr : lazy_constr -> unit
+val join_opaque : opaque -> unit
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The following two functions activate
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a93415f92..241e9d565 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -283,8 +283,8 @@ let safe_push_named (id,_,_ as d) env =
let push_named_def (id,de) senv =
let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
let c,cst' = match c with
- | Def c -> Lazyconstr.force c, Univ.empty_constraint
- | OpaqueDef c -> Lazyconstr.force_opaque_w_constraints c
+ | Def c -> Mod_subst.force_constr c, Univ.empty_constraint
+ | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o
| _ -> assert false in
let senv = add_constraints (Now cst') senv in
let senv' = add_constraints (Now cst) senv in
@@ -321,7 +321,7 @@ let constraints_of_sfb = function
match cb.const_body with
| (Undef _ | Def _) -> []
| OpaqueDef lc ->
- match Lazyconstr.get_opaque_future_constraints lc with
+ match Opaqueproof.get_constraints lc with
| None -> []
| Some fc ->
match Future.peek_val fc with
@@ -383,7 +383,7 @@ let add_constant dir l decl senv =
| OpaqueDef lc when DirPath.is_empty dir ->
(* In coqc, opaque constants outside sections will be stored
indirectly in a specific table *)
- { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
+ { cb with const_body = OpaqueDef (Opaqueproof.turn_indirect lc) }
| _ -> cb
in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6cedb6ad2..af4468981 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -290,8 +290,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
| Def lc1 ->
(* NB: cb1 might have been strengthened and appear as transparent.
Anyway [check_conv] will handle that afterwards. *)
- let c1 = Lazyconstr.force lc1 in
- let c2 = Lazyconstr.force lc2 in
+ let c1 = Mod_subst.force_constr lc1 in
+ let c2 = Mod_subst.force_constr lc2 in
check_conv NotConvertibleBodyField cst conv env c1 c2))
| IndType ((kn,i),mind1) ->
ignore (Errors.error (
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f059ea1ae..c86c13e04 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -69,12 +69,12 @@ let handle_side_effects env body side_eff =
match cb.const_body with
| Undef _ -> assert false
| Def b ->
- let b = Lazyconstr.force b in
+ let b = Mod_subst.force_constr b in
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
mkLetIn (cname c, b, b_ty, t)
| OpaqueDef b ->
- let b = Lazyconstr.force_opaque b in
+ let b = Opaqueproof.force_proof b in
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
@@ -108,7 +108,7 @@ let infer_declaration env dcl =
let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
feedback_completion_typecheck feedback_id;
j.uj_val, cst) in
- let def = OpaqueDef (Lazyconstr.opaque_from_val proofterm) in
+ let def = OpaqueDef (Opaqueproof.create proofterm) in
let typ = NonPolymorphicType typ in
def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx
| DefinitionEntry c ->
@@ -120,7 +120,7 @@ let infer_declaration env dcl =
let j = hcons_j j in
let typ, cst = constrain_type env j cst (map_option_typ typ) in
feedback_completion_typecheck feedback_id;
- let def = Def (Lazyconstr.from_val j.uj_val) in
+ let def = Def (Mod_subst.from_val j.uj_val) in
def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
let global_vars_set_constant_type env = function
@@ -159,9 +159,9 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
let ids_typ = global_vars_set_constant_type env typ in
let ids_def = match def with
| Undef _ -> Idset.empty
- | Def cs -> global_vars_set env (Lazyconstr.force cs)
+ | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
| OpaqueDef lc ->
- let vars = global_vars_set env (Lazyconstr.force_opaque lc) in
+ let vars = global_vars_set env (Opaqueproof.force_proof lc) in
!suggest_proof_using kn env vars ids_typ context_ids;
if !Flags.compilation_mode = Flags.BuildVo then
record_aux env ids_typ vars;
@@ -179,12 +179,12 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
| Undef _ as x -> x (* nothing to check *)
| Def cs as x ->
let ids_typ = global_vars_set_constant_type env typ in
- let ids_def = global_vars_set env (Lazyconstr.force cs) in
+ let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
check declared inferred;
x
| OpaqueDef lc -> (* In this case we can postpone the check *)
- OpaqueDef (Lazyconstr.iter_direct_lazy_constr (fun c ->
+ OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
let ids_typ = global_vars_set_constant_type env typ in
let ids_def = global_vars_set env c in
let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 20:26:43 +0000