(************************************************************************) (* * 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) *) (************************************************************************)
(** This module is about the low-level declaration of logical objects *)
open Pp open Util open Names open Safe_typing
module NamedDecl = Context.Named.Declaration
(* Hooks naturally belong here as they apply to both definitions and lemmas *)
module Hook = struct
module S = struct type t =
{ uctx : UState.t (** [ustate]: universe constraints obtained when the term was closed *)
; obls : (Names.Id.t * Constr.t) list (** [(n1,t1),...(nm,tm)]: association list between obligation name and the corresponding defined term (might be a constant,
but also an arbitrary term in the Expand case of obligations) *)
; scope : Locality.definition_scope (** [locality]: Locality of the original declaration *)
; dref : Names.GlobRef.t (** [ref]: identifier of the original declaration *)
} end
type'a g = (S.t -> 'a -> 'a) CEphemeron.key type t = unit g
let make_g hook = CEphemeron.create hook let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x)
let hcall hook x s = CEphemeron.default hook (fun _ x -> x) x s
let call_g ?hook x s = Option.cata (fun hook -> hcall hook x s) s hook let call ?hook x = Option.iter (fun hook -> hcall hook x ()) hook
end
let warn_using_fallback_loc = CWarnings.create ~name:"using-fallback-loc" ~category:CWarnings.CoreCategories.internal ~default:Disabled
Pp.(fun name -> str "Using fallback loc for " ++ Id.print name ++ str ".")
let fallback_loc ?(warn=true) name = function
| Some _ as loc -> loc
| None -> match Loc.get_current_command_loc () with
| None -> None
| Some _ as loc -> let () = if warn then warn_using_fallback_loc name in
loc
module CInfo = struct
type'constr t =
{ name : Id.t (** Name of theorem *)
; typ : 'constr (** Type of theorem *)
; args : Name.t list (** Names to pre-introduce *)
; impargs : Impargs.manual_implicits (** Explicitily declared implicit arguments *)
; loc : Loc.t option
}
let make ?loc ~name ~typ ?(args=[]) ?(impargs=[]) () = let loc = fallback_loc name loc in
{ name; typ; args; impargs; loc }
let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
let get_typ { typ; _ } = typ let get_name { name; _ } = name
end
(** Information for a declaration, interactive or not, includes
parameters shared by mutual constants *)
module Info = struct
(** Note that [opaque] doesn't appear here as it is not known at the
start of the proof in the interactive case. *) let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
?(udecl=UState.default_univ_decl) ?(scope=Locality.default_scope)
?(clearbody=false) ?hook ?typing_flags ?user_warns ?(ntns=[]) () =
{ poly; inline; kind; udecl; scope; hook; typing_flags; clearbody; user_warns; ntns } end
(** Declaration of constants and parameters *)
(* Deferred proofs: monomorphic, opaque, and udecl is for body+type *) type'eff deferred_opaque_proof_body = {
body : ((Constr.t * Univ.ContextSet.t) * 'eff) Future.computation;
feedback_id : Stateid.t option (* State id on which the completion of type checking is reported *)
}
(* Opacity of default proofs, possibly with private universes *) type default_body_opacity =
| Transparent (* udecl is for body+type; all universes are in proof_entry_universes *)
| Opaque of Univ.ContextSet.t (* if poly, the private uctx, udecl excludes the private uctx *) (* if mono, the body uctx *)
(* A proof body is either immediate or deferred *) type'eff proof_body =
| DeferredOpaque of'eff deferred_opaque_proof_body
| Default of'eff default_proof_body
(* A proof entry, parameterized with its kind of proof body *) type'body pproof_entry = {
proof_entry_body : 'body;
proof_entry_secctx : Id.Set.t option; (* List of section variables *)
proof_entry_type : Constr.types option; (* the initial type if deferred *)
proof_entry_universes : UState.named_universes_entry; (* refers to: - the initial uctx if opaque deferred; - the uctx of type only if opaque private;
- the full uctx otherwise *)
proof_entry_inline_code : bool;
}
(* The most general form of proof entry *) type proof_entry = Evd.side_effects proof_body pproof_entry
let default_univ_entry = UState.Monomorphic_entry Univ.ContextSet.empty let default_named_univ_entry = default_univ_entry, UnivNames.empty_binders
let extract_monomorphic = function
| UState.Monomorphic_entry ctx -> Entries.Monomorphic_entry, ctx
| UState.Polymorphic_entry uctx -> Entries.Polymorphic_entry uctx, Univ.ContextSet.empty
let instance_of_univs = function
| UState.Monomorphic_entry _, _ -> UVars.Instance.empty
| UState.Polymorphic_entry uctx, _ -> UVars.UContext.instance uctx
let add_mono_uctx uctx = function
| UState.Monomorphic_entry ctx, ubinders -> UState.Monomorphic_entry (Univ.ContextSet.union (UState.context_set uctx) ctx), ubinders
| UState.Polymorphic_entry _, _ as x -> assert (Univ.ContextSet.is_empty (UState.context_set uctx)); x
let make_ubinders uctx (univs, ubinders as u) = match univs with
| UState.Monomorphic_entry _ -> (UState.Monomorphic_entry uctx, ubinders)
| UState.Polymorphic_entry _ -> u
let universes_of_body_type ~used_univs body typ = let used_univs_typ = Option.cata (Vars.universes_of_constr ~init:used_univs) used_univs typ in let used_univs = Vars.universes_of_constr body ~init:used_univs_typ in
used_univs_typ, used_univs
let make_univs_deferred_private_mono ~initial_euctx ?feedback_id ~uctx ~udecl body typ = let _, used_univs = universes_of_body_type ~used_univs:Univ.Level.Set.empty body typ in let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of
the body. So we keep the two sets distinct. *) let uctx_body = UState.restrict uctx used_univs in
UState.check_mono_univ_decl uctx_body udecl
let make_univs_immediate_private_mono ~initial_euctx ~uctx ~udecl ~eff ~used_univs body typ = let utyp = UState.univ_entry ~poly:false initial_euctx in let _, used_univs = universes_of_body_type ~used_univs body typ in let ubody = let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of
the body. So we keep the two sets distinct. *) let uctx_body = UState.restrict uctx used_univs in
UState.check_mono_univ_decl uctx_body udecl in
initial_euctx, utyp, used_univs, Default { body = (body, eff); opaque = Opaque ubody }
let make_univs_immediate_private_poly ~uctx ~udecl ~eff ~used_univs body typ = let used_univs_typ, used_univs = universes_of_body_type ~used_univs body typ in let uctx' = UState.restrict uctx used_univs_typ in let utyp = UState.check_univ_decl ~poly:true uctx' udecl in let ubody = let uctx = UState.restrict uctx used_univs in
Univ.ContextSet.diff
(UState.context_set uctx)
(UState.context_set uctx') in
uctx', utyp, used_univs, Default { body = (body, eff); opaque = Opaque ubody }
let make_univs_immediate_default ~poly ~opaque ~uctx ~udecl ~eff ~used_univs body typ = let _, used_univs = universes_of_body_type ~used_univs body typ in (* Since the proof is computed now, we can simply have 1 set of constraints in which we merge the ones for the body and the ones for the typ. We recheck the declaration after restricting with the actually used universes.
TODO: check if restrict is really necessary now. *) let uctx = UState.restrict uctx used_univs in let utyp = UState.check_univ_decl ~poly uctx udecl in let utyp = match fst utyp with
| Polymorphic_entry _ -> utyp
| Monomorphic_entry uctx -> (* the constraints from the body may depend on universes from the side effects, so merge it all together. Example failure if we don't is "l1" in test-suite/success/rewrite.v.
Not sure if it makes more sense to merge them in the ustate before restrict/check_univ_decl or here. Since we only do it
when monomorphic it shouldn't really matter. *)
Monomorphic_entry (Univ.ContextSet.union uctx (Safe_typing.universes_of_private eff.Evd.seff_private)), snd utyp in
uctx, utyp, used_univs, Default { body = (body, eff); opaque = if opaque then Opaque Univ.ContextSet.empty else Transparent }
let make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff ~used_univs body typ = (* allow_deferred case *) match keep_body_ucst_separate with
| Some initial_euctx when not poly -> make_univs_immediate_private_mono ~initial_euctx ~uctx ~udecl ~eff ~used_univs body typ
| _ -> (* private_poly_univs case *) if poly && opaque && private_poly_univs () then make_univs_immediate_private_poly ~uctx ~udecl ~eff ~used_univs body typ else make_univs_immediate_default ~poly ~opaque ~uctx ~udecl ~eff ~used_univs body typ
(** [univsbody] are universe-constraints attached to the body-only,
used in vio-delayed opaque constants and private poly universes *) let definition_entry_core ?using ?(inline=false) ?types
?(univs=default_named_univ_entry) body =
{ proof_entry_body = body;
proof_entry_secctx = using;
proof_entry_type = types;
proof_entry_universes = univs;
proof_entry_inline_code = inline}
let pure_definition_entry ?(opaque=Transparent) ?using ?inline ?types ?univs body =
definition_entry_core ?using ?inline ?types ?univs body
let definition_entry ?(opaque=false) ?using ?inline ?types ?univs body = let opaque = if opaque then Opaque Univ.ContextSet.empty else Transparent in
definition_entry_core ?using ?inline ?types ?univs (Default { body = (body, Evd.empty_side_effects); opaque })
let delayed_definition_entry ?feedback_id ?using ~univs ?types body =
definition_entry_core ?using ?types ~univs (DeferredOpaque { body; feedback_id })
let parameter_entry ?inline ?(univs=default_named_univ_entry) typ = {
parameter_entry_secctx = None;
parameter_entry_type = typ;
parameter_entry_universes = univs;
parameter_entry_inline_code = inline;
}
let primitive_entry ?types c = {
prim_entry_type = types;
prim_entry_content = c;
}
type constant_entry =
| DefinitionEntry of proof_entry
| ParameterEntry of parameter_entry
| PrimitiveEntry of primitive_entry
| SymbolEntry of symbol_entry
module ProofEntry = struct
let map_entry_body ~f = function
| Default { body = body; opaque } -> Default { body = f body; opaque }
| DeferredOpaque { body; feedback_id } -> let body = Future.chain body (fun ((b,c),eff) -> let b, eff = f (b,eff) in ((b,c),eff)) in
DeferredOpaque { body; feedback_id }
let map_entry ~f entry =
{ entry with
proof_entry_body = map_entry_body ~f:(on_fst f) entry.proof_entry_body;
proof_entry_type = Option.map f entry.proof_entry_type }
let get_entry_body entry = let (body, eff), opaque = force_entry_body entry in let uctx = match opaque with
| Opaque uctx -> uctx
| Transparent -> Univ.ContextSet.empty in
(body, uctx), eff
let rec shrink ctx sign c t accu = letopen Constr in letopen Vars in match ctx, sign with
| [], [] -> (c, t, accu)
| p :: ctx, decl :: sign -> if noccurn 1 c && noccurn 1 t then let c = subst1 mkProp c in let t = subst1 mkProp t in
shrink ctx sign c t accu else let c = Term.mkLambda_or_LetIn p c in let t = Term.mkProd_or_LetIn p t in let accu = if Context.Rel.Declaration.is_local_assum p then EConstr.mkVar (NamedDecl.get_id decl) :: accu else accu in
shrink ctx sign c t accu
| _ -> assert false
(* If [sign] is [x1:T1..xn:Tn], [c] is [fun x1:T1..xn:Tn => c'] and [t] is [forall x1:T1..xn:Tn, t'], returns a new [c'] and [t'], where all non-dependent [xi] are removed, as well as a
restriction [args] of [x1..xn] such that [c' args] = [c x1..xn] *) let shrink_entry sign body typ = let typ = match typ with
| None -> assert false
| Some t -> t in let (ctx, body, typ) = Term.decompose_lambda_prod_n_decls (List.length sign) body typ in let (body, typ, args) = shrink ctx sign body typ [] in
body, Some typ, args
end
let local_csts = Summary.ref ~name:"local-csts" Cset_env.empty
let is_local_constant c = Cset_env.mem c !local_csts
let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then raise (DeclareUniv.AlreadyDeclared (None, Libnames.basename sp)); let con = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef con in
Nametab.push ?user_warns:obj.cst_warn (Nametab.Until i) sp gr;
Dumpglob.add_constant_kind con obj.cst_kind;
obj.cst_loc |> Option.iter (fun loc -> Nametab.set_cci_src_loc (TrueGlobal gr) loc); beginmatch obj.cst_locl with
| Locality.ImportNeedQualified -> local_csts := Cset_env.add con !local_csts
| Locality.ImportDefaultBehavior -> () end
(* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = (* Never open a local definition *) match obj.cst_locl with
| Locality.ImportNeedQualified -> ()
| Locality.ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in
Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
let exists_name id =
Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
let check_exists id = if exists_name id then raise (DeclareUniv.AlreadyDeclared (None, id))
let cache_constant ((sp,kn), obj) = let kn = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef kn in
Nametab.push ?user_warns:obj.cst_warn (Nametab.Until 1) sp gr;
Dumpglob.add_constant_kind kn obj.cst_kind;
obj.cst_loc |> Option.iter (fun loc -> Nametab.set_cci_src_loc (TrueGlobal gr) loc)
let inConstant v = Libobject.Dyn.Easy.inj v objConstant
(* Register the libobjects attached to the constants *) let register_constant loc cst kind ?user_warns local = (* Register the declaration *) let id = Label.to_id (Constant.label cst) in let loc = fallback_loc id loc in let o = inConstant (id, { cst_kind = kind; cst_locl = local; cst_warn = user_warns; cst_loc = loc; }) in let () = Lib.add_leaf o in (* Register associated data *)
Impargs.declare_constant_implicits cst;
Notation.declare_ref_arguments_scope (GlobRef.ConstRef cst)
let register_side_effect (c, body, role) = (* Register the body in the opaque table *) let () = match body with
| None -> ()
| Some opaque -> Opaques.declare_private_opaque opaque in let id = Label.to_id @@ Constant.label c in let () = register_constant (fallback_loc ~warn:false id None) c Decls.(IsProof Theorem) Locality.ImportDefaultBehavior in match role with
| None -> ()
| Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme SuperGlobal kind (ind,c)
let get_roles export eff = letmap (c, body) = let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
(c, body, role) in List.mapmap export
let export_side_effects eff = let export = Global.export_private_constants eff.Evd.seff_private in let export = get_roles export eff in List.iter register_side_effect export
let record_aux env s_ty s_bo = letopen Environ in let in_ty = keep_hyps env s_ty in let v = String.concat " "
(CList.map_filter (fun decl -> let id = NamedDecl.get_id decl in ifList.exists (NamedDecl.get_id %> Id.equal id) in_ty then None else Some (Id.to_string id))
(keep_hyps env s_bo)) in
Aux_file.record_in_aux "context_used" v
let cast_pure_proof_entry (e : Constr.constr pproof_entry) = let univ_entry, ctx = extract_monomorphic (fst (e.proof_entry_universes)) in
{ Entries.definition_entry_body = e.proof_entry_body;
definition_entry_secctx = e.proof_entry_secctx;
definition_entry_type = e.proof_entry_type;
definition_entry_universes = univ_entry;
definition_entry_inline_code = e.proof_entry_inline_code;
},
ctx
let section_context_of_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (body : a) typ = letopen Environ in let env = Global.env () in let hyp_typ, hyp_def = ifList.is_empty (Environ.named_context env) then
Id.Set.empty, Id.Set.empty else let ids_typ = global_vars_set env typ in let (pf : Constr.constr), env = match entry with
| PureEntry -> body, env
| ImmediateEffectEntry -> let (pf, _), eff = body in let env = Safe_typing.push_private_constants env eff in
pf, env
| DeferredEffectEntry -> let (pf, _), eff = Future.force body in let env = Safe_typing.push_private_constants env eff in
pf, env in let vars = global_vars_set env pf in
ids_typ, vars in let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a pproof_entry) : b Entries.opaque_entry * _ = let typ = match e.proof_entry_type with
| None -> assert false
| Some typ -> typ in let secctx = match e.proof_entry_secctx with
| None -> section_context_of_opaque_proof_entry entry e.proof_entry_body typ
| Some hyps -> hyps in let body : b = match entry with
| PureEntry -> e.proof_entry_body
| ImmediateEffectEntry -> ()
| DeferredEffectEntry -> () in let univ_entry, ctx = extract_monomorphic (fst (e.proof_entry_universes)) in
{ Entries.opaque_entry_body = body;
opaque_entry_secctx = secctx;
opaque_entry_type = typ;
opaque_entry_universes = univ_entry;
},
ctx
let feedback_axiom () = Feedback.(feedback AddedAxiom)
let is_unsafe_typing_flags flags = let flags = Option.default (Global.typing_flags ()) flags in letopen Declarations in not (flags.check_universes && flags.check_guarded && flags.check_positive)
let declare_constant ~loc ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags ?user_warns cd = let before_univs = Global.universes () in let make_constant = function (* Logically define the constant and its subproofs, no libobject tampering *)
| DefinitionEntry de -> (* We deal with side effects *)
(match de.proof_entry_body with
| Default { body = (body, eff); opaque = Transparent } -> (* This globally defines the side-effects in the environment
and registers their libobjects. *) let () = export_side_effects eff in let de = { de with proof_entry_body = body } in let e, ctx = cast_pure_proof_entry de in let ubinders = make_ubinders ctx de.proof_entry_universes in (* We register the global universes after exporting side-effects, since
the latter depend on the former. *) let () = Global.push_context_set ctx in
Entries.DefinitionEntry e, false, ubinders, None, ctx
| Default { body = (body, eff); opaque = Opaque body_uctx } -> let body = ((body, body_uctx), eff.Evd.seff_private) in let de = { de with proof_entry_body = body } in let cd, ctx = cast_opaque_proof_entry ImmediateEffectEntry de in let ubinders = make_ubinders ctx de.proof_entry_universes in let () = Global.push_context_set ctx in
Entries.OpaqueEntry cd, false, ubinders, Some (Future.from_val body, None), ctx
| DeferredOpaque { body; feedback_id } -> letmap (body, eff) = body, eff.Evd.seff_private in let body = Future.chain body mapin let de = { de with proof_entry_body = body } in let cd, ctx = cast_opaque_proof_entry DeferredEffectEntry de in let ubinders = make_ubinders ctx de.proof_entry_universes in let () = Global.push_context_set ctx in
Entries.OpaqueEntry cd, false, ubinders, Some (body, feedback_id), ctx)
| ParameterEntry e -> let univ_entry, ctx = extract_monomorphic (fst e.parameter_entry_universes) in let ubinders = make_ubinders ctx e.parameter_entry_universes in let () = Global.push_context_set ctx in let e = {
Entries.parameter_entry_secctx = e.parameter_entry_secctx;
Entries.parameter_entry_type = e.parameter_entry_type;
Entries.parameter_entry_universes = univ_entry;
Entries.parameter_entry_inline_code = e.parameter_entry_inline_code;
} in
Entries.ParameterEntry e, not (Lib.is_modtype_strict()), ubinders, None, ctx
| PrimitiveEntry e -> let typ, univ_entry, ctx = match e.prim_entry_type with
| None ->
None, (UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders), Univ.ContextSet.empty
| Some (typ, entry_univs) -> let univ_entry, ctx = extract_monomorphic (fst entry_univs) in
Some (typ, univ_entry), entry_univs, ctx in let () = Global.push_context_set ctx in let e = {
Entries.prim_entry_type = typ;
Entries.prim_entry_content = e.prim_entry_content;
} in let ubinders = make_ubinders ctx univ_entry in
Entries.PrimitiveEntry e, false, ubinders, None, ctx
| SymbolEntry { symb_entry_type=typ; symb_entry_unfold_fix=un_fix; symb_entry_universes=entry_univs } -> let univ_entry, ctx = extract_monomorphic (fst entry_univs) in let () = Global.push_context_set ctx in let e = {
Entries.symb_entry_type = typ;
Entries.symb_entry_unfold_fix = un_fix;
Entries.symb_entry_universes = univ_entry;
} in let ubinders = make_ubinders ctx entry_univs in
Entries.SymbolEntry e, false, ubinders, None, ctx in let declare_opaque kn = function
| None -> ()
| Some (body, feedback_id) -> letopen Declarations in match (Global.lookup_constant kn).const_body with
| OpaqueDef o -> let (_, _, _, i) = Opaqueproof.repr o in
Opaques.declare_defined_opaque ?feedback_id i body
| Def _ | Undef _ | Primitive _ | Symbol _ -> assert false in let () = check_exists name in let decl, unsafe, ubinders, delayed, ctx = make_constant cd in let kn = Global.add_constant ?typing_flags name decl in let () = let is_new_constraint (u,_,v as c) = match UGraph.check_declared_universes before_univs Univ.Level.Set.(add u (add v empty)) with
| Ok () -> not (UGraph.check_constraint before_univs c)
| Error _ -> true in let ctx = on_snd (Univ.Constraints.filter is_new_constraint) ctx in
DeclareUniv.add_constraint_source (ConstRef kn) ctx in let () = DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) ubinders in let () = declare_opaque kn delayed in let () = register_constant loc kn kind local ?user_warns in if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
kn
let declare_private_constant ?role ~name ~opaque de effs = let de, ctx = ifnot opaque then let de, ctx = cast_pure_proof_entry de in
DefinitionEff de, ctx else let de, ctx = cast_opaque_proof_entry PureEntry de in
OpaqueEff de, ctx
in let kn, eff = Global.add_private_constant name ctx de in let () = if Univ.Level.Set.is_empty (fst ctx) then () else DeclareUniv.declare_univ_binders (ConstRef kn)
(Monomorphic_entry ctx, UnivNames.empty_binders) in let seff_roles = match role with
| None -> effs.Evd.seff_roles
| Some r -> Cmap.add kn r effs.Evd.seff_roles in let seff_private = Safe_typing.concat_private eff effs.Evd.seff_private in let effs = { Evd.seff_private; Evd.seff_roles } in
kn, effs
let inline_private_constants ~uctx env (body, eff) = let body, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
body, uctx
(** Declaration of section variables and local definitions *) type variable_declaration =
| SectionLocalDef of {
clearbody : bool;
entry : proof_entry;
}
| SectionLocalAssum of {
typ : Constr.types;
impl : Glob_term.binding_kind;
univs : UState.named_universes_entry;
}
(* This object is only for things which iterate over objects to find
variables (only Prettyp.print_context AFAICT) *) let objVariable : Id.t Libobject.Dyn.tag = letopen Libobject in
declare_object_full { (default_object "VARIABLE") with
classify_function = (fun _ -> Dispose)}
let inVariable v = Libobject.Dyn.Easy.inj v objVariable
let declare_variable ~name ~kind ~typing_flags d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then raise (DeclareUniv.AlreadyDeclared (None, name));
let impl,opaque = match d with(* Fails if not well-typed *)
| SectionLocalAssum {typ;impl;univs} -> let () = match fst univs with
| UState.Monomorphic_entry uctx -> (* XXX [snd univs] is ignored, should we use it? *)
DeclareUniv.name_mono_section_univs (fst uctx);
Global.push_context_set uctx
| UState.Polymorphic_entry uctx -> Global.push_section_context uctx in let () = Global.push_named_assum (name,typ) in
impl, true
| SectionLocalDef { clearbody; entry = de } -> (* The body should already have been forced upstream because it is a
section-local definition, but it's not enforced by typing *) let ((body, body_uctx), eff), opaque, feedback_id = ProofEntry.force_extract_body de in let () = export_side_effects eff in (* We must declare the universe constraints before type-checking the
term. *) let univs = match fst de.proof_entry_universes with
| UState.Monomorphic_entry uctx ->
DeclareUniv.name_mono_section_univs (fst uctx);
Global.push_context_set (Univ.ContextSet.union uctx body_uctx);
UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders
| UState.Polymorphic_entry uctx ->
Global.push_section_context uctx; let mk_anon_names u = let qs, us = UVars.Instance.to_array u in
{UVars.quals = Array.make (Array.length qs) Anonymous; UVars.univs = Array.make (Array.length us) Anonymous} in
Global.push_section_context
(UVars.UContext.of_context_set mk_anon_names Sorts.QVar.Set.empty body_uctx);
UState.Polymorphic_entry UVars.UContext.empty, UnivNames.empty_binders in let se = if opaque then let cname = Id.of_string (Id.to_string name ^ "_subproof") in let cname = Namegen.next_global_ident_away (Global.safe_env ()) cname Id.Set.empty in let de = {
proof_entry_body = DeferredOpaque { body = Future.from_val ((body, Univ.ContextSet.empty), Evd.empty_side_effects); feedback_id };
proof_entry_secctx = None; (* de.proof_entry_secctx is NOT respected *)
proof_entry_type = de.proof_entry_type;
proof_entry_universes = univs;
proof_entry_inline_code = de.proof_entry_inline_code;
} in let kn = declare_constant ~name:cname ~loc:None
~local:ImportNeedQualified ~kind:(IsProof Lemma) ~typing_flags
(DefinitionEntry de) in
{
Entries.secdef_body = Constr.mkConstU (kn, UVars.Instance.empty);
secdef_type = None;
} else {
Entries.secdef_body = body;
secdef_type = de.proof_entry_type;
} in let () = Global.push_named_def (name, se) in (* opaque implies clearbody, so we don't see useless "foo := foo_subproof" in the context *)
Glob_term.Explicit, opaque || clearbody in
Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
Decls.(add_variable_data name {opaque;kind});
Lib.add_leaf (inVariable name);
Impargs.declare_var_implicits ~impl name;
Notation.declare_ref_arguments_scope (GlobRef.VarRef name)
(* Declaration messages *)
let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
Flags.if_verbose Feedback.msg_info (match l with
| [] -> CErrors.anomaly (Pp.str "no recursive definition.")
| [id] -> Id.print id ++ str " is recursively defined" ++
(match indexes with
| Some [|i|] -> str " (guarded on "++pr_rank i++str " argument)"
| _ -> mt ())
| l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
spc () ++ str "are recursively defined" ++ match indexes with
| Some a -> spc () ++ str "(guarded respectively on " ++
prvect_with_sep pr_comma pr_rank a ++
str " arguments)"
| None -> mt ()))
let cofixpoint_message l =
Flags.if_verbose Feedback.msg_info (match l with
| [] -> CErrors.anomaly (Pp.str "No corecursive definition.")
| [id] -> Id.print id ++ str " is corecursively defined"
| l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
spc () ++ str "are corecursively defined"))
let recursive_message indexes l = match indexes with
| None -> cofixpoint_message l
| Some indexes -> fixpoint_message (Some indexes) l
let definition_message id =
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
let assumption_message id = (* Changing "assumed" to "declared", "assuming" referring more to the type of the object than to the name of the object (see
discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
module Internal = struct
module Constant = struct type t = constant_obj let tag = objConstant let kind obj = obj.cst_kind end
let objVariable = objVariable
let export_side_effects = export_side_effects
end
(* The word [proof] is to be understood as [justification] *) (* A possible alternatve would be [evidence]?? *) type closed_proof_output = ((Constr.t * Evd.side_effects) * Constr.t option) list * UState.t
let future_map2_pair_list_distribute p l f = List.map_i (fun i c -> f (Future.chain p (fun (a, b) -> (List.nth a i, b))) c) 0 l
let process_proof ~info:Info.({ udecl; poly }) ?(is_telescope=false) = function
| DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate } -> (* Force transparency for Derive-like dependent statements *) let opaques = let n = List.length entries in List.init n (fun i -> if i < n-1 && is_telescope then(* waiting for addition of cinfo-based opacity in #19029 *) false else opaque) in (* Multiple entries mean either a recursive block of definitions (as in Co/Fixpoint) or a sequence of dependent definitions (as in "Derive"). In the second case, the dependency in the previous entries requires to accumulate the universes from the
previous definitions *)
snd (List.fold_left2_map (fun used_univs ((body, eff), typ) opaque -> let uctx, univs, used_univs, body =
make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff ~used_univs body typ in
(used_univs, (definition_entry_core ?using ~univs ?types:typ body, uctx))) Univ.Level.Set.empty entries opaques)
| DeferredOpaqueProof { deferred_proof = bodies; using; initial_proof_data; feedback_id; initial_euctx } -> let { Proof.poly; entry; sigma } = initial_proof_data in (* Deferred multiple entries currently assume either a mutual Co/Fixpoint or no dependency (thus no "Derive"); to support "Derive"-like statements, we would need a combinator on futures
that fold used universes *)
future_map2_pair_list_distribute bodies (Proofview.initial_goals entry)
(fun body_typ_uctx (_, _, initial_typ) -> (* Testing if evar-closed? *) let initial_typ = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr initial_typ) in (* The flags keep_body_ucst_separate, opaque, etc. should be consistent with evar-closedness? *) let univs = UState.univ_entry ~poly:false initial_euctx in let body = Future.chain body_typ_uctx (fun (((body, eff), _typ), uctx) -> let uctx = make_univs_deferred_private_mono ~initial_euctx ~uctx ~udecl body (Some initial_typ) in
((body, uctx), eff)) in
(delayed_definition_entry ?using ~univs ~types:initial_typ ~feedback_id body, initial_euctx))
let declare_definition_scheme ~internal ~univs ~role ~name ~effs ?loc c = let kind = Decls.(IsDefinition Scheme) in let entry = pure_definition_entry ~univs c in let kn, effs = declare_private_constant ~role ~name ~opaque:false entry effs in let () = register_constant (fallback_loc ~warn:false name None) kn kind Locality.ImportDefaultBehavior in
Dumpglob.dump_definition
(CAst.make ?loc (Constant.label kn |> Label.to_id)) false"scheme"; let () = if internal then () else definition_message name in
kn, effs
(* Locality stuff *) let declare_entry ~loc ~name ?(scope=Locality.default_scope) ?(clearbody=false) ~kind ~typing_flags ~user_warns ?hook ?(obls=[]) ~impargs ~uctx entry = let should_suggest =
ProofEntry.get_opacity entry
&& not (List.is_empty (Global.named_context()))
&& Option.is_empty entry.proof_entry_secctx in let dref = match scope with
| Locality.Discharge -> let () = declare_variable ~typing_flags ~name ~kind (SectionLocalDef {clearbody; entry}) in if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
Names.GlobRef.VarRef name
| Locality.Global local ->
assert (not clearbody); let kn = declare_constant ~loc ~name ~local ~kind ~typing_flags ?user_warns (DefinitionEntry entry) in let gr = Names.GlobRef.ConstRef kn in if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
gr in let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = definition_message name in
Hook.call ?hook { Hook.S.uctx; obls; scope; dref };
dref
let warn_let_as_axiom =
CWarnings.create ~name:"let-as-axiom" ~category:CWarnings.CoreCategories.vernacular
Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
spc () ++ strbrk "declared as an axiom.")
(* Declare an assumption when not in a section: Parameter/Axiom but also
Variable/Hypothesis seen as Local Parameter/Axiom *) let declare_parameter ~loc ~name ~scope ~hook ~impargs ~uctx pe = let local = match scope with
| Locality.Discharge -> warn_let_as_axiom name; Locality.ImportNeedQualified
| Locality.Global local -> local in let kind = Decls.(IsAssumption Conjectural) in let decl = ParameterEntry pe in let cst = declare_constant ~loc ~name ~local ~kind ~typing_flags:None decl in let dref = Names.GlobRef.ConstRef cst in let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = assumption_message name in let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in
cst
(* Using processing *) let interp_proof_using_gen f env evd cinfo using = let cextract v (fixnames, terms) = let name, new_terms = f v in
name :: fixnames, new_terms @ terms in let fixnames, terms = CList.fold_right cextract cinfo ([],[]) in
Proof_using.definition_using env evd ~fixnames ~terms ~using
let interp_proof_using_cinfo env evd cinfo using = let f { CInfo.name; typ; _ } = name, [typ] in
interp_proof_using_gen f env evd cinfo using
let gather_mutual_using_data cinfo = List.fold_left2 (fun acc CInfo.{name} (body, typ) -> let l = Option.List.flatten EConstr.[Option.map of_constr typ; Some (of_constr body)] in
(name, l) :: acc) [] cinfo
let interp_mutual_using env cinfo bodies_types using = let evd = Evd.from_env env in Option.map (fun using -> let cinfos = gather_mutual_using_data cinfo bodies_types in let f x = x in
interp_proof_using_gen f env evd cinfos using)
using
let declare_possibly_mutual_definitions ~info ~cinfo ~obls ?(is_telescope=false) obj = let entries = process_proof ~info ~is_telescope obj in let { Info.hook; scope; clearbody; kind; typing_flags; user_warns; ntns; _ } = info in let _, refs = List.fold_left2_map (fun subst CInfo.{name; impargs; loc} (entry, uctx) -> (* replacing matters for Derive-like statement but it does not hurt otherwise *) let entry = ProofEntry.map_entry entry ~f:(Vars.replace_vars subst) in let gref = declare_entry ~loc ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~obls ~uctx entry in let inst = instance_of_univs entry.proof_entry_universes in letconst = Constr.mkRef (gref, inst) in
((name, const) :: subst, gref)) [] cinfo entries in let () = (* For the recursive case, we override the temporary notations used while proving, now using the global names *) let local = info.scope=Locality.Discharge in if ntns <> [] then
CWarnings.with_warn ("-"^Notation.warning_overridden_name)
(List.iter (Metasyntax.add_notation_interpretation ~local (Global.env()))) ntns in
refs
let declare_possibly_mutual_parameters ~info ~cinfo ?(mono_uctx_extra=UState.empty) ~sec_vars typs = (* Note, if an initial uctx, minimize and restrict have not been done *) (* if the uctx of an abandonned proof, minimize is redundant (see close_proof) *) let { Info.scope; poly; hook; udecl } = info in
pi3 (List.fold_left2 ( fun (i, subst, csts) { CInfo.name; loc; impargs } (typ, uctx) -> let uctx' = UState.restrict uctx (Vars.universes_of_constr typ) in let univs = UState.check_univ_decl ~poly uctx' udecl in let univs = if i = 0 then add_mono_uctx mono_uctx_extra univs else univs in let typ = Vars.replace_vars subst typ in let pe = {
parameter_entry_secctx = sec_vars;
parameter_entry_type = Evarutil.nf_evars_universes (Evd.from_ctx uctx) typ;
parameter_entry_universes = univs;
parameter_entry_inline_code = None;
} in let cst = declare_parameter ~loc ~name ~scope ~hook ~impargs ~uctx pe in let inst = instance_of_univs univs in
(i+1, (name, Constr.mkConstU (cst,inst))::subst, (cst, univs)::csts)
) (0, [], []) cinfo typs)
let make_recursive_bodies env ~typing_flags ~possible_guard ~rec_declaration = let env = Environ.update_typing_flags ?typing_flags env in let indexes = Pretyping.search_guard env possible_guard rec_declaration in let mkbody i = match indexes with
| Some indexes -> Constr.mkFix ((indexes,i), rec_declaration)
| None -> Constr.mkCoFix (i, rec_declaration) in List.map_i (fun i typ -> (mkbody i, typ)) 0 (Array.to_list (pi2 rec_declaration)), indexes
let prepare_recursive_declaration cinfo fixtypes fixrs fixdefs = let fixnames = List.map (fun CInfo.{name} -> name) cinfo in let names = List.map2 (fun name r -> Context.make_annot (Name name) r) fixnames fixrs in let defs = List.map (Vars.subst_vars (List.rev fixnames)) fixdefs in
(Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
let prepare_recursive_edeclaration sigma cinfo fixtypes fixrs fixdefs = let fixnames = List.map (fun CInfo.{name} -> name) cinfo in let names = List.map2 (fun name r -> Context.make_annot (Name name) r) fixnames fixrs in let defs = List.map (EConstr.Vars.subst_vars sigma (List.rev fixnames)) fixdefs in
(Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
let declare_mutual_definitions ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guard ?using () = (* Note: uctx is supposed to be already minimized *) let { Info.typing_flags; _ } = info in let env = Global.env() in let possible_guard, fixrelevances = possible_guard in let fixtypes = List.map (fun CInfo.{typ} -> typ) cinfo in let rec_declaration = prepare_recursive_declaration cinfo fixtypes fixrelevances bodies in let bodies_types, indexes = make_recursive_bodies env ~typing_flags ~rec_declaration ~possible_guard in let entries = List.map (fun (body, typ) -> ((body, Evd.empty_side_effects), Some typ)) bodies_types in let entries_for_using = List.map (fun (body, typ) -> (body, Some typ)) bodies_types in let using = interp_mutual_using env cinfo entries_for_using using in let obj = DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate = None } in let refs = declare_possibly_mutual_definitions ~info ~cinfo ~obls:[] obj in let fixnames = List.map (fun { CInfo.name } -> name) cinfo in
recursive_message indexes fixnames;
refs
(* Preparing proof entries *) let error_unresolved_evars env sigma t evars = let pr_unresolved_evar e =
hov 2 (str"- " ++ Printer.pr_existential_key env sigma e ++ str ": " ++
Himsg.explain_pretype_error env sigma
(Pretype_errors.UnsolvableImplicit (e,None)))
in
CErrors.user_err (hov 0 begin
str "The following term contains unresolved implicit arguments:"++ fnl () ++
str " " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++
str "More precisely: " ++ fnl () ++
v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements evars))
end)
let check_evars_are_solved env sigma t =
let evars = Evarutil.undefined_evars_of_term sigma t in ifnot (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
let declare_definition ~info ~cinfo ~opaque ~obls ~body ?using sigma =
let { CInfo.name; typ; _ } = cinfo in
let env = Global.env () in
Option.iter (check_evars_are_solved env sigma) typ;
check_evars_are_solved env sigma body;
let sigma = Evd.minimize_universes sigma in
let body = EConstr.to_constr sigma body in
let typ = Option.map (EConstr.to_constr sigma) typ in
let uctx = Evd.ustate sigma in
let using = interp_mutual_using env [cinfo] [body,typ] using in
let obj = DefaultProof { proof = ([((body,Evd.empty_side_effects),typ)], uctx); opaque; using; keep_body_ucst_separate = None } in
let gref = List.hd (declare_possibly_mutual_definitions ~info ~cinfo:[cinfo] ~obls obj) in
gref, uctx
let prepare_obligations ~name ?types ~body env sigma =
let env = Global.env () in
let types = match types with
| Some t -> t
| None -> Retyping.get_type_of env sigma body
in
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
sigma (fun nf -> nf body, nf types)
in
RetrieveObl.check_evars env sigma;
let body, types = EConstr.(of_constr body, of_constr types) in
let obls, (_, evmap), body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in
let uctx = Evd.ustate sigma in
body, cty, uctx, evmap, obls
let prepare_parameter ~poly ~udecl ~types sigma =
let env = Global.env () in
Pretyping.check_evars_are_solved ~program_mode:false env sigma;
let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true
sigma (fun nf -> nf types)
in
let univs = Evd.check_univ_decl ~poly sigma udecl in
let pe = {
parameter_entry_secctx = None;
parameter_entry_type = typ;
parameter_entry_universes = univs;
parameter_entry_inline_code = None;
} in
sigma, pe
type progress = Remain of int | Dependent | Defined of GlobRef.t
module Obls_ = struct
open Constr
type'a obligation_body = DefinedObl of 'a | TermObl of constr
let make ~info ~cinfo ~opaque ~reduce ~deps ~uctx ~body ~possible_guard ?obl_hook ?using obls =
let obls', body =
match body with
| None ->
assert (Int.equal (Array.length obls) 0);
let n = Nameops.add_suffix cinfo.CInfo.name "_obligation" in
( [| { obl_name = n
; obl_body = None
; obl_location = Loc.tag Evar_kinds.InternalHole
; obl_type = cinfo.CInfo.typ
; obl_status = (false, Evar_kinds.Expand)
; obl_deps = Int.Set.empty
; obl_tac = None } |]
, mkVar n )
| Some b ->
( Array.mapi
(fun i (n, t, l, o, d, tac) ->
{ obl_name = n
; obl_body = None
; obl_location = l
; obl_type = t
; obl_status = o
; obl_deps = d
; obl_tac = tac })
obls
, b )
in
let prg_uctx = if info.Info.poly then UState.make_flexible_nonalgebraic uctx
else
(* declare global univs of the main constant before we do obligations *)
let uctx = UState.collapse_sort_variables uctx in
let () = Global.push_context_set (UState.context_set uctx) in
let cst = Constant.make2 (Lib.current_mp()) (Label.of_id cinfo.CInfo.name) in
let () = DeclareUniv.declare_univ_binders (ConstRef cst)
(UState.univ_entry ~poly:false uctx)
in
UState.Internal.reboot (Global.env()) uctx
in
{ prg_cinfo = { cinfo with CInfo.typ = reduce cinfo.CInfo.typ }
; prg_info = info
; prg_using = using
; prg_hook = obl_hook
; prg_opaque = opaque
; prg_body = body
; prg_uctx
; prg_obligations = {obls = obls'; remaining = Array.length obls'}
; prg_deps = deps
; prg_possible_guard = possible_guard
; prg_reduce = reduce }
let show prg =
let { CInfo.name; typ; _ } = prg.prg_cinfo in
let env = Global.env () in
let sigma = Evd.from_env env in
Id.print name ++ spc () ++ str ":" ++ spc ()
++ Printer.pr_constr_env env sigma typ
++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env env sigma prg.prg_body
module Internal = struct
let get_name prg = prg.prg_cinfo.CInfo.name
let get_uctx prg = prg.prg_uctx
let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
let get_poly prg = prg.prg_info.Info.poly
let get_obligations prg = prg.prg_obligations
let get_using prg = prg.prg_using
end
end
open Obligation
open ProgramDecl
(* Saving an obligation *)
(* XXX: Is this the right place for this? *)
let it_mkLambda_or_LetIn_or_clean t ctx =
let open Context.Rel.Declaration in
let fold t decl = if is_local_assum decl then Term.mkLambda_or_LetIn decl t
else if Vars.noccurn 1 t then Vars.subst1 mkProp t
else Term.mkLambda_or_LetIn decl t
in
Context.Rel.fold_inside fold ctx ~init:t
(* XXX: Is this the right place for this? *)
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
let rec aux ctx c ty =
match (Constr.kind c, Constr.kind ty) with
| LetIn (x, b, t, c), LetIn (x', b', t', ty)
when Constr.equal b b' && Constr.equal t t' ->
let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in
aux ctx' c ty
| _, LetIn (x', b', t', ty) ->
let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in
aux ctx' (lift 1 c) ty
| LetIn (x, b, t, c), _ ->
let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in
aux ctx' c (lift 1 ty)
| Lambda (x, b, t), Prod (x', b', t')
(* By invariant, must be convertible *) ->
let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in
aux ctx' t t'
| Cast (c, _, _), _ -> aux ctx c ty
| _, _ -> (ctx, c, ty)
in
aux Context.Rel.empty c ty
(* XXX: What's the relation of this with Abstract.shrink ? *)
let shrink_body c ty =
let ctx, b, ty =
match ty with
| None ->
let ctx, b = Term.decompose_lambda_decls c in
(ctx, b, None)
| Some ty ->
let ctx, b, ty = decompose_lam_prod c ty in
(ctx, b, Some ty)
in
let b', ty', n, args =
List.fold_left
(fun (b, ty, i, args) decl -> if Vars.noccurn 1 b && Option.cata (Vars.noccurn 1) true ty then
(Vars.subst1 mkProp b, Option.map (Vars.subst1 mkProp) ty, succ i, args)
else
let open Context.Rel.Declaration in
let args = if is_local_assum decl then mkRel i :: args else args in
( Term.mkLambda_or_LetIn decl b
, Option.map (Term.mkProd_or_LetIn decl) ty
, succ i
, args ))
(b, ty, 1, []) ctx
in
(ctx, b', ty', Array.of_list args)
(***********************************************************************)
(* Saving an obligation *)
(***********************************************************************)
let universes_of_decl body typ =
let univs_typ = match typ with None -> Univ.Level.Set.empty | Some ty -> Vars.universes_of_constr ty in
let univs_body = Vars.universes_of_constr body in
Univ.Level.Set.union univs_body univs_typ
let update_global_obligation_uctx prg uctx =
let uctx = if prg.prg_info.Info.poly then
(* Accumulate the polymorphic constraints *)
UState.union prg.prg_uctx uctx
else
(* The monomorphic universe context of the main constant has
been declared by the first obligation; it is now in the
global env and we now remove it for the further
declarations *)
UState.Internal.reboot (Global.env ()) uctx in
ProgramDecl.Internal.set_uctx ~uctx prg
let declare_obligation prg obl ~uctx ~types ~body =
let body = prg.prg_reduce body in
let types = Option.map prg.prg_reduce types in
match obl.obl_status with
| _, Evar_kinds.Expand ->
let prg_uctx = UState.union prg.prg_uctx uctx in
let prg = ProgramDecl.Internal.set_uctx ~uctx:prg_uctx prg in
(prg, {obl with obl_body = Some (TermObl body)}, [])
| force, Evar_kinds.Define opaque ->
let opaque = (not force) && opaque in
let poly = prg.prg_info.Info.poly in
let ctx, body, ty, args = ifnot poly then shrink_body body types
else ([], body, types, [||])
in
let uctx' = UState.restrict uctx (universes_of_decl body types) in
let univs = UState.univ_entry ~poly uctx' in
let inst = instance_of_univs univs in
let ce = definition_entry ?types:ty ~opaque ~univs body in
(* ppedrot: seems legit to have obligations as local *)
let constant =
declare_constant ~loc:(fallback_loc ~warn:false obl.obl_name None) ~name:obl.obl_name
~typing_flags:prg.prg_info.Info.typing_flags
~local:Locality.ImportNeedQualified
~kind:Decls.(IsProof Property)
(DefinitionEntry ce)
in
definition_message obl.obl_name;
let prg = update_global_obligation_uctx prg uctx in
let body = if poly then DefinedObl (constant, inst)
else
let const = mkConstU (constant, inst) in
TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (const, args)) ctx)
in
(prg, {obl with obl_body = Some body}, [GlobRef.ConstRef constant])
(* Updating the obligation meta-info on close *)
let not_transp_msg =
Pp.(
str "Obligation should be transparent but was declared opaque."
++ spc ()
++ str "Use 'Defined' instead.")
let err_not_transp () =
CErrors.user_err not_transp_msg
module ProgMap = Id.Map
module State = struct
type t = prg_hook ProgramDecl.t CEphemeron.key ProgMap.t
and prg_hook = PrgHook of t Hook.g
let call_prg_hook { prg_hook=hook } x pm =
let hook = Option.map (fun (PrgHook h) -> h) hook in
Hook.call_g ?hook x pm
let empty = ProgMap.empty
let pending pm =
ProgMap.filter
(fun _ v -> (CEphemeron.get v).prg_obligations.remaining > 0)
pm
let num_pending pm = pending pm |> ProgMap.cardinal
let get_unique_open_prog pm name : (_, Id.t list) result =
match name with
| Some n ->
Option.cata
(fun p -> Ok (CEphemeron.get p))
(Error []) (ProgMap.find_opt n pm)
| None -> (
let n = num_pending pm in
match n with
| 0 -> Error []
| 1 -> Option.cata (fun p -> Ok p) (Error []) (first_pending pm)
| _ ->
let progs = Id.Set.elements (ProgMap.domain pm) in
Error progs )
let add t key prg = ProgMap.add key (CEphemeron.create prg) t
let fold t ~f ~init =
let f k v acc = f k (CEphemeron.get v) acc in
ProgMap.fold f t init
let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v)
let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get
module View = struct
module Obl = struct type t =
{ name : Id.t
; loc : Loc.t option
; status : bool * Evar_kinds.obligation_definition_status
; solved : bool
}
let make (o : Obligation.t) =
let { obl_name; obl_location; obl_status; obl_body; _ } = o in
{ name = obl_name
; loc = fst obl_location
; status = obl_status
; solved = Option.has_some obl_body
}
end
type t =
{ opaque : bool
; remaining : int
; obligations : Obl.t array
}
(* In all cases, the use of the map is read-only so we don't expose the ref *)
let map_non_empty_keys is_empty m =
ProgMap.fold (fun k prg l -> if is_empty prg then l else k :: l) m []
let check_solved_obligations is_empty ~pm ~what_for : unit = ifnot (ProgMap.is_empty pm) then
let keys = map_non_empty_keys is_empty pm in
let have_string = if Int.equal (List.length keys) 1 then" has " else " have " in
CErrors.user_err
Pp.(
str "Unsolved obligations when closing "
++ what_for ++ str ":" ++ spc ()
++ prlist_with_sep spc (fun x -> Id.print x) keys
++ str have_string
++ str "unsolved obligations." )
let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
let progmap_remove pm prg = ProgMap.remove prg.prg_cinfo.CInfo.name pm
let progmap_replace prg' pm = map_replace prg'.prg_cinfo.CInfo.name prg' pm
let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
let obligations_message rem =
Format.asprintf "%s %s remaining"
(ifrem > 0 then string_of_int rem else "No more")
(CString.plural rem "obligation")
|> Pp.str |> Flags.if_verbose Feedback.msg_info
let get_obligation_body expand obl =
match obl.obl_body with
| None -> None
| Some c -> ( if expand && snd obl.obl_status == Evar_kinds.Expand then
match c with
| DefinedObl pc -> Some (Environ.constant_value_in (Global.env ()) pc)
| TermObl c -> Some c
else
match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c )
let obl_substitution expand obls deps =
Int.Set.fold
(fun x acc ->
let xobl = obls.(x) in
match get_obligation_body expand xobl with
| None -> acc
| Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
deps []
let rec intset_to = function
| -1 -> Int.Set.empty
| n -> Int.Set.add n (intset_to (pred n))
let obligation_substitution expand prg =
let obls = prg.prg_obligations.obls in
let ints = intset_to (pred (Array.length obls)) in
obl_substitution expand obls ints
let subst_prog subst prg =
let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
( Vars.replace_vars subst' prg.prg_body
, Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
let declare_definition ~pm prg =
let varsubst = obligation_substitution true prg in
let sigma = Evd.from_ctx prg.prg_uctx in
let body, types = subst_prog varsubst prg in
let body, types = EConstr.(of_constr body, of_constr types) in
let cinfo = { prg.prg_cinfo with CInfo.typ = Some types } in
let name, info, opaque, using = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque, prg.prg_using in
let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
(* XXX: This is doing normalization twice *)
let kn, uctx = declare_definition ~cinfo ~info ~obls ~body ~opaque ?using sigma in
(* XXX: We call the obligation hook here, by consistency with the
previous imperative behaviour, however I'm not sure this is right *)
let pm = State.call_prg_hook prg
{ Hook.S.uctx; obls; scope = prg.prg_info.Info.scope; dref = kn} pm in
let pm = progmap_remove pm prg in
pm, kn
let declare_mutual_definitions ~pm l =
let first = List.hd l in
let defobl x =
let oblsubst = obligation_substitution true x in
let subs, typ = subst_prog oblsubst x in
let sigma = Evd.from_ctx x.prg_uctx in
let term = EConstr.of_constr subs in
let typ = EConstr.of_constr typ in
let term = EConstr.to_constr sigma term in
let typ = EConstr.to_constr sigma typ in
let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in
let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
(def, oblsubst)
in
let defs, obls = List.split (List.map defobl l) in
let obls = List.flatten obls in
let fixitems = List.map2 (fun (d, typ, impargs) name ->
let loc = fallback_loc ~warn:false name None in
CInfo.make ?loc ~name ~typ ~impargs ()) defs first.prg_deps in
let fixdefs, fixtypes, _ = List.split3 defs in
let possible_guard = Option.get first.prg_possible_guard in
(* Declare the recursive definitions *)
let kns =
declare_mutual_definitions ~info:first.prg_info
~uctx:first.prg_uctx ~bodies:fixdefs ~possible_guard ~opaque:first.prg_opaque
~cinfo:fixitems ?using:first.prg_using ()
in
(* Only for the first constant *)
let dref = List.hd kns in
let scope = first.prg_info.Info.scope in
let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in
Hook.call ?hook:first.prg_info.Info.hook s_hook;
(* XXX: We call the obligation hook here, by consistency with the
previous imperative behaviour, however I'm not sure this is right *)
let pm = State.call_prg_hook first s_hook pm in
let pm = List.fold_left progmap_remove pm l in
pm, dref
let update_obls ~pm prg obls rem =
let prg_obligations = {obls; remaining = rem} in
let prg' = {prg with prg_obligations} in
let pm = progmap_replace prg' pm in
obligations_message rem; ifrem > 0 then pm, Remain rem
else
match prg'.prg_deps with
| [] ->
let pm, kn = declare_definition ~pm prg' in
pm, Defined kn
| l ->
let progs =
List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps
in if List.for_all (fun x -> obligations_solved x) progs then
let pm, kn = declare_mutual_definitions ~pm progs in
pm, Defined kn
else pm, Dependent
let dependencies obls n =
let res = ref Int.Set.empty in
Array.iteri
(fun i obl -> if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then
res := Int.Set.add i !res)
obls;
!res
let update_program_decl_on_defined ~pm prg obls num obl rem ~auto =
let obls = Array.copy obls in
let () = obls.(num) <- obl in
let pm, _progress = update_obls ~pm prg obls (pred rem) in
let pm = if pred rem > 0 then
let deps = dependencies obls num in ifnot (Int.Set.is_empty deps) then
let pm, _progress = auto ~pm (Some prg.prg_cinfo.CInfo.name) deps None in
pm
else pm
else pm
in
pm
type obligation_resolver =
pm:State.t
-> Id.t option
-> Int.Set.t
-> unit Proofview.tactic option
-> State.t * progress
type obl_check_final = AllFinal | SpecificFinal of Id.t
type obligation_qed_info = {
name : Id.t;
num : int;
auto : obligation_resolver;
check_final : obl_check_final option;
}
let not_final_obligation n =
let msg = match n with
| AllFinal -> str "This obligation is not final."
--> --------------------
--> maximum size reached
--> --------------------
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.53Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
