cottax.core.maths.plan.algebra module

An edit as a record, and the fold of a sequence of them: GraphOp (graph -> graph), ComposedOp (an op that is other ops), Plan (a base graph plus the ops applied to it). Over any NestingGraph; the primitives with their proofs are primitive.py.

refusals[N: Label, V: Place](op: GraphOp[N, V], graph: NestingGraph[N, V])

Why op does not apply to graph, as data – every checks_graph case.

Most derived level first: an op’s own precondition is asked before the one it inherits, since an inherited check reads what the derived op computes (Rewire’s reads Cut’s renaming).

Return type:

Iterator[Violation]

proved_once[G: NestingGraph](build: Callable[[], G])

build(), the rules its steps would ask in full asked once of the graph it returns, if this is the outermost composition; inside one, the outermost asks them. A step’s own preconditions and proofs are asked as ever.

Return type:

G

class GraphOp[N: Label, V: Place]

Bases: Frozen, Generic[N, V]

Graph operation: changing the computational graph.

Four stages:

1. op alone: is this a valid op? [checks of frozen]

2. op and graph: can this op apply to this graph? [checks_graph]

3. op, graph, and delta: does this delta make sense to apply [ checks_delta]

4. new graph: does this graph need less proving [covers]

3 and 4 are a Primitive’s (primitive.py), the ops that build a graph. Any other op composes them and has only 1 and 2: it proves nothing of its own.

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

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

Type:

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

apply[G: NestingGraph](graph: G)

The rewrite: refuses, or returns the graph with this op applied.

Return type:

G

class ComposedOp[N: Label, V: Place]

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

An op that is other ops, in order, all decided off the graph it meets. It proves nothing of its own: every graph it passes on was built by the op that built it, with its proofs; what a step would ask in full is asked once, of the result (proved_once).

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

The ops this one is. Takes a graph, so an expansion may depend on what it meets.

Return type:

Sequence[GraphOp[N, V]]

class Stage[N: Label, V: Place](ops: tuple[GraphOp[N, V], ...], graph: NestingGraph[N, V])

Bases: Frozen, Generic[N, V]

One stage of a StagedOp: the ops decided, and the graph they leave.

ops: tuple[GraphOp[N, V], ...]

graph: NestingGraph[N, V]

class StagedOp[N: Label, V: Place]

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

A composition decided stage by stage: each stage’s ops are read off the graph the one before left. No proofs

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

Yield a stage’s ops; receive the graph they leave.

Return type:

Generator[Sequence[GraphOp[N, V]], NestingGraph[N, V], None]

staged(graph: NestingGraph[N, V])

Every stage, each op applied to the graph that op meets: the derivation, kept.

Return type:

tuple[Stage[N, V], ...]

class Plan[N: Label, V: Place](base: NestingGraph[N, V], ops: tuple[GraphOp[N, V], ...] = ())

Bases: Frozen, Generic[N, V]

A base graph plus the operations applied to it. A Frozen with no rules of its own: what it buys is the cached hash and a pickle that carries base and ops and no prefix graph, which graph rebuilds on demand.

base: NestingGraph[N, V]

ops: tuple[GraphOp[N, V], ...] = ()

property trunk: Optional[Plan[N, V]]

This plan minus its last op; None for the base. Cached, so every prefix of a plan is one object and is built once.

property graph: NestingGraph[N, V]

base with every op applied.