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