diff options
| -rw-r--r-- | kernel/cooking.ml | 7 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/opaqueproof.ml | 13 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 5 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 12 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 2 |
6 files changed, 22 insertions, 19 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9b6e37251f..13851319cd 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -212,7 +212,7 @@ let lift_univs cb subst auctx0 = let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in subst, (Polymorphic (AUContext.union auctx0 auctx')) -let cook_constant ~hcons { from = cb; info } = +let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in @@ -220,10 +220,7 @@ let cook_constant ~hcons { from = cb; info } = let expmod = expmod_constr_subst cache modlist usubst in let hyps0 = Context.Named.map expmod abstract in let hyps = abstract_context hyps0 in - let map c = - let c = abstract_constant_body (expmod c) hyps in - if hcons then Constr.hcons c else c - in + let map c = abstract_constant_body (expmod c) hyps in let body = on_body modlist (hyps0, usubst, abs_ctx) map cb.const_body diff --git a/kernel/cooking.mli b/kernel/cooking.mli index b022e2ac09..024eed1285 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -27,7 +27,7 @@ type 'opaque result = { cook_context : Constr.named_context option; } -val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result +val cook_constant : recipe -> Opaqueproof.opaque result val cook_constr : Opaqueproof.cooking_info -> constr -> constr (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 75f96da3eb..0ff27eb4ea 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -52,10 +52,15 @@ let turn_indirect dp o tab = match o with then CErrors.anomaly (Pp.str "Indirect in a different table.") else CErrors.anomaly (Pp.str "Already an indirect opaque.") | Direct (d,cu) -> - (** Uncomment to check dynamically that all terms turned into - indirections are hashconsed. *) -(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *) -(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *) + (* 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. *) + let hcons (c, u) = + let c = Constr.hcons c in + let u = 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 (d,cu) tab.opaque_val in let opaque_dir = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 873cc2a172..eb03854af4 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -555,6 +555,8 @@ let add_constant_aux ~in_section senv (kn, cb) = end | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] in + (* This is the only place where we hashcons the contents of a constant body *) + let cb = if in_section then cb else Declareops.hcons_const_body cb in let cb, otab = match cb.const_body with | OpaqueDef lc when not in_section -> (* In coqc, opaque constants outside sections will be stored @@ -771,8 +773,7 @@ let export_private_constants ~in_section ce senv = let add_recipe ~in_section l r senv = let kn = Constant.make2 senv.modpath l in - let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in - let cb = if in_section then cb else Declareops.hcons_const_body cb in + let cb = Term_typing.translate_recipe senv.env kn r in let senv = add_constant_aux ~in_section senv (kn, cb) in kn, senv diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 74c6189a65..088dd98db8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -74,7 +74,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let j = Typeops.infer env t in let usubst, univs = Declareops.abstract_universes uctx in let r = Typeops.assumption_of_judgment env j in - let t = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in + let t = Vars.subst_univs_level_constr usubst j.uj_val in { Cooking.cook_body = Undef nl; cook_type = t; @@ -95,7 +95,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | Some typ -> let typ = Typeops.infer_type env typ in Typeops.check_primitive_type env op_t typ.utj_val; - Constr.hcons typ.utj_val + typ.utj_val | None -> match op_t with | CPrimitives.OT_op op -> Typeops.type_of_prim env op @@ -151,7 +151,7 @@ the polymorphic case let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in j, uctx in - let c = Constr.hcons j.uj_val in + let c = j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef proofterm in @@ -205,7 +205,7 @@ the polymorphic case let _ = Typeops.judge_of_cast env j DEFAULTcast tj in Vars.subst_univs_level_constr usubst tj.utj_val in - let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in + let def = Vars.subst_univs_level_constr usubst j.uj_val in let def = if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) else Def (Mod_subst.from_val def) @@ -328,9 +328,9 @@ let translate_local_assum env t = let t = Typeops.assumption_of_judgment env j in j.uj_val, t -let translate_recipe ~hcons env _kn r = +let translate_recipe env _kn r = let open Cooking in - let result = Cooking.cook_constant ~hcons r in + let result = Cooking.cook_constant r in let univs = result.cook_universes in let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in let tps = Option.map Cemitcodes.from_val res in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 592a97e132..fd0f2a18e4 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -35,7 +35,7 @@ val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> Opaqueproof.proofterm constant_body -val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body +val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body (** Internal functions, mentioned here for debug purpose only *) |