# SPEC 8: every term has one canonical text. The programs state terms and
# print them back as conclusions.

=== atoms are written as Python's repr of the string
spec: 8.1
--- program.py
from peye import *
fact(d('plain'), d("it's"), d('say "hi"'), d('both \' and "'), d('tab\there'), d('new\nline'))
fact(d('back\\slash'), d('café'), d('😀'), d('bell\x07'), d('zero\u200bwidth'), d(''))
query(d(X))
--- stdout
d('plain')
d("it's")
d('say "hi"')
d('both \' and "')
d('tab\there')
d('new\nline')
d('back\\slash')
d('café')
d('😀')
d('bell\x07')
d('zero\u200bwidth')
d('')

=== the empty list is written []
spec: 8.1
--- program.py
from peye import *
fact(d([]), d('[]'), d(struct('[]')))
query(d(X))
--- stdout
d([])

=== integers are written in decimal
spec: 8.1
--- program.py
from peye import *
fact(d(0), d(-7), d(10 ** 40))
query(d(X))
--- stdout
d(0)
d(-7)
d(10000000000000000000000000000000000000000)

=== floats are written as Python's repr
spec: 8.1
--- program.py
from peye import *
fact(d(0.1), d(2.0), d(-0.5), d(1e22), d(0.00001), d(1e17), d(123456789.0), d(1.7976931348623157e308), d(-0.0))
query(d(X))
--- stdout
d(0.1)
d(2.0)
d(-0.5)
d(1e+22)
d(1e-05)
d(1e+17)
d(123456789.0)
d(1.7976931348623157e+308)
d(-0.0)

=== a variable is written as its name
spec: 8.1
args: --proof
--- stdin
from peye import *
Lower, Kw = vars('lowercase struct')
fact(p(Some_Var1, Lower, Kw))
query(p(A, B, C))
--- stdout
p(A, B, C)

clause(1, fact(p(Some_Var1, lowercase, struct)))

step(p(A, B, C), clause(1), {'Some_Var1': A, 'lowercase': B, 'struct': C}, [])

=== a variable name starting with VAR_ is encoded
spec: 8.1
args: --proof
--- stdin
from peye import *
Odd = vars('VAR_X')
fact(p(Odd))
query(p(A))
--- stdout
p(A)

clause(1, fact(p(VAR_VAR__X)))

step(p(A), clause(1), {'VAR_X': A}, [])

=== an encoded variable name reads back as the variable it encodes
spec: 8.1, 9
args: --goal "unify(VAR_X, 1) & unify(X, Y)"
--- stdin
from peye import *
--- stdout
unify(1, 1) & unify(1, 1)

=== an identifier starting with VAR_ that encodes no name is rejected
spec: 8.1, 9
args: --goal "unify(VAR_a_b, 1)"
exit: 1
stderr: prefix peye:
--- stdin
from peye import *
--- stdout

=== variables in conclusions are named A, B, ... in order of first occurrence
spec: 8.3
args: --goal "unify(f(Y, X, Y), Z)" --goal "unify(g(P), Q)"
--- stdin
from peye import *
--- stdout
unify(f(A, B, A), f(A, B, A))
unify(g(C), g(C))

=== each _ of a clause is a variable named _0, _1, ... skipping names the clause uses
spec: 4.4
args: --proof --skolem-genid test
--- stdin
from peye import *
fact(p(1))
implies(p(X) & unify(_0, _), q(X, _, [X, *_]))
--- stdout
q(1, 'https://eyereasoner.github.io/.well-known/genid/test#sk_0', [1, *'https://eyereasoner.github.io/.well-known/genid/test#sk_1'])

clause(1, fact(p(1)))
clause(2, implies(p(X) & unify(_0, _3), q(X, _1, [X, *_2])))

step(q(1, 'https://eyereasoner.github.io/.well-known/genid/test#sk_0', [1, *'https://eyereasoner.github.io/.well-known/genid/test#sk_1']), clause(2), {'X': 1, '_1': 'https://eyereasoner.github.io/.well-known/genid/test#sk_0', '_2': 'https://eyereasoner.github.io/.well-known/genid/test#sk_1', '_0': A, '_3': A}, [p(1), unify(A, A)])
step(p(1), clause(1), {}, [])
step(unify(A, A), 'builtin', {}, [])

=== lists and open lists
spec: 8.1
args: --goal "unify(L, [1, [2, 3], []])" --goal "unify(M, [1, *T])" --goal "unify(N, struct('.', 1, 'b'))"
--- stdin
from peye import *
--- stdout
unify([1, [2, 3], []], [1, [2, 3], []])
unify([1, *A], [1, *A])
unify([1, *'b'], [1, *'b'])

=== a compound named by an identifier is written as a call
spec: 8.2
--- program.py
from peye import *
fact(d(struct('Upper', 1)), d(struct('café', 'x')), d(struct('_hidden', 2)))
query(d(X))
--- stdout
d(Upper(1))
d(café('x'))
d(_hidden(2))

=== any other compound is written with struct
spec: 8.2
--- program.py
from peye import *
fact(d(struct('hello world', 1)), d(struct('from', 1)), d(struct('struct', 1)), d(struct('=', 1, 2)))
fact(d(struct('+', 1, 2, 3)), d(struct('.', 1)), d(struct('9lives', 0)))
query(d(X))
--- stdout
d(struct('hello world', 1))
d(struct('from', 1))
d(struct('struct', 1))
d(struct('=', 1, 2))
d(struct('+', 1, 2, 3))
d(struct('.', 1))
d(struct('9lives', 0))

=== binary operators and left associativity
spec: 8.2
--- program.py
from peye import *
fact(d(struct('+', 1, 2)), d(struct('-', struct('-', 1, 2), 3)), d(struct('-', 1, struct('-', 2, 3))))
fact(d(struct('*', struct('+', 1, 2), 3)), d(struct('+', 1, struct('*', 2, 3))), d(struct('%', 7, 2)))
fact(d(struct('//', 7, 2)), d(struct('/', 7, 2)), d(struct('<<', 1, 2)), d(struct('>>', 8, 1)), d(struct('^', 1, 2)))
query(d(X))
--- stdout
d(1 + 2)
d(1 - 2 - 3)
d(1 - (2 - 3))
d((1 + 2) * 3)
d(1 + 2 * 3)
d(7 % 2)
d(7 // 2)
d(7 / 2)
d(1 << 2)
d(8 >> 1)
d(1 ^ 2)

=== power is right associative and binds tighter than unary minus
spec: 8.2
--- program.py
from peye import *
fact(d(struct('**', 2, struct('**', 3, 2))), d(struct('**', struct('**', 2, 3), 2)))
fact(d(struct('-', struct('**', 2, 2))), d(struct('**', -2, 2)), d(struct('**', 2, -1)), d(struct('**', 2, struct('-', 'x'))))
query(d(X))
--- stdout
d(2 ** 3 ** 2)
d((2 ** 3) ** 2)
d(-2 ** 2)
d((-2) ** 2)
d(2 ** -1)
d(2 ** -'x')

=== unary operators
spec: 8.2
--- program.py
from peye import *
fact(d(struct('-', 'x')), d(struct('+', 1)), d(struct('~', 'g')), d(struct('-', struct('-', 'x'))), d(struct('-', struct('+', 1, 2))))
query(d(X))
--- stdout
d(-'x')
d(+1)
d(~'g')
d(--'x')
d(-(1 + 2))

=== minus applied to a number is written with struct
spec: 8.2
--- program.py
from peye import *
fact(d(struct('-', 1)), d(struct('-', -1)), d(struct('-', 2.5)))
query(d(X))
--- stdout
d(struct('-', 1))
d(struct('-', -1))
d(struct('-', 2.5))

=== conjunction, disjunction and negation
spec: 8.2
--- program.py
from peye import *
fact(d(struct(',', struct(',', 'a', 'b'), 'c')), d(struct(',', 'a', struct(',', 'b', 'c'))))
fact(d(struct(';', 'a', struct(',', 'b', 'c'))), d(struct(',', struct(';', 'a', 'b'), 'c')))
fact(d(struct('~', struct(',', 'a', 'b'))), d(struct(',', struct('~', 'a'), 'b')))
query(d(X))
--- stdout
d('a' & 'b' & 'c')
d('a' & ('b' & 'c'))
d('a' | 'b' & 'c')
d(('a' | 'b') & 'c')
d(~('a' & 'b'))
d(~'a' & 'b')

=== comparisons do not chain and bind looser than every other operator
spec: 8.2
--- program.py
from peye import *
fact(d(struct('<', struct('<', 1, 2), 3)), d(struct(',', struct('<', 1, 2), struct('>=', 3, 4))))
fact(d(struct('<=', struct('+', 1, 2), struct('|', 1, 2))), d(struct('<', 1, struct(';', 2, 3))))
query(d(X))
--- stdout
d((1 < 2) < 3)
d((1 < 2) & (3 >= 4))
d(1 + 2 <= struct('|', 1, 2))
d(1 < 2 | 3)

=== an open list's tail is parenthesized only when Python needs it
spec: 8.1, 8.2
--- program.py
from peye import *
fact(d(struct('.', 1, struct('<', 1, 2))), d(struct('.', 1, struct(';', 'a', 'b'))))
query(d(X))
--- stdout
d([1, *(1 < 2)])
d([1, *'a' | 'b'])

=== a negative number is parenthesized like a unary minus
spec: 8.2
--- program.py
from peye import *
fact(d(struct('-', 1, -1)), d(struct('-', -1, 1)), d(struct('*', -2, 3)))
query(d(X))
--- stdout
d(1 - -1)
d(-1 - 1)
d(-2 * 3)