def decision_interpretation

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws

117def decision_interpretation(+fuel: Nat, -shape: Shape.Shape, tensor: Core.Tensor<shape>, +cursor: Nat,
118  +accumulator: F32, +head: F32, +values: List<&2, F32>,
119  -rec: @tensor: Core.Tensor<shape> -> @logical: Laws.LogicalValues(fuel, shape, tensor, 1n+cursor, values) ->
120    {Laws.loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head))) ==
121      Some{Reduction.sequential_sum(values, F32.add(accumulator, head))} : Maybe<&2, F32>},
122  logical: Laws.LogicalStep<fuel, shape, tensor, cursor, head, values>,
123  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
124  Laws.Interpretation<Laws.loop_value(shape, Reduction.sum_decided(shape,
125    tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), tensor, cursor, U32.from_nat(cursor), accumulator, decision)),
126    Some{Reduction.sequential_sum(head <> values, accumulator)}>:
127  Laws.LogicalStep{exact, observed, remaining} = logical
128  match decision:
129    case Shape.BFalse{equal}:
130      Laws.Interpretation{unit => Empty.absurd({None{} == Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>},
131        conversion_clash(U32.to_nat(U32.from_nat(cursor)), cursor, exact, equal))}
132    case Shape.BTrue{equal}:
133      Laws.Interpretation{unit =>
134        prove : @certificates: Core.SourceRead<shape, tensor, U32.from_nat(cursor)> & Core.SourceReadKeeps<shape, tensor, U32.from_nat(cursor)> ->
135          {Laws.loop_value(shape, Reduction.read_step(shape,
136            tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, tensor, U32.from_nat(cursor)))) ==
137            Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>} =
138          \{Tuple: \{Core.SourceRead: meaning => \{Core.SourceReadKeeps: kept =>
139            read_certificate_interpretation(fuel, shape, tensor, cursor, accumulator, head, values, rec, observed, remaining,
140              Core.read_certificate(shape, tensor, U32.from_nat(cursor)), meaning, kept)}}}
141        prove((Core.source_read_model(shape, tensor, U32.from_nat(cursor)), Core.source_read_keeps(shape, tensor, U32.from_nat(cursor))))}