for review: rewrite of termination analysis (part 3)
Zoltan Somogyi
zs at cs.mu.oz.au
Mon Dec 22 14:50:57 AEDT 1997
This has effectively already been reviewed by Chris. It consists mostly
of benchmark programs from elsewhere, and the (correct) output of
termination analysis for them.
Zoltan.
Index: tests/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/Mmakefile,v
retrieving revision 1.1
diff -u -r1.1 Mmakefile
--- Mmakefile 1997/02/13 21:38:45 1.1
+++ Mmakefile 1997/11/03 01:25:06
@@ -1,4 +1,4 @@
-SUBDIRS = benchmarks general hard_coded invalid misc_tests valid warnings
+SUBDIRS = benchmarks general hard_coded invalid misc_tests term valid warnings
NUPROLOG_SUBDIRS = benchmarks general
main_target: check
New File: tests/term/Mmakefile
===================================================================
#-----------------------------------------------------------------------------#
main_target: check
include ../Mmake.common
#-----------------------------------------------------------------------------#
PROGS= \
ack \
append \
arit_exp \
associative \
dds1_2 \
dds3_13 \
dds3_14 \
dds3_15 \
dds3_17 \
dds3_8 \
fold \
list \
lte \
map \
member \
mergesort \
mergesort_ap \
mergesort_t \
mmatrix \
money \
naive_rev \
occur \
ordered \
overlap \
permutation \
pl1_1 \
pl1_2 \
pl2_3_1 \
pl3_1_1 \
pl3_5_6 \
pl3_5_6a \
pl4_01 \
pl4_4_3 \
pl4_4_6a \
pl4_5_2 \
pl4_5_3a \
pl5_2_2 \
pl6_1_1 \
pl7_2_9 \
pl7_6_2a \
pl7_6_2b \
pl7_6_2c \
pl8_2_1 \
pl8_2_1a \
pl8_3_1 \
pl8_3_1a \
pl8_4_1 \
pl8_4_2 \
queens \
quicksort \
select \
subset \
sum \
vangelder
modules:
@echo $(PROGS)
New File: tests/term/ack.m
===================================================================
:- module ack.
:- interface.
:- type nat ---> zero ; s(nat).
:- pred ack(nat, nat, nat).
:- mode ack(in, in, out) is det.
:- implementation.
% int(zero).
% int(s(X)) :- int(X).
ack(zero, N, s(N)). % :- int(N).
ack(s(M), zero, A) :-
ack(M, s(zero), A).
ack(s(M), s(N), A) :-
ack(s(M), N, A1),
ack(M, A1, A).
New File: tests/term/ack.trans_opt_exp
===================================================================
:- module ack.
:- pragma termination_info(ack:ack(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/append.m
===================================================================
:- module append.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred app(list(T), list(T), list(T)).
:- mode app(out, out, in) is multi.
:- implementation.
app([X|Xs], Ys, [X|Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/append.trans_opt_exp
===================================================================
:- module append.
:- pragma termination_info(append:app(mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, no, yes]), cannot_loop).
New File: tests/term/arit_exp.m
===================================================================
:- module arit_exp.
:- interface.
:- type expr ---> expr + expr ; expr * expr ; - expr ; int(int).
:- pred e(expr).
:- mode e(in) is semidet.
:- implementation.
e(X+Y) :-
f(X),
e(Y).
e(X) :-
f(X).
:- pred f(expr).
:- mode f(in) is semidet.
f(X*Y) :-
g(X),
f(Y).
f(X) :-
g(X).
:- pred g(expr).
:- mode g(in) is semidet.
g(-(X)) :-
e(X).
g(int(_X)).
New File: tests/term/arit_exp.trans_opt_exp
===================================================================
:- module arit_exp.
:- pragma termination_info(arit_exp:e(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/associative.m
===================================================================
:- module associative.
:- interface.
:- type expr ---> base ; op(expr, expr).
:- pred normal_form(expr, expr).
:- mode normal_form(in, out) is det.
:- implementation.
normal_form(F, N) :-
( rewrite(F, F1) ->
normal_form(F1, N)
;
N = F
).
:- pred rewrite(expr, expr).
:- mode rewrite(in, out) is semidet.
rewrite(In, Out) :-
( In = op(op(A, B), C) ->
Out = op(A, op(B, C))
;
In = op(A, op(B, C)),
Out = op(A, L),
rewrite(op(B, C), L)
).
New File: tests/term/associative.trans_opt_exp
===================================================================
:- module associative.
:- pragma termination_info(associative:normal_form(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/dds1_2.m
===================================================================
:- module dds1_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred permute(list(T)::in, list(T)::out) is nondet.
:- implementation.
permute([], []).
permute([X|Y], [U|V]) :-
delete(U, [X|Y], W),
permute(W, V).
:- pred delete(T, list(T), list(T)).
:- mode delete(out, in, out).
delete(X, [X|Y], Y).
delete(U, [X|Y], [X|Z]) :-
delete(U, Y, Z).
New File: tests/term/dds1_2.trans_opt_exp
===================================================================
:- module dds1_2.
:- pragma termination_info(dds1_2:permute(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/dds3_13.m
===================================================================
:- module dds3_13.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred duplicate(list(T)::in, list(T)::out) is det.
:- implementation.
duplicate([], []).
duplicate([X | Y], [X, X | Z]) :-
duplicate(Y, Z).
New File: tests/term/dds3_13.trans_opt_exp
===================================================================
:- module dds3_13.
:- pragma termination_info(dds3_13:duplicate(mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/dds3_14.m
===================================================================
:- module dds3_14.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred sum(list(int)::in, list(int)::in, list(int)::out) is semidet.
:- implementation.
:- import_module int.
sum([], [], []).
sum([X1 | Y1], [X2 | Y2], [X3 | Y3]) :-
X3 is X1+X2,
sum(Y1, Y2, Y3).
New File: tests/term/dds3_14.trans_opt_exp
===================================================================
:- module dds3_14.
:- pragma termination_info(dds3_14:sum(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/dds3_15.m
===================================================================
:- module dds3_15.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred merge(list(int)::in, list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
merge([], X, X).
merge(X, [], X).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X =< Y,
merge(Xs, [Y | Ys], Zs).
merge([X | Xs], [Y | Ys], [Y | Zs]) :-
Y > X,
merge([X | Xs], Ys, Zs).
New File: tests/term/dds3_15.trans_opt_exp
===================================================================
:- module dds3_15.
:- pragma termination_info(dds3_15:merge(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [yes, yes, no]), cannot_loop).
New File: tests/term/dds3_17.m
===================================================================
:- module dds3_17.
:- interface.
:- type expr ---> true ; false ; or(expr, expr) ; and(expr, expr).
:- pred dis(expr::in) is semidet.
:- pred con(expr::in) is semidet.
:- implementation.
dis(or(B1, B2)) :-
con(B1),
dis(B2).
dis(B) :-
con(B).
con(and(B1, B2)) :-
dis(B1),
con(B2).
con(B) :-
bool(B).
:- pred bool(expr).
:- mode bool(in).
bool(true).
bool(false).
New File: tests/term/dds3_17.trans_opt_exp
===================================================================
:- module dds3_17.
:- pragma termination_info(dds3_17:dis(mercury_builtin:in), finite(0, [no]), cannot_loop).
:- pragma termination_info(dds3_17:con(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/dds3_8.m
===================================================================
:- module dds3_8.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reverse(list(T)::in, list(T)::out, list(T)::in) is det.
:- implementation.
reverse([], X, X).
reverse([X | Y], Z, U) :-
reverse(Y, Z, [X | U]).
New File: tests/term/dds3_8.trans_opt_exp
===================================================================
:- module dds3_8.
:- pragma termination_info(dds3_8:reverse(mercury_builtin:in, mercury_builtin:out, mercury_builtin:in), finite(0, [no, yes, no, yes]), cannot_loop).
New File: tests/term/fold.m
===================================================================
:- module fold.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- type sym ---> a ; b ; c ; d.
:- pred fold(sym, list(sym), sym).
:- mode fold(in, in, out) is semidet.
:- implementation.
fold(X, [Y | Ys], Z) :-
xop(X, Y, V),
fold(V, Ys, Z).
fold(X, [], X).
:- pred xop(sym, sym, sym).
:- mode xop(in, in, out).
xop(a, b, c).
New File: tests/term/fold.trans_opt_exp
===================================================================
:- module fold.
:- pragma termination_info(fold:fold(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no, no]), cannot_loop).
New File: tests/term/list.m
===================================================================
:- module list.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred list(list(T)::in) is semidet.
:- implementation.
list([_H | Ts]) :-
list(Ts).
list([]).
New File: tests/term/list.trans_opt_exp
===================================================================
:- module list.
:- pragma termination_info(list:list(mercury_builtin:in), finite(0, [no, no]), cannot_loop).
New File: tests/term/lte.m
===================================================================
:- module lte.
:- interface.
:- pred goal is semidet.
:- implementation.
:- type nat ---> zero ; s(nat).
goal :-
lte(X, s(s(s(s(zero))))),
even(X).
:- pred lte(nat, nat).
:- mode lte(out, in).
lte(s(X), s(Y)) :-
lte(X, Y).
lte(zero, _Y).
:- pred even(nat).
:- mode even(in).
even(s(s(X))) :-
even(X).
even(zero).
New File: tests/term/lte.trans_opt_exp
===================================================================
:- module lte.
:- pragma termination_info(lte:goal, finite(0, []), cannot_loop).
New File: tests/term/map.m
===================================================================
:- module map.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred map(list(x)::in, list(x)::out) is semidet.
:- type x ---> val_i ; val_j ; val_k.
:- implementation.
:- pred p(x, x).
:- mode p(in, out).
p(val_i, val_j).
map([X | Xs], [Y | Ys]) :-
p(X, Y),
map(Xs, Ys).
map([], []).
New File: tests/term/map.trans_opt_exp
===================================================================
:- module map.
:- pragma termination_info(map:map(mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/member.m
===================================================================
:- module member.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred member(T::out, list(T)::in) is nondet.
:- implementation.
member(X, [_Y| Xs]) :-
member(X, Xs).
member(X, [X| _Xs]).
New File: tests/term/member.trans_opt_exp
===================================================================
:- module member.
:- pragma termination_info(member:member(mercury_builtin:out, mercury_builtin:in), finite(-1, [no, no, yes]), cannot_loop).
New File: tests/term/mergesort.m
===================================================================
:- module mergesort.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([X], [X]).
mergesort([X, Y | Xs], Ys) :-
split([X, Y | Xs], X1s, X2s),
mergesort(X1s, Y1s),
mergesort(X2s, Y2s),
merge(Y1s, Y2s, Ys).
:- pred split(list(T), list(T), list(T)).
:- mode split(in, out, out).
split([], [], []).
split([X | Xs], [X | Ys], Zs) :-
split(Xs, Zs, Ys).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X =< Y,
merge(Xs, [Y | Ys], Zs).
merge([X | Xs], [Y | Ys], [Y | Zs]) :-
X > Y,
merge([X | Xs], Ys, Zs).
New File: tests/term/mergesort.trans_opt_exp
===================================================================
:- module mergesort.
:- pragma termination_info(mergesort:mergesort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/mergesort_ap.m
===================================================================
% this is a version of mergesort that appears in
% K. A. Apt and D. Pedreschi, Modular Termination Proofs for Logic and Pure
% Prolog Programs, Dipartimento di Informatica, Universita di Pisa, 1993
% mergesort(Xs, Ys, Xs) if Ys is an ordered permutation of the list Xs
:- module mergesort_ap.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out, list(int)::in) is nondet.
:- implementation.
:- import_module int.
mergesort([], [], _Ls).
mergesort([X], [X], _Ls).
mergesort([X, Y | Xs], Ys, [H | Ls]) :-
split([X, Y | Xs], X1s, X2s, [H | Ls]),
mergesort(X1s, Y1s, Ls),
mergesort(X2s, Y2s, Ls),
merge(Y1s, Y2s, Ys, [H | Ls]).
:- pred split(list(T), list(T), list(T), list(T)).
:- mode split(in, out, out, in).
split([], [], [], _Ls).
split([X | Xs], [X | Ys], Zs, [_H | Ls]) :-
split(Xs, Zs, Ys, Ls).
:- pred merge(list(int), list(int), list(int), list(int)).
:- mode merge(in, in, out, in).
merge([], Xs, Xs, _Ls).
merge(Xs, [], Xs, _Ls).
merge([X | Xs], [Y | Ys], [X | Zs], [_H | Ls]) :-
X =< Y,
merge(Xs, [Y | Ys], Zs, Ls).
merge([X | Xs], [Y | Ys], [Y | Zs], [_H | Ls]) :-
X > Y,
merge([X | Xs], Ys, Zs, Ls).
New File: tests/term/mergesort_ap.trans_opt_exp
===================================================================
:- module mergesort_ap.
:- pragma termination_info(mergesort_ap:mergesort(mercury_builtin:in, mercury_builtin:out, mercury_builtin:in), finite(0, [yes, no, no]), cannot_loop).
New File: tests/term/mergesort_t.m
===================================================================
:- module mergesort_t.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([X], [X]).
mergesort([X, Y | Xs], Ys) :-
split2([X, Y | Xs], X1s, X2s),
mergesort(X1s, Y1s),
mergesort(X2s, Y2s),
merge(Y1s, Y2s, Ys).
:- pred split(list(T), list(T), list(T)).
:- mode split(in, out, out).
split(Xs, Ys, Zs) :-
split0(Xs, Ys, Zs).
split(Xs, Ys, Zs) :-
split1(Xs, Ys, Zs).
split(Xs, Ys, Zs) :-
split2(Xs, Ys, Zs).
:- pred split0(list(T), list(T), list(T)).
:- mode split0(in, out, out).
split0([], [], []).
:- pred split1(list(T), list(T), list(T)).
:- mode split1(in, out, out).
split1([X], [X], []).
:- pred split2(list(T), list(T), list(T)).
:- mode split2(in, out, out).
split2([X, Y | Xs], [X | Ys], [Y | Zs]) :-
split(Xs, Ys, Zs).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X=<Y,
merge(Xs, [Y | Ys], Zs).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X>Y,
merge([X | Xs], Ys, Zs).
New File: tests/term/mergesort_t.trans_opt_exp
===================================================================
:- module mergesort_t.
:- pragma termination_info(mergesort_t:mergesort(mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/mmatrix.m
===================================================================
%------------------------------------------------------------------------------
% Benchmark Program - matrix*matrix multiplication
%
% Copyright by Manuel Hermenegildo
% Date: January 17 1986
%
%------------------------------------------------------------------------------
:- module mmatrix.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mmultiply(list(list(int)), list(list(int)), list(list(int))).
:- mode mmultiply(in, in, out) is semidet.
:- implementation.
:- import_module int.
mmultiply([], _, []).
mmultiply([V0 | Rest], V1, [Result | Others]) :-
mmultiply(Rest, V1, Others),
multiply(V1, V0, Result).
:- pred multiply(list(list(int)), list(int), list(int)).
:- mode multiply(in, in, out).
multiply([], _, []).
multiply([V0 | Rest], V1, [Result | Others]) :-
multiply(Rest, V1, Others),
vmul(V0, V1, Result).
:- pred vmul(list(int), list(int), int).
:- mode vmul(in, in, out).
vmul([], [], 0).
vmul([H1 | T1], [H2 | T2], Result) :-
vmul(T1, T2, Newresult),
Product is H1*H2,
Result is Product+Newresult.
New File: tests/term/mmatrix.trans_opt_exp
===================================================================
:- module mmatrix.
:- pragma termination_info(mmatrix:mmultiply(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/money.m
===================================================================
/*-----------------------------------------------------------------------------
Program: Cryptarithmetic puzzle SENDMORY
Author: Rong Yang (adapted)
Date:
Notes:
1. To run:
?- money(S, E, N, D, M, O, R, Y).
2. Solution is reached in the domain approach so as to recognize determinism
as the ecuations are being resolved.
3. After-checks are used and calc/5 ordering is better (L to R).
compiled it takes about 50 sec.
-----------------------------------------------------------------------------*/
:- module money.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred solve(list(int)::out) is nondet.
:- implementation.
:- import_module int.
solve([S, E, N, D, M, O, R, Y]) :-
money(S, E, N, D, M, O, R, Y).
:- pred money(int, int, int, int, int, int, int, int).
:- mode money(out, out, out, out, out, out, out, out).
money(S, E, N, D, M, O, R, Y) :-
carry(C1),
carry(C2),
carry(C3),
carry(C4),
C4 = M,
M \= 0,
domain([S, E, N, D, M, O, R, Y], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]),
S \= 0,
calc(C3, S, M, C4, O),
calc(C2, E, O, C3, N),
calc(C1, N, R, C2, E),
calc( 0, D, E, C1, Y).
:- pred calc(int, int, int, int, int).
:- mode calc(in, in, in, in, in).
calc(C0, D, E, C1, Y) :-
sum(C0, D, CD),
sum(CD, E, S),
carry10(C1, C10),
sum(C10, Y, S).
:- pred sum(int, int, int).
:- mode sum(in, in, out).
sum(X, Y, Z) :-
Z is X+Y.
:- pred domain(list(T), list(T)).
:- mode domain(out, in).
domain([], _).
domain([X1 | R], L) :-
del(X1, L, NL),
domain(R, NL).
:- pred del(T, list(T), list(T)).
:- mode del(out, in, out).
del(X, [X | T], T).
del(X, [Y | T], [Y | NT]) :-
del(X, T, NT).
:- pred carry(int).
:- mode carry(out).
carry(1).
carry(0).
:- pred carry10(int, int).
:- mode carry10(in, out).
carry10(0, 0).
carry10(1, 10).
New File: tests/term/money.trans_opt_exp
===================================================================
:- module money.
:- pragma termination_info(money:solve(mercury_builtin:out), finite(10, [no]), cannot_loop).
New File: tests/term/naive_rev.m
===================================================================
:- module naive_rev.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reverse(list(T)::in, list(T)::out) is det.
:- implementation.
reverse([X | Xs], Ys) :-
reverse(Xs, Zs),
app(Zs, [X], Ys).
reverse([], []).
:- pred app(list(T)::in, list(T)::in, list(T)::out).
app([X | Xs], Ys, [X | Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/naive_rev.trans_opt_exp
===================================================================
:- module naive_rev.
:- pragma termination_info(naive_rev:reverse(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/occur.m
===================================================================
%------------------------------------------------------------------------------
% Benchmark Program - Counting occurrences in lists
%
% Author: B. Ramkumar and L. V. Kale
% Date:
%
% To test: run o/1.
%------------------------------------------------------------------------------
% Benchmark is o(31), runs with -A1 -E256 -C128
:- module occur.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred occurall(list(int), list(list(int)), list(list(int))).
:- mode occurall(in, in, out) is nondet.
:- implementation.
:- import_module int.
occurall([], _X, []).
occurall([X | Y], Z, [[X, W] | V]) :-
occur(X, Z, W),
occurall(Y, Z, V).
:- pred occur(T1, list(list(T1)), int).
:- mode occur(in, in, out).
occur(_X, [], 0).
occur(X, [Y | Z], W) :-
(
count(X, Y, A),
occur(X, Z, B)
->
W is A + B
;
fail
).
:- pred count(T1, list(T1), int).
:- mode count(in, in, out).
count(_X, [], 0).
count(X, [Y | Z], W) :-
( count(X, Z, W1) ->
addx(X, Y, W1, W)
;
fail
).
:- pred addx(T1, T1, int, int).
:- mode addx(in, in, in, out).
addx(X, X, W1, W) :-
W is W1 + 1.
addx(X, Y, W1, W1) :-
X \= Y.
New File: tests/term/occur.trans_opt_exp
===================================================================
:- module occur.
:- pragma termination_info(occur:occurall(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/ordered.m
===================================================================
:- module ordered.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred ordered(list(int)::in) is semidet.
:- implementation.
:- import_module int.
ordered([]).
ordered([_X]).
ordered([X,Y | Xs]) :-
X =< Y,
ordered([Y | Xs]).
New File: tests/term/ordered.trans_opt_exp
===================================================================
:- module ordered.
:- pragma termination_info(ordered:ordered(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/overlap.m
===================================================================
:- module overlap.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred overlap(list(T)::in, list(T)::in) is semidet.
:- implementation.
overlap(Xs, Ys) :-
member(X, Xs),
member(X, Ys).
% has_a_or_b(Xs) :- overlap(Xs, [a, b]).
:- pred member(T, list(T)).
:- mode member(out, in).
member(X, [_Y | Xs]) :-
member(X, Xs).
member(X, [X | _Xs]).
New File: tests/term/overlap.trans_opt_exp
===================================================================
:- module overlap.
:- pragma termination_info(overlap:overlap(mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no]), cannot_loop).
New File: tests/term/permutation.m
===================================================================
:- module permutation.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred perm(list(T)::in, list(T)::out) is nondet.
:- implementation.
perm(Xs, [X | Ys]) :-
app(X1s, [X | X2s], Xs),
app(X1s, X2s, Zs),
perm(Zs, Ys).
perm([], []).
:- pred app(list(T), list(T), list(T)).
:- mode app(out, out, in).
:- mode app(in, in, out).
app([X | Xs], Ys, [X | Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/permutation.trans_opt_exp
===================================================================
:- module permutation.
:- pragma termination_info(permutation:perm(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/pl1_1.m
===================================================================
:- module pl1_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out) is det.
:- mode append(out, out, in) is multi.
% :- mode append(out, in, out) is nondet. NOT WELL MODED
:- implementation.
append([], L, L).
append([H | L1], L2, [H | L3]) :-
append(L1, L2, L3).
New File: tests/term/pl1_1.trans_opt_exp
===================================================================
:- module pl1_1.
:- pragma termination_info(pl1_1:append(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, yes, no]), cannot_loop).
:- pragma termination_info(pl1_1:append(mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, no, yes]), cannot_loop).
New File: tests/term/pl1_2.m
===================================================================
:- module pl1_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred perm(list(T)::in, list(T)::out) is nondet.
:- implementation.
perm([], []).
perm(L, [H | T]) :-
append(V, [H | U], L),
append(V, U, W),
perm(W, T).
:- pred append(list(T), list(T), list(T)).
:- mode append(out, out, in).
:- mode append(in, in, out).
append([], Y, Y).
append([H | X], Y, [H | Z]) :-
append(X, Y, Z).
New File: tests/term/pl1_2.trans_opt_exp
===================================================================
:- module pl1_2.
:- pragma termination_info(pl1_2:perm(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/pl2_3_1.m
===================================================================
:- module pl2_3_1.
:- interface.
:- type node ---> a ; b ; c.
:- pred p(node::in, node::out) is multi.
:- implementation.
p(X, Z) :-
q(X, Y),
p(Y, Z).
p(X, X).
:- pred q(node, node).
:- mode q(in, out).
q(a, b).
New File: tests/term/pl2_3_1.trans_opt_exp
===================================================================
:- module pl2_3_1.
:- pragma termination_info(pl2_3_1:p(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/pl3_1_1.m
===================================================================
:- module pl3_1_1.
:- interface.
:- pred a is semidet. % DIAGNOSED BY COMPILER
:- pred b is semidet. % DIAGNOSED BY COMPILER
:- pred c is semidet. % DIAGNOSED BY COMPILER
:- pred d is semidet. % DIAGNOSED BY COMPILER
:- pred e is semidet. % DIAGNOSED BY COMPILER
:- pred f is semidet. % DIAGNOSED BY COMPILER
:- pred g is semidet. % DIAGNOSED BY COMPILER
:- implementation.
a :- b.
a :- e.
b :- c.
c :- d.
d :- b.
e :- f.
f :- g.
g :- e.
New File: tests/term/pl3_1_1.trans_opt_exp
===================================================================
:- module pl3_1_1.
:- pragma termination_info(pl3_1_1:a, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:b, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:c, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:d, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:e, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:f, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:g, finite(0, []), can_loop).
New File: tests/term/pl3_5_6.m
===================================================================
:- module pl3_5_6.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred p(list(int)::out) is nondet.
:- implementation.
p(X) :-
l(X),
q(X).
:- pred q(list(T)).
:- mode q(in).
q([_A]).
:- pred r(int).
:- mode r(out).
r(1).
:- pred l(list(int)).
:- mode l(out). % DIAGNOSED BY COMPILER
l([]).
l([H | T]) :-
r(H),
l(T).
New File: tests/term/pl3_5_6.trans_opt_exp
===================================================================
:- module pl3_5_6.
:- pragma termination_info(pl3_5_6:p(mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl3_5_6a.m
===================================================================
:- module pl3_5_6a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred p(list(int)::out) is nondet.
:- implementation.
p([A]) :-
l([A]).
:- pred q(list(T)).
:- mode q(in).
q([_A]).
:- pred r(int).
:- mode r(out).
r(1).
:- pred l(list(int)).
:- mode l(out). % DIAGNOSED BY COMPILER
l([]).
l([H | T]) :-
r(H),
l(T).
New File: tests/term/pl3_5_6a.trans_opt_exp
===================================================================
:- module pl3_5_6a.
:- pragma termination_info(pl3_5_6a:p(mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl4_01.m
===================================================================
:- module pl4_01.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred append3(list(T), list(T), list(T), list(T)).
:- mode append3(in, in, in, out) is det.
:- mode append3(out, out, out, in) is multi.
:- implementation.
append3(A, B, C, D) :-
append(A, B, E),
append(E, C, D).
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out).
:- mode append(out, out, in).
append([], L, L).
append([H | L1], L2, [H | L3]) :-
append(L1, L2, L3).
New File: tests/term/pl4_01.trans_opt_exp
===================================================================
:- module pl4_01.
:- pragma termination_info(pl4_01:append3(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, yes, yes, no]), cannot_loop).
:- pragma termination_info(pl4_01:append3(mercury_builtin:out, mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, no, no, yes]), cannot_loop).
New File: tests/term/pl4_4_3.m
===================================================================
:- module pl4_4_3.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred merge(list(int)::in, list(int)::in, list(int)::out) is nondet.
:- import_module int.
:- implementation.
merge(X, [], X).
merge([], X, X).
merge([A | X], [B | Y], [A | Z]) :-
A =< B,
merge(X, [B | Y], Z).
merge([A | X], [B | Y], [B | Z]) :-
A > B,
merge([A | X], Y, Z).
New File: tests/term/pl4_4_3.trans_opt_exp
===================================================================
:- module pl4_4_3.
:- pragma termination_info(pl4_4_3:merge(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [yes, yes, no]), cannot_loop).
New File: tests/term/pl4_4_6a.m
===================================================================
:- module pl4_4_6a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred perm(list(T)::in, list(T)::out) is nondet.
:- implementation.
perm([], []).
perm([X | L], Z) :-
perm(L, Y),
insert(X, Y, Z).
:- pred insert(T, list(T), list(T)).
:- mode insert(in, in, out).
insert(X, [], [X]).
insert(X, L, [X | L]).
insert(X, [H | L1], [H | L2]) :-
insert(X, L1, L2).
New File: tests/term/pl4_4_6a.trans_opt_exp
===================================================================
:- module pl4_4_6a.
:- pragma termination_info(pl4_4_6a:perm(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/pl4_5_2.m
===================================================================
:- module pl4_5_2.
:- interface.
:- type expr ---> expr + expr
; num(int).
:- pred s(expr::in, expr::out) is nondet.
:- implementation.
:- import_module int.
s(A+(B+C), D) :-
s((A+B)+C, D).
s(A+B, C) :-
s(B+A, C).
s(X+num(0), X).
s(X+Y, Z) :-
s(X, A),
s(Y, B),
s(A+B, Z).
s(A+B, C) :-
A = num(Anum),
B = num(Bnum),
Cnum is Anum + Bnum,
C = num(Cnum).
New File: tests/term/pl4_5_2.trans_opt_exp
===================================================================
:- module pl4_5_2.
:- pragma termination_info(pl4_5_2:s(mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl4_5_3a.m
===================================================================
:- module pl4_5_3a.
:- interface.
:- type node ---> a ; b ; c.
:- pred p(node).
:- mode p(in) is semidet. % DIAGNOSED BY COMPILER
:- mode p(out) is multi.
:- implementation.
p(b).
p(a) :-
p(_X).
New File: tests/term/pl4_5_3a.trans_opt_exp
===================================================================
:- module pl4_5_3a.
:- pragma termination_info(pl4_5_3a:p(mercury_builtin:in), finite(0, [no]), can_loop).
:- pragma termination_info(pl4_5_3a:p(mercury_builtin:out), finite(0, [no]), can_loop).
New File: tests/term/pl5_2_2.m
===================================================================
:- module pl5_2_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred turing(t_tuple, state, list(p_tuple), t_tuple).
:- mode turing(in, in, in, out) is nondet.
:- type t_tuple ---> t(list(sym), sym, list(sym)).
:- type p_tuple ---> p(state, sym, state, sym, dir).
:- type sym ---> blank ; nonblank.
:- type dir ---> r ; l.
:- type state ---> halt ; nonhalt.
:- implementation.
turing(t(X, Y, Z), S, P, t(X, Y, Z)) :-
member(p(S, Y, halt, _W, _D), P).
turing(t(X, Y, [R | L]), S, P, T) :-
member(p(S, Y, S1, W, r), P),
turing(t([W | X], R, L), S1, P, T).
turing(t(X, Y, []), S, P, T) :-
member(p(S, Y, S1, W, r), P),
turing(t([W | X], blank, []), S1, P, T).
turing(t([X | L], Y, R), S, P, T) :-
member(p(S, Y, S1, W, l), P),
turing(t(L, X, [W | R]), S1, P, T).
turing(t([], Y, R), S, P, T) :-
member(p(S, Y, S1, W, l), P),
turing(t([], blank, [W | R]), S1, P, T).
:- pred member(T, list(T)).
:- mode member(out, in) is nondet.
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
New File: tests/term/pl5_2_2.trans_opt_exp
===================================================================
:- module pl5_2_2.
:- pragma termination_info(pl5_2_2:turing(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl6_1_1.m
===================================================================
:- module pl6_1_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred qsort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
qsort([], []).
qsort([H | L], S) :-
split(L, H, A, B),
qsort(A, A1),
qsort(B, B1),
append(A1, [H | B1], S).
:- pred split(list(int), int, list(int), list(int)).
:- mode split(in, in, out, out).
split([], _Y, [], []).
split([X | Xs], Y, [X | Ls], Bs) :-
X =< Y,
split(Xs, Y, Ls, Bs).
split([X | Xs], Y, Ls, [X | Bs]) :-
X > Y,
split(Xs, Y, Ls, Bs).
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out).
append([], L, L).
append([H | L1], L2, [H | L3]) :-
append(L1, L2, L3).
New File: tests/term/pl6_1_1.trans_opt_exp
===================================================================
:- module pl6_1_1.
:- pragma termination_info(pl6_1_1:qsort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/pl7_2_9.m
===================================================================
:- module pl7_2_9.
:- interface.
:- pred mult(nat::in, nat::in, nat::out) is det.
:- type nat ---> zero ; s(nat).
:- implementation.
mult(zero, _Y, zero).
mult(s(X), Y, Z) :-
mult(X, Y, Z1),
add(Z1, Y, Z).
:- pred add(nat, nat, nat).
:- mode add(in, in, out).
add(zero, Y, Y).
add(s(X), Y, s(Z)) :-
add(X, Y, Z).
New File: tests/term/pl7_2_9.trans_opt_exp
===================================================================
:- module pl7_2_9.
:- pragma termination_info(pl7_2_9:mult(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/pl7_6_2a.m
===================================================================
:- module pl7_6_2a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reach(T::in, T::in, list(list(T))::in) is semidet.
:- implementation.
reach(X, Y, Edges) :-
member([X, Y], Edges).
reach(X, Z, Edges) :-
member([X, Y], Edges),
reach(Y, Z, Edges).
:- pred member(T, list(T)).
:- mode member(in, in).
:- mode member(out, in).
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
New File: tests/term/pl7_6_2a.trans_opt_exp
===================================================================
:- module pl7_6_2a.
:- pragma termination_info(pl7_6_2a:reach(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no, no]), can_loop).
New File: tests/term/pl7_6_2b.m
===================================================================
:- module pl7_6_2b.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reach(T::in, T::in, list(list(T))::in, list(T)::in) is semidet.
:- implementation.
reach(X, Y, Edges, _Visited) :-
member([X, Y], Edges).
reach(X, Z, Edges, Visited) :-
member([X, Y], Edges),
\+ member(Y, Visited),
reach(Y, Z, Edges, [Y | Visited]).
:- pred member(T, list(T)).
:- mode member(in, in).
:- mode member(out, in).
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
New File: tests/term/pl7_6_2b.trans_opt_exp
===================================================================
:- module pl7_6_2b.
:- pragma termination_info(pl7_6_2b:reach(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no, no, no]), can_loop).
New File: tests/term/pl7_6_2c.m
===================================================================
:- module pl7_6_2c.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reach(T::in, T::in, list(list(T))::in, list(T)::in) is semidet.
:- implementation.
reach(X, Y, Edges, _Not_Visited) :-
member([X, Y], Edges).
reach(X, Z, Edges, Not_Visited) :-
member([X, Y], Edges),
member(Y, Not_Visited),
delete(Y, Not_Visited, V1),
reach(Y, Z, Edges, V1).
:- pred member(T, list(T)).
:- mode member(in, in).
:- mode member(out, in).
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
:- pred delete(T, list(T), list(T)).
:- mode delete(out, in, out).
delete(X, [X | Y], Y).
delete(X, [H | T1], [H | T2]) :-
delete(X, T1, T2).
New File: tests/term/pl7_6_2c.trans_opt_exp
===================================================================
:- module pl7_6_2c.
:- pragma termination_info(pl7_6_2c:reach(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no, no, no]), cannot_loop).
New File: tests/term/pl8_2_1.m
===================================================================
:- module pl8_2_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([E], [E]).
mergesort([E, F | U], V) :-
s([E, F | U], W, Y),
mergesort(W, X),
mergesort(Y, Z),
merge(X, Z, V).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge(X, [], X).
merge([], X, X).
merge([A | X], [B | Y], [A | Z]) :-
A =< B,
merge(X, [B | Y], Z).
merge([A | X], [B | Y], [B | Z]) :-
A > B,
merge([A | X], Y, Z).
:- pred s(list(T), list(T), list(T)).
:- mode s(in, out, out).
s([], [], []).
s([E | U], [E | V], W) :-
s(U, W, V).
New File: tests/term/pl8_2_1.trans_opt_exp
===================================================================
:- module pl8_2_1.
:- pragma termination_info(pl8_2_1:mergesort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/pl8_2_1a.m
===================================================================
:- module pl8_2_1a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([E], [E]).
mergesort([X, Y | Z], U) :-
s(Z, V, W),
mergesort([X | V], X1),
mergesort([Y | W], Y1),
merge(X1, Y1, U).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge([], X, X).
merge([A | X], [B | Y], [A | Z]) :-
A =< B,
merge(X, [B | Y], Z).
merge([A | X], [B | Y], [B | Z]) :-
A > B,
merge([A | X], Y, Z).
:- pred s(list(T), list(T), list(T)).
:- mode s(in, out, out).
s([], [], []).
s([E | U], [E | V], W) :-
s(U, W, V).
New File: tests/term/pl8_2_1a.trans_opt_exp
===================================================================
:- module pl8_2_1a.
:- pragma termination_info(pl8_2_1a:mergesort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/pl8_3_1.m
===================================================================
:- module pl8_3_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred xminsort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
xminsort([], []).
xminsort(L, [X | L1]) :-
xmin1(X, L),
remove(X, L, L2),
xminsort(L2, L1).
:- pred xmin1(int, list(int)).
:- mode xmin1(out, in).
xmin1(M, [X | L]) :-
xmin2(X, M, L).
:- pred xmin2(int, int, list(int)).
:- mode xmin2(in, out, in).
xmin2(X, X, []).
xmin2(X, A, [M | L]) :-
xmin(X, M, B),
xmin2(B, A, L).
:- pred xmin(int, int, int).
:- mode xmin(in, in, out).
xmin(X, Y, X) :-
X =< Y.
xmin(X, Y, Y) :-
X > Y.
:- pred remove(T, list(T), list(T)).
:- mode remove(in, in, out).
remove(_N, [], []).
remove(N, [N | L], L).
remove(N, [M | L], [M | L1]) :-
N \= M,
remove(N, L, L1).
New File: tests/term/pl8_3_1.trans_opt_exp
===================================================================
:- module pl8_3_1.
:- pragma termination_info(pl8_3_1:xminsort(mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl8_3_1a.m
===================================================================
:- module pl8_3_1a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred xminsort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
xminsort([], []).
xminsort(L, [X | L1]) :-
xmin1(X, L),
remove(X, L, L2),
xminsort(L2, L1).
:- pred xmin1(int, list(int)).
:- mode xmin1(out, in).
xmin1(M, [X | L]) :-
xmin2(X, M, L).
:- pred xmin2(int, int, list(int)).
:- mode xmin2(in, out, in).
xmin2(X, X, []).
xmin2(X, A, [M | L]) :-
xmin(X, M, B),
xmin2(B, A, L).
:- pred xmin(int, int, int).
:- mode xmin(in, in, out).
xmin(X, Y, X) :-
X =< Y.
xmin(X, Y, Y) :-
X > Y.
:- pred remove(T, list(T), list(T)).
:- mode remove(in, in, out).
%remove(N, [], []). (this case cannot occur in our program)
remove(N, [N | L], L).
remove(N, [M | L], [M | L1]) :-
\+ N = M,
remove(N, L, L1).
New File: tests/term/pl8_3_1a.trans_opt_exp
===================================================================
:- module pl8_3_1a.
:- pragma termination_info(pl8_3_1a:xminsort(mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/pl8_4_1.m
===================================================================
:- module pl8_4_1.
:- interface.
:- type nat ---> zero ; s(nat).
:- pred even(nat::in) is semidet.
:- pred odd(nat::in) is semidet.
:- implementation.
even(zero).
even(s(X)) :-
odd(X).
odd(s(X)) :-
even(X).
New File: tests/term/pl8_4_1.trans_opt_exp
===================================================================
:- module pl8_4_1.
:- pragma termination_info(pl8_4_1:even(mercury_builtin:in), finite(0, [no]), cannot_loop).
:- pragma termination_info(pl8_4_1:odd(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/pl8_4_2.m
===================================================================
:- module pl8_4_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- type token ---> a ; b ; c ; plus ; times ; lparen ; rparen.
:- pred e(list(token)::in, list(token)::out) is nondet.
:- implementation.
e(L, T) :- t(L, T).
e(L, T) :- t(L, [plus | C]), e(C, T).
:- pred t(list(token), list(token)).
:- mode t(in, out).
t(L, T) :- n(L, T).
t(L, T) :- n(L, [times | C]), t(C, T).
:- pred n(list(token), list(token)).
:- mode n(in, out).
n([L | T], T) :-
z(L).
n([lparen | A], B) :-
e(A, [rparen | B]).
:- pred z(token).
:- mode z(in).
z(a).
z(b).
z(c).
New File: tests/term/pl8_4_2.trans_opt_exp
===================================================================
:- module pl8_4_2.
:- pragma termination_info(pl8_4_2:e(mercury_builtin:in, mercury_builtin:out), finite(-1, [yes, no]), cannot_loop).
New File: tests/term/queens.m
===================================================================
:- module queens.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred queens(list(int), list(int)).
:- mode queens(in, out) is nondet.
:- implementation.
:- import_module int.
queens(X, Y) :-
perm(X, Y),
safe(Y).
:- pred perm(list(T), list(T)).
:- mode perm(in, out).
perm([], []).
perm([X | Y], [V | Res]) :-
delete(V, [X | Y], Rest),
perm(Rest, Res).
:- pred delete(T, list(T), list(T)).
:- mode delete(out, in, out).
delete(X, [X | Y], Y).
delete(X, [F | T], [F | R]) :-
delete(X, T, R).
:- pred safe(list(int)).
:- mode safe(in).
safe([]).
safe([X | Y]) :-
noattack(X, Y, 1),
safe(Y).
:- pred noattack(int, list(int), int).
:- mode noattack(in, in, di).
noattack(_X, [], _N).
noattack(X, [F | T], N) :-
X \= F,
X \= F + N,
F \= X + N,
N1 is N + 1,
noattack(X, T, N1).
New File: tests/term/queens.trans_opt_exp
===================================================================
:- module queens.
:- pragma termination_info(queens:queens(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/quicksort.m
===================================================================
:- module quicksort.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred qs(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
qs([X | Xs], Ys) :-
part(X, Xs, Littles, Bigs),
qs(Littles, Ls),
qs(Bigs, Bs),
app(Ls, [X | Bs], Ys).
qs([], []).
:- pred part(int, list(int), list(int), list(int)).
:- mode part(in, in, out, out).
part(X, [Y | Xs], [Y | Ls], Bs) :-
X > Y,
part(X, Xs, Ls, Bs).
part(X, [Y | Xs], Ls, [Y | Bs]) :-
X =< Y,
part(X, Xs, Ls, Bs).
part(_X, [], [], []).
:- pred app(list(int), list(int), list(int)).
:- mode app(in, in, out).
app([X | Xs], Ys, [X | Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/quicksort.trans_opt_exp
===================================================================
:- module quicksort.
:- pragma termination_info(quicksort:qs(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/runtests
===================================================================
#!/bin/sh
# Test whether the termination analysis algorithm of the Mercury compiler
# is working right.
# Return a status of 0 (true) if everything is all right, and 1 otherwise.
set -x
stdoptions="--make-trans-opt --enable-termination"
options="$stdoptions --term-single-arg 5 --term-norm simple"
modules=`mmake modules`
cat /dev/null > .allres
failure=""
for module in $modules
do
/bin/rm $module.trans_opt > /dev/null 2>&1
lmc3 -C $options $module > $module.out 2>&1
if test "$?" = 0
then
diff -u $module.trans_opt $module.trans_opt_exp > $module.res
cat $module.res >> .allres
else
failure="$failure $module"
fi
done
if test ! -s .allres -a "$failure" = ""
then
echo "the tests in the term directory succeeded"
rm -f .allres
exit 0
else
echo "the tests in the term directory failed"
echo "the following modules had the compiler fail:"
echo $failure
echo "the differences are:"
cat .allres
exit 1
fi
New File: tests/term/select.m
===================================================================
:- module select.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred select(T::out, list(T)::in, list(T)::out) is nondet.
:- implementation.
select(X, [X | Xs], Xs).
select(X, [Y | Xs], [Y | Zs]) :-
select(X, Xs, Zs).
New File: tests/term/select.trans_opt_exp
===================================================================
:- module select.
:- pragma termination_info(select:select(mercury_builtin:out, mercury_builtin:in, mercury_builtin:out), finite(-1, [no, no, yes, no]), cannot_loop).
New File: tests/term/subset.m
===================================================================
:- module subset.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred subset(list(T), list(T)).
:- mode subset(in, in) is semidet.
:- mode subset(out, in) is multi. % gets warning
:- implementation.
subset([X | Xs], Ys) :-
member(X, Ys),
subset(Xs, Ys).
subset([], _Ys).
:- pred member(T, list(T)).
:- mode member(out, in).
member(X, [_Y | Xs]) :-
member(X, Xs).
member(X, [X | _Xs]).
New File: tests/term/subset.trans_opt_exp
===================================================================
:- module subset.
:- pragma termination_info(subset:subset(mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no]), cannot_loop).
:- pragma termination_info(subset:subset(mercury_builtin:out, mercury_builtin:in), infinite, can_loop).
New File: tests/term/sum.m
===================================================================
:- module sum.
:- interface.
:- pred sum(nat, nat, nat).
% :- mode sum(out, in, out) is nondet. SECOND CLAUSE NOT WELL MODED
:- mode sum(out, out, in) is multi.
:- type nat ---> zero ; s(nat).
:- implementation.
sum(X, s(Y), s(Z)) :-
sum(X, Y, Z).
sum(X, zero, X).
New File: tests/term/sum.trans_opt_exp
===================================================================
:- module sum.
:- pragma termination_info(sum:sum(mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, yes]), cannot_loop).
New File: tests/term/vangelder.m
===================================================================
% The vangelder example from Lindenstrauss and Sagiv
% (takes them more than four minutes to crack).
:- module vangelder.
:- interface.
:- type foo ---> a ; b ; c ; f(foo).
:- pred q(foo, foo).
:- mode q(in, in) is semidet.
:- implementation.
q(X, Y) :-
e(X, Y).
q(X, f(f(X))) :-
p(X, f(f(X))),
q(X, f(X)).
q(X, f(f(Y))) :-
p(X, f(Y)).
:- pred p(foo, foo).
:- mode p(in, in) is semidet.
p(X, Y) :-
e(X, Y).
p(X, f(Y)) :-
r(X, f(Y)),
p(X, Y).
:- pred r(foo, foo).
:- mode r(in, in) is semidet.
r(X, Y) :-
e(X, Y).
r(X, f(Y)) :-
q(X, Y),
r(X, Y).
r(f(X), f(X)) :-
t(f(X), f(X)).
:- pred t(foo, foo).
:- mode t(in, in) is semidet.
t(X, Y) :-
e(X, Y).
t(f(X), f(Y)) :-
q(f(X), f(Y)),
t(X, Y).
:- pred e(foo, foo).
:- mode e(in, in) is semidet.
e(a, b).
New File: tests/term/vangelder.trans_opt_exp
===================================================================
:- module vangelder.
:- pragma termination_info(vangelder:q(mercury_builtin:in, mercury_builtin:in), finite(0, [no, no]), can_loop).
More information about the developers
mailing list