claude-bot
ca98703538
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
49 lines
2.1 KiB
Python
49 lines
2.1 KiB
Python
"""Cheap static checks for formalizations that compile and are probably wrong.
|
||
|
||
These are a baseline for the fidelity filter, not a replacement for one: each looks
|
||
at the projected roles and the text of the declaration only, with no model and no
|
||
Lean. They catch encoding hazards (natural-number subtraction, integer division),
|
||
binders the statement never uses, and goals that say nothing.
|
||
"""
|
||
from __future__ import annotations
|
||
|
||
import re
|
||
|
||
from .project import Projection
|
||
from .schema import KIND_FACT, KIND_GOAL, KIND_OBJECT
|
||
|
||
_NAT = re.compile(r"\b(ℕ|Nat)\b")
|
||
_OTHER_NUMBERS = re.compile(r"[ℤℚℝℂ]|\b(Int|Rat|Real|Complex)\b")
|
||
_SUBTRACTION = re.compile(r"[\w)\]]\s*-\s*[\w(]")
|
||
_DIVISION = re.compile(r"[\w)\]]\s*/\s*[\w(]")
|
||
_IDENT = re.compile(r"[A-Za-z_][A-Za-z0-9_']*")
|
||
|
||
|
||
def lint(projection: Projection) -> list[str]:
|
||
findings: list[str] = []
|
||
if projection.degenerate:
|
||
findings.append("degenerate")
|
||
texts = [r.type_text for r in projection.roles if r.kind in (KIND_FACT, KIND_GOAL)]
|
||
body = " ".join(texts)
|
||
declared = " ".join(r.type_text for r in projection.roles if r.kind == KIND_OBJECT)
|
||
|
||
for role in projection.roles:
|
||
if role.kind != KIND_OBJECT or role.attrs.get("binder_kind") != "explicit":
|
||
continue
|
||
if role.type_text.strip().startswith(("Type", "Sort")):
|
||
continue # a carrier: used by the instances that constrain it
|
||
used = set(_IDENT.findall(body)) | set(_IDENT.findall(declared.replace(role.type_text, "")))
|
||
if role.name != "_" and role.name not in used:
|
||
findings.append(f"unused_binder:{role.name}")
|
||
|
||
nat_only = _NAT.search(declared + " " + body) and not _OTHER_NUMBERS.search(declared + body)
|
||
if nat_only and _SUBTRACTION.search(body):
|
||
findings.append("nat_subtraction")
|
||
if (_NAT.search(declared) or re.search(r"\b(ℤ|Int)\b", declared)) and _DIVISION.search(body):
|
||
findings.append("integer_division")
|
||
|
||
goal = next((r for r in projection.roles if r.kind == KIND_GOAL), None)
|
||
if goal is not None and goal.type_text.strip() in ("", "True", "False", "1 = 1", "0 = 0"):
|
||
findings.append("trivial_goal")
|
||
return findings
|