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 + 6 files changed, 137 insertions(+) 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/derive') 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 -- cgit v1.2.3