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.