def words_step

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:941

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

941def words_step(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +position: Nat,
942  below: {Nat.is_lt(position, 1n+previous) == True{} : Bool}, decision: Shape.BoolCase<Nat.is_eq(position, previous)>,
943  earlier: @inside: {Nat.is_lt(position, previous) == True{} : Bool} ->
944    {ReduceLaws.word_at(Laws.words(shape, fill, ops, previous), position) ==
945      Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}) ->
946  {ReduceLaws.word_at(Laws.words(shape, fill, ops, 1n+previous), position) ==
947    Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}:
948  match decision:
949    case Shape.BFalse{equal}:
950      +before = Laws.words(shape, fill, ops, previous)
951      +last = Replayed.value(shape, fill, ops, U32.from_nat(previous))
952      +inside = PointwiseProof.lt_succ_ne(position, previous, below, equal)
953      Equal.trans(Maybe<&2, F32>, ReduceLaws.word_at(List.append(&2, F32, before, [last]), position), ReduceLaws.word_at(before, position),
954        Some{Replayed.value(shape, fill, ops, U32.from_nat(position))},
955        word_at_front(before, last, position,
956          %Equal.sym(Nat, List.length(&2, F32, before), previous, words_length(shape, fill, ops, previous)) :
957            {Nat.is_lt(position, _) == True{} : Bool}
958          inside),
959        earlier(inside))
960    case Shape.BTrue{equal}:
961      +before = Laws.words(shape, fill, ops, previous)
962      +last = Replayed.value(shape, fill, ops, U32.from_nat(previous))
963      %Equal.sym(Nat, position, previous, Arith.eq_true(position, previous, Equal.sym(Bool, True{}, Nat.is_eq(position, previous), equal))) :
964        {ReduceLaws.word_at(List.append(&2, F32, before, [last]), _) == Some{Replayed.value(shape, fill, ops, U32.from_nat(_))} : Maybe<&2, F32>}
965      %words_length(shape, fill, ops, previous) :
966        {ReduceLaws.word_at(List.append(&2, F32, before, [last]), _) == Some{last} : Maybe<&2, F32>}
967      word_at_last(before, last)