def List.merge.go

Base · base.bend:1150

1150# The fuel bounds the steps: a sort passes its length, enough for any merge.
1151def List.merge.go(
1152  ~A: Data, ~le: A -> A -> Bool, fuel: Nat,
1153  st: List<&2, A> & List<&2, A> & List<&2, A>
1154) -> List<&2, A>:
1155  match fuel:
1156    case 0n:
1157      (acc, xs, ys) = st
1158      List.reverse.go(&2, A, acc, List.append(&2, A, xs, ys))
1159    case 1n+f:
1160      (acc, xs, ys) = st
1161      match xs ys:
1162        case Nil{} Nil{}:
1163          List.reverse.go(&2, A, acc, Nil{})
1164        case Nil{} y <> yt:
1165          List.reverse.go(&2, A, acc, y <> yt)
1166        case x <> xt Nil{}:
1167          List.reverse.go(&2, A, acc, x <> xt)
1168        case +x <> xt +y <> yt:
1169          List.merge.go(~A, ~le, f,
1170            List.merge.step(A, acc, x, xt, y, yt, le(x, y)))