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

• opam install . (new dependency: 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]

Report:

• Just merged with master
• I reevaluated loading times now that lambdapi is faster: doing lambdapi check on an empty file takes 0.045s with master and 0.08s with this PR (presumably due to loading elpi). This is satisfying to me, but I believe I could try improving if necessary by using the Marshall module.
• Two errors appear in tests:
  • I'm using a function that does not exist in OCaml 4.14.4, which I shall fix in the next commit.
  • It seems that dune build / tests are different in Ocaml 5.5.0, where the test directory is not at the same place, and therefore my ad hoc way of locating files I need fails. I don't know yet of a better solution to avoid this kind of problems happening.