Constraint Solver and Program Theory

QVR_PROGRAM_PROTOCOL is the panproto protocol over which QVR programs are schemas. extract_program_schema walks a compiled environment and emits a panproto 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 as a panproto panproto.Schema: every object, space, morphism, and output the program declares, together with the checked computation and effect graph the QIEC elaboration produced for it. This sits one layer above the syntactic qvr protocol compiled from the in-tree QVR grammar: the syntactic protocol carries the AST as parsed, while this protocol carries the AST after the resolution layer (_resolve_type, _resolve_space) and the kernel check have 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 discretize_decl embed_decl output_decl

Kernel declarations (mirrors quivers.qiec.module): effect_decl operation instance_decl handler_decl handler_clause computation_decl computation_parameter program_entry program_parameter program_site

Edge kinds

decl program -> *_decl: each declaration, source or kernel, 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 | discretize_decl | embed_decl -> set_object | space. output program -> output_decl. operation effect_decl -> operation; handler_clause -> operation: the operations an interface declares and the one a clause answers. instance_of instance_decl -> effect_decl: the interface an instance applies. handles handler_decl -> effect_decl. clause handler_decl -> handler_clause. parameter computation_decl -> computation_parameter; program_entry -> program_parameter. row computation_decl -> instance_decl: the instances a computation's declared row names. calls computation_decl | handler_clause -> computation_decl: the computations a body calls. performs computation_decl | handler_clause -> instance_decl: the instances a body performs requests on. installs computation_decl | handler_clause -> handler_decl: the handlers a body installs. entry program -> program_entry. body program_entry -> computation_decl. site program_entry -> program_site. random / score program_entry -> instance_decl: the lexical instances the entry's samples and scores address.

Constraint sorts carry the per-vertex scalar metadata: name, cardinality, dim, low, high, family, modality, morphism_kind, replicate, n_bins, and for kernel vertices identity, type, effects, role, site_kind, grade, implementation, total, batch, event, and gap.

QVR_PROGRAM_PROTOCOL module-attribute

QVR_PROGRAM_PROTOCOL: Protocol = panproto.define_protocol({'name': 'qvr_program', 'schema_theory': 'ThBratSchema', 'instance_theory': 'ThBratInstance', 'edge_rules': _EDGE_RULES, 'obj_kinds': _OBJECT_KINDS, 'constraint_sorts': _CONSTRAINT_SORTS})

Panproto protocol for a compiled QVR program.

extract_program_schema writes schemas in this protocol. The vertex kinds, edge rules, and constraint sorts are the ones the module docstring lists.

QVR_DEDUCTION_PROTOCOL module-attribute

QVR_DEDUCTION_PROTOCOL: Protocol = panproto.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 its checked kernel module (effects, instances, handlers, computations, and program entry points) 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 its checked kernel module (effects, instances, handlers,
    computations, and program entry points) 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 : 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")

    if compiler.qiec_module is not None:
        _KernelWriter(builder, compiler.qiec_module).write()

    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.

PARAMETER	DESCRIPTION
compiler	A compiler whose _deductions registry is populated. TYPE: Compiler

RETURNS	DESCRIPTION
Schema	A schema in the qvr_deduction protocol.

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.

    Parameters
    ----------
    compiler : Compiler
        A compiler whose ``_deductions`` registry is populated.

    Returns
    -------
    panproto.Schema
        A schema in the ``qvr_deduction`` protocol.
    """
    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()