Theory bridge¶

didactic.theory._theory.build_theory_spec ¶

build_theory_spec(cls: type[Model]) -> TheorySpec

Build a panproto-compatible Theory spec dict for a Model class.

Parameters:

Name	Type	Description	Default
`cls`	`type[Model]`	A Model subclass with `__field_specs__` and `__schema_kind__` populated by the metaclass.	required

Returns:

Type Description

dict

A dict shaped to be deserialised by panproto's Rust core into a Theory. Specifically::

{
    "name": str,  # the model's class name
    "extends": list[str],  # parent theories (none yet)
    "sorts": list[Sort],  # primary sort + per-field sorts
    "ops": list[Operation],  # field accessors / edges
    "eqs": list[Equation],  # axioms
    "directed_eqs": [],  # rewrites; reserved
    "policies": [],  # merge policies; reserved
}

Notes

The dict only encodes information available on the didactic side. The panproto core may further validate the shape and reject malformed specs; in that case, the caller surfaces a panproto.GatError.

didactic.theory._theory.build_theory ¶

build_theory(cls: type) -> Theory

Materialise a panproto.Theory from a Model class.

Parameters:

Name	Type	Description	Default
`cls`	`type`	A Model subclass.	required

Returns:

Type	Description
`Theory`	The Theory produced by `panproto.create_theory(spec)`. For a class with multiple Model parents, the result is the panproto colimit (pushout) of the parent theories over their lowest common ancestor; otherwise it's the flat theory built from `cls`'s `__field_specs__`.

Raises:

Type	Description
`ImportError`	If `panproto` is not installed in the current environment.
`GatError`	If panproto rejects the spec; usually a sign that didactic's translation is producing a malformed dict.

Notes

Single inheritance flattens transparently because the metaclass walks the full MRO when collecting field specs; the resulting Theory already includes every inherited field. Multiple inheritance triggers a real panproto.colimit_theories call, which validates that the merge is consistent and is the categorical pushout of the two branches over their shared ancestor.

This call is the only place in didactic proper that imports panproto. Doing it lazily lets the rest of the package be authored and unit-tested without panproto installed.