import Base
import ./stg.bend as S

# STG -> C backend (v1). Covers the first-order subset -- SVar/SLit/SAdd/
# SLet/SCase -- completely. Mapping is `long`-valued C with depth-numbered
# locals (v0, v1, ...): de Bruijn idx i at depth d reads v(d-1-i), so no
# compile-time env list is needed. SLet becomes a strict C local; this is
# sound because every STG surface program terminates (no fixpoint form),
# hence strict vs lazy is unobservable. SCase becomes a GNU statement
# expression (clang accepts it; we already require clang for native Bend).
# SApp is emitted as a loud 0: with no lambda source form, higher-order
# needs closure conversion (phase 2), and the emitter refuses to pretend.
# String building for SAdd's two sides is a parallel pair, like the
# interpreters. Laws pin exact output strings; running the emitted C
# through clang must print the same answer as s_eval (checked by hand
# below, not by law -- Bend cannot prove C semantics).

def s_vname_go(ok: Bool, u: Nat, d: Nat) -> String:
  match ok:
    case True{}:
      "v" ++ Nat.show(Nat.sub(Nat.sub(d, u), 1n))
    case False{}:
      "0"

def s_vname(+u: Nat, +d: Nat) -> String:
  s_vname_go(Nat.is_lt(u, d), u, d)

def s_emit(+e: S.SExp, +d: Nat) -> String:
  match e:
    case S.SVar{i}:
      s_vname(U32.to_nat(i), d)
    case S.SLit{v}:
      Nat.show(v)
    case S.SAdd{a, b}:
      x y = s_emit(a, d) s_emit(b, d)
      "(" ++ x ++ " + " ++ y ++ ")"
    case S.SLet{b, e2}:
      "({ long v" ++ Nat.show(d) ++ " = " ++ s_emit(b, d) ++ "; " ++ s_emit(e2, 1n+d) ++ "; })"
    case S.SCase{e2, z, s}:
      +dn = Nat.show(d)
      se sz = s_emit(e2, d) s_emit(z, d)
      ss = s_emit(s, 1n+d)
      "({ long c" ++ dn ++ " = " ++ se ++ "; long v" ++ dn ++ " = c" ++ dn ++ " - 1; c" ++ dn ++ " == 0 ? " ++ sz ++ " : " ++ ss ++ "; })"
    case S.SApp{f, x}:
      "(0 /* STG->C v1: SApp needs closure conversion */)"

def s_prog(+e: S.SExp) -> String:
  "#include <stdio.h>\nlong stg_main(void) {\nreturn " ++ s_emit(e, 0n) ++ ";\n}\nint main(void) {\nprintf(\"%ld\\n\", stg_main());\nreturn 0;\n}\n"

def demo84() -> S.SExp:
  S.SLet{S.SLit{42n}, S.SAdd{S.SVar{0}, S.SVar{0}}}

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print(s_prog(demo84()))