def join_facts

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

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

103def join_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
104  +p: P, -start: (A & B), +inner: Nat, +count: Nat, +base: Nat, -a: Array<F32>, high: Array<F32> & (A & B),
105  -low: Fact<Cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a)>,
106  -facts: Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), high)>) ->
107  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, Build.join(~(A & B), a, high))>:
108  (b, rest) = high
109  Fact{(
110    {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, (A & B), (b, rest)) == start : (A & B)})> -> {Pair.snd(Array<F32>, (A & B), (b, rest)) == start : (A & B)}}(
111      facts_kept(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), (b, rest), facts)),
112    {\{Fact: q => q} : Fact<(Cells(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, ANode{a, b}))> ->
113      Cells(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, ANode{a, b})}(
114      node_cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a, b, low,
115        facts_cells(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), (b, rest), facts))))}