def node_cells

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

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

93def node_cells(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
94  +p: P, -start: (A & B), +inner: Nat, +count: Nat, +base: Nat, -a: Array<F32>, -b: Array<F32>,
95  -low: Fact<Cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a)>,
96  -high: Fact<Cells(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), b)>) ->
97  Fact<Cells(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, ANode{a, b})>:
98  Fact{path => {\{Fact: q => q} :
99    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)))> ->
100    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))}(
101      node_cell(~P, ~A, ~B, ~cell, p, start, inner, count, base, a, b, path, low, high))}