"""Synthetic example: one isomorphism schema relates two groups and a map."""
from __future__ import annotations

import json

from leanbench.schema import KIND_FACT, KIND_GOAL, Role, Simplex, SimplexInstance
from leanbench.schema_registry import SchemaRegistry, slot_key


def example():
    group = Role("group", type_text="group carrier", context="Reusable group role definition")
    schema = Simplex("group_isomorphism", {
        "left": group,
        "right": group,
        "map": Role("homomorphism", type_text="left →* right",
                    attrs={"references": ["left", "right"]}),
        "bijective": Role("bijective", KIND_FACT, type_text="Bijective map",
                          attrs={"references": ["map"]}),
        "goal": Role("isomorphic", KIND_GOAL, type_text="Nonempty (left ≃* right)",
                     attrs={"references": ["left", "right"]}),
    }, context="A bijective homomorphism supplies a group isomorphism")
    with SchemaRegistry() as registry:
        registry.set_role(group, "role:group")
        key = registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"})
        instance = SimplexInstance(schema, facts={
            "left": "group A", "right": "group B", "map": "f", "bijective": "supplied evidence"})
        candidates = registry.find_solvable([slot_key(key, alias) for alias in instance.facts])
        return {"schema": registry.get_simplex(key).as_dict(), "definition_keys": registry.slots(key),
                "bindings": {alias: fact.value for alias, fact in instance.facts.items()},
                "structural_candidates": candidates, "completed": instance.is_completed(),
                "note": "Evidence is symbolic user input; this example does not run a Lean proof."}


if __name__ == "__main__":
    print(json.dumps(example(), indent=2, ensure_ascii=False))