Experiments with program generation in Prolog

gen.pl

:- discontiguous nat/2.
:- discontiguous typ/2.

natlit(0, _).
natlit(X, s(N)) :-
    natlit(Y, N),
    X is Y + 1.

nat(lit(nat, X), s(N)) :- natlit(X, N).

nat(op(plus, X, Y), s(N)) :-
    nat(X, N),
    nat(Y, N).

typ(nat, _).

charlit('a', _).
charlit('b', _).

char(lit(char, C), s(N)) :- charlit(C, N).

typ(char, _).

listlit(_, [], _).
listlit(P, [H|T], s(N)) :- call(P, H, N), listlit(P, T, N).

list(P, lit(list, L), s(N)) :- listlit(P, L, N).

list(P, op(concat, X, Y), s(N)) :- list(P, X, N), list(P, Y, N).

typ(list(P), s(N)) :- typ(P, N).

nat(app(len, L), s(N)) :-
    typ(P, N),
    list(P, L, N).

to_peano(0, z).
to_peano(N, s(P)) :-
    N > 0,
    N1 is N - 1,
    to_peano(N1, P).

generate(What, Res, Upto) :-
    to_peano(Upto, N),
    typ(What, N),
    call(What, Res, N).

test.md

Examples

Generate all expressions of type nat up to depth 2

?- generate(nat, R, 2).
R = lit(nat, 0) ;
R = lit(nat, 1) ;
R = op(plus, lit(nat, 0), lit(nat, 0)) ;
R = app(len, lit(list, [])) ;
R = app(len, lit(list, [])) ;
R = app(len, lit(list, [])) ;
R = app(len, lit(list, [])) ;
false.

How many expressions of type list(nat) are there up to depth 5?

?- findall(R, generate(list(nat), R, 5), Q), length(Q, L).
Q = [lit(list, []), lit(list, [lit(nat, 0)]), lit(list, [lit(nat, 0), lit(nat, 0)]), lit(list, [lit(nat, 0), lit(nat, 0), lit(nat, 0)]), lit(list, [lit(nat, 0), lit(nat, 1)]), lit(list, [lit(nat, 0), lit(..., ...)|...]), lit(list, [lit(..., ...)|...]), lit(list, [...|...]), lit(..., ...)|...],
L = 3562.

How many expressions of arbitrary type are there up to depth 3?

?- findall((T, R), generate(T, R, 4), Q), length(Q, L).
Q = [(nat, lit(nat, 0)),  (nat, lit(nat, 1)),  (nat, lit(nat, 2)),  (nat, lit(nat, 3)),  (nat, op(plus, lit(nat, 0), lit(nat, 0))),  (nat, op(plus, lit(nat, 0), lit(nat, 1))),  (nat, op(plus, lit(..., ...), lit(..., ...))),  (nat, op(..., ..., ...)),  (..., ...)|...],
L = 4504.