Rocq-Elpi

Rocq plugin embedding Elpi.

Elpi provides an easy-to-embed implementation of a dialect of λProlog, a programming language well suited to manipulate abstract syntax trees containing binders and unification variables.

Rocq-Elpi provides a Rocq plugin that lets one define new commands and tactics in Elpi. For that purpose it provides an embedding of Rocq's terms into λProlog using the Higher-Order Abstract Syntax approach (HOAS).

Rocq-Elpi also exports to Elpi a comprehensive set of Rocq's primitives, so that one can print a message, access the environment of theorems and data types, define a new constant, declare implicit arguments, type classes instances, and so on. For convenience it also provides quotations and anti-quotations for Rocq's syntax, so that one can write {{ nat -> lp:X }} in the middle of an Elpi program instead of the equivalent AST.

Finally Rocq-Elpi provides an FFI to bind OCaml libraries. For example apps/json provides access to external data in json format via the Yojson library, and apps/xml does the same for xml-light.

What is the purpose of all that

In the short term, provide an extension language for Rocq well suited to manipulate terms containing binders. One can already use Elpi to implement commands and tactics.

As ongoing research we are looking forward to express algorithms like higher order unification and type inference, and to provide an alternative elaborator for Rocq.

Installation

The simplest way is to use OPAM and type

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install rocq-elpi
opam install rocq-elpi-json # example of optional plugin

Editor Setup

The recommended user interface is VSRocq. We provide an extension for vscode in the market place, just look for Elpi. The extension provides syntax hilighting for both languages even when they are nested via quotations and antiquotations.

Other editors (click to expand)

At the time of writing Proof General does not handle quotations correctly, see ProofGeneral/PG#437. In particular Elpi Accumulate lp:{{ .... }}. is used in tutorials to mix Rocq and Elpi code without escaping. Rocq-Elpi also accepts Elpi Accumulate " .... ". but strings part of the Elpi code needs to be escaped. Finally, for non-tutorial material, one can always put the code in an external file declared with From some.load.path Extra Dependency "filename" as f. and use Elpi Accumulate File f..

RocqIDE does handle quotations. The installation process puts coq-elpi.lang in a place where RocqIDE can find it. Then you can select coq-elpi from the menu Edit -> Preferences -> Colors.

For Vim users, Coqtail provides syntax highlighting and handles quotations.

Development version (click to expand)

To install the development version one can type

opam pin add rocq-elpi https://github.com/LPCIC/coq-elpi.git

One can also clone this repository and type make, but check you have all the dependencies installed first (see rocq-elpi.opam).

We recommend to look at the CI setup for ocaml versions being tested. Also, we recommend to install dot-merlin-reader and ocaml-lsp-server (version 1.15).

Documentation

The reference manual includes tutorials. For a not so short demo, you can look the Elpi: rule-based meta-language for Rocq video recording of the keynote at RocqPL25 (slides & demo files).

The reference manual of the Elpi language is a separate document.

Supported features of Gallina (core calculus of Rocq)

(click to expand)

• functional core (fun, forall, match, application, let-in, sorts)
• evars (unification variables)
• Inductive types (including mutual)
• CoInductive types (including mutual)
• fixpoints (including mutual)
• cofixpoints (including mutual)
• primitive records
• primitive projections
• primitive integers
• primitive floats
• primitive strings
• primitive arrays (of primitive values)
• universe polymorphism
• modules
• module types
• functor application
• functor definition

Supported features of Gallina's extensions (extra logical features, APIs)

(click to expand)

Checked boxes are available, unchecked boxes are planned, missing items are not planned. This is a high level list, for the details see coq-builtin.

• i/o: messages, warnings, errors, Rocq version
• logical environment: read, write, locate
  • dependencies between objects
• type classes database: read, write
  • take over resolution
• canonical structures database: read, write
  • take over resolution
• coercions database: read, write
• sections: open, close
• scope management: import, export
• hints: mode, opaque, resolve, strategy
• arguments: implicit, name, scope, simpl
• abbreviations: read, write, locate
• typing and elaboration
• unification
• reduction: lazy, cbv, vm, native
  • flags for lazy and cbv
• ltac1: bridge to call ltac1 code, mono and multi-goal tactics
• option system: get, set, add
• pretty printer: boxes, printing width
• attributes: read

Relevant files

• coq-builtin documents the HOAS encoding of Rocq terms and the API to access Rocq
• coq-builtin-synterp documents APIs to interact with Rocq at parsing time
• elpi-buitin documents Elpi's standard library, you may look here for list processing code
• coq-lib provides some utilities to manipulate Rocq terms; it is an addendum to coq-builtin
• elpi-command-template provides the pre-loaded code for Elpi Command (execution phase) and Elpi Tactic
• elpi-command-template-synterp provides the pre-loaded code for Elpi Command (parsing phase)
• elpi-tactic-template provides the pre-loaded code for Elpi Tactic (note tactics also load elpi-command-template)

Organization of the repository

The code of the Rocq plugin is at the root of the repository in the src, elpi and theories directories.

The apps directory contains client applications written in Rocq-Elpi.

License

Rocq-Elpi is free software under the LGPL v2.1 license or any later version.