Possible issue regarding `:-`.

[enoperm]

I have been playing around with prolog recently, and I got a meta-interpreter running (mostly by going along with https://www.metalevel.at/acomip) that provides a reasoning as to how a goal was fulfilled, as well as allow for using a list provided as a parameter in place of the global database.

mi(+true, _Facts, true).
mi(+Conj, Facts, [ReasonA|ReasonB]) :- Conj = (A, B), mi(+A, Facts, ReasonA), mi(+B, Facts, ReasonB).
mi(+Disj, Facts, Reason) :- Disj = (A; B), (mi(+A, Facts, Reason); mi(+B, Facts, Reason)).
mi(+Fact, Facts, [fact(Fact)]) :- member(Fact, Facts).
mi(+R, Facts, [rule(R, Body) | Reason]) :- member(Rule, Facts), :-(R, Body) = Rule, mi(+Body, Facts, Reason).

This works fine in SWI Prolog:

?- [meta].
true.

?- mi(+mortal(X), [(mortal(X) :- man(X)), man(socrates)], Reasoning).
X = socrates,
Reasoning = [rule(mortal(socrates), man(socrates)), fact(man(socrates))] .

In a 1pl repl, however, I get an error.

Top level for ichiban/prolog v0.9.1
This is for testing purposes only!
See https://github.com/ichiban/prolog for more details.
Type Ctrl-C or 'halt.' to exit.
?- [meta].
true.
?- mi(+mortal(X), [(mortal(X) :- man(X)), man(socrates)], Reasoning).
2022/06/30 19:31:41 error(existence_error(procedure, :- /1), 'Unknown procedure.')

Which is odd, because I do not see :-/1 anywhere in the code, at most I'd expect to see an error about :-/2. I have tried defining :-/1 as a dynamic predicate in the source file where the meta-interpreter lies, as below:

:- dynamic((:-)/1).

This line was accepted by both implementations, and the behaviour of SWIPL did not change. With that addition, I do not receive an error message from 1pl anymore, but it still did not behave as I expected.

?- [meta].
true.
?- mi(+mortal(X), [(mortal(X) :- man(X)), man(socrates)], Reasoning).
false.

Curiously, if I replace my use of :-(Head, Body) with a custom predicate, such as rule(Head, Body), it behaves the same in both implementations:

?- [meta].
true.
?- mi(+mortal(X), [rule(mortal(X), man(X)), man(socrates)], Reasoning).
X = socrates,
Reasoning = [rule(mortal(socrates), man(socrates)), fact(man(socrates))].

I'm not quite sure what is going wrong, but I suspect :- may be receiving special treatment somewhere in Ichiban Prolog?

[ichiban]

Thank you very much for reporting this! I think this is because of a bug in the parser.

This implementation does special treatment to :- in a couple of places:

• directives
• compiling rules
• ...

But none of them distinguish between Head :- Body and :-(Head, Body)- they're same after the parsing phase.

I'm working hard on the parser/lexer/writer right now and the next release, hopefully this weekend, will fix the most of syntax related bugs.

[ichiban]

@enoperm Could you try the latest release v0.10.1, please? I fixed all the syntax bugs known so far including the ones regarding operators. The problem you're seeing here might have been fixed as well.

[UWN]

Defining a predicate (:-)/1 is quite problematic as it is easily confused with the principal functor of a directive. For this reason SICStus and IF produce a permission_error(modify,static_procedure,_). From a conformity standpoint they consider (:-)/1 an implementation specific built-in (5.5.9) that cannot be called (they produce there either an existence error or some implementation specific one). Same for (:-)/2, (?-)/1, and (-->)/2.

In SWI this kind of works, but note that it can be abused for code injection. Just try listing((:-)/1) to see why. Similarly GNU.

[enoperm]

@enoperm Could you try the latest release v0.10.1, please? I fixed all the syntax bugs known so far including the ones regarding operators. The problem you're seeing here might have been fixed as well.

Seems to work, now.

Defining a predicate (:-)/1 is quite problematic as it is easily confused with the principal functor of a directive. For this reason SICStus and IF produce a permission_error(modify,static_procedure,_). From a conformity standpoint they consider (:-)/1 an implementation specific built-in (5.5.9) that cannot be called (they produce there either an existence error or some implementation specific one). Same for (:-)/2, (?-)/1, and (-->)/2.

In SWI this kind of works, but note that it can be abused for code injection. Just try listing((:-)/1) to see why. Similarly GNU.

I tried testing it with an SWI toplevel, but it raises an existience_error for both of listing((:-)/1) and listing((:-)/2) from either a clean state or after loading the current iteration of my metainterpreter.

GNU prolog simply yields yes, which is interesting, though I'm not quite sure how that leads to code injection, yet.

EDIT: I just realized I forgot to prepend :-, listing((:-)/1). does yield a result now.

[enoperm]

Though I might add, I only included a definition for :-/1 to see whether it changes the behaviour of 1pl, it is neither needed nor wanted in the code.

[UWN]

Maybe I was a bit too terse concerning SWI, so this I meant:

?- catch(asserta((:-a)),Error,true).
true.

?- listing(:-).
:- dynamic (:-)/1.

:-a.

true.