def insert_row.go

unified-nsga-iii@0.2.2.0 · survival.bend:1032

import Base

1032# Insertion sort step. One def: the recursive call is only the
1033# `before = False` arm, and that arm's tail is the original rest.
1034# `before = True` conses onto that same rest (no second insert).
1035# phase 0 reads the next cons; phase 1 places the row. Fuel is 1+2|xs|.
1036# Recursing through a tail that already contains `x`, then consing `x`
1037# again, duplicates the row. Each smaller CV doubles the list. At the
1038# constrained budgets that exponential spine overflows the native stack
1039# (`memory fault (machine stack overflow?)` on OSY / C1-DTLZ1; TNK
1040# fail-stops). `src/constrained_budget.bend` runs those budgets.
1041def insert_row.go(fuel: Nat, phase: Nat, before: Bool, +x: CvRow, xs: List<&2, CvRow>, +h: CvRow) -> List<&2, CvRow>:
1042  match fuel phase before:
1043    case 0n p b:
1044      x <> xs
1045    case 1n+f 0n b:
1046      match xs:
1047        case Nil{}:
1048          x <> Nil{}
1049        case +head <> tail:
1050          insert_row.go(f, 1n, row_before(x, head), x, tail, head)
1051    case 1n+f 1n+ph True{}:
1052      x <> h <> xs
1053    case 1n+f 1n+ph False{}:
1054      h <> insert_row.go(f, 0n, False{}, x, xs, h)