def present_observation

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1222

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/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/route.bend as Route

1222def present_observation(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
1223  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1224  PresentObservation<shape, tensor, index>:
1225  Core.TTensor{storage, exact} = tensor
1226  match storage:
1227    case Storage.Empty{}:
1228      present_impossible(shape, Core.TTensor{Storage.Empty{}, exact}, index,
1229        Arith.lt_zero(U32.to_nat(index),
1230          %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1231          inside))
1232    case Storage.Owned{+depth, +length, array, balanced, valid}:
1233      PresentObservation{Refinement.second(F32, Array.get(F32, array, index)),
1234        Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index),
1235          Model.observe(F32, depth, array, Refinement.route(depth, index)), Some{Refinement.second(F32, Array.get(F32, array, index))},
1236          observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length),
1237            %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1238            inside,
1239            Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
1240              Route.index_complete(depth, length, index, valid,
1241                %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1242                inside))),
1243          Equal.sym(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, array, index))},
1244            Model.observe(F32, depth, array, Refinement.route(depth, index)), Refinement.law_get_refines(F32, depth, array, index, balanced)))}