Stream: Elpi users & devs

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


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Enrico Tassi (Apr 21 2021 at 17:30):

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

view this post on Zulip Enrico Tassi (Apr 21 2021 at 17:30):

performance wise, I have no idea if it sucks

view this post on Zulip Kazuhiko Sakaguchi (Apr 22 2021 at 04:34):

A good technique to know! Thanks.

view this post on Zulip 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.

view this post on Zulip 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