diff --git a/doc/changelog/02-specification-language/19092-master+fix18951-anomaly-derive-admitted.rst b/doc/changelog/02-specification-language/19092-master+fix18951-anomaly-derive-admitted.rst new file mode 100644 index 000000000000..767760aa4ed0 --- /dev/null +++ b/doc/changelog/02-specification-language/19092-master+fix18951-anomaly-derive-admitted.rst @@ -0,0 +1,5 @@ +- **Fixed:** + :cmd:`Derive` now supports :cmd:`Admitted` + (`#19092 `_, + fixes `#18951 `_, + by Hugo Herbelin). diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 12d566834a5b..2f2679a79bd0 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -8,14 +8,18 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Context open Context.Named.Declaration +open Vernacentries.DefAttributes (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -let start_deriving f suchthat name : Declare.Proof.t = +let start_deriving ~atts CAst.{v=f;loc} suchthat name : Declare.Proof.t = + + let scope, _local, poly, program_mode, user_warns, typing_flags, using, clearbody = + atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in + if program_mode then CErrors.user_err (Pp.str "Program mode not supported."); let env = Global.env () in let sigma = Evd.from_env env in @@ -24,22 +28,26 @@ let start_deriving f suchthat name : Declare.Proof.t = (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one that looked the most general. *) - let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in - let f_type_type = EConstr.mkSort f_type_sort in + let sigma, (f_type, f_impargs) = + let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in + let f_type_type = EConstr.mkSort f_type_sort in + let sigma, f_type = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.GoalEvar) ~typeclass_candidate:false f_type_type in + let sigma = Evd.shelve sigma [fst (EConstr.destEvar sigma f_type)] in + sigma, (f_type, []) + in + let (sigma, ef) = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.GoalEvar) ~typeclass_candidate:false f_type in + let env' = EConstr.push_named (LocalDef (EConstr.annotR f, ef, f_type)) env in + let impls = Names.Id.Map.add f (Constrintern.compute_internalization_data env sigma f Constrintern.Variable f_type f_impargs) Constrintern.empty_internalization_env in + let sigma = Evd.shelve sigma [fst (EConstr.destEvar sigma ef)] in + let sigma, (suchthat, impargs) = Constrintern.interp_type_evars_impls env' sigma ~impls suchthat in (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in - TCons ( env , sigma , f_type_type , (fun sigma f_type -> - TCons ( env , sigma , f_type , (fun sigma ef -> - let f_type = EConstr.Unsafe.to_constr f_type in - let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in - TCons ( env' , sigma , suchthat , (fun sigma _ -> - TNil sigma)))))) - in - - let info = Declare.Info.make ~poly:false ~kind () in - let lemma = Declare.Proof.start_derive ~name ~f ~info goals in + TCons ( env , sigma , f_type , (fun sigma ef' -> + let sigma = Evd.define (fst (EConstr.destEvar sigma ef')) ef sigma in + TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))) in + let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ?typing_flags ?user_warns () in (* TODO: udecl *) + let cinfo = Declare.CInfo.[make ~name:f ~typ:() ~impargs:f_impargs (); make ~name ~typ:() ~impargs ()] in + let lemma = Declare.Proof.start_derive ~name ~f ~info ~cinfo goals in Declare.Proof.map lemma ~f:(fun p -> - Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 1 shelve) p) diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 06e7dacd3611..49740dc9534a 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -13,7 +13,8 @@ [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) val start_deriving - : Names.Id.t + : atts:Vernacentries.DefAttributes.t + -> Names.Id.t CAst.t -> Constrexpr.constr_expr -> Names.Id.t -> Declare.Proof.t diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 21cbf167accb..70c237fcf44e 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -23,6 +23,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof -| [ "Derive" identref(f) "SuchThat" constr(suchthat) "As" identref(lemma) ] -> - { Derive.start_deriving f.CAst.v suchthat lemma.CAst.v } +| #[ atts = Vernacentries.DefAttributes.def_attributes; ] + [ "Derive" identref(f) "SuchThat" constr(suchthat) "As" identref(lemma) ] -> + { Derive.start_deriving ~atts f suchthat lemma.CAst.v } END diff --git a/test-suite/bugs/bug_19234.v b/test-suite/bugs/bug_19234.v new file mode 100644 index 000000000000..40ec250f19bd --- /dev/null +++ b/test-suite/bugs/bug_19234.v @@ -0,0 +1,7 @@ +Require Import Derive. +Derive b SuchThat b As spec. +Unshelve. +2:exact Type. +unfold b. +exact Type. +Defined. diff --git a/test-suite/success/Derive.v b/test-suite/success/Derive.v new file mode 100644 index 000000000000..a0d0d3968369 --- /dev/null +++ b/test-suite/success/Derive.v @@ -0,0 +1,10 @@ +Require Import Derive. + +(* Tests when x is refined by typechecking *) +Derive x SuchThat (eq_refl x = eq_refl 0) As x_ok. +reflexivity. +Qed. + +Derive s SuchThat (forall z, eq_refl (s z) = eq_refl (S z)) As s_ok. +reflexivity. +Qed. diff --git a/vernac/declare.ml b/vernac/declare.ml index f3fe67412324..f13340c6540c 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1641,11 +1641,10 @@ let start_core ~info ~cinfo ?proof_ending ?using sigma = let start = start_core ?proof_ending:None -let start_dependent ~info ~name ~proof_ending goals = +let start_dependent ~info ~cinfo ~name ~proof_ending goals = let { Info.poly; typing_flags; _ } = info in let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in let initial_euctx = Evd.ustate Proof.((data proof).sigma) in - let cinfo = [] in let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in { proof ; endline_tactic = None @@ -1654,13 +1653,13 @@ let start_dependent ~info ~name ~proof_ending goals = ; pinfo } -let start_derive ~f ~name ~info goals = +let start_derive ~f ~name ~info ~cinfo goals = let proof_ending = Proof_ending.End_derive {f; name} in - start_dependent ~info ~name ~proof_ending goals + start_dependent ~info ~cinfo ~name ~proof_ending goals let start_equations ~name ~info ~hook ~types sigma goals = let proof_ending = Proof_ending.End_equations {hook; i=name; types; sigma} in - start_dependent ~name ~info ~proof_ending goals + start_dependent ~name ~cinfo:[] ~info ~proof_ending goals let start_definition ~info ~cinfo ?using sigma = let { CInfo.name; typ; args } = cinfo in @@ -2239,6 +2238,7 @@ let finish_admitted ~pm ~pinfo ~uctx ~sec_vars typs = let save_admitted ~pm ~proof = let Proof.{ entry; sigma } = Proof.data (get proof) in let typs = List.map pi3 (Proofview.initial_goals entry) in + List.iter (check_type_evars_solved (Global.env()) sigma) typs; let iproof = get proof in List.iter (check_type_evars_solved (Global.env()) sigma) typs; let sec_vars = compute_proof_using_for_admitted proof.pinfo proof typs iproof in @@ -2256,42 +2256,28 @@ let save_admitted ~pm ~proof = (* Saving a lemma-like constant *) (************************************************************************) -let finish_derived ~f ~name ~entries = +let finish_derived ~f ~name {entries; pinfo; uctx} = (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) - let f_def, lemma_def = - match entries with - | [_;f_def;lemma_def] -> - f_def, lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = ProofEntry.set_transparent_for_derived f_def in - let f_kind = Decls.(IsDefinition Definition) in - let f_def = DefinitionEntry f_def in - let f_kn = declare_constant ~name:f ~kind:f_kind f_def ~typing_flags:None in - (* Derive does not support univ poly *) - let () = assert (not (Global.is_polymorphic (ConstRef f_kn))) in - let f_kn_term = Constr.UnsafeMonomorphic.mkConst f_kn in - (* In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype typ = - match typ with - | Some t -> Some (substf t) - | None -> assert false (* Declare always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_def = ProofEntry.map_entry_type lemma_def ~f:lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_def = ProofEntry.map_proof_entry lemma_def ~f:(fun (b,fx) -> (substf b, fx)) in - let lemma_def = DefinitionEntry lemma_def in - let ct = declare_constant ~name ~typing_flags:None ~kind:Decls.(IsProof Proposition) lemma_def in - [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct] + let { Proof_info.info = { Info.hook; scope; clearbody; kind; typing_flags; user_warns; poly; udecl; _ } } = pinfo in + let _, _, refs, _ = + List.fold_left2 (fun (i, subst, refs, used_univs) CInfo.{name; impargs} entry -> + (* The opacity of the specification is adjusted to be [false], as it must.*) + let entry = if i = 0 then ProofEntry.set_transparent_for_derived entry else entry in + let f c = UState.nf_universes uctx (Vars.replace_vars subst c) in + let entry = ProofEntry.map_entry_type entry ~f:(Option.map f) in + let entry = ProofEntry.map_proof_entry entry ~f:(fun (b,fx) -> (f b, fx)) in + let used_univs_body = Vars.universes_of_constr (fst (fst (ProofEntry.get_entry_body entry))) (* Currently assume not delayed *) in + let used_univs_typ = Option.cata Vars.universes_of_constr Univ.Level.Set.empty entry.proof_entry_type in + let used_univs = Univ.Level.Set.union used_univs (Univ.Level.Set.union used_univs_body used_univs_typ) in + let uctx' = UState.restrict uctx used_univs in + let entry = { entry with proof_entry_universes = UState.check_univ_decl ~poly uctx' udecl } in + let gref = declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~uctx entry in + let cst = match gref with ConstRef cst -> cst | _ -> assert false in + let inst = instance_of_univs entry.proof_entry_universes in + (i+1, (name, Constr.mkConstU (cst,inst))::subst, gref::refs, used_univs)) + (0, [], [], Univ.Level.Set.empty) pinfo.Proof_info.cinfo entries in + refs let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = @@ -2331,7 +2317,7 @@ let finish_proof ~pm proof_obj proof_info = let entry, uctx = check_single_entry proof_obj "Obligation.save" in Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo | End_derive { f ; name } -> - pm, finish_derived ~f ~name ~entries:proof_obj.entries + pm, finish_derived ~f ~name proof_obj | End_equations { hook; i; types; sigma } -> let kind = proof_info.Proof_info.info.Info.kind in finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma diff --git a/vernac/declare.mli b/vernac/declare.mli index 22badc20c91e..60e2f932b5fa 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -193,7 +193,7 @@ module Proof : sig both of them. Please, get in touch with the developers if you would like to experiment with multi-goal dependent proofs so we can use your input on the design of the new API. *) - val start_derive : f:Id.t -> name:Id.t -> info:Info.t -> Proofview.telescope -> t + val start_derive : f:Id.t -> name:Id.t -> info:Info.t -> cinfo:unit CInfo.t list -> Proofview.telescope -> t val start_equations : name:Id.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6f796b679052..de818d00de3f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -104,24 +104,27 @@ module DefAttributes = struct let clearbody = bool_attribute ~name:"clearbody" (* [XXX] EJGA: coercion is unused here *) - let parse ?(coercion=false) ?(discharge=NoDischarge,"","") f = + let def_attributes_gen ?(coercion=false) ?(discharge=NoDischarge,"","") () = let discharge, deprecated_thing, replacement = discharge in let clearbody = match discharge with DoDischarge -> clearbody | NoDischarge -> return None in - let (((((((locality, user_warns), polymorphic), program), - canonical_instance), typing_flags), using), - reversible), clearbody = - parse (locality ++ user_warns_with_use_globref_instead ++ polymorphic ++ program ++ - canonical_instance ++ typing_flags ++ using ++ - reversible ++ clearbody) - f - in - let using = Option.map Proof_using.using_from_string using in - let reversible = Option.default false reversible in - let () = if Option.has_some clearbody && not (Lib.sections_are_opened()) - then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.") - in - let scope = scope_of_locality locality discharge deprecated_thing replacement in - { scope; locality; polymorphic; program; user_warns; canonical_instance; typing_flags; using; reversible; clearbody } + (locality ++ user_warns_with_use_globref_instead ++ polymorphic ++ program ++ + canonical_instance ++ typing_flags ++ using ++ + reversible ++ clearbody) >>= fun ((((((((locality, user_warns), polymorphic), program), + canonical_instance), typing_flags), using), + reversible), clearbody) -> + let using = Option.map Proof_using.using_from_string using in + let reversible = Option.default false reversible in + let () = if Option.has_some clearbody && not (Lib.sections_are_opened()) + then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.") + in + let scope = scope_of_locality locality discharge deprecated_thing replacement in + return { scope; locality; polymorphic; program; user_warns; canonical_instance; typing_flags; using; reversible; clearbody } + + let parse ?coercion ?discharge f = + Attributes.parse (def_attributes_gen ?coercion ?discharge ()) f + + let def_attributes = def_attributes_gen () + end let with_def_attributes ?coercion ?discharge ~atts f = diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 74f76da93353..eef655c12f8d 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -71,3 +71,22 @@ val preprocess_inductive_decl -> Vernacexpr.inductive_kind -> (Vernacexpr.inductive_expr * Vernacexpr.notation_declaration list) list -> Preprocessed_Mind_decl.t + +module DefAttributes : sig + +type t = { + scope : Locality.definition_scope; + locality : bool option; + polymorphic : bool; + program : bool; + user_warns : Globnames.extended_global_reference UserWarn.with_qf option; + canonical_instance : bool; + typing_flags : Declarations.typing_flags option; + using : Vernacexpr.section_subset_expr option; + reversible : bool; + clearbody: bool option; +} + +val def_attributes : t Attributes.attribute + +end