def pair_join_facts

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

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

130# The depth-1 tree: the leaf of cell `base` next to the leaf of the cell
131# after it, which reads the state the first hands back.
132def pair_join_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
133  +p: P, -start: (A & B), +count: Nat, +base: Nat, x: F32, high: F32 & (A & B),
134  -low: Fact<Cells(~P, ~A, ~B, ~cell, p, start, 0n, count, base, ALeaf{x})>,
135  -exact: {high == cell(p, Nat.add(1n, base), start, Nat.is_lt(Nat.add(1n, base), count)) : F32 & (A & B)},
136  -keeps: Keeps(~P, ~A, ~B, ~cell, p, start)) ->
137  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 1n, count, base, Build.pair_join(~(A & B), x, high))>:
138  (y, rest) = high
139  join_facts(~P, ~A, ~B, ~cell, p, start, 0n, count, base, ALeaf{x}, Build.leaf(~(A & B), (y, rest)), low,
140    leaf_facts(~P, ~A, ~B, ~cell, p, start, count, Build.upper(0n, base), (y, rest), exact, keeps))