1	import Base
2	import ../shape/core.bend as Shape
3	import ./core.bend as Core
4	import ./allocation_spec.bend as Allocation
5	import ./transform_totality.bend as TransformTotality
6	
7	def 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	
15	type 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	
21	type 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	
28	def 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	
36	type 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)}