Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

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).
  • Loading branch information...
commit 078efbe2dfff0b783cd35b0b3ab2354f554e95a6 1 parent 3c199b8
@aspiwack aspiwack authored
View
9 Makefile.common
@@ -67,7 +67,7 @@ CORESRCDIRS:=\
PLUGINS:=\
omega romega micromega quote \
setoid_ring xml extraction fourier \
- cc funind firstorder \
+ cc funind firstorder Derive \
rtauto nsatz syntax decl_mode btauto
SRCDIRS:=\
@@ -183,12 +183,14 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
ascii_syntax_plugin.cma \
string_syntax_plugin.cma )
DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
+DERIVECMA:=plugins/Derive/derive_plugin.cma
PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
$(QUOTECMA) $(RINGCMA) \
$(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
$(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
- $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
+ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \
+ $(DERIVECMA)
ifneq ($(HASNATDYNLINK),false)
STATICPLUGINS:=
@@ -305,11 +307,12 @@ RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
XMLVO:=
CCVO:=
+DERIVEVO:=$(call cat_vo_itarget, plugins/Derive)
PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
$(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
$(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \
- $(NSATZVO) $(EXTRACTIONVO)
+ $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO)
ALLVO:= $(THEORIESVO) $(PLUGINSVO)
VFILES:= $(ALLVO:.vo=.v)
View
1  plugins/Derive/Derive.v
@@ -0,0 +1 @@
+Declare ML Module "derive_plugin".
View
74 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
+ ()
+
View
12 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
View
2  plugins/Derive/derive_plugin.mllib
@@ -0,0 +1,2 @@
+Derive
+G_derive
View
18 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
View
1  plugins/Derive/vo.itarget
@@ -0,0 +1 @@
+Derive.vo
View
1  plugins/pluginsbyte.itarget
@@ -19,3 +19,4 @@ syntax/r_syntax_plugin.cma
syntax/string_syntax_plugin.cma
syntax/z_syntax_plugin.cma
quote/quote_plugin.cma
+Derive/derive_plugin.cma
View
1  plugins/pluginsdyn.itarget
@@ -22,3 +22,4 @@ syntax/r_syntax_plugin.cmxs
syntax/string_syntax_plugin.cmxs
syntax/z_syntax_plugin.cmxs
quote/quote_plugin.cmxs
+Derive/derive_plugin.cmxs
View
1  plugins/pluginsopt.itarget
@@ -19,3 +19,4 @@ syntax/r_syntax_plugin.cmxa
syntax/string_syntax_plugin.cmxa
syntax/z_syntax_plugin.cmxa
quote/quote_plugin.cmxa
+Derive/derive_plugin.cmxa
View
1  plugins/pluginsvo.itarget
@@ -9,3 +9,4 @@ romega/vo.otarget
rtauto/vo.otarget
setoid_ring/vo.otarget
extraction/vo.otarget
+Derive/vo.otarget
Please sign in to comment.
Something went wrong with that request. Please try again.