Kernel IR

The typed, target-independent mirror of a checked kernel module.

qiec_ir

Typed, target-independent IR for the Quivers Indexed Effect Core.

The QIEC kernel deliberately uses frozen dataclasses: they are convenient for type checking and evaluation, but are not part of the structural transpiler IR. This module is the lossless boundary between the two. Every stable QIEC construct has a corresponding :mod:didactic model, so a backend can inspect effects, values, evidence, resumptions, and source provenance without parsing an opaque JSON side channel.

QiecFeature

QiecFeature = Literal['declarations', 'return', 'bind', 'perform', 'handle', 'case', 'if', 'call', 'recursion', 'resume', 'local-instance', 'authored-handler', 'arithmetic', 'comparison', 'boolean', 'string', 'conversion', 'math', 'tuple', 'tensor', 'distribution', 'plate', 'log-density', 'site', 'gather', 'segment-sum', 'kernel-matrix', 'affine-map', 'table-map', 'neural-attachment', 'search', 'reduction', 'rowwise', 'comprehension', 'special', 'activation', 'weight', 'evidence', 'transport', 'attachment', 'structured-value', 'effectful-row', 'open-effect-row', 'type-polymorphism', 'index-polymorphism', 'effect-polymorphism', 'named-parameter', 'non-scalar-result', 'non-scalar-parameter', 'zero-resumption', 'affine-resumption', 'linear-resumption', 'unrestricted-resumption']

One QIEC construct a target may or may not preserve.

analyze_qiec_capabilities names the features a module needs, and a QiecTargetCapabilities names the ones a target has.

IRQiecId didactic-model

IRQiecId(*, namespace: str, digest: str)

Bases: Model

A stable QIEC identifier, split into namespace and digest.

text property

text: str

The identifier's qiec:<namespace>:<digest> spelling.

IRQiecSourceOrigin didactic-model

IRQiecSourceOrigin(*, module: str, structural_path: tuple[IRPathPart, ...], role: str, source_protocol: str, file: str | None = None, line: int | None = None, column: int | None = None)

Bases: Model

Mirror of a kernel source origin: a site's structural location.

Line and column are diagnostic coordinates; the structural path alone locates the site.

PARAMETER	DESCRIPTION
module	The module the site belongs to. TYPE: str
structural_path	The path of names and positions from the module root to the site. TYPE: tuple[IRPathPart, ...]
role	What the site is, such as "sample" or "call". TYPE: str
source_protocol	The source language or protocol the path is expressed in. TYPE: str
file	The file the site was read from, if any. TYPE: str | None DEFAULT: None
line	The one-based line of the site, if known. TYPE: int | None DEFAULT: None
column	The one-based column of the site, if known. TYPE: int | None DEFAULT: None

IRQiecDynamicAddressFrame didactic-model

IRQiecDynamicAddressFrame(*, scope: str, key: str | int)

Bases: Model

One component of a dynamic effect address.

PARAMETER	DESCRIPTION
scope	What kind of frame this is, such as a call, a handler clause, a resumption, or a local instance. TYPE: str
key	The frame's position within its scope: a name or an ordinal. TYPE: str | int

IRQiecSiteProvenance didactic-model

IRQiecSiteProvenance(*, origin: IRQiecSourceOrigin, dynamic_path: tuple[IRQiecDynamicAddressFrame, ...] = (), resumption_path: tuple[int, ...] = (), relation: Literal['preserve', 'split', 'duplicate', 'eliminate'] = 'preserve', parents: tuple[IRQiecId, ...] = ())

Bases: Model

Static and dynamic provenance of an effect request.

PARAMETER	DESCRIPTION
origin	The source site the request was written at. TYPE: IRQiecSourceOrigin
dynamic_path	The address frames entered to reach this occurrence of the site, outermost first. TYPE: tuple[IRQiecDynamicAddressFrame, ...] DEFAULT: ()
resumption_path	The ordinal of each resumption taken to reach this occurrence. TYPE: tuple[int, ...] DEFAULT: ()
relation	How this request relates to the source site: "preserve" for the request as written, "split" or "duplicate" for a request a handler derived from it, and "eliminate" for one it discharged. TYPE: Literal['preserve', 'split', 'duplicate', 'eliminate'] DEFAULT: 'preserve'
parents	The static sites a derived request was generated from. TYPE: tuple[IRQiecId, ...] DEFAULT: ()

IRQiecKind didactic-model

IRQiecKind()

Bases: TaggedUnion

Kind in the QIEC static language.

IRQiecTypeKind didactic-model

IRQiecTypeKind(*, kind: Literal['type'] = 'type')

Bases: IRQiecKind

The kind of types.

PARAMETER	DESCRIPTION
kind	The discriminator; always "type". TYPE: Literal['type'] DEFAULT: 'type'

IRQiecEffectKind didactic-model

IRQiecEffectKind(*, kind: Literal['effect'] = 'effect')

Bases: IRQiecKind

The kind of effect interfaces.

PARAMETER	DESCRIPTION
kind	The discriminator; always "effect". TYPE: Literal['effect'] DEFAULT: 'effect'

IRQiecRowKind didactic-model

IRQiecRowKind(*, kind: Literal['row'] = 'row')

Bases: IRQiecKind

The kind of effect rows.

PARAMETER	DESCRIPTION
kind	The discriminator; always "row". TYPE: Literal['row'] DEFAULT: 'row'

IRQiecArrowKind didactic-model

IRQiecArrowKind(*, domain: IRQiecKind, codomain: IRQiecKind, kind: Literal['arrow'] = 'arrow')

Bases: IRQiecKind

The kind of a constructor from one kind to another.

PARAMETER	DESCRIPTION
domain	The kind of the argument. TYPE: IRQiecKind
codomain	The kind of the result. TYPE: IRQiecKind
kind	The discriminator; always "arrow". TYPE: Literal['arrow'] DEFAULT: 'arrow'

IRQiecIndexSort didactic-model

IRQiecIndexSort()

Bases: TaggedUnion

Closed index sort.

IRQiecNatSort didactic-model

IRQiecNatSort(*, kind: Literal['nat'] = 'nat')

Bases: IRQiecIndexSort

The sort of natural-number indices.

PARAMETER	DESCRIPTION
kind	The discriminator; always "nat". TYPE: Literal['nat'] DEFAULT: 'nat'

IRQiecShapeSort didactic-model

IRQiecShapeSort(*, rank: int | None = None, kind: Literal['shape'] = 'shape')

Bases: IRQiecIndexSort

The sort of shapes, optionally restricted to a fixed rank.

PARAMETER	DESCRIPTION
rank	The number of dimensions, or None for any rank. TYPE: int | None DEFAULT: None
kind	The discriminator; always "shape". TYPE: Literal['shape'] DEFAULT: 'shape'

IRQiecContextSort didactic-model

IRQiecContextSort(*, signature: str, kind: Literal['context'] = 'context')

Bases: IRQiecIndexSort

The sort of logic-program contexts over a named signature.

PARAMETER	DESCRIPTION
signature	The name of the signature whose contexts inhabit this sort. TYPE: str
kind	The discriminator; always "context". TYPE: Literal['context'] DEFAULT: 'context'

IRQiecUserIndexSort didactic-model

IRQiecUserIndexSort(*, name: str, constructors: tuple[str, ...], arities: tuple[int, ...], kind: Literal['user'] = 'user')

Bases: IRQiecIndexSort

A closed user-defined index datatype.

PARAMETER	DESCRIPTION
name	The sort's name, part of its identity. TYPE: str
constructors	The constructor names, part of the identity. TYPE: tuple[str, ...]
arities	The argument count of each constructor, aligned with constructors. TYPE: tuple[int, ...]
kind	The discriminator; always "user". TYPE: Literal['user'] DEFAULT: 'user'

IRQiecBinder didactic-model

IRQiecBinder(*, name: str, refinable: bool = False)

Bases: TaggedUnion

A telescope binder for a static argument.

The subclasses distinguish type, index, and effect binders by the kind discriminator.

PARAMETER	DESCRIPTION
name	The binder's display name. TYPE: str
refinable	Whether case analysis may refine the bound argument; true for a family's indices and false for its uniform parameters. TYPE: bool DEFAULT: False

IRQiecTypeBinder didactic-model

IRQiecTypeBinder(*, name: str, refinable: bool = False, type_kind: IRQiecKind, kind: Literal['type'] = 'type')

Bases: IRQiecBinder

A telescope binder for a type-kinded static argument.

Inherits name and refinable from IRQiecBinder.

PARAMETER	DESCRIPTION
type_kind	The kind of the bound argument. TYPE: IRQiecKind
kind	The discriminator; always "type". TYPE: Literal['type'] DEFAULT: 'type'

IRQiecIndexBinder didactic-model

IRQiecIndexBinder(*, name: str, refinable: bool = False, sort: IRQiecIndexSort, kind: Literal['index'] = 'index')

Bases: IRQiecBinder

A telescope binder for an index argument.

Inherits name and refinable from IRQiecBinder.

PARAMETER	DESCRIPTION
sort	The closed index sort of the bound argument. TYPE: IRQiecIndexSort
kind	The discriminator; always "index". TYPE: Literal['index'] DEFAULT: 'index'

IRQiecEffectBinder didactic-model

IRQiecEffectBinder(*, name: str, refinable: bool = False, kind: Literal['effect'] = 'effect')

Bases: IRQiecBinder

A telescope binder for an effect argument.

Inherits name and refinable from IRQiecBinder.

PARAMETER	DESCRIPTION
kind	The discriminator; always "effect". TYPE: Literal['effect'] DEFAULT: 'effect'

IRQiecStatic didactic-model

IRQiecStatic()

Bases: TaggedUnion

Type, index, or effect argument in the QIEC static language.

IRQiecIndexVariable didactic-model

IRQiecIndexVariable(*, name: str, sort: IRQiecIndexSort, identity: IRQiecId | None = None, kind: Literal['index-variable'] = 'index-variable')

Bases: IRQiecStatic

A variable standing for an index term.

PARAMETER	DESCRIPTION
name	The variable's display name. TYPE: str
sort	The closed index sort of the terms it stands for. TYPE: IRQiecIndexSort
identity	The rigid identity of a case branch's skolem, or None for a declaration binder matched by name. TYPE: IRQiecId | None DEFAULT: None
kind	The discriminator; always "index-variable". TYPE: Literal['index-variable'] DEFAULT: 'index-variable'

IRQiecIndexLiteral didactic-model

IRQiecIndexLiteral(*, value: int | str, sort: IRQiecIndexSort, kind: Literal['index-literal'] = 'index-literal')

Bases: IRQiecStatic

A closed index literal.

PARAMETER	DESCRIPTION
value	A natural number for the nat sort, or a nullary constructor name for a user-defined index sort. TYPE: int | str
sort	The sort the literal inhabits. TYPE: IRQiecIndexSort
kind	The discriminator; always "index-literal". TYPE: Literal['index-literal'] DEFAULT: 'index-literal'

IRQiecIndexConstructor didactic-model

IRQiecIndexConstructor(*, name: str, arguments: tuple[IRQiecStatic, ...], sort: IRQiecIndexSort, kind: Literal['index-constructor'] = 'index-constructor')

Bases: IRQiecStatic

A fully applied constructor of a user-defined index sort.

PARAMETER	DESCRIPTION
name	The constructor's name, which belongs to sort. TYPE: str
arguments	The constructor's index arguments, in order. TYPE: tuple[IRQiecStatic, ...]
sort	The sort the constructor builds. TYPE: IRQiecIndexSort
kind	The discriminator; always "index-constructor". TYPE: Literal['index-constructor'] DEFAULT: 'index-constructor'

IRQiecShapeIndex didactic-model

IRQiecShapeIndex(*, dimensions: tuple[IRQiecStatic, ...], kind: Literal['shape-index'] = 'shape-index')

Bases: IRQiecStatic

A shape given by its dimensions.

PARAMETER	DESCRIPTION
dimensions	One index term per dimension, outermost first. TYPE: tuple[IRQiecStatic, ...]
kind	The discriminator; always "shape-index". TYPE: Literal['shape-index'] DEFAULT: 'shape-index'

IRQiecTypeVariable didactic-model

IRQiecTypeVariable(*, name: str, type_kind: IRQiecKind, identity: IRQiecId | None = None, kind: Literal['type-variable'] = 'type-variable')

Bases: IRQiecStatic

A variable standing for a type-kinded static argument.

PARAMETER	DESCRIPTION
name	The variable's display name. TYPE: str
type_kind	The kind of the arguments it stands for. TYPE: IRQiecKind
identity	The rigid identity of a case branch's skolem, or None for a declaration binder matched by name. TYPE: IRQiecId | None DEFAULT: None
kind	The discriminator; always "type-variable". TYPE: Literal['type-variable'] DEFAULT: 'type-variable'

IRQiecTypeConstructor didactic-model

IRQiecTypeConstructor(*, id: IRQiecId, name: str, telescope: tuple[IRQiecBinder, ...] = ())

Bases: Model

A fully qualified type constructor and its kinding telescope.

PARAMETER	DESCRIPTION
id	The constructor's stable identity, which alone determines equality. TYPE: IRQiecId
name	The constructor's display name. TYPE: str
telescope	The binders the constructor's arguments instantiate, in order. TYPE: tuple[IRQiecBinder, ...] DEFAULT: ()

IRQiecTypeApplication didactic-model

IRQiecTypeApplication(*, constructor: IRQiecTypeConstructor, arguments: tuple[IRQiecStatic, ...] = (), kind: Literal['type-application'] = 'type-application')

Bases: IRQiecStatic

A type constructor applied to static arguments.

PARAMETER	DESCRIPTION
constructor	The constructor applied. TYPE: IRQiecTypeConstructor
arguments	The arguments instantiating the constructor's telescope, in order; empty for a nullary constructor. TYPE: tuple[IRQiecStatic, ...] DEFAULT: ()
kind	The discriminator; always "type-application". TYPE: Literal['type-application'] DEFAULT: 'type-application'

IRQiecFunctionType didactic-model

IRQiecFunctionType(*, parameter: IRQiecStatic, result: IRQiecStatic, kind: Literal['function-type'] = 'function-type')

Bases: IRQiecStatic

A pure function type.

An effectful codomain is a IRQiecComputationType, which keeps the value and computation strata apart.

PARAMETER	DESCRIPTION
parameter	The argument type. TYPE: IRQiecStatic
result	The result type. TYPE: IRQiecStatic
kind	The discriminator; always "function-type". TYPE: Literal['function-type'] DEFAULT: 'function-type'

IRQiecEqualityType didactic-model

IRQiecEqualityType(*, classifier: IRQiecKind | IRQiecIndexSort, left: IRQiecStatic, right: IRQiecStatic, kind: Literal['equality-type'] = 'equality-type')

Bases: IRQiecStatic

The proposition that two static arguments are equal.

PARAMETER	DESCRIPTION
classifier	The kind or index sort both sides inhabit. TYPE: IRQiecKind | IRQiecIndexSort
left	The left side of the equation. TYPE: IRQiecStatic
right	The right side of the equation. TYPE: IRQiecStatic
kind	The discriminator; always "equality-type". TYPE: Literal['equality-type'] DEFAULT: 'equality-type'

IRQiecEffectVariable didactic-model

IRQiecEffectVariable(*, name: str, identity: IRQiecId | None = None, kind: Literal['effect-variable'] = 'effect-variable')

Bases: IRQiecStatic

A variable standing for an effect interface application.

PARAMETER	DESCRIPTION
name	The variable's display name. TYPE: str
identity	The rigid identity of a case branch's skolem, or None for a declaration binder matched by name. TYPE: IRQiecId | None DEFAULT: None
kind	The discriminator; always "effect-variable". TYPE: Literal['effect-variable'] DEFAULT: 'effect-variable'

IRQiecEffectRef didactic-model

IRQiecEffectRef(*, id: IRQiecId, name: str, arguments: tuple[IRQiecStatic, ...] = (), kind: Literal['effect-ref'] = 'effect-ref')

Bases: IRQiecStatic

One closed effect interface application.

PARAMETER	DESCRIPTION
id	The stable identity of the interface declaration. TYPE: IRQiecId
name	The interface's display name. TYPE: str
arguments	The arguments instantiating the interface's telescope, in order. TYPE: tuple[IRQiecStatic, ...] DEFAULT: ()
kind	The discriminator; always "effect-ref". TYPE: Literal['effect-ref'] DEFAULT: 'effect-ref'

IRQiecLocal didactic-model

IRQiecLocal(*, name: str, type: IRQiecStatic)

Bases: Model

A typed binder for a runtime value.

PARAMETER	DESCRIPTION
name	The binder's display name. TYPE: str
type	The type of every value bound to it. TYPE: IRQiecStatic

IRQiecRowVariable didactic-model

IRQiecRowVariable(*, name: str, identity: IRQiecId, lacks: tuple[IRQiecId, ...] = ())

Bases: Model

The open tail of an effect row, with the instances it excludes.

PARAMETER	DESCRIPTION
name	The display name, used in diagnostics only. TYPE: str
identity	The stable identity, which equality is taken from. TYPE: IRQiecId
lacks	The instances the tail is proven not to contain. TYPE: tuple[IRQiecId, ...] DEFAULT: ()

IRQiecRowEntry didactic-model

IRQiecRowEntry(*, instance: IRQiecId, effect: IRQiecEffectRef)

Bases: Model

One lexical effect instance and the interface it implements.

PARAMETER	DESCRIPTION
instance	The lexical instance, which is the row's key. TYPE: IRQiecId
effect	The interface application the instance implements. TYPE: IRQiecEffectRef

IRQiecEffectRow didactic-model

IRQiecEffectRow(*, entries: tuple[IRQiecRowEntry, ...] = (), tail: IRQiecRowVariable | None = None)

Bases: Model

A finite map from lexical instances to interfaces, plus a tail.

PARAMETER	DESCRIPTION
entries	The instances the row names, each with its interface. TYPE: tuple[IRQiecRowEntry, ...] DEFAULT: ()
tail	A row variable standing for further entries, or None for a closed row. TYPE: IRQiecRowVariable | None DEFAULT: None

IRQiecComputationType didactic-model

IRQiecComputationType(*, effects: IRQiecEffectRow, result: IRQiecStatic)

Bases: Model

The type of a computation: its effect row and result type.

PARAMETER	DESCRIPTION
effects	The row of effect instances the computation may perform. TYPE: IRQiecEffectRow
result	The type of the value it returns. TYPE: IRQiecStatic

IRQiecEvidence didactic-model

IRQiecEvidence()

Bases: TaggedUnion

Kernel-issued equality evidence.

IRQiecReflexivity didactic-model

IRQiecReflexivity(*, equality: IRQiecEqualityType, kind: Literal['reflexivity'] = 'reflexivity')

Bases: IRQiecEvidence

Evidence that an equality holds because both sides are the same term.

PARAMETER	DESCRIPTION
equality	The proposition witnessed. TYPE: IRQiecEqualityType
kind	The discriminator; always "reflexivity". TYPE: Literal['reflexivity'] DEFAULT: 'reflexivity'

IRQiecBranchGiven didactic-model

IRQiecBranchGiven(*, id: IRQiecId, equality: IRQiecEqualityType, kind: Literal['branch-given'] = 'branch-given')

Bases: IRQiecEvidence

Evidence granted by a case branch's constructor refinement.

PARAMETER	DESCRIPTION
id	The stable identity of the given, derived from the branch scope. TYPE: IRQiecId
equality	The proposition the branch's constructor makes available. TYPE: IRQiecEqualityType
kind	The discriminator; always "branch-given". TYPE: Literal['branch-given'] DEFAULT: 'branch-given'

IRQiecLiteral didactic-model

IRQiecLiteral()

Bases: TaggedUnion

JSON-safe literal data, including bytes and nested tuples.

IRQiecNullLiteral didactic-model

IRQiecNullLiteral(*, kind: Literal['null'] = 'null')

Bases: IRQiecLiteral

The null literal.

PARAMETER	DESCRIPTION
kind	The discriminator; always "null". TYPE: Literal['null'] DEFAULT: 'null'

IRQiecBoolLiteral didactic-model

IRQiecBoolLiteral(*, value: bool, kind: Literal['bool'] = 'bool')

Bases: IRQiecLiteral

A Boolean literal.

PARAMETER	DESCRIPTION
value	The Boolean. TYPE: bool
kind	The discriminator; always "bool". TYPE: Literal['bool'] DEFAULT: 'bool'

IRQiecIntLiteral didactic-model

IRQiecIntLiteral(*, value: int, kind: Literal['int'] = 'int')

Bases: IRQiecLiteral

An integer literal.

PARAMETER	DESCRIPTION
value	The integer. TYPE: int
kind	The discriminator; always "int". TYPE: Literal['int'] DEFAULT: 'int'

IRQiecFloatLiteral didactic-model

IRQiecFloatLiteral(*, value: float, kind: Literal['float'] = 'float')

Bases: IRQiecLiteral

A floating-point literal.

PARAMETER	DESCRIPTION
value	The number. TYPE: float
kind	The discriminator; always "float". TYPE: Literal['float'] DEFAULT: 'float'

IRQiecStringLiteral didactic-model

IRQiecStringLiteral(*, value: str, kind: Literal['string'] = 'string')

Bases: IRQiecLiteral

A string literal.

PARAMETER	DESCRIPTION
value	The string. TYPE: str
kind	The discriminator; always "string". TYPE: Literal['string'] DEFAULT: 'string'

IRQiecBytesLiteral didactic-model

IRQiecBytesLiteral(*, value: str, kind: Literal['bytes'] = 'bytes')

Bases: IRQiecLiteral

A byte-string literal.

PARAMETER	DESCRIPTION
value	The bytes, written as a hexadecimal string. TYPE: str
kind	The discriminator; always "bytes". TYPE: Literal['bytes'] DEFAULT: 'bytes'

IRQiecTupleLiteral didactic-model

IRQiecTupleLiteral(*, items: tuple[IRQiecLiteral, ...], kind: Literal['tuple'] = 'tuple')

Bases: IRQiecLiteral

A tuple of literals.

PARAMETER	DESCRIPTION
items	The component literals, in order. TYPE: tuple[IRQiecLiteral, ...]
kind	The discriminator; always "tuple". TYPE: Literal['tuple'] DEFAULT: 'tuple'

IRQiecValue didactic-model

IRQiecValue()

Bases: TaggedUnion

Stable value node consumed by QIEC-capable renderers.

IRQiecVar didactic-model

IRQiecVar(*, local: IRQiecLocal, kind: Literal['var'] = 'var')

Bases: IRQiecValue

Reference to a bound local.

PARAMETER	DESCRIPTION
local	The binder referenced. TYPE: IRQiecLocal
kind	The discriminator; always "var". TYPE: Literal['var'] DEFAULT: 'var'

IRQiecLiteralValue didactic-model

IRQiecLiteralValue(*, value: IRQiecLiteral, type: IRQiecStatic, kind: Literal['literal'] = 'literal')

Bases: IRQiecValue

A literal host value at a primitive or tuple type.

PARAMETER	DESCRIPTION
value	The literal's data. TYPE: IRQiecLiteral
type	The literal's type. TYPE: IRQiecStatic
kind	The discriminator; always "literal". TYPE: Literal['literal'] DEFAULT: 'literal'

IRQiecConstructorValue didactic-model

IRQiecConstructorValue(*, constructor: IRQiecId, static_arguments: tuple[IRQiecStatic, ...], fields: tuple[IRQiecValue, ...], result_type: IRQiecStatic, kind: Literal['constructor'] = 'constructor')

Bases: IRQiecValue

Application of a declared constructor to static and value arguments.

PARAMETER	DESCRIPTION
constructor	The stable identity of the constructor applied. TYPE: IRQiecId
static_arguments	The constructor's telescope instantiation, in binder order. TYPE: tuple[IRQiecStatic, ...]
fields	The field values, in declaration order. TYPE: tuple[IRQiecValue, ...]
result_type	The indexed family type the application inhabits. TYPE: IRQiecStatic
kind	The discriminator; always "constructor". TYPE: Literal['constructor'] DEFAULT: 'constructor'

IRQiecEvidenceValue didactic-model

IRQiecEvidenceValue(*, evidence: IRQiecEvidence, kind: Literal['evidence'] = 'evidence')

Bases: IRQiecValue

Kernel-checked equality evidence used as a value.

PARAMETER	DESCRIPTION
evidence	The evidence term. TYPE: IRQiecEvidence
kind	The discriminator; always "evidence". TYPE: Literal['evidence'] DEFAULT: 'evidence'

IRQiecAttachmentRef didactic-model

IRQiecAttachmentRef(*, attachment: IRQiecId, type: IRQiecStatic, kind: Literal['attachment'] = 'attachment')

Bases: IRQiecValue

A stable reference to a runtime-owned host value.

PARAMETER	DESCRIPTION
attachment	The identity under which a runtime provider binds the host value. TYPE: IRQiecId
type	The type the bound value inhabits. TYPE: IRQiecStatic
kind	The discriminator; always "attachment". TYPE: Literal['attachment'] DEFAULT: 'attachment'

IRQiecPrimitiveApplication didactic-model

IRQiecPrimitiveApplication(*, primitive: IRQiecId, name: str, arguments: tuple[IRQiecValue, ...], result_type: IRQiecStatic, origin: IRQiecSourceOrigin, kind: Literal['primitive'] = 'primitive')

Bases: IRQiecValue

Application of a pure primitive from the closed registry.

PARAMETER	DESCRIPTION
primitive	The primitive's stable identity. TYPE: IRQiecId
name	The primitive's nominal name. TYPE: str
arguments	The value arguments, in order. TYPE: tuple[IRQiecValue, ...]
result_type	The primitive's result type. TYPE: IRQiecStatic
origin	The application's source location. TYPE: IRQiecSourceOrigin
kind	The discriminator; always "primitive". TYPE: Literal['primitive'] DEFAULT: 'primitive'

IRQiecTupleValue didactic-model

IRQiecTupleValue(*, items: tuple[IRQiecValue, ...], result_type: IRQiecStatic, kind: Literal['tuple'] = 'tuple')

Bases: IRQiecValue

Construction of a finite product from its components.

PARAMETER	DESCRIPTION
items	The component values, in order. TYPE: tuple[IRQiecValue, ...]
result_type	The product type. TYPE: IRQiecStatic
kind	The discriminator; always "tuple". TYPE: Literal['tuple'] DEFAULT: 'tuple'

IRQiecTensorValue didactic-model

IRQiecTensorValue(*, items: tuple[IRQiecValue, ...], result_type: IRQiecStatic, kind: Literal['tensor'] = 'tensor')

Bases: IRQiecValue

Construction of a tensor from its entries along the outermost axis.

PARAMETER	DESCRIPTION
items	The entries, each an element or a tensor one rank lower. TYPE: tuple[IRQiecValue, ...]
result_type	The Tensor type constructed. TYPE: IRQiecStatic
kind	The discriminator; always "tensor". TYPE: Literal['tensor'] DEFAULT: 'tensor'

IRQiecProjection didactic-model

IRQiecProjection(*, value: IRQiecValue, position: int, result_type: IRQiecStatic, kind: Literal['projection'] = 'projection')

Bases: IRQiecValue

Selection of one component of a finite product.

PARAMETER	DESCRIPTION
value	The product value. TYPE: IRQiecValue
position	The zero-based component selected. TYPE: int
result_type	The component's type. TYPE: IRQiecStatic
kind	The discriminator; always "projection". TYPE: Literal['projection'] DEFAULT: 'projection'

IRQiecNamedArgument didactic-model

IRQiecNamedArgument(*, name: str, value: IRQiecValue)

Bases: Model

One named argument of a distribution construction.

PARAMETER	DESCRIPTION
name	The family parameter supplied. TYPE: str
value	The value supplied for it. TYPE: IRQiecValue

IRQiecPlateAxis didactic-model

IRQiecPlateAxis(*, name: str, size: IRQiecStatic)

Bases: Model

One axis of a plated distribution.

PARAMETER	DESCRIPTION
name	The axis's source name. TYPE: str
size	Its extent, an index term. TYPE: IRQiecStatic

IRQiecPlateShape didactic-model

IRQiecPlateShape(*, batch: tuple[IRQiecPlateAxis, ...] = (), event: tuple[IRQiecPlateAxis, ...] = ())

Bases: Model

The plate a distribution is constructed over.

PARAMETER	DESCRIPTION
batch	The independent replication axes, outermost first. TYPE: tuple[IRQiecPlateAxis, ...] DEFAULT: ()
event	The joint axes, outermost first. TYPE: tuple[IRQiecPlateAxis, ...] DEFAULT: ()

IRQiecDistributionValue didactic-model

IRQiecDistributionValue(*, family: IRQiecId, name: str, arguments: tuple[IRQiecNamedArgument, ...], result_type: IRQiecStatic, origin: IRQiecSourceOrigin, plate: IRQiecPlateShape = IRQiecPlateShape(), kind: Literal['distribution'] = 'distribution')

Bases: IRQiecValue

Construction of a distribution from a family of the registry.

PARAMETER	DESCRIPTION
family	The family's stable identity. TYPE: IRQiecId
name	The family's source name. TYPE: str
arguments	The named parameters, in source order. TYPE: tuple[IRQiecNamedArgument, ...]
result_type	The Sampleable type constructed. TYPE: IRQiecStatic
origin	The construction's source location. TYPE: IRQiecSourceOrigin
plate	The plate the construction ranges over; empty for one draw. TYPE: IRQiecPlateShape DEFAULT: IRQiecPlateShape()
kind	The discriminator; always "distribution". TYPE: Literal['distribution'] DEFAULT: 'distribution'

IRQiecLogDensity didactic-model

IRQiecLogDensity(*, sampleable: IRQiecValue, value: IRQiecValue, origin: IRQiecSourceOrigin, batch: tuple[IRQiecPlateAxis, ...] = (), kind: Literal['log_density'] = 'log_density')

Bases: IRQiecValue

Evaluation of a distribution's log density at a value.

PARAMETER	DESCRIPTION
sampleable	The distribution. TYPE: IRQiecValue
value	The point evaluated. TYPE: IRQiecValue
origin	The evaluation's source location. TYPE: IRQiecSourceOrigin
batch	The batch axes the weights are kept apart over; empty for one total weight. TYPE: tuple[IRQiecPlateAxis, ...] DEFAULT: ()
kind	The discriminator; always "log_density". TYPE: Literal['log_density'] DEFAULT: 'log_density'

IRQiecGather didactic-model

IRQiecGather(*, value: IRQiecValue, index: IRQiecValue, result_type: IRQiecStatic, kind: Literal['gather'] = 'gather')

Bases: IRQiecValue

Selection along a tensor's outermost axis.

PARAMETER	DESCRIPTION
value	The tensor selected from. TYPE: IRQiecValue
index	An integer or a tensor of integers. TYPE: IRQiecValue
result_type	The selection's type. TYPE: IRQiecStatic
kind	The discriminator; always "gather". TYPE: Literal['gather'] DEFAULT: 'gather'

IRQiecWeightSum didactic-model

IRQiecWeightSum(*, value: IRQiecValue, kind: Literal['weight_sum'] = 'weight_sum')

Bases: IRQiecValue

The total of a tensor of log weights.

PARAMETER	DESCRIPTION
value	The weights. TYPE: IRQiecValue
kind	The discriminator; always "weight_sum". TYPE: Literal['weight_sum'] DEFAULT: 'weight_sum'

IRQiecSegmentSum didactic-model

IRQiecSegmentSum(*, value: IRQiecValue, index: IRQiecValue, groups: IRQiecStatic, result_type: IRQiecStatic, kind: Literal['segment_sum'] = 'segment_sum')

Bases: IRQiecValue

Per-group totals of a vector of log weights.

PARAMETER	DESCRIPTION
value	The weights. TYPE: IRQiecValue
index	Each entry's group. TYPE: IRQiecValue
groups	The number of groups. TYPE: IRQiecStatic
result_type	The totals' type. TYPE: IRQiecStatic
kind	The discriminator; always "segment_sum". TYPE: Literal['segment_sum'] DEFAULT: 'segment_sum'

IRQiecKernelMatrix didactic-model

IRQiecKernelMatrix(*, inputs: IRQiecValue, kernel: str, length_scale: float, jitter: float, result_type: IRQiecStatic, kind: Literal['kernel_matrix'] = 'kernel_matrix')

Bases: IRQiecValue

A covariance matrix over input locations.

PARAMETER	DESCRIPTION
inputs	The locations. TYPE: IRQiecValue
kernel	The kernel's name. TYPE: str
length_scale	Its length scale. TYPE: float
jitter	The diagonal jitter. TYPE: float
result_type	The matrix type. TYPE: IRQiecStatic
kind	The discriminator; always "kernel_matrix". TYPE: Literal['kernel_matrix'] DEFAULT: 'kernel_matrix'

IRQiecAffineMap didactic-model

IRQiecAffineMap(*, weight: IRQiecValue, bias: IRQiecValue, sources: tuple[IRQiecValue, ...], row_offset: int, rows: int, transform: Literal['identity', 'exp', 'exp_floor'], result_type: IRQiecStatic, kind: Literal['affine_map'] = 'affine_map')

Bases: IRQiecValue

One head of an affine parameter map.

PARAMETER	DESCRIPTION
weight	The weight matrix. TYPE: IRQiecValue
bias	The bias vector. TYPE: IRQiecValue
sources	The conditioning row's factors in order. TYPE: tuple[IRQiecValue, ...]
row_offset	The first row of the head's block. TYPE: int
rows	The block's height. TYPE: int
transform	"identity", "exp", or "exp_floor". TYPE: Literal['identity', 'exp', 'exp_floor']
result_type	The head's type. TYPE: IRQiecStatic
kind	The discriminator; always "affine_map". TYPE: Literal['affine_map'] DEFAULT: 'affine_map'

IRQiecTableMap didactic-model

IRQiecTableMap(*, table: IRQiecValue, index: IRQiecValue, row_offset: int, rows: int, transform: Literal['identity', 'exp', 'exp_floor'], result_type: IRQiecStatic, kind: Literal['table_map'] = 'table_map')

Bases: IRQiecValue

One head of a table-indexed parameter map.

PARAMETER	DESCRIPTION
table	The parameter table, one row per element of the domain. TYPE: IRQiecValue
index	The element of the domain. TYPE: IRQiecValue
row_offset	The first column of the head's block. TYPE: int
rows	The block's width. TYPE: int
transform	"identity", "exp", or "exp_floor". TYPE: Literal['identity', 'exp', 'exp_floor']
result_type	The head's type. TYPE: IRQiecStatic
kind	The discriminator; always "table_map". TYPE: Literal['table_map'] DEFAULT: 'table_map'

IRQiecSiteValue didactic-model

IRQiecSiteValue(*, label: str, result_type: IRQiecStatic, kind: Literal['site'] = 'site')

Bases: IRQiecValue

A named sample site.

PARAMETER	DESCRIPTION
label	The site's source name. TYPE: str
result_type	The Site type of the value it produces. TYPE: IRQiecStatic
kind	The discriminator; always "site". TYPE: Literal['site'] DEFAULT: 'site'

IRQiecReduction didactic-model

IRQiecReduction(*, operator: str, value: IRQiecValue, result_type: IRQiecStatic, kind: Literal['reduction'] = 'reduction')

Bases: IRQiecValue

A number summarizing every entry of a tensor.

PARAMETER	DESCRIPTION
operator	The reduction. TYPE: str
value	The tensor. TYPE: IRQiecValue
result_type	The element type. TYPE: IRQiecStatic
kind	The discriminator; always "reduction". TYPE: Literal['reduction'] DEFAULT: 'reduction'

IRQiecRowwise didactic-model

IRQiecRowwise(*, operator: str, value: IRQiecValue, result_type: IRQiecStatic, kind: Literal['rowwise'] = 'rowwise')

Bases: IRQiecValue

An operation along a tensor's last axis keeping its shape.

PARAMETER	DESCRIPTION
operator	The operation. TYPE: str
value	The tensor. TYPE: IRQiecValue
result_type	The tensor's type. TYPE: IRQiecStatic
kind	The discriminator; always "rowwise". TYPE: Literal['rowwise'] DEFAULT: 'rowwise'

IRQiecComprehension didactic-model

IRQiecComprehension(*, binder: IRQiecLocal, extent: IRQiecStatic, body: IRQiecValue, result_type: IRQiecStatic, kind: Literal['comprehension'] = 'comprehension')

Bases: IRQiecValue

A tensor built by evaluating a body at every index of an axis.

PARAMETER	DESCRIPTION
binder	The index local. TYPE: IRQiecLocal
extent	The axis's extent. TYPE: IRQiecStatic
body	The entry at each index. TYPE: IRQiecValue
result_type	The tensor type. TYPE: IRQiecStatic
kind	The discriminator; always "comprehension". TYPE: Literal['comprehension'] DEFAULT: 'comprehension'

IRQiecTransportValue didactic-model

IRQiecTransportValue(*, evidence: IRQiecEvidence, value: IRQiecValue, target_type: IRQiecStatic, kind: Literal['transport'] = 'transport')

Bases: IRQiecValue

Transport of a value along kernel-checked equality evidence.

PARAMETER	DESCRIPTION
evidence	The equality the value is carried across. TYPE: IRQiecEvidence
value	The value at the equality's left type. TYPE: IRQiecValue
target_type	The type the transported value inhabits, which the equality's right side determines. TYPE: IRQiecStatic
kind	The discriminator; always "transport". TYPE: Literal['transport'] DEFAULT: 'transport'

IRQiecEffectRequest didactic-model

IRQiecEffectRequest(*, instance: IRQiecId, effect: IRQiecEffectRef, operation: IRQiecId, static_arguments: tuple[IRQiecStatic, ...], arguments: tuple[IRQiecValue, ...], result_type: IRQiecStatic, origin: IRQiecSiteProvenance)

Bases: Model

A typed request for one effect operation.

PARAMETER	DESCRIPTION
instance	The effect instance the request is addressed to. TYPE: IRQiecId
effect	The instance's interface application. TYPE: IRQiecEffectRef
operation	The operation requested. TYPE: IRQiecId
static_arguments	The operation's telescope instantiation, in binder order. TYPE: tuple[IRQiecStatic, ...]
arguments	The value arguments, one per operation argument. TYPE: tuple[IRQiecValue, ...]
result_type	The type of the value the operation returns under the instantiation. TYPE: IRQiecStatic
origin	Where the request was written and how it was reached. TYPE: IRQiecSiteProvenance

IRQiecComputation didactic-model

IRQiecComputation()

Bases: TaggedUnion

Stable computation node consumed by QIEC-capable renderers.

IRQiecReturn didactic-model

IRQiecReturn(*, value: IRQiecValue, kind: Literal['return'] = 'return')

Bases: IRQiecComputation

Return of a value with no effects.

PARAMETER	DESCRIPTION
value	The value produced. TYPE: IRQiecValue
kind	The discriminator; always "return". TYPE: Literal['return'] DEFAULT: 'return'

IRQiecBindStep didactic-model

IRQiecBindStep(*, binder: IRQiecLocal, first: IRQiecComputation)

Bases: Model

One step of a bind sequence: a computation and the local it binds.

PARAMETER	DESCRIPTION
binder	The local the step's result is bound to. TYPE: IRQiecLocal
first	The computation run at the step. TYPE: IRQiecComputation

IRQiecBind didactic-model

IRQiecBind(*, steps: tuple[IRQiecBindStep, ...], then: IRQiecComputation, kind: Literal['bind'] = 'bind')

Bases: IRQiecComputation

A straight-line sequence of binds ending in a computation.

A kernel Bind chain nests one bind inside the next; the mirror keeps the chain flat so a long straight-line body is a tuple of steps rather than a term as deep as it is long.

PARAMETER	DESCRIPTION
steps	The binds, in evaluation order; each may read the binders before it. TYPE: tuple[IRQiecBindStep, ...]
then	The computation after the last step, which may read every binder. TYPE: IRQiecComputation
kind	The discriminator; always "bind". TYPE: Literal['bind'] DEFAULT: 'bind'

IRQiecPerform didactic-model

IRQiecPerform(*, request: IRQiecEffectRequest, kind: Literal['perform'] = 'perform')

Bases: IRQiecComputation

Performance of one effect operation.

PARAMETER	DESCRIPTION
request	The operation, its instance, arguments, and result type. TYPE: IRQiecEffectRequest
kind	The discriminator; always "perform". TYPE: Literal['perform'] DEFAULT: 'perform'

IRQiecHandle didactic-model

IRQiecHandle(*, instance: IRQiecId, handler: IRQiecId, computation: IRQiecComputation, static_arguments: tuple[IRQiecStatic, ...] = (), kind: Literal['handle'] = 'handle')

Bases: IRQiecComputation

A computation run under a handler installed for one effect instance.

PARAMETER	DESCRIPTION
instance	The effect instance whose operations the handler intercepts. TYPE: IRQiecId
handler	The stable identity of the handler installed. TYPE: IRQiecId
computation	The handled computation. TYPE: IRQiecComputation
static_arguments	The handler's telescope instantiation, in binder order. TYPE: tuple[IRQiecStatic, ...] DEFAULT: ()
kind	The discriminator; always "handle". TYPE: Literal['handle'] DEFAULT: 'handle'

IRQiecCaseMotive didactic-model

IRQiecCaseMotive(*, indices: tuple[IRQiecBinder, ...], result_type: IRQiecStatic)

Bases: Model

The result family of an indexed case expression.

PARAMETER	DESCRIPTION
indices	The binders abstracting the scrutinee's indices in result_type. TYPE: tuple[IRQiecBinder, ...]
result_type	The type every branch produces, over indices. TYPE: IRQiecStatic

IRQiecCaseBranch didactic-model

IRQiecCaseBranch(*, constructor: IRQiecId, static_arguments: tuple[IRQiecStatic, ...], fields: tuple[IRQiecLocal, ...], body: IRQiecComputation, scope: IRQiecId)

Bases: Model

One branch of an indexed case expression.

PARAMETER	DESCRIPTION
constructor	The constructor this branch matches. TYPE: IRQiecId
static_arguments	The constructor's static arguments as bound by the pattern, in binder order. TYPE: tuple[IRQiecStatic, ...]
fields	The locals binding the constructor's fields, in declaration order. TYPE: tuple[IRQiecLocal, ...]
body	The computation run when the branch is selected. TYPE: IRQiecComputation
scope	The static scope identity under which the branch's skolems and equality evidence are minted. TYPE: IRQiecId

IRQiecCase didactic-model

IRQiecCase(*, scrutinee: IRQiecValue, motive: IRQiecCaseMotive, branches: tuple[IRQiecCaseBranch, ...], kind: Literal['case'] = 'case')

Bases: IRQiecComputation

Case analysis over an indexed family value.

PARAMETER	DESCRIPTION
scrutinee	The value analyzed. TYPE: IRQiecValue
motive	The result family, over the scrutinee's indices. TYPE: IRQiecCaseMotive
branches	One branch per constructor considered. TYPE: tuple[IRQiecCaseBranch, ...]
kind	The discriminator; always "case". TYPE: Literal['case'] DEFAULT: 'case'

IRQiecIf didactic-model

IRQiecIf(*, condition: IRQiecValue, then: IRQiecComputation, otherwise: IRQiecComputation, kind: Literal['if'] = 'if')

Bases: IRQiecComputation

Branch on a Boolean value.

PARAMETER	DESCRIPTION
condition	The Boolean value branched on. TYPE: IRQiecValue
then	The computation run when the condition holds. TYPE: IRQiecComputation
otherwise	The computation run when it does not. TYPE: IRQiecComputation
kind	The discriminator; always "if". TYPE: Literal['if'] DEFAULT: 'if'

IRQiecCall didactic-model

IRQiecCall(*, callee: IRQiecId, name: str, static_arguments: tuple[IRQiecStatic, ...], arguments: tuple[IRQiecValue, ...], result_type: IRQiecStatic, effects: IRQiecEffectRow, origin: IRQiecSourceOrigin, kind: Literal['call'] = 'call')

Bases: IRQiecComputation

Application of a named computation by stable identity.

PARAMETER	DESCRIPTION
callee	The identity of the computation called. TYPE: IRQiecId
name	The callee's display name. TYPE: str
static_arguments	The callee's telescope instantiation, in binder order. TYPE: tuple[IRQiecStatic, ...]
arguments	The value arguments, one per callee parameter. TYPE: tuple[IRQiecValue, ...]
result_type	The callee's result type under the instantiation. TYPE: IRQiecStatic
effects	The callee's effect row under the instantiation. TYPE: IRQiecEffectRow
origin	The call site's source location. TYPE: IRQiecSourceOrigin
kind	The discriminator; always "call". TYPE: Literal['call'] DEFAULT: 'call'

IRQiecResume didactic-model

IRQiecResume(*, value: IRQiecValue, origin: IRQiecSourceOrigin, kind: Literal['resume'] = 'resume')

Bases: IRQiecComputation

Invocation of the enclosing handler clause's continuation.

PARAMETER	DESCRIPTION
value	The value returned to the suspended computation. TYPE: IRQiecValue
origin	The resumption's source location. TYPE: IRQiecSourceOrigin
kind	The discriminator; always "resume". TYPE: Literal['resume'] DEFAULT: 'resume'

IRQiecNewInstance didactic-model

IRQiecNewInstance(*, instance: IRQiecId, effect: IRQiecEffectRef, body: IRQiecComputation, origin: IRQiecSourceOrigin, kind: Literal['new_instance'] = 'new_instance')

Bases: IRQiecComputation

Lexically scoped allocation of an effect instance.

PARAMETER	DESCRIPTION
instance	The scope-derived identity of the allocated instance. TYPE: IRQiecId
effect	The applied interface the instance provides. TYPE: IRQiecEffectRef
body	The computation within which the instance is in scope. TYPE: IRQiecComputation
origin	The allocation's source location. TYPE: IRQiecSourceOrigin
kind	The discriminator; always "new_instance". TYPE: Literal['new_instance'] DEFAULT: 'new_instance'

IRQiecFieldDef didactic-model

IRQiecFieldDef(*, name: str, type: IRQiecStatic)

Bases: Model

One named, typed field of a constructor.

PARAMETER	DESCRIPTION
name	The field's display name. TYPE: str
type	The field's type, which may mention the constructor's telescope. TYPE: IRQiecStatic

IRQiecFamilyDecl didactic-model

IRQiecFamilyDecl(*, id: IRQiecId, name: str, parameters: tuple[IRQiecBinder, ...], indices: tuple[IRQiecBinder, ...], constructors: tuple[IRQiecId, ...], closed: bool = True)

Bases: Model

A closed or opaque indexed data family.

PARAMETER	DESCRIPTION
id	The family's stable identity. TYPE: IRQiecId
name	The family's source name. TYPE: str
parameters	The binders uniform across every constructor. TYPE: tuple[IRQiecBinder, ...]
indices	The binders a constructor result may refine. TYPE: tuple[IRQiecBinder, ...]
constructors	The constructors the family declares. TYPE: tuple[IRQiecId, ...]
closed	Whether the constructor list is exhaustive, which admits coverage checking. TYPE: bool DEFAULT: True

IRQiecConstructorDecl didactic-model

IRQiecConstructorDecl(*, id: IRQiecId, family: IRQiecId, name: str, telescope: tuple[IRQiecBinder, ...], fields: tuple[IRQiecFieldDef, ...], result_indices: tuple[IRQiecStatic, ...])

Bases: Model

One constructor of an indexed data family.

PARAMETER	DESCRIPTION
id	The constructor's stable identity. TYPE: IRQiecId
family	The family the constructor belongs to. TYPE: IRQiecId
name	The constructor's source name. TYPE: str
telescope	The binders local to the constructor, which are rigid while a branch matching it is checked. TYPE: tuple[IRQiecBinder, ...]
fields	The values the constructor carries. TYPE: tuple[IRQiecFieldDef, ...]
result_indices	What the constructor fixes the family's indices to, one per family index. TYPE: tuple[IRQiecStatic, ...]

IRQiecArgumentDef didactic-model

IRQiecArgumentDef(*, name: str, type: IRQiecStatic)

Bases: Model

One named, typed value argument of an operation.

PARAMETER	DESCRIPTION
name	The argument's display name. TYPE: str
type	The argument's type, which may mention the operation's telescope. TYPE: IRQiecStatic

IRQiecOperationDef didactic-model

IRQiecOperationDef(*, id: IRQiecId, name: str, telescope: tuple[IRQiecBinder, ...], arguments: tuple[IRQiecArgumentDef, ...], result_type: IRQiecStatic)

Bases: Model

One result-indexed request constructor of an effect interface.

PARAMETER	DESCRIPTION
id	The operation's stable identity. TYPE: IRQiecId
name	The operation's source name. TYPE: str
telescope	The static binders the operation adds to the interface's own. TYPE: tuple[IRQiecBinder, ...]
arguments	The value arguments the request carries. TYPE: tuple[IRQiecArgumentDef, ...]
result_type	What resuming the request supplies. TYPE: IRQiecStatic

IRQiecEffectDef didactic-model

IRQiecEffectDef(*, ref: IRQiecEffectRef, telescope: tuple[IRQiecBinder, ...], operations: tuple[IRQiecOperationDef, ...])

Bases: Model

An effect interface: its telescope and operations.

PARAMETER	DESCRIPTION
ref	The declaration's own reference. TYPE: IRQiecEffectRef
telescope	The static binders the interface takes. TYPE: tuple[IRQiecBinder, ...]
operations	The declared operations. TYPE: tuple[IRQiecOperationDef, ...]

IRQiecHandlerClauseDef didactic-model

IRQiecHandlerClauseDef(*, operation: IRQiecId, grade: Literal['0', 'aff', '1', 'omega'], parameters: tuple[IRQiecLocal, ...] = (), body: IRQiecComputation | None = None)

Bases: Model

One operation a handler covers, and how it may resume.

PARAMETER	DESCRIPTION
operation	The operation the clause handles. TYPE: IRQiecId
grade	How often the clause may invoke its continuation: never ("0"), at most once ("aff"), exactly once ("1"), or any number of times ("omega"). TYPE: Literal['0', 'aff', '1', 'omega']
parameters	The binders for the operation's value arguments, in declaration order. TYPE: tuple[IRQiecLocal, ...] DEFAULT: ()
body	What the clause does, or None for a clause whose implementation a runtime provider supplies. TYPE: IRQiecComputation | None DEFAULT: None

IRQiecHandlerReturnClauseDef didactic-model

IRQiecHandlerReturnClauseDef(*, binder: IRQiecLocal, body: IRQiecComputation)

Bases: Model

What a handler does with a value its computation returns.

PARAMETER	DESCRIPTION
binder	The local naming the returned value inside the body. TYPE: IRQiecLocal
body	What the handler produces from it. TYPE: IRQiecComputation

IRQiecHandlerDef didactic-model

IRQiecHandlerDef(*, id: IRQiecId, name: str, effect: IRQiecEffectRef, clauses: tuple[IRQiecHandlerClauseDef, ...], input_type: IRQiecStatic, output_type: IRQiecStatic, introduced: IRQiecEffectRow, total: bool, forwards_unknown: bool, telescope: tuple[IRQiecBinder, ...], return_clause: IRQiecHandlerReturnClauseDef | None = None, implementation: Literal['authored', 'foreign'] = 'foreign')

Bases: Model

The type-and-coverage signature of a handler.

PARAMETER	DESCRIPTION
id	The handler's stable identity. TYPE: IRQiecId
name	The handler's display name. TYPE: str
effect	The interface application the handler handles. TYPE: IRQiecEffectRef
clauses	One clause per operation the handler covers. TYPE: tuple[IRQiecHandlerClauseDef, ...]
input_type	The result type of the computation the handler accepts. TYPE: IRQiecStatic
output_type	The type of the handler's answer. TYPE: IRQiecStatic
introduced	The effects the handler's own clauses perform. TYPE: IRQiecEffectRow
total	Whether the clauses cover every operation of effect. TYPE: bool
forwards_unknown	Whether an operation no clause covers is forwarded outward rather than rejected. TYPE: bool
telescope	The static parameters the handler abstracts over, in order. TYPE: tuple[IRQiecBinder, ...]
return_clause	How the handler answers the computation's return, or None to return the value unchanged. TYPE: IRQiecHandlerReturnClauseDef | None DEFAULT: None
implementation	"authored" when every clause carries a body, "foreign" when a runtime provider supplies the behavior. TYPE: Literal['authored', 'foreign'] DEFAULT: 'foreign'

IRQiecNamedEffectInstance didactic-model

IRQiecNamedEffectInstance(*, name: str, entry: IRQiecRowEntry, origin: IRQiecSourceOrigin)

Bases: Model

A source name for one lexical effect instance.

PARAMETER	DESCRIPTION
name	The name requests resolve through. TYPE: str
entry	The allocated instance and its interface application. TYPE: IRQiecRowEntry
origin	Where the instance was declared. TYPE: IRQiecSourceOrigin

IRQiecNamedComputation didactic-model

IRQiecNamedComputation(*, id: IRQiecId, name: str, telescope: tuple[IRQiecBinder, ...], parameters: tuple[IRQiecLocal, ...], body: IRQiecComputation, type: IRQiecComputationType, origin: IRQiecSourceOrigin)

Bases: Model

One named computation and its checked type.

PARAMETER	DESCRIPTION
id	The computation's stable identity, which calls refer to. TYPE: IRQiecId
name	The display name, unique within the module. TYPE: str
telescope	The static parameters the computation abstracts over, in order. TYPE: tuple[IRQiecBinder, ...]
parameters	The value parameters, in order. TYPE: tuple[IRQiecLocal, ...]
body	The computation's body, with the parameters in scope. TYPE: IRQiecComputation
type	The checked effect row and result type of body. TYPE: IRQiecComputationType
origin	Where the computation was declared. TYPE: IRQiecSourceOrigin

IRQiecProgramParameter didactic-model

IRQiecProgramParameter(*, name: str, role: str, type: IRQiecStatic, axes: tuple[str, ...] = ())

Bases: Model

One parameter of an elaborated program.

PARAMETER	DESCRIPTION
name	The parameter's name. TYPE: str
role	How it is supplied. TYPE: str
type	Its type. TYPE: IRQiecStatic
axes	The name of each dimension of a tensor-typed parameter. TYPE: tuple[str, ...] DEFAULT: ()

IRQiecProgramSite didactic-model

IRQiecProgramSite(*, name: str, kind: str, family: str, batch: tuple[IRQiecPlateAxis, ...] = (), event: tuple[IRQiecPlateAxis, ...] = ())

Bases: Model

One probabilistic step of an elaborated program.

PARAMETER	DESCRIPTION
name	The site's label. TYPE: str
kind	"sample", "observe", or "marginal". TYPE: str
family	The family drawn from. TYPE: str
batch	The plate's batch axes. TYPE: tuple[IRQiecPlateAxis, ...] DEFAULT: ()
event	The plate's event axes. TYPE: tuple[IRQiecPlateAxis, ...] DEFAULT: ()

IRQiecProgramEntry didactic-model

IRQiecProgramEntry(*, name: str, computation: IRQiecId, parameters: tuple[IRQiecProgramParameter, ...], return_names: tuple[str, ...], return_labels: tuple[str, ...] | None, sites: tuple[IRQiecProgramSite, ...], random_instance: IRQiecId, score_instance: IRQiecId, telescope: tuple[IRQiecBinder, ...] = ())

Bases: Model

The typed entry point a program declaration elaborates to.

PARAMETER	DESCRIPTION
name	The program's name. TYPE: str
computation	The identity of the computation holding its body. TYPE: IRQiecId
parameters	The computation's parameters with their roles. TYPE: tuple[IRQiecProgramParameter, ...]
return_names	The names the program returns. TYPE: tuple[str, ...]
return_labels	The labels of a labelled return, or None. TYPE: tuple[str, ...] | None
sites	The program's probabilistic steps. TYPE: tuple[IRQiecProgramSite, ...]
random_instance	The Random instance the program samples on. TYPE: IRQiecId
score_instance	The Score instance the program scores on. TYPE: IRQiecId
telescope	The static index binders of the open input extents. TYPE: tuple[IRQiecBinder, ...] DEFAULT: ()

IRQiecModule didactic-model

IRQiecModule(*, module: str, source_protocol: str, index_sorts: tuple[IRQiecUserIndexSort, ...] = (), families: tuple[IRQiecFamilyDecl, ...] = (), constructors: tuple[IRQiecConstructorDecl, ...] = (), effects: tuple[IRQiecEffectDef, ...] = (), instances: tuple[IRQiecNamedEffectInstance, ...] = (), handlers: tuple[IRQiecHandlerDef, ...] = (), computations: tuple[IRQiecNamedComputation, ...] = (), entries: tuple[IRQiecProgramEntry, ...] = (), programs: tuple[IRQiecId, ...] = (), gap: str = '', abi: str)

Bases: Model

Lossless structural projection of one checked :class:QiecModule.

program_computations

program_computations() -> frozenset[str]

The computations that hold programs and their marginal helpers.

RETURNS	DESCRIPTION
frozenset[str]	Identity texts of every entry point's computation and of every helper it calls, transitively, as the kernel module recorded them at lowering.

Source code in src/quivers/transpile/qiec_ir.py

def program_computations(self) -> frozenset[str]:
    """The computations that hold programs and their marginal helpers.

    Returns
    -------
    frozenset[str]
        Identity texts of every entry point's computation and of
        every helper it calls, transitively, as the kernel module
        recorded them at lowering.
    """
    return frozenset(identity.text for identity in self.programs)

QiecTargetCapabilities didactic-model

QiecTargetCapabilities(*, features: frozenset[QiecFeature] = frozenset({'declarations'}))

Bases: Model

Feature set one target can preserve without semantic erasure.

PARAMETER	DESCRIPTION
features	The features the target preserves. TYPE: frozenset[QiecFeature] DEFAULT: frozenset({'declarations'})

supports

supports(feature: QiecFeature) -> bool

Whether the target preserves one feature.

PARAMETER	DESCRIPTION
feature	The feature asked about. TYPE: QiecFeature

RETURNS	DESCRIPTION
bool	True when feature is in the set.

Source code in src/quivers/transpile/qiec_ir.py

def supports(self, feature: QiecFeature) -> bool:
    """Whether the target preserves one feature.

    Parameters
    ----------
    feature
        The feature asked about.

    Returns
    -------
    bool
        ``True`` when ``feature`` is in the set.
    """
    return feature in self.features

QiecCapabilityDiagnostic didactic-model

QiecCapabilityDiagnostic(*, code: Literal['qiec-capability'] = 'qiec-capability', target: str, feature: QiecFeature, computation: str | None = None, origin: IRQiecSourceOrigin | None = None, detail: str)

Bases: Model

One precise target mismatch discovered before renderer dispatch.

PARAMETER	DESCRIPTION
code	The diagnostic code; always "qiec-capability". TYPE: Literal['qiec-capability'] DEFAULT: 'qiec-capability'
target	The target that lacks the feature. TYPE: str
feature	The feature the target lacks. TYPE: QiecFeature
computation	The computation that needs the feature, or None for the module. TYPE: str | None DEFAULT: None
origin	Where the computation was declared, when known. TYPE: IRQiecSourceOrigin | None DEFAULT: None
detail	Why the target cannot preserve the feature, phrased to follow the target's name, as in "has no semantics-preserving lowering". TYPE: str

kind property

kind: str

The qiec:capability:<feature>:<subject> refusal identifier.

message property

message: str

The diagnostic as one user-facing sentence.

lower_qiec_ir

lower_qiec_ir(module: QiecModule) -> IRQiecModule

Project an already checked kernel module into structural IR.

PARAMETER	DESCRIPTION
module	The checked module. TYPE: QiecModule

RETURNS	DESCRIPTION
IRQiecModule	The mirror, with the program computations recorded so a renderer need not walk every body to find them.

Source code in src/quivers/transpile/qiec_ir.py

def lower_qiec_ir(module: QiecModule) -> IRQiecModule:
    """Project an already checked kernel module into structural IR.

    Parameters
    ----------
    module : QiecModule
        The checked module.

    Returns
    -------
    IRQiecModule
        The mirror, with the program computations recorded so a renderer
        need not walk every body to find them.
    """
    reachable = m.reachable_computations(module)
    standalone_deduction_roots = (
        {
            computation.id
            for computation in module.computations
            if _is_deduction_origin(computation.origin)
            and computation.name.endswith("__run")
        }
        if not module.entries
        else set()
    )
    values = {
        field.name: _convert(getattr(module, field.name))
        for field in fields(module)
        if field.name not in ("tag", "computations")
    }
    # A deduction's computations serve the reference machine; a target
    # carries them only when a program the module transpiles calls one,
    # and then refuses the search they perform.
    values["computations"] = _convert(
        tuple(
            computation
            for computation in module.computations
            if not _is_deduction_origin(computation.origin)
            or computation.id in reachable
            or computation.id in standalone_deduction_roots
        )
    )
    values["programs"] = tuple(
        _id(identity)
        for identity in sorted(
            m.program_computations(module), key=lambda identity: identity.digest
        )
    )
    return IRQiecModule(**values)

capabilities_for_target

capabilities_for_target(target: str) -> QiecTargetCapabilities

Return the registered QIEC capability set for target.

The eight host-language backends lower the full stable core through the QIEC runtime ABI. Stan admits closed, monomorphic, effect-free scalar computations as user-defined functions: binds, scalar primitives, conditionals, calls, and recursion. BUGS and JAGS admit only return/bind computations, which they inline. Unknown targets safely retain declaration metadata only.

PARAMETER	DESCRIPTION
target	The target name, with or without the qvr- prefix. TYPE: str

RETURNS	DESCRIPTION
QiecTargetCapabilities	The features the target preserves.

Source code in src/quivers/transpile/qiec_ir.py

def capabilities_for_target(target: str) -> QiecTargetCapabilities:
    """Return the registered QIEC capability set for ``target``.

    The eight host-language backends lower the full stable core through the
    QIEC runtime ABI. Stan admits closed, monomorphic, effect-free scalar
    computations as user-defined functions: binds, scalar primitives,
    conditionals, calls, and recursion. BUGS and JAGS admit only
    ``return``/``bind`` computations, which they inline. Unknown targets
    safely retain declaration metadata only.

    Parameters
    ----------
    target
        The target name, with or without the ``qvr-`` prefix.

    Returns
    -------
    QiecTargetCapabilities
        The features the target preserves.
    """
    normalized = target.removeprefix("qvr-").lower()
    if normalized in {
        "pyro",
        "numpyro",
        "pymc",
        "edward2",
        "turing",
        "gen",
        "webppl",
        "church",
    }:
        return _GENERIC_RUNTIME
    if normalized == "stan":
        return _STAN_STATIC
    if normalized in {"bugs", "jags"}:
        return _GRAPH_STATIC
    return _DECLARATION_ONLY

analyze_qiec_capabilities

analyze_qiec_capabilities(module_or_ir: QiecModule | IRQiecModule | None, target: str, *, capabilities: QiecTargetCapabilities | None = None) -> tuple[QiecCapabilityDiagnostic, ...]

Report every QIEC feature target cannot preserve.

PARAMETER	DESCRIPTION
module_or_ir	The checked module or its IR projection; None reports nothing. TYPE: QiecModule | IRQiecModule | None
target	The target name. TYPE: str
capabilities	The feature set to check against, else the target's registered one. TYPE: QiecTargetCapabilities | None DEFAULT: None

RETURNS	DESCRIPTION
tuple[QiecCapabilityDiagnostic, ...]	One diagnostic per feature a computation or handler needs that the target lacks. Program computations and their marginal helpers are excluded: a renderer emits them from the program's target plan rather than through the host runtime.

Source code in src/quivers/transpile/qiec_ir.py

def analyze_qiec_capabilities(
    module_or_ir: QiecModule | IRQiecModule | None,
    target: str,
    *,
    capabilities: QiecTargetCapabilities | None = None,
) -> tuple[QiecCapabilityDiagnostic, ...]:
    """Report every QIEC feature ``target`` cannot preserve.

    Parameters
    ----------
    module_or_ir
        The checked module or its IR projection; ``None`` reports nothing.
    target
        The target name.
    capabilities
        The feature set to check against, else the target's registered
        one.

    Returns
    -------
    tuple[QiecCapabilityDiagnostic, ...]
        One diagnostic per feature a computation or handler needs that
        the target lacks. Program computations and their marginal
        helpers are excluded: a renderer emits them from the program's
        target plan rather than through the host runtime.
    """
    if module_or_ir is None:
        return ()
    module = (
        module_or_ir
        if isinstance(module_or_ir, IRQiecModule)
        else lower_qiec_ir(module_or_ir)
    )
    supported = capabilities or capabilities_for_target(target)
    diagnostics: list[QiecCapabilityDiagnostic] = list(
        host_runtime_capability_diagnostics(
            module,
            target,
            capabilities=supported,
        )
    )
    if not supported.supports("declarations") and (
        module.index_sorts or module.families or module.effects or module.handlers
    ):
        diagnostics.append(
            QiecCapabilityDiagnostic(
                target=target,
                feature="declarations",
                detail="cannot preserve its typed declarations",
            )
        )
    grade_features = {
        "0": "zero-resumption",
        "aff": "affine-resumption",
        "1": "linear-resumption",
        "omega": "unrestricted-resumption",
    }
    recursive = _recursive_computations(module)
    # A program's computation and its marginal helpers are rendered from
    # the target plan the renderer builds for the program, and a program
    # another program draws from is planned in place, so the host
    # runtime is never asked to carry them.
    programs = module.program_computations()
    for computation in module.computations:
        if _is_deduction_origin(computation.origin) or _is_structural_origin(
            computation.origin
        ):
            # These computations have one canonical entry-level diagnostic,
            # selected by ``host_runtime_capability_diagnostics``. Walking
            # every generated helper would make the editor and transpiler
            # disagree about which source construct is unsupported.
            continue
        if computation.id.text in programs:
            continue
        required = _required_features(computation)
        if computation.id.text in recursive:
            required.add("recursion")
        handler_ids = _handled_ids(computation.body)
        for handler in module.handlers:
            if handler.id.text not in handler_ids:
                continue
            required.update(
                cast(QiecFeature, grade_features[clause.grade])
                for clause in handler.clauses
            )
            if handler.implementation == "authored":
                required.add("authored-handler")
                for clause in handler.clauses:
                    if clause.body is not None:
                        required.update(_body_features(clause.body))
                if handler.return_clause is not None:
                    required.update(_body_features(handler.return_clause.body))
        for feature in sorted(required):
            if supported.supports(feature):
                continue
            diagnostics.append(
                QiecCapabilityDiagnostic(
                    target=target,
                    feature=feature,
                    computation=computation.name,
                    origin=computation.origin,
                    detail="has no semantics-preserving lowering for that feature",
                )
            )
    return tuple(diagnostics)

host_runtime_capability_diagnostics

host_runtime_capability_diagnostics(module_or_ir: QiecModule | IRQiecModule, target: str, *, capabilities: QiecTargetCapabilities | None = None) -> tuple[QiecCapabilityDiagnostic, ...]

Report unavailable search and neural runtime boundaries.

This is the shared entry-root policy used by transpilation, the CLI, the REPL, the TUI, and the language server. Keeping it beside the general capability analyzer prevents those surfaces from diagnosing different generated helpers for the same source declaration.

PARAMETER	DESCRIPTION
module_or_ir	The checked module or its IR projection. TYPE: QiecModule | IRQiecModule
target	The target name. TYPE: str
capabilities	The feature set to check against, else the target's registered one. TYPE: QiecTargetCapabilities | None DEFAULT: None

RETURNS	DESCRIPTION
tuple[QiecCapabilityDiagnostic, ...]	One diagnostic per search or neural host-runtime boundary an entry root reaches that the target cannot provide.

Source code in src/quivers/transpile/qiec_ir.py

def host_runtime_capability_diagnostics(
    module_or_ir: QiecModule | IRQiecModule,
    target: str,
    *,
    capabilities: QiecTargetCapabilities | None = None,
) -> tuple[QiecCapabilityDiagnostic, ...]:
    """Report unavailable search and neural runtime boundaries.

    This is the shared entry-root policy used by transpilation, the CLI, the
    REPL, the TUI, and the language server. Keeping it beside the general
    capability analyzer prevents those surfaces from diagnosing different
    generated helpers for the same source declaration.

    Parameters
    ----------
    module_or_ir
        The checked module or its IR projection.
    target
        The target name.
    capabilities
        The feature set to check against, else the target's registered
        one.

    Returns
    -------
    tuple[QiecCapabilityDiagnostic, ...]
        One diagnostic per search or neural host-runtime boundary an entry
        root reaches that the target cannot provide.
    """

    supported = capabilities or capabilities_for_target(target)
    if isinstance(module_or_ir, QiecModule):
        candidates = tuple(
            computation
            for computation in module_or_ir.computations
            if _is_deduction_origin(computation.origin)
            or _is_structural_origin(computation.origin)
        )
        if not candidates:
            return ()
        roots = _core_host_runtime_root_ids(module_or_ir)
        diagnostics: list[QiecCapabilityDiagnostic] = []
        for computation in candidates:
            if computation.id not in roots:
                continue
            feature: QiecFeature | None = None
            detail = "has no semantics-preserving lowering for that feature"
            if _is_deduction_origin(computation.origin) and computation.name.endswith(
                "__run"
            ):
                feature = "search"
                detail = "has no search runtime to enumerate its derivations"
            elif _is_structural_origin(computation.origin):
                feature = "neural-attachment"
            if feature is None or supported.supports(feature):
                continue
            diagnostics.append(
                QiecCapabilityDiagnostic(
                    target=target,
                    feature=feature,
                    computation=computation.name,
                    origin=cast(IRQiecSourceOrigin, _convert(computation.origin)),
                    detail=detail,
                )
            )
        return tuple(diagnostics)

    module = module_or_ir
    candidates = tuple(
        computation
        for computation in module.computations
        if _is_deduction_origin(computation.origin)
        or _is_structural_origin(computation.origin)
    )
    # Nearly every transpiled module has only ordinary QIEC computations.
    # Avoid decoding its (potentially large) Didactic term graph merely to
    # discover that no host-runtime boundary exists. This guard keeps the
    # shared CLI/LSP/transpiler check constant-time on that common path.
    if not candidates:
        return ()
    roots = _host_runtime_root_ids(module)
    diagnostics: list[QiecCapabilityDiagnostic] = []
    for computation in candidates:
        if computation.id.text not in roots:
            continue
        feature: QiecFeature | None = None
        detail = "has no semantics-preserving lowering for that feature"
        if _is_deduction_origin(computation.origin) and computation.name.endswith(
            "__run"
        ):
            feature = "search"
            detail = "has no search runtime to enumerate its derivations"
        elif _is_structural_origin(computation.origin):
            feature = "neural-attachment"
        if feature is None or supported.supports(feature):
            continue
        diagnostics.append(
            QiecCapabilityDiagnostic(
                target=target,
                feature=feature,
                computation=computation.name,
                origin=computation.origin,
                detail=detail,
            )
        )
    return tuple(diagnostics)