Derive plugin.

A small plugin to support program deriving (à la Richard Bird) in Coq.

It's fairly simple:

  Require Coq.Derive.Derive.

  Derive f From g Upto eq As h.

Produces a goal (actually two, but the first one is automatically shelved):

  |- eq g ?42

And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).

6 files changed, 108 insertions, 0 deletions

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..c6a96b31a
--- /dev/null
+++ b/plugins/Derive/derive.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  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 interp_init_def_and_relation env sigma init_def r =
+  let init_def = Constrintern.interp_constr sigma env init_def in
+  let init_type = Typing.type_of env sigma init_def in
+
+  let r_type =
+    let open Term in
+    mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp))
+  in
+  let r = Constrintern.interp_casted_constr sigma env r r_type in
+  init_def , init_type , r
+  
+
+(** [start_deriving f init r lemma] starts a proof of [r init
+    ?x]. When the proof ends, [f] is defined as the value of [?x] and
+    [lemma] as the proof. *)
+let start_deriving f init_def r lemma =
+  let env = Global.env () in
+  let kind = Decl_kinds.(Global,DefinitionBody Definition) in
+  let ( init_def , init_type , r ) =
+    interp_init_def_and_relation env Evd.empty init_def r
+  in
+  let goals =
+    let open Proofview in
+    TCons ( env , init_type , (fun ef ->
+      TCons ( env , Term.mkApp ( r , [| init_def ; ef |] ) , (fun _ -> TNil))))
+  in
+  let terminator com =
+    let open Proof_global in
+    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) ->
+        let (f_def,lemma_def) =
+          match Proof_global.(obj.entries) with
+          | [f_def;lemma_def] ->
+              f_def , lemma_def
+          | _ -> assert false
+        in
+        (* The opacity of [f_def] is adjusted to be [false]. *)
+        let f_def = let open Entries in { f_def with
+          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 lemma_typ = Term.(mkApp ( r , [| init_def ; mkConst f_kn |] )) in
+        (* The type of [lemma_def] is adjusted to refer to [f_kn], the
+           opacity is adjusted by the proof ending command.  *)
+        let lemma_def = let open Entries in { lemma_def with
+          const_entry_type = Some lemma_typ ;
+          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 1 shelve) p
+  end in
+  ()
+
diff --git a/plugins/Derive/derive.mli b/plugins/Derive/derive.mli
new file mode 100644
index 000000000..33f982bb6
--- /dev/null
+++ b/plugins/Derive/derive.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*  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 init r lemma] starts a proof of [r init
+    ?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 -> 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..354643c09
--- /dev/null
+++ b/plugins/Derive/g_derive.ml4
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  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*)
+
+(* arnaud: on a sans doute besoin des noms dans la liste. *)
+(* arnaud: est-ce que VtNow signifie bien qu'on ne peut pas skipper la preuve? *)
+let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtNow)
+
+VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
+| [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] ->
+     [ Derive.start_deriving f init r 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