cottax.core.maths.plan.primitive module

The primitive graph operations, each proved through rebound: Rebind on the bindings (its finals Insert, Delete, Redefine, Combine), Nest and Unnest on the nesting.

unbreakable(before, after, delta)

A rule the op cannot break, by argument: nothing is asked.

Return type:

Iterator[Violation]

in_full(before, after, delta)

No proof: the rule is asked of the result. Never called – rebound knows it.

Return type:

Iterator[Violation]

class Edited[N: Label, V: Place](delta: Any, definitions: OrderedMap[N, NodeDefinition[V]] | None, within: OrderedMap[N, N] | None)

Bases: Frozen, Generic[N, V]

What a primitive changes: the delta its checks read, and the new definitions or nesting, None for one left as it is.

delta: Any

definitions: OrderedMap[N, NodeDefinition[V]] | None

within: OrderedMap[N, N] | None

class Primitive[N: Label, V: Place]

Bases: GraphOp[N, V], Generic[N, V]

An op that builds a graph. Two additional delta-checks:

• Stage 3, checks_delta: what it needs of its delta, (graph, delta) -> Iterator[Violation], asked before building.

• Stage 4, covers: every rule of NestingGraph and how it is covered.

checks_delta: PerLevel[tuple[Callable, ...]] = ()

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

covers: AbstractClassVar[Mapping[Callable, Callable]]

a level below cannot rebind it (Frozen).

Type:

Bound once, by the primitive

abstractmethod edited(graph: NestingGraph[N, V])

What this op changes of graph, which may assume every checks_graph case holds.

Return type:

Edited[N, V]

fully_checked()

Every proved rule asked in full as well: a proof passing what its rule refuses is a bug in the op, not in the graph. The test suite runs under it.

rebound[G: NestingGraph](op: Primitive, graph: G, delta, *, definitions=None, within=None)

op’s delta checks asked of graph and delta; then graph with definitions or within changed, and every rule of the result asked as op.covers says: through its proof, not at all where unbreakable, in full where in_full. A rule a final adds, which no op can name, is asked in full.

Return type:

G

class Rebinding[N: Label, V: Place](remove: frozenset[N], define: OrderedMap[N, NodeDefinition[V]])

Bases: Frozen, Generic[N, V]

What a Rebind changes of the bindings: names removed, and names defined – in place where bound, appended where new. The two are disjoint.

remove: frozenset[N]

define: OrderedMap[N, NodeDefinition[V]]

check_rebound_owns_disjoint[N: Label, V: Place](before: AbstractGraph[N, V], after: AbstractGraph[N, V], r: Rebinding[N, V])

check_one_producer_per_place of a rebinding. A removal frees places, and a node redefined owning what it owned moves none: nothing to ask. New nodes: their owns among themselves, then against the standing owners. Once something is removed while something is defined, or an own moved in place, the rule of the result.

Return type:

Iterator[Violation]

check_rebound_reads_exact[N: Label, V: Place](before: AbstractGraph[N, V], after: AbstractGraph[N, V], r: Rebinding[N, V])

check_reads_are_exact of a rebinding. A removal only turns reads into boundary inputs: nothing to ask. Otherwise the defined nodes’ reads against every owner after, and the new owns against the reads that already stand. Once something is removed while something is defined, or an own moved in place, the rule of the result.

Return type:

Iterator[Violation]

class Rebind[N: Label, V: Place]

Bases: Primitive[N, V], Generic[N, V]

The binding primitive: names removed and names defined, in one step, so only the result need be valid. A derived op says what (rebinding) and its intent (checks_delta, of the Rebinding); the proof is this level’s, and not overridden.

covers: AbstractClassVar[Mapping[Callable, Callable]] = {<function check_nesting_ends_are_problems>: <function in_full>, <function check_nesting_ends_bound>: <function in_full>, <function check_nesting_ends_on_one_cycle>: <function in_full>, <function check_no_nesting_loops>: <function in_full>, <function check_one_producer_per_place>: <function check_rebound_owns_disjoint>, <function check_reads_are_exact>: <function check_rebound_reads_exact>}

a level below cannot rebind it (Frozen).

Type:

Bound once, by the primitive

abstractmethod rebinding(graph: NestingGraph[N, V])

What this op removes and defines of graph.

Return type:

Rebinding[N, V]

edited(graph: NestingGraph[N, V])

The bindings kept in their order, the defined ones in place; the new ones appended; a nesting pair through a removed node dropped (a derived op that may not strand one refuses first).

Return type:

Edited[N, V]

check_names_free[N: Label](g: NestingGraph[N, Place], r: Rebinding)

What it defines, it binds anew: nothing holds the names.

Return type:

Iterator[Violation]

check_names_bound[N: Label](g: NestingGraph[N, Place], r: Rebinding)

What it removes or redefines is bound.

Return type:

Iterator[Violation]

check_delete_keeps_nesting_whole[N: Label](g: NestingGraph[N, Place], r: Rebinding)

A node removed goes with its edges; a nesting is not an edge but a decision the plan recorded, so a pair losing exactly one end is Stranded – Unnest first. Both ends going is fine.

Return type:

Iterator[Violation]

check_inserts(op: Insert)

Something is inserted.

Return type:

Iterator[Violation]

class Insert[N: Label, V: Place](nodes: OrderedMap[N, NodeDefinition[V]])

Bases: Rebind[N, V], Generic[N, V]

Add nodes to the graph.

nodes: OrderedMap[N, NodeDefinition[V]]

checks: PerLevel[tuple[Callable[[Any], object], ...]] = (<function check_inserts>,)

Callable [self] -> iterable of violations, which are raised at construction unless skipped (see unchecked).

checks_delta: PerLevel[tuple[Callable, ...]] = (<function check_names_free>,)

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

rebinding(graph: NestingGraph[N, V])

What this op removes and defines of graph.

Return type:

Rebinding[N, V]

check_deletes(op: Delete)

Return type:

Iterator[Violation]

class Delete[N: Label](nodes: tuple[N, ...])

Bases: Rebind[N, Place], Generic[N]

Remove named nodes. What a survivor read from a removed node becomes an unowned input, which is a well-formed graph. A nesting is a recorded decision, so an end going alone is refused (Stranded).

nodes: tuple[N, ...]

checks: PerLevel[tuple[Callable[[Any], object], ...]] = (<function check_deletes>,)

Callable [self] -> iterable of violations, which are raised at construction unless skipped (see unchecked).

checks_delta: PerLevel[tuple[Callable, ...]] = (<function check_names_bound>, <function check_delete_keeps_nesting_whole>)

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

rebinding(graph: NestingGraph[N, Place])

What this op removes and defines of graph.

Return type:

Rebinding[N, Place]

class Redefine[N: Label, V: Place]

Bases: Rebind[N, V], Generic[N, V]

Replace definitions in place.

checks_delta: PerLevel[tuple[Callable, ...]] = (<function check_names_bound>,)

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

abstractmethod redefined(graph: NestingGraph[N, V])

The new definition for each node this touches. Names not here are untouched.

Return type:

Mapping[N, NodeDefinition[V]]

rebinding(graph: NestingGraph[N, V])

What this op removes and defines of graph.

Return type:

Rebinding[N, V]

check_nodes(op: Combine)

At least two nodes, none twice, and a kind that can be folded at all.

Return type:

Iterator[Violation]

check_folds_one_kind(op: Combine, graph: NestingGraph)

Every node folded is of the declared kind: a fold is well-defined over one only, and this is what lets definition take the + for granted.

Return type:

Iterator[Violation]

check_lands_on_its_own(op: Combine, graph: NestingGraph)

The fold lands on a node it folds, or on a name nothing holds.

Return type:

Iterator[Violation]

class Combine[N: Label, V: Place, D: NodeDefinition](at: N, nodes: tuple[N, ...], kind: type[D])

Bases: Rebind[N, V], Generic[N, V, D]

Several nodes folded into one, by the + they define: the folded nodes removed and the fold defined at at, in one rebinding, so only the result need be valid. Whether the result keeps one producer per place and exact reads is the +’s business, which a fold cannot see: Rebind’s proof asks those rules of the result.

at: N

if in nodes, that node is redefined instead.

Type:

Resulting location

nodes: tuple[N, ...]

What is combined

kind: type[D]

The class whose + folds the nodes; each node must be one.

checks: PerLevel[tuple[Callable[[Any], object], ...]] = (<function check_nodes>,)

Callable [self] -> iterable of violations, which are raised at construction unless skipped (see unchecked).

checks_graph: PerLevel[tuple[Callable, ...]] = (<function check_folds_one_kind>, <function check_lands_on_its_own>)

(op, graph) -> Iterator[Violation], collected by refusals and raised by apply.

Type:

What the op needs of the graph before it can compute anything

checks_delta: PerLevel[tuple[Callable, ...]] = (<function check_delete_keeps_nesting_whole>,)

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

definition(graph: NestingGraph[N, V])

New node definition: the + of the nodes it folds. Every one is of the declared kind by check_folds_one_kind, so the + is the one that kind defines.

Return type:

D

rebinding(graph: NestingGraph[N, V])

The fold read off this graph, where every node still is; the binding of at kept in place if it is folded, else appended.

Return type:

Rebinding[N, V]

check_nesting[N: Label](g: NestingGraph[N, Place], pair: tuple[N, N])

What one new pair needs of the nesting alone: both ends bound; the inner not already answered inside something; both problems; a forest still (not a problem inside itself, no loop through what already encloses the outer). That the pair – and every pair now under inner – shares a cycle at its level is check_nesting_ends_on_one_cycle of the result, which rebound asks next.

Return type:

Iterator[Violation]

check_unnesting[N: Label](g: NestingGraph[N, Place], inner: N)

Unnest check that it was a nested one.

Return type:

Iterator[Violation]

class Nest[N: Label](inner: N, outer: N)

Bases: Primitive[N, Place], Generic[N]

Record that one problem is answered inside another’s iteration.

inner: N

outer: N

checks_delta: PerLevel[tuple[Callable, ...]] = (<function check_nesting>,)

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

covers: AbstractClassVar[Mapping[Callable, Callable]] = {<function check_nesting_ends_are_problems>: <function in_full>, <function check_nesting_ends_bound>: <function in_full>, <function check_nesting_ends_on_one_cycle>: <function in_full>, <function check_no_nesting_loops>: <function in_full>, <function check_one_producer_per_place>: <function unbreakable>, <function check_reads_are_exact>: <function unbreakable>}

a level below cannot rebind it (Frozen).

Type:

Bound once, by the primitive

edited(graph: NestingGraph[N, Place])

What this op changes of graph, which may assume every checks_graph case holds.

Return type:

Edited[N, Place]

class Unnest[N: Label](inner: N)

Bases: Primitive[N, Place], Generic[N]

The inverse of Nest: the problem is answered at its own level again.

inner: N

checks_delta: PerLevel[tuple[Callable, ...]] = (<function check_unnesting>,)

a level adds to its ancestors’ and never replaces them.

Type:

Each level’s own, accumulated root first as checks are

covers: AbstractClassVar[Mapping[Callable, Callable]] = {<function check_nesting_ends_are_problems>: <function in_full>, <function check_nesting_ends_bound>: <function in_full>, <function check_nesting_ends_on_one_cycle>: <function in_full>, <function check_no_nesting_loops>: <function in_full>, <function check_one_producer_per_place>: <function unbreakable>, <function check_reads_are_exact>: <function unbreakable>}

a level below cannot rebind it (Frozen).

Type:

Bound once, by the primitive

edited(graph: NestingGraph[N, Place])

What this op changes of graph, which may assume every checks_graph case holds.

Return type:

Edited[N, Place]

class NothingInserted

Bases: Violation

template: AbstractClassVar[str] = 'insert(): nothing to insert'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NothingDeleted

Bases: Violation

template: AbstractClassVar[str] = 'delete(): nothing to delete'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NothingToCombine

Bases: Violation

template: AbstractClassVar[str] = 'combine(): fewer than two nodes, so nothing to combine'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NodeTwice(nodes: tuple[Label, ...])

Bases: Violation

nodes: tuple[Label, ...]

template: AbstractClassVar[str] = 'combine(): {nodes!r} names a node twice'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NotAddable(kind: str)

Bases: Violation

kind: str

template: AbstractClassVar[str] = 'combine(): a {kind} defines no `+`, so no two of them can be folded'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NotOfKind(nodes: tuple[Label, ...], kind: str, found: str)

Bases: Violation

nodes: tuple[Label, ...]

kind: str

found: str

template: AbstractClassVar[str] = 'combine({kind}): {nodes!r} is {found}, and a fold is well-defined over one kind only'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NameTaken(name: Label)

Bases: Violation

name: Label

template: AbstractClassVar[str] = 'node name {name!r} is already bound -- an insert adds a binding, it does not replace one'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NotBound(name: Label)

Bases: Violation

name: Label

template: AbstractClassVar[str] = 'not a node of this graph: {name!r} -- an edit names what is bound'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class Stranded(inner: tuple[Label, ...], outer: tuple[Label, ...])

Bases: Violation

inner: tuple[Label, ...]

outer: tuple[Label, ...]

template: AbstractClassVar[str] = '{inner} in {outer} would lose one end and keep the other -- `Unnest` it first, so a plan never quietly voids what an earlier op recorded'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class NotNested(inner: Label)

Bases: Violation

inner: Label

template: AbstractClassVar[str] = '{inner!r} is not nested inside anything, so there is nothing to undo'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording

class AlreadyNested(inner: Label, outer: Label)

Bases: Violation

inner: Label

outer: Label

template: AbstractClassVar[str] = '{inner!r} is already answered inside {outer!r} -- a problem has one enclosing iteration, so `Unnest` it before nesting it somewhere else'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording