search

trealla-prolog / trealla

A compact, efficient Prolog interpreter written in plain-old C.
MIT License
272 stars 13 forks source link

Odd behavior on backtracking #52

Open guregu opened 2 years ago

guregu commented 2 years ago

Backtracking here seems to use the wrong variable substitutions (as mentioned here: https://github.com/trealla-prolog/trealla/issues/46#issuecomment-1259576921). Here's the smallest way to reproduce it I could find. See comment below for smaller version.

/* Old version of the WASM toplevel stripped down. */
:- module(js_toplevel, [js_ask/1]).

:- use_module(library(lists)).

js_ask(Input) :-
    read_term_from_chars(Query, [variable_names(Vars)], Input),
    query(Query, Vars, Status, Solution),
    write_result(Status, Solution),
    flush_output.

write_result(Status, Solution) :-
    write(Status), write(' '), write(Solution), nl.

query(Query, Vars, Status, Solution) :-
    (   catch(call(Query), Error, true)
    *-> OK = true
    ;   OK = false
    ),
    query_status(OK, Error, Status),
    (  nonvar(Error)
    -> Solution = Error
    ;  Solution = Vars
    ).

query_status(_OK, Error, error) :- nonvar(Error), !.
query_status(true, _, success).
query_status(false, _, failure).

person(socrates).
person(plato).
mortal(X) :- person(X).
?- use_module(js_toplevel).
   true.

% bug?
?- js_ask("mortal(X)").
success [X=socrates]
   true
;  false. % expected plato

% this is ok:
?- js_ask("person(X)").
success [X=socrates]
   true
; success [X=plato]
 true.

% this is ok:
?- js_ask("findall(X, mortal(X), Xs)").
success [X=_5,Xs=[socrates,plato]]
   true.

Trace shows odd backtracking:

?- trace, js_ask("mortal(X)").
[js_toplevel:0:f0:fp:1:cp0:sp0:hp0:tp0] EXIT trace
[js_toplevel:1:f0:fp:1:cp0:sp0:hp0:tp0] CALL js_ask("mortal(X)")
[js_toplevel:2:f1:fp:2:cp0:sp5:hp0:tp0] CALL read_term_from_chars(_0,[variable_names(_1)],"mortal(X)")
[js_toplevel:3:f1:fp:2:cp0:sp6:hp7:tp2] EXIT read_term_from_chars(mortal(_5),[variable_names(['X'=_5])],"mortal(X)")
[js_toplevel:4:f1:fp:2:cp0:sp6:hp7:tp2] CALL query(mortal(_5),['X'=_5],_3,_4)
[js_toplevel:5:f2:fp:3:cp1:sp12:hp18:tp0] CALL catch(call(mortal(_5)),_7,true)
[js_toplevel:6:f3:fp:4:cp1:sp15:hp18:tp0] CALL '$catch'(call(call(mortal(_5))),_7,call(true))
[js_toplevel:7:f3:fp:4:cp2:sp15:hp24:tp0] EXIT '$catch'(call(call(mortal(_5))),_7,call(true))
[js_toplevel:8:f3:fp:4:cp2:sp15:hp24:tp0] CALL call(call(mortal(_5)))
[js_toplevel:9:f3:fp:4:cp3:sp15:hp30:tp0] EXIT call(call(mortal(_5)))
[js_toplevel:10:f3:fp:4:cp3:sp15:hp30:tp0] CALL call(mortal(_5))
[js_toplevel:11:f3:fp:4:cp4:sp15:hp35:tp0] EXIT call(mortal(_5))
[js_toplevel:12:f3:fp:4:cp4:sp15:hp35:tp0] CALL mortal(_5)
[js_toplevel:13:f4:fp:5:cp4:sp16:hp35:tp0] CALL person(_5)
[js_toplevel:14:f5:fp:6:cp5:sp16:hp35:tp1] EXIT person(socrates)
[js_toplevel:15:f3:fp:5:cp5:sp16:hp35:tp1] CALL '$drop_barrier'
[js_toplevel:16:f3:fp:5:cp5:sp16:hp35:tp1] EXIT '$drop_barrier'
[js_toplevel:17:f3:fp:5:cp5:sp16:hp35:tp1] CALL '$drop_barrier'
[js_toplevel:18:f3:fp:5:cp5:sp16:hp35:tp1] EXIT '$drop_barrier'
[js_toplevel:19:f3:fp:5:cp5:sp16:hp35:tp1] CALL '$block_catcher'(1)
[js_toplevel:20:f3:fp:5:cp6:sp16:hp35:tp1] EXIT '$block_catcher'(1)
[js_toplevel:21:f3:fp:5:cp6:sp16:hp35:tp1] EXIT person(socrates)
[js_toplevel:22:f2:fp:5:cp6:sp16:hp35:tp1] CALL '$soft_cut'
[js_toplevel:23:f2:fp:5:cp6:sp16:hp35:tp1] EXIT '$soft_cut'
[js_toplevel:24:f2:fp:5:cp6:sp16:hp35:tp1] CALL _8=true
[js_toplevel:25:f2:fp:5:cp6:sp16:hp35:tp2] EXIT true=true
[js_toplevel:26:f2:fp:5:cp6:sp16:hp35:tp2] CALL query_status(true,_7,_3)
[js_toplevel:27:f5:fp:6:cp7:sp18:hp35:tp5] CALL nonvar(_7)
[js_toplevel:28:f5:fp:6:cp7:sp18:hp35:tp5] FAIL nonvar(_7)
[js_toplevel:29:f2:fp:5:cp6:sp16:hp35:tp2] REDO query_status(true,_7,_3)
[js_toplevel:30:f5:fp:6:cp6:sp17:hp35:tp4] EXIT query_status(true,_7,success)
[js_toplevel:31:f2:fp:4:cp7:sp15:hp43:tp4] CALL nonvar(_7)
[js_toplevel:32:f2:fp:4:cp7:sp15:hp43:tp4] FAIL nonvar(_7)
[js_toplevel:33:f2:fp:4:cp6:sp15:hp43:tp4] CALL _4=['X'=socrates]
[js_toplevel:34:f2:fp:4:cp6:sp15:hp43:tp5] EXIT ['X'=socrates]=['X'=socrates]
[js_toplevel:35:f2:fp:4:cp6:sp15:hp43:tp5] EXIT query_status(true,mortal(socrates),success)
[js_toplevel:36:f1:fp:4:cp6:sp15:hp43:tp5] CALL write_result(success,['X'=socrates])
[js_toplevel:37:f4:fp:5:cp6:sp17:hp43:tp5] CALL write(success)
success[js_toplevel:38:f4:fp:5:cp6:sp17:hp43:tp5] EXIT write(success)
[js_toplevel:39:f4:fp:5:cp6:sp17:hp43:tp5] CALL write(' ')
 [js_toplevel:40:f4:fp:5:cp6:sp17:hp43:tp5] EXIT write(' ')
[js_toplevel:41:f4:fp:5:cp6:sp17:hp43:tp5] CALL write(['X'=socrates])
[X=socrates][js_toplevel:42:f4:fp:5:cp6:sp17:hp43:tp5] EXIT write(['X'=socrates])
[js_toplevel:43:f4:fp:5:cp6:sp17:hp43:tp5] CALL nl

[js_toplevel:44:f4:fp:5:cp6:sp17:hp43:tp5] EXIT nl
[js_toplevel:45:f4:fp:5:cp6:sp17:hp43:tp5] EXIT write_result(success,['X'=socrates])
[js_toplevel:46:f1:fp:5:cp6:sp17:hp43:tp5] CALL flush_output
[js_toplevel:47:f1:fp:5:cp6:sp17:hp43:tp5] EXIT flush_output
[js_toplevel:48:f1:fp:5:cp6:sp17:hp43:tp5] EXIT write_result(mortal(socrates),['X'=socrates])
   true
; [js_toplevel:49:f3:fp:5:cp5:sp16:hp35:tp1] REDO '$block_catcher'(1)
[js_toplevel:50:f3:fp:5:cp5:sp16:hp35:tp1] FAIL '$block_catcher'(1)
[js_toplevel:51:f4:fp:5:cp4:sp16:hp35:tp0] REDO person(success) <---------------- why is it using 'success' here?
[js_toplevel:52:f4:fp:5:cp4:sp16:hp35:tp0] FAIL person(success)
[js_toplevel:53:f3:fp:4:cp3:sp15:hp35:tp0] REDO call(mortal(_5))
[js_toplevel:54:f3:fp:4:cp3:sp15:hp35:tp0] FAIL call(mortal(_5))
[js_toplevel:55:f3:fp:4:cp2:sp15:hp30:tp0] REDO call(call(mortal(_5)))
[js_toplevel:56:f3:fp:4:cp2:sp15:hp30:tp0] FAIL call(call(mortal(_5)))
[js_toplevel:57:f3:fp:4:cp1:sp15:hp24:tp0] REDO '$catch'(call(call(mortal(_5))),_7,call(true))
[js_toplevel:58:f3:fp:4:cp1:sp15:hp24:tp0] FAIL '$catch'(call(call(mortal(_5))),_7,call(true))
 false.

In particular step 51 looks suspect.

guregu commented 2 years ago

Reduced it further:

:- module(js_toplevel, [js_ask/1]).

:- use_module(library(lists)).

js_ask(Input) :-
    read_term_from_chars(Query, [variable_names(Vars)], Input),
    query(Query, Status),
    write(Vars), nl, write(Status), nl,
    call_any_predicate(Status). % deleting this fixes it?

call_any_predicate(_).

query(Query, Status) :-
    % weird:
    catch(Query, Error, true),
    % ok:
    % call(Query),
    query_status(true, Error, Status).

query_status(_OK, Error, error) :- nonvar(Error), !.
query_status(true, _, success).
query_status(false, _, failure).

person(socrates).
person(plato).
mortal(X) :- person(X).

I think optimization is the culprit:

$ ./tpl --version
Trealla Prolog (c) Infradig 2020-2022, v2.2.15

# weird
$ ./tpl js_toplevel.pl -g 'js_ask("mortal(X)")' --ns
[X=socrates]
success
   true
;

# ok
$ ./tpl js_toplevel.pl -O0 -g 'js_ask("mortal(X)")' --ns
[X=socrates]
success
   true
; [X=plato]
success
 true
;
infradig commented 2 years ago

It would seem so.

On Sat, Oct 1, 2022 at 12:32 AM guregu @.***> wrote:

Reduced it further:

:- module(js_toplevel, [js_ask/1]).

:- use_module(library(lists)). js_ask(Input) :- read_term_from_chars(Query, [variable_names(Vars)], Input), query(Query, Status), write(Vars), nl, write(Status), nl, call_any_predicate(Status). % deleting this fixes it? call_anypredicate(). write_result(Status, Solution) :- write(Status), write(' '), write(Solution), nl. query(Query, Status) :- % weird: catch(Query, Error, true), % ok: % call(Query), query_status(true, Error, Status). query_status(_OK, Error, error) :- nonvar(Error), !.querystatus(true, , success).querystatus(false, , failure). person(socrates).person(plato).mortal(X) :- person(X).

I think optimization is the culprit:

$ ./tpl --version Trealla Prolog (c) Infradig 2020-2022, v2.2.15

weird

$ ./tpl js_toplevel.pl -g 'js_ask("mortal(X)")' --ns [X=socrates] success true;

ok

$ ./tpl js_toplevel.pl -O0 -g 'js_ask("mortal(X)")' --ns [X=socrates] success true; [X=plato] success true;

— Reply to this email directly, view it on GitHub https://github.com/trealla-prolog/trealla/issues/52#issuecomment-1263654417, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNKSESLJQEYI2KQFZKFFILWA32ZHANCNFSM6AAAAAAQZZVIGA . You are receiving this because you are subscribed to this thread.Message ID: @.***>