163 lines
7.7 KiB
Python
163 lines
7.7 KiB
Python
"""Semantic role definitions, scoped occurrences and structural candidate retrieval."""
|
|
import json
|
|
|
|
import pytest
|
|
|
|
from leanbench.schema import (
|
|
KIND_FACT,
|
|
KIND_GOAL,
|
|
Fact,
|
|
Role,
|
|
Simplex,
|
|
SimplexInstance,
|
|
role_from_dict,
|
|
)
|
|
from leanbench.schema_registry import SchemaRegistry, slot_key
|
|
|
|
|
|
def theorem(name="t"):
|
|
return Simplex(name, {"G": Role("group", context="A group carrier"),
|
|
"g": Role("element", type_text="G", attrs={"references": ["G"]}),
|
|
"finite": Role("finite", KIND_FACT, type_text="Finite G",
|
|
attrs={"references": ["G"]}),
|
|
"goal": Role("claim", KIND_GOAL, type_text="P G g",
|
|
attrs={"references": ["G", "g"]})},
|
|
context="A multi-object claim", attrs={"provenance": "synthetic"})
|
|
|
|
|
|
def test_json_roundtrip_keeps_metadata_and_nesting():
|
|
outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)},
|
|
context="Composed relation", attrs={"version": 1})
|
|
encoded = json.loads(json.dumps(outer.as_dict()))
|
|
restored = role_from_dict(encoded)
|
|
assert restored.as_dict() == outer.as_dict()
|
|
assert restored.roles["lemma"].roles["g"].attrs["references"] == ["G"]
|
|
|
|
|
|
def test_registry_persists_nested_schemas_in_one_transaction(tmp_path):
|
|
path = tmp_path / "registry.sqlite"
|
|
outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)})
|
|
with SchemaRegistry(path) as registry:
|
|
registry.set_simplex(outer)
|
|
registry.set_simplex(outer)
|
|
assert registry.info() == {"roles": 5, "simplices": 2, "slots": 6}
|
|
with SchemaRegistry(path) as registry:
|
|
assert registry.get_simplex("schema:outer").as_dict() == outer.as_dict()
|
|
leaf = slot_key(slot_key("schema:outer", "lemma"), "g")
|
|
assert registry.find_by_roles([leaf], match_all=True) == [
|
|
"schema:outer", slot_key("schema:outer", "lemma")]
|
|
|
|
|
|
def test_same_names_in_different_theorems_are_scoped():
|
|
with SchemaRegistry() as registry:
|
|
registry.set_simplex(theorem("first"))
|
|
registry.set_simplex(theorem("second"))
|
|
first_group = slot_key("schema:first", "G")
|
|
assert registry.find_by_roles([first_group]) == ["schema:first"]
|
|
assert registry.get_role(first_group).name == "group"
|
|
assert registry.slots("schema:first")["G"] != registry.slots("schema:second")["G"]
|
|
|
|
|
|
def test_explicit_reuse_does_not_equate_local_bindings_or_multiplicity():
|
|
group = Role("group")
|
|
schema = Simplex("isomorphism", {"left": group, "right": group,
|
|
"goal": Role("equivalence", KIND_GOAL)})
|
|
with SchemaRegistry() as registry:
|
|
registry.set_role(group, "role:group")
|
|
registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"})
|
|
assert registry.slots("schema:isomorphism")["left"] == "role:group"
|
|
assert registry.find_solvable(["role:group"]) == []
|
|
assert registry.find_solvable([slot_key("schema:isomorphism", "left")]) == []
|
|
candidate = registry.find_solvable([slot_key("schema:isomorphism", x) for x in ["left", "right"]])
|
|
assert candidate[0]["target_slots"] == [slot_key("schema:isomorphism", "goal")]
|
|
instance = SimplexInstance(schema, {"left": "C2", "right": "C3"})
|
|
assert instance.facts["left"].value != instance.facts["right"].value
|
|
assert not instance.is_completed()
|
|
instance.resolve("goal", "a supplied result, not checked by the registry")
|
|
assert instance.is_completed()
|
|
|
|
|
|
def test_premise_is_required_and_known_goal_is_not_a_missing_target():
|
|
with SchemaRegistry() as registry:
|
|
registry.set_simplex(theorem())
|
|
inputs = [slot_key("schema:t", alias) for alias in ["G", "g", "finite"]]
|
|
assert registry.find_solvable(inputs[:-1]) == []
|
|
assert registry.find_solvable(inputs)[0]["structural_candidate_only"]
|
|
assert registry.find_solvable(inputs + [slot_key("schema:t", "goal")]) == []
|
|
|
|
|
|
def test_failed_write_rolls_back_every_child():
|
|
with SchemaRegistry() as registry:
|
|
registry.set_role(Role("incompatible"), "role:shared")
|
|
before = registry.info()
|
|
with pytest.raises(ValueError, match="does not match"):
|
|
registry.set_simplex(theorem(), role_keys={"goal": "role:shared"})
|
|
assert registry.info() == before
|
|
assert registry.get_simplex("schema:t") is None
|
|
|
|
|
|
def test_cyclic_nesting_is_rejected_without_partial_write():
|
|
schema = Simplex("cycle", {"a": Role("a"), "b": Role("b")})
|
|
schema.roles["b"] = schema
|
|
with SchemaRegistry() as registry:
|
|
with pytest.raises(ValueError, match="cyclic"):
|
|
registry.set_simplex(schema)
|
|
assert registry.info() == {"roles": 0, "simplices": 0, "slots": 0}
|
|
|
|
|
|
def test_keys_are_immutable_and_reuse_map_cannot_silently_change():
|
|
with SchemaRegistry() as registry:
|
|
registry.set_role(Role("G"), "role:G")
|
|
with pytest.raises(ValueError, match="different content"):
|
|
registry.set_role(Role("H"), "role:G")
|
|
schema = theorem()
|
|
registry.set_simplex(schema)
|
|
registry.set_role(schema.roles["G"], "role:shared")
|
|
with pytest.raises(ValueError, match="cannot change"):
|
|
registry.set_simplex(schema, role_keys={"G": "role:shared"})
|
|
assert registry.search_roles("%") == []
|
|
assert registry.search_roles("group", limit=1)[0]["role"]["name"] == "group"
|
|
|
|
|
|
def test_instance_constraints_unknown_slots_and_invalid_references():
|
|
role = Role("parity", choices=["even", "odd"])
|
|
with pytest.raises(ValueError, match="not allowed"):
|
|
Fact(role, "prime")
|
|
schema = Simplex("pair", {"input": role, "goal": Role("result", KIND_GOAL, choices=[True])})
|
|
instance = SimplexInstance(schema, {"input": "even"})
|
|
with pytest.raises(ValueError, match="not allowed"):
|
|
instance.resolve("goal", False)
|
|
with pytest.raises(ValueError, match="declared"):
|
|
SimplexInstance(schema, {"unknown": "value"})
|
|
with pytest.raises(ValueError, match="references"):
|
|
Simplex("invalid", {"x": Role("x", attrs={"references": ["missing"]}), "y": Role("y")})
|
|
with pytest.raises(ValueError, match="name"):
|
|
Role(" ")
|
|
with pytest.raises(ValueError, match="sequence"):
|
|
Role("choice", choices="even")
|
|
with SchemaRegistry() as registry, pytest.raises(ValueError, match="Simplex object"):
|
|
registry.set_role(Role("fake", "simplex"))
|
|
|
|
|
|
def test_pilot_materialization_keeps_partial_lean_projection_explicit():
|
|
import importlib.util
|
|
from pathlib import Path
|
|
|
|
path = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/build_schemas.py"
|
|
spec = importlib.util.spec_from_file_location("build_schemas", path)
|
|
builder = importlib.util.module_from_spec(spec)
|
|
spec.loader.exec_module(builder)
|
|
items = [{"id": "closed", "lean_code": "theorem t : True := trivial"}]
|
|
assessment = {"records": [{"id": "closed", "blind_id": "P01", "source": {
|
|
"roles": [{"kind": "object", "symbols": ["G"], "description": "group"},
|
|
{"kind": "goal", "description": "A synthetic claim"}]}}]}
|
|
with SchemaRegistry() as registry:
|
|
index, snapshots = builder.build(items, assessment, {"P01": "closed"}, registry)
|
|
assert registry.info()["simplices"] == 1
|
|
assert index[0]["source_status"] == "unreviewed_annotation_seed"
|
|
assert index[0]["lean_schema"] is None
|
|
assert index[0]["lean_status"] == "insufficient_projected_roles"
|
|
assert snapshots[0]["lean_projection"]["roles"][0]["kind"] == "goal"
|
|
with pytest.raises(ValueError, match="exactly once"):
|
|
builder.build(items, {"records": []}, {"P01": "closed"}, registry)
|