claude-bot
ca98703538
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
261 lines
9.7 KiB
Python
261 lines
9.7 KiB
Python
"""Read a Lean declaration's parameters as roles.
|
||
|
||
``project(code)`` is deterministic and never calls Lean or a model. It splits the
|
||
signature into
|
||
|
||
* **objects** explicit/implicit binders whose type is data or a sort: ``(G : Type*)``,
|
||
``(n : ℕ)``; instance binders ``[Group G]`` attach to the object they
|
||
constrain (``attrs["instances"]``);
|
||
* **facts** binders whose type is a proposition: ``(h : a ∣ b)``, and, when the goal
|
||
is an implication, its premises;
|
||
* **goal** the conclusion of a theorem, or **own** for what a definition is.
|
||
|
||
Leading ``∀`` binders of the goal are unpacked into objects, so ``(n : ℕ) : n = n`` and
|
||
``∀ n : ℕ, n = n`` project to the same roles. Whether a binder is a fact is decided by
|
||
a syntactic heuristic (relation symbols, known predicate heads, the ``h…`` naming
|
||
convention) and every role records how it was decided in ``attrs["classified_by"]``,
|
||
so the heuristic's accuracy can be measured against a manual parse.
|
||
"""
|
||
from __future__ import annotations
|
||
|
||
import re
|
||
from dataclasses import dataclass, field
|
||
from typing import Any
|
||
|
||
from .schema import (
|
||
KIND_FACT,
|
||
KIND_GOAL,
|
||
KIND_OBJECT,
|
||
KIND_OWN,
|
||
Role,
|
||
Simplex,
|
||
)
|
||
from .typeindex import _DECL, _IDENT, PROOF_KEYWORDS, _split_top_level, _strip_comments
|
||
|
||
OPENERS = {"(": ")", "{": "}", "[": "]", "⦃": "⦄", "⟨": "⟩"}
|
||
CLOSERS = set(OPENERS.values())
|
||
BINDER_KIND = {"(": "explicit", "{": "implicit", "⦃": "strict_implicit", "[": "instance"}
|
||
|
||
_SORT = re.compile(r"^(Type|Sort)(\b|\*|_)")
|
||
_RELATION = re.compile(r"[=≠<>≤≥∣∈∉⊆⊂⊇⊃≡∧∨¬↔∀∃≃≅≈]|\bTrue\b|\bFalse\b")
|
||
_PROP_HEAD = re.compile(
|
||
r"^(Is[A-Z]\w*|Nat\.Prime|Prime|Nat\.Coprime|Int\.Coprime|Coprime|Function\.\w+|"
|
||
r"Injective|Surjective|Bijective|Continuous\w*|Differentiable\w*|Monotone\w*|Antitone\w*|"
|
||
r"Finite|Set\.Finite|Set\.Infinite|Infinite|Odd|Even|Irreducible|Squarefree|"
|
||
r"Nonempty|Set\.Nonempty|Nat\.Even|Nat\.Odd)\b"
|
||
)
|
||
_HYPOTHESIS_NAME = re.compile(r"^h[\w'₀-₉]*$")
|
||
|
||
|
||
def _split_depth0(text: str, separator: str) -> list[str]:
|
||
"""Split on ``separator`` outside every bracket pair."""
|
||
parts: list[str] = []
|
||
depth = 0
|
||
start = 0
|
||
for index, char in enumerate(text):
|
||
if char in OPENERS:
|
||
depth += 1
|
||
elif char in CLOSERS:
|
||
depth = max(0, depth - 1)
|
||
elif depth == 0 and text.startswith(separator, index):
|
||
parts.append(text[start:index])
|
||
start = index + len(separator)
|
||
parts.append(text[start:])
|
||
return parts
|
||
|
||
|
||
def _first_depth0(text: str, needle: str) -> int:
|
||
depth = 0
|
||
for index, char in enumerate(text):
|
||
if char in OPENERS:
|
||
depth += 1
|
||
elif char in CLOSERS:
|
||
depth = max(0, depth - 1)
|
||
elif depth == 0 and text.startswith(needle, index):
|
||
if needle == ":" and text.startswith(":=", index):
|
||
continue
|
||
return index
|
||
return -1
|
||
|
||
|
||
def classify(type_text: str, names: list[str], objects: set[str]) -> tuple[str, str]:
|
||
"""(kind, how) for a binder with these names and this type."""
|
||
text = type_text.strip()
|
||
if not text:
|
||
return KIND_OBJECT, "untyped"
|
||
if _SORT.match(text):
|
||
return KIND_OBJECT, "sort"
|
||
if _RELATION.search(text):
|
||
return KIND_FACT, "relation"
|
||
if _PROP_HEAD.match(text):
|
||
return KIND_FACT, "predicate"
|
||
if names and all(_HYPOTHESIS_NAME.match(n) for n in names):
|
||
tokens = {t for t in _IDENT.findall(text) if t[:1].islower()}
|
||
if tokens & objects:
|
||
return KIND_FACT, "name"
|
||
return KIND_OBJECT, "default"
|
||
|
||
|
||
@dataclass
|
||
class Projection:
|
||
name: str
|
||
keyword: str
|
||
roles: list[Role] = field(default_factory=list)
|
||
simplex: Simplex | None = None
|
||
notes: list[str] = field(default_factory=list)
|
||
|
||
@property
|
||
def degenerate(self) -> bool:
|
||
return self.simplex is None
|
||
|
||
def by_kind(self, kind: str) -> list[Role]:
|
||
return [r for r in self.roles if r.kind == kind]
|
||
|
||
def as_dict(self) -> dict[str, Any]:
|
||
return {
|
||
"name": self.name,
|
||
"keyword": self.keyword,
|
||
"degenerate": self.degenerate,
|
||
"roles": [r.as_dict() for r in self.roles],
|
||
"notes": self.notes,
|
||
}
|
||
|
||
|
||
def _cut_signature(rest: str) -> str:
|
||
depth = 0
|
||
for index, char in enumerate(rest):
|
||
if char in OPENERS:
|
||
depth += 1
|
||
elif char in CLOSERS:
|
||
depth = max(0, depth - 1)
|
||
elif depth == 0:
|
||
if rest.startswith(":=", index) or rest.startswith("\nwhere", index):
|
||
return rest[:index]
|
||
if rest.startswith(" where", index) and index > 0:
|
||
return rest[:index]
|
||
return rest
|
||
|
||
|
||
def _roles_from_group(opener: str, inner: str, objects: set[str], origin: str) -> list[Role]:
|
||
binder_kind = BINDER_KIND.get(opener, "explicit")
|
||
head, _, tail = inner.partition(":")
|
||
names = head.split()
|
||
type_text = tail.strip() if ":" in inner else ""
|
||
if not names or any(not _IDENT.fullmatch(n) and n != "_" for n in names):
|
||
return []
|
||
kind, how = classify(type_text, names, objects)
|
||
roles = []
|
||
for name in names:
|
||
attrs = {"binder_kind": binder_kind, "classified_by": how, "origin": origin}
|
||
roles.append(Role(name, kind, type_text=type_text, attrs=attrs))
|
||
if kind == KIND_OBJECT:
|
||
objects.add(name)
|
||
return roles
|
||
|
||
|
||
def _attach_instance(inner: str, roles: dict[str, Role], notes: list[str]) -> None:
|
||
text = inner.split(":", 1)[1].strip() if ":" in inner else inner.strip()
|
||
owner = None
|
||
for token in _IDENT.findall(text):
|
||
if token in roles and roles[token].kind == KIND_OBJECT:
|
||
owner = roles[token]
|
||
if owner is None:
|
||
notes.append(f"instance [{text}] constrains no named object")
|
||
return
|
||
owner.attrs.setdefault("instances", []).append(text)
|
||
|
||
|
||
def _unpack_forall(goal: str, objects: set[str]) -> tuple[list[Role], str]:
|
||
"""Lift leading ``∀`` binders of the goal into object/fact roles."""
|
||
lifted: list[Role] = []
|
||
text = goal.strip()
|
||
while text.startswith("∀"):
|
||
body = text[1:].lstrip()
|
||
comma = _first_depth0(body, ",")
|
||
if comma < 0:
|
||
break
|
||
binders, text = body[:comma].strip(), body[comma + 1 :].strip()
|
||
groups = _split_top_level(binders)
|
||
if groups and binders.startswith(tuple(OPENERS)):
|
||
for opener, inner in groups:
|
||
lifted.extend(_roles_from_group(opener, inner, objects, "forall_in_goal"))
|
||
continue
|
||
bound = re.match(r"^([\w'₀-₉ ]+?)\s*(∈|∉|<|≤|>|≥|≠)\s*(.+)$", binders)
|
||
if bound and ":" not in binders:
|
||
for name in bound.group(1).split():
|
||
lifted.append(Role(name, KIND_OBJECT, attrs={
|
||
"binder_kind": "explicit", "classified_by": "bounded", "origin": "forall_in_goal"}))
|
||
objects.add(name)
|
||
lifted.append(Role(
|
||
f"h_{name}", KIND_FACT, type_text=f"{name} {bound.group(2)} {bound.group(3)}",
|
||
attrs={"binder_kind": "explicit", "classified_by": "bounded",
|
||
"origin": "forall_in_goal"}))
|
||
continue
|
||
lifted.extend(_roles_from_group("(", binders, objects, "forall_in_goal"))
|
||
return lifted, text
|
||
|
||
|
||
def project(code: str) -> Projection:
|
||
clean = _strip_comments(code)
|
||
match = _DECL.search(clean)
|
||
if not match:
|
||
return Projection("", "", notes=["no declaration found"])
|
||
keyword, name = match.group(1), match.group(2)
|
||
result = Projection(name, keyword)
|
||
signature = _cut_signature(clean[match.end() :])
|
||
|
||
colon = _first_depth0(signature, ":")
|
||
binder_text = signature if colon < 0 else signature[:colon]
|
||
goal_text = "" if colon < 0 else signature[colon + 1 :].strip()
|
||
|
||
objects: set[str] = set()
|
||
named: dict[str, Role] = {}
|
||
instances: list[str] = []
|
||
for opener, inner in _split_top_level(binder_text):
|
||
if opener == "[":
|
||
instances.append(inner)
|
||
continue
|
||
if opener == "⟨":
|
||
continue
|
||
for role in _roles_from_group(opener, inner, objects, "binder"):
|
||
result.roles.append(role)
|
||
named[role.name] = role
|
||
for inner in instances:
|
||
_attach_instance(inner, named, result.notes)
|
||
|
||
if keyword in PROOF_KEYWORDS:
|
||
lifted, goal_text = _unpack_forall(goal_text, objects)
|
||
for role in lifted:
|
||
result.roles.append(role)
|
||
named[role.name] = role
|
||
parts = _split_depth0(goal_text, "→") if goal_text else []
|
||
if len(parts) >= 2:
|
||
for index, premise in enumerate(parts[:-1], start=1):
|
||
result.roles.append(Role(
|
||
f"premise{index}", KIND_FACT, type_text=premise.strip(),
|
||
attrs={"binder_kind": "goal_implication", "classified_by": "implication",
|
||
"origin": "goal"}))
|
||
goal_text = parts[-1].strip()
|
||
result.roles.append(Role(
|
||
"goal", KIND_GOAL, type_text=goal_text,
|
||
attrs={
|
||
"exists_count": goal_text.count("∃"),
|
||
"forall_count": goal_text.count("∀"),
|
||
"is_iff": "↔" in goal_text,
|
||
}))
|
||
else:
|
||
result.roles.append(Role(
|
||
"own", KIND_OWN, type_text=goal_text or keyword, attrs={"keyword": keyword}))
|
||
|
||
seen: dict[str, int] = {}
|
||
aliased: dict[str, Role] = {}
|
||
for role in result.roles:
|
||
count = seen.get(role.name, 0) + 1
|
||
seen[role.name] = count
|
||
aliased[role.name if count == 1 else f"{role.name}_{count}"] = role
|
||
if len(aliased) >= 2:
|
||
result.simplex = Simplex(name, aliased)
|
||
else:
|
||
result.notes.append(f"degenerate: only {len(aliased)} role(s)")
|
||
return result
|