content: {-# LANGUAGE LambdaCase #-}
  
  module Term
    ( Term(..)
    , fromBLC
    , nf
    ) where
  
  import           Control.Concurrent.MVar
  import           Data.List                      ( elemIndex )
  import           Data.Map.Strict                ( Map )
  import qualified Data.Map.Strict               as Map
  import           Data.Maybe                     ( fromMaybe )
  import           Utils
  
  data Term = Abs Term | App Term Term | Idx Int
    deriving (Eq, Ord)
  
  instance Show Term where
    showsPrec _ (Abs body) = showString "[" . shows body . showString "]"
    showsPrec _ (App lhs rhs) =
      showString "(" . shows lhs . showString " " . shows rhs . showString ")"
    showsPrec _ (Idx i) = shows i
  
  fromBLC' :: String -> (Term, String)
  fromBLC' inp = case inp of
    '0' : '0' : rst -> let (e, es) = fromBLC' rst in (Abs e, es)
    '0' : '1' : rst ->
      let (exp1, rst1) = fromBLC' rst
          (exp2, rst2) = fromBLC' rst1
      in  (App exp1 exp2, rst2)
    '1' : _ : rst -> binaryBruijn rst
    _             -> invalid
   where
    binaryBruijn rst =
      let idx = length (takeWhile (== '1') inp) - 1
      in  case rst of
            "" -> (Idx idx, "")
            _  -> (Idx idx, drop idx rst)
  
  fromBLC :: String -> Term
  fromBLC = fst . fromBLC'
  
  -- RKNL abstract machine, call-by-need reducer
  -- written for my bruijn programming language
  
  type Store = Map Int Box
  type Stack = [Redex]
  
  newtype NameGen = NameGen Int
  data BoxValue = Todo Redex | Done Redex | Empty
  newtype Box = Box (MVar BoxValue)
  data Ridx = Num Int | Hole
  data Redex = Rabs Int Redex | Rapp Redex Redex | Ridx Ridx | Rclosure Redex Store | Rcache Box Redex
  data Conf = Econf NameGen Redex Store Stack | Cconf NameGen Stack Redex | End
  
  nextName :: NameGen -> (Int, NameGen)
  nextName (NameGen x) = (x, NameGen $ x + 1)
  
  toRedex :: Term -> Redex
  toRedex = convertWorker (NameGen 1) []
   where
    convertWorker g ns (Abs e) =
      let (v, g') = nextName g
          t       = convertWorker g' (v : ns) e
      in  Rabs v t
    convertWorker g ns (App l r) =
      let lhs = convertWorker g ns l
          rhs = convertWorker g ns r
      in  Rapp lhs rhs
    convertWorker _ ns (Idx i) =
      Ridx $ Num (if i < 0 || i >= length ns then i else ns !! i)
  
  fromRedex :: Redex -> Term
  fromRedex = convertWorker []
   where
    convertWorker es (Rabs n e) = Abs $ convertWorker (n : es) e
    convertWorker es (Rapp l r) =
      let lhs = convertWorker es l
          rhs = convertWorker es r
      in  App lhs rhs
    convertWorker es (Ridx (Num n)) = Idx $ fromMaybe n (elemIndex n es)
    convertWorker _  _              = invalid
  
  transition :: Conf -> IO Conf
  transition (Econf g (Rapp u v) e s) =
    pure $ Econf g u e (Rapp (Ridx Hole) (Rclosure v e) : s)
  transition (Econf g (Rabs x t) e s) = do
    box <- newMVar Empty
    pure $ Cconf g s (Rcache (Box box) (Rclosure (Rabs x t) e))
  transition (Econf g (Ridx (Num x)) e s) = do
    def <- newMVar $ Done $ Ridx $ Num x
    let b@(Box m) = Map.findWithDefault (Box def) x e
    rd <- readMVar m
    case rd of
      Todo (Rclosure v e') -> pure $ Econf g v e' (Rcache b (Ridx Hole) : s)
      Done t               -> pure $ Cconf g s t
      _                    -> invalid
  transition (Cconf g ((Rcache (Box m) (Ridx Hole)) : s) t) = do
    modifyMVar_ m (\_ -> pure $ Done t)
    pure $ Cconf g s t
  transition (Cconf g ((Rapp (Ridx Hole) ve) : s) (Rcache _ (Rclosure (Rabs x t) e)))
    = do
      box <- newMVar (Todo ve)
      pure $ Econf g t (Map.insert x (Box box) e) s
  transition (Cconf g s (Rcache (Box m) (Rclosure (Rabs x t) e))) = do
    rd <- readMVar m
    case rd of
      Done v -> pure $ Cconf g s v
      Empty  -> do
        let (x1, g') = nextName g
        box <- newMVar $ Done $ Ridx $ Num x1
        pure $ Econf g'
                     t
                     (Map.insert x (Box box) e)
                     (Rabs x1 (Ridx Hole) : Rcache (Box m) (Ridx Hole) : s)
      Todo _ -> invalid
  transition (Cconf g ((Rapp (Ridx Hole) (Rclosure v e)) : s) t) =
    pure $ Econf g v e (Rapp t (Ridx Hole) : s)
  transition (Cconf g ((Rapp t (Ridx Hole)) : s) v) = pure $ Cconf g s (Rapp t v)
  transition (Cconf g ((Rabs x1 (Ridx Hole)) : s) v) =
    pure $ Cconf g s (Rabs x1 v)
  transition (Cconf _ [] _) = pure End
  transition _              = invalid
  
  forEachState :: Conf -> (Conf -> IO Conf) -> IO Conf
  forEachState conf trans = trans conf >>= \case
    End  -> pure conf
    next -> forEachState next trans
  
  -- TODO: NameGen is arbitrary to not conflict with toRedex
  loadTerm :: Redex -> Conf
  loadTerm t = Econf (NameGen 1000000) t Map.empty []
  
  nf :: Term -> IO Term
  nf e = do
    let redex = toRedex e
    forEachState (loadTerm redex) transition >>= \case
      Cconf _ [] v -> pure $ fromRedex v
      _            -> invalid
  