1	import Base
2	import ../shape/core.bend as Shape
3	import ./core.bend as Core
4	import ./elementwise.bend as Elementwise
5	
6	def dimensions(dynamic: Core.Dynamic) -> List<&2, U32>:
7	  Core.Packed{shape, tensor} = dynamic
8	  Shape.dimensions(shape)
9	
10	def dynamic_shape(dynamic: Core.Dynamic) -> Shape.Shape:
11	  Core.Packed{shape, tensor} = dynamic
12	  shape
13	
14	def retained_left(pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>) -> Core.Dynamic:
15	  ((left, right), result) = pair
16	  left
17	
18	def retained_right(pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>) -> Core.Dynamic:
19	  ((left, right), result) = pair
20	  right
21	
22	def succeeded(pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>) -> Bool:
23	  (inputs, result) = pair
24	  Result.is_done(&2, &1, Core.Error, Core.Dynamic, result)
25	
26	type Property is Data:
27	  Dimensions{}
28	  Checked{index: U32}
29	  Raw{index: U32}
30	
31	type Inspection is Data:
32	  Dims{dimensions: List<&2, U32>}
33	  Value{value: Maybe<&2, F32>}
34	
35	def inspect(property: Property, dynamic: Core.Dynamic) -> Inspection:
36	  match property:
37	    case Dimensions{}:
38	      Dims{dimensions(dynamic)}
39	    case Checked{index}:
40	      Value{Core.checked_observe_dynamic(dynamic, index)}
41	    case Raw{index}:
42	      Value{Core.observe_dynamic(dynamic, index)}
43	
44	def SameSource(-original: Core.Dynamic, -retained: Core.Dynamic) -> Type:
45	  @+property: Property -> {inspect(property, retained) == inspect(property, original) : Inspection}
46	
47	type Retention<-left: Core.Dynamic, -right: Core.Dynamic,
48	  -pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
49	  Retention{-left: SameSource(left, retained_left(pair)),
50	    -right: SameSource(right, retained_right(pair))}
51	
52	def OutputDimensions(+output: List<&2, U32>, pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>) -> Type:
53	  (inputs, result) = pair
54	  match result:
55	    case Fail{error}:
56	      Unit
57	    case Done{dynamic}:
58	      {dimensions(dynamic) == output : List<&2, U32>}
59	
60	type DimensionsModel<-output: List<&2, U32>,
61	  -pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
62	  DimensionsModel{-exact: OutputDimensions(output, pair)}
63	
64	type Success<-pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
65	  Success{-successful: {succeeded(pair) == True{} : Bool}}
66	
67	type Compatible<-left: Core.Dynamic, -right: Core.Dynamic, -output: List<&2, U32>> is Data:
68	  Compatible{alignment: Shape.Broadcast<Shape.extents(dynamic_shape(left)), Shape.extents(dynamic_shape(right)), Shape.naturals(output)>,
69	    rank: Shape.LE(Shape.rank_dimensions(output), 4n), capacity: Shape.LE(Shape.logical_numel(output), 1048576n)}