% module:   peano_unit_tests.pl
% date:     November 17, 2005
% author:   unit_test_case_generator

% copyright (c) 2005, Cotillion Group, Inc.  All rights reserved.

% synopsis: Unit test cases for exported predicates in peano

:- module(peano_unit_tests, [
        unit_test_case_suite_brief/2,
        unit_test_case_suite/2,
        tautology/4,
        what_unit_tests/1
]).

% modified: November 18, 2005, Douglas M. Auclair (DMA)
% changed:  Now that peano/2 is properly constrained, added test cases
%           to cover two unbound arguments (both for a single solution
% 			and for multiple returns).  Added unit tests to insure
%			integrity of values returned.

:- use_module(library(unit_test_utils), [
        extract_names_from/3,
        add_to_successes/3,
        add_to_failures/3
]).

:- use_module(library(peano), [increment/2, peano/2]).
:- use_module(library(syntax), [(~)/1, (=>)/2, (<=>)/2]).

:- op(900,   fy, ~).
:- op(920,  xfy,  =>).
:- op(920,  xfy, <=>).

unit_test_case_suite_brief(Briefs, Failures) :-
%    Gives only the names (and not other information) on the tests that 
%    succeeded; failures reported with other information included. 
  unit_test_case_suite(Successes, Failures),
  extract_names_from(Successes, Briefs, []).

unit_test_case_suite(Successes, Failures) :-
%    Runs all the unit test cases and reports on successes and failures 
  what_unit_tests(tautologies(TestSets)),
  test_each_set(TestSets, tests_complete([], []),
                          tests_complete(Successes, Failures)).

what_unit_tests(tautologies([
        test_set(peano/2,
                 [nominal(to_peano(0)), nominal(to_peano(5)),
		  		  nominal(to_integral(zero)),
		  		  nominal(to_integral(s(s(s(zero))))),
				  nominal(a_solution(both_free, _, _)),
				  nominal(a_solution(both_free, _, s(_))),
				  nominal(a_solution(both_ground, 3, s(s(s(zero))))),
				  nominal(multiple_solutions(both_free, _, _)),
				  nominal(multiple_solutions(both_free, _, s(_))),
				  nominal(not_equal(both_ground(2, 4))),
				  nominal(not_equal(out(_, 7))),
				  nominal(equal(both_ground(1, 1))),
				  nominal(equal(both_free(_, _))),
				  nominal(equal(out(_, 6))),
				  nominal(multi_equal(both_free(_, _))),
				  extrinsic(not_equal(both_ground(5, 5)),
						    reason(peano_numerals_for_the_same_integer_are_the_same)),
				  extrinsic(equal(both_ground(5, 6)),
						    reason(peano_numerals_for_different_integers_cannot_be_equal)),
				  extrinsic(equal(both_free(X, s(X))),
						    reason(a_peano_numeral_cannot_be_its_own_successor)),
		  		  extrinsic(to_peano(-1),
		            		reason(no_negative_peano_representation)),
		  		  extrinsic(to_peano(5.3),
		            		reason(no_fractional_peano_representation)),
		  		  extrinsic(to_integral(foobar),
		            		reason(not_a_peano_numeral)),
				  extrinsic(a_solution(both_ground, 0, s(zero)),
		            		reason(unequal_numerals_have_no_solution)),
				  extrinsic(multiple_solutions(both_ground, 0, zero),
		            		reason(only_one_solution_for_equal_bound_arguments)),
				  extrinsic(multiple_solutions(both_ground, 2, s(s(zero))),
		            		reason(only_one_solution_for_equivalent_and_bound_arguments)),
				  extrinsic(multiple_solutions(out_free, 9, _),
		            		reason(exactly_one_peano_numeral_represents_an_integral)),
				  extrinsic(multiple_solutions(out_free, 0, _),
		            		reason(exactly_one_peano_numeral_represents_an_integral)),
				  extrinsic(multiple_solutions(in_free, _, zero),
		            		reason(exactly_one_integral_equivalent_to_one_peano_numeral))]),
        test_set(increment/2,
	             [nominal(in(zero)), nominal(in(s(s(zero)))),
		  		  nominal(out(s(zero))),
		  		  nominal(out(s(s(s(s(zero)))))),
				  nominal(a_solution(both_free, _, _)),
				  nominal(a_solution(both_free, _, s(_))),
				  nominal(a_solution(both_ground, zero, s(zero))),
		    	  extrinsic(out(zero), reason(cannot_decrement_from_zero)),
				  extrinsic(a_solution(both_free, X, s(s(X))),
							reason(successor_applied_once_only_a_single_increment)),
				  extrinsic(a_solution(both_ground, zero, s(s(zero))),
							reason(successor_applied_once_only_a_single_increment)),
				  extrinsic(a_solution(both_free, X, X),
							reason(a_peano_numeral_cannot_be_its_own_successor)),
				  extrinsic(a_solution(both_ground, zero, zero),
							reason(a_peano_numeral_cannot_be_its_own_successor)),
				  extrinsic(a_solution(both_ground, s(s(zero)), s(s(zero))),
							reason(a_peano_numeral_cannot_be_its_own_successor)),
				  extrinsic(multiple_solutions(_, _),
							reason(increment_is_deterministic))])])).
%    Indicates what unit tests cases are available for this module and 
%    the expected pass/fail-for-reason result for each unit test. 

% ------------------------------------------------------------------------
% peano/2 unit test cases

tautology(peano/2, nominal(to_peano(Integral)), Peano, Peano) :-
%    Tests converting an integral into a peano numeral
  peano(Integral, Peano),
  peano_numeral(Peano).

tautology(peano/2, nominal(to_integral(Peano)), Integral, Integral) :-
%    Tests converting a peano numeral into an integral
  peano(Integral, Peano),
  integer(Integral),
  ~(Integral < 0).

tautology(peano/2, nominal(a_solution(_Type, A, B)), Pair, Pair) :-
%    Tests that we can obtain a pair of bindings for unbound inputs
  peano(A, B),
  integer(A),
  peano_numeral(B),
  Pair = equivalent_numerals(A, B).

tautology(peano/2, nominal(multiple_solutions(both_free, A, B)), Pairs, Pairs) :-
%    Tests that we can obtain multiple pairs of bindings for unbound inputs
  peano(A, B),
  peano(C, D),
  integer(A),
  integer(C),
  ~(C = A),
  peano_numeral(B),
  peano_numeral(D),
  Pairs = pairs(equivalent_numerals(A, B), equivalent_numerals(C, D)).

tautology(peano/2, nominal(equal(both_ground(A, B))), Pair, Pair) :-
%    Ensure peano numerals for the same integral are the same
  A = B,
  peano(A, C),
  peano(B, C),
  Pair = pairs(equivalent_numerals(A, C), equivalent_numerals(B, C)).

tautology(peano/2, nominal(equal(both_free(A, B))), Pair, Pair) :-
%    There exists an integral that has an equivalent peano representation
  peano(A, C),
  peano(B, D),
  C = D,
  Pair = pairs(equivalent_numerals(A, C), equivalent_numerals(B, D)).

tautology(peano/2, nominal(equal(out(A, B))), Pair, Pair) :-
%    There exists an integral that has an equivalent peano representation
%    that can be converted back into the (equivalent) integral.
  peano(A, C),
  peano(B, D),
  C = D,
  A = B,
  Pair = pairs(equivalent_numerals(A, C), equivalent_numerals(B, D)).

tautology(peano/2, nominal(multi_equal(both_free(A, B))), Pair, Pair) :-
%    There exists multiple numbers with corresponding peano equivalents
  peano(A, C),
  peano(B, D),
  ~(A = B),
  Pair = pairs(equivalent_numerals(A, C), equivalent_numerals(B, D)).

tautology(peano/2, nominal(not_equal(both_ground(A, B))), Pair, Pair) :-
%    Ensure peano numerals for different integrals are different
  ~(A = B),
  peano(A, C),
  peano(B, D),
  ~(C = D),
  Pair = pairs(equivalent_numerals(A, C), equivalent_numerals(B, D)).

tautology(peano/2, nominal(not_equal(out(A, B))), Pair, Pair) :-
%    There exists an integral with a different peano representation
%    than the given integral's peano representation
  peano(A, C),
  peano(B, D),
  ~(C = D),
  ~(A = B),
  Pair = pairs(equivalent_numerals(A, C), equivalent_numerals(B, D)).

tautology(peano/2, extrinsic(to_peano(Number), _), a_peano_numeral, failure) :-
%    Test negative or non-integral (bound) numbers
  (integer(Number), Number >= 0; Number = '_|_') <=> peano(Number, _Arg1).

tautology(peano/2, extrinsic(to_integral(NonPeano), _), an_integral, failure) :-
%    try to convert a non-peano-numeral
  peano_numeral(NonPeano) <=> peano(_Number, NonPeano).

tautology(peano/2, extrinsic(not_equal(both_ground(A, B)), _),
	      two_distinct_peano_numerals, failure) :-
%    tries to obtain two different peano numerals for the same number
  (A = B, peano(A, P0), peano(B, P1)) <=> P0 = P1.

tautology(peano/2, extrinsic(equal(both_ground(A, B)), _),
	 	  one_peano_numeral_representing_two_unequal_integrals, failure) :-
%    there is no peano numeral equal to two different integrals
  (~ A = B, peano(A, P0), peano(B, P1)) <=> ~ P0 = P1.

tautology(peano/2, extrinsic(equal(both_free(A, s(A))), _),
	      one_integral_for_two_distinct_peano_numerals, failure) :-
%    There is no single integral that represents a peano numeral and
%    its immediate successor.  We do not prove this inductively...
  peano(X, A),
  peano(Y, s(A)),
  ~(X = Y).

tautology(peano/2, extrinsic(a_solution(both_ground, Int, Peano), _),
	      unification_of_peano_numeral_and_different_integral, failure) :-
%    there are no solutions to an attempt to unify a peano numeral with
%    a integral that doesn't have the same representation
  ~ peano(Int, Peano).

tautology(peano/2, extrinsic(multiple_solutions(both_ground, Int, Peano), _),
	      different_solution_sets_for_ground_arguments, failure) :-
%    peano/2 is (semi-)deterministic for ground arguments
  peano(Int, P0),
  peano(I0, Peano),
  (I0 = Int <=> P0 = Peano).

tautology(peano/2, extrinsic(multiple_solutions(out_free, Int, Peano), _),
	      different_peano_numerals_for_same_integral, failure) :-
%    peano/2 is (semi-)deterministic for ground arguments
  (peano(Int, P0), peano(Int, Peano) => P0 = Peano).

tautology(peano/2, extrinsic(multiple_solutions(in_free, Int, Peano), _),
	      different_peano_numerals_for_same_integral, failure) :-
%    'in_free' as in 'olley, olley, in free!'
  (peano(Int, Peano), peano(I0, Peano) => I0 = Int).

% ------------------------------------------------------------------------
% increment/2 unit test cases

tautology(increment/2, nominal(in(Peano)), Actual, Actual) :-
%    Ensures Peano is incremented by s/1 to Actual
  increment(Peano, Actual),
  Actual = s(Peano).

tautology(increment/2, nominal(out(Peano)), Actual, Actual) :-
%    Ensures Peano is /decremented/ by s/1 to Actual
  increment(Actual, Peano),
  Peano = s(Actual).

tautology(increment/2, nominal(a_solution(_Type, A, B)), Actual, Actual) :-
%    Sees if it is possible to obtain a solution given no information
  increment(A, B),
  B = s(A),
  Actual = numerals(A, incremented_to(B)).

tautology(increment/2, extrinsic(out(zero), _Reason), negative(s(zero)), failure) :-
%    Tests that we cannot decrement from zero
  ~ increment(_Integral, zero).

tautology(increment/2, extrinsic(a_solution(_Type, A, B), _),
          successor(A, B), failure) :-
%    We cannot prove increment(A, B) if ~ s(A) = B.
  increment(A, C),
  ~ C = B.

tautology(increment/2, extrinsic(multiple_solutions(A, B), _Reason),
		  different_bindings, failure) :-
%    We attempt to obtain multiple solutions from increment/2, but this
%    predicate is (semi-)deterministic
  (increment(A, B), increment(A, C) <=> B = C).

% ------------------------------------------------------------------------
% INTERNAL IMPLEMENTATION PREDICATES

% test_each_set/3 breaks the unit tests down by predicate

test_each_set([]) --> [].
test_each_set([test_set(Pred, Tests)|Sets]) -->
  test_each_case(Pred, Tests),
  test_each_set(Sets).

% test_each_case/4 runs a unit test and records the result
% (pass/fail) by putting it in an appropriate result list.

test_each_case(_, []) --> [].
test_each_case(Pred, [Test|Tests]) -->
  ({ tautology(Pred, Test, Expected, Actual) } ->
     add_to_successes(test_result(Pred, Test, Expected, Actual))
   ;
     add_to_failures(test_result(Pred, Test, _, failure))),
  test_each_case(Pred, Tests).

peano_numeral(s(Peano)) :- peano_numeral(Peano).
peano_numeral(zero).