Program Theory¶

def extract_program_schema(compiler: "Compiler") -> panproto.Schema:
    """Produce a :class:`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
    :data:`QVR_PROGRAM_PROTOCOL` protocol. The returned schema validates
    against that protocol and is suitable for :func:`panproto.diff_schemas`,
    :func:`panproto.auto_generate_lens`, and the rest of panproto's
    schema-level operations.

    Parameters
    ----------
    compiler
        A :class:`~quivers.dsl.compiler.Compiler` after :meth:`compile_env`
        (or :meth:`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._quantale is not None:
        builder.constraint("program", "quantale", type(compiler._quantale).__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()