Tools to use Elpi in Lambdapi + type classes

[agontard]

Up-to-date version of #418, with important help from Enrico Tassi.
Draft adding tools to convert Lambdapi terms to and from Elpi, used to write a typeclass solver in Elpi, which is now called in tac_solve to help with inference.

How to use

• We found and fixed a bug in Elpi, so it is required to use the master branch of Elpi

Added syntax

• Symbol declaration modifiers: "typeclass" and "instance".
• Declaring existing symbols as tc or tc instance: typeclass s or instance s
• Note that currently, a class must have type A → TYPE for some A

Example

An example of use is in tests/OK/elpi_isa_test.lp, which mimics the construction of groups from the Isabelle Group.thy file from the HOL session. It looks a bit overcomplicated without proper syntax for record types, I did not even use inductive syntax.

TODO

When changing the syntax of Lambdapi, make sure to update the
following files:

• doc/lambdapi.bnf
• src/core/lpLexer.ml
• src/core/lpParser.ml
• src/core/pretty.ml
• src/core/print.ml
• editors/vim/syntax/lambdapi.vim
• editors/emacs/lambdapi-vars.el (syntax coloring)
• editors/emacs/lambdapi-smie.el (grammar and indentation)
• editors/vscode/lp.configuration.json (comments configuration),
• editors/vscode/syntaxes/lp.tmLanguage.json (syntax highlighting),
• misc/lambdapi.tex
• the User Manual files in the doc/ repository (do make doc to generate and check the Sphynx documentation).

[agontard]

@fblanqui are the following two files contradicting each other? Or perhaps it would be clearer if the second one explained how the file should be updated?

lambdapi/doc/README.md

Lines 58 to 60 in 1e3b2ba

	**Note:** BNF grammars are auto generated using
	[Obelisk](https://github.com/Lelio-Brun/Obelisk). They should not be edited
	directly.

lambdapi/CONTRIBUTING.md

Lines 67 to 69 in 1e3b2ba

	When changing the syntax of Lambdapi, make sure to update the
	following files:
	- `doc/lambdapi.bnf`

[fblanqui]

Fixed in 7c36a3f . The BNF grammar is not generated anymore. It is written by hand.