Encountered `representation_error(max_arity, assertz/1)` when running `check/1` with LPTP

[thierrymarianne]

Hello,

When trying to run the test suite for Logic Program Theorem Prover (LPTP) with Scryer Prolog,
I have encountered the representation_error(max_arity, assertz/1) error
for the following proofs examples:

• ./examples/parser/pr/termination.pr,
• ./examples/parser/pr/soundness.pr,
• ./examples/taut/taut.pr.

(Please note that the file extension is not conventional but checking proofs works as expected
with a few adjustments detailed in this pull-request git log history and reply.

I don't really expect this issue to be solved because of what I gathered from #67 (7.11.2.3 ?).
I don't have the ISO standard at my disposal
but I trust there are ways how to work around this issue somehow.

Besides, after discovering past discussions like #2594 on the topic,
I thought it could be helpful to have some use cases.

A test case exhibiting the error thrown has been pushed to this branch.

[triska]

Excellent additional example for the usefulness of unbounded arity, thank you a lot!

You may be able to work around it "manually", with a dedicated term lets you chain additional arguments, such as:

T = functor_args(f, [arg1,arg2,...,argn]).

It is clear that the engine should be able to do this on demand, while using a more efficient internal representation where possible.

[thierrymarianne]

Alright, thank you 👍🏼.

I will try to use dedicated term(s) as you've pointed out in the meantime.