Merge pull request #64 from uwplse/0.1

0.1 release

.gitignore

@@ -2,6 +2,7 @@ plugin/*~
 plugin/src/*~
 plugin/*.coq.bak
 plugin/*.cmi
+*.d
 *.ml4.d
 *.mli.d
 *.ml.d
@@ -21,3 +22,4 @@ plugin/*.cmi
 *.a
 *.cmxa
 *.conf
+.merlin

.gitmodules

@@ -0,0 +1,9 @@
+[submodule "plugin/src/coq-plugin-lib"]
+	path = plugin/src/coq-plugin-lib
+	url = https://github.com/uwplse/coq-plugin-lib.git
+[submodule "plugin/deps/fix-to-elim"]
+	path = plugin/deps/fix-to-elim
+	url = https://github.com/uwplse/fix-to-elim.git
+[submodule "plugin/deps/ornamental-search"]
+	path = plugin/deps/ornamental-search
+	url = https://github.com/uwplse/ornamental-search.git

licensing/LICENSE → LICENSE

@@ -1,6 +1,6 @@
 The MIT License (MIT)
 
-Copyright (c) 2017 Talia Ringer, Nate Yazdani
+Copyright (c) 2017-2019 Talia Ringer, Nate Yazdani
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -1,19 +1,29 @@
-**!!! IMPORTANT NOTE: If you came here for DEVOID, it is currently located [here](https://github.com/uwplse/ornamental-search). By ITP, this plugin will include DEVOID as a dependency. !!!**
+Welcome to the PUMPKIN PATCH proof repair plugin suite!
+This plugin suite is a collection of plugins for maintaining proofs as
+specifications change over time:
 
-# PUMPKIN PATCH User Guide
+* PUMPKIN PATCH ([paper](http://tlringer.github.io/pdf/pumpkinpaper.pdf), [talk video](http://www.youtube.com/watch?v=p-V9oerg5DU)): example-based proof repair
+* DEVOID ([paper](http://tlringer.github.io/pdf/ornpaper.pdf), [standalone plugin](https://github.com/uwplse/ornamental-search)): reusing functions and proofs over unindexed types to derive indexed versions
+
+In addition, this plugin suite includes some development tools, like
+the [fix-to-elim](https://github.com/uwplse/fix-to-elim) plugin for automatic
+fixpoint translation, that may be useful for plugin developers and Coq
+contributors more broadly. We discuss these briefly at the end of the document.
+
+All of these tools, including DEVOID, are included as dependencies of the 
+main PUMPKIN PATCH plugin, so you can use both at the same time.
+**More information on using DEVOID
+can be found in the the standalone plugin repository. The remainder of this
+document will focus on how to use the main PUMPKIN PATCH plugin.**
+We hope to add an example of using these both together soon.
+
+# PUMPKIN PATCH for Users
 
 This is a prototype plugin for finding patches for broken Coq proofs.
 To use PUMPKIN, the programmer modifies a single proof script to provide 
 an _example_ adaptation of a proof to a change. PUMPKIN generalizes this example 
 into a _reusable patch_ which can be used to fix other broken proofs.
 
-This is a research prototype, so it is definitely not production-ready.
-With that in mind, I hope that by getting it out into the open I can
-contribute what I've learned so far. You can use it on the example proofs and
-you can extend it if you are interested. Don't hesitate to reach out
-if you have any questions. Similarly, please let me know if anything I have mentioned
-in this user guide does not work or is unclear.
-
 Reading the [paper](http://tlringer.github.io/pdf/pumpkinpaper.pdf) may help if you are interested
 in understanding the internals of the tool. The paper links to a release that captures
 the code as it was when we wrote the paper. The [talk video](http://www.youtube.com/watch?v=p-V9oerg5DU)
@@ -26,7 +36,7 @@ longer maintaining.
 
 ```
 cd plugin
-make
+./build.sh
 ```
 
 If you would like to use PUMPKIN in all of your developments, add this line:
@@ -175,6 +185,7 @@ Patch Proof Old'.old New'.new as patch.
 See [Preprocess.v](/plugin/coq/Preprocess.v) and [PreprocessModule.v](/plugin/coq/PreprocessModule.v) for examples
 of how to use these commands. There are also proofs in [Regress.v](/plugin/coq/Regress.v) and [IntegersNew.v](/plugin/coq/IntegersNew.v) 
 that demonstrate its use with `Patch Proof`.
+This command is available as a [standalone plugin](https://github.com/uwplse/fix-to-elim) as well, if you are interested.
 
 ### Cutting Lemmas
 
@@ -211,16 +222,20 @@ around limitations.
 
 ### Support & Limitations
 
-Speaking of limitations: PUMPKIN is a research prototype, and so it is currently limited in the 
+PUMPKIN is a research prototype, and so it is currently limited in the 
 kinds of proofs and changes it supports. PUMPKIN is best equipped to handle changes in conclusions of inductive proofs.
 It has introductory support for changes in hypotheses.
 It also supports certain changes in definitions (for example, changes in a constructors
 of an inductive type that a proof inducts over, or changes in a case of a fixpoint that a theorem applies),
 and some other styles of proofs (for example, simple applicative proofs, or
 proofs that apply constructors).
 
-PUMPKIN does not yet support structural changes like adding new hypotheses,
-adding constructors or parameters to an inductive type, or adding cases to a fixpoint.
+With the help of [DEVOID](https://github.com/uwplse/ornamental-search), PUMPKIN 
+can also handle certain changes from unindexed types to indexed versions.
+Please see the DEVOID repository for more of those examples.
+
+PUMPKIN does not yet support adding new hypotheses,
+adding constructors to an inductive type, or adding cases to a fixpoint.
 PUMPKIN has very limited support for proofs using logic specific to decidable domains
 (such as proofs that use `omega`) and nested induction.
 Supporting all of these features is on our roadmap.
@@ -284,10 +299,20 @@ The relevant examples are as follows:
 9. [Theorem.v](/plugin/coq/Theorem.v): Example fo the experimental theorem patching command
 10. [Hypotheses.v](/plugin/coq/Hypotheses.v): Very simple changes in hypotheses.
 
-## Extending PUMPKIN
+# PUMPKIN PATCH for Developers
+
+We welcome contributors! Especially those willing to help us
+with build tools, continuous integration, updating Coq versions,
+documentation, and other infrastructure.
+
+In addition, we have included some useful infrastructure for plugin
+developers more broadly.
+
+## Contributing
 
 If you've never written a Coq plugin before, you might want to check out
-and toy with my [starter plugin](http://github.com/uwplse/CoqAST/) first. 
+the [plugin tutorials](https://github.com/coq/coq/tree/master/doc/plugin_tutorial)
+in the main Coq repository.
 
 To get an idea of how the code is structured, I highly recommend reading Section 5 of the paper
 and following along in the code. The entry-point to the code is [patcher.ml4](/plugin/src/patcher.ml4). 
@@ -298,11 +323,23 @@ if you are modifying the tool, you may want to use it.
 Minor note: .ml4 files don't appear to work with a lot of emacs OCaml plugins.
 You can run tuareg-mode manually on .ml4 files.
 
-## Contributors
+## Developer Tools
+
+This plugin suite includes two useful tools for plugin developers:
+
+* The [fix-to-elim](https://github.com/uwplse/fix-to-elim) plugin for translating fixpoints to inductive proofs
+* The [coq-plugin-lib](https://github.com/uwplse/coq-plugin-lib) library for plugin development
+
+# Contributors
 
 This plugin is maintained by Talia Ringer with help from Nate Yazdani.
 John Leo and Dan Grossman have made conceptual contributions.
 
 The following community members have also contributed to the code:
 1. Emilio Jesús Gallego Arias
 2. Your name here!
+
+# Licensing
+
+We use the MIT license because we think that Coq plugins are allowed to do so.
+If this is incorrect, please let us know kindly so we can fix it.

plugin/_CoqProject

@@ -1,9 +1,19 @@
--I src/library/utilities
--I src/library/categories
--I src/library/coq
--I src/library/proofsearch/representation
--I src/library/proofsearch/compilation
--I src/core/configuration
+-I src/coq-plugin-lib/src/utilities
+-I src/coq-plugin-lib/src/coq
+-I src/coq-plugin-lib/src/coq/termutils
+-I src/coq-plugin-lib/src/coq/constants
+-I src/coq-plugin-lib/src/coq/logicutils
+-I src/coq-plugin-lib/src/coq/logicutils/contexts
+-I src/coq-plugin-lib/src/coq/logicutils/typesandequality
+-I src/coq-plugin-lib/src/coq/logicutils/hofs
+-I src/coq-plugin-lib/src/coq/logicutils/inductive
+-I src/coq-plugin-lib/src/coq/devutils
+-I src/coq-plugin-lib/src/coq/representationutils
+-I src/representation
+-I src/representation/categories
+-I src/configuration
+-I src/compilation
+-I src/compilation/categories
 -I src/core/components/abstraction
 -I src/core/components/specialization
 -I src/core/components/inversion
@@ -14,53 +24,90 @@
 -R src Patcher
 -Q theories Patcher
 
-src/library/utilities/utilities.mli
-src/library/utilities/utilities.ml
-
-src/library/categories/category.mli
-src/library/categories/category.ml
-
-src/library/coq/coqterms.mli
-src/library/coq/coqterms.ml
-src/library/coq/printing.mli
-src/library/coq/printing.ml
-src/library/coq/hofs.mli
-src/library/coq/hofs.ml
-src/library/coq/debruijn.mli
-src/library/coq/debruijn.ml
-src/library/coq/substitution.mli
-src/library/coq/substitution.ml
-src/library/coq/filters.mli
-src/library/coq/filters.ml
-src/library/coq/reducers.mli
-src/library/coq/reducers.ml
-
-src/library/proofsearch/representation/candidates.mli
-src/library/proofsearch/representation/candidates.ml
-src/library/proofsearch/representation/assumptions.mli
-src/library/proofsearch/representation/assumptions.ml
-src/library/proofsearch/representation/merging.mli
-src/library/proofsearch/representation/merging.ml
-src/library/proofsearch/representation/proofcat.mli
-src/library/proofsearch/representation/proofcat.ml
-src/library/proofsearch/representation/proofcatterms.mli
-src/library/proofsearch/representation/proofcatterms.ml
-src/library/proofsearch/representation/cutlemma.mli
-src/library/proofsearch/representation/cutlemma.ml
-src/library/proofsearch/representation/kindofchange.mli
-src/library/proofsearch/representation/kindofchange.ml
-
-src/library/proofsearch/compilation/evaluation.mli
-src/library/proofsearch/compilation/evaluation.ml
-src/library/proofsearch/compilation/expansion.mli
-src/library/proofsearch/compilation/expansion.ml
-src/library/proofsearch/compilation/proofdiff.mli
-src/library/proofsearch/compilation/proofdiff.ml
-src/library/proofsearch/compilation/zooming.mli
-src/library/proofsearch/compilation/zooming.ml
-
-src/core/configuration/searchopts.mli
-src/core/configuration/searchopts.ml
+src/coq-plugin-lib/src/utilities/utilities.ml
+src/coq-plugin-lib/src/utilities/utilities.mli
+
+src/coq-plugin-lib/src/coq/termutils/apputils.mli
+src/coq-plugin-lib/src/coq/termutils/apputils.ml
+src/coq-plugin-lib/src/coq/termutils/funutils.mli
+src/coq-plugin-lib/src/coq/termutils/funutils.ml
+
+src/coq-plugin-lib/src/coq/representationutils/defutils.mli
+src/coq-plugin-lib/src/coq/representationutils/defutils.ml
+
+src/coq-plugin-lib/src/coq/logicutils/typesandequality/inference.mli
+src/coq-plugin-lib/src/coq/logicutils/typesandequality/inference.ml
+src/coq-plugin-lib/src/coq/logicutils/typesandequality/convertibility.mli
+src/coq-plugin-lib/src/coq/logicutils/typesandequality/convertibility.ml
+src/coq-plugin-lib/src/coq/logicutils/typesandequality/checking.mli
+src/coq-plugin-lib/src/coq/logicutils/typesandequality/checking.ml
+
+src/coq-plugin-lib/src/coq/constants/equtils.mli
+src/coq-plugin-lib/src/coq/constants/equtils.ml
+src/coq-plugin-lib/src/coq/constants/sigmautils.mli
+src/coq-plugin-lib/src/coq/constants/sigmautils.ml
+src/coq-plugin-lib/src/coq/constants/idutils.mli
+src/coq-plugin-lib/src/coq/constants/idutils.ml
+
+src/coq-plugin-lib/src/coq/logicutils/contexts/stateutils.mli
+src/coq-plugin-lib/src/coq/logicutils/contexts/stateutils.ml
+src/coq-plugin-lib/src/coq/logicutils/contexts/envutils.mli
+src/coq-plugin-lib/src/coq/logicutils/contexts/envutils.ml
+src/coq-plugin-lib/src/coq/logicutils/contexts/contextutils.mli
+src/coq-plugin-lib/src/coq/logicutils/contexts/contextutils.ml
+
+src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/hofimpls.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/hofimpls.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/debruijn.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/debruijn.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/substitution.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/substitution.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/reducers.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/reducers.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/typehofs.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/typehofs.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/zooming.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/zooming.ml
+src/coq-plugin-lib/src/coq/logicutils/hofs/filters.mli
+src/coq-plugin-lib/src/coq/logicutils/hofs/filters.ml
+
+src/coq-plugin-lib/src/coq/logicutils/inductive/indutils.mli
+src/coq-plugin-lib/src/coq/logicutils/inductive/indutils.ml
+
+src/coq-plugin-lib/src/coq/devutils/printing.mli
+src/coq-plugin-lib/src/coq/devutils/printing.ml
+
+src/representation/candidates.mli
+src/representation/candidates.ml
+src/representation/assumptions.mli
+src/representation/assumptions.ml
+src/representation/merging.mli
+src/representation/merging.ml
+src/representation/cutlemma.mli
+src/representation/cutlemma.ml
+
+src/representation/categories/category.mli
+src/representation/categories/category.ml
+src/representation/categories/proofcat.mli
+src/representation/categories/proofcat.ml
+src/representation/categories/proofcatterms.mli
+src/representation/categories/proofcatterms.ml
+
+src/compilation/evaluation.mli
+src/compilation/evaluation.ml
+src/compilation/expansion.mli
+src/compilation/expansion.ml
+src/compilation/proofdiff.mli
+src/compilation/proofdiff.ml
+src/compilation/categories/catzooming.mli
+src/compilation/categories/catzooming.ml
+
+src/configuration/kindofchange.mli
+src/configuration/kindofchange.ml
+src/configuration/searchopts.mli
+src/configuration/searchopts.ml
 
 src/core/components/specialization/specialization.mli
 src/core/components/specialization/specialization.ml
@@ -99,8 +146,6 @@ src/core/procedures/search.mli
 src/core/procedures/search.ml
 src/core/procedures/theorem.mli
 src/core/procedures/theorem.ml
-src/core/procedures/desugar.mli
-src/core/procedures/desugar.ml
 
 src/patcher.ml4
 src/patch.mlpack

plugin/build.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+git submodule init
+git submodule update
+echo "building PUMPKIN PATCH dependencies"
+cd deps/fix-to-elim/plugin
+./build.sh
+cd ../../..
+cd deps/ornamental-search/plugin
+./build.sh
+cd ../../..
+echo "done building PUMPKIN PATCH dependencies"
+echo "building PUMPKIN PATCH"
+coq_makefile -f _CoqProject -o Makefile
+make clean && make && make install

plugin/coq/Induction.v

@@ -169,7 +169,7 @@ Qed.
 (** [] *)
 
 Theorem bin_to_nat_nat_to_bin : forall n : nat,
-  bin_to_nat(nat_to_bin(n)) = n.
+  bin_to_nat (nat_to_bin n) = n.
 Proof.
   induction n as [|n'].
   - reflexivity.
@@ -547,7 +547,7 @@ Print patch_inv.
 (* Talia: Now we have an isomorphism. *)
 
 Theorem bin_to_nat_nat_to_bin : forall n : nat,
-  bin_to_nat(nat_to_bin(n)) = n.
+  bin_to_nat (nat_to_bin n) = n.
 Proof.
   induction n as [|n'].
   - reflexivity.