Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update apps/tc/README.md #568

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
+140 −118
Draft

Update apps/tc/README.md #568

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
77f39e0
Update README.md
gares Jan 4, 2024
4bf7454
more cleanup
gares Jan 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
236 changes: 125 additions & 111 deletions apps/tc/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
# Type class solver

This folder contains an alternative implementation of a type class solver for
coq written in elpi. This solver is composed by two main parts, the **compiler**
and the **solver**. The former takes coq classes and instances and "translates"
them into the elpi representation, whereas the latter is the elpi tactic aiming
to make instance search on coq goals.
The TC app is an alternative implementation of a type class solver for
Coq written in elpi. This solver is composed by two main parts, the **compiler**
and the **solver**. The former takes Coq classes and instances and "translates"
them into the elpi rules, whereas the latter is the elpi tactic performing instance
search on Coq goals.

- [The compiler](#the-compiler)
- [Class compilation](#class-compilation)
- [Deterministic search](#deterministic-search)
- [Hint modes](#hint-modes)
- [Modes](#modes)
- [Instance compilation](#instance-compilation)
- [Instance priorities](#instance-priorities)
- [Technical details](#technical-details)
Expand All @@ -22,55 +22,56 @@ to make instance search on coq goals.

## The compiler

In our implementation by compiler we mean the set of rules abstracting coq
terms, *1.* classes and *2* instances, in the elpi world. In the next two
paragraphs, we briefly explain these two phases of the compilation, where,
intuitively, a type class can be seen as a prolog predicate and the instances of
a type class $C$ as rule (clause or fact) of the elpi predicate for $C$.

For instance, if
The compiler translates Coq type classes and Coq type class instances to the elpi
rules. A type class is represented as a predicate and its instances as rules
(with or without premises) for that predicate.

For instance the Coq class `eqb` (for correct equality tests) and its
instance `eqBool` (for the `bool` data type):
```coq
Class Eqb (T: Type) := {
eqb : T -> T -> bool;
eq_leibniz : forall (A B: T), eqb A B = true -> A = B
Class eqb (T: Type) := {
test : T -> T -> bool;
test_correct : forall (a b: T), test a b = true -> a = b
}.
```

is the type class representing the leibniz equality between two objects of type
$T$, and

```coq
Program Instance eqBool : Eqb bool := {
eqb A B := if A then B else negb B
Program Instance eqBool : eqb bool := {
eqb a b := if a then b else negb b
}.
Next Obligation. now intros [] []. Qed.
```
are represented as follows:

is an implementation of `Eqb` for the type `bool`, their corresponding elpi
representation will be:

```prolog
pred tc-Eqb i:term, o:term.
tc-Eqb {{bool}} {{eqBool}}.
```prolog
pred tc-eqb i:term, o:term.
tc-eqb {{ bool }} {{ eqBool }}.
```

### Class compilation

The compilation of a type class creates dynamically (thanks to the
`coq.elpi.add-predicate` API) a new predicate called `tc-Path.tc-ClassName` with
$N + 1$ terms where:
The compilation of a type class creates new predicate called
```
pred tc-Path.tc-ClassName m_1 : term, ..., m_n : term.
```

where:
- `Path` is the is the logical path in which the type class `ClassName` is
located
- $N$ is the number of parameter of the `ClassName`. In particular, if a type
class $C$ as the parameters $P_1,\dots, P_n$ then the corresponding predicate
will have $N$ parameters of type `term` ($1$ per parameter) and a last
located, for example `tc-Coq.Classes.EquivDec.tc-EqDec`
- $n$ is the number of parameter of the `ClassName`. In particular, if a type
class $C$ as the parameters $P_1,\dots, P_m$ then the corresponding predicate
will have $m = n-1$ parameters of type `term` ($1$ per parameter) and a last
parameter in output mode containing the result of the instance search.
By default, all the first $P_1,\dots,P_n$ parameters are in output mode.
By default, all the first $P_1,\dots,P_m$ parameters are in output mode.
For example
```coq
EqDec : forall (A : Type) (R : Relation_Definitions.relation A), equivalence R -> Type
```
has 3 parameters, hence `tc-Coq.Classes.EquivDec.tc-EqDec` will have four.

The set of rules allowing to add new type-class predicates in elpi are grouped
in [create_tc_predicate.elpi](elpi/create_tc_predicate.elpi).
In order to specify the modes $m_i$ of the class parameters, one has to use
the `TC.Declare` command with the `#[mode(...)]` attribute
(see the [modes](README.md#modes) section below).

The source code for class compilation is in the file
[create_tc_predicate.elpi](elpi/create_tc_predicate.elpi).

#### Deterministic search

Expand All @@ -85,32 +86,39 @@ In the example below, we want the `NoBacktrack` type class not to backtrack if
a solution is found.

```coq
#[deterministic] TC.declare Class NoBacktrack (n: nat).
#[deterministic] TC.Declare Class NoBacktrack (n: nat).
TC.Declare Class A (n: nat).
TC.Declare Class B.

Instance nb0 : NoBacktrack 0. Proof. split. Qed.
Instance nb1 : NoBacktrack 1. Proof. split. Qed.
(* Note: that nb1 has precedence over nb0 *)

Class A (n: nat).
Instance a0 : A 0. Proof. split. Qed.
Instance b0 n : NoBacktrack n -> A n -> B. Proof. split. Qed.

Instance a0 : A 0. Qed.
Instance nb0 : NoBacktrack 0. Qed.
Instance nb1 : NoBacktrack 1. Qed.
Instance a3 n : NoBacktrack n -> A n -> A 3. Qed.
TC.AddAllInstances.

Goal A 3. Fail apply _. Abort.
Goal B.
Fail apply _.
```

The goal `A 3` fails since the only instance matching it is `a3`, but we are not
able to satisfy both its premises. In particular, the instance `nb1` is applied
first, which fixes the parameter `n` of `a3` to `1`. Then the algorithm tries to
find a solution for `A 1` (the second premise), but no implementation of `A` can
solve it. In the classic approach, the type class solver would backtrack on the
premise `NoBacktrack n` and try to apply `nb0` (this would find a solution), but
since the type class `NoBacktrack` is deterministic, then `nb0` is discarded.
The goal `B` fails since its only instance `b0` fails to apply.
In particular, the instance `nb1` is applied first, which fixes the parameter
`n` of `b0` to `1`. Then the algorithm tries to
find a solution for `A 1` (the second premise of `b0`), but no instance for
`A` can solve it.
In the classic approach, the type class solver would backtrack on the
premise `NoBacktrack n` and try to apply `nb0` and then `a0`, but
since the type class `NoBacktrack` is deterministic, when once of its
instances is applied all the alternative ones are discarded.

In this implementation, the elpi rule for the instance `a3` is:
The elpi rule for the instance `b0` is:

```elpi
tc-A {{3}} {{a3 lp:A lp:B lp:C}} :-
do-once (tc-NoBacktrack A B),
tc-A A C.
```
tc-B {{ b0 lp:A lp:B lp:C }} :-
do-once (tc-NoBacktrack A B),
tc-A A C.
```

The predicate `do-once i:prop` has
Expand All @@ -119,25 +127,23 @@ The predicate `do-once i:prop` has
do-once P :- P, !.
```

as implementation. The cut (`!`) operator is in charge to avoid backtracking on
the query `tc-NoBacktrack A B`

#### Hint modes

Instance search is done looking to the arguments passed to the class. If there
is an instance $I$ unifying to it, the premises of $I$ are tried to be solved to
commit $I$ as the solution of the current goal (modulo backtracking). Concerning
the parameters of a type class, coq type class solver allows to constrain the
argument to be ground, in input or output modes (see
[here](https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Mode)).
We provide a similar behavior in elpi: classes represent elpi predicates where
the parameters can be in input `i` or output `o` mode (see
[here](https://github.com/LPCIC/elpi/blob/master/ELPI.md#modes)). We translate
coq modes in the following way: `+` and `!` become `i` in elpi and `-` becomes
`o` (see
[here](https://github.com/FissoreD/coq-elpi/blob/c3cce183c3b2727ef82178454f0c583196ee2c21/apps/tc/elpi/create_tc_predicate.elpi#L12)).

In elpi we allow type classes to have at most one mode, if that mode is not
as implementation. The cut (`!`) operator is in charge of discarding all
alternative solutions to `P` (in this case `tc-NoBacktrack A B`).

#### Modes

Coq's type class solver honors [Hint Modes](https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Mode).
We provide a similar mechanism based on [elpi's notion of mode](https://github.com/LPCIC/elpi/blob/master/ELPI.md#modes).

Each type class argument can be in input `i` or output `o` mode. A goal argument
in input mode is matched against the corresponding rule the pattern. Otherwise
said, if the goal contains a hole (an evar) where the elpi rules expects a
constant, matching fails. Conversely, arguments in output mode are unified.
Intuitively input arguments are expected to be present in the goal and are
matched (consumed) by the rules. If such input data is not available, rules
don't apply.

We allow type classes to have at most one mode, if that mode is not
defined, all parameters are considered in `o` mode. The command to be used
to let elpi compile classes with modes is done via the command `TC.Declare`.

Expand All @@ -147,92 +153,97 @@ to let elpi compile classes with modes is done via the command `TC.Declare`.

The pragma `mode` is taken into account to make `T1` and `N` in input mode and
`T2` in output mode. The command `TC.Declare` both create the class in elpi and
in coq. Note that the accepted list arguments for the attribute `mode` are
in Coq. Note that the accepted list arguments for the attribute `mode` are
`i, o, +, -` and `!` with their respective meaning.

For classes declared in Coq, we translate
Coq modes in the following way: `+` and `!` become `i` in elpi and `-` becomes
`o` (see [the source code](https://github.com/FissoreD/coq-elpi/blob/c3cce183c3b2727ef82178454f0c583196ee2c21/apps/tc/elpi/create_tc_predicate.elpi#L12)).

### Instance compilation

Instances are compiled in elpi from their type. In particular, since the
$\forall$-quantification and the left hand side of implications of coq are both
represented with the `prod` type in elpi, we can say that the type of an
instance $I$ is essentially a tower of

<pre>
```
prod N_1 T_1 (x_1\
prod N_2 T_2 (x_2\
...
prod N_n T_n (x_n\
app [global GR, A_1, A_2, ... A_M])))
</pre>
```

where $\forall i \in [1, N],\ T_i$ is the type of the quantified variable $x_i$.
Each $x_1$ represents a premise $P$ of the current instance and, if its type
$T_i$ is a type class, then $P$ is recursively compiled and added to the final
clause as a premise. The last `prod` contains `app [global GR, A_1, ..., A_M]`
clause as a premise. The conclusion is `app [global GR, A_1, ..., A_M]`
where `GR` is the gref of the type class implemented by $I$ and each $A_j$ is an
argument applied to `GR` which sees every $x_i$. Note that during the
compilation of the instance the binders $x_i$ are recursively replaced by fresh
`pi` elpi variables.

For example, the instance `eqBool` showed before, has type

`Eqb bool`, it has no quantified variable and it is directly compiled in the
clause `tc-Eqb {{bool}} {{eqBool}}`.
`eqb bool`, it has no quantified variable and it is directly compiled in the
clause `tc-eqb {{ bool }} {{ eqBool }}`.

On the other hand, if we take the instance below,

```coq
Instance eqProd (A B: Type) : Eqb A -> Eqb B -> Eqb (A * B) := { ... }
Instance eqProd (A B: Type) : eqb A -> eqb B -> eqb (A * B) := { ... }
```

we see that its type is

```
prod `A` (sort (typ eqProd.u0»)) c0 \
prod `B` (sort (typ eqProd.u1»)) c1 \
prod `H0` (app [global (indt «Eqb»), c0]) c2 \
prod `H1` (app [global (indt «Eqb»), c1]) c3 \
app [global (indt «Eqb»), app [global (indt «prod»), c0, c1]]
prod `H0` (app [global (indt «eqb»), c0]) c2 \
prod `H1` (app [global (indt «eqb»), c1]) c3 \
app [global (indt «eqb»), app [global (indt «prod»), c0, c1]]
```

there are in fact four variables that produce the elpi clause:
there are in fact four variables that produce the elpi rule:

```
pi x0 x1 x2 x3\
tc-Eqb {{prod lp:A lp:B}} Sol :-
tc-Eqb A S1, tc-Eqb B S2,
Sol = {{eqProd lp:A lp:B lp:S1 lp:S2}}.
```prolog
% pi A B S1 S2\ % these quantifications are implicit in elpi's concrete syntax
tc-eqb {{ prod lp:A lp:B }} Sol :-
tc-eqb A S1, tc-Eqb B S2, % recursive calls H1 and H2
Sol = {{ eqProd lp:A lp:B lp:S1 lp:S2 }}.
```

the four variable $c_0,...,c_3$ are quantified with `pi`, the two premises
`H0` and `H1` are compiled as premises of the current goal (we need to find a
proof that there exists an implementation of the class `Eqb` for the types
of $c_0$ and $c_1$). Then the application of `«Eqb»` is used to create the head of
proof that there exists an implementation of the class `eqb` for the types
of $c_0$ and $c_1$). Then the application of `«eqb»` is used to create the head of
the clause with its arguments and `eqProd`, the gref of the current instance,
is used as the solution of the current goal applied to all of the quantified
variables.

The set of rules allowing to compile instances in elpi are grouped in
[compiler.elpi](elpi/compiler.elpi).

****

#### Instance priorities

To reproduce coq behavior, instances need to respect a notion of priority:
sometime multiple instances can be applied on a goal, but, for sake of
performances, the order in which they are tried is essential.
Priority among rules is represented by their textual order.

In the previous example, the goal `Eqb ?V` where `?V` is a meta-variable, it
is important to first use the rules `eqBool` and then `eqProd`, the latter
causing an infinite loop.
```prolog
pred tc-c i:term, o:term.
tc-c ... :- ... % this rule is tried before
tc-c ... :- ... % this other rule
```

In elpi, we have the possibility to create rules with names and, then, new rules
can be added with respect to a particular grafting (see
[here](https://github.com/FissoreD/coq-elpi/blob/a11558758de0a1283bd9224b618cc75e40f118fb/coq-builtin.elpi#L1679)).
can be grafted before/after existing (named) rules (see
[grafting](https://github.com/FissoreD/coq-elpi/blob/a11558758de0a1283bd9224b618cc75e40f118fb/coq-builtin.elpi#L1679)).

Our strategy of instance insertion in the elpi database reposes on a predicate
`pred hook o:string` having, by default, $1.001$ implementations each of them
having a name going from `"0"` to `"1000"` (bounds included). Roughly what we
have is the following:
`pred hook o:string` going from `"0"` to `"1000"` (bounds included).
Roughly the scaffolding for grafting rules looks like:

```prolog
:name "0" hook "0".
Expand All @@ -242,8 +253,11 @@ have is the following:
:name "1000" hook "1000".
```

In this way an instance can be added at the wanting position to respect its
priority. In particular, the priority of an instance can be defined in two
In this way an instance can be added at the wanted position to respect its
priority. These anchor points have names corresponding to Coq's numbered
priorities, to ease porting existing code.

The priority of an instance can be defined in two
different ways by the user by coq and we retrieve this piece of
information via the `Event` listener from `coq` (see
[here](https://github.com/coq/coq/blob/f022d5d194cb42c2321ea91cecbcce703a9bcad3/vernac/classes.mli#L81)).
Expand All @@ -255,7 +269,7 @@ get its priority (see

1. If the instance has no user defined priority, the attribute containing the
priority of the instance is set to `None`. In this case, the priority is
computed as the number of premises the instance has. For example, `eqBool`
computed as the number of premises the instance has. For example, `eqProd`
has priority $2$, since it has two hypothesis triggering recursive instance
search.
2. If $P$ is the priority of both the instance $I_1$ and the instance $I_2$ of
Expand Down Expand Up @@ -473,7 +487,7 @@ A small recap of the available elpi commands:
<code>TC.Declare ClassDef</code> (click to expand)
</summary>

See [here](#deterministic-search) and [here](#hint-modes) for respectively
See [here](#deterministic-search) and [here](#modes) for respectively
deterministic type class and mode declaration

</details>
Expand Down
1 change: 1 addition & 0 deletions apps/tc/_CoqProject.test
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,5 +50,6 @@ tests/test.v
tests/indt_to_inst.v

tests/bigTest.v
tests/test_tc.v

examples/tutorial.v
Loading
Loading