def digits_step

bendtorch-core@0.1.0.0 · src/shape/coordinate_proofs.bend:93

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index

93def digits_step(+head: Nat, +tail: List<&2, Nat>, rec: @+index: Shape.Fin(Shape.numel(tail)) -> {Shape.indices(tail, Shape.unflatten(tail, index)) == Shape.digits(tail, Shape.Fin.value(Shape.numel(tail), index)) : List<&2, Nat>}, coordinate: Shape.Fin(head) & Shape.Fin(Shape.numel(tail))) -> {Shape.indices(head <> tail, Shape.unflatten.step(head, tail, rest => Shape.unflatten(tail, rest), coordinate)) == Shape.digits(head <> tail, Shape.Fin.value(Nat.mul(head, Shape.numel(tail)), Shape.Fin.pack(head, Shape.numel(tail), coordinate))) : List<&2, Nat>}:
94  (+first, +last) = coordinate
95  +stride = Shape.numel(tail)
96  +major = Shape.Fin.value(head, first)
97  +minor = Shape.Fin.value(stride, last)
98  %Equal.sym(Nat, Shape.Fin.value(Nat.mul(head, stride), Shape.Fin.pack(head, stride, (first, last))), Nat.add(Nat.mul(major, stride), minor), Index.pack_value(head, stride, first, last)) : {major <> Shape.indices(tail, Shape.unflatten(tail, last)) == Shape.digits(head <> tail, _) : List<&2, Nat>}
99  %Nats.divmod_exact(major, stride, minor, Shape.Fin.bound(stride, last)) : {major <> Shape.indices(tail, Shape.unflatten(tail, last)) == Pair.fst(Nat, Nat, _) <> Shape.digits(tail, Pair.snd(Nat, Nat, _)) : List<&2, Nat>}
100  %rec(last) : {major <> Shape.indices(tail, Shape.unflatten(tail, last)) == major <> _ : List<&2, Nat>}
101  {==}