Merge pull request #2027 from bakaq/dif

Improvements to dif/2

src/lib/dif.pl

@@ -7,7 +7,7 @@ arguments are different terms.
 
 :- use_module(library(atts)).
 :- use_module(library(dcgs)).
-:- use_module(library(lists), [append/3]).
+:- use_module(library(lists), [append/3, maplist/3]).
 
 :- attribute dif/1.
 
@@ -23,6 +23,32 @@ dif_set_variables([Var|Vars], X, Y) :-
     put_dif_att(Var, X, Y),
     dif_set_variables(Vars, X, Y).
 
+remove_goal([], _, []).
+remove_goal([G0|G0s], Goal0, Goals) :-
+    (   G0 == Goal0 ->
+        remove_goal(G0s, Goal0, Goals)
+    ;   Goals = [G0|Goals1],
+        remove_goal(G0s, Goal0, Goals1)
+    ).
+
+vars_remove_goal([], _).
+vars_remove_goal([Var|Vars], Goal0) :-
+    get_atts(Var, +dif(Goals0)),
+    remove_goal(Goals0, Goal0, Goals),
+    (   Goals = [] ->
+        put_atts(Var, -dif(_))
+    ;   put_atts(Var, +dif(Goals))
+    ),
+    vars_remove_goal(Vars, Goal0).
+
+reinforce_goal(Goal0, Goal) :-
+    Goal = (
+        term_variables(Goal0, Vars),
+        dif:vars_remove_goal(Vars, Goal0),
+        Goal0 = (L \== R),
+        dif(L, R)
+    ).
+
 append_goals([], _).
 append_goals([Var|Vars], Goals) :-
     (   get_atts(Var, +dif(VarGoals)) ->
@@ -34,9 +60,10 @@ append_goals([Var|Vars], Goals) :-
     append_goals(Vars, Goals).
 
 verify_attributes(Var, Value, Goals) :-
-    (   get_atts(Var, +dif(Goals)) ->
+    (   get_atts(Var, +dif(Goals0)) ->
 	    term_variables(Value, ValueVars),
-	    append_goals(ValueVars, Goals)
+	    append_goals(ValueVars, Goals0),
+        maplist(reinforce_goal, Goals0, Goals)
     ;   Goals = []
     ).
 

src/tests/dif.pl

@@ -0,0 +1,259 @@
+/**/
+
+:- use_module(library(format)).
+:- use_module(library(dcgs)).
+:- use_module(library(lists)).
+:- use_module(library(debug)).
+:- use_module(library(atts)).
+:- use_module(library(dif)).
+
+% Tests from https://www.complang.tuwien.ac.at/ulrich/iso-prolog/dif
+
+test("dif#1",(
+    call_residual_goals(dif(1,2), Res),
+    Res = []
+)).
+
+test("dif#2",(
+    \+ (dif(1,Y), Y = 1)
+)).
+
+test("dif#3",(
+    call_residual_goals((dif(1,Y), Y=2), Res),
+    Y == 2,
+    Res = []
+)).
+
+test("dif#4",(
+    \+ (dif(X,-Y), X= -Y)
+)).
+
+test("dif#5",(
+    \+ (dif(X,Y), X=Y)
+)).
+
+test("dif#6",(
+    \+ (dif(X,Y), X=Y, X=1)
+)).
+
+test("dif#7",(
+    \+ (dif(-X,-Y), X=Y)
+)).
+
+test("dif#8",(
+    \+ (dif(-X,-Y), X=Y, X=1)
+)).
+
+% I don't understand exactly what is expected for dif#9 and dif#10
+
+test("dif#11",(
+    call_residual_goals((X=Y, dif(X-Y,1-2)), Res),
+    X == Y,
+    Res = []
+)).
+
+test("dif#12",(
+    call_residual_goals((dif(X-Y,1-2), X=Y), Res),
+    X == Y,
+    Res = []
+)).
+
+test("dif#13",(
+    call_residual_goals((X=Y, Y=1, dif(X-Y,1-2)), Res),
+    X == 1,
+    Y == 1,
+    Res = []
+)).
+
+test("dif#14",(
+    call_residual_goals((dif(X-Y,1-2), X=Y, Y=1), Res),
+    X == 1,
+    Y == 1,
+    Res = []
+)).
+
+test("dif#15",(
+    call_residual_goals((dif(X-Y,1-2), X=Y, X=2), Res),
+    X == 2,
+    Y == 2,
+    Res = []
+)).
+
+test("dif#16",(
+    call_residual_goals((dif(A-C,B-D), C-D=z-z, A-B=1-2), Res),
+    A == 1,
+    B == 2,
+    C == z,
+    D == z,
+    Res = []
+)).
+
+test("dif#17",(
+    call_residual_goals((A-B=1-2, C-D=z-z, dif(A-C,B-D)), Res),
+    A == 1,
+    B == 2,
+    C == z,
+    D == z,
+    Res = []
+)).
+
+test("dif#18",(
+    call_residual_goals((dif(A,[C|B]), A=[[]|_], A=[B]), Res),
+    A == [[]],
+    B == [],
+    Res = [dif:dif([[]], [C])]
+)).
+
+test("dif#19",(
+    call_residual_goals((dif([E],[/]), E=1), Res),
+    E == 1,
+    Res = []
+)).
+
+test("dif#20",(
+    call_residual_goals((dif([a],B), B=[_|_], B=[b]), Res),
+    B == [b],
+    Res = []
+)).
+
+test("dif#21",(
+    call_residual_goals((dif([],A), A = [_]), Res),
+    A = [_],
+    Res = []
+)).
+
+test("dif#22",(
+    call_residual_goals((A = [_], dif([],A)), Res),
+    A = [_],
+    Res = []
+)).
+
+test("dif#t1",(
+    set_prolog_flag(occurs_check, false),
+    \+ \+ -X=X
+)).
+
+test("dif#t2",(
+    set_prolog_flag(occurs_check, false),
+    \+ (-X=X, -Y=Y, X\=Y)
+)).
+
+test("dif#t3",(
+    set_prolog_flag(occurs_check, false),
+    call_residual_goals((-X=X, dif(X,1)), Res),
+    X == -X,
+    Res = []
+)).
+
+test("dif#t4",(
+    set_prolog_flag(occurs_check, false),
+    \+ (-X=X, -Y=Y, dif(X,Y))
+)).
+
+test("dif#t5",(
+    set_prolog_flag(occurs_check, false),
+    \+ (dif(X,Y), -X=X, -Y=Y)
+)).
+
+test("dif#t6",(
+    set_prolog_flag(occurs_check, false),
+    \+ (A=[[]|A],dif(A,B),B=[[]|A])
+)).
+
+test("dif#t7",(
+    set_prolog_flag(occurs_check, false),
+    \+ (dif(-X,X),-Y=Y,X=Y)
+)).
+
+test("dif#o1",(
+    set_prolog_flag(occurs_check, true),
+    \+ (-X = X)
+)).
+
+test("dif#o2",(
+    set_prolog_flag(occurs_check, true),
+    call_residual_goals((dif(-X,X)), Res),
+    Res = []
+)).
+
+test("dif#o3",(
+    set_prolog_flag(occurs_check, true),
+    call_residual_goals((dif(-X,Y), X=Y), Res),
+    X == Y,
+    Res = []
+)).
+
+test("dif#12 but with multiple variables in the residuals",(
+    call_residual_goals((dif(X-Y-_, 1-2-3), X = Y), Res),
+    X == Y,
+    Res = []
+)).
+
+% https://github.com/mthom/scryer-prolog/issues/1956
+test("scryer-prolog#1956",(
+    call_residue_vars((dif(a-a,X-_),X=b), Res),
+    X == b,
+    Res = []
+)).
+
+main :-
+    findall(test(Name, Goal), test(Name, Goal), Tests),
+    run_tests(Tests, Failed),
+    show_failed(Failed),
+    halt.
+
+main_quiet :-
+    findall(test(Name, Goal), test(Name, Goal), Tests),
+    run_tests_quiet(Tests, Failed),
+    (   Failed = [] ->
+        format("All tests passed", [])
+    ;   format("Some tests failed", [])
+    ),
+    halt.
+
+portray_failed_([]) --> [].
+portray_failed_([F|Fs]) -->
+    "\"", F, "\"",  "\n", portray_failed_(Fs).
+
+portray_failed([]) --> [].
+portray_failed([F|Fs]) -->
+    "\n", "Failed tests:", "\n", portray_failed_([F|Fs]).
+
+show_failed(Failed) :-
+    phrase(portray_failed(Failed), F),
+    format("~s", [F]).
+
+run_tests([], []).
+run_tests([test(Name, Goal)|Tests], Failed) :-
+    format("Running test \"~s\"~n", [Name]),
+    (   call(Goal) ->
+        Failed = Failed1
+    ;   format("Failed test \"~s\"~n", [Name]),
+        Failed = [Name|Failed1]
+    ),
+    run_tests(Tests, Failed1).
+
+run_tests_quiet([], []).
+run_tests_quiet([test(Name, Goal)|Tests], Failed) :-
+    (   call(Goal) ->
+        Failed = Failed1
+    ;   Failed = [Name|Failed1]
+    ),
+    run_tests_quiet(Tests, Failed1).
+
+assert_p(A, B) :-
+    phrase(portray_clause_(A), Portrayed),
+    phrase((B, ".\n"), Portrayed).
+
+call_residual_goals(Goal, ResidualGoals) :-
+    call_residue_vars(Goal, Vars),
+    variables_residual_goals(Vars, ResidualGoals).
+
+variables_residual_goals(Vars, Goals) :-
+    phrase(variables_residual_goals(Vars), Goals).
+
+variables_residual_goals([]) --> [].
+variables_residual_goals([Var|Vars]) -->
+    dif:attribute_goals(Var),
+    variables_residual_goals(Vars).
+

tests/scryer/src_tests.rs

@@ -75,3 +75,12 @@ fn clpz_load() {
 fn iso_conformity_tests() {
     load_module_test("tests-pl/iso-conformity-tests.pl", "All tests passed");
 }
+
+#[test]
+fn dif_tests() {
+    run_top_level_test_with_args(
+        &["src/tests/dif.pl", "-f", "-g", "main_quiet"],
+        "",
+        "All tests passed",
+    );
+}