49 lines
1.6 KiB
Haskell
49 lines
1.6 KiB
Haskell
module Program where
|
|
|
|
import Check
|
|
import Control.Monad.Except
|
|
import qualified Data.Map.Strict as M
|
|
import Elaborator
|
|
import Errors
|
|
import Eval (Env, checkBeta)
|
|
import qualified Eval
|
|
import Expr (Expr)
|
|
import qualified Expr
|
|
import IR
|
|
import Parser (parseProgram)
|
|
import Preprocessor (runPreprocessor)
|
|
|
|
insertDef :: Text -> Expr -> Expr -> Env -> Env
|
|
insertDef name ty body = M.insert name (Eval.Def ty body)
|
|
|
|
handleDef :: IRDef -> StateT Env Result ()
|
|
handleDef (Axiom name ty) = do
|
|
env <- get
|
|
_ <- liftEither $ checkType env $ elaborate ty
|
|
modify $ insertDef name (elaborate ty) (Expr.Axiom name)
|
|
handleDef (Def name Nothing irBody) = do
|
|
env <- get
|
|
ty <- liftEither $ checkType env body
|
|
modify $ insertDef name ty body
|
|
where
|
|
body = elaborate irBody
|
|
handleDef (Def name (Just irTy) irBody) = do
|
|
env <- get
|
|
ty' <- liftEither $ checkType env body
|
|
liftEither $ checkBeta env ty ty' body
|
|
modify $ insertDef name ty' body
|
|
where
|
|
body = elaborate irBody
|
|
ty = elaborate irTy
|
|
|
|
evalDef :: Env -> IRDef -> Result Env
|
|
evalDef = flip (execStateT . handleDef)
|
|
|
|
handleProgram :: Env -> IRProgram -> Result Env
|
|
handleProgram env = flip execStateT env . mapM_ handleDef
|
|
|
|
handleAndParseProgram :: Env -> String -> Text -> Either String Env
|
|
handleAndParseProgram env filename input = (first toString . handleProgram env) =<< parseProgram filename input
|
|
|
|
handleAndParseFile :: Env -> String -> ExceptT String IO Env
|
|
handleAndParseFile env filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . handleAndParseProgram env filename
|