From a69bb15b1d76b71628b61bc42eb8d79c098074a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Jun 2019 12:27:37 +0200 Subject: Merge universe quantification and delayed constraints in opaque proofs. This enforces more invariants statically. --- kernel/cooking.ml | 33 ++++++++++++++-------------- kernel/cooking.mli | 2 +- kernel/opaqueproof.ml | 58 ++++++++++++++++++++++---------------------------- kernel/opaqueproof.mli | 9 ++++---- kernel/safe_typing.ml | 19 +++++++---------- kernel/term_typing.ml | 4 ++-- 6 files changed, 59 insertions(+), 66 deletions(-) (limited to 'kernel') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index fbc0822570..4e1917eb1d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -201,29 +201,30 @@ 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 } (univs, (c, priv)) = +let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) = let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract 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 - let c = abstract_constant_body (expmod c) hyps in - let priv = match priv with + let usubst, priv = match priv with | Opaqueproof.PrivateMonomorphic () -> let () = assert (AUContext.is_empty abs_ctx) in - priv - | Opaqueproof.PrivatePolymorphic ctx -> + let () = assert (Instance.is_empty usubst) in + usubst, priv + | Opaqueproof.PrivatePolymorphic (univs, ctx) -> + let ainst = Instance.of_array (Array.init univs Level.var) in + let usubst = Instance.append usubst ainst in let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in - Opaqueproof.PrivatePolymorphic ctx + let univs = univs + AUContext.size abs_ctx in + usubst, Opaqueproof.PrivatePolymorphic (univs, ctx) in - univs + AUContext.size abs_ctx, (c, priv) + let expmod = expmod_constr_subst cache modlist usubst in + let hyps = Context.Named.map expmod abstract in + let hyps = abstract_context hyps in + let c = abstract_constant_body (expmod c) hyps in + (c, priv) -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_constr infos c = + let fold info c = cook_constr info c in + List.fold_right fold infos c let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in diff --git a/kernel/cooking.mli b/kernel/cooking.mli index c98fb0bc3a..b22eff7c32 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -27,7 +27,7 @@ type 'opaque result = { } val cook_constant : recipe -> Opaqueproof.opaque result -val cook_constr : Opaqueproof.cooking_info list -> int -> +val cook_constr : Opaqueproof.cooking_info list -> (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) val cook_inductive : diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 66c50c4b57..bbc90ef9db 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -22,13 +22,13 @@ type cooking_info = { type 'a delayed_universes = | PrivateMonomorphic of 'a -| PrivatePolymorphic of Univ.ContextSet.t +| PrivatePolymorphic of int * Univ.ContextSet.t -type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; - access_discharge : cooking_info list -> int -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); + access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } let drop_mono = function @@ -36,13 +36,12 @@ let drop_mono = function | PrivatePolymorphic _ as ctx -> ctx type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation -type universes = int type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) - | Direct of universes * cooking_info list * proofterm + | Direct of cooking_info list * proofterm type opaquetab = { - opaque_val : (int * cooking_info list * proofterm) Int.Map.t; + opaque_val : (cooking_info list * proofterm) Int.Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) @@ -57,14 +56,14 @@ let empty_opaquetab = { let not_here () = CErrors.user_err Pp.(str "Cannot access opaque delayed proof") -let create ~univs cu = Direct (univs, [],cu) +let create cu = Direct ([],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 (nunivs, d, cu) -> + | Direct (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. *) @@ -72,13 +71,13 @@ let turn_indirect dp o tab = match o with let c = Constr.hcons c in let u = match u with | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) - | PrivatePolymorphic u -> PrivatePolymorphic (Univ.hcons_universe_context_set u) + | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) in (c, u) in let cu = Future.chain cu hcons in let id = tab.opaque_len in - let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in + let opaque_val = Int.Map.add id (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 @@ -93,8 +92,8 @@ let subst_opaque sub = function let discharge_direct_opaque ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (n, d, cu) -> - Direct (n, ci :: d, cu) + | Direct (d, cu) -> + Direct (ci :: d, cu) let join except cu = match except with | None -> ignore (Future.join cu) @@ -103,28 +102,28 @@ 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) = 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 (n, d, cu) -> + | Direct (d, cu) -> let (c, u) = Future.force cu in - access.access_discharge d n (c, drop_mono u) + access.access_discharge d (c, drop_mono u) | Indirect (l,dp,i) -> let c, u = if DirPath.equal dp odp then - let (n, d, cu) = Int.Map.find i prfs in + let (d, cu) = Int.Map.find i prfs in let (c, u) = Future.force cu in - access.access_discharge d n (c, drop_mono u) + access.access_discharge d (c, drop_mono u) else - let (n, d, cu) = access.access_proof dp i in + let (d, cu) = access.access_proof dp i in match cu with | None -> not_here () - | Some (c, u) -> access.access_discharge n d (c, u) + | Some (c, u) -> access.access_discharge d (c, u) in let c = force_constr (List.fold_right subst_substituted l (from_val c)) in (c, u) @@ -134,44 +133,39 @@ let get_mono (_, u) = match u with | PrivatePolymorphic _ -> Univ.ContextSet.empty let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,_,cu) -> + | Direct (_,cu) -> get_mono (Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then - let (_, _, cu) = Int.Map.find i prfs in + let ( _, cu) = Int.Map.find i prfs in get_mono (Future.force cu) else Univ.ContextSet.empty let get_direct_constraints = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") -| Direct (_, _, cu) -> +| Direct (_, cu) -> Future.chain cu get_mono module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n ([], 0, None) in + let opaque_table = Array.make n ([], None) in let f2t_map = ref FMap.empty in - let iter n (univs, d, cu) = + let iter n (d, cu) = let uid = Future.uuid cu in let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in let c = if Future.is_val cu then let (c, priv) = Future.force cu in - let priv = match priv with - | PrivateMonomorphic _ -> - let () = assert (Int.equal univs 0) in - PrivateMonomorphic () - | PrivatePolymorphic _ as priv -> priv - in + let priv = drop_mono priv in Some (c, priv) 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) + opaque_table.(n) <- (d, c) in let () = Int.Map.iter iter otab in opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 20c862c651..8b844e0812 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -23,7 +23,8 @@ open Mod_subst type 'a delayed_universes = | PrivateMonomorphic of 'a -| PrivatePolymorphic of Univ.ContextSet.t +| PrivatePolymorphic of int * Univ.ContextSet.t + (** Number of surrounding bound universes + local constraints *) type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaquetab @@ -32,7 +33,7 @@ type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : univs:int -> proofterm -> opaque +val create : 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 @@ -46,11 +47,11 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; - access_discharge : cooking_info list -> int -> + access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } (** When stored indirectly, opaque terms are indexed by their library diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 596fcd210c..7e7734b247 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -728,7 +728,8 @@ let export_side_effects mb env (b_ctx, eff) = let map cu = let (c, u) = Future.force cu in let () = match u with - | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx -> + | Opaqueproof.PrivateMonomorphic ctx + | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) in c @@ -748,11 +749,11 @@ let export_side_effects mb env (b_ctx, eff) = let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in let map univs p = - let univs, local = match univs with - | Monomorphic _ -> 0, Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty - | Polymorphic auctx -> Univ.AUContext.size auctx, Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty + let local = match univs with + | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty + | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) in - Opaqueproof.create ~univs (Future.from_val (p, local)) + Opaqueproof.create (Future.from_val (p, local)) in let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in let bodies = List.map map exported in @@ -781,11 +782,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let univs = match cb.const_universes with - | Monomorphic _ -> 0 - | Polymorphic auctx -> Univ.AUContext.size auctx - in - let cb = map_constant (fun c -> Opaqueproof.create ~univs c) cb in + let cb = map_constant (fun c -> Opaqueproof.create c) cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -805,7 +802,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen match cb.const_universes, delayed with | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') - | Polymorphic auctx, Opaqueproof.PrivatePolymorphic ctx -> + | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> (* Upper layers enforce that there are no internal constraints *) let () = assert (Univ.ContextSet.is_empty ctx) in OpaqueDef b, Polymorphic auctx diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9ec3269375..6c065292d4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -181,7 +181,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let _ = Typeops.judge_of_cast env j DEFAULTcast tj in let def = Vars.subst_univs_level_constr usubst j.uj_val in let () = feedback_completion_typecheck feedback_id in - def, Opaqueproof.PrivatePolymorphic private_univs + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) end in let def = OpaqueDef proofterm in let typ = Vars.subst_univs_level_constr usubst tj.utj_val in @@ -402,7 +402,7 @@ let translate_local_def env _id centry = the body by virtue of the typing of [Entries.section_def_entry]. *) let () = match cst with | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) - | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) in p | Undef _ | Primitive _ -> assert false -- cgit v1.2.3