def walk_left_below

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:398

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

398# The left walk of a position below the output count lies below the
399# left count.
400def walk_left_below(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +aligned: Shape.Aligned(left, right, output),
401  +q: Nat, +below: {Nat.is_lt(q, Shape.numel(output)) == True{} : Bool}) ->
402  {Nat.is_lt(Shape.walk_left(Shape.index_rows(left, right, output), q), Shape.numel(left)) == True{} : Bool}:
403  match left right output:
404    case Nil{} Nil{} Nil{}:
405      {==}
406    case +lh <> +lt +rh <> +rt +oh <> +ot:
407      Shape.AStep{+axis, +tail} = aligned
408      +s = Shape.numel(ot)
409      walk_left_row(lh, rh, oh, axis, Shape.numel(lt), Nat.div(q, s), Shape.walk_left(Shape.index_rows(lt, rt, ot), Nat.mod(q, s)),
410        div_below(q, oh, s, below),
411        walk_left_below(lt, rt, ot, tail, Nat.mod(q, s),
412          {\{Decomposed: m_below => sum => m_below} : Decomposed<q, s> -> {Nat.is_lt(Nat.mod(q, s), s) == True{} : Bool}}(
413            decompose(q, s, positive_of(q, oh, s, below)))))
414    case Nil{} Nil{} +oh <> +ot:
415      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(Nil{}, Nil{}, oh <> ot), q), 1n) == True{} : Bool}, aligned)
416    case Nil{} +rh <> +rt Nil{}:
417      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(Nil{}, rh <> rt, Nil{}), q), 1n) == True{} : Bool}, aligned)
418    case +lh <> +lt Nil{} Nil{}:
419      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(lh <> lt, Nil{}, Nil{}), q), Shape.numel(lh <> lt)) == True{} : Bool}, aligned)
420    case Nil{} +rh <> +rt +oh <> +ot:
421      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(Nil{}, rh <> rt, oh <> ot), q), 1n) == True{} : Bool}, aligned)
422    case +lh <> +lt Nil{} +oh <> +ot:
423      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(lh <> lt, Nil{}, oh <> ot), q), Shape.numel(lh <> lt)) == True{} : Bool}, aligned)
424    case +lh <> +lt +rh <> +rt Nil{}:
425      Empty.absurd({Nat.is_lt(Shape.walk_left(Shape.index_rows(lh <> lt, rh <> rt, Nil{}), q), Shape.numel(lh <> lt)) == True{} : Bool}, aligned)