Awesome

lngen

Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott

Overview

LNgen generates statements and proofs of "infrastructure" lemmas for locally nameless representations in the [Coq proof assistant] 1. It takes as input language definitions written in the [Ott specification language] 2. LNgen is not a complete replacement for Ott's Coq back end: the output from LNgen relies on the definitions generated by Ott.

Dependencies

GHC is required in order to compile LNgen.

Recently tested with GHC 8.10.7
LNgen's output must be combined with the output of Ott.

Obtain Ott from https://github.com/sweirich/ott

(Fork of ott.0.31)
The Coq Proof assistant.

This version works with Coq 8.15.0
LNgen's output requires a copy of Penn's metatheory library. The most recent version of the library can be found at

https://github.com/plclub/metalib/

Last tested with the 8.15.0 version of metalib.

Building LNgen

You can use either the Haskell tools cabal or stack to build lngen.

To compile and run with cabal (new style, uses system GHC)

  cabal new-build
  cabal new-exec lngen  <command line flags, see below>

To compile and run with stack (GHC version determined by stack.yaml)

  stack build
  stack exec lngen <command line flags, see below>

To compile with cabal (old style, installs lngen in your path):

  cabal v1-build
  lngen

Using LNgen

Write an Ott specification for your language, e.g., lang.ott, keeping in mind the restrictions below.
Run ott on the specification to produce a Coq file containing the language's definitions, e.g.,
```
 ott --coq lang_ott.v lang.ott
```
Run lngen on the specification to produce a Coq file containing additional infrastructure for the language, e.g.,
```
 lngen --coq lang_inf.v lang.ott
```

Options

The following options to lngen may be useful:

--coq-admitted : Tells LNgen to emit every infrastructure lemma as an axiom. This is useful if you're still tweaking your language's definition and do not wish to spend time recompiling the infrastructure file.
--coq-loadpath dir : Tells LNgen to include a line
```
  Add LoadPath "dir".
```
at the beginning of the file that it generates. For example, this option can be used to specify the directory containing the metatheory library.
--coq-no-proofs : Same as --coq-admitted.
--coq-ott lib : Tells LNgen to include a line
```
  Require Import lib.
```
at the beginning of the file that it generates. For example, this option can be used to Require the library generated by Ott. (In fact, LNgen's output won't compile without it.)

Restrictions on Ott specifications

LNgen handles no more than what Ott's locally nameless back-end can handle. In particular, LNgen doesn't handle multi-substitutions and list forms.
Every metavar that is used as a binder must include
```
  {{ repr-locally-nameless }}
```
as a homomorphism.
LNgen reads only the initial part of a single Ott file. This initial part should be ordered as follows:
```
* `metavar` declarations
* a `grammar` block
* a `substitutions` block
* a `freevars` block
```
Anything after this initial part will be ignored by LNgen but still processed by Ott. Note that you may declare indexvars and embeds between the parts listed above.

The initial grammar block should include only those grammars for which you expect Ott to generate an inductive datatype declaration. The initial substitutions and freevars blocks must declare names for all possible (sensible) substitution and free-variables functions.

Examples

The examples directory contains examples of Ott specifications and the corresponding outputs generated by Ott and LNgen. Each example uses LoadPath directives and symlinks to import copy the metatheory library that comes with the LNgen distribution. The README file in the examples directory contains additional information about each example.

To compile the Coq code for all the examples, run make examples.

Credit

Original code by Brian Aydemir