Add public check_source() and export the checker API

src/liminate/__init__.py

@@ -13,6 +13,7 @@
     TestDomainPack,
 )
 from .analyzer import SymbolEntry, analyze
+from .checker import CheckerUnavailable, CheckResult, Finding, check_agreement, check_source
 from .interpreter import execute
 from .listener import listen
 from .lexer import leading_indent, tokenize
@@ -27,8 +28,11 @@
     "AdapterDone",
     "AdapterFailure",
     "AdapterUpdate",
+    "CheckResult",
+    "CheckerUnavailable",
     "ContractResult",
     "DomainPack",
+    "Finding",
     "LiminateResult",
     "LiveValueDeclaration",
     "LiveValueEntry",
@@ -39,6 +43,8 @@
     "TestAdapter",
     "TestDomainPack",
     "analyze",
+    "check_agreement",
+    "check_source",
     "execute",
     "leading_indent",
     "listen",

src/liminate/checker.py

@@ -23,6 +23,7 @@
 from dataclasses import dataclass
 from datetime import date
 
+from .lexer import LexError, leading_indent, tokenize
 from .parser import (
     ArithmeticNode,
     BareWord,
@@ -42,8 +43,13 @@
     RememberValueNode,
     RequireNode,
     SequenceNode,
+    parse,
 )
 from .renderer import render
+from .reorderer import reorder
+from .result import LiminateResult
+from .run import run
+from .vocabulary import TokenType
 
 
 class CheckerUnavailable(Exception):
@@ -927,3 +933,130 @@ def check_agreement(statements, symbol_table) -> CheckResult:
         elapsed_ms=(time.monotonic() - start) * 1000,
         encodable=True, skipped_reason=None,
     )
+
+
+# ---------------------------------------------------------------------------
+# check_source — static inspection from contract text (Halverson dry run,
+# liminate-dev PR #89, product findings 1/2)
+# ---------------------------------------------------------------------------
+
+# check_agreement's _VERB_NAMES covers all four deontic verbs — widened
+# from run._collect_deontic_statements's ("require", "forbid"), which only
+# needs two for its narrower contradiction-detection use case.
+_CHECK_DEONTIC_VERBS = ("require", "forbid", "permit", "expect")
+
+
+def _collect_checkable_statements(source: str) -> list:
+    """Best-effort pre-pass collecting the top-level statement ASTs
+    check_agreement needs from raw contract text: every `define`,
+    `require`, `forbid`, `permit`, `expect`, and value-form `remember`
+    line at indent 0.
+
+    Deliberately NOT a thin wrapper around run._collect_deontic_statements
+    — reusing that collector as-is silently breaks two of check_agreement's
+    seven checks:
+
+    1. `define` lines: run._collect_deontic_statements accumulates the
+       name into a local predicate_names set (so later require/forbid
+       applications parse correctly) and then `continue`s WITHOUT
+       appending the DefineNode. check_agreement's check 7
+       (_check_constant_predicate) iterates DefineNode from the statement
+       list — a collector that drops it yields a silent zero-finding
+       result for check 7, not an error.
+    2. `remember ... with/from <value>` lines that parse to a
+       RememberValueNode: _build_definitions scans the statement list for
+       these to build the name -> defining-expression map that
+       value-position name inlining (TI-Q13 closure) depends on. Without
+       them, nonlinear arithmetic reached through a name (e.g. `remember
+       a value called doubled from beta multiplied by beta`, then
+       `forbid x is above doubled`) is silently never caught.
+
+    run._collect_deontic_statements itself is untouched — its output feeds
+    detect_contradictions in the live run() path, and changing what it
+    returns would alter contradiction-detection behavior for every
+    program. This is a deliberate duplicate of its scan structure, not a
+    shared helper, for exactly that reason.
+
+    Anything that fails to tokenize/reorder/parse is silently skipped —
+    this pass is advisory and must never introduce an error check_source's
+    own run() call wouldn't also produce. Indented lines (when-block
+    action lines) are excluded, matching the forward-declaration rule for
+    predicate names run._collect_deontic_statements also follows.
+    """
+    statements: list = []
+    predicate_names: set[str] = set()
+    for line in source.splitlines():
+        stripped = line.lstrip()
+        if not stripped or stripped.startswith("--"):
+            continue
+        try:
+            if leading_indent(line) != 0:
+                continue
+            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)
+                statements.append(node)
+            continue
+
+        if not (toks and toks[0].type is TokenType.VERB):
+            continue
+        verb = toks[0].value
+        if verb not in _CHECK_DEONTIC_VERBS and verb != "remember":
+            continue
+
+        reordered = reorder(toks)
+        if isinstance(reordered, LiminateResult):
+            continue
+        node = parse(reordered, predicate_names=predicate_names)
+        if isinstance(node, LiminateResult):
+            continue
+
+        if verb == "remember":
+            if isinstance(node, RememberValueNode):
+                statements.append(node)
+            continue
+
+        statements.append(node)
+    return statements
+
+
+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.
+
+    Runs `run(source, domain_packs=domain_packs, enter_phase2=False,
+    auto_confirm_amber=True)` to populate a symbol table without entering
+    Phase 2 (this is static inspection, not execution — no listener, no
+    I/O) and without leaving an amber outcome unresolved. Collects the
+    top-level define/require/forbid/permit/expect/remember statement ASTs
+    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.
+
+    Never catches `CheckerUnavailable` — it propagates exactly as
+    `check_agreement` raises it (z3 not installed). An out-of-fragment
+    program is not an error either: `check_agreement` reports it as
+    `CheckResult(encodable=False, skipped_reason=...)`, passed through
+    unchanged. A program that fails to parse entirely collects zero
+    statements and reports `checked=0` with no findings — also not an
+    error; a caller wanting parse diagnostics should call `run()`.
+    """
+    contract_result = run(
+        source,
+        domain_packs=domain_packs,
+        enter_phase2=False,
+        auto_confirm_amber=True,
+    )
+    statements = _collect_checkable_statements(source)
+    return check_agreement(statements, contract_result.symbol_table)

tests/test_checker.py

@@ -1002,3 +1002,145 @@ def test_check_agreement_descends_into_sequence_node():
     result = checker.check_agreement([seq], symtab)
     assert result.encodable is True
     assert any(f.kind == "always_deny" for f in result.findings)
+
+
+# ---------------------------------------------------------------------------
+# Phase 8 — check_source: public export + text-in, CheckResult-out
+# ---------------------------------------------------------------------------
+
+
+def test_liminate_package_importable_without_z3():
+    """`import liminate` must succeed even when z3 cannot be imported at
+    all — mirrors test_checker_module_importable_without_z3 above, but for
+    the package root now that it re-exports names from checker.py."""
+    script = (
+        "import sys, builtins\n"
+        "_orig_import = builtins.__import__\n"
+        "def _blocked(name, *a, **k):\n"
+        "    if name == 'z3' or name.startswith('z3.'):\n"
+        "        raise ImportError('z3 not installed (simulated)')\n"
+        "    return _orig_import(name, *a, **k)\n"
+        "builtins.__import__ = _blocked\n"
+        "import liminate\n"
+        "assert callable(liminate.check_agreement)\n"
+        "assert callable(liminate.check_source)\n"
+        "print('IMPORT_OK')\n"
+    )
+    result = subprocess.run(
+        [sys.executable, "-c", script], capture_output=True, text=True
+    )
+    assert result.returncode == 0, result.stderr
+    assert "IMPORT_OK" in result.stdout
+
+
+def test_check_agreement_and_friends_exported_from_package():
+    import liminate
+
+    assert liminate.check_agreement is checker.check_agreement
+    assert liminate.CheckResult is checker.CheckResult
+    assert liminate.Finding is checker.Finding
+    assert liminate.CheckerUnavailable is checker.CheckerUnavailable
+    assert liminate.check_source is checker.check_source
+    for name in (
+        "CheckerUnavailable", "CheckResult", "Finding",
+        "check_agreement", "check_source",
+    ):
+        assert name in liminate.__all__
+
+
+def test_check_source_finds_unless_swallows_rule():
+    source = "\n".join([
+        "remember a number called amount with 10",
+        "forbid amount is above 1000 unless amount is above 0",
+    ])
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is True
+    kinds = [f.kind for f in result.findings]
+    assert "unless_swallows_rule" in kinds
+
+
+def test_check_source_finds_constant_predicate_regression_for_define_node():
+    """Regression test for the DefineNode trap: a naive collector built on
+    run._collect_deontic_statements tracks `define` names into
+    predicate_names but never appends the DefineNode itself, so check 7
+    (_check_constant_predicate, which iterates DefineNode from the
+    statement list) silently finds nothing. This program has zero
+    require/forbid/permit/expect statements — checked stays 0 — but must
+    still surface the constant_predicate finding for the tautological
+    `define`."""
+    source = "define always_big_or_small: is above 0 or is below 1000000"
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is True
+    assert result.checked == 0
+    kinds = [f.kind for f in result.findings]
+    assert "constant_predicate" in kinds
+
+
+def test_check_source_threads_predicate_names_matches_hand_built_ast():
+    """Both require and forbid apply the named predicate `big` to the same
+    field — proves check_source's collector threads predicate_names the
+    same way a hand-built AST list (built exactly like the rest of this
+    file's tests do, via _parse_line with predicate_names threaded by
+    hand) would, rather than misparsing `is big` as string equality."""
+    lines = [
+        "remember a number called cutoff with 100",
+        "define big: is above cutoff",
+        "remember a number called amount with 150",
+        "require amount is big",
+        "forbid amount is big",
+    ]
+    source = "\n".join(lines)
+    session, results = run_lines(lines)
+    for r in results:
+        assert r.status.name in ("SUCCESS", "PROHIBITION_VIOLATED"), r.message
+
+    predicate_names = set()
+    define_ast = _parse_line(lines[1], predicate_names=predicate_names)
+    predicate_names.add(define_ast.name)
+    hand_built = [
+        define_ast,
+        _parse_line(lines[3], predicate_names=predicate_names),
+        _parse_line(lines[4], predicate_names=predicate_names),
+    ]
+
+    expected = checker.check_agreement(hand_built, session.symtab)
+    actual = checker.check_source(source)
+
+    assert actual.encodable == expected.encodable
+    assert actual.checked == expected.checked
+    assert [(f.kind, f.severity, f.statements) for f in actual.findings] == [
+        (f.kind, f.severity, f.statements) for f in expected.findings
+    ]
+    assert [f.kind for f in actual.findings] == ["require_forbid_conflict"]
+
+
+def test_check_source_out_of_fragment_nonlinear_via_remembered_name():
+    """Doubles as the RememberValueNode-collection regression test: the
+    nonlinearity in `doubled`'s definition (beta multiplied by beta, both
+    runtime names) is only visible to check_agreement if the collector
+    appended `doubled`'s RememberValueNode into the statement list for
+    _build_definitions to find. A collector that only gathers deontic
+    verbs (dropping value-form remember lines) would hand check_agreement
+    a `doubled` that resolves to an opaque, already-allocated constant —
+    missing the nonlinear multiplication entirely and reporting a clean
+    (wrong) bill of health instead of encodable=False."""
+    source = "\n".join([
+        "remember a number called alpha with 10",
+        "remember a number called beta with 2",
+        "remember a value called doubled from beta multiplied by beta",
+        "forbid alpha is above doubled",
+    ])
+    result = checker.check_source(source)
+    assert isinstance(result, checker.CheckResult)
+    assert result.encodable is False
+    assert result.skipped_reason is not None
+    assert "doubled" in result.skipped_reason
+
+
+def test_check_source_unparseable_source_returns_checked_zero_no_raise():
+    result = checker.check_source("gibberish nonsense flarn blorp")
+    assert isinstance(result, checker.CheckResult)
+    assert result.checked == 0
+    assert result.findings == []