"""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)