def words_step

bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:97

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 Contracts
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

97def words_step(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +position: Nat,
98  below: {Nat.is_lt(position, 1n+previous) == True{} : Bool}, decision: Shape.BoolCase<Nat.is_eq(position, previous)>,
99  earlier: @inside: {Nat.is_lt(position, previous) == True{} : Bool} ->
100    {ReduceLaws.word_at(Contracts.words(shape, fill, ops, previous), position) ==
101      Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}) ->
102  {ReduceLaws.word_at(Contracts.words(shape, fill, ops, 1n+previous), position) ==
103    Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}:
104  match decision:
105    case Shape.BFalse{equal}:
106      +before = Contracts.words(shape, fill, ops, previous)
107      +last = Replayed.value(shape, fill, ops, U32.from_nat(previous))
108      +inside = PointwiseProof.lt_succ_ne(position, previous, below, equal)
109      Equal.trans(Maybe<&2, F32>, ReduceLaws.word_at(List.append(&2, F32, before, [last]), position), ReduceLaws.word_at(before, position),
110        Some{Replayed.value(shape, fill, ops, U32.from_nat(position))},
111        word_at_front(before, last, position,
112          %Equal.sym(Nat, List.length(&2, F32, before), previous, words_length(shape, fill, ops, previous)) :
113            {Nat.is_lt(position, _) == True{} : Bool}
114          inside),
115        earlier(inside))
116    case Shape.BTrue{equal}:
117      +before = Contracts.words(shape, fill, ops, previous)
118      +last = Replayed.value(shape, fill, ops, U32.from_nat(previous))
119      %Equal.sym(Nat, position, previous, Arith.eq_true(position, previous, Equal.sym(Bool, True{}, Nat.is_eq(position, previous), equal))) :
120        {ReduceLaws.word_at(List.append(&2, F32, before, [last]), _) == Some{Replayed.value(shape, fill, ops, U32.from_nat(_))} : Maybe<&2, F32>}
121      %words_length(shape, fill, ops, previous) :
122        {ReduceLaws.word_at(List.append(&2, F32, before, [last]), _) == Some{last} : Maybe<&2, F32>}
123      word_at_last(before, last)