diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-08 18:18:02 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-08 19:05:14 +0100 |
commit | d08532d5344d96d10604760fa44109c9d56e73ce (patch) | |
tree | 2f5b472f526a6ad9f72cb57bde4503501f9c7129 /plugins/Derive | |
parent | b584c5529f7195849b0dd4f1eebf7c73c46f60db (diff) |
Avoiding introducing yet another convention in naming files.
Diffstat (limited to 'plugins/Derive')
-rw-r--r-- | plugins/Derive/Derive.v | 1 | ||||
-rw-r--r-- | plugins/Derive/derive.ml | 104 | ||||
-rw-r--r-- | plugins/Derive/derive.mli | 13 | ||||
-rw-r--r-- | plugins/Derive/derive_plugin.mllib | 2 | ||||
-rw-r--r-- | plugins/Derive/g_derive.ml4 | 16 | ||||
-rw-r--r-- | plugins/Derive/vo.itarget | 1 |
6 files changed, 0 insertions, 137 deletions
diff --git a/plugins/Derive/Derive.v b/plugins/Derive/Derive.v deleted file mode 100644 index 0d5a93b03..000000000 --- a/plugins/Derive/Derive.v +++ /dev/null @@ -1 +0,0 @@ -Declare ML Module "derive_plugin".
\ No newline at end of file diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml deleted file mode 100644 index 156c9771a..000000000 --- a/plugins/Derive/derive.ml +++ /dev/null @@ -1,104 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body) - : Entries.const_entry_body = - Future.chain ~pure:true 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 env = Global.env () in - let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - - (** 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 = Term.mkSort f_type_sort 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 env' = Environ.push_named (f , (Some ef) , f_type) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , 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 -> Errors.error"Admitted isn't supported in Derive." - | Proved (_,Some _,_) -> - Errors.error"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 , 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 = 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 () = Proof_global.start_dependent_proof lemma kind goals terminator in - let _ = Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p - end in - () - - - - diff --git a/plugins/Derive/derive.mli b/plugins/Derive/derive.mli deleted file mode 100644 index 5157c4a27..000000000 --- a/plugins/Derive/derive.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** [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. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> unit diff --git a/plugins/Derive/derive_plugin.mllib b/plugins/Derive/derive_plugin.mllib deleted file mode 100644 index 5ee0fc6da..000000000 --- a/plugins/Derive/derive_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Derive -G_derive diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4 deleted file mode 100644 index 0721c675f..000000000 --- a/plugins/Derive/g_derive.ml4 +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "grammar/grammar.cma" i*) - -let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) - -VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command -| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - [ Derive.start_deriving f suchthat lemma ] -END diff --git a/plugins/Derive/vo.itarget b/plugins/Derive/vo.itarget deleted file mode 100644 index b48098219..000000000 --- a/plugins/Derive/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Derive.vo
\ No newline at end of file |