Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % (SWI-Prolog) :- use_module(library(plunit)). :- use_module(library(lists)). :- reexport(peano_ari). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :-meta_predicate calln_(+, 1, +, +). calln_(K, G, N, F) :- flag(K, _, 1), call(G, R), flag(K, I, I + 1), nb_setarg(I, F, R), I == N, !. non_nat_(X) :- member(X, [1, '', {}, [1, []], [[1]], [{_}]]). any_nat_(X) :- member(X, [[], [[]], _, [_]]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- begin_tests(nat). test('nat(+non_nat) throws', [ forall(non_nat_(N)), throws(error(type_error(nat_part, N), _)) ]) :- nat(N). test('nat(+nat) true', [ forall(member(N, [[], [[]], [[[]]], [[[[]]]]])), true ]) :- nat(N). test('nat(-nat) multi', [ forall(member(N, [_, [_], [[_]], [[[_]]]])), nondet ]) :- nat(N). test('nat(-nat) sequence', [ true(Ns == ns([], [[]], [[[]]], [[[[]]]])) ]) :- Ns = ns(_, _, _, _), calln_('nat(-nat) sequence', nat, 4, Ns). :- end_tests(nat). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- begin_tests(nat_zero). test('nat_zero(+non_nat) throws', [ forall(non_nat_(N)), throws(error(type_error(nat_part, N), _)) ]) :- nat_zero(N). test('nat_zero(+nat) fail', [ forall(member(N, [[[]], [[[]]], [_], [[_]]])), fail ]) :- nat_zero(N). test('nat_zero(+nat) true', [ forall(N = []), true ]) :- nat_zero(N). test('nat_zero(-nat) true', [ true(N == []) ]) :- nat_zero(N). :- end_tests(nat_zero). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- begin_tests(nat_lte). test('nat_lte(+non_nat, ?nat) throws', [ forall((non_nat_(N0), any_nat_(N))), throws(error(type_error(nat_part, N0), _)) ]) :- nat_lte(N0, N). test('nat_lte(?nat, +non_nat) throws', [ forall((any_nat_(N0), non_nat_(N))), throws(error(type_error(nat_part, N), _)) ]) :- nat_lte(N0, N). test('nat_lte(+nat, +nat) fail', [ forall((N0 = [[[]]], member(N, [[], [[]]]))), fail ]) :- nat_lte(N0, N). test('nat_lte(+nat, +nat) true', [ forall((N = [[[]]], member(N0, [[], [[]], [[[]]]]))), true ]) :- nat_lte(N0, N). test('nat_lte(+nat, -nat) nondet', [ forall(member(N0, [[], [[]], [[[[]]]]])), nondet ]) :- nat_lte(N0, _). test('nat_lte(-nat, +nat) nondet', [ forall(member(N, [[], [[]], [[[[]]]]])), nondet ]) :- nat_lte(_, N). test('nat_lte(-nat, -nat) nondet', [ nondet ]) :- nat_lte(_, _). :- end_tests(nat_lte). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- begin_tests(nat_succ). test('nat_succ(+non_nat, ?nat) throws', [ forall((non_nat_(N0), any_nat_(N))), throws(error(type_error(nat_part, N0), _)) ]) :- nat_succ(N0, N). test('nat_succ(?nat, +non_nat) throws', [ forall((any_nat_(N0), non_nat_(N))), throws(error(type_error(nat_part, N), _)) ]) :- nat_succ(N0, N). test('nat_succ(+nat, +nat) fail', [ forall((member(N0, [[], [[]], [[[[]]]]]), member(N, [N0, [[N0]]]))), fail ]) :- nat_succ(N0, N). test('nat_succ(+nat, +nat) true', [ forall((member(N0, [[], [[]], [[[[]]]]]), N = [N0])), true ]) :- nat_succ(N0, N). test('nat_succ(+nat, -nat) true', [ forall((member(N0, [[], [[]], [[[[]]]]]), N = [N0])), true(X == N) ]) :- nat_succ(N0, X). test('nat_succ(-nat, +nat) true', [ forall((member(N0, [[], [[]], [[[[]]]]]), N = [N0])), true(X == N0) ]) :- nat_succ(X, N). test('nat_succ(-nat, -nat) nondet', [ nondet ]) :- nat_succ(_, _). :- end_tests(nat_succ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- begin_tests(nat_add). test('nat_add(+non_nat, ?nat, ?nat) throws', [ forall((non_nat_(N1), any_nat_(N2), any_nat_(N))), throws(error(type_error(nat_part, N1), _)) ]) :- nat_add(N1, N2, N). test('nat_add(?nat, +non_nat, ?nat) fail', [ forall((any_nat_(N1), non_nat_(N2), any_nat_(N))), throws(error(type_error(nat_part, N2), _)) ]) :- nat_add(N1, N2, N). test('nat_add(?nat, ?nat, +non_nat) fail', [ forall((any_nat_(N1), any_nat_(N2), non_nat_(N))), throws(error(type_error(nat_part, N), _)) ]) :- nat_add(N1, N2, N). test('nat_add(+nat, +nat, +nat) fail', [ forall((member(N1, [[], [[]], [[[[]]]]]), member(N2, [[[]], [[[[]]]]]), N = [[N1]])), fail ]) :- nat_add(N1, N2, N). test('nat_add(+nat, +nat, +nat) true', [ forall((member(N1, [[], [[]], [[[[]]]]]), N2 = [[[]]], N = [[N1]])), true ]) :- nat_add(N1, N2, N). test('nat_add(+nat, +nat, -nat) true', [ forall((member(N1-N, [[]-[[]], [[]]-[[[]]], [[[[]]]]-[[[[[]]]]]]), N2 = [[]])), true(X == N) ]) :- nat_add(N1, N2, X). test('nat_add(+nat, -nat, +nat) true', [ forall((member(N1-N, [[]-[[]], [[]]-[[[]]], [[[[]]]]-[[[[[]]]]]]), N2 = [[]])), true(X == N2) ]) :- nat_add(N1, X, N). test('nat_add(-nat, +nat, +nat) true', [ forall((member(N1-N, [[]-[[]], [[]]-[[[]]], [[[[]]]]-[[[[[]]]]]]), N2 = [[]])), true(X == N1) ]) :- nat_add(X, N2, N). test('nat_add(+nat, -nat, -nat) nondet', [ forall(member(N, [[], [[]], [[[[]]]]])), nondet ]) :- nat_add(N, _, _). test('nat_add(-nat, +nat, -nat) nondet', [ forall(member(N, [[], [[]], [[[[]]]]])), nondet ]) :- nat_add(_, N, _). test('nat_add(-nat, -nat, +nat) nondet', [ forall(member(N, [[], [[]], [[[[]]]]])), nondet ]) :- nat_add(_, _, N). test('nat_add(-nat, -nat, -nat) nondet', [ nondet ]) :- nat_add(_, _, _). :- end_tests(nat_add). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%