diff --git a/src/liminate/analyzer.py b/src/liminate/analyzer.py index edb77a1..1e50646 100644 --- a/src/liminate/analyzer.py +++ b/src/liminate/analyzer.py @@ -266,8 +266,8 @@ def __init__(self, verb, field, op, kind, value, text, exception_text=None): self.verb = verb # "require" | "forbid" self.field = field # field name (str) self.op = op # normalized: "above" | "below" | "is" - self.kind = kind # "num" | "str" - self.value = value # int/float for "num", str for "str" + self.kind = kind # "num" | "str" | "pred" + self.value = value # int/float for "num", str for "str", predicate name for "pred" self.text = text # e.g. "require x is above 50" # v28 — rendering of the statement's `unless` exception condition, # if any, e.g. "approved is equal to yes". None when unguarded. @@ -290,6 +290,26 @@ def _extract_deontic(node) -> "_Deontic | None": its condition is out of scope (compound, non-name field, or a value that isn't a literal / bareword).""" cond = node.condition + if isinstance(cond, PredicateApplicationNode): + # Opaque-atom predicate awareness (Item 1). A predicate application is + # treated as a single indivisible fact `field is `. The + # detector cannot see the predicate body (deliberately unbuilt), but it + # can still reason that P and not-P are jointly unsatisfiable. Negated + # applications are out of scope — parity with the existing `not_*` + # operator exclusion for literals. + if cond.negated: + return None + if not isinstance(cond.subject, NameRef): + return None + field = cond.subject.name + verb = "require" if isinstance(node, RequireNode) else "forbid" + text = f"{verb} {field} is {cond.predicate_name}" + exception_text = None + if node.exception is not None: + exception_text = render(node.exception) + return _Deontic( + verb, field, "is", "pred", cond.predicate_name, text, exception_text, + ) # Compound conditions are out of scope — skip entirely (no leaf extraction). if not isinstance(cond, ConditionNode): return None @@ -361,8 +381,14 @@ def _pair_contradicts(a: _Deontic, b: _Deontic) -> bool: if above_val >= below_val: return True # Rule 4 — two equality requirements with different values can never - # both hold. - if a.op == "is" and b.op == "is" and not _values_equal(a, b): + # both hold. Predicates are opaque atoms: two different predicates (or + # a predicate and a literal) may well co-hold, so Rule 4 is suppressed + # whenever either side is a predicate application. + if ( + a.op == "is" and b.op == "is" + and a.kind != "pred" and b.kind != "pred" + and not _values_equal(a, b) + ): return True return False diff --git a/src/liminate/run.py b/src/liminate/run.py index aedee13..d220364 100644 --- a/src/liminate/run.py +++ b/src/liminate/run.py @@ -31,7 +31,7 @@ from .interpreter import HandlerTable, _infer_type_and_schema, execute from .lexer import LexError, leading_indent, tokenize from .listener import listen -from .parser import _ParseError, parse, parse_about, parse_when_block +from .parser import DefineNode, _ParseError, parse, parse_about, parse_when_block from .reorderer import reorder from .result import LiminateResult, ResultStatus from .vocabulary import ( @@ -417,8 +417,17 @@ def _collect_deontic_statements(lines: list[str]) -> list: context (compositions, packs) is never parsed here. Anything that fails to tokenize/reorder/parse is silently skipped: this pass is advisory and must never introduce an error the main loop wouldn't also produce. + + A single ordered scan also tracks `define` lines, accumulating predicate + names as they are declared, so a `require`/`forbid` that applies a named + predicate (`require account is high-risk`) parses to a + PredicateApplicationNode instead of misparsing as string equality. This + mirrors the forward-declaration rule the interpreter enforces via + `Session.predicate_names()`: a bareword is a predicate application only + if it was `define`d on a strictly earlier line. """ asts: list = [] + predicate_names: set[str] = set() for line in lines: stripped = line.lstrip() if not stripped or stripped.startswith("--"): @@ -429,6 +438,14 @@ def _collect_deontic_statements(lines: list[str]) -> list: toks = tokenize(line) except LexError: continue + if toks and toks[0].type is TokenType.DECLARATION and toks[0].value == "define": + reordered = reorder(toks) + if isinstance(reordered, LiminateResult): + continue + node = parse(reordered, predicate_names=predicate_names) + if isinstance(node, DefineNode): + predicate_names.add(node.name) + continue if not ( toks and toks[0].type is TokenType.VERB @@ -438,7 +455,7 @@ def _collect_deontic_statements(lines: list[str]) -> list: reordered = reorder(toks) if isinstance(reordered, LiminateResult): continue - ast = parse(reordered) + ast = parse(reordered, predicate_names=predicate_names) if isinstance(ast, LiminateResult): continue asts.append(ast) diff --git a/tests/test_contradiction_detection.py b/tests/test_contradiction_detection.py index 15cb7b9..d96fc89 100644 --- a/tests/test_contradiction_detection.py +++ b/tests/test_contradiction_detection.py @@ -231,3 +231,100 @@ def test_guarded_permit_still_never_contradicts(): "permit X is above 50 unless override is equal to yes", ]) assert w == [] + + +# --------------------------------------------------------------------------- +# Item 1 — opaque-atom predicate awareness (Definitional Era `define`) +# --------------------------------------------------------------------------- +# +# `warnings_for` parses each line independently via the module-level `_parse` +# (which calls `parse(reordered)` with no predicate table), so it CANNOT +# exercise predicate applications — a predicate line run through it would +# misparse exactly as the bug did. Predicate tests must go through the +# whole-program `run` path, which threads predicate names through the fixed +# pre-pass. + + +def program_warnings(source_lines): + """Collect contradiction warnings by running the whole-program loop, + which threads predicate names through the pre-pass. Required for any + program that uses `define` — the analyzer-only `warnings_for` helper + parses without a predicate table and would misparse `is `.""" + from liminate.run import run as run_program + source = "\n".join(source_lines) + contract = run_program(source, enter_phase2=False) + return [ + line + for r in contract.results + if r and r.output + for line in r.output + if line.startswith("⚠") + ] + + +def test_same_predicate_require_forbid_warns(): + """Same-predicate require/forbid warns — the sound P-and-not-P case.""" + w = program_warnings([ + "define big: is above 100", + "require X is big", + "forbid X is big", + ]) + assert len(w) == 1 + assert "contradiction" in w[0].lower() + + +def test_different_predicates_no_warning(): + """Different-predicate require/require does not warn — the + false-positive kill this build exists for.""" + w = program_warnings([ + "define big: is above 100", + "define positive: is above 0", + "require X is big", + "require X is positive", + ]) + assert w == [] + + +def test_predicate_and_literal_no_warning(): + """Predicate + literal require/require does not warn.""" + w = program_warnings([ + "define big: is above 100", + "require X is big", + "require X is 500", + ]) + assert w == [] + + +def test_pre_declaration_use_stays_string_equality(): + """A bareword used before its `define` is string equality at that + point — the pre-pass must agree with the interpreter's forward- + declaration rule, not treat it as a predicate application.""" + w = program_warnings([ + "require X is big", + "require X is 500", + "define big: is above 100", + ]) + assert len(w) == 1 + assert "require x is big" in w[0] + assert "require x is 500" in w[0] + + +def test_negated_predicate_application_out_of_scope(): + """`is not ` is out of scope for extraction — no warning.""" + w = program_warnings([ + "define big: is above 100", + "require X is big", + "forbid X is not big", + ]) + assert w == [] + + +def test_guarded_predicate_deontic_keeps_conditional_wording(): + """A guarded predicate deontic still gets conditional warning wording.""" + w = program_warnings([ + "define high-risk: is above 90", + "require X is high-risk", + "forbid X is high-risk unless approved is equal to yes", + ]) + assert len(w) == 1 + assert "unless approved is equal to yes" in w[0]