The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunck of standard library.
The plugin currently works on a branch of coq (hopefully, in the future, it will also work on a stable official release). The easy (and long) way to test the plugin is to follow the following steps:
Create a fresh directory and move into it:
mkdir testplugin && cd testplugin
Retrieve my branch of coq and compile it (and go take a coffee, or may be 5 coffees):
git clone https://github.com/mlasson/coq.git cd coq ./configure -local make -j 4 cd ..
Retrieve the plugin and compile it:
git clone https://github.com/mlasson/paramcoq.git cd paramcoq make
To test the plugin:
cd test-suite make ide
It will compile Parametricity.vo which loads the plugin and contains a translation of the initial modules. Then, it launches coq-ide with some simple examples.
The default arity is 2. The default name is automatically generated when translating a constant (otherwise you need to provide it).
- Parametricity term [as name] [arity n].
Define a new constant named name obtained by computing the parametricity translation of term.
- Parametricity Inductive inductive [as name] [arity n].
Declare a new inductive type named name from the translation of inductive.
- Parametricity Module modulepath.
Recursively translate everything in a module.
- Realizer constant or variable [as name] [arity n] := term.
Declare term to be the translation of a constant. Useful to translate terms containing section variables, or axioms.
Note that all that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import ProofIrrelevence).
- [Global | Local] Parametricity Tactict := t.
Use the tactic t to solve proof obligations generated by the Parametricity command.