diff --git a/.gdbinit b/.gdbinit new file mode 100644 index 000000000..9136c9010 --- /dev/null +++ b/.gdbinit @@ -0,0 +1 @@ +file ./target/debug/scryer-prolog diff --git a/.gitignore b/.gitignore index f63be9e99..2ffdb11e6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ src/static_atoms.rs target/ +tests/scryer/cli/issues/incorrect_arithmetics.in/chnytjl.pl diff --git a/src/loader.pl b/src/loader.pl index 0998182d1..cabfa5508 100644 --- a/src/loader.pl +++ b/src/loader.pl @@ -36,6 +36,46 @@ write('.'). +:- meta_predicate maplistdif(3, ?, ?, ?). + +maplistdif(_, [], [], L-L). +maplistdif(G__2, [H1|T1], [H2|T2], L0-LX) :- + call(G__2, H1, H2, L0-L1), + maplistdif(G__2, T1, T2, L1-LX). + +%% arithmetic_expansion(+Type, ?Term, -ExpandedTerm, -Unifier-Rest). +% +% `ExpandedTerm` is the minimal generalization of `Term` which makes a valid +% arithmetic relation (`Type = rela`) or functional expression (`Type = func`). +% That means if all unifications from `Unifier` hold then `ExpandedTerm == Term`. +% `Unifier-Rest` form together a list difference. `Term` is traversed from left +% to right, depth-first. Given an invalid arithmetic term, as seen in the +% example below, `E` becomes valid arithmetic term, `L` - unifier: +% +% ``` +% ?- arithmetic_expansion(rela, X is sqrt([]+Y*foo(e/2)), E, L-[]). +% E = (X is sqrt(_A+Y*_B)), L = [[]=_A,foo(e/2)=_B]. +% ``` +% +% NOTE: Order of clauses is important for correctness. +arithmetic_expansion(func, T, T, L-L) :- + (var(T); number(T)), !. +arithmetic_expansion(Set, T, R, LD) :- + functor(T, F, A), + arithmetic_term(Set, A, Fs), + member(F, Fs), !, + functor(R, F, A), + T =.. [F|Ts], + R =.. [F|Rs], + maplistdif(arithmetic_expansion(func), Ts, Rs, LD). +arithmetic_expansion(func, T, R, [T=R|L]-L). + +arithmetic_term(func, 0, [e,pi,epsilon]). +arithmetic_term(func, 1, [+,-,\,sqrt,exp,log,sin,cos,tan,asin,acos,atan,sign,abs,round,ceiling,floor,truncate,float,float_integer_part,float_fractional_part]). +arithmetic_term(func, 2, [+,-,/,*,**,^,/\,\/,xor,div,//,rdiv,<<,>>,mod,rem,max,min,gcd,atan2]). +arithmetic_term(rela, 2, [is,>,<,>=,=<,=:=,=\=]). + + :- non_counted_backtracking '$print_message_and_fail'/1. '$print_message_and_fail'(Error) :- @@ -72,6 +112,11 @@ :- non_counted_backtracking goal_expansion/3. +goal_expansion(G, _, Gx) :- + % Additional rule just to replace invalid arithmetic expression with + % runtime exception + nonvar(G), + arithmetic_expansion(rela, G, R, Gx-[R]). goal_expansion(Goal, Module, ExpandedGoal) :- ( atom(Module), '$predicate_defined'(Module, goal_expansion, 2), diff --git a/tests/scryer/cli/issues/incorrect_arithmetics.in/incorrect_arithmetics.pl b/tests/scryer/cli/issues/incorrect_arithmetics.in/incorrect_arithmetics.pl new file mode 100644 index 000000000..6d238061c --- /dev/null +++ b/tests/scryer/cli/issues/incorrect_arithmetics.in/incorrect_arithmetics.pl @@ -0,0 +1,92 @@ +:- use_module(library(lists)). +:- use_module(library(random)). +:- use_module(library(dcgs)). +:- use_module(library(iso_ext)). +:- use_module(library(format)). +:- use_module(library(debug)). +:- use_module(library(time)). +:- use_module(library(gensym)). + +% Asserting and consulting of erroneous arithmetic relation shall succeed, +% but then it must fail at runtime. +main :- + template_relation("tttft", R), + load_test(assertz, R), + load_test(reconsult, R). + +load_test(Setup, Body) :- + portray_clause(start:Setup), + gensym(test, Test), + setup_call_cleanup( + ignore_exception(call(Setup, (Test :- false, Body))), + ( + (ignore_exception(listing(Test/0)),!;true), + \+ignore_exception(Test) -> Result = pass; Result = fail + ), + ignore_exception(retractall(Test)) + ), + portray_clause(Result:Setup). + +reconsult(Clause) :- + Clause = (Head :- Body), + File = 'chnytjl.pl', + portray_consult(File, (canary :- Body)), + setup_call_cleanup( + assertz(Head), + portray_consult(File, Clause), + retract(Head) + ). + +portray_consult(File, Clause) :- + setup_call_cleanup( + open(File, write, S), + portray_clause(S, Clause), + close(S) + ), + consult(File). + +template_relation(Template, R) :- + time(setof(E, phrase(arith_relation(E), Template), Es)), + length(Es, L), + random_integer(0, L, I), + format(" % Info: Selected ~d/~d aritmetic terms that satisfy ~s template:~n\t", [I,L,Template]), + nth0(I, Es, R), + portray_clause(R). + +%% phrase(arith_relation(Relation), Template). +% +% `Relation` is valid or invalid arithmetic relation (like `A is 3`) according +% to a template: `t` means correct term, `f` – incorrect. Position of template +% elements correspond to position of a term in the same relation written in +% Polish notation. Given expression: `1 < [] + 3` its template is: `"tttft"`, +% because it can be written as `< 1 + [] 3` using PN. +% +% Not all possible terms can be utilized and are commented out or otherwise not +% included, because it unnecessarily increases solution space. +arith_relation(F) --> rel(expr(F,A)), arith_expression(A). +arith_relation(F) --> rel(expr(F,A,B)), arith_expression(A), arith_expression(B). +arith_expression(A) --> func(expr(A)). +arith_expression(F) --> func(expr(F,A)), arith_expression(A). +arith_expression(F) --> func(expr(F,A,B)), arith_expression(A), arith_expression(B). + +func(Expr) --> {fn(T, Expr)}, [T]. +rel(Expr) --> {rl(T, Expr)}, [T]. + +rl(t, expr(F,A,B)) :- member(F, [A number(N); (maybe -> random(N); random_integer(-1000, 1000, N)). + +ignore_exception(G) :- catch($-G, _, true). diff --git a/tests/scryer/cli/issues/incorrect_arithmetics.stderr b/tests/scryer/cli/issues/incorrect_arithmetics.stderr new file mode 100644 index 000000000..e69de29bb diff --git a/tests/scryer/cli/issues/incorrect_arithmetics.stdout b/tests/scryer/cli/issues/incorrect_arithmetics.stdout new file mode 100644 index 000000000..0bceb4f39 --- /dev/null +++ b/tests/scryer/cli/issues/incorrect_arithmetics.stdout @@ -0,0 +1,3 @@ +% Info: Selected 1432th out of 2136 found aritmetic relations that satisfy ttttt template: + A is+sqrt(-e). +% Warning: singleton variables A at line 0 of chnytjl.pl diff --git a/tests/scryer/cli/issues/incorrect_arithmetics.toml b/tests/scryer/cli/issues/incorrect_arithmetics.toml new file mode 100644 index 000000000..98c377d6b --- /dev/null +++ b/tests/scryer/cli/issues/incorrect_arithmetics.toml @@ -0,0 +1,6 @@ +args = [ + "-f", + "--no-add-history", + "-g", "main,halt", + "incorrect_arithmetics.pl" +]