Is it possible to declare a bidirectional Elpi predicate that computes a Coq term of type `N`

from a given Elpi `int`

and vice versa? Currently, I have an implementation that works only for the first case:

```
pred positive-constant o:int, o:term.
positive-constant N _ :- N < 1, !, fail.
positive-constant 1 {{ lib:num.pos.xH }} :- !.
positive-constant N {{ lib:num.pos.xO lp:T }} :-
0 is N mod 2, !, positive-constant {calc (N div 2)} T.
positive-constant N {{ lib:num.pos.xI lp:T }} :-
1 is N mod 2, !, positive-constant {calc (N div 2)} T.
pred n-constant o:int, o:term.
n-constant N _ :- N < 0, !, fail.
n-constant 0 {{ lib:num.N.N0 }} :- !.
n-constant N {{ lib:num.N.Npos lp:T }} :- !, positive-constant {calc N} T.
```

```
From elpi Require Import elpi.
From Coq Require Import ssreflect ZArith.
Elpi Command test.
Elpi Accumulate lp:{{
% [divn N D M R] relates N and M as N = D * M + R, assuming D and R are known.
% If both N and M are unkown it suspends until one of the two becomes known.
pred divn o:int, i:int, o:int, i:int.
divn N D M R :- var N, var M, !, % if both N and M are unknown, suspend
declare_constraint (divn N D M R) [N, M]. % resume as soon N or M is known
divn N D M R :- var N, N is D * M + R. % if M is known
divn N D M R :- var M, M is N div D, R is N mod D. % if N is known
% [positive-constant N T] works both ways.
% - If N is known it divides it by 2 and chooses the branch looking at the reminder.
% - If T is known it delays all [divn N 2 M 1] or [divn N 2 M 0] goals until the very last
% M becomes 1. This resumes the last suspended goal which
% computes N out of [divn N 2 1 1] or [divn N 2 1 0]; in turn this N plays the role
% of M for the one to last suspended goal, which is resumed...
pred positive-constant o:int, o:term.
positive-constant 1 {{ lib:num.pos.xH }}.
positive-constant N {{ lib:num.pos.xO lp:T }} :- divn N 2 M 0, positive-constant M T.
positive-constant N {{ lib:num.pos.xI lp:T }} :- divn N 2 M 1, positive-constant M T.
main [int I] :- positive-constant I T, coq.say I T.
main [trm T] :- positive-constant I T, coq.say I T.
}}.
Elpi Typecheck.
Elpi test 3.
Elpi test 4.
Elpi test 5.
Elpi test (3%positive).
Elpi test (4%positive).
Elpi test (5%positive).
```

Constraints are "documented" here https://github.com/LPCIC/elpi/blob/master/ELPI.md#syntactic-constraints

performance wise, I have no idea if it sucks

A good technique to know! Thanks.

If you finish this example, covering Z, we could put it in the repo among the other examples, since I've none about constraints.

I could also add it in its current form. Let me anyway try do write some comments and tell me if they are clear enough.

Last updated: Feb 27 2024 at 22:02 UTC