1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/arith.bend as Arith
4	import ./core.bend as Core
5	import ./allocation_spec.bend as Allocation
6	import ./allocation_PROOF.bend as AllocationProof
7	import ./observation.bend as Observation
8	
9	type 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	
16	def 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	
25	def 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	
30	def 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	
39	def 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	
48	def 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	
57	def 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)}