-- OldCheck:
-- (omitted)

# The Interaction Calculus

The [Interaction Calculus](https://github.com/VictorTaelin/Interaction-Calculus)
is a minimal term rewriting system inspired by the Lambda Calculus (λC), but
with some key differences:
1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
3. There is a new core primitive: the superposition.

An Interaction Calculus term is defined by the following grammar:

```haskell
Term ::=
  | VAR: Name
  | ERA: "*"
  | LAM: "λ" Name "." Term
  | APP: "(" Term " " Term ")"
  | SUP: "&" Label "{" Term "," Term "}"
  | DUP: "!" "&" Label "{" Name "," Name "}" "=" Term ";" Term
```

Where:
- VAR represents a variable.
- ERA represents an erasure.
- LAM represents a lambda.
- APP represents a application.
- SUP represents a superposition.
- DUP represents a duplication.

Lambdas are curried, and work like their λC counterpart, except with a relaxed
scope, and with affine usage. Applications eliminate lambdas, like in λC,
through the beta-reduce (APP-LAM) interaction.

Superpositions work like pairs. Duplications eliminate superpositions through
the DUP-SUP interaction, which works exactly like a pair projection.

What makes SUPs and DUPs unique is how they interact with LAMs and APPs. When a
SUP is applied to an argument, it reduces through the APP-SUP interaction, and
when a LAM is projected, it reduces through the DUP-LAM interaction. This gives
a computational behavior for every possible interaction: there are no runtime
errors on the core Interaction Calculus.

The 'Label' is a numeric value that affects some interactions, like DUP-SUP,
causing terms to commute, instead of annihilate. Read Lafont's Interaction
Combinators paper to learn more.

The core interaction rules are listed below:

```haskell
(* a)
----- APP-ERA
*

(λx.f a)
-------- APP-LAM
x <- a
f

(&L{a,b} c)
----------------- APP-SUP
! &L{c0,c1} = c;
&L{(a c0),(b c1)}

! &L{r,s} = *;
K
-------------- DUP-ERA
r <- *
s <- *
K

! &L{r,s} = λx.f;
K
----------------- DUP-LAM
r <- λx0.f0
s <- λx1.f1
x <- &L{x0,x1}
! &L{f0,f1} = f;
K

! &L{x,y} = &L{a,b};
K
-------------------- DUP-SUP (if equal labels)
x <- a
y <- b
K

! &L{x,y} = &R{a,b};
K
-------------------- DUP-SUP (if different labels)
x <- &R{a0,b0} 
y <- &R{a1,b1}
! &L{a0,a1} = a;
! &L{b0,b1} = b;
K
```

Where `x <- t` stands for a global substitution of `x` by `t`.

Since variables are affine, substitutions can be implemented efficiently by just
inserting an entry in a global substitution map (`sub[var] = value`). There is
no need to traverse the target term, or to handle name capture, as long as fresh
variable names are globally unique. Thread-safe substitutions can be performed
with a single atomic-swap.

Below is a pseudocode implementation of these interaction rules:

```python
def app_lam(app, lam):
  sub[lam.nam] = app.arg
  return lam.bod

def app_sup(app, sup):
  x0 = fresh()
  x1 = fresh()
  a0 = App(sup.lft, Var(x0))
  a1 = App(sup.rgt, Var(x1))
  return Dup(sup.lab, x0, x1, app.arg, Sup(a0, a1))

def dup_lam(dup, lam):
  x0 = fresh()
  x1 = fresh()
  f0 = fresh()
  f1 = fresh()
  sub[dup.lft] = Lam(x0, Var(f0))
  sub[dup.rgt] = Lam(x1, Var(f1))
  sub[lam.nam] = Sup(dup.lab, Var(x0), Var(x1))
  return Dup(dup.lab, f0, f1, lam.bod, dup.bod)

def dup_sup(dup, sup):
  if dup.lab == sup.lab:
    sub[dup.lft] = sup.lft
    sub[dup.rgt] = sup.rgt
    return dup.bod
```

Terms can be reduced to weak head normal form, which means reducing until the
outermost constructor is a value (LAM, SUP, etc.), or until no more reductions
are possible. Example:

```python
def whnf(term):
  while True:
    match term:
      case Var(nam):
        if nam in sub:
          term = sub[nam]
        else:
          return term
      case App(fun, arg):
        fun = whnf(fun)
        match fun.tag:
          case LAM: term = app_lam(term, fun)
          case SUP: term = app_sup(term, fun)
          case _  : return App(fun, arg)
      case Dup(lft, rgt, val, bod):
        val = whnf(val)
        match val.tag:
          case LAM: term = dup_lam(term, val)
          case SUP: term = dup_sup(term, val)
          case _  : return Dup(lft, rgt, val, bod)
      case _:
        return term
```

Terms can be reduced to full normal form by recursively taking the whnf:

```python
def normal(term):
  term = whnf(term)
  match term:
    case Lam(nam, bod):
      bod_nf = normal(bod)
      return Lam(nam, bod_nf)
    case App(fun, arg):
      fun_nf = normal(fun)
      arg_nf = normal(arg)
      return App(fun_nf, arg_nf)
    ...
    case _:
      return term
```

Below are some normalization examples.

Example 0: (simple λ-term)

```haskell
(λx.λt.(t x) λy.y)
------------------ APP-LAM
λt.(t λy.y)
```

Example 1: (larger λ-term)

```haskell
(λb.λt.λf.((b f) t) λT.λF.T)
---------------------------- APP-LAM
λt.λf.((λT.λF.T f) t)
----------------------- APP-LAM
λt.λf.(λF.t f)
-------------- APP-LAM
λt.λf.t
```

Example 2: (global scopes)

```haskell
{x,(λx.λy.y λk.k)}
------------------ APP-LAM
{λk.k,λy.y}
```

Example 3: (superposition)

```haskell
!{a,b} = {λx.x,λy.y}; (a b)
--------------------------- DUP-SUP
(λx.x λy.y)
----------- APP-LAM
λy.y
```

Example 4: (overlap)

```haskell
({λx.x,λy.y} λz.z)
------------------ APP-SUP  
! {x0,x1} = λz.z; {(λx.x x0),(λy.y x1)}  
--------------------------------------- DUP-LAM  
! {f0,f1} = {r,s}; {(λx.x λr.f0),(λy.y λs.f1)}  
---------------------------------------------- DUP-SUP  
{(λx.x λr.r),(λy.y λs.s)}  
------------------------- APP-LAM  
{λr.r,(λy.y λs.s)}  
------------------ APP-LAM  
{λr.r,λs.s}  
```

Example 5: (default test term)

The following term can be used to test all interactions:

```haskell
((λf.λx.!{f0,f1}=f;(f0 (f1 x)) λB.λT.λF.((B F) T)) λa.λb.a)
----------------------------------------------------------- 16 interactions
λa.λb.a
```

# Collapsing

An Interaction Calculus term can be collapsed to a superposed tree of pure
Lambda Calculus terms without SUPs and DUPs, by extending the evaluator with the
following collapse interactions:

```haskell
λx.*
------ ERA-LAM
x <- *
*

(f *)
----- ERA-APP
*

λx.&L{f0,f1}
----------------- SUP-LAM
x <- &L{x0,x1}
&L{λx0.f0,λx1.f1}

(f &L{x0,x1})
------------------- SUP-APP
!&L{f0,f1} = f;
&L{(f0 x0),(f1 x1)}

&R{&L{x0,x1},y}
----------------------- SUP-SUP-X (if R>L)
!&R{y0,y1} = y;
&L{&R{x0,x1},&R{y0,y1}}

&R{x,&L{y0,y1}}
----------------------- SUP-SUP-Y (if R>L)
!&R{x0,x1} = x;
&L{&R{x0,x1},&R{y0,y1}}

!&L{x0,x1} = x; K
----------------- DUP-VAR
x0 <- x
x1 <- x
K

!&L{a0,a1} = (f x); K
--------------------- DUP-APP
a0 <- (f0 x0)
a1 <- (f1 x1)
!&L{f0,f1} = f;
!&L{x0,x1} = x;
K
```

module Type where

import Data.Word
import Foreign.Ptr

import Control.Applicative ((<|>))
import Control.Monad (forM)
import Data.Char (chr, ord)
import Data.Char (intToDigit)
import Data.IORef
import Data.List
import Data.Word
import Numeric (showIntAtBase)
import System.IO.Unsafe (unsafePerformIO)
import qualified Data.Map.Strict as MS hiding (map)

-- Core Types
-- ----------

type Tag  = Word8
type Lab  = Word32
type Loc  = Word32
type Term = Word64

type FnID = Word16
type Name = String
type Move = (Name, Core) -- !x = term

data LetT = LAZY | STRI deriving (Eq, Enum)
data MatT = SWI | MAT Word16 | IFL Word16 deriving (Show, Eq)

-- **Note: we're refactoring HVM3's Code Type.**

-- OLD TYPE:

-- data Core
  -- = Var Name                    -- x
  -- | Ref Name Word16 [Core]      -- @fn
  -- | Era                         -- *
  -- | Sup Lab Core Core           -- &L{a b}
  -- | Dup Lab Name Name Core Core -- ! &L{a b} = v body
  -- | Set                         -- Set
  -- | All Core Core               -- ∀A.B
  -- | Lam Name Core               -- λx(F)
  -- | App Core Core               -- (f x)
  -- | Adt Name [Core]             -- #Typ{a b ...}
  -- | Ctr Name [Core]             -- #Ctr{a b ...}
  -- | U32                         -- U32
  -- | W32 Word32                  -- 123
  -- | Chr Char                    -- 'a'
  -- | Op2 Oper Core Core          -- (+ a b)
  -- | Let LetT Name Core Core     -- ! x = v body
  -- | Mat MatT Core [Move] [Case] -- ~ v !moves { cases }
  -- deriving (Eq)

-- NEW TYPE:

data Core
  = Var Name                    -- x
  | Ref Name FnID [Core]        -- @fun(a,b...)
  | Let LetT Name Core Core     -- !x=v;f
  | Era                         -- *
  | Sup Lab Core Core           -- &L{a,b}
  | Dup Lab Name Name Core Core -- !&L{a,b}=v;f
  | Set                         -- Set
  | Emp                         -- ⊥
  | Efq Core [Move]             -- ~x!ms{}
  | Uni                         -- ⊤
  | Nil                         -- ()
  | Use Core [Move] Core        -- ~x!ms{():f}
  | U32                         -- U32
  | W32 Word32                  -- 12345
  | Swi Core [Move] Core Core   -- ~x!ms{0:z;+:s}
  | Op2 Oper Core Core          -- (+ a b)
  | Sig Core Core               -- ΣA.B
  | Tup Core Core               -- (a,b)
  | Get Core [Move] Core        -- ~x!ms{(,):f}
  | All Core Core               -- ∀A.B
  | Lam Name Core               -- λx.F
  | App Core Core               -- (f x)
  | Ann Bool Core Core          -- <x:T>
  deriving (Eq)

-- The changes include:
-- - Addition of Type-Formers, like Emp, All, Sig, etc.
-- - Addition of empty: Emp/Efq
-- - Addition of unit: Uni/Nil/Use
-- - Addition of pairs: Sig/Tup/Get (behaves like a 0-label Sup/Dup)
-- - Removal of ADT/CTR, in favor of more primitive types
-- - Removal of CHR (which was just another W32)
-- - Removal of the generic MAT, in favor of specific pattern-matches:
-- - - Efq: for the Empty type
-- - - Use: for the Unit type
-- - - Swi: for the U32 type
-- - - Get: for the Sigma type
-- - For simplicity, now, SWI is always ~x{0:z;+:s} (no multi-number switch)
-- - FWD has been removed (it was unused)
-- **Our goal is to update the whole codebase to reflect this change.**
-- 
-- INSTRUCTIONS:
-- 
-- When asked to fill below a commented-out code, you must rewrite it completely, updating it to comply to the changes above.
-- Remove discarded cases (like CTR), keep old cases (like Lam/App) verbatin (important: don't change existing definitions!), include new/missing cases (like Tup).
-- Preserve original comments and everything else. Avoid loss of information.
-- 
-- When asked to implement a missing interaction, reason about it longer, to make sure you get it right.
-- For example, the missing DUP-ALL interaction is:
-- !&L{x0,x1}=∀A.B
-- ----------------- DUP-ALL
-- !&L{A0,A1}=A
-- !&L{B0,B1}=B
-- &L{∀A0.B0,∀A1.B1}
-- Because All doesn't bind a variable.
-- Getting these right demands reasoning.
-- 
-- NOTES:
-- 
-- The following terms bind variables:
-- - `λx.f`: a lambda binds 'x' in its body, 'f'
-- - `!x=v;f`; a let binds 'x' in its body, 'f'
-- The following terms DO NOT bind variables:
-- - `~x{}`
-- - `~x{():f}`
-- - `~x{(,):f}`
-- - `~x{0:z;+:s}`
-- - `ΣA.B`
-- - `∀A.B`
-- Instead, we use lambdas *inside* them. For example:
-- @id  = λx.~x{0:0;+:λp.(+ 1 @id(p))}
-- @fst = λx.~x{(,):λa.λb.a}

-- Below is the complete list of new elims/intros/types:
-- Eliminators:
-- - APP
-- - USE
-- - GET
-- - SWI
-- - DUP
-- - OPX
-- - OPY
-- Introducers:
-- - ERA
-- - SUP
-- - NIL
-- - W32
-- - TUP
-- - LAM
-- Type-Formers:
-- - SET
-- - EMP
-- - UNI
-- - U32
-- - SIG
-- - ALL

-- STYLE GUIDE:
-- - Always order cases in the SAME order as they were defined on the Core type.
-- - As much as possible, favor SINGLE-LETTER field names, or TWO-LETTER field names (on list-like fields), inspired by the letters used in the comments on the Core type.
-- - For example, instead of `format (Use moves body) = ...`, write `format (Use ms b) = ...`
-- - Since Haskell doesn't accept uppercase variable names, prepend an underscore. Example: `format (All _A _B) = ...`.
-- - Do NOT use the ' (apostrophe) character in variable names. Prefer underscores. Example: `a_` instead of `a'`
-- - In general, attempt to mimic the original coding style as close as possible.
-- - KEEP COMMENTS, ERROR HANDLERS, ETC. FROM THE ORIGINAL CODE - DON'T LOSE INFORMATION

data Oper
  = OP_ADD | OP_SUB | OP_MUL | OP_DIV
  | OP_MOD | OP_EQ  | OP_NE  | OP_LT
  | OP_GT  | OP_LTE | OP_GTE | OP_AND
  | OP_OR  | OP_XOR | OP_LSH | OP_RSH
  deriving (Eq, Enum)

-- A top-level function, including:
-- - copy: true when ref-copy mode is enabled
-- - args: a list of (isArgStrict, argName) pairs
-- - core: the function's body
-- Note: ref-copy improves C speed, but increases interaction count
type Func = ((Bool, [(Bool,String)]), Core)


-- Set of labels in a function's body
type HasLab = (MS.Map Lab ())

-- data Book = Book
  -- { fidToFun :: MS.Map Word16 Func   -- func id to Func object
  -- , fidToLab :: MS.Map Word16 HasLab -- func id to dup labels used
  -- , fidToNam :: MS.Map Word16 Name   -- func id to name
  -- , namToFid :: MS.Map Name   Word16 -- func name to id
  -- , cidToAri :: MS.Map Word16 Word16 -- ctor id to field count (arity)
  -- , cidToLen :: MS.Map Word16 Word16 -- ctor id to cases length (ADT ctors)
  -- , cidToCtr :: MS.Map Word16 Name   -- ctor id to name
  -- , ctrToCid :: MS.Map Name   Word16 -- ctor name to id
  -- , cidToADT :: MS.Map Word16 Word16 -- ctor id to ADT id (first ADT cid)
  -- , freshLab :: Lab                  -- auto dup label counter
  -- } deriving (Show, Eq)

data Book = Book
  { fidToFun :: MS.Map FnID Func   -- func id to Func object
  , fidToLab :: MS.Map FnID HasLab -- func id to dup labels used
  , fidToNam :: MS.Map FnID Name   -- func id to name
  , namToFid :: MS.Map Name FnID   -- func name to id
  , freshLab :: Lab                -- auto dup label counter
  } deriving (Show, Eq)

-- Runtime Types
-- -------------

type HVM = IO

-- Constants
-- ---------

-- -- Tags
-- _DP0_ = 0x00 :: Tag
-- _DP1_ = 0x01 :: Tag
-- _VAR_ = 0x02 :: Tag
-- _FWD_ = 0x03 :: Tag
-- _REF_ = 0x04 :: Tag
-- _LET_ = 0x05 :: Tag
-- _APP_ = 0x06 :: Tag
-- _MAT_ = 0x08 :: Tag
-- _IFL_ = 0x09 :: Tag
-- _SWI_ = 0x0A :: Tag
-- _OPX_ = 0x0B :: Tag
-- _OPY_ = 0x0C :: Tag
-- _ERA_ = 0x0D :: Tag
-- _LAM_ = 0x0E :: Tag
-- _SUP_ = 0x0F :: Tag
-- _CTR_ = 0x10 :: Tag
-- _W32_ = 0x11 :: Tag
-- _CHR_ = 0x12 :: Tag

-- Tags
_DP0_ = 0x00 :: Tag
_DP1_ = 0x01 :: Tag
_VAR_ = 0x02 :: Tag
_REF_ = 0x03 :: Tag
_LET_ = 0x04 :: Tag
_ERA_ = 0x05 :: Tag
_SUP_ = 0x06 :: Tag
_SET_ = 0x08 :: Tag
_EMP_ = 0x09 :: Tag
_EFQ_ = 0x0A :: Tag
_UNI_ = 0x0B :: Tag
_NIL_ = 0x0C :: Tag
_USE_ = 0x0D :: Tag
_U32_ = 0x0E :: Tag
_W32_ = 0x0F :: Tag
_SWI_ = 0x10 :: Tag
_OPX_ = 0x11 :: Tag
_OPY_ = 0x12 :: Tag
_SIG_ = 0x13 :: Tag
_TUP_ = 0x14 :: Tag
_GET_ = 0x15 :: Tag
_ALL_ = 0x16 :: Tag
_LAM_ = 0x17 :: Tag
_APP_ = 0x18 :: Tag
_ANN_ = 0x19 :: Tag
_VAL_ = 0x1A :: Tag

-- Let Types
modeT :: Lab -> LetT
modeT 0x00 = LAZY
modeT 0x01 = STRI
modeT mode = error $ "unknown mode: " ++ show mode

-- Primitive Functions
_DUP_F_ = 0xFFFF :: Lab
_SUP_F_ = 0xFFFE :: Lab
_LOG_F_ = 0xFFFD :: Lab

primitives :: [(String, Word16)]
primitives =
  [ ("SUP", fromIntegral _SUP_F_)
  , ("DUP", fromIntegral _DUP_F_)
  , ("LOG", fromIntegral _LOG_F_)
  ]

-- Utils
-- -----

-- Getter function for maps
mget :: (Ord k, Show k) => MS.Map k a -> k -> a
mget map key =
  case MS.lookup key map of
    Just val -> val
    Nothing  -> error $ "key not found: " ++ show key

funArity :: Book -> Word16 -> Word16
funArity book fid
  | fid == fromIntegral _SUP_F_ = 3
  | fid == fromIntegral _DUP_F_ = 3
  | fid == fromIntegral _LOG_F_ = 1
  | otherwise = case MS.lookup fid (fidToFun book) of
      Just ((_, args), _) ->
        fromIntegral (length args)
      Nothing ->
        error $ "Function ID not found: " ++ show fid

-- Stringification
-- ---------------

padLeft :: String -> Int -> Char -> String
padLeft str n c = replicate (n - length str) c ++ str

showHex :: Word64 -> String
showHex x = showIntAtBase 16 intToDigit (fromIntegral x) ""

showName :: Int -> String
showName n = go (n + 1) "" where
  go n ac | n == 0    = ac
          | otherwise = go q (chr (ord 'a' + r) : ac)
          where (q,r) = quotRem (n - 1) 26

-- showTag :: Tag -> String
-- showTag tag
  -- | tag == _DP0_ = "DP0"
  -- | tag == _DP1_ = "DP1"
  -- | tag == _VAR_ = "VAR"
  -- | tag == _FWD_ = "FWD"
  -- | tag == _REF_ = "REF"
  -- | tag == _LET_ = "LET"
  -- | tag == _APP_ = "APP"
  -- | tag == _MAT_ = "MAT"
  -- | tag == _IFL_ = "IFL"
  -- | tag == _SWI_ = "SWI"
  -- | tag == _OPX_ = "OPX"
  -- | tag == _OPY_ = "OPY"
  -- | tag == _ERA_ = "ERA"
  -- | tag == _LAM_ = "LAM"
  -- | tag == _SUP_ = "SUP"
  -- | tag == _CTR_ = "CTR"
  -- | tag == _W32_ = "W32"
  -- | tag == _CHR_ = "CHR"
  -- | otherwise    = error $ "unknown tag: " ++ show tag

showTag :: Tag -> String
showTag tag
  | tag == _DP0_ = "DP0"
  | tag == _DP1_ = "DP1"
  | tag == _VAR_ = "VAR"
  | tag == _REF_ = "REF"
  | tag == _LET_ = "LET"
  | tag == _ERA_ = "ERA"
  | tag == _SUP_ = "SUP"
  | tag == _SET_ = "SET"
  | tag == _EMP_ = "EMP"
  | tag == _EFQ_ = "EFQ"
  | tag == _UNI_ = "UNI"
  | tag == _NIL_ = "NIL"
  | tag == _USE_ = "USE"
  | tag == _U32_ = "U32"
  | tag == _W32_ = "W32"
  | tag == _SWI_ = "SWI"
  | tag == _OPX_ = "OPX"
  | tag == _OPY_ = "OPY"
  | tag == _SIG_ = "SIG"
  | tag == _TUP_ = "TUP"
  | tag == _GET_ = "GET"
  | tag == _ALL_ = "ALL"
  | tag == _LAM_ = "LAM"
  | tag == _APP_ = "APP"
  | tag == _ANN_ = "ANN"
  | tag == _VAL_ = "VAL"
  | otherwise    = error $ "unknown tag: " ++ show tag

showLab :: Lab -> String
showLab lab = padLeft (showHex (fromIntegral lab)) 6 '0'

showLoc :: Loc -> String
showLoc loc = padLeft (showHex (fromIntegral loc)) 8 '0'

instance Show Oper where
  show OP_ADD = "+"
  show OP_SUB = "-"
  show OP_MUL = "*"
  show OP_DIV = "/"
  show OP_MOD = "%"
  show OP_EQ  = "=="
  show OP_NE  = "!="
  show OP_LT  = "<"
  show OP_GT  = ">"
  show OP_LTE = "<="
  show OP_GTE = ">="
  show OP_AND = "&"
  show OP_OR  = "|"
  show OP_XOR = "^"
  show OP_LSH = "<<"
  show OP_RSH = ">>"

instance Show LetT where
  show LAZY = ""
  show STRI = "."

showCore :: Core -> String
showCore = format
  where
    format :: Core -> String
    format (Var k) = k
    format (Ref k i xs) =
      let xs' = intercalate " " (map showCore xs) in
      concat ["@", k, "(", xs', ")"]
    format (Let m k v f) =
      let v' = showCore v in
      let f' = showCore f in
      if k == "" then
        concat [v', "\n", f']
      else
        concat ["! ", show m, k, " = ", v', "\n", f']
    format Era = "*"
    format (Sup l a b) =
      let a' = showCore a in
      let b' = showCore b in
      concat ["&", show l, "{", a', ",", b', "}"]
    format (Dup l x y v f) =
      let v' = showCore v in
      let f' = showCore f in
      concat ["! &", show l, "{", x, ",", y, "} = ", v', "\n", f']
    format Set = "Set"
    format Emp = "⊥"
    format (Efq c ms) =
      let c' = showCore c in
      let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
      concat ["~", c', ms', "{}"]
    format Uni = "⊤"
    format Nil = "()"
    format (Use c ms b) =
      let c' = showCore c in
      let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
      let b' = showCore b in
      concat ["~", c', ms', "{():", b', "}"]
    format U32 = "U32"
    format (W32 v) = show v
    format (Swi c ms z s) =
      let c' = showCore c in
      let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
      let z' = showCore z in
      let s' = showCore s in
      concat ["~", c', ms', "{0:", z', ";+:", s', "}"]
    format (Op2 o a b) =
      let a' = showCore a in
      let b' = showCore b in
      concat ["(", show o, " ", a', " ", b', ")"]
    format (Sig _A _B) =
      let a' = showCore _A in
      let b' = showCore _B in
      concat ["Σ", a', ".", b']
    format (Tup a b) =
      let a' = showCore a in
      let b' = showCore b in
      concat ["(", a', ",", b', ")"]
    format (Get c ms b) =
      let c' = showCore c in
      let ms' = concatMap (\(k,v) -> concat [" !", k, "=", showCore v]) ms in
      let b' = showCore b in
      concat ["~", c', ms', "{(,):", b', "}"]
    format (All _A _B) =
      let a' = showCore _A in
      let b' = showCore _B in
      concat ["∀", a', ".", b']
    format (Lam x f) =
      let f' = showCore f in
      concat ["λ", x, ".", f']
    format (App f x) =
      let f' = showCore f in
      let x' = showCore x in
      concat ["(", f', " ", x', ")"]
    format (Ann c x t) =
      let x' = showCore x in
      let t' = showCore t in
      concat ["<", x', " : ", t', ">"]

renamer :: IORef (MS.Map String String) -> Core -> IO Core
renamer names core = case core of
  Var k -> do
    k' <- genName names k
    return $ Var k'
  Ref k i xs -> do
    xs' <- mapM (renamer names) xs
    return $ Ref k i xs'
  Let m k v f -> do
    k' <- genName names k
    v' <- renamer names v
    f' <- renamer names f
    return $ Let m k' v' f'
  Era -> 
    return Era
  Sup l a b -> do
    a' <- renamer names a
    b' <- renamer names b
    return $ Sup l a' b'
  Dup l x y v f -> do
    x' <- genName names x
    y' <- genName names y
    v' <- renamer names v
    f' <- renamer names f
    return $ Dup l x' y' v' f'
  Set -> 
    return Set
  Emp -> 
    return Emp
  Efq c ms -> do
    c' <- renamer names c
    ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
    return $ Efq c' ms'
  Uni -> 
    return Uni
  Nil -> 
    return Nil
  Use c ms b -> do
    c' <- renamer names c
    ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
    b' <- renamer names b
    return $ Use c' ms' b'
  U32 -> 
    return U32
  W32 v -> 
    return $ W32 v
  Swi c ms z s -> do
    c' <- renamer names c
    ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
    z' <- renamer names z
    s' <- renamer names s
    return $ Swi c' ms' z' s'
  Op2 o a b -> do
    a' <- renamer names a
    b' <- renamer names b
    return $ Op2 o a' b'
  Sig _A _B -> do
    _A' <- renamer names _A
    _B' <- renamer names _B
    return $ Sig _A' _B'
  Tup a b -> do
    a' <- renamer names a
    b' <- renamer names b
    return $ Tup a' b'
  Get c ms b -> do
    c' <- renamer names c
    ms' <- forM ms $ \(k,v) -> do v' <- renamer names v; return (k,v')
    b' <- renamer names b
    return $ Get c' ms' b'
  All _A _B -> do
    _A' <- renamer names _A
    _B' <- renamer names _B
    return $ All _A' _B'
  Lam x f -> do
    x' <- genName names x
    f' <- renamer names f
    return $ Lam x' f'
  App f x -> do
    f' <- renamer names f
    x' <- renamer names x
    return $ App f' x'
  Ann c x t -> do
    x' <- renamer names x
    t' <- renamer names t
    return $ Ann c x' t'

rename :: Core -> Core
rename core = unsafePerformIO $ do
  names <- newIORef MS.empty
  renamer names core

genName :: IORef (MS.Map String String) -> String -> IO String
genName names name =
  atomicModifyIORef' names $ \map ->
    case MS.lookup name map of
      Just val -> (map, val)
      Nothing  ->
        let new  = showName (MS.size map)
            map' = MS.insert name new map
        in (map', new)

instance Show Core where
  show = showCore . rename

-- COMPLETE INTERACTION TABLE (updated)

-- @foo(a,b...)
-- ----------------- REF
-- book[foo](a,b...)

-- Let:

-- ! x = v ; f
-- ----------- LET
-- x <- v
-- f

-- (* a)
-- ----- APP-ERA
-- *

-- (λx.f a)
-- -------- APP-LAM
-- x <- a
-- f

-- (&L{f0,f1} a)
-- ------------------- APP-SUP
-- ! &L{a0,a1} = a;
-- &L{(f0 x0),(f1 x1)}

-- (() a)
-- ------ APP-NIL
-- error

-- ((f0,f1) a)
-- ----------- APP-TUP
-- error

-- (123 a)
-- ------- APP-W32
-- error

-- (T a)
-- ----- APP-TYP
-- error

-- ~*{():f}
-- -------- USE-ERA
-- *

-- ~&L{a,b}{():f}
-- ----------------------- USE-SUP
-- ! &L{f0,f1} = f;
-- &L{~a{():f0},~b{():f1}}

-- ~λx.g{():f}
-- ----------- USE-LAM
-- error

-- ~(){():f}
-- --------- USE-NIL
-- f

-- ~(p,q){():f}
-- ------------ USE-TUP
-- error

-- ~123{():f}
-- ---------- USE-W32
-- error

-- ~T{():f}
-- -------- USE-TYP
-- error

-- ~*{(,):f}
-- --------- GET-ERA
-- *

-- ~&L{a,b}{(,): f}
-- ------------------------- GET-SUP
-- ! &L{f0,f1} = f;
-- &L{~a{(,):f0},~b{(,):f1}}

-- ~(){(,):f}
-- ---------- GET-NIL
-- error

-- ~(a,b){(,):f}
-- ------------- GET-TUP
-- (f a b)

-- ~λx.g{(,):f}
-- ------------ GET-LAM
-- error

-- ~123{(,):f}
-- ----------- GET-W32
-- error

-- ~TYP{(,):f}
-- ----------- GET-TYP
-- error

-- ~*{0:z;+:s}
-- ----------- SWI-ERA
-- *

-- ~&L{a,b}{0:z;+:s}
-- ------------------------------- SWI-SUP
-- ! &L{z0,z1} = z;
-- ! &L{s0,s1} = s;
-- &L{~a{0:z0;+:s0},~b{0:z1;+:s1}}

-- ~(){0:z;+:s}
-- ------------ SWI-NIL
-- error

-- ~(a,b){0:z;+:s}
-- --------------- SWI-TUP
-- error

-- ~λx.g{0:z;+:s}
-- -------------- SWI-LAM
-- error

-- ~n{0:z;+:s}
-- ----------- SWI-W32
-- if n = 0:
--   z
-- else:
--   (s (n-1))

-- ~T{0:z;+:s}
-- ----------- SWI-TYP
-- error

-- ! &L{r,s} = *
-- ------------- DUP-ERA
-- r <- *
-- s <- *

-- ! &L{x,y} = &L{a,b}
-- ------------------- DUP-SUP
-- x <- a
-- y <- b

-- ! &L{r,s} = λx.f
-- ---------------- DUP-LAM
-- r <- λx0.f0
-- s <- λx1.f1
-- x <- &L{x0,x1}
-- ! &L{f0,f1} = f

-- ! &L{x,y} = ()
-- -------------- DUP-NIL
-- x <- ()
-- y <- ()

-- ! &L{x,y} = (a,b)
-- ----------------- DUP-TUP
-- ! &L{a0,a1} = a
-- ! &L{b0,b1} = b
-- x <- &L{a0,b0}
-- y <- &L{a1,b1}

-- ! &L{x,y} = 123
-- --------------- DUP-W32
-- x <- 123
-- y <- 123

-- ! &L{x,y} = Set
-- --------------- DUP-SET
-- x <- Set
-- y <- Set

-- ! &L{x,y} = ⊥
-- ------------- DUP-EMP
-- x <- ⊥
-- y <- ⊥

-- ! &L{x,y} = ⊤
-- ------------- DUP-UNI
-- x <- ⊤
-- y <- ⊤

-- ! &L{x,y} = U32
-- -------------- DUP-U32
-- x <- U32
-- y <- U32

-- ! &L{x,y} = ΣA.B
-- ----------------- DUP-SIG
-- ! &L{A0,A1} = A
-- ! &L{B0,B1} = B
-- x <- ΣA0.B0
-- y <- ΣA1.B1

-- ! &L{x,y} = ∀A.B
-- ----------------- DUP-ALL
-- ! &L{A0,A1} = A
-- ! &L{B0,B1} = B
-- x <- ∀A0.B0
-- y <- ∀A1.B1

-- (<op * y)
-- --------- OPX-ERA
-- *

-- (<op λx.f y)
-- ----------- OPX-LAM
-- error

-- (<op &L{a,b} y)
-- ------------------------- OPX-SUP
-- ! &L{y0,y1} = y;
-- &L{(<op a y0),(<op b y1)}

-- (<op () y)
-- ---------- OPX-NIL
-- error

-- (<op (x0,x1) y)
-- --------------- OPX-TUP
-- error

-- (<op x y)
-- --------- OPX-W32
-- (>op y x)

-- (<op T y)
-- --------- OPX-TYP
-- error

-- (>op x *)
-- --------- OPY-ERA
-- *

-- (>op x λy.f)
-- ------------ OPY-LAM
-- error

-- (>op x &L{y0,y1})
-- ----------------------- OPY-SUP
-- &L{>op(x y0),>op(x y1)}

-- (>op x ())
-- ---------- OPY-NIL
-- error

-- (>op x (y0,y1))
-- --------------- OPY-TUP
-- error

-- (>op x y)
-- --------- OPY-W32
-- x <op> y

-- (>op x T)
-- --------- OPY-TYP
-- error

-- ! &L{x,y} = @foo(a,b...)
-- ------------------------ DUP-REF-COPY (when &L not in @foo)
-- ! &L{a0,a1} = a
-- ! &L{b0,b1} = b
-- ...
-- x <- @foo(a0,b0...)
-- y <- @foo(a1,b1...)

-- @foo(&L{ax,ay},b,c...)
-- ---------------------- REF-SUP-COPY (when @L not in @foo)
-- ! &L{bx,by} = b
-- ! &L{cx,by} = c
-- ...
-- &L{@foo(ax,bx,cx...),@foo(ay,by,cy,...)}


{-./Type.hs-}

module Inject where

import Control.Monad (foldM, when, forM_)
import Control.Monad.State
import Data.Bits (shiftL, (.|.))
import Data.Char (ord)
import Data.List (foldr)
import Data.Word
import Debug.Trace
import Foreign
import Type
import qualified Data.Map.Strict as MS

type InjectM a = StateT InjectState HVM a

data InjectState = InjectState
  { args :: MS.Map String Term -- maps var names to binder locations
  , vars :: [(String, Loc)]    -- list of (var name, usage location) pairs
  }

emptyState :: InjectState
emptyState = InjectState MS.empty []

-- injectCore :: Book -> Core -> Loc -> InjectM ()

-- injectCore _ Era loc = do
  -- lift $ set loc (termNew _ERA_ 0 0)

-- injectCore _ (Var nam) loc = do
  -- argsMap <- gets args
  -- case MS.lookup nam argsMap of
    -- Just term -> do
      -- lift $ set loc term
      -- when (head nam /= '&') $ do
        -- modify $ \s -> s { args = MS.delete nam (args s) }
    -- Nothing -> do
      -- modify $ \s -> s { vars = (nam, loc) : vars s }

-- injectCore book (Let mod nam val bod) loc = do
  -- let_node <- lift $ allocNode 2
  -- modify $ \s -> s { args = MS.insert nam (termNew _VAR_ 0 (let_node + 0)) (args s) }
  -- injectCore book val (let_node + 0)
  -- injectCore book bod (let_node + 1)
  -- lift $ set loc (termNew _LET_ (fromIntegral $ fromEnum mod) let_node)

-- injectCore book (Lam vr0 bod) loc = do
  -- lam <- lift $ allocNode 1
  -- modify $ \s -> s { args = MS.insert vr0 (termNew _VAR_ 0 (lam + 0)) (args s) }
  -- injectCore book bod (lam + 0)
  -- lift $ set loc (termNew _LAM_ 0 lam)

-- injectCore book (App fun arg) loc = do
  -- app <- lift $ allocNode 2
  -- injectCore book fun (app + 0)
  -- injectCore book arg (app + 1)
  -- lift $ set loc (termNew _APP_ 0 app)

-- injectCore book (Sup lab tm0 tm1) loc = do
  -- sup <- lift $ allocNode 2
  -- injectCore book tm0 (sup + 0)
  -- injectCore book tm1 (sup + 1)
  -- lift $ set loc (termNew _SUP_ lab sup)

-- injectCore book (Dup lab dp0 dp1 val bod) loc = do
  -- dup <- lift $ allocNode 1
  -- modify $ \s -> s 
    -- { args = MS.insert dp0 (termNew _DP0_ lab dup) 
           -- $ MS.insert dp1 (termNew _DP1_ lab dup) (args s) 
    -- }
  -- injectCore book val (dup + 0)
  -- injectCore book bod loc

-- injectCore book (Ref nam fid arg) loc = do
  -- let ari = funArity book fid
  -- let lab = fromIntegral fid
  -- when (ari /= fromIntegral (length arg)) $ do
    -- error $ "Arity mismatch on term: " ++ show (Ref nam fid arg) ++ ". Expected " ++ show ari ++ ", got " ++ show (length arg) ++ "."
  -- ref <- lift $ allocNode (fromIntegral ari)
  -- sequence_ [injectCore book x (ref + i) | (i,x) <- zip [0..] arg]
  -- lift $ set loc (termNew _REF_ lab ref)

-- injectCore book (Ctr nam fds) loc = do
  -- let ari = length fds
  -- let cid = mget (ctrToCid book) nam
  -- let lab = fromIntegral cid
  -- ctr <- lift $ allocNode (fromIntegral ari)
  -- sequence_ [injectCore book fd (ctr + ix) | (ix,fd) <- zip [0..] fds]
  -- lift $ set loc (termNew _CTR_ lab ctr)

-- injectCore book tm@(Mat kin val mov css) loc = do
  -- mat <- lift $ allocNode (1 + fromIntegral (length css))
  -- injectCore book val (mat + 0)
  -- forM_ (zip [0..] css) $ \ (idx, (ctr, fds, bod)) -> do
    -- injectCore book (foldr (\x b -> Lam x b) (foldr (\x b -> Lam x b) bod (map fst mov)) fds) (mat + 1 + fromIntegral idx)
  -- let tag = case kin of { SWI -> _SWI_ ; (MAT _) -> _MAT_ ; (IFL _) -> _IFL_ }
  -- let lab = case kin of { SWI -> fromIntegral $ length css ; (MAT cid) -> fromIntegral cid ; (IFL cid) -> fromIntegral cid }
  -- trm <- return $ termNew tag lab mat
  -- ret <- foldM (\mat (_, val) -> do
      -- app <- lift $ allocNode 2
      -- lift $ set (app + 0) mat
      -- injectCore book val (app + 1)
      -- return $ termNew _APP_ 0 app)
    -- trm
    -- mov
  -- lift $ set loc ret

-- injectCore book (W32 val) loc = do
  -- lift $ set loc (termNew _W32_ 0 (fromIntegral val))

-- injectCore book (Chr val) loc = do
  -- lift $ set loc (termNew _CHR_ 0 (fromIntegral $ ord val))

-- injectCore book (Op2 opr nm0 nm1) loc = do
  -- opx <- lift $ allocNode 2
  -- injectCore book nm0 (opx + 0)
  -- injectCore book nm1 (opx + 1)
  -- lift $ set loc (termNew _OPX_ (fromIntegral $ fromEnum opr) opx)

-- injectCore _ Set loc = do
  -- lift $ set loc (termNew _SET_ 0 0)

-- injectCore book (All typ bod) loc = do
  -- all_node <- lift $ allocNode 2
  -- injectCore book typ (all_node + 0)
  -- injectCore book bod (all_node + 1)
  -- lift $ set loc (termNew _ALL_ 0 all_node)

-- injectCore book (Adt nam fds) loc = do
  -- let ari = length fds
  -- let cid = mget (ctrToCid book) nam
  -- let lab = fromIntegral cid
  -- adt <- lift $ allocNode (fromIntegral ari)
  -- sequence_ [injectCore book fd (adt + ix) | (ix,fd) <- zip [0..] fds]
  -- lift $ set loc (termNew _ADT_ lab adt)

-- injectCore _ U32 loc = do
  -- lift $ set loc (termNew _W32_ 0 0)

-- doInjectCoreAt :: Book -> Core -> Loc -> [(String,Term)] -> HVM Term
-- doInjectCoreAt book core host argList = do
  -- (_, state) <- runStateT (injectCore book core host) (emptyState { args = MS.fromList argList })
  -- foldM (\m (name, loc) -> do
    -- case MS.lookup name (args state) of
      -- Just term -> do
        -- set loc term
        -- return $ MS.delete name m
      -- Nothing -> do
        -- error $ "Unbound variable: \n\x1b[2m" ++ name ++ "\n\x1b[0mIn term:\n\x1b[2m" ++ Data.List.take 1024 (show core) ++ "...\x1b[0m")
    -- (args state)
    -- (vars state)
  -- got host

-- UPDATED:

injectCore :: Book -> Core -> Loc -> InjectM ()

injectCore _ Era loc = do
  lift $ set loc (termNew _ERA_ 0 0)

injectCore _ (Var x) loc = do
  argsMap <- gets args
  case MS.lookup x argsMap of
    Just term -> do
      lift $ set loc term
      when (head x /= '&') $ do
        modify $ \s -> s { args = MS.delete x (args s) }
    Nothing -> do
      modify $ \s -> s { vars = (x, loc) : vars s }

injectCore book (Ref x i xs) loc = do
  let ari = funArity book i
  let lab = fromIntegral i
  when (ari /= fromIntegral (length xs)) $ do
    error $ "Arity mismatch on term: " ++ show (Ref x i xs) ++ ". Expected " ++ show ari ++ ", got " ++ show (length xs) ++ "."
  ref <- lift $ allocNode (fromIntegral ari)
  sequence_ [injectCore book x (ref + i) | (i,x) <- zip [0..] xs]
  lift $ set loc (termNew _REF_ lab ref)

injectCore book (Let m x v f) loc = do
  let_node <- lift $ allocNode 2
  modify $ \s -> s { args = MS.insert x (termNew _VAR_ 0 (let_node + 0)) (args s) }
  injectCore book v (let_node + 0)
  injectCore book f (let_node + 1)
  lift $ set loc (termNew _LET_ (fromIntegral $ fromEnum m) let_node)

injectCore _ Era loc = do
  lift $ set loc (termNew _ERA_ 0 0)

injectCore book (Sup l a b) loc = do
  sup <- lift $ allocNode 2
  injectCore book a (sup + 0)
  injectCore book b (sup + 1)
  lift $ set loc (termNew _SUP_ l sup)

injectCore book (Dup l x y v f) loc = do
  dup <- lift $ allocNode 1
  modify $ \s -> s 
    { args = MS.insert x (termNew _DP0_ l dup) 
           $ MS.insert y (termNew _DP1_ l dup) (args s) 
    }
  injectCore book v (dup + 0)
  injectCore book f loc

injectCore _ Set loc = do
  lift $ set loc (termNew _SET_ 0 0)

injectCore _ Emp loc = do
  lift $ set loc (termNew _EMP_ 0 0)

injectCore book (Efq c ms) loc = do
  efq <- lift $ allocNode 1
  injectCore book c (efq + 0)
  applyMoves book (termNew _EFQ_ 0 efq) ms loc

injectCore _ Uni loc = do
  lift $ set loc (termNew _UNI_ 0 0)

injectCore _ Nil loc = do
  lift $ set loc (termNew _NIL_ 0 0)

injectCore book (Use c ms b) loc = do
  use <- lift $ allocNode 2
  injectCore book c (use + 0)
  injectCore book b (use + 1)
  applyMoves book (termNew _USE_ 0 use) ms loc

injectCore _ U32 loc = do
  lift $ set loc (termNew _U32_ 0 0)

injectCore _ (W32 n) loc = do
  lift $ set loc (termNew _W32_ 0 (fromIntegral n))

injectCore book (Swi c ms z s) loc = do
  swi <- lift $ allocNode 3
  injectCore book c (swi + 0)
  injectCore book z (swi + 1)
  injectCore book s (swi + 2)
  applyMoves book (termNew _SWI_ 0 swi) ms loc

injectCore book (Op2 o a b) loc = do
  opx <- lift $ allocNode 2
  injectCore book a (opx + 0)
  injectCore book b (opx + 1)
  lift $ set loc (termNew _OPX_ (fromIntegral $ fromEnum o) opx)

injectCore book (Sig _A _B) loc = do
  sig <- lift $ allocNode 2
  injectCore book _A (sig + 0)
  injectCore book _B (sig + 1)
  lift $ set loc (termNew _SIG_ 0 sig)

injectCore book (Tup a b) loc = do
  tup <- lift $ allocNode 2
  injectCore book a (tup + 0)
  injectCore book b (tup + 1)
  lift $ set loc (termNew _TUP_ 0 tup)

injectCore book (Get c ms b) loc = do
  get <- lift $ allocNode 2
  injectCore book c (get + 0)
  injectCore book b (get + 1)
  applyMoves book (termNew _GET_ 0 get) ms loc

injectCore book (All _A _B) loc = do
  all_node <- lift $ allocNode 2
  injectCore book _A (all_node + 0)
  injectCore book _B (all_node + 1)
  lift $ set loc (termNew _ALL_ 0 all_node)

injectCore book (Lam x f) loc = do
  lam <- lift $ allocNode 1
  modify $ \s -> s { args = MS.insert x (termNew _VAR_ 0 (lam + 0)) (args s) }
  injectCore book f (lam + 0)
  lift $ set loc (termNew _LAM_ 0 lam)

injectCore book (App f x) loc = do
  app <- lift $ allocNode 2
  injectCore book f (app + 0)
  injectCore book x (app + 1)
  lift $ set loc (termNew _APP_ 0 app)

injectCore book (Ann c x t) loc = do
  ann <- lift $ allocNode 2
  injectCore book x (ann + 0)
  injectCore book t (ann + 1)
  lift $ set loc (termNew _ANN_ (if c then 1 else 0) ann)

applyMoves :: Book -> Term -> [Move] -> Loc -> InjectM ()
applyMoves book base ms loc = do
  result <- foldM (\term (_, v) -> do
      app <- lift $ allocNode 2
      lift $ set (app + 0) term
      injectCore book v (app + 1)
      return $ termNew _APP_ 0 app)
    base
    ms
  lift $ set loc result

doInjectCoreAt :: Book -> Core -> Loc -> [(String,Term)] -> HVM Term
doInjectCoreAt book core host argList = do
  (_, state) <- runStateT (injectCore book core host) (emptyState { args = MS.fromList argList })
  _ <- foldM (\m (name, loc) -> do
    case MS.lookup name m of
      Just term -> do
        set loc term
        return $ MS.delete name m
      Nothing -> do
        error $ "Unbound variable: \n\x1b[2m" ++ name ++ "\n\x1b[0mIn term:\n\x1b[2m" ++ Prelude.take 1024 (show core) ++ "...\x1b[0m")
    (args state)
    (vars state)
  got host

{-./Type.hs-}
{-./Foreign.hs-}

-- module Reduce where

-- import Control.Monad (when, forM, forM_)
-- import Data.Word
-- import Collapse
-- import Extract
-- import Foreign
-- import Inject
-- import Type
-- import System.Exit
-- import qualified Data.Map.Strict as MS

-- reduceAt :: Bool -> (Book -> Loc -> HVM Term)

-- reduceAt debug book host = do 
  -- term <- got host
  -- let tag = termTag term
  -- let lab = termLab term
  -- let loc = termLoc term

  -- when debug $ do
    -- root <- doExtractCoreAt gotT book 0
    -- core <- doExtractCoreAt gotT book host
    -- putStrLn $ "reduce: " ++ showTerm term
    -- -- putStrLn $ "---------------- CORE: "
    -- -- putStrLn $ showCore core
    -- putStrLn $ "---------------- ROOT: "
    -- putStrLn $ showCore (doLiftDups root)

  -- case tag of
    -- t | t == _LET_ -> do
      -- case modeT lab of
        -- LAZY -> do
          -- val <- got (loc + 0)
          -- cont host (reduceLet term val)
        -- STRI -> do
          -- val <- reduceAt debug book (loc + 0)
          -- cont host (reduceLet term val)

    -- t | t == _APP_ -> do
      -- fun <- reduceAt debug book (loc + 0)
      -- case termTag fun of
        -- t | t == _ERA_ -> cont host (reduceAppEra term fun)
        -- t | t == _LAM_ -> cont host (reduceAppLam term fun)
        -- t | t == _SUP_ -> cont host (reduceAppSup term fun)
        -- t | t == _CTR_ -> cont host (reduceAppCtr term fun)
        -- t | t == _W32_ -> cont host (reduceAppW32 term fun)
        -- t | t == _CHR_ -> cont host (reduceAppW32 term fun)
        -- _   -> set (loc + 0) fun >> return term

    -- t | t == _MAT_ -> do
      -- val <- reduceAt debug book (loc + 0)
      -- case termTag val of
        -- t | t == _ERA_ -> cont host (reduceMatEra term val)
        -- t | t == _LAM_ -> cont host (reduceMatLam term val)
        -- t | t == _SUP_ -> cont host (reduceMatSup term val)
        -- t | t == _CTR_ -> cont host (reduceMatCtr term val)
        -- t | t == _W32_ -> cont host (reduceMatW32 term val)
        -- t | t == _CHR_ -> cont host (reduceMatW32 term val)
        -- _   -> set (loc + 0) val >> return term

    -- t | t == _IFL_ -> do
      -- val <- reduceAt debug book (loc + 0)
      -- case termTag val of
        -- t | t == _ERA_ -> cont host (reduceMatEra term val)
        -- t | t == _LAM_ -> cont host (reduceMatLam term val)
        -- t | t == _SUP_ -> cont host (reduceMatSup term val)
        -- t | t == _CTR_ -> cont host (reduceMatCtr term val)
        -- t | t == _W32_ -> cont host (reduceMatW32 term val)
        -- t | t == _CHR_ -> cont host (reduceMatW32 term val)
        -- _   -> set (loc + 0) val >> return term

    -- t | t == _SWI_ -> do
      -- val <- reduceAt debug book (loc + 0)
      -- case termTag val of
        -- t | t == _ERA_ -> cont host (reduceMatEra term val)
        -- t | t == _LAM_ -> cont host (reduceMatLam term val)
        -- t | t == _SUP_ -> cont host (reduceMatSup term val)
        -- t | t == _CTR_ -> cont host (reduceMatCtr term val)
        -- t | t == _W32_ -> cont host (reduceMatW32 term val)
        -- t | t == _CHR_ -> cont host (reduceMatW32 term val)
        -- _   -> set (loc + 0) val >> return term

    -- t | t == _OPX_ -> do
      -- val <- reduceAt debug book (loc + 0)
      -- case termTag val of
        -- t | t == _ERA_ -> cont host (reduceOpxEra term val)
        -- t | t == _LAM_ -> cont host (reduceOpxLam term val)
        -- t | t == _SUP_ -> cont host (reduceOpxSup term val)
        -- t | t == _CTR_ -> cont host (reduceOpxCtr term val)
        -- t | t == _W32_ -> cont host (reduceOpxW32 term val)
        -- t | t == _CHR_ -> cont host (reduceOpxW32 term val)
        -- _   -> set (loc + 0) val >> return term

    -- t | t == _OPY_ -> do
      -- val <- reduceAt debug book (loc + 0)
      -- case termTag val of
        -- t | t == _ERA_ -> cont host (reduceOpyEra term val)
        -- t | t == _LAM_ -> cont host (reduceOpyLam term val)
        -- t | t == _SUP_ -> cont host (reduceOpySup term val)
        -- t | t == _CTR_ -> cont host (reduceOpyCtr term val)
        -- t | t == _W32_ -> cont host (reduceOpyW32 term val)
        -- t | t == _CHR_ -> cont host (reduceOpyW32 term val)
        -- _ -> set (loc + 0) val >> return term

    -- t | t == _DP0_ -> do
      -- sb0 <- got (loc + 0)
      -- if termGetBit sb0 == 0
        -- then do
          -- val <- reduceAt debug book (loc + 0)
          -- case termTag val of
            -- t | t == _ERA_ -> cont host (reduceDupEra term val)
            -- t | t == _LAM_ -> cont host (reduceDupLam term val)
            -- t | t == _SUP_ -> cont host (reduceDupSup term val)
            -- t | t == _CTR_ -> cont host (reduceDupCtr term val)
            -- t | t == _W32_ -> cont host (reduceDupW32 term val)
            -- t | t == _CHR_ -> cont host (reduceDupW32 term val)
            -- _ -> set (loc + 0) val >> return term
        -- else do
          -- set host (termRemBit sb0)
          -- reduceAt debug book host

    -- t | t == _DP1_ -> do
      -- sb1 <- got (loc + 0)
      -- if termGetBit sb1 == 0
        -- then do
          -- val <- reduceAt debug book (loc + 0)
          -- case termTag val of
            -- t | t == _ERA_ -> cont host (reduceDupEra term val)
            -- t | t == _LAM_ -> cont host (reduceDupLam term val)
            -- t | t == _SUP_ -> cont host (reduceDupSup term val)
            -- t | t == _CTR_ -> cont host (reduceDupCtr term val)
            -- t | t == _W32_ -> cont host (reduceDupW32 term val)
            -- t | t == _CHR_ -> cont host (reduceDupW32 term val)
            -- _ -> set (loc + 0) val >> return term
        -- else do
          -- set host (termRemBit sb1)
          -- reduceAt debug book host

    -- t | t == _VAR_ -> do
      -- sub <- got (loc + 0)
      -- if termGetBit sub == 0
        -- then return term
        -- else do
          -- set host (termRemBit sub)
          -- reduceAt debug book host

    -- t | t == _REF_ -> do
      -- reduceRefAt book host
      -- reduceAt debug book host

    -- _ -> do
      -- return term

  -- where
    -- cont host action = do
      -- ret <- action
      -- set host ret
      -- reduceAt debug book host

-- gotT :: Book -> Loc -> HVM Term
-- gotT book host = got host

-- reduceRefAt :: Book -> Loc -> HVM Term
-- reduceRefAt book host = do
  -- term <- got host
  -- let lab = termLab term
  -- let loc = termLoc term
  -- let fid = fromIntegral lab
  -- let ari = funArity book fid
  -- case lab of
    -- x | x == _DUP_F_ -> reduceRefAt_DupF book host loc ari
    -- x | x == _SUP_F_ -> reduceRefAt_SupF book host loc ari
    -- x | x == _LOG_F_ -> reduceRefAt_LogF book host loc ari
    -- otherwise -> case MS.lookup fid (fidToFun book) of
      -- Just ((copy, args), core) -> do
        -- incItr
        -- when (length args /= fromIntegral ari) $ do
          -- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@" ++ mget (fidToNam book) fid ++ "'."
          -- exitFailure
        -- argTerms <- if ari == 0
          -- then return []
          -- else forM (zip [0..] args) $ \(i, (strict, _)) -> do
            -- term <- got (loc + i)
            -- if strict
              -- then reduceAt False book (loc + i)
              -- else return term
        -- doInjectCoreAt book core host $ zip (map snd args) argTerms
      -- Nothing -> do
        -- putStrLn $ "RUNTIME_ERROR: Function ID " ++ show fid ++ " not found in fidToFun book."
        -- exitFailure

-- -- Primitive: Dynamic Dup `@DUP(lab val λdp0λdp1(bod))`
-- reduceRefAt_DupF :: Book -> Loc -> Loc -> Word16 -> HVM Term  
-- reduceRefAt_DupF book host loc ari = do
  -- incItr
  -- when (ari /= 3) $ do
    -- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@DUP'."
    -- exitFailure
  -- lab <- reduceAt False book (loc + 0)
  -- val <- got (loc + 1)
  -- bod <- got (loc + 2)
  -- dup <- allocNode 1
  -- case termTag lab of
    -- t | t == _W32_ -> do
      -- when (termLoc lab > 0xFFFFFF) $ do
        -- error "RUNTIME_ERROR: dynamic DUP label too large"
      -- -- Create the DUP node with value
      -- set (dup + 0) val
      -- -- Create first APP node for (APP bod DP0)
      -- app1 <- allocNode 2
      -- set (app1 + 0) bod
      -- set (app1 + 1) (termNew _DP0_ (termLoc lab) dup)
      -- -- Create second APP node for (APP (APP bod DP0) DP1)
      -- app2 <- allocNode 2
      -- set (app2 + 0) (termNew _APP_ 0 app1)
      -- set (app2 + 1) (termNew _DP1_ (termLoc lab) dup)
      -- let ret = termNew _APP_ 0 app2
      -- set host ret
      -- return ret
    -- _ -> do
      -- core <- doExtractCoreAt gotT book (loc + 0)
      -- putStrLn $ "RUNTIME_ERROR: dynamic DUP without numeric label: " ++ showTerm lab
      -- putStrLn $ showCore (doLiftDups core)
      -- exitFailure

-- -- Primitive: Dynamic Sup `@SUP(lab tm0 tm1)`
-- reduceRefAt_SupF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_SupF book host loc ari = do
  -- incItr
  -- when (ari /= 3) $ do
    -- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@SUP'."
    -- exitFailure
  -- lab <- reduceAt False book (loc + 0)
  -- tm0 <- got (loc + 1)
  -- tm1 <- got (loc + 2)
  -- sup <- allocNode 2
  -- case termTag lab of
    -- t | t == _W32_ -> do
      -- when (termLoc lab > 0xFFFFFF) $ do
        -- error "RUNTIME_ERROR: dynamic SUP label too large"
      -- let ret = termNew _SUP_ (termLoc lab) sup
      -- set (sup + 0) tm0
      -- set (sup + 1) tm1
      -- set host ret
      -- return ret
    -- _ -> error "RUNTIME_ERROR: dynamic SUP without numeric label."

-- -- Primitive: Logger `@LOG(msg)`
-- -- Will extract the term and log it. 
-- -- Returns 0.
-- reduceRefAt_LogF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_LogF book host loc ari = do
  -- incItr
  -- when (ari /= 1) $ do
    -- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@LOG'."
    -- exitFailure
  -- msg <- doExtractCoreAt gotT book (loc + 0)
  -- putStrLn $ showCore (doLiftDups msg)
  -- -- msgs <- doCollapseFlatAt gotT book (loc + 0)
  -- -- forM_ msgs $ \msg -> do
    -- -- putStrLn $ showCore msg
  -- let ret = termNew _W32_ 0 0
  -- set host ret
  -- return ret

-- -- Primitive: Fresh `@FRESH`
-- -- Returns a fresh dup label.
-- reduceRefAt_FreshF :: Book -> Loc -> Loc -> Word16 -> HVM Term
-- reduceRefAt_FreshF book host loc ari = do
  -- incItr
  -- when (ari /= 0) $ do
    -- putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@Fresh'."
    -- exitFailure
  -- num <- fromIntegral <$> fresh
  -- let ret = termNew _W32_ 0 num
  -- set host ret
  -- return ret

-- reduceCAt :: Bool -> (Book -> Loc -> HVM Term)
-- reduceCAt = \ _ _ host -> reduceAtC host

-- UPDATED:

module Reduce where

import Control.Monad (when, forM, forM_)
import Data.Word
import Collapse
import Extract
import Foreign
import Inject
import Type
import System.Exit
import qualified Data.Map.Strict as MS

reduceAt :: Bool -> Book -> Loc -> HVM Term

reduceAt debug book host = do 
  term <- got host
  let tag = termTag term
  let lab = termLab term
  let loc = termLoc term

  when debug $ do
    root <- doExtractCoreAt gotT book 0
    core <- doExtractCoreAt gotT book host
    putStrLn $ "reduce: " ++ showTerm term
    -- putStrLn $ "---------------- CORE: "
    -- putStrLn $ showCore core
    putStrLn $ "---------------- ROOT: "
    putStrLn $ showCore (doLiftDups root)

  case tag of
    t | t == _LET_ -> do
      case modeT lab of
        LAZY -> do
          val <- got (loc + 0)
          cont host (reduceLet term val)
        STRI -> do
          val <- reduceAt debug book (loc + 0)
          cont host (reduceLet term val)

    t | t == _APP_ -> do
      fun <- reduceAt debug book (loc + 0)
      case termTag fun of
        t | t == _ERA_ -> cont host (reduceAppEra term fun)
        t | t == _LAM_ -> cont host (reduceAppLam term fun)
        t | t == _SUP_ -> cont host (reduceAppSup term fun)
        t | t == _NIL_ -> cont host (reduceAppNil term fun)
        t | t == _TUP_ -> cont host (reduceAppTup term fun)
        t | t == _W32_ -> cont host (reduceAppW32 term fun)
        t | t == _SET_ -> cont host (reduceAppTyp term fun)
        t | t == _EMP_ -> cont host (reduceAppTyp term fun)
        t | t == _UNI_ -> cont host (reduceAppTyp term fun)
        t | t == _U32_ -> cont host (reduceAppTyp term fun)
        t | t == _SIG_ -> cont host (reduceAppTyp term fun)
        t | t == _ALL_ -> cont host (reduceAppTyp term fun)
        _   -> set (loc + 0) fun >> return term

    t | t == _USE_ -> do
      val <- reduceAt debug book (loc + 0)
      case termTag val of
        t | t == _ERA_ -> cont host (reduceUseEra term val)
        t | t == _SUP_ -> cont host (reduceUseSup term val)
        t | t == _LAM_ -> cont host (reduceUseLam term val)
        t | t == _NIL_ -> cont host (reduceUseNil term val)
        t | t == _TUP_ -> cont host (reduceUseTup term val)
        t | t == _W32_ -> cont host (reduceUseW32 term val)
        t | t == _SET_ -> cont host (reduceUseTyp term val)
        t | t == _EMP_ -> cont host (reduceUseTyp term val)
        t | t == _UNI_ -> cont host (reduceUseTyp term val)
        t | t == _U32_ -> cont host (reduceUseTyp term val)
        t | t == _SIG_ -> cont host (reduceUseTyp term val)
        t | t == _ALL_ -> cont host (reduceUseTyp term val)
        _   -> set (loc + 0) val >> return term

    t | t == _GET_ -> do
      val <- reduceAt debug book (loc + 0)
      case termTag val of
        t | t == _ERA_ -> cont host (reduceGetEra term val)
        t | t == _SUP_ -> cont host (reduceGetSup term val)
        t | t == _NIL_ -> cont host (reduceGetNil term val)
        t | t == _TUP_ -> cont host (reduceGetTup term val)
        t | t == _LAM_ -> cont host (reduceGetLam term val)
        t | t == _W32_ -> cont host (reduceGetW32 term val)
        t | t == _SET_ -> cont host (reduceGetTyp term val)
        t | t == _EMP_ -> cont host (reduceGetTyp term val)
        t | t == _UNI_ -> cont host (reduceGetTyp term val)
        t | t == _U32_ -> cont host (reduceGetTyp term val)
        t | t == _SIG_ -> cont host (reduceGetTyp term val)
        t | t == _ALL_ -> cont host (reduceGetTyp term val)
        _   -> set (loc + 0) val >> return term

    t | t == _SWI_ -> do
      val <- reduceAt debug book (loc + 0)
      case termTag val of
        t | t == _ERA_ -> cont host (reduceSwiEra term val)
        t | t == _SUP_ -> cont host (reduceSwiSup term val)
        t | t == _NIL_ -> cont host (reduceSwiNil term val)
        t | t == _TUP_ -> cont host (reduceSwiTup term val)
        t | t == _LAM_ -> cont host (reduceSwiLam term val)
        t | t == _W32_ -> cont host (reduceSwiW32 term val)
        t | t == _SET_ -> cont host (reduceSwiTyp term val)
        t | t == _EMP_ -> cont host (reduceSwiTyp term val)
        t | t == _UNI_ -> cont host (reduceSwiTyp term val)
        t | t == _U32_ -> cont host (reduceSwiTyp term val)
        t | t == _SIG_ -> cont host (reduceSwiTyp term val)
        t | t == _ALL_ -> cont host (reduceSwiTyp term val)
        _   -> set (loc + 0) val >> return term

    t | t == _OPX_ -> do
      val <- reduceAt debug book (loc + 0)
      case termTag val of
        t | t == _ERA_ -> cont host (reduceOpxEra term val)
        t | t == _LAM_ -> cont host (reduceOpxLam term val)
        t | t == _SUP_ -> cont host (reduceOpxSup term val)
        t | t == _NIL_ -> cont host (reduceOpxNil term val)
        t | t == _TUP_ -> cont host (reduceOpxTup term val)
        t | t == _W32_ -> cont host (reduceOpxW32 term val)
        t | t == _SET_ -> cont host (reduceOpxTyp term val)
        t | t == _EMP_ -> cont host (reduceOpxTyp term val)
        t | t == _UNI_ -> cont host (reduceOpxTyp term val)
        t | t == _U32_ -> cont host (reduceOpxTyp term val)
        t | t == _SIG_ -> cont host (reduceOpxTyp term val)
        t | t == _ALL_ -> cont host (reduceOpxTyp term val)
        _   -> set (loc + 0) val >> return term

    t | t == _OPY_ -> do
      val <- reduceAt debug book (loc + 0)
      case termTag val of
        t | t == _ERA_ -> cont host (reduceOpyEra term val)
        t | t == _LAM_ -> cont host (reduceOpyLam term val)
        t | t == _SUP_ -> cont host (reduceOpySup term val)
        t | t == _NIL_ -> cont host (reduceOpyNil term val)
        t | t == _TUP_ -> cont host (reduceOpyTup term val)
        t | t == _W32_ -> cont host (reduceOpyW32 term val)
        t | t == _SET_ -> cont host (reduceOpyTyp term val)
        t | t == _EMP_ -> cont host (reduceOpyTyp term val)
        t | t == _UNI_ -> cont host (reduceOpyTyp term val)
        t | t == _U32_ -> cont host (reduceOpyTyp term val)
        t | t == _SIG_ -> cont host (reduceOpyTyp term val)
        t | t == _ALL_ -> cont host (reduceOpyTyp term val)
        _ -> set (loc + 0) val >> return term

    t | t == _DP0_ -> do
      sb0 <- got (loc + 0)
      if termGetBit sb0 == 0
        then do
          val <- reduceAt debug book (loc + 0)
          case termTag val of
            t | t == _ERA_ -> cont host (reduceDupEra term val)
            t | t == _LAM_ -> cont host (reduceDupLam term val)
            t | t == _SUP_ -> cont host (reduceDupSup term val)
            t | t == _NIL_ -> cont host (reduceDupNil term val)
            t | t == _TUP_ -> cont host (reduceDupTup term val)
            t | t == _W32_ -> cont host (reduceDupW32 term val)
            t | t == _SET_ -> cont host (reduceDupSet term val)
            t | t == _EMP_ -> cont host (reduceDupEmp term val)
            t | t == _UNI_ -> cont host (reduceDupUni term val)
            t | t == _U32_ -> cont host (reduceDupU32 term val)
            t | t == _SIG_ -> cont host (reduceDupSig term val)
            t | t == _ALL_ -> cont host (reduceDupAll term val)
            _ -> set (loc + 0) val >> return term
        else do
          set host (termRemBit sb0)
          reduceAt debug book host

    t | t == _DP1_ -> do
      sb1 <- got (loc + 0)
      if termGetBit sb1 == 0
        then do
          val <- reduceAt debug book (loc + 0)
          case termTag val of
            t | t == _ERA_ -> cont host (reduceDupEra term val)
            t | t == _LAM_ -> cont host (reduceDupLam term val)
            t | t == _SUP_ -> cont host (reduceDupSup term val)
            t | t == _NIL_ -> cont host (reduceDupNil term val)
            t | t == _TUP_ -> cont host (reduceDupTup term val)
            t | t == _W32_ -> cont host (reduceDupW32 term val)
            t | t == _SET_ -> cont host (reduceDupSet term val)
            t | t == _EMP_ -> cont host (reduceDupEmp term val)
            t | t == _UNI_ -> cont host (reduceDupUni term val)
            t | t == _U32_ -> cont host (reduceDupU32 term val)
            t | t == _SIG_ -> cont host (reduceDupSig term val)
            t | t == _ALL_ -> cont host (reduceDupAll term val)
            _ -> set (loc + 0) val >> return term
        else do
          set host (termRemBit sb1)
          reduceAt debug book host

    t | t == _VAR_ -> do
      sub <- got (loc + 0)
      if termGetBit sub == 0
        then return term
        else do
          set host (termRemBit sub)
          reduceAt debug book host

    t | t == _REF_ -> do
      reduceRefAt book host
      reduceAt debug book host

    _ -> do
      return term

  where
    cont host action = do
      ret <- action
      set host ret
      reduceAt debug book host

gotT :: Book -> Loc -> HVM Term
gotT book host = got host

reduceRefAt :: Book -> Loc -> HVM Term
reduceRefAt book host = do
  term <- got host
  let lab = termLab term
  let loc = termLoc term
  let fid = fromIntegral lab
  let ari = funArity book fid
  case lab of
    x | x == _DUP_F_ -> reduceRefAt_DupF book host loc ari
    x | x == _SUP_F_ -> reduceRefAt_SupF book host loc ari
    x | x == _LOG_F_ -> reduceRefAt_LogF book host loc ari
    otherwise -> case MS.lookup fid (fidToFun book) of
      Just ((copy, args), core) -> do
        incItr
        when (length args /= fromIntegral ari) $ do
          putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@" ++ mget (fidToNam book) fid ++ "'."
          exitFailure
        argTerms <- if ari == 0
          then return []
          else forM (zip [0..] args) $ \(i, (strict, _)) -> do
            term <- got (loc + i)
            if strict
              then reduceAt False book (loc + i)
              else return term
        doInjectCoreAt book core host $ zip (map snd args) argTerms
      Nothing -> do
        putStrLn $ "RUNTIME_ERROR: Function ID " ++ show fid ++ " not found in fidToFun book."
        exitFailure

-- Primitive: Dynamic Dup `@DUP(lab val λdp0λdp1(bod))`
reduceRefAt_DupF :: Book -> Loc -> Loc -> Word16 -> HVM Term  
reduceRefAt_DupF book host loc ari = do
  incItr
  when (ari /= 3) $ do
    putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@DUP'."
    exitFailure
  lab <- reduceAt False book (loc + 0)
  val <- got (loc + 1)
  bod <- got (loc + 2)
  dup <- allocNode 1
  case termTag lab of
    t | t == _W32_ -> do
      when (termLoc lab > 0xFFFFFF) $ do
        error "RUNTIME_ERROR: dynamic DUP label too large"
      -- Create the DUP node with value
      set (dup + 0) val
      -- Create first APP node for (APP bod DP0)
      app1 <- allocNode 2
      set (app1 + 0) bod
      set (app1 + 1) (termNew _DP0_ (termLoc lab) dup)
      -- Create second APP node for (APP (APP bod DP0) DP1)
      app2 <- allocNode 2
      set (app2 + 0) (termNew _APP_ 0 app1)
      set (app2 + 1) (termNew _DP1_ (termLoc lab) dup)
      let ret = termNew _APP_ 0 app2
      set host ret
      return ret
    _ -> do
      core <- doExtractCoreAt gotT book (loc + 0)
      putStrLn $ "RUNTIME_ERROR: dynamic DUP without numeric label: " ++ showTerm lab
      putStrLn $ showCore (doLiftDups core)
      exitFailure

-- Primitive: Dynamic Sup `@SUP(lab tm0 tm1)`
reduceRefAt_SupF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_SupF book host loc ari = do
  incItr
  when (ari /= 3) $ do
    putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@SUP'."
    exitFailure
  lab <- reduceAt False book (loc + 0)
  tm0 <- got (loc + 1)
  tm1 <- got (loc + 2)
  sup <- allocNode 2
  case termTag lab of
    t | t == _W32_ -> do
      when (termLoc lab > 0xFFFFFF) $ do
        error "RUNTIME_ERROR: dynamic SUP label too large"
      let ret = termNew _SUP_ (termLoc lab) sup
      set (sup + 0) tm0
      set (sup + 1) tm1
      set host ret
      return ret
    _ -> error "RUNTIME_ERROR: dynamic SUP without numeric label."

-- Primitive: Logger `@LOG(msg)`
-- Will extract the term and log it. 
-- Returns 0.
reduceRefAt_LogF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_LogF book host loc ari = do
  incItr
  when (ari /= 1) $ do
    putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@LOG'."
    exitFailure
  msg <- doExtractCoreAt gotT book (loc + 0)
  putStrLn $ showCore (doLiftDups msg)
  -- msgs <- doCollapseFlatAt gotT book (loc + 0)
  -- forM_ msgs $ \msg -> do
    -- putStrLn $ showCore msg
  let ret = termNew _W32_ 0 0
  set host ret
  return ret

-- Primitive: Fresh `@FRESH`
-- Returns a fresh dup label.
reduceRefAt_FreshF :: Book -> Loc -> Loc -> Word16 -> HVM Term
reduceRefAt_FreshF book host loc ari = do
  incItr
  when (ari /= 0) $ do
    putStrLn $ "RUNTIME_ERROR: arity mismatch on call to '@Fresh'."
    exitFailure
  num <- fromIntegral <$> fresh
  let ret = termNew _W32_ 0 num
  set host ret
  return ret

reduceCAt :: Bool -> Book -> Loc -> HVM Term
reduceCAt = \ _ _ host -> reduceAtC host

reduce :: Bool -> Book -> Term -> HVM Term
reduce debug book term = do
  loc <- allocNode 1
  set loc term
  reduceAt debug book loc

{-./Type.hs-}
{-./Check.hs-}

-- [># LANGUAGE OverloadedStrings #<]
-- [># LANGUAGE TemplateHaskell #<]

-- module Main where

-- import Network.Socket as Network
-- import System.IO (hSetEncoding, utf8, hPutStrLn, stderr)
-- import Control.Exception (try, fromException, SomeException, finally, AsyncException(UserInterrupt))
-- import Control.Monad (guard, when, foldM, forM_, unless)
-- import Data.FileEmbed
-- import Data.List (partition, isPrefixOf, take, find)
-- import Data.Word
-- import Foreign.C.Types
-- import Foreign.LibFFI
-- import Foreign.LibFFI.Types
-- import GHC.Clock
-- import GHC.Conc
-- import Collapse
-- import Compile
-- import Extract
-- import Foreign
-- import Inject
-- import Parse
-- import Reduce
-- import Type
-- import System.Environment (getArgs)
-- import System.Exit (exitWith, ExitCode(ExitSuccess, ExitFailure))
-- import System.IO
-- import System.IO (readFile')
-- import System.IO.Unsafe (unsafePerformIO)
-- import System.IO.Error (tryIOError)
-- import System.Posix.DynamicLinker
-- import System.Process (callCommand)
-- import Text.Printf
-- import Data.IORef
-- import qualified Data.Map.Strict as MS
-- import Text.Read (readMaybe)

-- runtime_c :: String
-- runtime_c = $(embedStringFile "./src/Runtime.c")

-- -- Main
-- -- ----

-- data RunMode
  -- = Normalize
  -- | Collapse (Maybe Int)
  -- deriving Eq

-- main :: IO ()
-- main = do
  -- args <- getArgs
  -- result <- case args of
    -- ("run" : file : rest) -> do
      -- let (flags, sArgs) = partition ("-" `isPrefixOf`) rest
      -- let compiled       = "-c" `elem` flags
      -- let collapseFlag   = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
      -- let stats          = "-s" `elem` flags
      -- let debug          = "-d" `elem` flags
      -- let hideQuotes     = "-Q" `elem` flags
      -- let mode           = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
      -- cliRun file debug compiled mode stats hideQuotes sArgs
    -- ("serve" : file : rest) -> do
      -- let (flags, _)     = partition ("-" `isPrefixOf`) rest
      -- let compiled       = "-c" `elem` flags
      -- let collapseFlag   = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
      -- let stats          = "-s" `elem` flags
      -- let debug          = "-d" `elem` flags
      -- let hideQuotes     = "-Q" `elem` flags
      -- let mode           = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
      -- cliServe file debug compiled mode stats hideQuotes
    -- ["help"] -> printHelp
    -- _ -> printHelp
  -- case result of
    -- Left err -> do
      -- putStrLn err
      -- exitWith (ExitFailure 1)
    -- Right _ -> do
      -- exitWith ExitSuccess

-- parseCollapseFlag :: String -> Maybe (Maybe Int)
-- parseCollapseFlag ('-':'C':rest) = 
  -- case rest of
    -- "" -> Just Nothing
    -- n  -> Just (readMaybe n)
-- parseCollapseFlag _ = Nothing

-- printHelp :: IO (Either String ())
-- printHelp = do
  -- putStrLn "HVM usage:"
  -- putStrLn "  hvm help       # Shows this help message"
  -- putStrLn "  hvm run <file> [flags] [args...] # Evals main"
  -- putStrLn "  hvm serve <file> [flags] # Starts socket server on port 8080"
  -- putStrLn "    -c  # Runs with compiled mode (fast)"
  -- putStrLn "    -C  # Collapse the result to a list of λ-Terms"
  -- putStrLn "    -CN # Same as above, but show only first N results"
  -- putStrLn "    -s  # Show statistics"
  -- putStrLn "    -d  # Print execution steps (debug mode)"
  -- putStrLn "    -Q  # Hide quotes in output"
  -- return $ Right ()

-- -- CLI Commands
-- -- ------------

-- cliRun :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> [String] -> IO (Either String ())
-- cliRun filePath debug compiled mode showStats hideQuotes strArgs = do
  -- book <- loadBook filePath compiled
  -- -- Abort when main isn't present
  -- when (not $ MS.member "main" (namToFid book)) $ do
    -- putStrLn "Error: 'main' not found."
    -- exitWith (ExitFailure 1)
  -- -- Abort when wrong number of strArgs
  -- let ((_, mainArgs), _) = mget (fidToFun book) (mget (namToFid book) "main")
  -- when (length strArgs /= length mainArgs) $ do
    -- putStrLn $ "Error: 'main' expects " ++ show (length mainArgs)
              -- ++ " arguments, found " ++ show (length strArgs)
    -- exitWith (ExitFailure 1)
  -- -- Normalize main
  -- init <- getMonotonicTimeNSec
  -- root <- injectMain book strArgs
  -- rxAt <- if compiled
    -- then return (reduceCAt debug)
    -- else return (reduceAt debug)
  -- vals <- case mode of
    -- Collapse _ -> doCollapseFlatAt rxAt book 0
    -- Normalize -> do
      -- core <- doExtractCoreAt rxAt book 0
      -- return [(doLiftDups core)]
  -- -- Print results
  -- case mode of
    -- Collapse limit -> do
      -- lastItrs <- newIORef 0
      -- let limitedVals = maybe id Data.List.take limit vals
      -- forM_ limitedVals $ \ term -> do
        -- currItrs <- getItr
        -- prevItrs <- readIORef lastItrs
        -- let output = if hideQuotes then removeQuotes (show term) else show term
        -- printf "%s\n" output
        -- writeIORef lastItrs currItrs
      -- putStrLn ""
    -- Normalize -> do
      -- let output = if hideQuotes
                   -- then removeQuotes (show (head vals))
                   -- else show (head vals)
      -- putStrLn output
  -- -- Prints total time
  -- end <- getMonotonicTimeNSec
  -- -- Show stats
  -- when showStats $ do
    -- itrs <- getItr
    -- size <- getLen
    -- let time = fromIntegral (end - init) / (10^9) :: Double
    -- let mips = (fromIntegral itrs / 1000000.0) / time
    -- printf "WORK: %llu interactions\n" itrs
    -- printf "TIME: %.7f seconds\n" time
    -- printf "SIZE: %llu nodes\n" size
    -- printf "PERF: %.3f MIPS\n" mips
    -- return ()
  -- -- Finalize
  -- hvmFree
  -- return $ Right ()

-- cliServe :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> IO (Either String ())
-- cliServe filePath debug compiled mode showStats hideQuotes = do
  -- book <- loadBook filePath compiled
  -- -- Abort when main isn't present
  -- when (not $ MS.member "main" (namToFid book)) $ do
    -- putStrLn "Error: 'main' not found."
    -- exitWith (ExitFailure 1)
  -- putStrLn "HVM serve mode. Listening on port 8080."
  -- sock <- socket AF_INET Stream 0
  -- setSocketOption sock ReuseAddr 1
  -- Network.bind sock (SockAddrInet 8080 0)
  -- listen sock 5
  -- putStrLn "Server started. Listening on port 8080."
  -- serverLoop sock book `finally` do
    -- close sock
    -- hvmFree
    -- putStrLn "\nServer terminated."
  -- return $ Right ()
  -- where
    -- serverLoop sock book = do
      -- result <- try $ do
        -- (conn, _) <- accept sock
        -- h <- socketToHandle conn ReadWriteMode
        -- hSetBuffering h LineBuffering
        -- hSetEncoding h utf8
        -- input <- hGetLine h
        -- unless (input == "exit" || input == "quit") $ do
          -- oldSize <- getLen
          -- root <- injectMain book [input]
          -- rxAt <- if compiled then return (reduceCAt debug) else return (reduceAt debug)
          -- vals <- case mode of
            -- Collapse _ -> doCollapseFlatAt rxAt book 0
            -- Normalize -> do
              -- core <- doExtractCoreAt rxAt book 0
              -- return [doLiftDups core]
          -- let output = case mode of
                -- Collapse limit -> do
                  -- let limitedVals = maybe id Data.List.take limit vals
                  -- let outputs = map (\term -> if hideQuotes then removeQuotes (show term) else show term) limitedVals
                  -- unlines outputs
                -- Normalize -> do
                  -- let result = head vals
                  -- if hideQuotes then removeQuotes (show result) else show result
          -- hPutStrLn h output
          -- setLen oldSize
          -- when showStats $ do
            -- itrs <- getItr
            -- size <- getLen
            -- hPutStrLn h $ "WORK: " ++ show itrs ++ " interactions"
            -- hPutStrLn h $ "SIZE: " ++ show size ++ " nodes"
            -- setItr 0
        -- hClose h
      -- case result of
        -- Left e -> case fromException e of
          -- Just UserInterrupt -> return () -- Exit loop on Ctrl+C
          -- _ -> do
            -- hPutStrLn stderr $ "Connection error: " ++ show (e :: SomeException)
            -- serverLoop sock book
        -- Right _ -> serverLoop sock book


-- -- Load and initialize a book from a file
-- loadBook :: FilePath -> Bool -> IO Book
-- loadBook filePath compiled = do
  -- hvmInit
  -- code <- readFile' filePath
  -- book <- doParseBook filePath code

  -- forM_ (MS.toList (cidToAri book)) $ \ (cid, ari) -> do
    -- hvmSetCari cid (fromIntegral ari)
  -- forM_ (MS.toList (cidToLen book)) $ \ (cid, len) -> do
    -- hvmSetClen cid (fromIntegral len)
  -- forM_ (MS.toList (cidToADT book)) $ \ (cid, adt) -> do
    -- hvmSetCadt cid (fromIntegral adt)
  -- forM_ (MS.toList (fidToFun book)) $ \ (fid, ((_, args), _)) -> do
    -- hvmSetFari fid (fromIntegral $ length args)

  -- when compiled $ do
    -- let decls = compileHeaders book
    -- let funcs = map (\ (fid, _) -> compile book fid) (MS.toList (fidToFun book))
    -- let mainC = unlines $ [runtime_c] ++ [decls] ++ funcs ++ [genMain book]
    -- -- Try to use a cached .so file
    -- callCommand "mkdir -p .build"
    -- let fName = last $ words $ map (\c -> if c == '/' then ' ' else c) filePath
    -- let cPath = ".build/" ++ fName ++ ".c"
    -- let oPath = ".build/" ++ fName ++ ".so"

    -- oldCFile <- tryIOError (readFile' cPath)
    -- bookLib <- if oldCFile == Right mainC then do
      -- dlopen oPath [RTLD_NOW]
    -- else do
      -- writeFile cPath mainC
      -- callCommand $ "gcc -O2 -fPIC -shared " ++ cPath ++ " -o " ++ oPath
      -- dlopen oPath [RTLD_NOW]

    -- forM_ (MS.keys (fidToFun book)) $ \ fid -> do
      -- funPtr <- dlsym bookLib (mget (fidToNam book) fid ++ "_f")
      -- hvmDefine fid funPtr
    -- -- Link compiled state
    -- hvmGotState <- hvmGetState
    -- hvmSetState <- dlsym bookLib "hvm_set_state"
    -- callFFI hvmSetState retVoid [argPtr hvmGotState]
  -- return book

-- genMain :: Book -> String
-- genMain book =
  -- let mainFid = mget (namToFid book) "main"
      -- registerFuncs = unlines ["  hvm_define(" ++ show fid ++ ", " ++ mget (fidToNam book) fid ++ "_f);" | fid <- MS.keys (fidToFun book)]
  -- in unlines
    -- [ "int main() {"
    -- , "  hvm_init();"
    -- , registerFuncs
    -- , "  clock_t start = clock();"
    -- , "  Term root = term_new(REF, "++show mainFid++", 0);"
    -- , "  normal(root);"
    -- , "  double time = (double)(clock() - start) / CLOCKS_PER_SEC * 1000;"
    -- , "  printf(\"WORK: %\"PRIu64\" interactions\\n\", get_itr());"
    -- , "  printf(\"TIME: %.3fs seconds\\n\", time / 1000.0);"
    -- , "  printf(\"SIZE: %llu nodes\\n\", get_len());"
    -- , "  printf(\"PERF: %.3f MIPS\\n\", (get_itr() / 1000000.0) / (time / 1000.0));"
    -- , "  hvm_free();"
    -- , "  return 0;"
    -- , "}"
    -- ]

-- -- Parse arguments and create a term with the given function name
-- injectMain :: Book -> [String] -> IO Term
-- injectMain book args = do
  -- (book, parsedArgs) <- foldM (\(b, as) str -> do
                               -- (b', a) <- doParseArgument str b
                               -- return (b', a:as)) (book, []) args
  -- let fid = mget (namToFid book) "main"
  -- let main = Ref "main" fid (reverse parsedArgs)
  -- root <- doInjectCoreAt book main 0 []
  -- return root

-- removeQuotes :: String -> String
-- removeQuotes s = case s of
  -- '"':rest -> init rest  -- Remove first and last quote if present
  -- _        -> s          -- Otherwise return as-is

-- TASK: update Main.hs fully
-- COMPLETE UPDATED MAIN.HS:

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}

module Main where

import Network.Socket as Network
import System.IO (hSetEncoding, utf8, hPutStrLn, stderr)
import Control.Exception (try, fromException, SomeException, finally, AsyncException(UserInterrupt))
import Control.Monad (guard, when, foldM, forM_, unless)
import Data.FileEmbed
import Data.List (partition, isPrefixOf, take, find)
import Data.Word
import Foreign.C.Types
import Foreign.LibFFI
import Foreign.LibFFI.Types
import GHC.Clock
import GHC.Conc
import Check
import Collapse
import Compile
import Extract
import Foreign
import Inject
import Parse
import Reduce
import Type
import System.Environment (getArgs)
import System.Exit (exitWith, ExitCode(ExitSuccess, ExitFailure))
import System.IO
import System.IO (readFile')
import System.IO.Unsafe (unsafePerformIO)
import System.IO.Error (tryIOError)
import System.Posix.DynamicLinker
import System.Process (callCommand)
import Text.Printf
import Data.IORef
import qualified Data.Map.Strict as MS
import Text.Read (readMaybe)

runtime_c :: String
runtime_c = $(embedStringFile "./src/Runtime.c")

-- Main
-- ----

data RunMode
  = Normalize
  | Collapse (Maybe Int)
  deriving Eq

main :: IO ()
main = do
  args <- getArgs
  result <- case args of
    ("run" : file : rest) -> do
      let (flags, sArgs) = partition ("-" `isPrefixOf`) rest
      let compiled       = "-c" `elem` flags
      let collapseFlag   = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
      let stats          = "-s" `elem` flags
      let debug          = "-d" `elem` flags
      let hideQuotes     = "-Q" `elem` flags
      let mode           = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
      cliRun file debug compiled mode stats hideQuotes sArgs
    ("serve" : file : rest) -> do
      let (flags, _)     = partition ("-" `isPrefixOf`) rest
      let compiled       = "-c" `elem` flags
      let collapseFlag   = Data.List.find (isPrefixOf "-C") flags >>= parseCollapseFlag
      let stats          = "-s" `elem` flags
      let debug          = "-d" `elem` flags
      let hideQuotes     = "-Q" `elem` flags
      let mode           = case collapseFlag of { Just n -> Collapse n ; Nothing -> Normalize }
      cliServe file debug compiled mode stats hideQuotes
    ["help"] -> printHelp
    _ -> printHelp
  case result of
    Left err -> do
      putStrLn err
      exitWith (ExitFailure 1)
    Right _ -> do
      exitWith ExitSuccess

parseCollapseFlag :: String -> Maybe (Maybe Int)
parseCollapseFlag ('-':'C':rest) = 
  case rest of
    "" -> Just Nothing
    n  -> Just (readMaybe n)
parseCollapseFlag _ = Nothing

printHelp :: IO (Either String ())
printHelp = do
  putStrLn "HVM usage:"
  putStrLn "  hvm help       # Shows this help message"
  putStrLn "  hvm run <file> [flags] [args...] # Evals main"
  putStrLn "  hvm serve <file> [flags] # Starts socket server on port 8080"
  putStrLn "    -c  # Runs with compiled mode (fast)"
  putStrLn "    -C  # Collapse the result to a list of λ-Terms"
  putStrLn "    -CN # Same as above, but show only first N results"
  putStrLn "    -s  # Show statistics"
  putStrLn "    -d  # Print execution steps (debug mode)"
  putStrLn "    -Q  # Hide quotes in output"
  return $ Right ()

-- CLI Commands
-- ------------

cliRun :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> [String] -> IO (Either String ())
cliRun filePath debug compiled mode showStats hideQuotes strArgs = do
  book <- loadBook filePath compiled
  -- Abort when main isn't present
  when (not $ MS.member "main" (namToFid book)) $ do
    putStrLn "Error: 'main' not found."
    exitWith (ExitFailure 1)
  -- Abort when wrong number of strArgs
  let ((_, mainArgs), _) = mget (fidToFun book) (mget (namToFid book) "main")
  when (length strArgs /= length mainArgs) $ do
    putStrLn $ "Error: 'main' expects " ++ show (length mainArgs)
              ++ " arguments, found " ++ show (length strArgs)
    exitWith (ExitFailure 1)
  -- Normalize main
  init <- getMonotonicTimeNSec
  root <- injectMain book strArgs
  rxAt <- if compiled
    then return (reduceCAt debug)
    else return (reduceAt debug)
  vals <- case mode of
    Collapse _ -> doCollapseFlatAt rxAt book 0
    Normalize -> do
      core <- doExtractCoreAt rxAt book 0
      return [(doLiftDups core)]
  -- Print results
  case mode of
    Collapse limit -> do
      lastItrs <- newIORef 0
      let limitedVals = maybe id Data.List.take limit vals
      forM_ limitedVals $ \ term -> do
        currItrs <- getItr
        prevItrs <- readIORef lastItrs
        let output = if hideQuotes then removeQuotes (show term) else show term
        printf "%s\n" output
        writeIORef lastItrs currItrs
      putStrLn ""
    Normalize -> do
      let output = if hideQuotes
                   then removeQuotes (show (head vals))
                   else show (head vals)
      putStrLn output
  -- Type check all nullary functions with annotated bodies
  forM_ (MS.toList (fidToFun book)) $ \ (fid, ((_, args), body)) -> do
    when (null args) $ do
      case body of
        Ann _ term typ -> do
          printf "Checking @%s...\n" (mget (fidToNam book) fid)
          hFlush stdout
          -- Inject the term and type into fresh locations
          termLoc <- allocNode 1
          typeLoc <- allocNode 1
          termTerm <- doInjectCoreAt book term termLoc []
          typeTerm <- doInjectCoreAt book typ typeLoc []
          -- Run the type check and store in a fresh location
          result <- check 0 termTerm typeTerm
          resultLoc <- allocNode 1
          set resultLoc result
          -- Collapse and print the result
          collapsed <- doCollapseFlatAt rxAt book resultLoc
          -- use unicode check / X symbols
          if length collapsed > 0
            then putStrLn "✓"
            else putStrLn "✗"
        _ -> return ()
  -- Prints total time
  end <- getMonotonicTimeNSec
  -- Show stats
  when showStats $ do
    itrs <- getItr
    size <- getLen
    let time = fromIntegral (end - init) / (10^9) :: Double
    let mips = (fromIntegral itrs / 1000000.0) / time
    printf "WORK: %llu interactions\n" itrs
    printf "TIME: %.7f seconds\n" time
    printf "SIZE: %llu nodes\n" size
    printf "PERF: %.3f MIPS\n" mips
    return ()
  -- Finalize
  hvmFree
  return $ Right ()

cliServe :: FilePath -> Bool -> Bool -> RunMode -> Bool -> Bool -> IO (Either String ())
cliServe filePath debug compiled mode showStats hideQuotes = do
  book <- loadBook filePath compiled
  -- Abort when main isn't present
  when (not $ MS.member "main" (namToFid book)) $ do
    putStrLn "Error: 'main' not found."
    exitWith (ExitFailure 1)
  putStrLn "HVM serve mode. Listening on port 8080."
  sock <- socket AF_INET Stream 0
  setSocketOption sock ReuseAddr 1
  Network.bind sock (SockAddrInet 8080 0)
  listen sock 5
  putStrLn "Server started. Listening on port 8080."
  serverLoop sock book `finally` do
    close sock
    hvmFree
    putStrLn "\nServer terminated."
  return $ Right ()
  where
    serverLoop sock book = do
      result <- try $ do
        (conn, _) <- accept sock
        h <- socketToHandle conn ReadWriteMode
        hSetBuffering h LineBuffering
        hSetEncoding h utf8
        input <- hGetLine h
        unless (input == "exit" || input == "quit") $ do
          oldSize <- getLen
          root <- injectMain book [input]
          rxAt <- if compiled then return (reduceCAt debug) else return (reduceAt debug)
          vals <- case mode of
            Collapse _ -> doCollapseFlatAt rxAt book 0
            Normalize -> do
              core <- doExtractCoreAt rxAt book 0
              return [doLiftDups core]
          let output = case mode of
                Collapse limit -> do
                  let limitedVals = maybe id Data.List.take limit vals
                  let outputs = map (\term -> if hideQuotes then removeQuotes (show term) else show term) limitedVals
                  unlines outputs
                Normalize -> do
                  let result = head vals
                  if hideQuotes then removeQuotes (show result) else show result
          hPutStrLn h output
          setLen oldSize
          when showStats $ do
            itrs <- getItr
            size <- getLen
            hPutStrLn h $ "WORK: " ++ show itrs ++ " interactions"
            hPutStrLn h $ "SIZE: " ++ show size ++ " nodes"
            setItr 0
        hClose h
      case result of
        Left e -> case fromException e of
          Just UserInterrupt -> return () -- Exit loop on Ctrl+C
          _ -> do
            hPutStrLn stderr $ "Connection error: " ++ show (e :: SomeException)
            serverLoop sock book
        Right _ -> serverLoop sock book


-- Load and initialize a book from a file
loadBook :: FilePath -> Bool -> IO Book
loadBook filePath compiled = do
  hvmInit
  code <- readFile' filePath
  book <- doParseBook filePath code

  forM_ (MS.toList (fidToFun book)) $ \ (fid, ((_, args), _)) -> do
    hvmSetFari fid (fromIntegral $ length args)

  when compiled $ do
    let decls = compileHeaders book
    let funcs = map (\ (fid, _) -> compile book fid) (MS.toList (fidToFun book))
    let mainC = unlines $ [runtime_c] ++ [decls] ++ funcs ++ [genMain book]
    -- Try to use a cached .so file
    callCommand "mkdir -p .build"
    let fName = last $ words $ map (\c -> if c == '/' then ' ' else c) filePath
    let cPath = ".build/" ++ fName ++ ".c"
    let oPath = ".build/" ++ fName ++ ".so"

    oldCFile <- tryIOError (readFile' cPath)
    bookLib <- if oldCFile == Right mainC then do
      dlopen oPath [RTLD_NOW]
    else do
      writeFile cPath mainC
      callCommand $ "gcc -O2 -fPIC -shared " ++ cPath ++ " -o " ++ oPath
      dlopen oPath [RTLD_NOW]

    forM_ (MS.keys (fidToFun book)) $ \ fid -> do
      funPtr <- dlsym bookLib (mget (fidToNam book) fid ++ "_f")
      hvmDefine fid funPtr
    -- Link compiled state
    hvmGotState <- hvmGetState
    hvmSetState <- dlsym bookLib "hvm_set_state"
    callFFI hvmSetState retVoid [argPtr hvmGotState]
  return book

genMain :: Book -> String
genMain book =
  let mainFid = mget (namToFid book) "main"
      registerFuncs = unlines ["  hvm_define(" ++ show fid ++ ", " ++ mget (fidToNam book) fid ++ "_f);" | fid <- MS.keys (fidToFun book)]
  in unlines
    [ "int main() {"
    , "  hvm_init();"
    , registerFuncs
    , "  clock_t start = clock();"
    , "  Term root = term_new(REF, "++show mainFid++", 0);"
    , "  normal(root);"
    , "  double time = (double)(clock() - start) / CLOCKS_PER_SEC * 1000;"
    , "  printf(\"WORK: %\"PRIu64\" interactions\\n\", get_itr());"
    , "  printf(\"TIME: %.3fs seconds\\n\", time / 1000.0);"
    , "  printf(\"SIZE: %llu nodes\\n\", get_len());"
    , "  printf(\"PERF: %.3f MIPS\\n\", (get_itr() / 1000000.0) / (time / 1000.0));"
    , "  hvm_free();"
    , "  return 0;"
    , "}"
    ]

-- Parse arguments and create a term with the given function name
injectMain :: Book -> [String] -> IO Term
injectMain book args = do
  (book, parsedArgs) <- foldM (\(b, as) str -> do
                               (b', a) <- doParseArgument str b
                               return (b', a:as)) (book, []) args
  let fid = mget (namToFid book) "main"
  let main = Ref "main" fid (reverse parsedArgs)
  root <- doInjectCoreAt book main 0 []
  return root

removeQuotes :: String -> String
removeQuotes s = case s of
  '"':rest -> init rest  -- Remove first and last quote if present
  _        -> s          -- Otherwise return as-is




-- TASK: write below a complete bidirectional type checker, based on OldCheck
-- the types must be:
-- infer : Int → Term → IO (Result Term)
-- check : Int → Term → Term → IO (Result ())
-- make it a 1-to-1 correspondence to OldCheck

-- (omitted)

-- this is a good start, but:
-- - 1. the style of this file doesn't match the rest of the codebase. refactor its style completely.
-- - 2. many infer/check cases are missing. remember to consult the original OldCheck file to learn how each case should work. this file should remain a close correspondence to it.
-- rewrite the file again, addressing these issues:

-- (omitted)

-- the file above is better, but it still has some issues.
-- first: `termEqual` must be renamed to just `equal`

-- second: due to how superpositions work on HVM, we need to update the `equal`
-- function to handle SUPs, as follows:

-- &L{a0,a1} == b
-- ----------------------- EQUAL-SUP-VAL
-- ! &L{b0,b1} = b;
-- &L{a0 == a1 , b0 == b1}

-- a == &L{b0,b1}
-- ----------------------- EQUAL-VAL-SUP
-- ! &L{a0,a1} = a;
-- &L{a0 == a1 , b0 == b1}

-- Now, since EQL can now return a SUP, its return type can't be Bool anymore - it has to be Term.
-- As such, we will return `()` (One) when the terms are equal, and `*` (Era) otherwise.

-- Similarly, the infer and check functions must be updated:

-- infer d &L{x0,x1}
-- --------------------------- INFER-SUP
-- &L{infer d x0 , infer d x1}

-- check d &L{x0,x1} t
-- ------------------------------- CHECK-SUP-VAL
-- &L{check d x0 t , check d x1 t}

-- check d x &L{t0,t1}
-- ------------------------------- CHECK-SUP-VAL
-- &L{check d x t0 , check d x t1}

-- These interactions should be incorporated into equal, infer and check, directly.
-- That is, when a term is a SUP, we must return a SUP of both recursive calls.
-- Note that, since infer/equal can also return SUPs, their return can't be Result anymore.
-- Instead, their type will be:
-- infer :: Int -> Term -> IO Term
-- check :: Int -> Term -> Term -> IO Term
-- infer and check will simply return the type (when well-typed) or `*` (Era) otherwise.
-- check will either return `()` (One) (when well-typed), or `*` (Era) otherwise.
-- to report errors, we will just use a `print` (not an Error type)

-- Finally, since `equal` returns a Term rather than a Bool, we must also properly
-- match on its return, and dispatch SUP interactions accordingly. for better style,
-- create an auxiliary `validate` function that will do that part.

-- Also, note there is a logic error in your code.
-- The check function does NOT call whnf on the term, only on the goal.
-- Why did you invent that whnf call out of nowhere?
-- Double check the rest of the code to avoid errors like that.
-- Also, this style is terrible:
-- foo :: ...
-- foo ... x ... = do
--   x_nf <- whnf x
--   let xTag = tTag x_nf
--   case () of
--     _ | xTag == _XYZ_ -> ...
--
-- Instead, let's do it as follows:
-- 1. *BEFORE* calling foo, we take the whnf of the 
-- 2. Then, we write foo like:
-- foo :: ...
-- foo ... x ...
--   | tTag x == _XYZ = ...
--   | ...
--
-- use this style in ALL functions, including equal.
-- NEVER use case () again.

-- Also, the following style is terrible:
-- foo = pure Something
-- Instead, let's ALWAYS use a do block, like:
-- foo = do
--   pure Something

-- Also, in many cases, you're allocating nodes like:
-- sup <- allocNode 2
-- set (sup + 0) dp0
-- set (sup + 1) dp1
-- That is very repetitive and error prone. Instead, create a function:
-- makeNode TAG LAB [children]
-- And use it through your code.

-- Complete updated file:
-- (omitted)

-- this initial implementation is good. there is a problem, though.
-- it is NOT exactly aligned with the OldCheck file.
-- for example, on OldCheck, the LAM-ALL case is:
--    #LAM{f}: ~ goal !f {
--      #ALL{A B}:
--        ! &{A0 A1}=A
--        ~ @check((+ dep 1) (f #ANN{#VAR{dep} A0}) #APP{B #ANN{#VAR{dep} A1}}) {
--          #Done{_}: #Done{1}
--          #Fail{e}: #Fail{e}
--        }
--      goal: #Fail{#TypeMismatch{#LAM{f} #ALL{#VAR{0} #LAM{λx.#VAR{0}}} goal}}
--    }
-- yet, on this file, it is:
-- | tTag tm == _LAM_ && tTag goal == _ALL_ = do
--     bod <- field tm 0
--     aTy <- field goal 0
--     bTy <- field goal 1
--     var <- makeNode _VAR_ (fromIntegral dep) [eraT]
--     app <- makeNode _APP_ 0 [bTy, var]
--     bTy <- whnf app
--     bOk <- checkGo (dep+1) bod bTy
--     if tTag bOk == _ERA_ 
--       then pure eraT
--       else pure nilT
-- problems:
-- - 'tm' should be named 'term', since that's how it is on OldCheck 
-- - we should first match '_LAM_', then, inside it, match '_ALL_', preserving the OldCheck structure
-- - the body check must be `check (dep+1) (App f (Ann (Var dep) A0) ) (App B (Ann (Var dep) A1))`,
--   where `A0` and `A1` are cloned variables (with a fresh `DUP` node). instead, what you have is:
--   `check (dep+1) f (App B (Var dep))`, which is absolutely NOT the same.
-- - across the implementation, there are many instances like this one, where the new checker is not
--   a 1-to-1 correspondence with the old one, as it was supposed to be.
-- your goal is to rewrite Checker.hs again, from scratch, in order to address this issue.
-- make sure to consult OldCheck to learn how the infer/check functions should be structured.
-- remember that equal, both are already correct - no need to change them.
-- write the updated, complete Check.hs file below:

-- (omitted)

-- in the code above, you're using 'ann' more than once. this is NOT ALLOWED.
-- HVM is linear! instead, what you need to do is: use a DUP node to clone
-- 'a', and then make separate ANN's. again, notice how, on OldCheck, we do:
-- ! &{A0 A1}=A
-- this creates a DUP NODE that CLONES 'A' as 'A0' and 'A1'.
-- you're struggling very hard with linearity, so, please, reason about it.
-- then, write below the FIXED version of every defective case:

-- (omitted)

-- OK, this approach does look sensible. now, let's apply this idea to the
-- entire code, in the format we used previously. reimplement the entire file,
-- from scratch, to include the new logic. remember that you ALWAYS need to dup
-- a variable that you use more than once!
-- also, in your reimplementation, attempt to be more consistent with variable
-- names and alignment. for example, this is not fine:
-- lam <- makeNode _LAM_ 0 [setT]
-- allSet <- makeNode _ALL_ 0 [setT, lam]
-- because 'lam' and 'allSet' don't align.
-- now, proceed to rewrite the COMPLETE Check.hs file below:

-- also:
-- 1. for some reason, 'infer' and 'check' are NOT in the proposed structure.
-- infer has been written like:
-- infer dep term0 = do
--   term <- whnf term0
--   case tTag term of
--     t | t == _XYZ_ -> do
--       ...
-- while the correct structure is:
-- infer dep term0 = ... take whnf then call inferGo ...
-- ...
-- inferGo dep tm
--   | tTag tm == _XYZ_ = do
-- ...
-- the same is true for 'check'.
-- also, matching on SUP should NOT be separated from the other cases.
-- that makes absolutely no sense. do not do that.
-- complete, fixed file below:

-- (omitted)

-- ok, this looks great. now, review the code above and:
-- - 1. check if there is still any occurrence of a HVM-side Term being accidentally cloned in Haskell (i.e., by using its variable more than once)
-- - 2. review the code for bugs and issues in general

-- report below all your findings, in English:

-- • The helper dup2 is only creating the two DP-links; it never allocates the
  -- actual _DUP_ node that owns them, so the run-time sharing discipline is
  -- broken.

-- • dup2 always returns the fixed label 1 (getLabAuto is a stub).  Every call
  -- therefore re-uses the same label, violating the “fresh label per DUP”
  -- rule.

-- • In inferGo (_SIG_, _APP_) and checkGo (_SIG_), the argument a/x is used
  -- once before the call to dup2 and then twice inside the DP0/DP1 links,
  -- yielding three usages of the same linear value.  The DUP must be performed
  -- before the very first consumption, not afterwards.

-- • both and equalGo forward the term b (or a) to two recursive calls without
  -- duplicating it, so the same run-time pointer is consumed twice.

-- • In the _LAM_ ▸ _ALL_ rule we create two fresh variables (var0 / var1) but
  -- use the original type a three times (once for check, twice in ANN) after a
  -- single dup2; same linearity issue.

-- • Node construction for DP0/DP1 uses makeNode, but the tag set should be
  -- _VAR_ when exposing the binder to the body; DP0/DP1 must live only inside
  -- the DUP structure.

-- • Shadowing: in the _APP_ branch new bindings named “a” and “b” override the
  -- outer ones, which is confusing and error-prone.
  -- NOTE: no - this is actually fine and desirable. use shadowing whenever
  -- possible. avoid prefixing names with ' and similar symbols.

-- • getLabAuto is only a placeholder; without a real fresh-label mechanism the
  -- interpreter will emit duplicated labels and break reductions that depend
  -- on label uniqueness.
  -- let's fix this by importing the `book` in ALL functions (both, etc.)

-- • makeNode is used to create DP0 / DP1 links with a child list of length 1;
  -- but a DP-link is *not* an allocated node: it is supposed to be a leaf term
  -- (termNew tag lab loc=0).  Allocating memory for them wastes space.
  -- NOTE: that's correct. DUP nodes are allocated and store the duplicated term,
  -- but the DP0/DP1 terms are leaves.

-- • Several inference branches (_REF_, _USE_, _GET_, _SWI_, …) still return
  -- eraT after printing a message, whereas OldCheck propagated a #Fail
  -- containing a structured error; the new checker therefore loses error
  -- information.
  -- NOTE: that's okay for now

-- • equalGo / both treat NIL as the only One value.  They should also return a
  -- SUP-tree when either side is a SUP of Ones, exactly like the other rules.
  -- NOTE: what do you mean by that? I'm confused.

-- Fixing the points above requires:
  -- – Implementing a real fresh-label supply and wrapping DP0/DP1 inside a
    -- proper _DUP_ node.
  -- – Performing DUP *before* the first duplicated use.
  -- – Never forwarding the same Term to two different consumers without a DUP.
  -- – Removing the stray debugging prints or turning them into proper error
    -- nodes.
  -- – Cleaning up variable shadowing and always using fresh names.

-- TASK: rewrite Check.hs from scratch, again, in order to address these issues.
-- Complete refactored Check.hs file. Remember to increment the fresh label.
-- Write the complete, final version below:
-- COMPLETE CHECK.HS:

-- (omitted)

-- this is still wrong. note that on rules like:
-- | tTag a == _SUP_ = do
    -- a0 <- field a 0
    -- a1 <- field a 1
    -- -- Need to duplicate b because it's used twice
    -- (b0, b1) <- makeDup bookRef b
    -- r0 <- both bookRef a0 b0
    -- r1 <- both bookRef a1 b1
    -- makeNode _SUP_ (tLab a) [r0, r1]
-- we need to use the SAME label for the new dup, and the returned SUP.
-- reason about this and update the code to reflect this change verywhere it applies

-- (...)

-- I now believe that we should NOT use the freshLab field from the Book. in
-- fact, I removed it. we should still receive it so we can pass to reduce later
-- on. but, for now, let's instead use a global no-inline counter implemented
-- inside this file itself, for the fresh label generation.
-- final Check.hs:

module Check where

import Control.Monad (when)
import Data.IORef (IORef, readIORef, modifyIORef', newIORef)
import Data.Word
import System.IO.Unsafe (unsafePerformIO)

import Extract
import Foreign
import Reduce
import Type

-- Global counter for fresh labels
{-# NOINLINE freshLabelCounter #-}
freshLabelCounter :: IORef Lab
freshLabelCounter = unsafePerformIO $ newIORef 0xC00000

-- Constants

setT, empT, uniT, u32T, nilT, eraT :: Term
setT = termNew _SET_ 0 0
empT = termNew _EMP_ 0 0
uniT = termNew _UNI_ 0 0
u32T = termNew _U32_ 0 0
nilT = termNew _NIL_ 0 0
eraT = termNew _ERA_ 0 0

-- Runtime helpers

debug :: Term -> IO ()
debug term = do
  core <- toCore term
  putStr $ concatMap (\c -> if c == '\n' then "; " else [c]) $ show core

whnf :: Term -> IO Term
whnf = reduceC

field :: Term -> Int -> IO Term
field t i = do
  got (tLoc t + fromIntegral i)

-- | Allocates a node and fills its children, returning the parent Term.
--   If the list of children is empty we return a leaf term (loc = 0).
makeNode :: Tag -> Lab -> [Term] -> IO Term
makeNode tag lab cs
  | null cs = do
      pure (termNew tag lab 0)
  | otherwise = do
      ptr <- allocNode (fromIntegral (length cs))
      mapM_ (\ (i, c) -> set (ptr + fromIntegral i) c) (zip [0 ..] cs)
      pure (termNew tag lab ptr)
      
-- | Create a DUP node that holds the original term, and return two DP0/DP1 terms
--   with the specified label
makeDup :: Lab -> Term -> IO (Term, Term)
makeDup lab term = do
  -- Create a DUP node to hold the original term
  loc <- allocNode 1
  set loc term
  -- Create the DP0/DP1 terms (leaf terms with the shared label)
  let t0 = termNew _DP0_ lab 0
  let t1 = termNew _DP1_ lab 0
  -- Return the DP0/DP1 terms
  pure (t0, t1)

-- | Gets a fresh label and increments the counter
genFreshLabel :: IO Lab
genFreshLabel = do
  lab <- readIORef freshLabelCounter
  modifyIORef' freshLabelCounter (+1)
  pure lab

-- | Create a DUP node with a fresh label
makeDupFresh :: Term -> IO (Term, Term)
makeDupFresh term = do
  -- Get a fresh label
  freshLab <- genFreshLabel
  makeDup freshLab term

-- | Boolean 'and', but for One|Era.
both :: Term -> Term -> IO Term
both a b
  | tTag a == _SUP_ = do
      a0 <- field a 0
      a1 <- field a 1
      -- Use the SUP's label when duplicating b
      (b0, b1) <- makeDup (tLab a) b
      r0 <- both a0 b0
      r1 <- both a1 b1
      makeNode _SUP_ (tLab a) [r0, r1]
  | tTag b == _SUP_ = do
      b0 <- field b 0
      b1 <- field b 1
      -- Use the SUP's label when duplicating a
      (a0, a1) <- makeDup (tLab b) a
      r0 <- both a0 b0
      r1 <- both a1 b1
      makeNode _SUP_ (tLab b) [r0, r1]
  | tTag a == _NIL_ && tTag b == _NIL_ = do
      pure nilT
  | otherwise = do
      pure eraT

-- Structural equality - returns nilT for equal, eraT for not equal
equal :: Int -> Term -> Term -> IO Term
equal dep a0 b0 = do
  a <- whnf a0
  b <- whnf b0
  putStrLn $ "== " ++ showTerm a
  putStrLn $ ".. " ++ showTerm b
  if a == b 
    then pure nilT 
    else equalGo dep a b

equalGo :: Int -> Term -> Term -> IO Term
equalGo dep a b
  | tTag a == _SUP_ = do
      a0 <- field a 0
      a1 <- field a 1
      (b0, b1) <- makeDup (tLab a) b
      r0 <- equalGo dep a0 b0
      r1 <- equalGo dep a1 b1
      makeNode _SUP_ (tLab a) [r0, r1]
  | tTag b == _SUP_ = do
      b0 <- field b 0
      b1 <- field b 1
      (a0, a1) <- makeDup (tLab b) a
      r0 <- equalGo dep a0 b0
      r1 <- equalGo dep a1 b1
      makeNode _SUP_ (tLab b) [r0, r1]
  | tTag a == _ERA_ && tTag b == _ERA_ = do
      pure nilT
  | tTag a == _SET_ && tTag b == _SET_ = do
      pure nilT
  | tTag a == _EMP_ && tTag b == _EMP_ = do
      pure nilT
  | tTag a == _UNI_ && tTag b == _UNI_ = do
      pure nilT
  | tTag a == _NIL_ && tTag b == _NIL_ = do
      pure nilT
  | tTag a == _U32_ && tTag b == _U32_ = do
      pure nilT
  | tTag a == _W32_ && tTag b == _W32_ = do
      if tLab a == tLab b
        then pure nilT
        else pure eraT
  | tTag a == _SIG_ && tTag b == _SIG_ = do
      ax <- field a 0
      ay <- field a 1
      bx <- field b 0
      by <- field b 1
      rx <- equalGo dep ax bx
      ry <- equalGo dep ay by
      both rx ry
  | tTag a == _TUP_ && tTag b == _TUP_ = do
      ax <- field a 0
      ay <- field a 1
      bx <- field b 0
      by <- field b 1
      rx <- equalGo dep ax bx
      ry <- equalGo dep ay by
      both rx ry
  | tTag a == _ALL_ && tTag b == _ALL_ = do
      aa <- field a 0
      ab <- field a 1
      ba <- field b 0
      bb <- field b 1
      ra <- equalGo dep aa ba
      rb <- equalGo dep ab bb
      both ra rb
  | tTag a == _LAM_ && tTag b == _LAM_ = do
      var0 <- makeNode _W32_ (fromIntegral dep) []
      var1 <- makeNode _W32_ (fromIntegral dep) []
      aApp <- makeNode _APP_ 0 [a, var0]
      bApp <- makeNode _APP_ 0 [b, var1]
      aRes <- whnf aApp
      bRes <- whnf bApp
      equalGo (dep+1) aRes bRes
  | tTag a == _APP_ && tTag b == _APP_ = do
      af <- field a 0
      ax <- field a 1
      bf <- field b 0
      bx <- field b 1
      rf <- equalGo dep af bf
      rx <- equalGo dep ax bx
      both rf rx
  | tTag a == _ANN_ && tTag b == _ANN_ = do
      av <- field a 0
      at <- field a 1
      bv <- field b 0
      bt <- field b 1
      rv <- equalGo dep av bv
      rt <- equalGo dep at bt
      both rv rt
  | otherwise = do
      pure eraT

-- Inference
infer :: Int -> Term -> IO Term
infer dep term = do
  -- putStr "infer: " ; debug term ; putStrLn ""
  putStrLn $ "infer: " ++ showTerm term
  inferGo dep term

inferGo :: Int -> Term -> IO Term
inferGo dep term
  | tTag term == _SUP_ = do
      a <- field term 0
      b <- field term 1
      aType <- infer dep a
      bType <- infer dep b
      makeNode _SUP_ (tLab term) [aType, bType]
  | tTag term == _VAR_ = do
      sub <- got (termLoc term)
      if termGetBit sub == 0
        then do
          putStr "(cant-infer-var)"
          pure eraT
        else do
          infer dep (termRemBit sub)
  | tTag term == _REF_ = do
      putStr "(cant-infer-ref)"
      pure eraT
  | tTag term == _LET_ = do
      val <- field term 0
      bod <- field term 1
      valType <- infer dep val
      if tTag valType == _ERA_ 
        then pure eraT
        else infer (dep+1) bod
  | tTag term == _ERA_ = do
      pure setT
  | tTag term == _SET_ = do
      pure setT
  | tTag term == _EMP_ = do
      pure setT
  | tTag term == _EFQ_ = do
      x <- field term 0
      rc <- check dep x empT
      if tTag rc == _ERA_ 
        then pure eraT
        else do
          lamB <- makeNode _LAM_ 0 [empT]
          makeNode _ALL_ 0 [empT, lamB]
  | tTag term == _UNI_ = do
      pure setT
  | tTag term == _NIL_ = do
      pure uniT
  | tTag term == _USE_ = do
      putStr "(cant-infer-use)"
      pure eraT
  | tTag term == _U32_ = do
      pure setT
  | tTag term == _W32_ = do
      pure u32T
  | tTag term == _SWI_ = do
      putStr "(cant-infer-swi)"
      pure eraT
  | tTag term == _OPX_ || tTag term == _OPY_ = do
      putStr "(cant-infer-op)"
      pure eraT
  | tTag term == _SIG_ = do
      a <- field term 0
      b <- field term 1
      (a0, a1) <- makeDupFresh a
      aOk <- check dep a0 setT
      if tTag aOk == _ERA_ 
        then pure eraT
        else do
          lamT <- makeNode _LAM_ 0 [setT]
          allT <- makeNode _ALL_ 0 [a1, lamT]
          bOk <- check dep b allT
          if tTag bOk == _ERA_ 
            then pure eraT
            else pure setT
  | tTag term == _TUP_ = do
      a <- field term 0
      b <- field term 1
      aType <- infer dep a
      if tTag aType == _ERA_ 
        then pure eraT
        else do
          bType <- infer dep b
          if tTag bType == _ERA_ 
            then pure eraT
            else do
              lamB <- makeNode _LAM_ 0 [bType]
              makeNode _SIG_ 0 [aType, lamB]
  | tTag term == _GET_ = do
      putStr "(cant-infer-get)"
      pure eraT
  | tTag term == _ALL_ = do
      a <- field term 0
      b <- field term 1
      aOk <- check dep a setT
      if tTag aOk == _ERA_ 
        then pure eraT
        else do
          lamT <- makeNode _LAM_ 0 [setT]
          allT <- makeNode _ALL_ 0 [setT, lamT]
          bOk <- check dep b allT
          if tTag bOk == _ERA_ 
            then pure eraT
            else pure setT
  | tTag term == _LAM_ = do
      putStr "(cant-infer-lam)"
      pure eraT
  | tTag term == _APP_ = do
      f <- field term 0
      x <- field term 1
      (x0, x1) <- makeDupFresh x
      fType <- infer dep f
      if tTag fType == _ERA_ 
        then pure eraT
        else do
          fTypeNf <- whnf fType
          if tTag fTypeNf /= _ALL_ 
            then do
              putStr "(non-fun-app)"
              pure eraT
            else do
              a <- field fTypeNf 0
              b <- field fTypeNf 1
              xOk <- check dep x0 a
              if tTag xOk == _ERA_ 
                then pure eraT
                else do
                  app <- makeNode _APP_ 0 [b, x1]
                  whnf app
  | tTag term == _ANN_ = do
      if termLab term == 0
        then do -- already checked
          tm <- field term 0
          ty <- field term 1
          pure ty
        else do
          tm <- field term 0
          ty <- field term 1
          rc <- check dep tm ty
          if tTag rc == _ERA_ 
            then pure eraT
            else pure ty
  | otherwise = do
      putStr $ "(cant-infer-unknown)"
      pure eraT

-- Checking
check :: Int -> Term -> Term -> IO Term
check dep term goal0 = do
  goal <- whnf goal0
  -- putStr "check: " ; debug term ; putStr " :: " ; debug goal ; putStrLn ""
  putStrLn $ "check: " ++ showTerm term ++ " :: " ++ showTerm goal
  checkGo dep term goal

checkGo :: Int -> Term -> Term -> IO Term
checkGo dep term goal
  | tTag term == _SUP_ = do
      a <- field term 0
      b <- field term 1
      -- Use the SUP's label when duplicating goal
      (goal0, goal1) <- makeDup (tLab term) goal
      ra <- checkGo dep a goal0
      rb <- checkGo dep b goal1
      makeNode _SUP_ (tLab term) [ra, rb]
  | tTag goal == _SUP_ = do
      a <- field goal 0
      b <- field goal 1
      -- Use the SUP's label when duplicating term
      (term0, term1) <- makeDup (tLab goal) term
      ra <- checkGo dep term0 a
      rb <- checkGo dep term1 b
      makeNode _SUP_ (tLab goal) [ra, rb]
  | tTag term == _ERA_ = do
      pure nilT
  | tTag term == _VAR_ = do
      sub <- got (termLoc term)
      if termGetBit sub == 0
        then do
          putStr "(cant-infer-var)"
          pure eraT
        else do
          check dep (termRemBit sub) goal
  | tTag term == _NIL_ && tTag goal == _UNI_ = do
      pure nilT
  | tTag term == _W32_ && tTag goal == _U32_ = do
      pure nilT
  | tTag term == _SET_ && tTag goal == _SET_ = do
      pure nilT
  | tTag term == _EMP_ && tTag goal == _SET_ = do
      pure nilT
  | tTag term == _UNI_ && tTag goal == _SET_ = do
      pure nilT
  | tTag term == _U32_ && tTag goal == _SET_ = do
      pure nilT
  | tTag term == _SIG_ && tTag goal == _SET_ = do
      a <- field term 0
      b <- field term 1
      -- Duplicate 'a' before first use
      (a0, a1) <- makeDupFresh a
      aOk <- check dep a0 setT
      if tTag aOk == _ERA_ 
        then pure eraT
        else do
          lamT <- makeNode _LAM_ 0 [setT]
          allT <- makeNode _ALL_ 0 [a1, lamT]
          bOk <- check dep b allT
          if tTag bOk == _ERA_ 
            then pure eraT
            else pure nilT
  | tTag term == _ALL_ && tTag goal == _SET_ = do
      a <- field term 0
      b <- field term 1
      aOk <- check dep a setT
      if tTag aOk == _ERA_ 
        then do
          pure eraT
        else do
          lamT <- makeNode _LAM_ 0 [setT]
          allT <- makeNode _ALL_ 0 [setT, lamT]
          bOk <- check dep b allT
          if tTag bOk == _ERA_ 
            then pure eraT
            else pure nilT
  | tTag term == _LAM_ && tTag goal == _ALL_ = do
      a <- field goal 0
      b <- field goal 1
      (a0, a1) <- makeDupFresh a
      -- Create fresh variables for the lambda binding
      -- NOTE: temporarily, we will use W32 to simulate bruijn indices
      -- this causes nums to identify with vars, but is otherwise fine
      let var0 = termNew _W32_ 0 (fromIntegral dep)
      let var1 = termNew _W32_ 0 (fromIntegral dep)
      -- Annotate variables with types
      ann0 <- makeNode _ANN_ 0 [var0, a0]
      ann1 <- makeNode _ANN_ 0 [var1, a1]
      -- Apply function body and type body to variable
      appF <- makeNode _APP_ 0 [term, ann0]
      appB <- makeNode _APP_ 0 [b, ann1]
      appF_nf <- reduceAppLam appF term
      -- appF_nf <- return appF
      appB_nf <- whnf appB
      -- print $ showTerm b
      -- print $ showTerm appB
      -- print $ showTerm appB_nf
      -- print $ showTerm appF
      -- Check with increased depth
      check (dep + 1) appF_nf appB_nf
  | tTag term == _TUP_ && tTag goal == _SIG_ = do
      a <- field term 0
      b <- field term 1
      aTy <- field goal 0
      bTy <- field goal 1
      -- Duplicate 'a' before first use
      (a0, a1) <- makeDupFresh a
      -- Check first component
      aOk <- check dep a0 aTy
      if tTag aOk == _ERA_ 
        then pure eraT
        else do
          -- Apply dependent type to first component
          app <- makeNode _APP_ 0 [bTy, a1]
          bTyA <- whnf app
          -- Check second component
          bOk <- check dep b bTyA
          if tTag bOk == _ERA_ 
            then pure eraT
            else pure nilT
  | tTag term == _EFQ_ = do
      c <- field term 0
      rc <- check dep c empT
      if tTag rc == _ERA_ 
        then pure eraT
        else pure nilT
  | tTag term == _USE_ = do
      c <- field term 0
      f <- field term 1
      rc <- check dep c uniT
      if tTag rc == _ERA_ 
        then pure eraT
        else do
          rf <- check dep f goal
          if tTag rf == _ERA_ 
            then pure eraT
            else pure nilT
  | tTag term == _GET_ = do
      c <- field term 0
      f <- field term 1
      cType <- infer dep c
      if tTag cType == _ERA_ 
        then pure eraT
        else do
          cTypeNf <- whnf cType
          if tTag cTypeNf /= _SIG_ 
            then do
              putStr "(expected-pair-type)"
              pure eraT
            else do
              rf <- check dep f goal
              if tTag rf == _ERA_ 
                then pure eraT
                else pure nilT
  | tTag term == _SWI_ = do
      c <- field term 0
      z <- field term 1
      s <- field term 2
      rc <- check dep c u32T
      if tTag rc == _ERA_ 
        then pure eraT
        else do
          -- Get a fresh label for duplicating the goal
          freshLab <- genFreshLabel
          (goal0, goal1) <- makeDup freshLab goal
          rz <- check dep z goal0
          if tTag rz == _ERA_ 
            then pure eraT
            else do
              rs <- check dep s goal1
              if tTag rs == _ERA_ 
                then pure eraT
                else pure nilT
  | otherwise = do
      ty <- infer dep term
      if tTag ty == _ERA_ 
        then pure eraT
        else do
          eq <- equal dep ty goal
          if tTag eq == _NIL_ 
            then pure nilT 
            else do
              putStr "(type-mismatch)"
              pure eraT

-- PROBLEM: I'm attempting to type-check the following HVM3 file:

-- @main = <λx.x : ∀x:U32.U32>

-- yet, when running the `hvm` command on that file, I get:

-- <λa.a : ∀U32.λb.U32>

-- Checking @main...
-- check: term_new(LAM,0x000000,0x00000009) :: term_new(ALL,0x000000,0x0000000a)
-- check: term_new(VAR,0x000000,0x00000009) :: term_new(U32,0x000000,0x00000000)
-- check: term_new(ANN,0x000000,0x0000000e) :: term_new(U32,0x000000,0x00000000)
-- infer: term_new(ANN,0x000000,0x0000000e)
-- == term_new(LAM,0x000000,0x00000016)
-- .. term_new(U32,0x000000,0x00000000)
-- (type-mismatch)✗
-- WORK: 5 interactions
-- TIME: 0.0004910 seconds
-- SIZE: 28 nodes

-- this is unexpected. instead, I expected this term to type-check fine.
-- in particular, that equality should be U32 == U32, not LAM == U32.
-- that means there is some error in my code.
-- reason about the issue, find the exact location of the error, and
-- propose the simplest change that will fix this specific issue.