plspec_test

atom_member(X, [X|_]) :- !.

atom_member(X, [_|T]) :-
    atom_member(X, T).

bar(A) :-
    my_tuple_with_incorrect_spec(A).

bind_to_zero(0).

if_atom_then_my_atomic(X) :-
    (atom(X) -> my_atomic(X)).

if_my_atomic_then_atom(X) :-
    (my_atomic(X) -> atom(X)).

invariant_violator(X) :-
    X = [1], X == [2]. % fail in a more sophisticated way

invariant_violator(a).

my_and_test(_).

my_atomic([_|_]) :- !, fail.

my_atomic(_).

my_compound_foo(foo(_)).

my_member(E,[E|_]).

my_member(E,[_|T]) :-
    my_member(E,T).

my_member_int(E,[E|_]).

my_member_int(E,[_|T]) :-
    my_member_int(E,T).

my_member_specific(E,[E|_]) :- !.

my_member_specific(E,[_|T]) :-
    my_member_specific(E,T).

my_or_test(_).

my_tuple_with_incorrect_spec([X, X]).

not_my_atomic(X) :-
    \+ my_atomic(X).

partial_instantiator([_,_]).

partial_instantiator([1,_]).

partial_instantiator([_,2]).

partial_instantiator([_,a]).

test(empty_is_atomic) :- % this works, because empty and 1 are both atomic.
    \+ my_member_specific(empty, [1,2,3]).

test(tree_in_tree_out) :-
    my_member_specific(empty, [empty, node(empty, 1, empty)]),
    my_member_specific(node(empty, 1, empty), [node(empty, 1, empty), node(empty, 2, empty)]),
    \+ my_member_specific(node(empty, 1, node(empty, 2, empty)), [node(empty, 1, empty), node(empty, 2, empty)]).

test(conform) :-
    my_tuple_with_incorrect_spec([a, a]).

test(conform) :-
    my_atomic([]).

test(conform2) :-
    \+ my_atomic([foo]).

test(conform3) :-
    my_atomic(foo).

test(conform4) :-
    my_atomic(2).

test(conform) :-
    my_or_test(foo).

test(conform) :-
    my_and_test(foo).

test(conform) :-
    invariant_violator(a).

test(conform2) :-
    \+ invariant_violator(b).

test(empty_is_tree) :-
    valid(tree(int), empty).

test(tree1) :-
    valid(tree(int), node(empty, 1, empty)).

test(tree2) :-
    valid(tree(int), node(node(empty, 1, empty),
    2,
    node(empty, 3, empty))).

test(tree3) :-
    \+ valid(tree(int), node(node(empty, 1, empty),
    a,
    node(empty, 3, empty))).

test(tree3) :-
    \+ valid(tree(int), node(node(empty, 1, emppty),
    1,
    node(empty, 3, empty))).

test(ints_are_okay) :-
    this_pred_has_an_extern_spec(1).

test(valid_my_member_int, [nondet]) :-
    my_member_int(1,[1,2,3]),
    \+ my_member_int(1,[4,5]).

test(invalid_my_member_int, [throws(_)]) :-
    my_member_int(a,[1,2,3]).

test(valid_my_member_specific, [nondet]) :-
    my_member_specific(1,[1,2,3]),
    \+ my_member_specific(a,[b,c]).

test(tree_no_int, [throws(_)]) :-
    my_member_specific(node(empty, 1, empty), [1,2,3]).

test(tree_no_atom, [throws(_)]) :-
    my_member_specific(node(node(empty, a, empty), b, empty), [these, are, atoms]).

test(instantiated_call, [nondet]) :-
    my_member(a, [a, b, c]).

test(partly_instantiated, [nondet]) :-
    my_member(_, [a, b, c]).

test(partly_instantiated_not_conform, [nondet, throws(_)]) :-
    % second argument is not a list
    my_member(a, _).

test(partly_instantiated3, [nondet]) :-
    my_member(c, [a, _, c]).

test(all_variables_not_conform, [nondet, throws(_)]) :-
    my_member(_, _).

test(not_conform, [throws(_)]) :-
    my_member([], a).

test(nonconform_call, [throws(_)]) :-
    my_compound_foo(foo(_)).

test(conform_call1, [nondet]) :-
    my_compound_foo(foo(1)).

test(conform_call2, [nondet]) :-
    my_compound_foo(foo(bar)).

test(not_conform, [throws(_)]) :-
    my_compound_foo(bar(_)).

test(conform_var, [throws(_)]) :-
    my_tuple_with_incorrect_spec([a, _]).

test(conform_var2, [throws(_)]) :-
    my_tuple_with_incorrect_spec([_, a]).

test(nonconform_both_var, [throws(_)]) :-
    my_tuple_with_incorrect_spec([_, _]).

test(conform, [nondet]) :-
    atom_member(a, [a,b,c]).

test(not_conform, [throws(_)]) :-
    atom_member(a, X), !,
    X = [a,b,c].

test(not_conform2, [throws(_)]) :-
    atom_member(a, [a,_|_]).

test(not_conform3, [throws(_)]) :-
    atom_member(a, [1,_|_]).

test(not_conform1, [throws(_)]) :-
    my_atomic(foo(_)).

test(not_conform2, [throws(_)]) :-
    \+ my_atomic([_]).

test(not_conform3, [throws(_)]) :-
    my_atomic([[2]]).

test(not_conform4, [throws(_)]) :-
    \+ my_atomic([_]).

test(nonconform, [throws(_)]) :-
    my_or_test(_).

test(nonconform, [throws(_)]) :-
    my_and_test([1]).

test(nonconform2, [throws(_)]) :-
    my_and_test(_).

test(nonconform, [throws(_)]) :-
    invariant_violator(_).

test(conform, [nondet]) :-
    partial_instantiator([_,_]).

test(conform2, [nondet]) :-
    partial_instantiator([X, _]), X == 1.

test(conform3, [nondet]) :-
    partial_instantiator([_, 2]).

test(conform4, [nondet]) :-
    partial_instantiator([1, 2]).

test(nonconform, [throws(_)]) :-
    partial_instantiator([a, 2]).

test(nonconform2, [throws(_)]) :-
    findall(A, partial_instantiator(A), _).

test(postcondition_violated, [throws(_)]) :-
    bind_to_zero(_).

test(atoms_are_not, [throws(_)]) :-
    this_pred_has_an_extern_spec(a).

this_pred_has_an_extern_spec(_).