Defining operators including vertical bars(|) in SWI-prolog

operators, prolog, swi-prolog

Solution

You cannot do this. Neither in ISO Prolog nor in SWI. While the vertical bar serves as an operator — provided a corresponding operator declaration is present, it cannot be used unquoted as part of an operator with a length of two or more characters. The best you can get in your situation is to declare an operator `|-` and use it in quoted form. In both cases below, quotes are strictly needed.

:- op(1200, xfx, '|-').  

a '|-' b.

Doesn't look too attractive. Alone, as a single character, the bar serves as an infix operator.

?- ( a | b ) = '|'(a, b).
   true.

?- current_op(Pri,Fix,'|').
   Pri = 1105, Fix = xfy.

There is another use of `|` as a head-tail separator in lists. Due to the restrictions to the priority the infix bar can take, there is no ambiguity between `[A|As]` and above use.

Note that `[a|-].` is valid Prolog text. Even `gamma |- a.` is valid in SWI and even valid Prolog text in ISO, provided there is an operator declaration!

?- write_canonical((gamma|-a)).
'|'(gamma,-(a))

Problem

I am trying to encode basic logical inferences in Prolog, and I want to define some custom operators to streamline the notation. It would be handy if I can type `|-` for ⊢. So I tried ``` :- op(1150, xfy, [ '|-' ]). gamma |- a. Gamma |- or(A,_) :- Gamma |- A. Gamma |- or(_,A) :- Gamma |- A. ``` but when I try the query `gamma |- or(a,X)`, I get the error message `ERROR: '<meta-call>'/1: Undefined procedure: gamma/0` instead of the `true` I expect. The problem seems to be that the defined operator includes a vertical bar character. If I modify the knowledge base to ``` :- op(1150, xfy, [ imp ]). gamma imp a. Gamma imp or(A,_) :- Gamma imp A. Gamma imp or(_,A) :- Gamma imp A. ``` Then Prolog has no problems answering the query `gamma imp or(a,X)`. Is the vertical bar a reserved character that I'm not allowed to use in definitions? Or is there some way around this?

Original source