Haskell Call By Value

{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}

module Main where

import System.Environment (getArgs)

data Term
  = TmVar Int Int
  | TmAbs Term
  | TmApp Term Term
  deriving (Show)

termShift :: Int -> Term -> Term
termShift d = walk 0
  where
    walk c t = case t of
      TmAbs t1 -> TmAbs (walk (c + 1) t1)
      TmApp t1 t2 -> TmApp (walk c t1) (walk c t2)
      TmVar x n ->
        if x >= c
          then TmVar (x + d) (n + d)
          else TmVar x (n + d)

termSubst :: Int -> Term -> Term -> Term
termSubst j s = walk 0
  where
    walk c t = case t of
      TmAbs t1 -> TmAbs (walk (c + 1) t1)
      TmApp t1 t2 -> TmApp (walk c t1) (walk c t2)
      TmVar x _ ->
        if x == j + c
          then termShift c s
          else t

termSubstTop :: Term -> Term -> Term
termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)

isVal :: Term -> Bool
isVal TmAbs {} = True
isVal _ = False

eval1 :: Term -> Maybe Term
eval1 t = case t of
  TmApp (TmAbs t12) v2
    | isVal v2 ->
        return $ termSubstTop v2 t12
  TmApp v1 t2 | isVal v1 -> do
    t2' <- eval1 t2
    return $ TmApp v1 t2'
  TmApp t1 t2 -> do
    t1' <- eval1 t1
    return $ TmApp t1' t2
  _ -> Nothing

eval :: Term -> Term
eval t = maybe t eval (eval1 t)

-- Wrapper around Term to include a recursion counter
data TrackedTerm = TrackedTerm
  { termVal :: Term,
    counter :: Int
  }
  deriving (Show)

-- Increment the counter in the TrackedTerm
increment :: TrackedTerm -> TrackedTerm
increment (TrackedTerm t c) = TrackedTerm t (c + 1)

-- A version of eval that tracks the number of recursive calls
-- Modified evalTracked to respect stepsLimit
evalTracked :: Int -> TrackedTerm -> TrackedTerm
evalTracked stepsLimit trackedTerm@(TrackedTerm t c)
  | c >= stepsLimit = trackedTerm  -- Stop if we've reached the step limit
  | otherwise = case eval1 t of
      Nothing -> trackedTerm  -- No more reductions can be done
      Just t' -> evalTracked stepsLimit (increment (TrackedTerm t' c))

-- To use evalTracked, you start with a counter of 0
-- Modified evalWithCounter to take stepsLimit and initiate evalTracked with it
evalWithCounter :: Term -> Int -> TrackedTerm
evalWithCounter t stepsLimit = evalTracked stepsLimit (TrackedTerm t 0)

-- Process a single term, returning the result as a string
processTerm :: Term -> Int -> IO String
processTerm inputTerm limit = do
      let TrackedTerm resultTerm reductionsCount = evalWithCounter inputTerm limit
      return $
        if (reductionsCount == 0) || (reductionsCount == limit) then "0"
        else show resultTerm
          ++ ","
          ++ show reductionsCount

nativeT :: Int -> Int -> Int
nativeT 0 m = m
nativeT n m =
  nativeT (n - 1) (m + 1)
    + sum [nativeT i m * nativeT (n - 1 - i) m | i <- [0 .. n - 1]]

appTerm :: Int -> Int -> Int -> Int -> Term
appTerm maxFreeVarCnt termSize j h
  | h <= tjmtnjm =
      let dv = (h - 1) `div` tnjm
          md = (h - 1) `mod` tnjm
          newApp = TmApp (unRankT j maxFreeVarCnt (dv + 1)) (unRankT (termSize - j) maxFreeVarCnt (md + 1))
       in newApp
  | otherwise = appTerm maxFreeVarCnt termSize (j + 1) (h - tjmtnjm)
  where
    tnjm = nativeT (termSize - j) maxFreeVarCnt
    tjmtnjm = nativeT j maxFreeVarCnt * tnjm

unRankT :: Int -> Int -> Int -> Term
unRankT termSize maxFreeVarCnt numberOfTerm
  | termSize == 0 = TmVar (numberOfTerm - 1) (numberOfTerm - 1 + 1)
  | numberOfTerm <= nativeT (termSize - 1) (maxFreeVarCnt + 1) = TmAbs (unRankT (termSize - 1) (maxFreeVarCnt + 1) numberOfTerm)
  | otherwise = appTerm maxFreeVarCnt (termSize - 1) 0 (numberOfTerm - nativeT (termSize - 1) (maxFreeVarCnt + 1))

generateTerm :: Int -> Int -> Int -> Term
generateTerm = unRankT

-- main :: IO ()
-- main = do
--   let term_size = (8 :: Int)
--   let term_num = (443769 :: Int)
--   putStr (show term_size ++ "," ++ show term_num ++ ",")
--   let term = generateTerm 8 0 443769
--   putStr (show term ++ ",")
--   resultString <- processTerm term
--   putStr resultString
--   putStr "\n"

main :: IO ()
main = do
  args <- getArgs
  case args of
    [maxSizeStr] -> do
      let maxSize = read maxSizeStr :: Int
      writeFile "data.csv" ""
      mapM_ processSize [1..maxSize]
    _ -> putStr "Wrong argument"

-- Process each size
processSize :: Int -> IO ()
processSize size = do
  let maxNum = nativeT size 0
  mapM_ (processTermForSize size) [1..maxNum]

-- Process each term for a given size and number
processTermForSize :: Int -> Int -> IO ()
processTermForSize size num = do
  let term = generateTerm size 0 num
  resultString <- processTerm term (size * 15)
  appendFile "data.csv" (if resultString == "0" then "" else show size ++ "," ++ show num ++ "," ++ resultString ++ "\n")