<commit_before>[![Build Status](https://travis-ci.org/LPCIC/elpi.svg?branch=master)](https://travis-ci.org/LPCIC/elpi)
# 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](http://opam.ocaml.org/) 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 https://github.com/LPCIC/elpi.git
```
You can also clone this repository and type `make`.  The build requirements
are listed at the end of the [Makefile](Makefile)

#### Syntax highlight in vim

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

```vim
"elpi
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 <commit_msg>Update README mentioning vscode<commit_after>[![Build Status](https://travis-ci.org/LPCIC/elpi.svg?branch=master)](https://travis-ci.org/LPCIC/elpi)
# 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](http://opam.ocaml.org/) 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 https://github.com/LPCIC/elpi.git
```
You can also clone this repository and type `make`.  The build requirements
are listed at the end of the [Makefile](Makefile)

#### Syntax highlight in Visual studio code

The [extension for vscode](https://github.com/LPCIC/elpi-lang) is available in the
market place, just look for Elpi.

#### Syntax highlight in vim

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

```vim
"elpi
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
```

## 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 
{'fraction_non_alphanumeric': 0.08041848844472205, 'fraction_numerical': 0.0006246096189881324, 'mean_word_length': 4.796380090497737, 'pattern_counts': {'":': 8, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 7, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5335025', 'n_tokens_mistral': 1969, 'n_tokens_neox': 1930, 'n_words': 860}