# GLIDER — the Life core.
#
# Conway's Game of Life on a torus: cells are U32 (0 dead, 1 alive), rows top
# to bottom, and the grid wraps on both axes, so every operation is total and
# no edge cases exist. Neighbor sums are rotation-based (no index arithmetic),
# which keeps the code small, parallel-friendly and proof-friendly.
import Base

type Board is Data:
  B{rows: List<&2, List<&2, U32>>}

# --- list glue --------------------------------------------------------------

def app(a, -A: Kind(a), xs: List<a, A>, ys: List<a, A>) -> List<a, A>:
  match xs:
    case Nil{}:
      ys
    case h <> t:
      h <> app(a, A, t, ys)

def rev.go(a, -A: Kind(a), xs: List<a, A>, acc: List<a, A>) -> List<a, A>:
  match xs:
    case Nil{}:
      acc
    case h <> t:
      rev.go(a, A, t, (h <> acc))

def rev(a, -A: Kind(a), xs: List<a, A>) -> List<a, A>:
  rev.go(a, A, xs, Nil{})

def rotl(a, -A: Kind(a), xs: List<a, A>) -> List<a, A>:
  match xs:
    case Nil{}:
      Nil{}
    case h <> t:
      app(a, A, t, (h <> Nil{}))

def rotr(a, -A: Kind(a), xs: List<a, A>) -> List<a, A>:
  rev(a, A, rotl(a, A, rev(a, A, xs)))

def rotr_row(r: List<&2, U32>) -> List<&2, U32>:
  rotr(&2, U32, r)

def zadd(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
  match xs ys:
    case Nil{} _:
      Nil{}
    case _ Nil{}:
      Nil{}
    case h1 <> t1 h2 <> t2:
      (U32.add(h1, h2)) <> zadd(t1, t2)

def zsub(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
  match xs ys:
    case Nil{} _:
      Nil{}
    case _ Nil{}:
      Nil{}
    case h1 <> t1 h2 <> t2:
      (U32.sub(h1, h2)) <> zsub(t1, t2)

def zsum(xs: List<&2, U32>) -> U32:
  match xs:
    case Nil{}:
      0
    case h <> t:
      U32.add(h, zsum(t))

def total.rows(rs: List<&2, List<&2, U32>>) -> U32:
  match rs:
    case Nil{}:
      0
    case h <> t:
      U32.add(zsum(h), total.rows(t))

def total(b: Board) -> U32:
  B{rows} = b
  total.rows(rows)

# map over the rows with a template function
def zmap(~f: List<&2, U32> -> List<&2, U32>, xs: List<&2, List<&2, U32>>) ->
  List<&2, List<&2, U32>>:
  match xs:
    case Nil{}:
      Nil{}
    case h <> t:
      f(h) <> zmap(~f, t)

# --- the rule ---------------------------------------------------------------

def b2u(b: Bool) -> U32:
  match b:
    case False{}:
      0
    case True{}:
      1

def rule.go(+n: U32, z: Bool) -> U32:
  match z:
    case True{}:
      b2u(U32.is_eq(n, 3))
    case False{}:
      b2u(Bool.or(U32.is_eq(n, 2), U32.is_eq(n, 3)))

# the new value of a cell: c its current value, n its live-neighbor count
def rule(c: U32, n: U32) -> U32:
  rule.go(n, U32.is_zero(c))

def zrule(selfs: List<&2, U32>, ns: List<&2, U32>) -> List<&2, U32>:
  match selfs ns:
    case Nil{} _:
      Nil{}
    case _ Nil{}:
      Nil{}
    case c <> t1 n <> t2:
      rule(c, n) <> zrule(t1, t2)

# --- the step ---------------------------------------------------------------

# per column, the sum of a cell with its left and right neighbors (0..3)
def hsum(+r: List<&2, U32>) -> List<&2, U32>:
  zadd(rotl(&2, U32, r), zadd(r, rotr(&2, U32, r)))

# one row of the next generation: full 3x3 count minus the cell itself
def step_row(+up: List<&2, U32>, +mid: List<&2, U32>, +down: List<&2, U32>) ->
  List<&2, U32>:
  +full = zadd(hsum(up), zadd(hsum(mid), hsum(down)))
  zrule(mid, zsub(full, mid))

def zmap3(up: List<&2, List<&2, U32>>, mid: List<&2, List<&2, U32>>,
  down: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
  match up mid down:
    case Nil{} _ _:
      Nil{}
    case _ Nil{} _:
      Nil{}
    case _ _ Nil{}:
      Nil{}
    case u <> tu m <> tm d <> td:
      step_row(u, m, d) <> zmap3(tu, tm, td)

# one generation: every row's neighborhood spans the rows above and below
def step(b: Board) -> Board:
  B{+rows} = b
  B{zmap3(rotl(&2, List<&2, U32>, rows), rows, rotr(&2, List<&2, U32>, rows))}

# n generations
def steps(n: Nat, b: Board) -> Board:
  match n:
    case 0n:
      b
    case 1n+p:
      steps(p, step(b))

# --- patterns ---------------------------------------------------------------

def sea(n: Nat) -> List<&2, U32>:
  match n:
    case 0n:
      Nil{}
    case 1n+p:
      0 <> sea(p)

def dead() -> Board:
  B{[sea(6n), sea(6n), sea(6n), sea(6n), sea(6n), sea(6n)]}

def block() -> Board:
  B{[
    [0, 0, 0, 0, 0, 0],
    [0, 1, 1, 0, 0, 0],
    [0, 1, 1, 0, 0, 0],
    [0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0]
  ]}

def single() -> Board:
  B{[
    [0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0],
    [0, 0, 1, 0, 0, 0],
    [0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0]
  ]}

# the doubling of a Nat, spelled out so proofs can unfold it structurally
def double(n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+p:
      1n + (1n + double(p))

def blinker() -> Board:
  B{[
    [0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0],
    [0, 1, 1, 1, 0],
    [0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0]
  ]}

def glider() -> Board:
  B{[
    [0, 0, 0, 0, 0, 0, 0],
    [0, 1, 0, 0, 0, 0, 0],
    [0, 0, 1, 1, 0, 0, 0],
    [0, 1, 1, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0],
    [0, 0, 0, 0, 0, 0, 0]
  ]}

# the same board with every row and every cell shifted one step
def shift_dr(b: Board) -> Board:
  B{+rows} = b
  B{zmap(~rotr_row, rotr(&2, List<&2, U32>, rows))}

# the glider, moved one step down-right
def glider4() -> Board:
  shift_dr(glider())

def glider8() -> Board:
  shift_dr(glider4())

# --- rendering --------------------------------------------------------------

def cell_str.go(z: Bool) -> String:
  match z:
    case True{}:
      "."
    case False{}:
      "#"

def cell_str(c: U32) -> String:
  cell_str.go(U32.is_zero(c))

def nl() -> String:
  SCon{Chr{10}, SNil{}}

def row_str(r: List<&2, U32>) -> String:
  match r:
    case Nil{}:
      SNil{}
    case Con{c, t}:
      cell_str(c) ++ row_str(t)

def rows_str(rs: List<&2, List<&2, U32>>) -> String:
  match rs:
    case Nil{}:
      SNil{}
    case h <> t:
      row_str(h) ++ nl() ++ rows_str(t)

def show_b(b: Board) -> String:
  B{rows} = b
  rows_str(rows)