Make check_source work on unbound rule templates

src/liminate/checker.py

@@ -23,6 +23,7 @@
 from dataclasses import dataclass
 from datetime import date
 
+from .analyzer import SymbolEntry
 from .lexer import LexError, leading_indent, tokenize
 from .parser import (
     ArithmeticNode,
@@ -1028,6 +1029,129 @@ def _collect_checkable_statements(source: str) -> list:
     return statements
 
 
+# ---------------------------------------------------------------------------
+# check_source's type-inference pre-pass — unbound rule templates
+# ---------------------------------------------------------------------------
+#
+# A Translate draft — and every shipped agreement template in
+# liminate-dev's app/agreement_templates.py — is an *unbound rule
+# template* by design: it references evidence fields (amount,
+# manager-approval, ...) that no `remember` binds, so run()'s symbol table
+# has no entry for them. _build_constants then allocates nothing for the
+# missing name, and encode_field raises UnencodableConstruct the first
+# time a condition actually touches it, so check_source reported
+# encodable=False for every such template (Halverson dry run, liminate-dev
+# PR #89, finding 1).
+#
+# This pass synthesizes type-only placeholder SymbolEntry objects
+# (value=None — the Z3 encoder only reads the type, in _build_constants,
+# to allocate a free constant) for referenced-but-unbound fields, inferred
+# from how each field is used: a literal it's directly compared against,
+# or, for `<subject> is <predicate>`, the predicate's own body. A field
+# typed by neither path stays unresolved and still raises
+# UnencodableConstruct at check time — that is invariant 8 working
+# correctly, not a gap to paper over. A real `remember`/`define` binding
+# always wins over an inferred placeholder (see the `name not in
+# symbol_table` guard in check_source below).
+#
+# Ported from case-studies/halverson/check-output/check_harness.py in
+# liminate-dev (the working prototype), adapted to checker.py's naming.
+#
+# Known limit: the heuristic below is exercised against the Halverson
+# corpus's condition shapes only. FieldAccessNode on records, and the
+# `within` / `includes` operators, were never hit by that corpus and are
+# not covered here — a field reached only through one of those shapes
+# stays unresolved. Generalizing beyond what that corpus proved is
+# separate work.
+
+
+def _condition_leaves(node):
+    """Yield every ConditionNode/PredicateApplicationNode leaf inside a
+    condition tree, descending CompoundConditionNode's and/or shape."""
+    if isinstance(node, CompoundConditionNode):
+        yield from _condition_leaves(node.left)
+        yield from _condition_leaves(node.right)
+    elif isinstance(node, (ConditionNode, PredicateApplicationNode)):
+        yield node
+
+
+def _literal_type(value_node) -> str | None:
+    if isinstance(value_node, NumberLiteral):
+        return "number"
+    if isinstance(value_node, DateLiteral):
+        return "date"
+    if isinstance(value_node, (QuotedString, BareWord)):
+        return "string"
+    return None
+
+
+def _predicate_subject_types(statements: list) -> dict[str, str]:
+    """For each `define <name>: <condition>`, infer the scalar type a
+    subject must have to be applied to it via `<subject> is <name>` —
+    mirrors _Encoder._value_sort_hint / _infer_subject_sort (used by check
+    7's standalone predicate-body encoding), but runs pre-encoding on raw
+    ASTs rather than during Z3 constant allocation. E.g. `define large: is
+    above 5000` implies a number subject."""
+    subject_types: dict[str, str] = {}
+
+    def hint(cond) -> str | None:
+        if isinstance(cond, CompoundConditionNode):
+            return hint(cond.left) or hint(cond.right)
+        if isinstance(cond, ConditionNode) and isinstance(cond.field, EachPronoun):
+            t = _literal_type(cond.value)
+            if t is None and cond.value2 is not None:
+                t = _literal_type(cond.value2)
+            return t
+        return None
+
+    for stmt in statements:
+        if isinstance(stmt, DefineNode):
+            t = hint(stmt.condition)
+            if t is not None:
+                subject_types[stmt.name] = t
+    return subject_types
+
+
+_INFERABLE_DEONTIC_TYPES = (RequireNode, ForbidNode, PermitNode, ExpectNode)
+
+
+def _infer_field_types(statements: list) -> dict[str, str]:
+    """Walk every deontic condition, exception, and define body for a bare
+    NameRef field and infer a scalar type — from the literal it's directly
+    compared against, or, for a predicate application (`<subject> is
+    <name>`), from the predicate's own body via `_predicate_subject_types`.
+    First inference wins; a field typed by neither path is simply absent
+    from the result and stays unresolved (raises UnencodableConstruct at
+    check time, same as any other out-of-fragment reference)."""
+    types: dict[str, str] = {}
+    subject_types = _predicate_subject_types(statements)
+
+    def note(name: str, scalar_type: str | None) -> None:
+        if scalar_type is not None:
+            types.setdefault(name, scalar_type)
+
+    def walk_condition(cond) -> None:
+        for leaf in _condition_leaves(cond):
+            if isinstance(leaf, ConditionNode) and isinstance(leaf.field, NameRef):
+                note(leaf.field.name, _literal_type(leaf.value))
+                if leaf.value2 is not None:
+                    note(leaf.field.name, _literal_type(leaf.value2))
+            elif isinstance(leaf, PredicateApplicationNode) and isinstance(
+                leaf.subject, NameRef
+            ):
+                note(leaf.subject.name, subject_types.get(leaf.predicate_name))
+
+    for stmt in statements:
+        if isinstance(stmt, DefineNode):
+            walk_condition(stmt.condition)
+        elif isinstance(stmt, _INFERABLE_DEONTIC_TYPES):
+            walk_condition(stmt.condition)
+            if stmt.exception is not None:
+                walk_condition(stmt.exception)
+
+    return types
+
+
 def check_source(source: str, *, domain_packs=None) -> CheckResult:
     """Static inspection of contract text: check_agreement, wired up from
     source instead of hand-built statements + a symbol table.
@@ -1040,9 +1164,21 @@ def check_source(source: str, *, domain_packs=None) -> CheckResult:
     from the same source text — see `_collect_checkable_statements`; in
     particular, `define` and value-form `remember` lines must both be
     collected, or check 7 and nonlinearity detection silently go inert.
-    Hands both to `check_agreement` and returns its `CheckResult`
-    unchanged — no wrapping, no extra fields. A caller that also needs
-    the symbol table calls `run()` directly instead.
+
+    A contract source is very often an *unbound rule template* — it
+    references evidence fields no `remember` in the source ever binds, so
+    run()'s symbol table has no entry for them. Before handing off to
+    check_agreement, this function adds a type-only placeholder
+    SymbolEntry (see `_infer_field_types`) for every referenced-but-unbound
+    field it can infer a scalar type for; a real binding from `run()`
+    always takes precedence. A field neither bound nor inferable is left
+    alone and still surfaces as `encodable=False` from check_agreement's
+    own UnencodableConstruct boundary.
+
+    Hands the (possibly widened) symbol table and the collected statements
+    to `check_agreement` and returns its `CheckResult` unchanged — no
+    wrapping, no extra fields. A caller that also needs the real symbol
+    table calls `run()` directly instead.
 
     Never catches `CheckerUnavailable` — it propagates exactly as
     `check_agreement` raises it (z3 not installed). An out-of-fragment
@@ -1059,4 +1195,8 @@ def check_source(source: str, *, domain_packs=None) -> CheckResult:
         auto_confirm_amber=True,
     )
     statements = _collect_checkable_statements(source)
-    return check_agreement(statements, contract_result.symbol_table)
+    symbol_table = dict(contract_result.symbol_table)
+    for name, scalar_type in _infer_field_types(statements).items():
+        if name not in symbol_table:
+            symbol_table[name] = SymbolEntry(name=name, value=None, type=scalar_type)
+    return check_agreement(statements, symbol_table)

tests/test_checker.py

@@ -1144,3 +1144,102 @@ def test_check_source_unparseable_source_returns_checked_zero_no_raise():
     assert isinstance(result, checker.CheckResult)
     assert result.checked == 0
     assert result.findings == []
+
+
+# ---------------------------------------------------------------------------
+# Phase 9 — check_source's type-inference pre-pass for unbound rule
+# templates (Halverson dry run, liminate-dev PR #89, finding 1)
+# ---------------------------------------------------------------------------
+
+
+def test_check_source_encodes_unbound_template_and_finds_violation():
+    """Regression test for the whole stage: before the type-inference
+    pre-pass, check_source(source) passed run()'s symbol table straight to
+    check_agreement, and a field no `remember` ever bound (here, `amount`)
+    raised UnencodableConstruct at encode_field, reported as
+    encodable=False. `amount` is only ever referenced, never bound — the
+    inference pass must type it from the literal `5000` and the check must
+    still find the genuine unless_swallows_rule violation."""
+    source = 'forbid amount is above 5000 unless amount is above 0 because "policy"'
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is True
+    assert result.skipped_reason is None
+    kinds = [f.kind for f in result.findings]
+    assert "unless_swallows_rule" in kinds
+
+
+def test_check_source_encodes_real_shipped_vendor_invoice_review_template():
+    """The exact template shipped in liminate-dev's
+    app/agreement_templates.py (AGREEMENT_TEMPLATES, id
+    'vendor_invoice_review'), copied verbatim rather than imported across
+    repos. Every evidence field it references — amount, manager-approval,
+    purchase-order, approval-status — has no `remember` binding it
+    anywhere in the source; this is the exact document finding 1 verified
+    against and must be encodable now."""
+    source = "\n".join([
+        'remember a string called agreement-purpose with "vendor invoice review"',
+        "define large: is above 5000",
+        'require amount is above 0 because "an invoice must have a positive amount"',
+        'forbid amount is large unless manager-approval is equal to "yes" '
+        'because "large invoices need manager sign-off"',
+        'require purchase-order is equal to "matched" because '
+        '"every invoice must match a PO"',
+        'permit approval-status is equal to "ready" because '
+        '"all invoice criteria are met"',
+    ])
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is True
+    assert result.skipped_reason is None
+
+
+def test_check_source_real_remember_not_overwritten_by_inference():
+    """A field bound by a real `remember` (here, `amount` as a number)
+    must win over the inference pass, even when the inferred type from a
+    literal comparison elsewhere in the source would disagree (here,
+    comparing `amount` against a quoted string would infer 'string'). If
+    the placeholder ever overwrote the real binding, this program would
+    encode cleanly as a same-sort string comparison; because the real
+    number binding takes precedence, comparing a Real constant against a
+    StringVal is a genuine sort mismatch and must be reported as
+    encodable=False, not silently swallowed (invariant 8)."""
+    source = "\n".join([
+        "remember a number called amount with 3000",
+        'forbid amount is equal to "five thousand" because "policy"',
+    ])
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is False
+    assert result.skipped_reason is not None
+
+
+def test_check_source_field_typed_only_via_predicate_application():
+    """`amount` is never compared against a literal directly — its only
+    appearance is `amount is large`, a PredicateApplicationNode. The type
+    must be resolved through `large`'s own body (`is above 5000`, a number
+    comparison) via `_predicate_subject_types`, not left unresolved."""
+    source = "\n".join([
+        "define large: is above 5000",
+        'forbid amount is large because "policy"',
+    ])
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is True
+    assert result.skipped_reason is None
+    assert result.checked == 1
+
+
+def test_check_source_untypeable_field_stays_encodable_false_no_raise():
+    """`category` is referenced only via `includes`, whose target must be
+    a statically known list (a real list_of_* symbol-table entry) — the
+    inference pass only ever produces scalar (number/string/date)
+    placeholders, so `category` stays untypeable for this purpose and the
+    program must still surface as encodable=False through check_agreement's
+    normal UnencodableConstruct boundary, never raise."""
+    source = 'forbid category includes "restricted" because "policy"'
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is False
+    assert result.skipped_reason is not None
+    assert result.findings == []