aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml18
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/dune11
-rw-r--r--kernel/entries.ml5
-rw-r--r--kernel/opaqueproof.ml78
-rw-r--r--kernel/opaqueproof.mli26
-rw-r--r--kernel/safe_typing.ml69
-rw-r--r--kernel/safe_typing.mli10
-rw-r--r--kernel/uint63_amd64_63.ml (renamed from kernel/uint63_amd64.ml)0
-rw-r--r--kernel/uint63_i386_31.ml (renamed from kernel/uint63_x86.ml)0
-rw-r--r--kernel/write_uint63.ml4
11 files changed, 115 insertions, 108 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 620efbafd6..1336e3e8bf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -202,17 +202,21 @@ let lift_univs cb subst auctx0 =
let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
subst, (Polymorphic auctx)
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
- (* For now the STM only handles deferred computation of monomorphic
- constants. The API will need to be adapted when it's not the case
- anymore. *)
- let () = assert (AUContext.is_empty abs_ctx) in
+ let ainst = Instance.of_array (Array.init univs Level.var) in
+ let usubst = Instance.append usubst ainst in
let expmod = expmod_constr_subst cache modlist usubst in
let hyps = Context.Named.map expmod abstract in
let hyps = abstract_context hyps in
- abstract_constant_body (expmod c) hyps
+ let c = abstract_constant_body (expmod c) hyps in
+ univs + AUContext.size abs_ctx, c
+
+let cook_constr infos univs c =
+ let fold info (univs, c) = cook_constr info (univs, c) in
+ let (_, c) = List.fold_right fold infos (univs, c) in
+ c
let cook_constant { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
@@ -227,7 +231,7 @@ let cook_constant { from = cb; info } =
| Undef _ as x -> x
| Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
| OpaqueDef o ->
- OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+ OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
| Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
in
let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index abae3880d7..934b7c6b50 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -28,7 +28,7 @@ type 'opaque result = {
}
val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
val cook_inductive :
Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/dune b/kernel/dune
index 5b23a705ae..4038bf5638 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,7 +3,7 @@
(synopsis "The Coq Kernel")
(public_name coq.kernel)
(wrapped false)
- (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63))
+ (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63))
(libraries lib byterun dynlink))
(executable
@@ -14,15 +14,10 @@
(targets copcodes.ml)
(action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml))))
-(executable
- (name write_uint63)
- (modules write_uint63)
- (libraries unix))
-
(rule
(targets uint63.ml)
- (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml)
- (action (run %{gen})))
+ (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml))
+ (action (copy# %{gen-file} %{targets})))
(documentation
(package coq))
diff --git a/kernel/entries.ml b/kernel/entries.ml
index adb3f6bd29..45b11e97ba 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -107,8 +107,3 @@ type module_entry =
| MType of module_params_entry * module_struct_entry
| MExpr of
module_params_entry * module_struct_entry * module_struct_entry option
-
-(** Not used by the kernel. *)
-type side_effect_role =
- | Subproof
- | Schema of inductive * string
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 1971c67c61..e18b726111 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,19 +16,22 @@ open Mod_subst
type work_list = (Instance.t * Id.t array) Cmap.t *
(Instance.t * Id.t array) Mindmap.t
+type cooking_info = {
+ modlist : work_list;
+ abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
type indirect_accessor = {
access_proof : DirPath.t -> int -> constr option;
+ access_discharge : cooking_info list -> int -> constr -> constr;
}
-type cooking_info = {
- modlist : work_list;
- abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type universes = int
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
- | Direct of cooking_info list * proofterm
+ | Direct of universes * cooking_info list * proofterm
type opaquetab = {
- opaque_val : (cooking_info list * proofterm) Int.Map.t;
+ opaque_val : (int * cooking_info list * proofterm) Int.Map.t;
(** Actual proof terms *)
opaque_len : int;
(** Size of the above map *)
@@ -43,14 +46,14 @@ let empty_opaquetab = {
let not_here () =
CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
-let create cu = Direct ([],cu)
+let create ~univs cu = Direct (univs, [],cu)
let turn_indirect dp o tab = match o with
| Indirect (_,_,i) ->
if not (Int.Map.mem i tab.opaque_val)
then CErrors.anomaly (Pp.str "Indirect in a different table.")
else CErrors.anomaly (Pp.str "Already an indirect opaque.")
- | Direct (d,cu) ->
+ | Direct (nunivs, d, cu) ->
(* Invariant: direct opaques only exist inside sections, we turn them
indirect as soon as we are at toplevel. At this moment, we perform
hashconsing of their contents, potentially as a future. *)
@@ -61,7 +64,7 @@ let turn_indirect dp o tab = match o with
in
let cu = Future.chain cu hcons in
let id = tab.opaque_len in
- let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+ let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in
let opaque_dir =
if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
else if DirPath.equal tab.opaque_dir DirPath.initial then dp
@@ -74,10 +77,10 @@ let subst_opaque sub = function
| Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
| Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
-let discharge_direct_opaque ~cook_constr ci = function
+let discharge_direct_opaque ci = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
- | Direct (d,cu) ->
- Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
+ | Direct (n, d, cu) ->
+ Direct (n, ci :: d, cu)
let join except cu = match except with
| None -> ignore (Future.join cu)
@@ -86,54 +89,61 @@ let join except cu = match except with
else ignore (Future.join cu)
let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> join except cu
+ | Direct (_,_,cu) -> join except cu
| Indirect (_,dp,i) ->
if DirPath.equal dp odp then
- let fp = snd (Int.Map.find i prfs) in
+ let (_, _, fp) = Int.Map.find i prfs in
join except fp
let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) ->
- fst(Future.force cu)
+ | Direct (n, d, cu) ->
+ let (c, _) = Future.force cu in
+ access.access_discharge d n c
| Indirect (l,dp,i) ->
- let pt =
+ let c =
if DirPath.equal dp odp
- then Future.chain (snd (Int.Map.find i prfs)) fst
+ then
+ let (n, d, cu) = Int.Map.find i prfs in
+ let (c, _) = Future.force cu in
+ access.access_discharge d n c
else match access.access_proof dp i with
| None -> not_here ()
- | Some v -> Future.from_val v
+ | Some v -> v
in
- let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> snd(Future.force cu)
+ | Direct (_,_,cu) ->
+ snd(Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
- then snd (Future.force (snd (Int.Map.find i prfs)))
+ then
+ let (_, _, cu) = Int.Map.find i prfs in
+ snd (Future.force cu)
else Univ.ContextSet.empty
let get_direct_constraints = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, cu) -> Future.chain cu snd
+| Direct (_, _, cu) -> Future.chain cu snd
module FMap = Future.UUIDMap
let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
- let opaque_table = Array.make n None in
- let disch_table = Array.make n [] in
+ let opaque_table = Array.make n ([], 0, None) in
let f2t_map = ref FMap.empty in
- let iter n (d, cu) =
+ let iter n (univs, d, cu) =
let uid = Future.uuid cu in
let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
- if Future.is_val cu then
- let (c, _) = Future.force cu in
- opaque_table.(n) <- Some c
- else if Future.UUIDSet.mem uid except then
- disch_table.(n) <- d
- else
- CErrors.anomaly
- Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+ let c =
+ if Future.is_val cu then
+ let (c, _) = Future.force cu in
+ Some c
+ else if Future.UUIDSet.mem uid except then None
+ else
+ CErrors.anomaly
+ Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+ in
+ opaque_table.(n) <- (d, univs, c)
in
let () = Int.Map.iter iter otab in
- opaque_table, disch_table, !f2t_map
+ opaque_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 46b0500507..6e275649cd 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,15 +28,23 @@ type opaque
val empty_opaquetab : opaquetab
(** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
+val create : univs:int -> proofterm -> opaque
(** Turn a direct [opaque] into an indirect one. It is your responsibility to
hashcons the inner term beforehand. The integer is an hint of the maximum id
used so far *)
val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
+type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
+ (Univ.Instance.t * Id.t array) Mindmap.t
+
+type cooking_info = {
+ modlist : work_list;
+ abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
type indirect_accessor = {
access_proof : DirPath.t -> int -> constr option;
+ access_discharge : cooking_info list -> int -> constr -> constr;
}
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The two functions above activate
@@ -51,23 +59,11 @@ val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
val subst_opaque : substitution -> opaque -> opaque
-type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
- (Univ.Instance.t * Id.t array) Mindmap.t
-
-type cooking_info = {
- modlist : work_list;
- abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
-
-(* 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
+ cooking_info -> opaque -> opaque
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : ?except:Future.UUIDSet.t -> opaquetab ->
- Constr.t option array *
- cooking_info list array *
+ (cooking_info list * int * Constr.t option) array *
int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9f7466902d..0b0f14eee7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -231,8 +231,7 @@ let check_engagement env expected_impredicative_set =
type side_effect = {
from_env : Declarations.structure_body CEphemeron.key;
seff_constant : Constant.t;
- seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body;
- seff_role : Entries.side_effect_role;
+ seff_body : Constr.t Declarations.constant_body;
}
module SideEffects :
@@ -299,11 +298,6 @@ let concat_private = SideEffects.concat
let universes_of_private eff =
let fold acc eff =
- let acc = match eff.seff_body.const_body with
- | Def _ -> acc
- | OpaqueDef (_, ctx) -> ctx :: acc
- | Primitive _ | Undef _ -> assert false
- in
match eff.seff_body.const_universes with
| Monomorphic ctx -> ctx :: acc
| Polymorphic _ -> acc
@@ -541,8 +535,7 @@ type 'a effect_entry =
type global_declaration =
| ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-type exported_private_constant =
- Constant.t * Entries.side_effect_role
+type exported_private_constant = Constant.t
let add_constant_aux ~in_section senv (kn, cb) =
let l = Constant.label kn in
@@ -601,7 +594,7 @@ let inline_side_effects env body side_eff =
let fold (subst, var, ctx, args) (c, cb) =
let (b, opaque) = match cb.const_body with
| Def b -> (Mod_subst.force_constr b, false)
- | OpaqueDef (b, _) -> (b, true)
+ | OpaqueDef b -> (b, true)
| _ -> assert false
in
match cb.const_universes with
@@ -689,13 +682,13 @@ let constant_entry_of_side_effect eff =
| Polymorphic auctx ->
Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
in
- let pt =
+ let p =
match cb.const_body with
- | OpaqueDef (b, c) -> b, c
- | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty
+ | OpaqueDef b -> b
+ | Def b -> Mod_subst.force_constr b
| _ -> assert false in
DefinitionEntry {
- const_entry_body = Future.from_val (pt, ());
+ const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
const_entry_secctx = None;
const_entry_feedback = None;
const_entry_type = Some cb.const_type;
@@ -704,7 +697,7 @@ let constant_entry_of_side_effect eff =
const_entry_inline_code = cb.const_inline_code }
let export_eff eff =
- (eff.seff_constant, eff.seff_body, eff.seff_role)
+ (eff.seff_constant, eff.seff_body)
let export_side_effects mb env (b_ctx, eff) =
let not_exists e =
@@ -721,11 +714,6 @@ let export_side_effects mb env (b_ctx, eff) =
match cb.const_universes with
| Polymorphic _ -> env
| Monomorphic ctx ->
- let ctx = match eff.seff_body.const_body with
- | Def _ -> ctx
- | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx
- | Undef _ | Primitive _ -> assert false
- in
Environ.push_context_set ~strict:true ctx env
in
let rec translate_seff sl seff acc env =
@@ -737,7 +725,12 @@ let export_side_effects mb env (b_ctx, eff) =
let kn = eff.seff_constant in
let ce = constant_entry_of_side_effect eff in
let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
- let cb = map_constant Future.force cb in
+ let map cu =
+ let (c, u) = Future.force cu in
+ let () = assert (Univ.ContextSet.is_empty u) in
+ c
+ in
+ let cb = map_constant map cb in
let eff = { eff with seff_body = cb } in
(push_seff env eff, export_eff eff)
in
@@ -749,11 +742,15 @@ let export_side_effects mb env (b_ctx, eff) =
in
translate_seff trusted seff [] env
+let n_univs cb = match cb.const_universes with
+| Monomorphic _ -> 0
+| Polymorphic auctx -> Univ.AUContext.size auctx
+
let export_private_constants ~in_section ce senv =
let exported, ce = export_side_effects senv.revstruct senv.env ce in
- let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in
+ let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
let bodies = List.map map exported in
- let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
+ let exported = List.map (fun (kn, _) -> kn) exported in
let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
(ce, exported), senv
@@ -763,7 +760,7 @@ let add_recipe ~in_section l r senv =
let senv = add_constant_aux ~in_section senv (kn, cb) in
kn, senv
-let add_constant ?role ~in_section l decl senv =
+let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
let kn = Constant.make2 senv.modpath l in
let cb =
match decl with
@@ -778,7 +775,7 @@ let add_constant ?role ~in_section l decl senv =
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
in
let senv =
- let cb = map_constant Opaqueproof.create cb in
+ let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
add_constant_aux ~in_section senv (kn, cb) in
let senv =
match decl with
@@ -787,16 +784,28 @@ let add_constant ?role ~in_section l decl senv =
add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
| _ -> senv
in
- let eff = match role with
- | None -> empty_private_constants
- | Some role ->
- let cb = map_constant Future.force cb in
+ let eff : a = match side_effect with
+ | PureEntry -> ()
+ | EffectEntry ->
+ let body, univs = match cb.const_body with
+ | (Primitive _ | Undef _) -> assert false
+ | Def c -> (Def c, cb.const_universes)
+ | OpaqueDef o ->
+ let (b, ctx) = Future.force o in
+ match cb.const_universes with
+ | Monomorphic ctx' ->
+ OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
+ | Polymorphic auctx ->
+ (* Upper layers enforce that there are no internal constraints *)
+ let () = assert (Univ.ContextSet.is_empty ctx) in
+ OpaqueDef b, Polymorphic auctx
+ in
+ let cb = { cb with const_body = body; const_universes = univs } in
let from_env = CEphemeron.create senv.revstruct in
let eff = {
from_env = from_env;
seff_constant = kn;
seff_body = cb;
- seff_role = role;
} in
SideEffects.add eff empty_private_constants
in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 770caf5406..3e902303c3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -87,18 +87,16 @@ type 'a effect_entry =
type global_declaration =
| ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-type exported_private_constant =
- Constant.t * Entries.side_effect_role
+type exported_private_constant = Constant.t
val export_private_constants : in_section:bool ->
private_constants Entries.proof_output ->
(Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
-(** returns the main constant plus a list of auxiliary constants (empty
- unless one requires the side effects to be exported) *)
+(** returns the main constant plus a certificate of its validity *)
val add_constant :
- ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
- (Constant.t * private_constants) safe_transformer
+ side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
+ (Constant.t * 'a) safe_transformer
val add_recipe :
in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64_63.ml
index 2d4d685775..2d4d685775 100644
--- a/kernel/uint63_amd64.ml
+++ b/kernel/uint63_amd64_63.ml
diff --git a/kernel/uint63_x86.ml b/kernel/uint63_i386_31.ml
index fa45c90241..fa45c90241 100644
--- a/kernel/uint63_x86.ml
+++ b/kernel/uint63_i386_31.ml
diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml
index beb59ce205..42bb5dfbb1 100644
--- a/kernel/write_uint63.ml
+++ b/kernel/write_uint63.ml
@@ -31,8 +31,8 @@ let ml_file_copy input output =
let write_uint63 () =
ml_file_copy
- (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml"
- else (* 64 bits *) "uint63_amd64.ml")
+ (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml"
+ else (* 64 bits *) "uint63_amd64_63.ml")
"uint63.ml"
let () = write_uint63 ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:15:02 +0000