Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422open Ppopen Utilopen Namesopen Conversionopen Declarationsopen Mod_declarationsopen Environ
(** {6 Checking constants } *)
type axioms = { cset : KerName.Set.t }
let empty_axioms = { cset = KerName.Set.empty }
let constants_of_axioms {cset} = KerName.Set.elements cset
let axioms_add c {cset} = {cset=KerName.Set.add c cset}
type check_state = { st_retro : (int * CPrimitives.prim_ind_ex) Mindmap.t * CPrimitives.prim_type_ex Cmap.t;}
let empty_state = { st_retro = (Mindmap.empty, Cmap.empty);}
let indirect_accessor : (Opaqueproof.opaque -> Opaqueproof.opaque_proofterm) ref = ref (fun _ -> assert false)
let set_indirect_accessor f = indirect_accessor := f
exception BadConstant of Constant.t * Pp.t
let check_constant_declaration env st kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); let env = CheckFlags.set_local_flags cb.const_typing_flags env in let poly, env = match cb.const_universes with | Monomorphic -> (* Monomorphic universes are stored at the library level, the ones in const_universes should not be needed *) false, env | Polymorphic auctx -> let ctx = UVars.AbstractContext.repr auctx in (* [env] contains De Bruijn universe variables *) let () = check_ucontext ctx env in let env = push_context ~strict:false ctx env in true, env in let ty = cb.const_type in let jty = Typeops.infer_type env ty in if not (Sorts.relevance_equal cb.const_relevance (Sorts.relevance_of_sort jty.utj_type)) then raise Pp.(BadConstant (kn, str "incorrect const_relevance")); let body, env = match cb.const_body with | Undef _ | Primitive _ | Symbol _ -> None, env | Def c -> Some c, env | OpaqueDef o -> let c, u = !indirect_accessor o in let env = match u, cb.const_universes with | Opaqueproof.PrivateMonomorphic (), Monomorphic -> env | Opaqueproof.PrivatePolymorphic local, Polymorphic _ -> push_subgraph local env | _ -> assert false in Some c, env in let () = match body with | Some bd -> let j = Typeops.infer env bd in begin match conv_leq env j.uj_type ty with | Result.Ok () -> () | Result.Error () -> Type_errors.error_actual_type env j ty end | None -> () in let retro, st = match Cmap.find_opt kn (snd st.st_retro) with | None -> None, st | Some retro -> let (ind_retro, cst_retro) = st.st_retro in let st = { st_retro = (ind_retro, Cmap.remove kn cst_retro) } in Some retro, st in retro, st
let check_constant_declaration env st kn cb = let retro, st = NewProfile.profile "check_constant" ~args:(fun () -> [("name", `String (Constant.to_string kn))]) (fun () -> check_constant_declaration env st kn cb) () in let env = Environ.add_constant kn cb env in let env = match retro with | None -> env | Some (CPrimitives.PTE prm) -> (* TODO: Some checking is performed by this function, but it looks too lightweight *) Primred.add_retroknowledge env (Retroknowledge.Register_type (prm, kn)) in env, st
let check_quality_mask env qmask lincheck = let open Sorts.Quality in match qmask with | PQConstant QSProp -> if Environ.sprop_allowed env then lincheck else Type_errors.error_not_allowed_sprop env | PQConstant (QProp | QType) | PQGlobal _ -> lincheck | PQVar qio -> Partial_subst.maybe_add_quality qio () lincheck
let check_instance_mask env udecl umask lincheck = match udecl, umask with | Monomorphic, ([||], [||]) -> lincheck | Polymorphic uctx, (qmask, umask) -> let lincheck = Array.fold_left_i (fun i lincheck mask -> check_quality_mask env mask lincheck) lincheck qmask in let lincheck = Array.fold_left_i (fun i lincheck mask -> Partial_subst.maybe_add_univ mask () lincheck) lincheck umask in if (Array.length qmask, Array.length umask) <> UVars.AbstractContext.size uctx then CErrors.anomaly Pp.(str "Bad univ mask length."); lincheck | _ -> CErrors.anomaly Pp.(str "Bad univ mask length.")
let rec get_holes_profiles env nargs ndecls lincheck el = List.fold_left (get_holes_profiles_elim env nargs ndecls) lincheck el
and get_holes_profiles_elim env nargs ndecls lincheck = function | PEApp args -> Array.fold_left (get_holes_profiles_parg env nargs ndecls) lincheck args | PECase (ind, ret, brs) -> let mib, mip = Inductive.lookup_mind_specif env ind in let lincheck = get_holes_profiles_parg env (nargs + mip.mind_nrealargs + 1) (ndecls + mip.mind_nrealdecls + 1) lincheck ret in Array.fold_left3 (fun lincheck nargs_b ndecls_b -> get_holes_profiles_parg env (nargs + nargs_b) (ndecls + ndecls_b) lincheck) lincheck mip.mind_consnrealargs mip.mind_consnrealdecls brs | PEProj proj -> let () = lookup_projection (Projection.make proj false) env |> ignore in lincheck
and get_holes_profiles_headelim env nargs ndecls lincheck (h, el) = let lincheck = get_holes_profiles_head env nargs ndecls lincheck h in get_holes_profiles env nargs ndecls lincheck el
and get_holes_profiles_parg env nargs ndecls lincheck = function | EHoleIgnored -> lincheck | EHole i -> Partial_subst.add_term i nargs lincheck | ERigid hel -> get_holes_profiles_headelim env nargs ndecls lincheck hel
and get_holes_profiles_head env nargs ndecls lincheck = function | PHRel n -> if n <= ndecls then lincheck else Type_errors.error_unbound_rel env n | PHSymbol (c, u) -> let cb = lookup_constant c env in check_instance_mask env cb.const_universes u lincheck | PHConstr (c, u) -> let (mib, _) = Inductive.lookup_mind_specif env (inductive_of_constructor c) in check_instance_mask env mib.mind_universes u lincheck | PHInd (ind, u) -> let (mib, _) = Inductive.lookup_mind_specif env ind in check_instance_mask env mib.mind_universes u lincheck | PHInt _ | PHFloat _ | PHString _ -> lincheck | PHSort PSSProp -> if Environ.sprop_allowed env then lincheck else Type_errors.error_not_allowed_sprop env | PHSort PSGlobal (_, io) | PHSort PSType io -> Partial_subst.maybe_add_univ io () lincheck | PHSort PSQSort (qio, uio) -> lincheck |> Partial_subst.maybe_add_quality qio () |> Partial_subst.maybe_add_univ uio () | PHSort _ -> lincheck | PHLambda (tys, bod) -> let lincheck = Array.fold_left_i (fun i -> get_holes_profiles_parg env (nargs + i) (ndecls + i)) lincheck tys in let lincheck = get_holes_profiles_headelim env (nargs + Array.length tys) (ndecls + Array.length tys) lincheck bod in lincheck | PHProd (tys, bod) -> let lincheck = Array.fold_left_i (fun i -> get_holes_profiles_parg env (nargs + i) (ndecls + i)) lincheck tys in let lincheck = get_holes_profiles_parg env (nargs + Array.length tys) (ndecls + Array.length tys) lincheck bod in lincheck
let check_rhs env holes_profile rhs = let rec check i c = match Constr.kind c with | App (f, args) when Constr.isRel f -> let n = Constr.destRel f in if n <= i then () else if n - i > Array.length holes_profile then CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site"); let d = holes_profile.(n-i-1) in if Array.length args >= d then () else CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site") | Rel n when n > i -> if n - i > Array.length holes_profile then CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site"); let d = holes_profile.(n-i-1) in if d = 0 then () else CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site") | _ -> Constr.iter_with_binders succ check i c in check 0 rhs
let check_rewrite_rule env lab i (symb, rule) = Flags.if_verbose Feedback.msg_notice (str " checking rule:" ++ Id.print lab ++ str"#" ++ Pp.int i); let { nvars; lhs_pat; rhs } = rule in let symb_cb = Environ.lookup_constant symb env in let () = match symb_cb.const_body with Symbol _ -> () | _ -> ignore @@ invalid_arg "Rule defined on non-symbol" in let lincheck = Partial_subst.make nvars in let lincheck = check_instance_mask env symb_cb.const_universes (fst lhs_pat) lincheck in let lincheck = get_holes_profiles env 0 0 lincheck (snd lhs_pat) in let holes_profile, _, _ = Partial_subst.to_arrays lincheck in let () = check_rhs env holes_profile rhs in ()
let check_rewrite_rules_body env lab rrb = List.iteri (check_rewrite_rule env lab) rrb.rewrules_rules
(** {6 Checking modules } *)
(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields. The only delicate part is when [mod_expr] is an algebraic expression : we need to expand it before checking it is indeed a subtype of [mod_type]. Fortunately, [mod_expr] cannot contain any [MEwith]. *)
let lookup_module mp env = try Environ.lookup_module mp env with Not_found -> failwith ("Unknown module: "^ModPath.to_string mp)
let mk_mtb sign delta = Mod_declarations.make_module_type sign delta
let rec check_mexpr env mse mp_mse res = match mse with | MEident mp -> let mb = lookup_module mp env in let mb = Modops.strengthen_and_subst_module_body mp mb mp_mse false in mod_type mb, mod_delta mb | MEapply (f,mp) -> let sign, delta = check_mexpr env f mp_mse res in let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let state = (Environ.universes env, Conversion.checked_universes) in let _ : UGraph.t = Subtyping.check_subtypes state env mp (MPbound farg_id) farg_b in let mp_delta = let mb = lookup_module mp env in match mod_type mb with | NoFunctor _ -> mod_delta mb | MoreFunctor _ -> Mod_subst.empty_delta_resolver mp in let subst = Mod_subst.map_mbid farg_id mp (Mod_subst.of_body_delta_resolver mp_delta) in Modops.subst_signature subst mp_mse fbody_b, Mod_subst.subst_codom_delta_resolver subst delta | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
let rec check_mexpression env sign mbtyp mp_mse res = match sign with | MEMoreFunctor body -> let arg_id, mtb, mbtyp = Modops.destr_functor mbtyp in let env' = Modops.add_module_parameter arg_id mtb env in let body, delta = check_mexpression env' body mbtyp mp_mse res in MoreFunctor(arg_id,mtb,body), delta | MENoFunctor me -> check_mexpr env me mp_mse res
let rec check_module env st mp (mb : Mod_declarations.module_body) = Flags.if_verbose Feedback.msg_notice (str " checking module: " ++ str (ModPath.to_string mp)); let delta_mb = mod_delta mb in let st = check_signature env st (mod_type mb) mp delta_mb in let optsign, st = match Mod_declarations.mod_expr mb with | Struct (reso, sign_struct) -> (* TODO: a bit wasteful, we recheck the types of parameters twice *) let sign_struct = Modops.annotate_struct_body sign_struct (mod_type mb) in (* The implementation is checked in its own right, hence its bytecode is compiled too; it is local to this check and never exported. With the VM disabled the bytecode is never run, so we skip the recompilation. *) let env, sign_struct = if !CheckFlags.enable_vm then let vmtab, sign_struct = Modops.compile_signature env (Environ.vm_library env) mp reso sign_struct in Environ.set_vm_library vmtab env, sign_struct else env, sign_struct in let st = check_signature env st sign_struct mp reso in Some (sign_struct, reso), st | Algebraic me -> Some (check_mexpression env me (mod_type mb) mp delta_mb), st | Abstract|FullStruct -> None, st in let () = match optsign with | None -> () | Some (sign,delta) -> let mtb1 = mk_mtb sign (Mod_subst.of_body_delta_resolver delta) and mtb2 = mk_mtb (mod_type mb) (Mod_subst.of_body_delta_resolver delta_mb) in let state = (Environ.universes env, Conversion.checked_universes) in let env = Modops.add_module mp (module_body_of_type mtb1) env in let _ : UGraph.t = Subtyping.check_subtypes state env mp mp mtb2 in () in st
and check_module_type env mp (mty : Mod_declarations.module_type_body) = Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string @@ mp)); let _ : check_state = check_signature env empty_state (mod_type mty) mp (mod_delta mty) in ()
and check_structure_field : type a. _ -> _ -> _ -> _ -> a Mod_subst.delta_resolver -> _ -> _ = fun env st mp lab res -> function | SFBconst cb -> let kn = KerName.make mp lab in let kn = Mod_subst.constant_of_delta_kn res kn in check_constant_declaration env st kn cb | SFBmind mib -> let kn = KerName.make mp lab in let kn = Mod_subst.mind_of_delta_kn res kn in let retro = Mindmap.find_opt kn (fst st.st_retro) in let st = match retro with | None -> st | Some _ -> let (ind_retro, cst_retro) = st.st_retro in let st = { st_retro = (Mindmap.remove kn ind_retro, cst_retro) } in st in CheckInductive.check_inductive env kn mib retro, st | SFBmodule msb -> let mp = MPdot(mp, lab) in let st = check_module env st mp msb in Modops.add_module mp msb env, st | SFBmodtype mty -> let mp = MPdot (mp, lab) in let () = check_module_type env mp mty in add_modtype mp mty env, st | SFBrules rrb -> check_rewrite_rules_body env lab rrb; Environ.add_rewrite_rules rrb.rewrules_rules env, st
and check_signature : type a. _ -> _ -> _ -> _ -> a Mod_subst.delta_resolver -> _ = fun env st sign mp_mse res -> match sign with | MoreFunctor (arg_id, mtb, body) -> let () = check_module_type env (MPbound arg_id) mtb in let env' = Modops.add_module_parameter arg_id mtb env in let st = check_signature env' st body mp_mse res in st | NoFunctor struc -> let (_:env), st = List.fold_left (fun (env, st) (lab,mb) -> check_structure_field env st mp_mse lab res mb) (env, st) struc in st
let rec collect_module_axioms axioms mp mb = match mod_expr mb with | Struct (reso, struc) -> (* Module with implementation separate from its type: don't produce axioms from the type *) let struc = Modops.annotate_struct_body struc (mod_type mb) in collect_signature_axioms axioms struc mp | Algebraic _ -> (* any axioms are already declared from the modules and functors involved in the application (this means an axiom in a functor is reported as coming from the functor rather than from the application) *) axioms | Abstract | FullStruct -> collect_signature_axioms axioms (mod_type mb) mp
and collect_signature_axioms axioms sign mp = match sign with | MoreFunctor (arg_id, mtb, body) -> collect_signature_axioms axioms body mp | NoFunctor struc -> let fold axioms (lab, field) = match field with | SFBconst cb -> let kn = KerName.make mp lab in let axioms = match cb.const_body with | Def _ | OpaqueDef _ | Primitive _ -> axioms | Undef _ | Symbol _ -> axioms_add kn axioms in axioms | SFBmodule mb -> let mp = MPdot (mp, lab) in let axioms = collect_module_axioms axioms mp mb in axioms | SFBmodtype _ -> axioms | SFBmind _ -> axioms | SFBrules _ -> axioms in List.fold_left fold axioms struc
let eq_prim_ind (type a b) (p : a CPrimitives.prim_ind) (q : b CPrimitives.prim_ind) = String.equal (CPrimitives.prim_ind_to_string p) (CPrimitives.prim_ind_to_string q)
let get_retroknowlege env retro = let fold (imap, cmap, extind) = function | Retroknowledge.Register_ind (prm, (ind, i)) -> (* Tolerate redeclarations because the kernel allows it somehow *) let check_prm map = match Mindmap.find_opt ind map with | None -> () | Some (_, CPrimitives.PIE prm') -> if not (eq_prim_ind prm prm') then CErrors.user_err Pp.(str "Inconsistent primitive registration for inductive " ++ MutInd.print ind ++ str ".") in let () = check_prm imap in let () = check_prm extind in (* It is allowed to register inductives coming from another library, so we have to account for that. *) if Environ.mem_mind ind env then let spec = Inductive.lookup_mind_specif env (ind, i) in let () = Safe_typing.check_register_ind (ind, i) prm spec in (imap, cmap, Mindmap.add ind (i, CPrimitives.PIE prm) extind) else (Mindmap.add ind (i, CPrimitives.PIE prm) imap, cmap, extind) | Retroknowledge.Register_type (prm, cst) -> let () = assert (not (Cmap.mem cst cmap)) in let () = assert (not (Environ.mem_constant cst env)) in (imap, Cmap.add cst (CPrimitives.PTE prm) cmap, extind) in let (imap, cmap, _) = List.fold_left fold (Mindmap.empty, Cmap.empty, Mindmap.empty) retro in (imap, cmap)
let check_module env axioms retro mp mb = let retro = get_retroknowlege env retro in let st = { st_retro = retro } in let { st_retro = (imap, cmap) } = check_module env st mp mb in let () = match Mindmap.choose_opt imap, Cmap.choose_opt cmap with | None, None -> () | Some (ind, _), (None | Some _) -> CErrors.user_err Pp.(str "Retroknowledge registration for unknown inductive " ++ MutInd.print ind ++ str ".") | None, Some (cst, _) -> CErrors.user_err Pp.(str "Retroknowledge registration for unknown constant " ++ Constant.print cst ++ str ".") in collect_module_axioms axioms mp mb
let check_module env axioms retro mp mb = NewProfile.profile "check_module" ~args:(fun () -> [("name", `String (ModPath.to_string mp))]) (fun () -> check_module env axioms retro mp mb) ()