src/tensor/construction_totality.bend

bendtorch-core@0.1.0.0 · 40 lines · 5 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
5import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
6
7def TensorReads(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) -> Type:
8  match result:
9    case Fail{error}:
10      Unit
11    case Done{tensor}:
12      @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool} ->
13        TransformTotality.ReadSuccess<shape, tensor, index>
14
15type TensorDone<-shape: Shape.Shape, -result: Result<&2, &1, Core.Error, Core.Tensor<shape>>> is Data:
16  TensorDone{
17    -witness: Allocation.TensorDone<shape, result>,
18    -successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool},
19    -readable: TensorReads(shape, result)}
20
21type ConstructionWitness<-dimensions: List<&2, U32>, -result: Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
22  ConstructionWitness{
23    -shape: Shape.Shape,
24    -tensor: Core.Tensor<shape>,
25    -same: {Done{Core.Packed{shape, tensor}} == result : Result<&2, &1, Core.Error, Core.Dynamic>},
26    -preserved: {Shape.dimensions(shape) == dimensions : List<&2, U32>}}
27
28def ConstructionReads(+dimensions: List<&2, U32>, result: Result<&2, &1, Core.Error, Core.Dynamic>) -> Type:
29  match result:
30    case Fail{error}:
31      Unit
32    case Done{Core.Packed{+shape, tensor}}:
33      @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(dimensions)) == True{} : Bool} ->
34        TransformTotality.ReadSuccess<shape, tensor, index>
35
36type ConstructionDone<-dimensions: List<&2, U32>, -result: Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
37  ConstructionDone{
38    -witness: ConstructionWitness<dimensions, result>,
39    -successful: {Result.is_done(&2, &1, Core.Error, Core.Dynamic, result) == True{} : Bool},
40    -readable: ConstructionReads(dimensions, result)}