Constraint Solver and Program Theory

The panproto protocol that QVR programs are schemas over (QVR_PROGRAM_PROTOCOL) and the extractor that walks a compiled environment to emit a panproto Schema (extract_program_schema).

program_theory

Program Theory: a panproto protocol for the resolved (post-compilation) DSL.

The QVR_PROGRAM_PROTOCOL protocol describes the static structure of a compiled .qvr program — every object, space, morphism, and output the program declares — as a panproto panproto.Schema. This sits one layer above the syntactic qvr protocol from panproto-grammars-all: the syntactic protocol carries the AST as parsed, this protocol carries the AST after the resolution layer (_resolve_type, _resolve_space) has run.

Why have it

Once two programs share this protocol, panproto's structural diff, auto-lens-generation, and breaking-change detection apply to compiled programs as a whole. Two .qvr files that compile to structurally equivalent programs produce equal Schemas; two that diverge surface their divergence through panproto.diff_schemas.

Vertex kinds

Top-level container: program the root vertex; one per compiled module.

Discrete objects (mirrors quivers.core.objects): finset product_set coproduct_set free_monoid empty_set

Continuous spaces (mirrors quivers.continuous.spaces): euclidean simplex positive_reals product_space

Top-level declarations: object_decl space_decl morphism_decl kernel_decl kernel_decl discretize_decl embed_decl output_decl

Edge kinds

decl program -> *_decl: each declaration is a child of the root program. binds_to object_decl -> set_object / space_decl -> space. component product_set | coproduct_set -> set_object; product_space -> space: structural recursion into composite types. domain / codomain morphism_decl | kernel_decl | kernel_decl -> set_object | space. output program -> output_decl.

Constraint sorts carry the per-vertex scalar metadata: name, cardinality, dim, low, high, family, modality, morphism_kind, replicate, n_bins.

QVR_DEDUCTION_PROTOCOL module-attribute

QVR_DEDUCTION_PROTOCOL: Protocol = define_protocol({'name': 'qvr_deduction', 'schema_theory': 'ThBratSchema', 'instance_theory': 'ThBratInstance', 'edge_rules': _DEDUCTION_EDGE_RULES, 'obj_kinds': _DEDUCTION_OBJECT_KINDS, 'constraint_sorts': _DEDUCTION_CONSTRAINT_SORTS})

Panproto protocol for a weighted deductive system.

Vertex kinds: * deduction_system — the top-level declaration. * deduction_atom — an atom of the item algebra. * deduction_rule — a named sequent-style inference rule. * deduction_premise — one premise pattern of a rule. * deduction_conclusion — a rule's conclusion pattern.

Edges: * decl — system :math:\to rule. * atom — system :math:\to atom. * premise — rule :math:\to premise. * conclusion — rule :math:\to conclusion.

Constraint sorts carry the system's semiring, start, depth, and each pattern's textual form. Schema morphisms over this protocol correspond to specializations of deduction systems (e.g., :math:\mathsf{CCG} \subset \mathsf{Lambek} \subset \mathsf{MultimodalLambek}).

extract_program_schema

extract_program_schema(compiler: 'Compiler') -> Schema

Produce a panproto.Schema for a compiled program.

Walks the compiler's resolved environment (objects, spaces, morphisms) and emits a graph of vertices and edges in the QVR_PROGRAM_PROTOCOL protocol. The returned schema validates against that protocol and is suitable for panproto.diff_schemas, panproto.auto_generate_lens, and the rest of panproto's schema-level operations.

PARAMETER	DESCRIPTION
compiler	A quivers.dsl.compiler.Compiler after compile_env (or compile) has populated the resolved environments. TYPE: 'Compiler'

RETURNS	DESCRIPTION
Schema	A program-level Schema in the qvr_program protocol.

Source code in src/quivers/dsl/program_theory.py

def extract_program_schema(compiler: "Compiler") -> panproto.Schema:
    """Produce a `panproto.Schema` for a compiled program.

    Walks the compiler's resolved environment (objects, spaces, morphisms)
    and emits a graph of vertices and edges in the
    `QVR_PROGRAM_PROTOCOL` protocol. The returned schema validates
    against that protocol and is suitable for `panproto.diff_schemas`,
    `panproto.auto_generate_lens`, and the rest of panproto's
    schema-level operations.

    Parameters
    ----------
    compiler
        A [`quivers.dsl.compiler.Compiler`][quivers.dsl.compiler.Compiler] after `compile_env`
        (or `compile`) has populated the resolved environments.

    Returns
    -------
    panproto.Schema
        A program-level Schema in the ``qvr_program`` protocol.
    """
    builder = QVR_PROGRAM_PROTOCOL.schema()
    writer = _SchemaWriter(builder)

    builder.vertex("program", "program")
    if compiler._algebra is not None:
        builder.constraint("program", "algebra", type(compiler._algebra).__name__)

    # object decls
    for name, obj in compiler._objects.items():
        decl_vid = f"object_decl::{name}"
        builder.vertex(decl_vid, "object_decl")
        builder.constraint(decl_vid, "name", name)
        builder.edge("program", decl_vid, "decl")
        target_vid = writer.write_set_object(obj)
        builder.edge(decl_vid, target_vid, "binds_to")

    # space decls
    for name, space in compiler._spaces.items():
        decl_vid = f"space_decl::{name}"
        builder.vertex(decl_vid, "space_decl")
        builder.constraint(decl_vid, "name", name)
        builder.edge("program", decl_vid, "decl")
        target_vid = writer.write_space(space)
        builder.edge(decl_vid, target_vid, "binds_to")

    # morphism decls — the compiler's _morphisms env holds named primitive
    # morphisms; we record them as morphism_decl vertices with domain/codomain.
    # Composite morphisms (let-bindings, output) are derived rather than
    # recorded directly; the structural Diff-able layer is the named decls.
    for name, morphism in compiler._morphisms.items():
        kind = _classify_morphism_kind(morphism)

        decl_vid = f"{kind}::{name}"
        builder.vertex(decl_vid, kind)
        builder.constraint(decl_vid, "name", name)
        builder.edge("program", decl_vid, "decl")

        dom = getattr(morphism, "domain", None)
        cod = getattr(morphism, "codomain", None)
        if dom is not None:
            dom_vid = writer.write_any(dom)
            builder.edge(decl_vid, dom_vid, "domain")
        if cod is not None:
            cod_vid = writer.write_any(cod)
            builder.edge(decl_vid, cod_vid, "codomain")

    # output decl — the compiler's `_output_expr` holds the AST expression
    # whose compilation produces the program's root morphism. We record an
    # output_decl vertex carrying the expression's source-text form (when
    # available) as a name constraint; the structural diff cares about
    # presence/absence of an output, not its detailed shape.
    if compiler._output_expr is not None:
        out_vid = "output_decl"
        builder.vertex(out_vid, "output_decl")
        # ExprIdent / ExprIdentity carry a single name; composite expressions
        # don't have a single canonical name, so mark them as "<composite>".
        expr = compiler._output_expr
        if isinstance(expr, ExprIdent):
            label = expr.name
        elif isinstance(expr, ExprIdentity):
            label = f"identity({expr.object_name})"
        else:
            label = "<composite>"
        builder.constraint(out_vid, "name", label)
        builder.edge("program", out_vid, "output")

    return builder.build()

extract_deduction_schema

extract_deduction_schema(compiler: 'Compiler') -> Schema

Produce a panproto.Schema for the compiler's deduction-system environment.

Walks the compiler's _deductions registry and emits one panproto vertex per deduction system, one per rule, one per atom, and per-premise / per-conclusion pattern vertices. The returned schema validates against QVR_DEDUCTION_PROTOCOL and is suitable for panproto.diff_schemas and panproto.auto_generate_lens operations over deduction systems.

Source code in src/quivers/dsl/program_theory.py

def extract_deduction_schema(compiler: "Compiler") -> panproto.Schema:
    """Produce a `panproto.Schema` for the compiler's
    deduction-system environment.

    Walks the compiler's ``_deductions`` registry and emits one
    panproto vertex per deduction system, one per rule, one per
    atom, and per-premise / per-conclusion pattern vertices. The
    returned schema validates against
    `QVR_DEDUCTION_PROTOCOL` and is suitable for
    `panproto.diff_schemas` and
    `panproto.auto_generate_lens` operations over deduction
    systems.
    """
    builder = QVR_DEDUCTION_PROTOCOL.schema()
    deductions = getattr(compiler, "_deductions", {})
    for name, system in deductions.items():
        sys_vid = f"deduction:{name}"
        builder.vertex(sys_vid, "deduction_system")
        builder.constraint(sys_vid, "name", name)
        builder.constraint(sys_vid, "semiring", system.semiring.__class__.__name__)
        for rule_idx, rule in enumerate(system.rules):
            rule_vid = f"{sys_vid}/rule:{rule.name}"
            builder.vertex(rule_vid, "deduction_rule")
            builder.constraint(rule_vid, "name", rule.name)
            builder.edge(sys_vid, rule_vid, "decl")
            for prem_idx, premise in enumerate(rule.premises):
                p_vid = f"{rule_vid}/premise:{prem_idx}"
                builder.vertex(p_vid, "deduction_premise")
                builder.constraint(p_vid, "pattern", repr(premise))
                builder.edge(rule_vid, p_vid, "premise")
            conc_vid = f"{rule_vid}/conclusion"
            builder.vertex(conc_vid, "deduction_conclusion")
            builder.constraint(conc_vid, "pattern", repr(rule.conclusion))
            builder.edge(rule_vid, conc_vid, "conclusion")
    return builder.build()