## Stream: Elpi users & devs

### Topic: Predicate to associate Elpi `int` and Coq terms of `N`

#### Kazuhiko Sakaguchi (Apr 21 2021 at 13:49):

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.
``````

#### Enrico Tassi (Apr 21 2021 at 17:26):

``````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).
``````

#### Enrico Tassi (Apr 21 2021 at 17:30):

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

#### Enrico Tassi (Apr 21 2021 at 17:30):

performance wise, I have no idea if it sucks

#### Kazuhiko Sakaguchi (Apr 22 2021 at 04:34):

A good technique to know! Thanks.

#### Enrico Tassi (Apr 22 2021 at 07:53):

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

#### Enrico Tassi (Apr 22 2021 at 08:31):

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 04 2023 at 02:03 UTC