src/tensor/read_write_contract_LAWS.bend
bendtorch-core@0.1.0.0 · 52 lines · 6 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/observation.bend as Observation
5import bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend as Records
6
7law read_inside:
8 for +shape: Shape.Shape
9 for +fill: F32
10 for +index: U32
11 for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
12 Records.ReadInside<shape, fill, index>
13
14law read_outside:
15 for +shape: Shape.Shape
16 for +fill: F32
17 for +index: U32
18 for outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}
19 Records.ReadContract<shape, fill, index, 8>
20
21law write_inside:
22 for +shape: Shape.Shape
23 for +fill: F32
24 for +index: U32
25 for +value: F32
26 for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
27 Records.WriteInside<shape, fill, index, value>
28
29law write_outside:
30 for +shape: Shape.Shape
31 for +fill: F32
32 for +index: U32
33 for +value: F32
34 for outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}
35 Records.WriteOutside<shape, fill, index, value>
36
37law coordinate_inside:
38 for +shape: Shape.Shape
39 for +fill: F32
40 for +coordinates: List<&2, U32>
41 for +index: U32
42 for +value: F32
43 for located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>}
44 for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
45 Records.CoordinateInside<shape, fill, coordinates, index, value>
46
47law dynamic_read_inside:
48 for +shape: Shape.Shape
49 for +fill: F32
50 for +index: U32
51 for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
52 {Observation.dynamic_point(shape, index, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}