Skip to content
Embeddable Lambda Prolog Interpreter
Branch: master
Clone or download
Latest commit 76a56d8 Apr 18, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
src loc: add compare function Apr 18, 2019
tests Enable multi-arg and deep indexing using unification hashes Apr 18, 2019
utils shorten: refine semantics by letting one chose the short name Apr 10, 2019
.gitattributes builtins: no need to load a file, Setup.init does it Apr 12, 2018
.gitignore [merlin] add PKG for trace_ppx Jun 11, 2018
.travis.yml fix opam package Apr 18, 2019 Update Aug 3, 2017 Update Apr 18, 2019
LICENSE final reorganization Jul 12, 2015
META Str -> Re_str (pure ocaml implementation of Str) Apr 20, 2018
builtin.elpi Enable multi-arg and deep indexing using unification hashes Apr 18, 2019
elpi-checker.elpi checker: do not warn for undeclared symbols in .aux. namespace Apr 1, 2019
elpi_REPL_config.mli elpi_config -> elpi_REPL_config Apr 18, 2019
elpi_quoted_syntax.elpi Custom -> Builtin Apr 4, 2018

Build Status

ELPI - Embeddable λProlog Interpreter

ELPI implements a variant of λProlog enriched with Constraint Handling Rules, a programming language well suited to manipulate syntax trees with binders.

ELPI is a research project aimed at providing a programming platform for the so called elaborator component of an interactive theorem prover.

ELPI is designed to be embedded into larger applications written in OCaml as an extension language. It comes with an API to drive the interpreter and with an FFI for defining built-in predicates and data types, as well as quotations and similar goodies that come in handy to adapt the language to the host application.

ELPI is free software released under LGPL vesion 2.1 or above.

How to install ELPI

ELPI is developed under Linux and is known to also work on MacOSX. The simplest way is to use OPAM and type

opam install elpi

This command gives you the command line tool elpi as well as the findlib -package elpi switch.

To install the development version of elpi directly from github you can type

opam pin add elpi

You can also clone this repository and type make. The build requirements are listed at the end of the Makefile

Syntax highlight in vim

We recommend to add the following lines to ~/.vimrc

autocmd BufRead,BufNewFile *.elpi set filetype=lprolog

autocmd FileType lprolog syn match   lprologIdentifier  "\<\l[-a-zA-Z\.+*/\\^<>=`'~?@#$&!_]*\>"
autocmd FileType lprolog syn region  lprologClause start="^\<\l[-a-zA-Z\.+*/\\^<>=`'~?@#$&!_]*\>" end=" \|:-\|\."
autocmd FileType lprolog syn match lprologClauseSymbols ":-"
autocmd FileType lprolog syn match lprologClauseSymbols "\."
autocmd FileType lprolog hi def link lprologClauseSymbols Type

autocmd FileType lprolog syn keyword elpiKeyword mode macro type pred namespace rule constraint uvar shorten
autocmd FileType lprolog syn match elpiKeyword ":before"
autocmd FileType lprolog syn match elpiKeyword ":after"
autocmd FileType lprolog syn match elpiKeyword ":name"
autocmd FileType lprolog syn match elpiMacro "@\(\w\|-\)\+"
autocmd FileType lprolog syn match elpiSpill "{"
autocmd FileType lprolog syn match elpiSpill "}"
autocmd FileType lprolog syn region elpiQuotation start="{{" end="}}" contains=@elpiAntiQuotation
autocmd FileType lprolog hi def link elpiKeyword Keyword
autocmd FileType lprolog hi def link elpiMacro Special
autocmd FileType lprolog hi def link elpiSpill Special

Syntax highlight in $EDITOR

We are happy to merge PRs! (Really, we use vim but we are happy to support any other editor).

What's an elaborator and what's so special about it?

The elaborator of an interactive prover is the component in charge of turning a term as input by the user into a well typed one. In a prover like Coq it performs type inference and is typically extended by the user.

The elaborator manipulates terms with binders and holes (unification variables) representing missing piece of information. Some of them have to be filled in in order to make the term well typed. Some other are are filled in because the user has programmed the eleborator to do so, e.g. ad-hoc polymorphism.

Such software component is characterized by an high complexity coming from the interplay of binders, reduction and unification, the heuristics to make it work in practice and the user extensions to customize its behavior.

What problem does ELPI (try to) solve and how?

The programming language has the following features

  • Native support for variable binding and substitution, via an Higher Order Abstract Syntax (HOAS) embedding of the object language. The programmer needs not to care about De Bruijn indexes.
  • Native support for hypothetical context. When moving under a binder one can attach to the bound variable extra information that is collected when the variable gets out of scope. For example when writing a type-checker the programmer needs not to care about managing the typing context.
  • Native support for higher order unification variables, again via HOAS. Unification variables of the meta-language (λProlog) can be reused to represent the unification variables of the object language. The programmer does not need to care about the unification-variable assignment map and cannot assign to a unification variable a term containing variables out of scope, or build a circular assignment.
  • Native support for syntactic constraints and their meta-level handling rules. The generative semantics of Prolog can be disabled by turning a goal into a syntactic constraint (suspended goal). A syntactic constraint is resumed as soon as relevant variables gets assigned. Syntactic constraints can be manipulated by constraint handling rules (CHR).
  • Native support for backtracking. To ease implementation of search.
  • The constraint store is extensible. The host application can declare non-syntactic constraints and use custom constraint solvers to check their consistency.
  • Clauses are graftable. The user is free to extend an existing program by inserting/removing clauses, both at runtime (using implication) and at "compilation" time by accumulating files.

Most of these feature come with λProlog. Constraints and propagation rules are novel in ELPI.


The language is quite compatible with standard λProlog and ELPI is known to be able to run most of the λProlog programs out there (see the list of known incompatibilities with the Teyjus system). Reading Programming with Higher-Order Logic by Miller and Nadathur is highly recommended and covers standard λProlog.

The extensions to λProlog implemented in ELPI are described in the ELPI file, built-in predicates are documented in builtin.

There is a short paper describing the implementation of the interpreter, in particular how it deals with binder mobility.

A longer paper describes, among other things, the part of the language for declaring and manipulating constraints.

For a lightweight introduction to Elpi one can look at the slides of the talk given at the ML Family workshop 2018 titled "Elpi: an extension language with binders and unification variables". The companion code of toyml that implements W (ML type inference) in Elpi is also available.

How to embed ELPI in your software

The easiest way of embedding ELPI is by linking it using findlib as in ocamlfind opt -package elpi -o myprogram. The API the host application can use to drive ELPI is documented in the elpi_API.mli file. The file contains example of (basic) built-in predicates declaration via ELPI's FFI.

The command line interface to ELPI is a very simple example of a client using ELPI as a library. More complex examples of embeddings of ELPI are coq-elpi and matita-elpi.

You can’t perform that action at this time.