From d08532d5344d96d10604760fa44109c9d56e73ce Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 8 Jan 2015 18:18:02 +0100 Subject: Avoiding introducing yet another convention in naming files. --- plugins/Derive/Derive.v | 1 - plugins/Derive/derive.ml | 104 ------------------------------------- plugins/Derive/derive.mli | 13 ----- plugins/Derive/derive_plugin.mllib | 2 - plugins/Derive/g_derive.ml4 | 16 ------ plugins/Derive/vo.itarget | 1 - plugins/derive/Derive.v | 1 + plugins/derive/derive.ml | 104 +++++++++++++++++++++++++++++++++++++ plugins/derive/derive.mli | 13 +++++ plugins/derive/derive_plugin.mllib | 2 + plugins/derive/g_derive.ml4 | 16 ++++++ plugins/derive/vo.itarget | 1 + plugins/quote/quote.ml | 2 +- 13 files changed, 138 insertions(+), 138 deletions(-) delete mode 100644 plugins/Derive/Derive.v delete mode 100644 plugins/Derive/derive.ml delete mode 100644 plugins/Derive/derive.mli delete mode 100644 plugins/Derive/derive_plugin.mllib delete mode 100644 plugins/Derive/g_derive.ml4 delete mode 100644 plugins/Derive/vo.itarget create mode 100644 plugins/derive/Derive.v create mode 100644 plugins/derive/derive.ml create mode 100644 plugins/derive/derive.mli create mode 100644 plugins/derive/derive_plugin.mllib create mode 100644 plugins/derive/g_derive.ml4 create mode 100644 plugins/derive/vo.itarget (limited to 'plugins') 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 *) -(* 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 *) -(* 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 *) -(* - [ 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 diff --git a/plugins/derive/Derive.v b/plugins/derive/Derive.v new file mode 100644 index 000000000..0d5a93b03 --- /dev/null +++ b/plugins/derive/Derive.v @@ -0,0 +1 @@ +Declare ML Module "derive_plugin". \ No newline at end of file diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml new file mode 100644 index 000000000..156c9771a --- /dev/null +++ b/plugins/derive/derive.ml @@ -0,0 +1,104 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 new file mode 100644 index 000000000..5157c4a27 --- /dev/null +++ b/plugins/derive/derive.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Constrexpr.constr_expr -> Names.Id.t -> unit diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mllib new file mode 100644 index 000000000..5ee0fc6da --- /dev/null +++ b/plugins/derive/derive_plugin.mllib @@ -0,0 +1,2 @@ +Derive +G_derive diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 new file mode 100644 index 000000000..0721c675f --- /dev/null +++ b/plugins/derive/g_derive.ml4 @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + [ Derive.start_deriving f suchthat lemma ] +END diff --git a/plugins/derive/vo.itarget b/plugins/derive/vo.itarget new file mode 100644 index 000000000..b48098219 --- /dev/null +++ b/plugins/derive/vo.itarget @@ -0,0 +1 @@ +Derive.vo \ No newline at end of file diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 64166a0de..1299c99ef 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -107,7 +107,7 @@ open Names open Term open Pattern open Patternops -open ConstrMatching +open Constr_matching open Tacmach (*i*) -- cgit v1.2.3