From 9c5bdb1020ce94f51014bb73e824a6ad06f95fc2 Mon Sep 17 00:00:00 2001
From: Aleksy Grabowski <hurufu@gmail.com>
Date: Thu, 18 Jul 2024 20:24:09 +0200
Subject: [PATCH] Remove bad test and add more unit tests

---
 src/tests/reif.pl | 76 +++++++++++++++++++++++++++++++++--------------
 1 file changed, 54 insertions(+), 22 deletions(-)

diff --git a/src/tests/reif.pl b/src/tests/reif.pl
index 5942a6e9f..93dba0951 100644
--- a/src/tests/reif.pl
+++ b/src/tests/reif.pl
@@ -4,10 +4,13 @@
 :- use_module(library(lists)).
 :- use_module(library(dif)).
 :- use_module(library(loader)).
+:- use_module(library(format)).
 :- use_module(test_framework).
 
-% Those tests are just sanity checks – examples from the paper, to make sure
-% I haven't messed up.
+/*
+Those tests are just sanity checks – examples from the paper, to make sure I
+haven't messed up.
+*/
 test("indexing dif/2 p6#1", (
     findall(X-Fs, tfilter(=(X),[1,2,3,2,3,3],Fs), [1-[1], 2-[2,2], 3-[3,3,3], Y-[]]),
     maplist(dif(Y), [1,2,3])
@@ -45,30 +48,59 @@
     X == Y
 )).
 
-% This test fails, and I don't know if goal_expanded/2 should be recursive or not,
-% and what properties it shall maintain (is idempotence even desirable?).
-%test("second expansion doesnt modify goal", (
-%    findall(G==Gxx, test_expand_goal_twice(G,Gxx), Goals),
-%    maplist(call, Goals)
-%)).
+/*
+Following tests capture current results of goal expansion
+TODO: Investigate if if_/3 can be further expanded, and if it will be beneficial
+*/
+test("goal_expansion (=)", (
+    subsumes_full_expansion(if_(1=2,a,b), (
+        1 \= 2 -> b
+    ;   1 == 2 -> a
+    ;   1 = 2, a
+    ;   dif(1,2), b)))).
 
-test("ge1", (
-    loader:goal_expansion(if_(1=2,false,true), reif_tests, _)
-)).
+test("goal_expansion (;)", (
+    subsumes_full_expansion(if_((1=2;3=3),a,b), (
+        1 \= 2 -> if_(3=3,a,b)
+    ;   1 == 2 -> a
+    ;   1 = 2, a
+    ;   dif(1,2), if_(3=3,a,b))))).
+
+test("goal_expansion (,)", (
+    subsumes_full_expansion(if_((1=2,3=3),a,b), (
+        1 \= 2 -> b
+    ;   1 == 2 -> if_(3=3,a,b)
+    ;   1 = 2, if_(3=3,a,b)
+    ;   dif(1,2), b)))).
+
+test("goal_expansion memberd_t", (
+    subsumes_full_expansion(if_(memberd_t(f,"abcdefgh"),t,f), (
+        call(memberd_t(f,"abcdefgh"),A),
+        (   A == true  -> t
+        ;   A == false -> f
+        ;   nonvar(A)  -> throw(error(type_error(boolean,A),_))
+        ;   throw(error(instantiation_error,_))))))).
+
+test("goal_expansion cond_t", (
+    subsumes_full_expansion(if_(cond_t(a,b),t,f), (
+        call(cond_t(a,b),A),
+        (   A == true  -> t
+        ;   A == false -> f
+        ;   nonvar(A)  -> throw(error(type_error(boolean,A),_))
+        ;   throw(error(instantiation_error,_))))))).
 
-test_expand_goal_twice(G, Gxx) :-
-    test_goal(G),
-    reif:goal_expanded(G,Gx),
-    reif:goal_expanded(Gx, Gxx).
+% Expand goal until fix point is found
+full_expansion(G, X) :-
+    user:goal_expansion(G, Gx) -> full_expansion(Gx, X); G = X.
 
-test_goal(_).
-test_goal(call(a)).
-test_goal(call(a:b(1))).
-test_goal(call(a:b,c)).
-test_goal(call(call(a))).
-test_goal(call(call(a:b))).
+% X is more general than fully expanded goal G
+subsumes_full_expansion(G, X) :-
+    full_expansion(G, Y),
+    subsumes_term(X, Y).
 
-% Extra predicates from the paper
+/*
+Extra predicates from the paper
+*/
 duplicate(X, Xs) :-
     tfilter(=(X), Xs, [_,_|_]).