|
| 1 | +:- module(reif_tests, []). |
| 2 | + |
| 3 | +:- use_module(library(reif)). |
| 4 | +:- use_module(library(lists)). |
| 5 | +:- use_module(library(dif)). |
| 6 | +:- use_module(library(lambda)). |
| 7 | +:- use_module(library(random)). |
| 8 | +:- use_module(test_framework). |
| 9 | + |
| 10 | +/* |
| 11 | +Those tests are just sanity checks – examples from the paper, to make sure I |
| 12 | +haven't messed up. |
| 13 | +*/ |
| 14 | +test("indexing dif/2 p6#1", ( |
| 15 | + findall(X-Fs, tfilter(=(X),[1,2,3,2,3,3],Fs), [1-[1], 2-[2,2], 3-[3,3,3], Y-[]]), |
| 16 | + maplist(dif(Y), [1,2,3]) |
| 17 | +)). |
| 18 | +test("indexing dif/2 p6#2", findall(X, duplicate(X,[1,2,3,2,3,3]), [2,3])). |
| 19 | +test("indexing dif/2 p7#1", firstduplicate(1, [1,2,3,1])). |
| 20 | +test("indexing dif/2 p7#2",( |
| 21 | + firstduplicate(X, [1,2,3,1]), |
| 22 | + X == 1 |
| 23 | +)). |
| 24 | +test("indexing dif/2 p7#3", ( |
| 25 | + findall(Y-A-B-C, firstduplicate(Y,[A,B,C]), [X-X-X-_, X-X-B1-X, X-A2-X-X]), |
| 26 | + dif(B1,X), |
| 27 | + dif(A2,X) |
| 28 | +)). |
| 29 | + |
| 30 | +test("doesnt modify free variables", (reif:goal_expanded(A,B), A == B, var(A))). |
| 31 | +test("expands call/1", reif:goal_expanded(call(a), a)). |
| 32 | +test("expands call/1 for modules", reif:goal_expanded(call(a:b(1)), a:b(1))). |
| 33 | +test("expands call/2 for modules", reif:goal_expanded(call(a:b,c), a:b(c))). |
| 34 | +test("doesn't expand call/2", reif:goal_expanded(call(b,c), call(b,c))). |
| 35 | +test("doesn't expand cyclic terms", ( |
| 36 | + X=a(X), |
| 37 | + reif:goal_expanded(call(X), Y), |
| 38 | + call(X) == Y |
| 39 | +)). |
| 40 | +test("doesn't expand cyclic call/1", ( |
| 41 | + X=call(X), |
| 42 | + reif:goal_expanded(X, Y), |
| 43 | + X == Y |
| 44 | +)). |
| 45 | +test("doesn't expand higher order predicates", ( |
| 46 | + X = maplist(=(1), _), |
| 47 | + reif:goal_expanded(X, Y), |
| 48 | + X == Y |
| 49 | +)). |
| 50 | + |
| 51 | +/* |
| 52 | +Following tests capture current results of goal expansion |
| 53 | +TODO: Investigate if if_/3 can be further expanded, and if it will be beneficial |
| 54 | +*/ |
| 55 | +test("goal_expansion (=)", ( |
| 56 | + subsumes_full_expansion(if_(1=2,a,b), ( |
| 57 | + 1 \= 2 -> b |
| 58 | + ; 1 == 2 -> a |
| 59 | + ; 1 = 2, a |
| 60 | + ; dif(1,2), b)))). |
| 61 | + |
| 62 | +test("goal_expansion (;)", ( |
| 63 | + subsumes_full_expansion(if_((1=2;3=3),a,b), ( |
| 64 | + 1 \= 2 -> if_(3=3,a,b) |
| 65 | + ; 1 == 2 -> a |
| 66 | + ; 1 = 2, a |
| 67 | + ; dif(1,2), if_(3=3,a,b))))). |
| 68 | + |
| 69 | +test("goal_expansion (,)", ( |
| 70 | + subsumes_full_expansion(if_((1=2,3=3),a,b), ( |
| 71 | + 1 \= 2 -> b |
| 72 | + ; 1 == 2 -> if_(3=3,a,b) |
| 73 | + ; 1 = 2, if_(3=3,a,b) |
| 74 | + ; dif(1,2), b)))). |
| 75 | + |
| 76 | +test("goal_expansion memberd_t", ( |
| 77 | + subsumes_full_expansion(if_(memberd_t(f,"abcdefgh"),t,f), ( |
| 78 | + call(memberd_t(f,"abcdefgh"),A), |
| 79 | + ( A == true -> t |
| 80 | + ; A == false -> f |
| 81 | + ; nonvar(A) -> throw(error(type_error(boolean,A),_)) |
| 82 | + ; throw(error(instantiation_error,_))))))). |
| 83 | + |
| 84 | +test("goal_expansion cond_t", ( |
| 85 | + subsumes_full_expansion(if_(cond_t(a,b),t,f), ( |
| 86 | + call(cond_t(a,b),A), |
| 87 | + ( A == true -> t |
| 88 | + ; A == false -> f |
| 89 | + ; nonvar(A) -> throw(error(type_error(boolean,A),_)) |
| 90 | + ; throw(error(instantiation_error,_))))))). |
| 91 | + |
| 92 | +test("set of solutions found by tpartition/4 and tfilter/3 is the same and correct", ( |
| 93 | + random_test_vector(TestVector), |
| 94 | + findall((N,Ts), tpartition(=(N),TestVector,Ts,_), S), |
| 95 | + findall((N,Ts), tfilter(=(N),TestVector,Ts), S), |
| 96 | + maplist(_+\(N,Ts)^maplist(=(N),Ts), S) |
| 97 | +)). |
| 98 | + |
| 99 | +test("cut in one of the branches does not influence condition", ( |
| 100 | + findall(X-Y, if_(X=1,!,Y=a), Solutions), |
| 101 | + Expected = [1-Y1,X2-a], |
| 102 | + subsumes_term(Expected, Solutions), |
| 103 | + Solutions = Expected, |
| 104 | + var(Y1), |
| 105 | + var(X2), dif(X2, 1) |
| 106 | +)). |
| 107 | + |
| 108 | +test("non-callable branch throws meaningful error", ( |
| 109 | + findall(R, result_or_exception(if_(_=1, _=a, 2), R), Solutions), |
| 110 | + Solutions == [if_(1=1,a=a,2), error(type_error(callable,2),call/1)] |
| 111 | +)). |
| 112 | + |
| 113 | +result_or_exception(Goal, Result) :- |
| 114 | + catch((Goal,Result=Goal), Result, true). |
| 115 | + |
| 116 | +random_test_vector(TestVector) :- |
| 117 | + random_integer(0, 1000, Length), |
| 118 | + length(TestVector, Length), |
| 119 | + maplist(random_integer(1,5), TestVector). |
| 120 | + |
| 121 | +% Expand goal until fix point is found |
| 122 | +full_expansion(G, X) :- |
| 123 | + user:goal_expansion(G, Gx) -> full_expansion(Gx, X); G = X. |
| 124 | + |
| 125 | +% X is more general than fully expanded goal G |
| 126 | +subsumes_full_expansion(G, X) :- |
| 127 | + full_expansion(G, Y), |
| 128 | + subsumes_term(X, Y). |
| 129 | + |
| 130 | +/* |
| 131 | +Extra predicates from the paper |
| 132 | +*/ |
| 133 | +duplicate(X, Xs) :- |
| 134 | + tfilter(=(X), Xs, [_,_|_]). |
| 135 | + |
| 136 | +firstduplicate(X, [E|Es]) :- |
| 137 | + if_(memberd_t(E,Es), X=E, firstduplicate(X, Es)). |
| 138 | + |
| 139 | +treememberd_t(_, nil, false). |
| 140 | +treememberd_t(E, t(F,L,R), T) :- |
| 141 | + call((E=F; treememberd_t(E,L); treememberd_t(E,R)), T). |
| 142 | + |
| 143 | +tree_non_member(_, nill). |
| 144 | +tree_non_member(E, t(F,L,R)) :- |
| 145 | + dif(E,F), |
| 146 | + tree_non_member(E, L), |
| 147 | + tree_non_member(E, R). |
0 commit comments