def checked_observation_model

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

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/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/route.bend as Route

1200def checked_observation_model(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
1201  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1202  CheckedObservationModel<shape, tensor, index>:
1203  Core.TTensor{storage, exact} = tensor
1204  match storage:
1205    case Storage.Empty{}:
1206      CheckedObservationModel{Arith.lt_zero(U32.to_nat(index),
1207        %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1208        inside)}
1209    case Storage.Owned{+depth, +length, array, balanced, valid}:
1210      CheckedObservationModel{Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
1211        Route.index_complete(depth, length, index, valid,
1212          %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1213          inside))}