def fork_eq

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:781

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as BinaryBuild
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

781def fork_eq(+input: Shape.Shape, +axes: List<&2, U32>, +fill: F32, +ops: List<&2, StorageLaws.Op>, +plan: Layout.Plan<input, axes>, +ds: Nat, +fits: {Storage.bounds(ds, U32.to_nat(Shape.count(input))) == True{} : Bool}, +count: Nat, +exact: {count == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, +inner: Nat, +rest: Nat, +base: Nat,
782  low: {Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, base, (Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), Array.new(F32, 0n, 0.0))) == spec(input, axes, fill, ops, count, inner, base) : Array<F32>},
783  high: {Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, Nat.add(Model.capacity(inner), base), (Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), Array.new(F32, 0n, 0.0))) == spec(input, axes, fill, ops, count, inner, Nat.add(Model.capacity(inner), base)) : Array<F32>},
784  lp: Array<F32> & Array<F32>, +le: {lp == Array.clone(F32, Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill)) : Array<F32> & Array<F32>}) ->
785  {Parallel.fork(~Array<F32>, ~Array<F32>, Build.halves(lp, Array.clone(F32, Array.new(F32, 0n, 0.0))), l => r => Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, base, (l, r)), l => r => Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, Nat.add(Model.capacity(inner), base), (l, r))) ==
786    spec(input, axes, fill, ops, count, 1n+inner, base) : Array<F32>}:
787  (l1, l2) = lp
788  %Equal.sym(Array<F32>, l1, Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), BinaryBuild.clone_first_eq(ds, (Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), fill, (l1, l2), le)) :
789    {ANode{Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, base, (_, Array.new(F32, 0n, 0.0))), Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, Nat.add(Model.capacity(inner), base), (l2, Array.new(F32, 0n, 0.0)))} == spec(input, axes, fill, ops, count, 1n+inner, base) : Array<F32>}
790  %Equal.sym(Array<F32>, l2, Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), BinaryBuild.clone_second_eq(ds, (Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), fill, (l1, l2), le)) :
791    {ANode{Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, base, (Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), Array.new(F32, 0n, 0.0))), Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, Nat.add(Model.capacity(inner), base), (_, Array.new(F32, 0n, 0.0)))} == spec(input, axes, fill, ops, count, 1n+inner, base) : Array<F32>}
792  %Equal.sym(Array<F32>, Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, base, (Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), Array.new(F32, 0n, 0.0))), spec(input, axes, fill, ops, count, inner, base), low) :
793    {ANode{_, Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, Nat.add(Model.capacity(inner), base), (Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), Array.new(F32, 0n, 0.0)))} == spec(input, axes, fill, ops, count, 1n+inner, base) : Array<F32>}
794  %Equal.sym(Array<F32>, Parallel.build(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell, Build.Request{input, axes}, inner, rest, count, Nat.add(Model.capacity(inner), base), (Api.arr((Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{})), ds, fill), Array.new(F32, 0n, 0.0))), spec(input, axes, fill, ops, count, inner, Nat.add(Model.capacity(inner), base)), high) :
795    {ANode{spec(input, axes, fill, ops, count, inner, base), _} == spec(input, axes, fill, ops, count, 1n+inner, base) : Array<F32>}
796  {==}