for review: new tests/tabling directory

[Zoltan Somogyi]

Tyson, please review this. DJ, this has the code of boyer.m, the test case
we discussed.

tests/Mmakefile:
	Add the new tabling directory to the list of directories.

tests/tabling/Mmakefile:
tests/tabling/runtests:
	The intrastructure of the new tests directory.

tests/tabling/fib.{m,exp}:
	A test of the memoing of a det procedure.

tests/tabling/tc_loop.{m,exp}:
	A test of loop checking for a nondet procedure.

tests/tabling/tc_minimal.{m,exp}:
	A test of minimal model tabling for a nondet procedure.
	(Doesn't work yet).

tests/tabling/boyer.{m,exp}:
	A benchmark program, translated to Mercury by Bart Demoen
	from an original in Prolog.
	(Doesn't work yet).

Zoltan.

cvs diff: Diffing .
Index: Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/Mmakefile,v
retrieving revision 1.2
diff -u -u -r1.2 Mmakefile
--- Mmakefile	1997/12/22 09:57:39	1.2
+++ Mmakefile	1998/08/13 02:23:29
@@ -1,4 +1,4 @@
-SUBDIRS = benchmarks general hard_coded invalid misc_tests term valid warnings
+SUBDIRS = benchmarks general hard_coded invalid misc_tests tabling term valid warnings
 NUPROLOG_SUBDIRS = benchmarks general
 
 main_target: check
cvs diff: Diffing benchmarks
cvs diff: Diffing debugger
cvs diff: Diffing general
cvs diff: Diffing hard_coded
cvs diff: Diffing hard_coded/typeclasses
cvs diff: Diffing invalid
cvs diff: Diffing misc_tests
cvs diff: Diffing tabling
Index: tabling/Mmakefile
===================================================================
RCS file: Mmakefile
diff -N Mmakefile
--- /dev/null	Wed May 28 10:49:58 1997
+++ Mmakefile	Thu Aug 13 15:43:13 1998
@@ -0,0 +1,50 @@
+#-----------------------------------------------------------------------------#
+
+main_target: check
+
+include ../Mmake.common
+
+#-----------------------------------------------------------------------------#
+
+PROGS=	\
+	fib \
+	tc_loop
+
+# We don't yet pass the following tests:
+#	boyer \
+#	tc_minimal
+
+#-----------------------------------------------------------------------------#
+
+# at the moment tabling only works with conservative gc
+GRADEFLAGS		=	--gc conservative
+
+# tc_loop is expected to fail, so we need to ignore the exit status
+# (hence the leading `-')
+tc_loop.out: tc_loop
+	-./tc_loop > tc_loop.out 2>&1;
+
+#-----------------------------------------------------------------------------#
+
+DEPS=	$(PROGS:%=%.dep)
+DEPENDS=$(PROGS:%=%.depend)
+OUTS=	$(PROGS:%=%.out)
+RESS=	$(PROGS:%=%.res)
+
+#-----------------------------------------------------------------------------#
+
+MMAKEFLAGS =
+
+dep:	$(DEPS)
+
+depend:	$(DEPENDS)
+
+check:	$(OUTS) $(RESS)
+
+all:	$(PROGS)
+
+clean:
+
+realclean:
+
+#-----------------------------------------------------------------------------#
Index: tabling/boyer.exp
===================================================================
RCS file: boyer.exp
diff -N boyer.exp
--- /dev/null	Wed May 28 10:49:58 1997
+++ boyer.exp	Thu Aug 13 15:45:04 1998
@@ -0,0 +1 @@
+rewriting...proving...done...
Index: tabling/boyer.m
===================================================================
RCS file: boyer.m
diff -N boyer.m
--- /dev/null	Wed May 28 10:49:58 1997
+++ boyer.m	Thu Aug 13 16:47:01 1998
@@ -0,0 +1,325 @@
+% generated: 20 November 1989
+% option(s): 
+%
+%   boyer
+%
+%   Evan Tick (from Lisp version by R. P. Gabriel)
+%
+%   November 1985
+%
+%   prove arithmetic theorem
+
+%	in Mercury by Bart Demoen - started 17 Jan 1997
+
+:- module boyer .
+
+:- interface.
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- import_module int, list.
+
+main --> boyer.
+
+:- pred boyer(io__state::di, io__state::uo) is det .
+
+boyer -->
+	{wff(Wff)} ,
+        io__write_string("rewriting...") ,
+	{ rewrite(Wff,NewWff) } ,
+        io__write_string("proving...") ,
+	({tautology(NewWff,[],[])} ->  io__write_string("done...\n") 
+	; io__write_string("not done ...")
+	) .
+
+:- type type_wff --->
+		(implies(type_wff,type_wff) ;
+		 and(type_wff,type_wff) ;
+		 f(type_wff) ;
+		 plus(type_wff,type_wff) ;
+		 equal(type_wff,type_wff) ;
+		 append(type_wff,type_wff) ;
+		 lessp(type_wff,type_wff) ;
+		 times(type_wff,type_wff) ;
+		 reverse(type_wff) ;
+		 difference(type_wff,type_wff) ;
+		 remainder(type_wff,type_wff) ;
+		 member(type_wff,type_wff) ;
+		 length(type_wff) ;
+		 if(type_wff,type_wff,type_wff) ;
+		 a1 ; b1 ; c1 ; d1 ; t1 ; f1 ; x1 ; y1 ; zero ; []
+		) .
+
+:- pred wff(type_wff) .
+:- mode wff(out) is det .
+
+wff(implies(and(implies(X,Y),
+                and(implies(Y,Z),
+                    and(implies(Z,U),
+                        implies(U,W)))),
+            implies(X,W))) :-
+        X = f(plus(plus(a1,b1),plus(c1,zero))),
+        Y = f(times(times(a1,b1),plus(c1,d1))),
+        Z = f(reverse(append(append(a1,b1),[]))),
+        U = equal(plus(a1,b1),difference(x1,y1)),
+        W = lessp(remainder(a1,b1),member(a1,length(b1))).
+
+:- pred tautology(type_wff,list(type_wff),list(type_wff)) .
+:- mode tautology(in,in,in) is semidet .
+
+tautology(Wff,Tlist,Flist) :-
+        (truep(Wff,Tlist) -> true
+        ;falsep(Wff,Flist) -> fail
+        ;Wff = if(If,Then,Else) ->
+		(truep(If,Tlist) -> tautology(Then,Tlist,Flist)
+		;falsep(If,Flist) -> tautology(Else,Tlist,Flist)
+		;tautology(Then,[If|Tlist],Flist), tautology(Else,Tlist,[If|Flist])
+                )
+	; fail
+        ).
+
+:- pragma memo(rewrite/2).
+
+:- pred rewrite(type_wff,type_wff) .
+:- mode rewrite(in,out) is det .
+
+rewrite(a1,a1) .
+rewrite(b1,b1) .
+rewrite(c1,c1) .
+rewrite(d1,d1) .
+rewrite(f1,f1) .
+rewrite(t1,t1) .
+rewrite(x1,x1) .
+rewrite(y1,y1) .
+rewrite(zero,zero) .
+rewrite([],[]) .
+
+rewrite(lessp(X1,X2),New) :-
+	rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = lessp(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(member(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = member(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(remainder(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = remainder(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(plus(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = plus(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(and(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = and(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(equal(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = equal(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(difference(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = difference(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(append(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = append(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(times(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = times(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(implies(X1,X2),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) ,
+	Mid = implies(Y1,Y2) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(length(X1),New) :-
+        rewrite(X1,Y1) ,
+	Mid = length(Y1) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(f(X1),New) :-
+        rewrite(X1,Y1) ,
+	Mid = f(Y1) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(reverse(X1),New) :-
+        rewrite(X1,Y1) ,
+	Mid = reverse(Y1) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+rewrite(if(X1,X2,X3),New) :-
+        rewrite(X1,Y1) , rewrite(X2,Y2) , rewrite(X3,Y3) ,
+	Mid = if(Y1,Y2,Y3) ,
+	(equal(Mid,Next) -> rewrite(Next,New)
+	;
+	 New = Mid
+	) .
+
+:- pred rewrite_args(list(type_wff),list(type_wff)) .
+:- mode rewrite_args(in,out) is det .
+
+rewrite_args([],[]) .
+rewrite_args([A|RA],[B|RB]) :- 
+        rewrite(A,B),
+        rewrite_args(RA,RB).
+
+:- pred truep(type_wff,list(type_wff)) .
+:- mode truep(in,in) is semidet .
+
+truep(Wff,List) :- Wff = t1 -> true ; member_chk(Wff,List) .
+
+:- pred falsep(type_wff,list(type_wff)) .
+:- mode falsep(in,in) is semidet .
+
+falsep(Wff,List) :- Wff = f1 -> true ; member_chk(Wff,List) .
+
+:- pred member_chk(type_wff,list(type_wff)) .
+:- mode member_chk(in,in) is semidet .
+
+member_chk(X,[Y|T]) :- X = Y -> true ; member_chk(X,T).
+
+:- pred equal(type_wff,type_wff) .
+:- mode equal(in,out) is semidet .
+
+equal(  and(P,Q),
+        if(P,if(Q,t1,f1),f1)
+        ).
+equal(  append(append(X,Y),Z),
+        append(X,append(Y,Z))
+        ).
+equal(  difference(A,B),
+        C
+        ) :- difference(A,B,C).
+equal(  equal(A,B),
+        C
+        ) :- eq(A,B,C).
+equal(  if(if(A,B,C),D,E),
+        if(A,if(B,D,E),if(C,D,E))
+        ).
+equal(  implies(P,Q),
+        if(P,if(Q,t1,f1),t1)
+        ).
+equal(  length(A),
+        B
+        ) :- mylength(A,B).
+equal(  lessp(A,B),
+        C
+        ) :- lessp(A,B,C).
+equal(  plus(A,B),
+        C
+        ) :- plus(A,B,C).
+equal(  remainder(A,B),
+        C
+        ) :- remainder(A,B,C).
+equal(  reverse(append(A,B)),
+        append(reverse(B),reverse(A))
+        ).
+
+:- pred difference(type_wff,type_wff,type_wff) .
+:- mode difference(in,in,out) is semidet .
+
+difference(X,Y,Z) :-
+		(X = Y -> Z = zero
+		;
+		 (X = plus(A,B), Y = plus(A,C) -> Z = difference(B,C)
+		 ;
+		  X = plus(B,plus(Y,C)) -> Z = plus(B,C) ; fail
+		 )
+		) .
+
+:- pred eq(type_wff,type_wff,type_wff) .
+:- mode eq(in,in,out) is semidet .
+
+eq(append(A,B), append(A,C), equal(B,C)) .
+eq(lessp(X,Y), Z, if(lessp(X,Y),
+                     equal(t1,Z),
+                     equal(f1,Z))).
+
+:- pred mylength(type_wff,type_wff) .
+:- mode mylength(in,out) is semidet .
+
+mylength(reverse(X),length(X)).
+
+:- pred lessp(type_wff,type_wff,type_wff) .
+:- mode lessp(in,in,out) is semidet .
+
+lessp(plus(X,Y), plus(X,Z), lessp(Y,Z)) :- !.
+
+:- pred plus(type_wff,type_wff,type_wff) .
+:- mode plus(in,in,out) is semidet .
+
+plus(plus(X,Y),Z,
+     plus(X,plus(Y,Z))).
+
+:- pred remainder(type_wff,type_wff,type_wff) .
+:- mode remainder(in,in,out) is semidet .
+
+remainder(U,V,zero) :-
+		(U = V -> true ;
+		 U = times(A,B) , (B = V -> true ; A = V)
+		) .
+
+:- pred times(type_wff,type_wff,type_wff) .
+:- mode times(in,in,out) is semidet .
+
+times(A,B,C) :-
+		(B = plus(Y,Z) -> C = plus(times(A,Y),times(A,Z))
+		;
+		 A = times(X,Y) -> C = times(X,times(Y,B))
+		;
+		 B = difference(CC,W) , C = difference(times(CC,A),times(W,A))
+		) .
Index: tabling/fib.exp
===================================================================
RCS file: fib.exp
diff -N fib.exp
--- /dev/null	Wed May 28 10:49:58 1997
+++ fib.exp	Thu Aug 13 16:44:02 1998
@@ -0,0 +1 @@
+tabling works
Index: tabling/fib.m
===================================================================
RCS file: fib.m
diff -N fib.m
--- /dev/null	Wed May 28 10:49:58 1997
+++ fib.m	Thu Aug 13 16:42:12 1998
@@ -0,0 +1,72 @@
+:- module fib.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is cc_multi.
+
+:- implementation.
+
+:- import_module benchmarking, require, int.
+
+main -->
+	perform_trials(10).
+
+:- pred perform_trials(int::in, io__state::di, io__state::uo) is cc_multi.
+
+perform_trials(N) -->
+	{ trial(N, Time, MTime) },
+	% io__write_int(Time),
+	% io__write_string(" "),
+	% io__write_int(MTime),
+	% io__write_string(" \n"),
+	(
+		{
+			Time > 10 * MTime,
+			MTime > 0	% untabled takes ten times as long
+		;
+			Time > 100,	% untabled takes at least 100 ms
+			MTime < 1	% while untabled takes at most 1 ms
+		}
+	->
+		io__write_string("tabling works\n")
+	;
+		{ Time > 10000 }	% Untabled takes at least 10 seconds
+	->
+		io__write_string("tabling does not appear to work\n")
+	;
+		% We couldn't get a measurable result with N,
+		% and it looks like we can afford a bigger trial
+		perform_trials(N+3)
+	).
+
+:- pred trial(int::in, int::out, int::out) is cc_multi.
+
+trial(N, Time, MTime) :-
+	benchmark_det(fib, N, Res, 1, Time),
+	benchmark_det(mfib, N, MRes, 1, MTime),
+	require(unify(Res, MRes), "tabling produces wrong answer").
+
+:- pred fib(int::in, int::out) is det.
+
+fib(N, F) :-
+	( N < 2 ->
+		F = 1
+	;
+		fib(N - 1, F1),
+		fib(N - 2, F2),
+		F is F1 + F2
+	).
+
+:- pred mfib(int::in, int::out) is det.
+:- pragma memo(mfib/2).
+
+mfib(N, F) :-
+	( N < 2 ->
+		F = 1
+	;
+		mfib(N - 1, F1),
+		mfib(N - 2, F2),
+		F is F1 + F2
+	).
Index: tabling/runtests
===================================================================
RCS file: runtests
diff -N runtests
--- /dev/null	Wed May 28 10:49:58 1997
+++ runtests	Thu Aug 13 15:04:41 1998
@@ -0,0 +1,27 @@
+#!/bin/sh
+# Test whether the code generated by the Mercury compiler
+# is producing the expected output.
+# Return a status of 0 (true) if everything is all right, and 1 otherwise.
+
+. ../handle_options
+. ../startup
+
+mmake $jfactor depend || exit 1
+eval mmake -k $jfactor $gradeopt $flagsopt $cflagsopt check
+checkstatus=$?
+
+cat *.res > .allres
+if test ! -s .allres -a "$checkstatus" = 0
+then
+	echo "the tests in the hard_coded directory succeeded"
+	echo "gradeopt=$gradeopt, flagsopt=$flagsopt, cflagsopt=$cflagsopt"
+	rm -f .allres
+	. ../shutdown
+	exit 0
+else
+	echo "the tests in the hard_coded directory failed"
+	echo "gradeopt=$gradeopt, flagsopt=$flagsopt, cflagsopt=$cflagsopt"
+	echo "the differences are:"
+	cat .allres
+	exit 1
+fi
Index: tabling/tc_loop.exp
===================================================================
RCS file: tc_loop.exp
diff -N tc_loop.exp
--- /dev/null	Wed May 28 10:49:58 1997
+++ tc_loop.exp	Fri Aug 14 10:21:19 1998
@@ -0,0 +1,2 @@
+Software error: detected infinite recursion in pred tc_loop:tc/2
+Stack dump not available in this grade.
Index: tabling/tc_loop.m
===================================================================
RCS file: tc_loop.m
diff -N tc_loop.m
--- /dev/null	Wed May 28 10:49:58 1997
+++ tc_loop.m	Thu Aug 13 15:18:24 1998
@@ -0,0 +1,37 @@
+:- module tc_loop.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- import_module std_util, list.
+
+main -->
+	{ solutions(tc(1), Solns) },
+	( { Solns = [] } ->
+		io__write_string("loopcheck failed, tc has no solutions\n")
+	;
+		io__write_string("loopcheck failed, tc has solutions\n")
+	).
+
+:- pred tc(int::in, int::out) is nondet.
+:- pragma loop_check(tc/2).
+
+tc(A, B) :-
+	(
+		edge(A, B)
+	;
+		edge(A, C),
+		tc(C, B)
+	).
+
+:- pred edge(int::in, int::out) is nondet.
+
+edge(1, 2).
+edge(1, 3).
+edge(2, 1).
+edge(3, 4).
Index: tabling/tc_minimal.exp
===================================================================
RCS file: tc_minimal.exp
diff -N tc_minimal.exp
--- /dev/null	Wed May 28 10:49:58 1997
+++ tc_minimal.exp	Thu Aug 13 15:43:33 1998
@@ -0,0 +1 @@
+[1, 2, 3, 4]
Index: tabling/tc_minimal.m
===================================================================
RCS file: tc_minimal.m
diff -N tc_minimal.m
--- /dev/null	Wed May 28 10:49:58 1997
+++ tc_minimal.m	Thu Aug 13 15:38:38 1998
@@ -0,0 +1,34 @@
+:- module tc_minimal.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- import_module std_util, list.
+
+main -->
+	{ solutions(tc(1), Solns) },
+	io__write(Solns),
+	io__write_string("\n").
+
+:- pred tc(int::in, int::out) is nondet.
+:- pragma minimal_model(tc/2).
+
+tc(A, B) :-
+	edge(A, C),
+	(
+		B = C
+	;
+		tc(C, B)
+	).
+
+:- pred edge(int::in, int::out) is nondet.
+
+edge(1, 2).
+edge(1, 3).
+edge(2, 1).
+edge(3, 4).
cvs diff: Diffing term
cvs diff: Diffing valid
cvs diff: Diffing warnings