src/tensor/construction_LAWS.bend
bendtorch-core@0.1.0.0 · 91 lines · 16 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/construction_totality.bend as Totality
5
6def clone_first_checked(-shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>, index: U32) -> Maybe<&2, F32>:
7 (first, second) = pair
8 Core.checked_observe(shape, first, index)
9
10def clone_second_checked(-shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>, index: U32) -> Maybe<&2, F32>:
11 (first, second) = pair
12 Core.checked_observe(shape, second, index)
13
14def clone_first_model(-shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>, index: U32) -> Maybe<&2, F32>:
15 (first, second) = pair
16 Core.observe(shape, first, index)
17
18def clone_second_model(-shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>, index: U32) -> Maybe<&2, F32>:
19 (first, second) = pair
20 Core.observe(shape, second, index)
21
22type CloneMeaning<-shape: Shape.Shape, -original: Core.Tensor<shape>> is Data:
23 CloneMeaning{
24 -first_checked: @+index: U32 -> {clone_first_checked(shape, Core.clone(shape, original), index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>},
25 -second_checked: @+index: U32 -> {clone_second_checked(shape, Core.clone(shape, original), index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>},
26 -first_model: @+index: U32 -> {clone_first_model(shape, Core.clone(shape, original), index) == Core.observe(shape, original, index) : Maybe<&2, F32>},
27 -second_model: @+index: U32 -> {clone_second_model(shape, Core.clone(shape, original), index) == Core.observe(shape, original, index) : Maybe<&2, F32>}}
28
29law public_clone_elements:
30 for +shape: Shape.Shape
31 for original: Core.Tensor<shape>
32 CloneMeaning<shape, original>
33
34def list_element(values: List<&2, F32>, position: Nat) -> Maybe<&2, F32>:
35 match values position:
36 case Nil{} _:
37 None{}
38 case value <> rest 0n:
39 Some{value}
40 case value <> rest 1n+p:
41 list_element(rest, p)
42
43def Elements(-shape: Shape.Shape, +values: List<&2, F32>, -tensor: Core.Tensor<shape>) -> Type:
44 @+index: U32 -> @inside: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) ->
45 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
46 ({Core.checked_observe(shape, tensor, index) == list_element(values, U32.to_nat(index)) : Maybe<&2, F32>} &
47 {Core.observe(shape, tensor, index) == list_element(values, U32.to_nat(index)) : Maybe<&2, F32>})
48
49def FromValuesMeaning(+shape: Shape.Shape, +values: List<&2, F32>, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) -> Type:
50 match result:
51 case Fail{error}:
52 Unit
53 case Done{tensor}:
54 Elements(shape, values, tensor)
55
56type FromValuesModel<-shape: Shape.Shape, -values: List<&2, F32>> is Data:
57 FromValuesModel{-meaning: FromValuesMeaning(shape, values, Core.from_values(shape, values))}
58
59def ConstructionMeaning(+values: List<&2, F32>, result: Result<&2, &1, Core.Error, Core.Dynamic>) -> Type:
60 match result:
61 case Fail{error}:
62 Unit
63 case Done{Core.Packed{+shape, tensor}}:
64 Elements(shape, values, tensor)
65
66type ConstructionModel<-dimensions: List<&2, U32>, -values: List<&2, F32>> is Data:
67 ConstructionModel{-meaning: ConstructionMeaning(values, Core.construct(dimensions, values))}
68
69law public_from_values_elements:
70 for +shape: Shape.Shape
71 for +values: List<&2, F32>
72 FromValuesModel<shape, values>
73
74law public_construction_elements:
75 for +dimensions: List<&2, U32>
76 for +values: List<&2, F32>
77 ConstructionModel<dimensions, values>
78
79law public_from_values_complete:
80 for +shape: Shape.Shape
81 for +values: List<&2, F32>
82 for counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
83 Totality.TensorDone<shape, Core.from_values(shape, values)>
84
85law public_construction_complete:
86 for +dimensions: List<&2, U32>
87 for +values: List<&2, F32>
88 for rank_bound: Shape.LE(Shape.rank_dimensions(dimensions), 4n)
89 for capacity_bound: Shape.LE(Shape.logical_numel(dimensions), 1048576n)
90 for counted: {List.length(&2, F32, values) == Shape.logical_numel(dimensions) : Nat}
91 Totality.ConstructionDone<dimensions, Core.construct(dimensions, values)>