# SPEC 13: unused clauses, reported with the line their statement begins on.

=== clauses no conclusion rests on are unused
spec: 13
args: --unused program.py
--- program.py
from peye import *

fact(p('a'))
fact(q('b'))
implied_by(s(X), q(X))
fact(z('c'))
implies(p('a') & ~s('a'), 'ok')
--- stdout
unused(line(4), fact(q('b')))
unused(line(5), implied_by(s(X), q(X)))
unused(line(6), fact(z('c')))

=== a program whose every clause is used lists nothing
spec: 13
args: --unused program.py
--- program.py
from peye import *
fact(type('socrates', 'human'))
fact(subclass_of('human', 'mortal'))
implies(type(S, A) & subclass_of(A, B), type(S, B))
query(type(X, Y))
--- stdout

=== a clause a negation consults is used when leaving it out changes the conclusions
spec: 13
args: --unused program.py
--- program.py
from peye import *
fact(p('a'), p('b'))
fact(blocked('b'))
implies(p(X) & ~blocked(X), ok(X))
--- stdout
unused(line(2), fact(p('b')))

=== a clause a negation consults is unused when leaving it out changes nothing
spec: 13
args: --unused program.py
--- program.py
from peye import *
fact(p('a'))
fact(blocked('b'))
implies(p(X) & ~blocked(X), ok(X))
--- stdout
unused(line(3), fact(blocked('b')))

=== a clause a collection consults is used when leaving it out changes the conclusions
spec: 13
args: --unused program.py
--- program.py
from peye import *
fact(p(1), p(2))
implies(findall(X, p(X), L) & length(L, N), count(N))
fact(length([], 0))
implied_by(length([_, *T], N), length(T, M) & is_(N, M + 1))
--- stdout

=== a multi-line clause is reported with its first line
spec: 13
args: --unused program.py
--- program.py
from peye import *
fact(p(1))
implied_by(
    never(X),
    q(X),
)
query(p(X))
--- stdout
unused(line(3), implied_by(never(X), q(X)))

=== unused clauses are relative to the goals asked
spec: 13
args: --unused --goal "a(X)" program.py
--- program.py
from peye import *
fact(a(1))
fact(b(2))
--- stdout
unused(line(3), fact(b(2)))

=== a forward rule that concludes nothing is unused
spec: 13
args: --unused program.py
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
implies(s(X), r(X))
--- stdout
unused(line(4), implies(s(X), r(X)))

=== facts stated by facts_from record the line of the call
spec: 4.2, 13
args: --unused program.py
--- program.py
from peye import *
fact(p(1))
facts_from(text="q(1)\nq(2)\n")
implies(p(X), r(X))
--- stdout
unused(line(3), fact(q(1)))
unused(line(3), fact(q(2)))