diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/opaqueproof.ml | 9 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 26 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 4 |
4 files changed, 19 insertions, 22 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 423a416ca4..18c1bcc0f8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -77,11 +77,6 @@ let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") -let iter_direct_opaque f = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) - let discharge_direct_opaque ~cook_constr ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> @@ -100,10 +95,6 @@ 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_direct = function -| Direct (_, cu) -> Future.force cu -| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> fst(Future.force cu) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 8b6e8a1c8f..4e8956af06 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -39,12 +39,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab indirect opaque accessor configured below. *) val force_proof : opaquetab -> opaque -> constr val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t -val force_direct : opaque -> (constr * Univ.ContextSet.t) val get_constraints : opaquetab -> opaque -> Univ.ContextSet.t Future.computation option val subst_opaque : substitution -> opaque -> opaque -val iter_direct_opaque : (constr -> unit) -> opaque -> opaque type work_list = (Univ.Instance.t * Id.t array) Cmap.t * (Univ.Instance.t * Id.t array) Mindmap.t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9e33b431fc..74c6189a65 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -232,7 +232,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration ~force ~iter env result = +let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -271,7 +271,7 @@ let build_constant_declaration ~force ~iter env result = | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let (lc, _) = force lc in + let (lc, _) = Future.force lc in let vars = global_vars_set env lc in if !Flags.record_aux_file then record_aux env ids_typ vars; vars @@ -293,6 +293,7 @@ let build_constant_declaration ~force ~iter env result = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) + let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in let kont c = let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in @@ -319,9 +320,7 @@ let build_constant_declaration ~force ~iter env result = (*s Global and local constant declaration. *) let translate_constant mb env _kn ce = - let force cu = Future.force cu in - let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in - build_constant_declaration ~force ~iter env + build_constant_declaration env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -330,9 +329,20 @@ let translate_local_assum env t = j.uj_val, t let translate_recipe ~hcons env _kn r = - let force o = Opaqueproof.force_direct o in - let iter k o = Opaqueproof.iter_direct_opaque k o in - build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r) + let open Cooking in + let result = Cooking.cook_constant ~hcons 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 + { const_hyps = Option.get result.cook_context; + const_body = result.cook_body; + const_type = result.cook_type; + const_body_code = tps; + const_universes = univs; + const_private_poly_univs = result.cook_private_univs; + const_relevance = result.cook_relevance; + const_inline_code = result.cook_inline; + const_typing_flags = Environ.typing_flags env } let translate_local_def env _id centry = let open Cooking in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index a046d26ea9..592a97e132 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -43,6 +43,4 @@ val infer_declaration : trust:'a trust -> env -> 'a constant_entry -> Opaqueproof.proofterm Cooking.result val build_constant_declaration : - force:('a -> constr * 'b) -> - iter:((constr -> unit) -> 'a -> 'a) -> - env -> 'a Cooking.result -> 'a constant_body + env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |