def zeros_from_mapping

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:615

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws

615def zeros_from_mapping(-input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
616  pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>,
617  -mapping: Laws.MappingWith(input, target, Done{plan}, pair),
618  -listed: Laws.Listed(input, Nil{}),
619  -empty: {Shape.logical_numel(Totality.dimensions(input)) == 0n : Nat}) -> Laws.Zeros<target, pair>:
620  (owner, outcome) = pair
621  match outcome:
622    case Fail{error}:
623      Laws.Zeros{Unit{}}
624    case Done{output}:
625      Laws.Zeros{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(output, index),
626        Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))), Some{0.0},
627        mapping_values(input, target, plan, output, mapping)(Nil{})(listed)(index)(inside),
628        {\{Holds: proof => proof} : Holds<{Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))) == Some{0.0} : Maybe<&2, F32>}> ->
629          {Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))) == Some{0.0} : Maybe<&2, F32>}}(
630          empty_fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input)), empty)))}