mthom / scryer-prolog

A modern Prolog implementation written mostly in Rust.
BSD 3-Clause "New" or "Revised" License
2.06k stars 123 forks source link

thread 'main' panicked at 'drain lower bound was too large' #416

Closed triska closed 4 years ago

triska commented 4 years ago

When I apply the following change to clpz.pl to enable goal expansion in user programs:

https://github.com/triska/scryer-prolog/commit/77d71194a19bfbf11650e53f8cce75f793288032

and then create crash.pl with the following contents:

:- use_module(library(clpz)).

t(X, Y) :- X #= Y + 1.

I get:

$ scryer-prolog crash.pl 
thread 'main' panicked at 'drain lower bound was too large', <::core::macros::panic macros>:2:2
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'main' panicked at 'drain lower bound was too large', <::core::macros::panic macros>:2:2
stack backtrace:
   0:        0x100b25a85 - ::fmt::hff7732c2e44ef8b9
   1:        0x100b45c8d - core::fmt::write::hd42cb3dea57bae40
   2:        0x100b223cb - std::io::Write::write_fmt::ha39f6009af02b1d2
   3:        0x100b2773a - std::panicking::default_hook::{{closure}}::h389f076017b5df43
   4:        0x100b2743a - std::panicking::default_hook::h04b06ec20c41bf02
   5:        0x100b27d9d - std::panicking::rust_panic_with_hook::hccde7faed9a5c398
   6:        0x100b27932 - rust_begin_unwind
   7:        0x100b4466f - core::panicking::panic_fmt::h272b9afd5b7b725a
   8:        0x100b445c7 - core::panicking::panic::h8627f9662a331d41
   9:        0x1009d5a5f - scryer_prolog::prolog::machine::code_repo::CodeRepo::truncate_terms::hcd25bd2d59bd8c53
  10:        0x1009df2ad - scryer_prolog::prolog::machine::term_expansion::TermStream::rollback_expansion_code::h742da23ed99333a7
  11:        0x1009ded16 - ::drop::hd47a3c5cf703c285
  12:        0x100a4eff6 - core::ptr::drop_in_place::hd929942006426bc1
...
triska commented 4 years ago

When I now apply the mentioned commit (https://github.com/triska/scryer-prolog/commit/77d71194a19bfbf11650e53f8cce75f793288032), I get:

?- use_module(library(clpz)).
nontermination

However, I expect this to terminate.

mthom commented 4 years ago

I plan to completely revamp the expansions system in the next few months. Once we have the ability to compile predicates incrementally, the culprit here will be obsolete and would then be removed from Scryer. A nice side effect is that library load times should become much faster, and many other issues will be resolved. For now, that means putting this issue (and similarly, other goal expansion issues; at least, those not related to top-level exception reporting) on hold until streams and sockets are done.

The progression of new work I have in mind for the summer is this:

1) Implement sockets, and later, the stream interface, 2) Clean up the compilation module: move more of it into Prolog, but primarily, use incremental compilation for term & goal expansions, dynamic clauses, and plan for the harmonious interoperation of the multifile, discontiguous, and dynamic declaratives; treat term and goal expansions as "normal" predicates instead of "elevated" ones, 3) Implement garbage collection and related goodies.

I think 2) is best handled as a large, monolithic chunk of work, allowing us to solve many problems at once, including this one. I hope that sounds good, and I thank you for your patience!

triska commented 4 years ago

I have pushed the enabled expansion and your latest changes to https://github.com/triska/scryer-prolog/tree/goal_expansion.

With that version, the following compiles successfully:

:- use_module(library(clpz)).
:- use_module(library(format)).

:- dynamic(t/2).

t(I0, I) :- I #= I0 + 1.

However, I get:

?- listing(t/2).
t(A,B) :-
   B#=A+1.

and so the defined goal expansion is apparently not applied to the code. The defined goal expansion in library(clpz) is:

:- dynamic(goal_expansion/1).

user:goal_expansion(Goal0, Goal) :-
        \+ clpz:goal_expansion(false),
        clpz_expandable(Goal0),
        clpz_expansion(Goal0, Goal).

Via user:', it is intended to be applied to all user-defined predicates.

The expected expansion is:

?- clpz:clpz_expansion(B#=A+1, E).
   E = (integer(B)->(integer(A)->B=:=A+1;_A is B,clpz:clpz_equal(_A,A+1));integer(A)->(var(B)->B is A+1;_A is A+1,clpz:clpz_equal(B,_A));clpz:clpz_equal(B,A+1))
;  false.

In portrayed form:

?- clpz:clpz_expansion(B#=A+1, E),
   portray_clause((t(A,B) :- E)).
t(A,B) :-
   (  integer(B) ->
      (  integer(A) ->
         B=:=A+1
      ;  C is B,
         clpz:clpz_equal(C,A+1)
      )
   ;  (  integer(A) ->
         (  var(B) ->
            B is A+1
         ;  C is A+1,
            clpz:clpz_equal(B,C)
         )
      ;  clpz:clpz_equal(B,A+1)
      )
   ).
mthom commented 4 years ago

This should now work.

triska commented 4 years ago

Unfortunately, it does not: Consulting the file with the goal_expansion branch (https://github.com/triska/scryer-prolog/tree/goal_expansion) runs indefinitely:

$ cat t.pl 
:- use_module(library(clpz)).
:- use_module(library(format)).

:- dynamic(t/2).

t(I0, I) :- I #= I0 + 1.

$ scryer-prolog t.pl 
loop
mthom commented 4 years ago

I'm sorry, I can't reproduce it. It doesn't loop for me, it goes to the query prompt.

triska commented 4 years ago

Hmm... with the goal_expansion branch, even already loading library(clpz) loops for me:

$ scryer-prolog
?- use_module(library(clpz)).
loop
mthom commented 4 years ago

No, you're right. It loops. My fault. Heh, I'm relieved to know the error does reproduce on my machine.

triska commented 4 years ago

It now compiles, but the goal expansion seems not to take place. With the code I posted, I get:

?- clause(t(X,Y), Body).
   Body = (Y#=X+1).

However, the intended and ostensibly defined expansion is:

?- clpz:clpz_expansion(Y#=X+1, E).
   E = (integer(Y)->(integer(X)->Y=:=X+1;_A is Y,clpz:clpz_equal(_A,X+1));integer(X)->(var(Y)->Y is X+1;_A is X+1,clpz:clpz_equal(Y,_A));clpz:clpz_equal(Y,X+1))
triska commented 4 years ago

Perfect, thank you a lot!

I have filed #425 to enable goal expansion for CLP(ℤ).