diff options
Diffstat (limited to 'kernel/term_typing.ml')
-rw-r--r-- | kernel/term_typing.ml | 148 |
1 files changed, 100 insertions, 48 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cf82d54ec..43c099712 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -77,6 +77,10 @@ end type side_effects = SideEffects.t +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + let uniq_seff_rev = SideEffects.repr let uniq_seff l = List.rev (SideEffects.repr l) @@ -232,7 +236,7 @@ let abstract_constant_universes abstract uctx = let sbst, auctx = Univ.abstract_universes uctx in sbst, Polymorphic_const auctx -let infer_declaration ~trust env kn dcl = +let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -243,7 +247,14 @@ let infer_declaration ~trust env kn dcl = in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, univs, false, ctx + { + Cooking.cook_body = Undef nl; + cook_type = RegularArity t; + cook_proj = None; + cook_universes = univs; + cook_inline = false; + cook_context = ctx; + } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -251,46 +262,65 @@ let infer_declaration ~trust env kn dcl = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_polymorphic = false} as c) -> - let env = push_context ~strict:true c.const_entry_universes env in + const_entry_universes = Monomorphic_const_entry univs } as c) -> + let env = push_context ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> - let body, uctx, signatures = - inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in - let env = push_context_set uctx env in - let j = + let j, uctx = match trust with + | Pure -> + let env = push_context_set uctx env in + let j = infer env body in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + | SideEffects mb -> + let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in + let valid_signatures = check_signatures mb signatures in + let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in - unzip ectx j in - let _ = judge_of_cast env j DEFAULTcast tyj in + let j = unzip ectx j in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + in let c = hcons_constr j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, - (Monomorphic_const c.const_entry_universes), - c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = RegularArity typ; + cook_proj = None; + cook_universes = Monomorphic_const univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx, _ = inline_side_effects env body - (Univ.ContextSet.union univsctx ctx) side_eff in - let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in - let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let poly, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> false, univs + | Polymorphic_const_entry univs -> true, univs + in + let univsctx = Univ.ContextSet.of_context univs in + let ctx = Univ.ContextSet.union univsctx ctx in + let body, ctx, _ = match trust with + | Pure -> body, ctx, [] + | SideEffects _ -> inline_side_effects env body ctx side_eff + in + let env = push_context_set ~strict:(not poly) ctx env in + let abstract = poly && not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in let typ = match typ with | None -> - if not c.const_entry_polymorphic then (* Old-style polymorphism *) + if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) | Some t -> @@ -304,7 +334,14 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -324,8 +361,14 @@ let infer_declaration ~trust env kn dcl = Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) in let term, typ = pb.proj_eta in - Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - univs, false, None + { + Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term)); + cook_type = RegularArity typ; + cook_proj = Some pb; + cook_universes = univs; + cook_inline = false; + cook_context = None; + } let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -349,7 +392,9 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = +let build_constant_declaration kn env result = + let open Cooking in + let typ = result.cook_type in let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -376,7 +421,8 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in - match ctx with + let def = result.cook_body in + match result.cook_context with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -419,9 +465,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in + let univs = result.cook_universes in let tps = let res = - match proj with + match result.cook_proj with | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because @@ -434,10 +481,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = None; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env; } in @@ -448,10 +495,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } (*s Global and local constant declaration. *) @@ -461,11 +508,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = - let poly, univs = + let univs = match cb.const_universes with - | Monomorphic_const ctx -> false, ctx + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx | Polymorphic_const auctx -> - true, Univ.AUContext.repr auctx + Polymorphic_const_entry (Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -473,12 +521,11 @@ let constant_entry_of_side_effect cb u = | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, empty_seff); + const_entry_body = Future.from_val (pt, ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } @@ -497,17 +544,18 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * side_effect_role let export_side_effects mb env ce = match ce with - | ParameterEntry _ | ProjectionEntry _ -> [], ce + | ParameterEntry e -> [], ParameterEntry e + | ProjectionEntry e -> [], ProjectionEntry e | DefinitionEntry c -> let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~pure:true body - (fun (b_ctx, _) -> b_ctx, empty_seff) } in + (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -547,8 +595,8 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + let cb = translate_constant Pure env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env | Some sl, cbs :: rest -> @@ -556,7 +604,7 @@ let export_side_effects mb env ce = let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, constant_entry_of_side_effect cb u, r) cbs in + kn, cb, r) cbs in translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env in translate_seff trusted seff [] env @@ -575,11 +623,11 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,univs,inline_code,ctx = - infer_declaration ~trust:mb env None (DefinitionEntry centry) in - let typ = type_of_constant_type env typ in - if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin - match def with + let open Cooking in + let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let typ = type_of_constant_type env decl.cook_type in + if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin + match decl.cook_body with | Undef _ -> () | Def _ -> () | OpaqueDef lc -> @@ -592,7 +640,11 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; - def, typ, univs + let univs = match decl.cook_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const _ -> assert false + in + decl.cook_body, typ, univs (* Insertion of inductive types. *) @@ -602,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), empty_seff); + (body, ctx'), ()); } let inline_side_effects env body side_eff = |