Lean4
/-- `posToShiftedPos lths diff` takes as input an array `lths` of natural numbers,
and one further natural number `diff`.
It adds up the elements of `lths` occupying the odd positions, as long as the sum of the
elements in the even positions does not exceed `diff`.
It returns the sum of the accumulated odds and `diff`.
This is useful to figure out the difference between the output of `polishSource s` and `s` itself.
It plays a role similar to the `fileMap`. -/
def posToShiftedPos (lths : Array Nat) (diff : Nat) : Nat :=
Id.run
(do
let mut (ws, noWS) := (diff, 0)
for con in [:lths.size / 2]do
let curr := lths[2 * con]!
if noWS + curr < diff then
noWS := noWS + curr
ws := ws + lths[2 * con + 1]!
else
break
return ws)
