module LText.Internal.Evaluation where
import LText.Internal.Expr
import LText.Internal.Classes
import qualified Data.Map as Map
import Data.Composition
import Control.Monad.Composition
import Control.Monad.Except
import Control.Monad.State
runEv :: ( Monad m
, MonadError String m
) => StateT (Int, Bool) m a -> m a
runEv e = evalStateT e (0, True)
freshExprVar :: ( Monad m
, MonadState (Int, Bool) m
) => String -> m String
freshExprVar prefix = do
(n,fresh) <- get
put (n+1, fresh)
return $ prefix ++ show n
reduce :: ( Monad m
, MonadState (Int, Bool) m
) => Expr -> m Expr
reduce (EVar n) = return $ EVar n
reduce (EApp e1 e2) = do
(n,fresh) <- get
put (n,True)
e1' <- reduce e1
case e1' of
EAbs n e3 -> do normRight <- alpha =<< reduce e2
reduce $ apply (Map.singleton n normRight) e3
_ -> return $ EApp e1' e2
reduce (EAbs n e1) = do
(d,fresh) <- get
if fresh
then case e1 of
EApp e2 (EVar m) | n == m -> reduce e2
| otherwise -> do put (d,False)
e2' <- reduce e2
return $ EAbs n (EApp e2' $ EVar m)
_ -> do put (d,False)
EAbs n <$> reduce e1
else EAbs n <$> reduce e1
reduce (ELet n x y) = do normRight <- alpha =<< reduce x
reduce $ apply (Map.singleton n normRight) y
reduce (EText fs) = return $ EText fs
reduce (EConc e1 e2) = liftM2 EConc (reduce e1) (reduce e2)
alpha :: ( Monad m
, MonadState (Int, Bool) m
) => Expr -> m Expr
alpha = go []
where
go xs (EAbs n e1)
| n `elem` xs = do n' <- freshExprVar n
e1' <- go (n:xs) e1
return $ EAbs n' $ apply (Map.singleton n $ EVar n') e1'
| otherwise = (return . EAbs n) =<< go (n:xs) e1
go xs (EApp e1 e2) = (return .* EApp) ==<< go xs e1 =<< go xs e2
go _ (EVar n) = return $ EVar n
go _ (EText ts) = return $ EText ts
go xs (EConc e1 e2) = (return .* EConc) ==<< go xs e1 =<< go xs e2