src/tensor/construction_metadata.bend

bendtorch-core@0.1.0.0 · 62 lines · 7 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
4import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
5import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
6import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
7import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
8
9type NewMetadata<-shape: Shape.Shape, -fill: F32> is Data:
10  NewMetadata{
11    successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, Core.new(shape, fill)) == True{} : Bool},
12    dimensions: {Observation.dimensions(shape, Core.new(shape, fill)) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
13    count: {Allocation.tensor_length(shape, Core.new(shape, fill)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
14    word_count: {Observation.count(shape, Core.new(shape, fill)) == Some{Shape.count(shape)} : Maybe<&2, U32>}}
15
16def status_is_length(-shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
17  {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) ==
18    Maybe.is_some(&2, Nat, Allocation.tensor_length(shape, result)) : Bool}:
19  match result:
20    case Fail{error}:
21      {==}
22    case Done{tensor}:
23      {==}
24
25def generic_count_producer(+shape: Shape.Shape, +fill: F32) ->
26  {Allocation.tensor_length(shape, Core.new(shape, fill)) ==
27    Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
28  AllocationProof.core_new(shape, fill)
29
30def generic_status_consumer(+shape: Shape.Shape, +fill: F32) ->
31  {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, Core.new(shape, fill)) == True{} : Bool}:
32  Equal.trans(Bool, Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, Core.new(shape, fill)),
33    Maybe.is_some(&2, Nat, Allocation.tensor_length(shape, Core.new(shape, fill))), True{},
34    status_is_length(shape, Core.new(shape, fill)),
35    Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value),
36      Allocation.tensor_length(shape, Core.new(shape, fill)), Some{Shape.logical_numel(Shape.dimensions(shape))},
37      generic_count_producer(shape, fill)))
38
39def completed_dimensions(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
40  successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}) ->
41  {Observation.dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
42  match result:
43    case Fail{error}:
44      Empty.absurd({None{} == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, Arith.clash(successful))
45    case Done{tensor}:
46      {==}
47
48def completed_count(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
49  successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}) ->
50  {Observation.count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
51  match result:
52    case Fail{error}:
53      Empty.absurd({None{} == Some{Shape.count(shape)} : Maybe<&2, U32>}, Arith.clash(successful))
54    case Done{tensor}:
55      {==}
56
57def construction(+shape: Shape.Shape, +fill: F32) -> NewMetadata<shape, fill>:
58  +successful = generic_status_consumer(shape, fill)
59  NewMetadata{successful,
60    completed_dimensions(shape, Core.new(shape, fill), successful),
61    AllocationProof.core_new(shape, fill),
62    completed_count(shape, Core.new(shape, fill), successful)}