def node_facts

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

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

117def node_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
118  +p: P, -start: (A & B), +inner: Nat, +count: Nat, +base: Nat, rec: A -> B -> Array<F32> & (A & B), low: Array<F32> & (A & B),
119  -facts: Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, inner, count, base, low)>,
120  -next: @l: A -> @r: B -> @-at: {(l, r) == start : (A & B)} ->
121    Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), rec(l, r))>) ->
122  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, Build.node(~A, ~B, rec, low))>:
123  (a, s) = low
124  (l, r) = s
125  join_facts(~P, ~A, ~B, ~cell, p, start, inner, count, base, a, rec(l, r),
126    facts_cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, (a, (l, r)), facts),
127    next(l)(r)({\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, (A & B), (a, (l, r))) == start : (A & B)})> -> {Pair.snd(Array<F32>, (A & B), (a, (l, r))) == start : (A & B)}}(
128      facts_kept(~P, ~A, ~B, ~cell, p, start, inner, count, base, (a, (l, r)), facts))))