optimize interaction calculus from Haskell to pure C

optimize_interaction_calculus_to_c_prompt.txt

{-# LANGUAGE MultilineStrings #-}

import Data.IORef
import Debug.Trace
import System.IO.Unsafe
import Text.ParserCombinators.ReadP
import qualified Data.Map as M

type Lab   = String
type Name  = String
type Map a = M.Map String a

-- dp0 ::= x₀
-- dp1 ::= x₁
-- era ::= &{}
-- sup ::= &L{a,b}
-- dup ::= !x&L=v;t
-- var ::= x
-- lam ::= λx.f
-- app ::= (f x)
-- nam ::= name
-- dry ::= (name arg)
data Term
  = Nam Name
  | Var Name
  | Dp0 Name
  | Dp1 Name
  | Era
  | Sup Lab Term Term
  | Dup Name Lab Term Term
  | Lam Name Term
  | Abs Name Term
  | Dry Term Term
  | App Term Term

instance Show Term where
  show (Nam k)       = k
  show (Dry f x)     = "(" ++ show f ++ " " ++ show x ++ ")"
  show (Var k)       = k
  show (Dp0 k)       = k ++ "₀"
  show (Dp1 k)       = k ++ "₁"
  show Era           = "&{}"
  show (Sup l a b)   = "&" ++ l ++ "{" ++ show a ++ "," ++ show b ++ "}"
  show (Dup k l v t) = "!" ++ k ++ "&" ++ l ++ "=" ++ show v ++ ";" ++ show t
  show (Lam k f)     = "λ" ++ k ++ "." ++ show f
  show (Abs k f)     = "λ" ++ k ++ "." ++ show f
  show (App f x)     = "(" ++ show f ++ " " ++ show x ++ ")"

-- Environment
-- ===========
data Env = Env
  { inters  :: Int
  , var_new :: Int
  , dup_new :: Int
  , var_map :: Map Term
  , dp0_map :: Map Term
  , dp1_map :: Map Term
  , dup_map :: Map (Lab,Term)
  } deriving Show

env :: Env
env = Env 0 0 0 M.empty M.empty M.empty M.empty

nameFrom :: String -> Int -> String
nameFrom chars n = build n "" where
  base = length chars
  build k acc | k <= 0    = acc
              | otherwise = let (q,r) = (k - 1) `divMod` base in build q (chars !! r : acc)

fresh :: (Env -> Int) -> (Env -> Int -> Env) -> String -> Env -> (Env, String)
fresh get set chars s =
  let next = get s + 1
  in (set s next, "$" ++ nameFrom chars next)

fresh_var = fresh var_new (\s n -> s { var_new = n }) ['a'..'z']
fresh_dup = fresh dup_new (\s n -> s { dup_new = n }) ['A'..'Z']

subst :: (Env -> Map a) -> (Env -> Map a -> Env) -> Env -> String -> a -> Env
subst get set s k v = set s (M.insert k v (get s))

subst_var = subst var_map (\s m -> s { var_map = m })
subst_dp0 = subst dp0_map (\s m -> s { dp0_map = m })
subst_dp1 = subst dp1_map (\s m -> s { dp1_map = m })
delay_dup = subst dup_map (\s m -> s { dup_map = m })

taker :: (Env -> Map a) -> (Env -> Map a -> Env) -> Env -> String -> (Maybe a, Env)
taker get set s k = let (mt, m) = M.updateLookupWithKey (\_ _ -> Nothing) k (get s) in (mt, set s m)

take_var = taker var_map (\s m -> s { var_map = m })
take_dp0 = taker dp0_map (\s m -> s { dp0_map = m })
take_dp1 = taker dp1_map (\s m -> s { dp1_map = m })
take_dup = taker dup_map (\s m -> s { dup_map = m })

inc_inters :: Env -> Env
inc_inters s = s { inters = inters s + 1 }

-- Parsing
-- =======

lexeme :: ReadP a -> ReadP a
lexeme p = skipSpaces *> p

name :: ReadP String
name = lexeme parse_nam

parse_term :: ReadP Term
parse_term = lexeme $ choice
  [ parse_lam
  , parse_dup
  , parse_app
  , parse_sup
  , parse_era
  , parse_var
  ]

parse_app :: ReadP Term
parse_app = do
  lexeme (char '(')
  ts <- many1 parse_term
  lexeme (char ')')
  case ts of
    (t:rest) -> return (Prelude.foldl App t rest)
    _        -> pfail

parse_lam :: ReadP Term
parse_lam = do
  lexeme (choice [char 'λ', char '\\'])
  k <- name
  lexeme (char '.')
  body <- parse_term
  return $ Lam k body

parse_dup :: ReadP Term
parse_dup = do
  lexeme (char '!')
  k <- name
  lexeme (char '&')
  l <- name
  lexeme (char '=')
  v <- parse_term
  lexeme (char ';')
  t <- parse_term
  return $ Dup k l v t

parse_sup :: ReadP Term
parse_sup = do
  lexeme (char '&')
  l <- name
  lexeme (char '{')
  a <- parse_term
  lexeme (char ',')
  b <- parse_term
  lexeme (char '}')
  return $ Sup l a b

parse_era :: ReadP Term
parse_era = lexeme (string "&{}") >> return Era

parse_var :: ReadP Term
parse_var = do
  k <- name
  choice
    [ string "₀"  >> return (Dp0 k)
    , string "₁"  >> return (Dp1 k)
    , return (Var k)
    ]

parse_nam :: ReadP String
parse_nam = munch1 $ \c
  -> c >= 'a' && c <= 'z'
  || c >= 'A' && c <= 'Z'
  || c >= '0' && c <= '9'
  || c == '_' || c == '/'

read_term :: String -> Term
read_term s = case readP_to_S (parse_term <* skipSpaces <* eof) s of
  [(t, "")] -> t
  _         -> error "bad-parse"

-- Evaluation
-- ==========

wnf :: Env -> Term -> (Env,Term)
wnf s t = go s t where
  go s (App f x)     = let (s0,f0) = wnf s f in app s0 f0 x
  go s (Dup k l v t) = wnf (delay_dup s k (l,v)) t
  go s (Var x)       = var s x
  go s (Dp0 x)       = dp0 s x
  go s (Dp1 x)       = dp1 s x
  go s f             = (s,f)

app :: Env -> Term -> Term -> (Env,Term)
app s (Nam fk)       x = app_nam s fk x
app s (Dry df dx)    x = app_dry s df dx x
app s (Lam fk ff)    x = app_lam s fk ff x
app s (Sup fl fa fb) x = app_sup s fl fa fb x
app s f              x = (s , App f x)

dup :: Env -> String -> Lab -> Term -> Term -> (Env,Term)
dup s k l (Nam vk)       t = dup_nam s k l vk t
dup s k l (Dry vf vx)    t = dup_dry s k l vf vx t
dup s k l (Lam vk vf)    t = dup_lam s k l vk vf t
dup s k l (Sup vl va vb) t = dup_sup s k l vl va vb t
dup s k l v              t = (s , Dup k l v t)

-- Interactions
-- ============
-- (λx.f v)
-- ---------- app-lam
-- x ← v
-- f
app_lam s fx ff v = 
  let s0 = inc_inters s in
  let s1 = subst_var s0 fx v in
  wnf s1 ff

-- (&fL{fa,fb} v)
-- -------------------- app-sup
-- ! x &fL = v
-- &fL{(fa x₀),(fa x₁)}
app_sup s fL fa fb v =
  let s0     = inc_inters s in
  let (s1,x) = fresh_dup s0 in
  let app0   = App fa (Dp0 x) in
  let app1   = App fb (Dp1 x) in
  let sup    = Sup fL app0 app1 in
  let dup    = Dup x fL v sup in
  wnf s1 dup

-- (fk v)
-- ------ app-nam
-- (fk v)
app_nam s fk v = (inc_inters s, Dry (Nam fk) v)

-- ((df dx) v)
-- ----------- app-dry
-- ((df dx) v)
app_dry s df dx v = (inc_inters s, Dry (Dry df dx) v)

-- ! k &L = λvk.vf; t
-- ------------------ dup-lam
-- k₀ ← λx0.g0
-- k₁ ← λx1.g1
-- vk ← &L{x0,x1}
-- ! g &L = vf
-- t
dup_lam s k l vk vf t =
  let s0       = inc_inters s in
  let (s1, x0) = fresh_var s0 in
  let (s2, x1) = fresh_var s1 in
  let (s3, g)  = fresh_dup s2 in
  let s4       = subst_dp0 s3 k  (Lam x0 (Dp0 g)) in
  let s5       = subst_dp1 s4 k  (Lam x1 (Dp1 g)) in
  let s6       = subst_var s5 vk (Sup l (Var x0) (Var x1)) in
  let dup      = Dup g l vf t in
  wnf s6 dup

-- ! k &L = &vL{va,vb}; t
-- ---------------------- dup-sup (==)
-- if l == vL:
--   k₀ ← va
--   k₁ ← vb
--   t
-- else:
--   k₀ ← &vL{a₀,b₀}
--   k₁ ← &vL{a₁,b₁}
--   ! a &L = va
--   ! b &L = vb
--   t
dup_sup s k l vl va vb t
  | l == vl =
    let s0 = inc_inters s in
    let s1 = subst_dp0 s0 k va in
    let s2 = subst_dp1 s1 k vb in
    wnf s2 t
  | l /= vl =
    let s0      = inc_inters s in
    let (s1, a) = fresh_dup s0 in
    let (s2, b) = fresh_dup s1 in
    let s3      = subst_dp0 s2 k (Sup vl (Dp0 a) (Dp0 b)) in
    let s4      = subst_dp1 s3 k (Sup vl (Dp1 a) (Dp1 b)) in
    let dup     = Dup a l va (Dup b l vb t) in
    wnf s4 dup

-- ! k &L = vk; t
-- -------------- dup-nam
-- k₀ ← vk
-- k₁ ← vk
-- t
dup_nam s k l vk t =
  let s0 = inc_inters s in
  let s1 = subst_dp0 s0 k (Nam vk) in
  let s2 = subst_dp1 s1 k (Nam vk) in
  wnf s2 t

-- ! k &L = (vf vx); t
-- --------------------- dup-dry
-- ! f &L = vf
-- ! x &L = vx
-- k₀ ← (f₀ x₀)
-- k₁ ← (f₁ x₁)
-- t
dup_dry s k l vf vx t =
  let s0      = inc_inters s in
  let (s1, f) = fresh_dup s0 in
  let (s2, x) = fresh_dup s1 in
  let s3      = subst_dp0 s2 k (Dry (Dp0 f) (Dp0 x)) in
  let s4      = subst_dp1 s3 k (Dry (Dp1 f) (Dp1 x)) in
  let dup     = Dup f l vf (Dup x l vx t) in
  wnf s4 dup

-- x
-- ------------ var
-- var_map[x]
var :: Env -> String -> (Env,Term)
var s k = case take_var s k of
  (Just t, s0)  -> wnf s0 t
  (Nothing, _)  -> (s, Var k)

-- x₀
-- ---------- dp0
-- dp0_map[x]
dp0 :: Env -> String -> (Env,Term)
dp0 s k = case take_dp0 s k of
  (Just t, s0)  -> wnf s0 t
  (Nothing, _)  -> case take_dup s k of
    (Just (l,v), s0) -> let (s1,v0) = wnf s0 v in dup s1 k l v0 (Dp0 k)
    (Nothing, _)     -> (s, Dp0 k)

-- x₁
-- ---------- dp1
-- dp1_map[x]
dp1 :: Env -> String -> (Env,Term)
dp1 s k = case take_dp1 s k of
  (Just t, s0)  -> wnf s0 t
  (Nothing, _)  -> case take_dup s k of
    (Just (l,v), s0) -> let (s1,v0) = wnf s0 v in dup s1 k l v0 (Dp1 k)
    (Nothing, _)     -> (s, Dp1 k)

-- Normalization
-- =============

nf :: Env -> Term -> (Env,Term)
nf s x = let (s0,x0) = wnf s x in go s0 x0 where
  go s (Nam k)       = (s, Nam k)
  go s (Dry f x)     = let (s0,f0) = nf s f in let (s1,x0) = nf s0 x in (s1, Dry f0 x0)
  go s (Var k)       = (s, Var k)
  go s (Dp0 k)       = (s, Dp0 k)
  go s (Dp1 k)       = (s, Dp1 k)
  go s Era           = (s, Era)
  go s (Sup l a b)   = let (s0,a0) = nf s a in let (s1,b0) = nf s0 b in (s1, Sup l a0 b0)
  go s (Dup k l v t) = let (s0,v0) = nf s v in let (s1,t0) = nf s0 t in (s1, Dup k l v0 t0)
  go s (Lam k f)     = let (s0,f0) = nf (subst_var s k (Nam k)) f in (s0, Lam k f0)
  go s (Abs k f)     = let (s0,f0) = nf s f in (s0, Abs k f0)
  go s (App f x)     = let (s0,f0) = nf s f in let (s1,x0) = nf s0 x in (s1, App f0 x0)

-- Main
-- ====

f :: Int -> String
f n = "λf. " ++ dups ++ final where
  dups  = concat [dup i | i <- [0..n-1]]
  dup 0 = "!F00 &A = f;\n    "
  dup i = "!F" ++ pad i ++ " &A = λx" ++ pad (i-1) ++ ".(F" ++ pad (i-1) ++ "₀ (F" ++ pad (i-1) ++ "₁ x" ++ pad (i-1) ++ "));\n    "
  final = "λx" ++ pad (n-1) ++ ".(F" ++ pad (n-1) ++ "₀ (F" ++ pad (n-1) ++ "₁ x" ++ pad (n-1) ++ "))"
  pad x = if x < 10 then "0" ++ show x else show x

term = read_term $ "((" ++ f 18 ++ " λX.((X λT0.λF0.F0) λT1.λF1.T1)) λT2.λF2.T2)"

main :: IO ()
main = do
  let res = nf env term
  print $          snd $ res
  print $ inters $ fst $ res


PROBLEM:

while the code above works, it is too slow. currently, it takes about 4 seconds
to return the correct result, performing about 450k interactions per second. for
a perspective, similar implementations in C perform about 100m interactions per
second - a 200x difference.

GOAL:

convert the file above to C, and optimize it as much as possible.

IMPORTANT:

keep a parser that reads the term as a string (don't build it manually)

check that the result is still preserved. currently, it prints:

  λ$bgqec.λ$bgqee.$bgqec
  1835080

it is fine to print an equivalent λ-term (ex: λt.λf.t or λa.λb.a, etc.), but
it is NOT fine to print a different λ-term. the interaction count (1835080)
must also be the same, confirming we're running "the same computation".

HINTS:

- you could replace immutable subst maps by a massive pre-allocated mmap'ed array

- you could remove strings / names from runtime terms and re-add when printing

- most work is done by recursive wnf calls. perhaps recursion could be avoided?

- most of the time is spent on allocation. a term pointer could be compacted in
  a single 64-bit word, or even less, using our own internal, fast allocator?

- wnf.h recurses deeply (>10000 nested calls). avoid stack overflows.

that said, it is your job to make it as fast as possible, while keeping the same
computation. you're free to ignore my suggestions and do anything you want!

now, write below a complete, converted C file that does the equivalent
computation, but runs much faster than the one above.

Extra hint of stack overflow; Prev Checkpoint; Code Execution: ON

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>
#include <ctype.h>

// --- Types and Constants ---

typedef uint64_t u64;
typedef uint8_t  u8;

typedef u64 Term;

#define TAG_VAR 0x0ULL
#define TAG_DP0 0x1ULL
#define TAG_DP1 0x2ULL
#define TAG_ERA 0x3ULL
#define TAG_LAM 0x4ULL
#define TAG_APP 0x5ULL
#define TAG_SUP 0x6ULL
#define TAG_DUP 0x7ULL
#define TAG_NAM 0x8ULL
#define TAG_DRY 0x9ULL

#define GET_TAG(t) ((t) >> 60)
#define GET_PAY(t) ((t) & 0x0FFFFFFFFFFFFFFFULL)
#define MAKE_TERM(tag, pay) (((u64)(tag) << 60) | ((pay) & 0x0FFFFFFFFFFFFFFFULL))

struct Node {
    u64 f0;
    u64 f1;
    u64 f2;
    u64 f3;
};

// --- Globals and Memory ---

#define MAX_NODES 0x8000000 // Increased for safety on larger inputs
struct Node* nodes;
u64 nodes_ptr = 0;

#define MAX_ID 0x10000000 // Increased for larger inputs
Term* var_map;
u8*   var_map_has;
Term* dp0_map;
u8*   dp0_map_has;
Term* dp1_map;
u8*   dp1_map_has;
u64*  dup_map_lab;
Term* dup_map_term;
u8*   dup_map_has;

u64 inters = 0;
u64 var_new = 0;
u64 dup_new = 0;

char* name_table[0x100000]; // Increased name table size
u64   name_count = 0;

#define BASE_VAR 0x20000000
#define BASE_DUP 0x40000000

// Manual stack for wnf to avoid recursion overflow
#define MAX_STACK 0x2000000 // 32M * 8B = 256MB stack
Term* arg_stack;
u64   arg_stack_top = 0;

// --- Helper Functions ---

static inline u64 alloc_node() {
    return nodes_ptr++;
}

static inline u64 intern_name(const char* name) {
    for (u64 i = 0; i < name_count; i++) {
        if (strcmp(name_table[i], name) == 0) return i;
    }
    name_table[name_count] = strdup(name);
    return name_count++;
}

static inline u64 fresh_var_id() { return BASE_VAR + var_new++; }
static inline u64 fresh_dup_id() { return BASE_DUP + dup_new++; }

static inline void subst_var(u64 k, Term v) { var_map[k] = v; var_map_has[k] = 1; }
static inline void subst_dp0(u64 k, Term v) { dp0_map[k] = v; dp0_map_has[k] = 1; }
static inline void subst_dp1(u64 k, Term v) { dp1_map[k] = v; dp1_map_has[k] = 1; }
static inline void delay_dup(u64 k, u64 l, Term v) { dup_map_lab[k] = l; dup_map_term[k] = v; dup_map_has[k] = 1; }

static inline int take_var(u64 k, Term* out) {
    if (var_map_has[k]) { *out = var_map[k]; var_map_has[k] = 0; return 1; }
    return 0;
}
static inline int take_dp0(u64 k, Term* out) {
    if (dp0_map_has[k]) { *out = dp0_map[k]; dp0_map_has[k] = 0; return 1; }
    return 0;
}
static inline int take_dp1(u64 k, Term* out) {
    if (dp1_map_has[k]) { *out = dp1_map[k]; dp1_map_has[k] = 0; return 1; }
    return 0;
}
static inline int take_dup(u64 k, u64* l_out, Term* v_out) {
    if (dup_map_has[k]) { *l_out = dup_map_lab[k]; *v_out = dup_map_term[k]; dup_map_has[k] = 0; return 1; }
    return 0;
}

Term wnf(Term t);

// --- Interaction Helpers (Non-recursive) ---
// These functions now return the newly created term (or the next term to evaluate)
// instead of calling wnf() themselves.

static inline Term interact_lam(u64 fk, Term ff, Term v) {
    inters++;
    subst_var(fk, v);
    return ff;
}

static inline Term interact_sup(u64 fl, Term fa, Term fb, Term v) {
    inters++;
    u64 x = fresh_dup_id();
    u64 app0 = alloc_node(); nodes[app0].f0 = fa; nodes[app0].f1 = MAKE_TERM(TAG_DP0, x);
    u64 app1 = alloc_node(); nodes[app1].f0 = fb; nodes[app1].f1 = MAKE_TERM(TAG_DP1, x);
    u64 sup  = alloc_node(); nodes[sup].f0 = fl;  nodes[sup].f1 = MAKE_TERM(TAG_APP, app0); nodes[sup].f2 = MAKE_TERM(TAG_APP, app1);
    u64 dup  = alloc_node(); nodes[dup].f0 = x;   nodes[dup].f1 = fl; nodes[dup].f2 = v; nodes[dup].f3 = MAKE_TERM(TAG_SUP, sup);
    return MAKE_TERM(TAG_DUP, dup);
}

static inline Term interact_nam(u64 fk, Term v) {
    inters++;
    u64 node = alloc_node(); nodes[node].f0 = MAKE_TERM(TAG_NAM, fk); nodes[node].f1 = v;
    return MAKE_TERM(TAG_DRY, node);
}

static inline Term interact_dry(Term df, Term dx, Term v) {
    inters++;
    u64 inner = alloc_node(); nodes[inner].f0 = df; nodes[inner].f1 = dx;
    u64 outer = alloc_node(); nodes[outer].f0 = MAKE_TERM(TAG_DRY, inner); nodes[outer].f1 = v;
    return MAKE_TERM(TAG_DRY, outer);
}

static inline Term interact_app(Term f, Term x) {
    u64 tag = GET_TAG(f);
    u64 pay = GET_PAY(f);
    switch (tag) {
        case TAG_LAM: return interact_lam(nodes[pay].f0, nodes[pay].f1, x);
        case TAG_SUP: return interact_sup(nodes[pay].f0, nodes[pay].f1, nodes[pay].f2, x);
        case TAG_NAM: return interact_nam(pay, x);
        case TAG_DRY: return interact_dry(nodes[pay].f0, nodes[pay].f1, x);
        default: // Should not happen if wnf loop is correct
             fprintf(stderr, "Error: interact_app called on non-interactive term tag %llu\n", (long long unsigned)tag);
             exit(1);
    }
}

// --- Duplication Helpers (Non-recursive) ---

static inline Term dup_lam(u64 k, u64 l, u64 vk, Term vf, Term t) {
    inters++;
    u64 x0 = fresh_var_id();
    u64 x1 = fresh_var_id();
    u64 g  = fresh_dup_id();
    u64 lam0 = alloc_node(); nodes[lam0].f0 = x0; nodes[lam0].f1 = MAKE_TERM(TAG_DP0, g);
    subst_dp0(k, MAKE_TERM(TAG_LAM, lam0));
    u64 lam1 = alloc_node(); nodes[lam1].f0 = x1; nodes[lam1].f1 = MAKE_TERM(TAG_DP1, g);
    subst_dp1(k, MAKE_TERM(TAG_LAM, lam1));
    u64 sup  = alloc_node(); nodes[sup].f0 = l; nodes[sup].f1 = MAKE_TERM(TAG_VAR, x0); nodes[sup].f2 = MAKE_TERM(TAG_VAR, x1);
    subst_var(vk, MAKE_TERM(TAG_SUP, sup));
    u64 dup = alloc_node(); nodes[dup].f0 = g; nodes[dup].f1 = l; nodes[dup].f2 = vf; nodes[dup].f3 = t;
    return MAKE_TERM(TAG_DUP, dup);
}

static inline Term dup_sup(u64 k, u64 l, u64 vl, Term va, Term vb, Term t) {
    if (l == vl) {
        inters++;
        subst_dp0(k, va);
        subst_dp1(k, vb);
        return t;
    } else {
        inters++;
        u64 a = fresh_dup_id();
        u64 b = fresh_dup_id();
        u64 sup0 = alloc_node(); nodes[sup0].f0 = vl; nodes[sup0].f1 = MAKE_TERM(TAG_DP0, a); nodes[sup0].f2 = MAKE_TERM(TAG_DP0, b);
        subst_dp0(k, MAKE_TERM(TAG_SUP, sup0));
        u64 sup1 = alloc_node(); nodes[sup1].f0 = vl; nodes[sup1].f1 = MAKE_TERM(TAG_DP1, a); nodes[sup1].f2 = MAKE_TERM(TAG_DP1, b);
        subst_dp1(k, MAKE_TERM(TAG_SUP, sup1));
        u64 dup_b = alloc_node(); nodes[dup_b].f0 = b; nodes[dup_b].f1 = l; nodes[dup_b].f2 = vb; nodes[dup_b].f3 = t;
        u64 dup_a = alloc_node(); nodes[dup_a].f0 = a; nodes[dup_a].f1 = l; nodes[dup_a].f2 = va; nodes[dup_a].f3 = MAKE_TERM(TAG_DUP, dup_b);
        return MAKE_TERM(TAG_DUP, dup_a);
    }
}

static inline Term dup_nam(u64 k, u64 l, u64 vk, Term t) {
    inters++;
    subst_dp0(k, MAKE_TERM(TAG_NAM, vk));
    subst_dp1(k, MAKE_TERM(TAG_NAM, vk));
    return t;
}

static inline Term dup_dry(u64 k, u64 l, Term vf, Term vx, Term t) {
    inters++;
    u64 f = fresh_dup_id();
    u64 x = fresh_dup_id();
    u64 dry0 = alloc_node(); nodes[dry0].f0 = MAKE_TERM(TAG_DP0, f); nodes[dry0].f1 = MAKE_TERM(TAG_DP0, x);
    subst_dp0(k, MAKE_TERM(TAG_DRY, dry0));
    u64 dry1 = alloc_node(); nodes[dry1].f0 = MAKE_TERM(TAG_DP1, f); nodes[dry1].f1 = MAKE_TERM(TAG_DP1, x);
    subst_dp1(k, MAKE_TERM(TAG_DRY, dry1));
    u64 dup_x = alloc_node(); nodes[dup_x].f0 = x; nodes[dup_x].f1 = l; nodes[dup_x].f2 = vx; nodes[dup_x].f3 = t;
    u64 dup_f = alloc_node(); nodes[dup_f].f0 = f; nodes[dup_f].f1 = l; nodes[dup_f].f2 = vf; nodes[dup_f].f3 = MAKE_TERM(TAG_DUP, dup_x);
    return MAKE_TERM(TAG_DUP, dup_f);
}

static inline Term dup_term(u64 k, u64 l, Term v, Term t) {
    u64 tag = GET_TAG(v);
    u64 pay = GET_PAY(v);
    switch (tag) {
        case TAG_LAM: return dup_lam(k, l, nodes[pay].f0, nodes[pay].f1, t);
        case TAG_SUP: return dup_sup(k, l, nodes[pay].f0, nodes[pay].f1, nodes[pay].f2, t);
        case TAG_NAM: return dup_nam(k, l, pay, t);
        case TAG_DRY: return dup_dry(k, l, nodes[pay].f0, nodes[pay].f1, t);
        default: {
             u64 node = alloc_node();
             nodes[node].f0 = k; nodes[node].f1 = l; nodes[node].f2 = v; nodes[node].f3 = t;
             return MAKE_TERM(TAG_DUP, node);
        }
    }
}

// --- Iterative Weak Normal Form ---

Term wnf(Term t) {
    u64 saved_stack = arg_stack_top;
    u64 l_val;
    Term v_val;

    while (1) {
        u64 tag = GET_TAG(t);
        u64 pay = GET_PAY(t);

        // 1. Reduce Head
        switch (tag) {
            case TAG_APP:
                arg_stack[arg_stack_top++] = nodes[pay].f1;
                t = nodes[pay].f0;
                continue;
            case TAG_DUP:
                delay_dup(nodes[pay].f0, nodes[pay].f1, nodes[pay].f2);
                t = nodes[pay].f3;
                continue;
            case TAG_VAR:
                if (take_var(pay, &t)) continue;
                goto stuck;
            case TAG_DP0:
                if (take_dp0(pay, &t)) continue;
                if (take_dup(pay, &l_val, &v_val)) {
                    // Recursing here for wnf(v_val) as specified in original logic.
                    // For absolute stack safety this should also be iterative,
                    // but usually this path is less deep than App spines.
                    t = dup_term(pay, l_val, wnf(v_val), MAKE_TERM(TAG_DP0, pay));
                    continue;
                }
                goto stuck;
            case TAG_DP1:
                if (take_dp1(pay, &t)) continue;
                if (take_dup(pay, &l_val, &v_val)) {
                    t = dup_term(pay, l_val, wnf(v_val), MAKE_TERM(TAG_DP1, pay));
                    continue;
                }
                goto stuck;
            case TAG_LAM:
            case TAG_SUP:
            case TAG_NAM:
            case TAG_DRY:
                // Head is a value, check for pending arguments to interact with.
                if (arg_stack_top > saved_stack) {
                    t = interact_app(t, arg_stack[--arg_stack_top]);
                    continue;
                }
                return t;
            default:
                goto stuck;
        }

        stuck:
        // Head is stuck. If we have pending arguments, we must rebuild the App chain
        // so that the returned term correctly represents the stuck application.
        if (arg_stack_top > saved_stack) {
             Term x = arg_stack[--arg_stack_top];
             u64 node = alloc_node();
             nodes[node].f0 = t;
             nodes[node].f1 = x;
             t = MAKE_TERM(TAG_APP, node);
             goto stuck; // Loop to rebuild all pending args
        }
        return t;
    }
}

// --- Normal Form (Recursive, but less depth-critical usually) ---

Term nf(Term t) {
    t = wnf(t);
    u64 tag = GET_TAG(t);
    u64 pay = GET_PAY(t);
    switch (tag) {
        case TAG_LAM: {
             u64 new_node = alloc_node();
             nodes[new_node].f0 = nodes[pay].f0;
             subst_var(nodes[pay].f0, MAKE_TERM(TAG_NAM, nodes[pay].f0));
             nodes[new_node].f1 = nf(nodes[pay].f1);
             return MAKE_TERM(TAG_LAM, new_node);
        }
        case TAG_APP: {
            u64 new_node = alloc_node();
            nodes[new_node].f0 = nf(nodes[pay].f0);
            nodes[new_node].f1 = nf(nodes[pay].f1);
            return MAKE_TERM(TAG_APP, new_node);
        }
        case TAG_SUP: {
            u64 new_node = alloc_node();
            nodes[new_node].f0 = nodes[pay].f0;
            nodes[new_node].f1 = nf(nodes[pay].f1);
            nodes[new_node].f2 = nf(nodes[pay].f2);
            return MAKE_TERM(TAG_SUP, new_node);
        }
        case TAG_DUP: {
            u64 new_node = alloc_node();
            nodes[new_node].f0 = nodes[pay].f0;
            nodes[new_node].f1 = nodes[pay].f1;
            nodes[new_node].f2 = nf(nodes[pay].f2);
            nodes[new_node].f3 = nf(nodes[pay].f3);
            return MAKE_TERM(TAG_DUP, new_node);
        }
        case TAG_DRY: {
             u64 new_node = alloc_node();
             nodes[new_node].f0 = nf(nodes[pay].f0);
             nodes[new_node].f1 = nf(nodes[pay].f1);
             return MAKE_TERM(TAG_DRY, new_node);
        }
        default: return t;
    }
}

// --- Printing ---

void print_base_name(u64 n, char flag) {
    if (flag == 0 && n < name_count) {
        printf("%s", name_table[n]);
        return;
    }
    char *chars = (flag == 2) ? "ABCDEFGHIJKLMNOPQRSTUVWXYZ" : "abcdefghijklmnopqrstuvwxyz";
    u64 base = 26;
    u64 k = n + 1;
    printf("$");
    char buf[64];
    int pos = 0;
    while (1) {
        if (k <= 0) break;
        u64 q = (k - 1) / base;
        u64 r = (k - 1) % base;
        buf[pos++] = chars[r];
        k = q;
    }
    for (int i = pos - 1; i >= 0; i--) putchar(buf[i]);
}

void print_name(u64 pay) {
    if (pay >= BASE_DUP) print_base_name(pay - BASE_DUP, 2);
    else if (pay >= BASE_VAR) print_base_name(pay - BASE_VAR, 1);
    else print_base_name(pay, 0);
}

void print_term(Term t) {
    u64 tag = GET_TAG(t);
    u64 pay = GET_PAY(t);
    switch (tag) {
        case TAG_NAM: print_name(pay); break;
        case TAG_VAR: print_name(pay); break;
        case TAG_DP0: print_name(pay); printf("₀"); break;
        case TAG_DP1: print_name(pay); printf("₁"); break;
        case TAG_ERA: printf("&{}"); break;
        case TAG_LAM: printf("λ"); print_name(nodes[pay].f0); printf("."); print_term(nodes[pay].f1); break;
        case TAG_APP: printf("("); print_term(nodes[pay].f0); printf(" "); print_term(nodes[pay].f1); printf(")"); break;
        case TAG_SUP: printf("&"); print_name(nodes[pay].f0); printf("{"); print_term(nodes[pay].f1); printf(","); print_term(nodes[pay].f2); printf("}"); break;
        case TAG_DUP: printf("!"); print_name(nodes[pay].f0); printf("&"); print_name(nodes[pay].f1); printf("="); print_term(nodes[pay].f2); printf(";"); print_term(nodes[pay].f3); break;
        case TAG_DRY: printf("("); print_term(nodes[pay].f0); printf(" "); print_term(nodes[pay].f1); printf(")"); break;
    }
}

// --- Parsing and Setup ---

char* parse_ptr;
void skip_spaces() { while (isspace(*parse_ptr)) parse_ptr++; }

u64 parse_name_val() {
    skip_spaces();
    char buf[256];
    int len = 0;
    while (isalnum(*parse_ptr) || *parse_ptr == '_' || *parse_ptr == '/' || *parse_ptr == '$') {
        buf[len++] = *parse_ptr++;
    }
    buf[len] = 0;
    return intern_name(buf);
}

Term parse_term_rec();
Term parse_app_rest(Term f) {
    skip_spaces();
    if (*parse_ptr == ')') { parse_ptr++; return f; }
    Term x = parse_term_rec();
    u64 node = alloc_node();
    nodes[node].f0 = f; nodes[node].f1 = x;
    return parse_app_rest(MAKE_TERM(TAG_APP, node));
}

Term parse_term_rec() {
    skip_spaces();
    char c = *parse_ptr;
    if (c == '(') {
        parse_ptr++; Term f = parse_term_rec(); return parse_app_rest(f);
    } else if (c == 'λ' || c == '\\') {
        parse_ptr++; u64 name = parse_name_val();
        skip_spaces(); if (*parse_ptr == '.') parse_ptr++;
        Term body = parse_term_rec();
        u64 node = alloc_node(); nodes[node].f0 = name; nodes[node].f1 = body;
        return MAKE_TERM(TAG_LAM, node);
    } else if (c == '&') {
        parse_ptr++;
        if (*parse_ptr == '{' && *(parse_ptr+1) == '}') { parse_ptr += 2; return MAKE_TERM(TAG_ERA, 0); }
        u64 l = parse_name_val();
        skip_spaces(); if (*parse_ptr == '{') parse_ptr++;
        Term a = parse_term_rec();
        skip_spaces(); if (*parse_ptr == ',') parse_ptr++;
        Term b = parse_term_rec();
        skip_spaces(); if (*parse_ptr == '}') parse_ptr++;
        u64 node = alloc_node(); nodes[node].f0 = l; nodes[node].f1 = a; nodes[node].f2 = b;
        return MAKE_TERM(TAG_SUP, node);
    } else if (c == '!') {
        parse_ptr++; u64 k = parse_name_val();
        skip_spaces(); if (*parse_ptr == '&') parse_ptr++;
        u64 l = parse_name_val();
        skip_spaces(); if (*parse_ptr == '=') parse_ptr++;
        Term v = parse_term_rec();
        skip_spaces(); if (*parse_ptr == ';') parse_ptr++;
        Term t = parse_term_rec();
        u64 node = alloc_node(); nodes[node].f0 = k; nodes[node].f1 = l; nodes[node].f2 = v; nodes[node].f3 = t;
        return MAKE_TERM(TAG_DUP, node);
    } else {
        u64 name = parse_name_val();
        if (strncmp(parse_ptr, "₀", 3) == 0) { parse_ptr += 3; return MAKE_TERM(TAG_DP0, name); }
        else if (strncmp(parse_ptr, "₁", 3) == 0) { parse_ptr += 3; return MAKE_TERM(TAG_DP1, name); }
        return MAKE_TERM(TAG_VAR, name);
    }
}

void gen_f(int n, char* buf) {
    char* p = buf;
    p += sprintf(p, "λf. ");
    for (int i = 0; i < n; i++) {
        if (i == 0) p += sprintf(p, "!F00 &A = f; ");
        else p += sprintf(p, "!F%02d &A = λx%02d.(F%02d₀ (F%02d₁ x%02d)); ", i, i-1, i-1, i-1, i-1);
    }
    p += sprintf(p, "λx%02d.(F%02d₀ (F%02d₁ x%02d))", n-1, n-1, n-1, n-1);
}

void init_mem() {
    nodes = malloc(sizeof(struct Node) * MAX_NODES);
    var_map = malloc(sizeof(Term) * MAX_ID);
    var_map_has = calloc(MAX_ID, 1);
    dp0_map = malloc(sizeof(Term) * MAX_ID);
    dp0_map_has = calloc(MAX_ID, 1);
    dp1_map = malloc(sizeof(Term) * MAX_ID);
    dp1_map_has = calloc(MAX_ID, 1);
    dup_map_lab = malloc(sizeof(u64) * MAX_ID);
    dup_map_term = malloc(sizeof(Term) * MAX_ID);
    dup_map_has = calloc(MAX_ID, 1);
    arg_stack = malloc(sizeof(Term) * MAX_STACK);
    if (!nodes || !var_map || !var_map_has || !dp0_map || !dp0_map_has || 
        !dp1_map || !dp1_map_has || !dup_map_lab || !dup_map_term || !dup_map_has || !arg_stack) {
        fprintf(stderr, "Error: Failed to allocate memory. Requires approx 6GB.\n");
        exit(1);
    }
}

char input_buf[5000000]; 

int main() {
    init_mem();
    char f_buf[131072];
    gen_f(18, f_buf); // Can now try increasing this if memory permits
    sprintf(input_buf, "((%s λX.((X λT0.λF0.F0) λT1.λF1.T1)) λT2.λF2.T2)", f_buf);
    
    parse_ptr = input_buf;
    Term root = parse_term_rec();
    
    Term res = nf(root);
    
    print_term(res);
    printf("\n%llu\n", (long long unsigned)inters);
    
    return 0;
}