Resolution Lenses

Bidirectional resolution from QVR TypeExpr / SpaceExpr AST trees to runtime SetObject / ContinuousSpace values, expressed as a dx.Lens family. The resolution environment (object/space inventory) is carried on each lens instance.

resolution

Bidirectional resolution lenses for QVR type and space expressions.

The compiler's _resolve_type and _resolve_space map syntactic AST trees (:class:~quivers.dsl.ast_nodes.TypeExpr and :class:~quivers.dsl.ast_nodes.SpaceExpr variants) to resolved values (:class:~quivers.core.objects.SetObject and :class:~quivers.continuous.spaces.ContinuousSpace variants). This module expresses those mappings as :class:didactic.api.Lens instances so the resolution layer becomes a first-class lens family rather than ad-hoc visitor code.

Each lens carries the resolution environment it needs (the object inventory and, for spaces, the previously-declared space inventory) on its own instance — that's the dependent-optics shape: the lens is parameterised by context that determines how each leaf vertex resolves. The forward direction performs the value-dependent lookup; the complement holds the original AST node so :meth:backward recovers it verbatim. Round-trip laws hold by construction:

  • backward(*forward(t)) == t (GetPut)
  • forward(backward(s, c)) == (s, c) (PutGet)

:class:didactic.api.Lens is a pure-Python authoring surface; the panproto-side compilation (each Lens becoming a panproto.Lens with formal complement-bearing get/put and runtime law-checking) is a later didactic feature. Today these lenses behave as ordinary Python objects with forward / backward methods and >> composition.

TypeExprToSetObject 

TypeExprToSetObject(env: dict[str, SetObject])

Bases: Lens[TypeExpr, SetObject, TypeExpr]

Resolve a :class:TypeExpr AST tree to a :class:SetObject.

The forward direction dispatches on the variant kind:

  • TypeName(name="X") → self.env[X] if X is bound, else FinSet(name=X, cardinality=int(X)) if X is an integer literal.
  • TypeProduct(components=…) → ProductSet(components=…) with each component recursively resolved.
  • TypeCoproduct(components=…) → CoproductSet(components=…) with each component recursively resolved.
PARAMETER DESCRIPTION
env

The object-name → :class:SetObject environment built from object declarations earlier in the program.

TYPE: dict[str, SetObject]

Source code in src/quivers/dsl/resolution.py 
88
89
def __init__(self, env: dict[str, SetObject]) -> None:
    self._env = env

SpaceExprToContinuousSpace 

SpaceExprToContinuousSpace(env_spaces: dict[str, ContinuousSpace], env_objects: dict[str, SetObject], name: str)

Bases: Lens[SpaceExpr, ContinuousSpace | SetObject, SpaceExpr]

Resolve a :class:SpaceExpr AST tree to a :class:ContinuousSpace.

Bare identifiers (:class:SpaceName) may resolve to either a previously declared continuous space or, for mixed-domain programs, a discrete :class:SetObject declared earlier — the forward direction dispatches accordingly:

  • :class:SpaceConstructor → invoke the named constructor with the parsed numeric args.
  • :class:SpaceName → look up in env_spaces (continuous) or env_objects (discrete fallback).
  • :class:SpaceProduct → recurse into components.
PARAMETER DESCRIPTION
env_spaces

The space-name → :class:ContinuousSpace environment from previously declared space blocks.

TYPE: dict[str, ContinuousSpace]

env_objects

The object-name → :class:SetObject environment, consulted when a bare identifier does not name a continuous space.

TYPE: dict[str, SetObject]

name

The binding name for the new space (used by :class:SpaceConstructor outputs); callers passing a :class:SpaceConstructor should provide the declaration name.

TYPE: str

Source code in src/quivers/dsl/resolution.py 
188
189
190
191
192
193
194
195
196
def __init__(
    self,
    env_spaces: dict[str, ContinuousSpace],
    env_objects: dict[str, SetObject],
    name: str,
) -> None:
    self._env_spaces = env_spaces
    self._env_objects = env_objects
    self._name = name