1	import Base
2	import ../shape/core.bend as Shape
3	import ./core.bend as Core
4	import ./transform_observation.bend as Observation
5	
6	type RetainedFailure<-input: Shape.Shape, -fill: F32, -request: Observation.Request, -code: U32> is Type:
7	  RetainedFailure{
8	    outcome: {Observation.failure_code(input, request, Core.new(input, fill)) == Some{code} : Maybe<&2, U32>},
9	    retained_dimensions: {Observation.kept_dimensions(input, request, Core.new(input, fill)) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
10	    retained_count: {Observation.kept_length(input, request, Core.new(input, fill)) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
11	    retained_word_count: {Observation.kept_count(input, request, Core.new(input, fill)) == Some{Shape.count(input)} : Maybe<&2, U32>},
12	    retained_value: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool} ->
13	      {Observation.kept_value(input, request, other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}
14	
15	type ReshapeContract<-input: Shape.Shape, -fill: F32, -target: Shape.Shape> is Type:
16	  ReshapeContract{
17	    outcome: {Observation.reshape_code(input, Shape.dimensions(target), Core.new(input, fill)) == Some{0} : Maybe<&2, U32>},
18	    dimensions: {Observation.reshape_dimensions(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
19	    count: {Observation.reshape_length(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.logical_numel(Shape.dimensions(target))} : Maybe<&2, Nat>},
20	    word_count: {Observation.reshape_count(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.count(target)} : Maybe<&2, U32>},
21	    value: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
22	      {Observation.reshape_value(input, Shape.dimensions(target), other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}
23	
24	type ReshapeWrite<-input: Shape.Shape, -fill: F32, -target: Shape.Shape, -index: U32, -value: F32> is Type:
25	  ReshapeWrite{
26	    written: {Observation.reshape_written(input, index, value, Shape.dimensions(target), index, Core.new(input, fill)) == Some{value} : Maybe<&2, F32>},
27	    frame: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
28	      @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
29	      {Observation.reshape_written(input, index, value, Shape.dimensions(target), other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}