Tools to use Elpi in Lambdapi + type classes

.gitignore

@@ -21,3 +21,4 @@ libraries/zenon_modulo
 .DS_Store
 *.map
 *.log
+_opam

CHANGES.md

@@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Added
 
 - Decimal numbers can now be qualified by a module path so that one can use the decimal notation with different types in the same file.
+- Support for typeclasses using Elpi
+  * Added syntax: two new symbol modifiers `typeclass` and `instance` and individual commands `typeclass/instance qid` to declare a previously defined symbol as a typeclass or instance.
+  * typeclass instance search is used in tactics, symbol definitions, and the `type` query, upon encountering any unsolvable hole (wildcard or implicit argument)
 
 ### Changed
 

doc/about.rst

@@ -34,6 +34,7 @@ Here are some of the features of Lambdapi:
 - support for unicode (UTF-8) and user-defined infix operators
 - symbols can be declared commutative, or associative and commutative
 - some arguments can be declared as implicit: the system will try to find out their value automatically
+- a typeclass solver, written in Elpi, allows to add rules to help the system infer implicit arguments
 - symbol and rule declarations are separated so that one can easily define inductive-recursive types or turn a proved equation into a rewriting rule
 - support for interactive resolution of typing goals, and unification goals as well, using tactics
 - a rewrite tactic similar to the one of SSReflect in Coq

doc/commands.rst

@@ -159,6 +159,18 @@ Finaly, here is an example of strictly-positive inductive type:
    assert p a b c x ⊢ ind_𝕆 p a b c (s x) ≡ b x (ind_𝕆 p a b c x);
    assert p a b c x y ⊢ ind_𝕆 p a b c (l x) ≡ c x (λ y, ind_𝕆 p a b c (x y));
 
+.. _instance:
+
+``instance``
+---------------
+
+The command ``instance`` allows to declare as typeclass instance (see **Typeclass modifiers**) a previously defined symbol.
+
+::
+
+   symbol bool_zero : zero_class bool ≔ is_zero true; // true is neutral for or/xor
+   instance bool_zero;
+
 .. _notation:
 
 ``notation``
@@ -479,6 +491,12 @@ the system with additional information on its properties and behavior.
     canonical term headed by ``f`` is of the form ``f t₁ (f t₂ (f t₃ …
     tₙ) … )``. Moreover, in both cases, we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``.
 
+- **Typeclass modifiers** (adding rules to the typeclass solver)
+
+  - ``instance``: if the conclusion of the type of the symbol is a typeclass,
+    adds a rule to automatically use the symbol to obtain an object of that type.
+  - ``typeclass``: allows to declare instances of that symbol (must be of type ``T → TYPE`` for some type ``T``)
+
 - **Exposition modifiers** define how a symbol can be used outside the
   module where it is defined. By default, the symbol can be used
   without restriction.
@@ -541,6 +559,18 @@ arguments must be explicitly given.
 **Notations**: Some notation can be declared for a symbol using the
 commands :ref:`notation` and :ref:`builtin`.
 
+.. _typeclass:
+
+``typeclass``
+---------------
+
+The command ``typeclass`` allows to declare as typeclass (see **Typeclass modifiers**) a previously defined symbol.
+
+::
+
+   symbol nonempty : U → TYPE;
+   typeclass nonempty; //One can now declare instances of [nonempty x] for any [x]
+
 .. _unif_rule:
 
 ``unif_rule``