diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 94 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 8 | ||||
| -rw-r--r-- | plugins/derive/g_derive.mlg | 10 |
3 files changed, 28 insertions, 84 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4425e41652..ead78f70a1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -8,25 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) - : Safe_typing.private_constants Entries.const_entry_body = - Future.chain x begin fun ((b,ctx),fx) -> - (f b , ctx) , fx - end - (** [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 lemma = +let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in + let poly = false in + let kind = Decls.(IsDefinition Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one @@ -36,72 +30,18 @@ let start_deriving f suchthat lemma = (* 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_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 - - (* The terminator handles the registering of constants when the proof is closed. *) - let terminator com = - let open Proof_global in - (* Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) - let (opaque,f_def,lemma_def) = - match com with - | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Proved (_,Some _,_) -> - CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Proved (opaque, None, obj) -> - match Proof_global.(obj.entries) with - | [_;f_def;lemma_def] -> - opaque <> Proof_global.Transparent , 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 = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in - let f_kn = Declare.declare_constant f f_def in - let f_kn_term = 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 = - match Entries.(lemma_def.const_entry_type) with - | Some t -> t - | None -> assert false (* Proof_global always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_body = - map_const_entry_body substf Entries.(lemma_def.const_entry_body) - in - let lemma_def = let open Entries in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } - in - let lemma_def = - Entries.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) - in - ignore (Declare.declare_constant lemma lemma_def) - in + 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 terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - fst @@ Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p - end pstate + let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in + let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in + Lemmas.pf_map (Proof_global.map_proof begin fun p -> + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + end) lemma diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..d4c62e802e 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,4 +12,8 @@ (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. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t +val start_deriving + : Names.Id.t + -> Constrexpr.constr_expr + -> Names.Id.t + -> Lemmas.t diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 214a9d8bb5..bfb67462a0 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -18,11 +18,11 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } -VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) } +VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof +| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + { Derive.start_deriving f suchthat lemma } END |