def node_cell

bendtorch-core@0.1.0.0 · src/tensor/parallel_proofs.bend:76

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Build

76def node_cell(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
77  +p: P, -start: (A & B), +inner: Nat, +count: Nat, +base: Nat, -a: Array<F32>, -b: Array<F32>, +path: Model.Path(1n+inner),
78  -low: Fact<Cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a)>,
79  -high: Fact<Cells(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), b)>) ->
80  Fact<CellIs(~P, ~A, ~B, ~cell, p, start, count, Nat.add(Model.offset(1n+inner, path), base), Model.observe(F32, 1n+inner, ANode{a, b}, path))>:
81  Model.Step{+bit, +rest} = path
82  match bit:
83    case False{}:
84      Fact{{\{Fact: q => q} : Fact<(Cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a))> ->
85        Cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a)}(low)(rest)}
86    case True{}:
87      Fact{
88        %position_step(Model.capacity(inner), Model.offset(inner, rest), base) :
89          CellIs(~P, ~A, ~B, ~cell, p, start, count, _, Model.observe(F32, inner, b, rest))
90        {\{Fact: q => q} : Fact<(Cells(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), b))> ->
91          Cells(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), b)}(high)(rest)}