Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of the Coq module system *)
(* This module provides the main entry points for type-checking basic declarations *)
open Utilopen Namesopen Constropen Declarationsopen Environopen Entriesopen UVars
module NamedDecl = Context.Named.Declaration
(* Checks the section variables for the body. Returns the closure of the union with the variables in the type.*)let check_section_variables env declared_vars body typ = let env_ids = ids_of_named_context_val (named_context_val env) in Id.Set.iter (fun id -> if not (Id.Set.mem id env_ids) then Type_errors.error_unbound_var env id) declared_vars; if List.is_empty (named_context env) then begin assert (Id.Set.is_empty declared_vars); declared_vars end else let type_vars = global_vars_set env typ in let declared_vars = Environ.really_needed env (Id.Set.union declared_vars type_vars) in let () = match body with | None -> () | Some body -> let ids_def = global_vars_set env body in let inferred_vars = Environ.really_needed env (Id.Set.union type_vars ids_def) in if not (Id.Set.subset inferred_vars declared_vars) then Type_errors.error_undeclared_used_variables env ~declared_vars ~type_vars ~inferred_vars in declared_vars
let compute_section_variables env body typ = if List.is_empty (named_context env) then (* Empty section context: optimization *) Id.Set.empty else let ids = Option.fold_right (fun c -> Id.Set.union (global_vars_set env c)) body (global_vars_set env typ) in Environ.really_needed env ids
let used_section_variables env declared_hyps body typ = let hyps = match declared_hyps with | None -> compute_section_variables env body typ | Some declared -> check_section_variables env declared body typ in (* Order the variables *) List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env)
(* Insertion of constants and parameters in environment. *)
type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
let skip_trusted_seff sl b e = let rec aux sl b e = let open Context.Rel.Declaration in if Int.equal sl 0 then b, e else match HConstr.kind b with | LetIn (n,c,ty,bo) -> let c = HConstr.self c in let ty = HConstr.self ty in aux (sl - 1) bo (Environ.push_rel (LocalDef (n,c,ty)) e) | App (hd, args) -> let () = assert (Int.equal (Array.length args) 1) in begin match HConstr.kind hd with | Lambda (n,ty,bo) -> let ty = HConstr.self ty in aux (sl - 1) bo (Environ.push_rel (LocalAssum (n,ty)) e) | _ -> assert false end | _ -> assert false in aux sl b e
type typing_context = TyCtx of Environ.env * unsafe_type_judgment * Id.Set.t * universes
let process_universes env = function | Entries.Monomorphic_entry -> env, UVars.Instance.empty, Monomorphic | Entries.Polymorphic_entry auctx -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let ctx = AbstractContext.repr auctx in let () = check_ucontext ctx env in let env = Environ.push_context ~strict:false ctx env in env, UVars.make_abstract_instance auctx, Polymorphic auctx
let check_primitive_type env op_t u t = let inft = Typeops.type_of_prim_or_type env u op_t in match Conversion.default_conv Conversion.CONV env inft t with | Result.Ok () -> () | Result.Error () -> Type_errors.error_incorrect_primitive env (make_judge op_t inft) t
let adjust_primitive_univ_entry p auctx = function | Monomorphic_entry -> assert (AbstractContext.is_empty auctx); (* ensured by ComPrimitive *) Monomorphic_entry | Polymorphic_entry uctx -> assert (not (AbstractContext.is_empty auctx)); (* ensured by ComPrimitive *) (* [push_context] will check that the universes aren't repeated in the instance so comparing the sizes works. No polymorphic primitive uses constraints currently. *) if not (AbstractContext.size auctx = AbstractContext.size uctx && PConstraints.is_empty (AbstractContext.constraints uctx)) then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++ str (CPrimitives.op_or_type_to_string p)); Polymorphic_entry (AbstractContext.refine_names (AbstractContext.names auctx) uctx)
let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = let open CPrimitives in let auctx = CPrimitives.op_or_type_univs p in let univs, typ = match utyp with | None -> let u = UContext.instance (AbstractContext.repr auctx) in let typ = Typeops.type_of_prim_or_type env u p in let univs = if AbstractContext.is_empty auctx then Monomorphic else Polymorphic auctx in univs, typ
| Some (typ, univ_entry) -> let univ_entry = adjust_primitive_univ_entry p auctx univ_entry in let env, u, univs = process_universes env univ_entry in let typ = (Typeops.infer_type env typ).utj_val in let () = check_primitive_type env p u typ in univs, typ in let body = match p with | OT_op op -> Declarations.Primitive op | OT_type _ -> Undef None | OT_const c -> Def (CPrimitives.body_of_prim_const c) in (* Primitives not allowed in sections (checked in safe_typing) *) assert (List.is_empty (named_context env)); { const_hyps = []; const_univ_hyps = Instance.empty; const_body = body; const_type = typ; const_body_code = (); const_universes = univs; const_relevance = Sorts.Relevant; const_inline_code = false; const_typing_flags = Environ.typing_flags env; const_def_height = None }
let infer_symbol env { symb_entry_universes; symb_entry_unfold_fix; symb_entry_type } = let env, _, univs = process_universes env symb_entry_universes in let j = Typeops.infer env symb_entry_type in let r = Typeops.assumption_of_judgment env j in { const_hyps = []; const_univ_hyps = Instance.empty; const_body = Symbol symb_entry_unfold_fix; const_type = j.uj_val; const_body_code = (); const_universes = univs; const_relevance = r; const_inline_code = false; const_typing_flags = Environ.typing_flags env; const_def_height = None; }
let make_univ_hyps = function | None -> Instance.empty | Some us -> us
let infer_parameter ~sec_univs env entry = let env, _, univs = process_universes env entry.parameter_entry_universes in let typ = entry.parameter_entry_type in let j = Typeops.infer env typ in let r = Typeops.assumption_of_judgment env j in let typ = j.uj_val in let undef = Undef entry.parameter_entry_inline_code in let hyps = used_section_variables env entry.parameter_entry_secctx None typ in { const_hyps = hyps; const_univ_hyps = make_univ_hyps sec_univs; const_body = undef; const_type = typ; const_body_code = (); const_universes = univs; const_relevance = r; const_inline_code = false; const_typing_flags = Environ.typing_flags env; const_def_height = None; }
let infer_definition ~sec_univs env entry = let env, _, univs = process_universes env entry.definition_entry_universes in let body = entry.definition_entry_body in let hbody = HConstr.of_constr env body in let j = Typeops.infer_hconstr env hbody in let typ = match entry.definition_entry_type with | None -> j.uj_type | Some t -> let tj = Typeops.infer_type env t in let () = Typeops.check_cast env j DEFAULTcast tj in tj.utj_val in let body = j.uj_val in let hbody = Some hbody in let def = Def body in let hyps = used_section_variables env entry.definition_entry_secctx (Some body) typ in let def_h = Environ.constant_definitional_height env def in hbody, { const_hyps = hyps; const_univ_hyps = make_univ_hyps sec_univs; const_body = def; const_type = typ; const_body_code = (); const_universes = univs; const_relevance = Relevanceops.relevance_of_term env body; const_inline_code = entry.definition_entry_inline_code; const_typing_flags = Environ.typing_flags env; const_def_height = Some def_h }
(** Definition is opaque (Qed), so we delay the typing of its body. *)let infer_opaque ~sec_univs env entry = let env, _, univs = process_universes env entry.opaque_entry_universes in let typ = entry.opaque_entry_type in let typj = Typeops.infer_type env typ in let context = TyCtx (env, typj, entry.opaque_entry_secctx, univs) in let def = OpaqueDef () in let typ = typj.utj_val in let hyps = used_section_variables env (Some entry.opaque_entry_secctx) None typ in { const_hyps = hyps; const_univ_hyps = make_univ_hyps sec_univs; const_body = def; const_type = typ; const_body_code = (); const_universes = univs; const_relevance = Sorts.relevance_of_sort typj.utj_type; const_inline_code = false; const_typing_flags = Environ.typing_flags env; const_def_height = None }, context
let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = let TyCtx (env, tyj, declared, univs) = tyenv in let ((body, uctx), side_eff) = body in let (body, uctx', valid_signatures) = handle env body side_eff in let uctx = Univ.ContextSet.union uctx uctx' in let env, univs = match univs with | Monomorphic -> push_context_set uctx env, Opaqueproof.PrivateMonomorphic uctx | Polymorphic _ -> let () = assert (Int.equal valid_signatures 0) in push_subgraph uctx env, Opaqueproof.PrivatePolymorphic uctx in let hbody = HConstr.of_constr env body in (* Note: non-trivial trusted side-effects only in monomorphic case *) let () = let eff_body, eff_env = skip_trusted_seff valid_signatures hbody env in let j = Typeops.infer_hconstr eff_env eff_body in let () = assert (HConstr.self eff_body == j.uj_val) in let j = { uj_val = HConstr.self hbody; uj_type = j.uj_type } in Typeops.check_cast eff_env j DEFAULTcast tyj in let declared = if List.is_empty (named_context env) then declared else Environ.really_needed env (Id.Set.union declared (global_vars_set env tyj.utj_val)) in let declared' = check_section_variables env declared (Some body) tyj.utj_val in let () = assert (Id.Set.equal declared declared') in let def = HConstr.self hbody in let hbody = Some hbody in hbody, def, univs
(*s Global and local constant declaration. *)
let infer_local_assum env t = let j = Typeops.infer env t in let t = Typeops.assumption_of_judgment env j in j.uj_val, t
let infer_local_def env _id { secdef_body; secdef_type; } = let j = Typeops.infer env secdef_body in let typ = match secdef_type with | None -> j.uj_type | Some typ -> let tj = Typeops.infer_type env typ in let () = Typeops.check_cast env j DEFAULTcast tj in tj.utj_val in let c = j.uj_val in let r = Relevanceops.relevance_of_term env c in c, r, typ