1	import Base
2	import ../shape/core.bend as Shape
3	import ../tensor/core.bend as Core
4	import ../tensor/elementwise_totality.bend as Totality
5	import ./reduce.bend as Reduce
6	import ./reduce_LAWS.bend as ReduceLaws
7	import ./sum_to_size.bend as SumToSize
8	
9	def Identity(-input: Core.Dynamic, +target: Shape.Shape, pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>) -> Type:
10	  (retained, result) = pair
11	  match result:
12	    case Fail{error}:
13	      Empty
14	    case Done{output}:
15	      {Totality.dimensions(output) == Shape.dimensions(target) : List<&2, U32>} &
16	        (@+index: U32 ->
17	          {Core.checked_observe_dynamic(output, index) == Core.checked_observe_dynamic(input, index) : Maybe<&2, F32>} &
18	            {Core.observe_dynamic(output, index) == Core.observe_dynamic(input, index) : Maybe<&2, F32>})
19	
20	type IdentityModel<-input: Core.Dynamic, -target: Shape.Shape,
21	  -pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>> is Data:
22	  IdentityModel{-identity: Identity(input, target, pair)}
23	
24	# The contribution owner comes back with the same dimensions and observations.
25	law sum_to_size_retains_input:
26	  for input: Core.Dynamic
27	  for +target: Shape.Shape
28	  ReduceLaws.Retained<input, SumToSize.sum_to_size(input, target)>
29	
30	# A target with the contribution's dimensions always succeeds, and the output
31	# has the target's dimensions and the contribution's exact words at every
32	# position: -0.0 stays -0.0, as in PyTorch's autograd.
33	law sum_to_size_identity:
34	  for input: Core.Dynamic
35	  for +target: Shape.Shape
36	  for same: {Totality.dimensions(input) == Shape.dimensions(target) : List<&2, U32>}
37	  IdentityModel<input, target, SumToSize.sum_to_size(input, target)>
38	
39	# A target with other dimensions gives exactly the ordered reduce_to result,
40	# so every reduce_to law applies to it.
41	law sum_to_size_reduces:
42	  for input: Core.Dynamic
43	  for +target: Shape.Shape
44	  for differ: {Totality.dimensions(input) != Shape.dimensions(target) : List<&2, U32>}
45	  {SumToSize.sum_to_size(input, target) == Reduce.reduce_to(input, target) : Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}