def kept_hit_step

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

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

714def kept_hit_step(+g: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat, +digit: Nat,
715  decision: Shape.BoolCase<Nat.is_eq(digit, Nat.div(target, left))>,
716  +from: {Nat.is_le(digit, Nat.div(target, left)) == True{} : Bool},
717  +until: {Nat.is_lt(Nat.div(target, left), Nat.add(digit, 1n+g)) == True{} : Bool},
718  +given: Decomposed<target, left>, +bound: BoundBy<rest, left, stride>,
719  rec: @+next: Nat -> @+from: {Nat.is_le(next, Nat.div(target, left)) == True{} : Bool} ->
720    @+until: {Nat.is_lt(Nat.div(target, left), Nat.add(next, g)) == True{} : Bool} ->
721    {masked(Nat.mul(g, stride), Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(next, stride)) ==
722      masked(stride, rest, Nat.mod(target, left), Nat.add(base, Nat.mul(right, Nat.div(target, left))), 0n) : List<&2, Nat>}) ->
723  {masked(Nat.mul(1n+g, stride), Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) ==
724    masked(stride, rest, Nat.mod(target, left), Nat.add(base, Nat.mul(right, Nat.div(target, left))), 0n) : List<&2, Nat>}:
725  match decision:
726    case Shape.BTrue{equal}:
727      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
728      +c = Nat.mul(digit, stride)
729      +dt = Nat.div(target, left)
730      +tr = Nat.mod(target, left)
731      +hit = masked(stride, rest, tr, Nat.add(base, Nat.mul(right, dt)), 0n)
732      +same = Arith.eq_true(digit, dt, Equal.sym(Bool, True{}, Nat.is_eq(digit, dt), equal))
733      +mine = masked(stride, rest, tr, Nat.add(base, Nat.mul(right, digit)), 0n)
734      %Equal.sym(List<&2, Nat>, masked(Nat.add(stride, Nat.mul(g, stride)), rows, target, base, c),
735        List.append(&2, Nat, masked(stride, rows, target, base, c), masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))),
736        masked_split(stride, Nat.mul(g, stride), rows, target, base, c)) :
737        {_ == hit : List<&2, Nat>}
738      %Equal.sym(List<&2, Nat>, masked(stride, rows, target, base, c), mine,
739        block(stride, left, right, rest, target, tr, base, digit, Hit{given, same, {==}})) :
740        {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == hit : List<&2, Nat>}
741      %next_cursor(digit, stride) :
742        {List.append(&2, Nat, mine, masked(Nat.mul(g, stride), rows, target, base, _)) == hit : List<&2, Nat>}
743      %Equal.sym(List<&2, Nat>, masked(Nat.mul(g, stride), rows, target, base, Nat.mul(1n+digit, stride)), Nil{},
744        kept_after(g, stride, left, right, rest, target, base, 1n+digit,
745          %same : {Nat.is_lt(_, 1n+digit) == True{} : Bool}
746          lt_self_succ(digit), bound)) :
747        {List.append(&2, Nat, mine, _) == hit : List<&2, Nat>}
748      %Equal.sym(List<&2, Nat>, List.append(&2, Nat, mine, Nil{}), mine, append_nil(mine)) : {_ == hit : List<&2, Nat>}
749      Equal.cong(Nat, List<&2, Nat>, d => masked(stride, rest, tr, Nat.add(base, Nat.mul(right, d)), 0n), digit, dt, same)
750    case Shape.BFalse{equal}:
751      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
752      +c = Nat.mul(digit, stride)
753      +dt = Nat.div(target, left)
754      +tr = Nat.mod(target, left)
755      +hit = masked(stride, rest, tr, Nat.add(base, Nat.mul(right, dt)), 0n)
756      +differ = Equal.sym(Bool, False{}, Nat.is_eq(digit, dt), equal)
757      %Equal.sym(List<&2, Nat>, masked(Nat.add(stride, Nat.mul(g, stride)), rows, target, base, c),
758        List.append(&2, Nat, masked(stride, rows, target, base, c), masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))),
759        masked_split(stride, Nat.mul(g, stride), rows, target, base, c)) :
760        {_ == hit : List<&2, Nat>}
761      %Equal.sym(List<&2, Nat>, masked(stride, rows, target, base, c), Nil{},
762        block_off(stride, left, right, rest, target, base, digit, Off{bound, differ})) :
763        {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == hit : List<&2, Nat>}
764      %next_cursor(digit, stride) :
765        {masked(Nat.mul(g, stride), rows, target, base, _) == hit : List<&2, Nat>}
766      rec(1n+digit, le_ne_succ(digit, dt, from, differ),
767        %Arith.add_succ(digit, g) : {Nat.is_lt(dt, _) == True{} : Bool}
768        until)