Agda-2.3.2.2: src/prototyping/terms/Monad.hs
module Monad where
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Error
import Name
import Term
data TCState = TCSt { stFresh :: Integer
, stSignature :: [(Name, Term)]
}
initState = TCSt { stFresh = 0
, stSignature = []
}
data TCEnv = TCEnv { envSubst :: Env }
initEnv = TCEnv { envSubst = [] }
type TC = StateT TCState (ReaderT TCEnv (Either String))
runTC :: TC a -> Either String a
runTC m = runReaderT (evalStateT m initState) initEnv
fresh :: String -> TC Name
fresh x = do
s <- get
put s { stFresh = stFresh s + 1 }
return $ Name x (stFresh s)
bindVar :: String -> (Name -> TC a) -> TC a
bindVar x ret = do
x <- fresh x
local (\e -> e { envSubst = (x, Var x []) : envSubst e }) (ret x)
addDecl :: Name -> Term -> TC ()
addDecl x v =
modify $ \s -> s { stSignature = (x, v) : stSignature s }
addConst :: String -> TC Name
addConst x = do
x <- fresh x
addDecl x (Con x [])
return x
addDef :: String -> Term -> TC Name
addDef x v = do
x <- fresh x
addDecl x v
return x
resolveName :: String -> TC Term
resolveName s = do
env <- asks envSubst
sig <- gets stSignature
case find var env ++ find con sig of
[] -> fail $ "unbound name: " ++ s
x:_ -> return x
where
find f sub = [ f x | x@(Name s' _) <- map fst sub, s == s' ]
var x = Var x []
con c = Con c []
varValue :: Name -> TC Term
varValue x = do
env <- asks envSubst
case lookup x env of
Just v -> return v
Nothing -> fail $ "panic: unbound var " ++ show x
conValue :: Name -> TC Term
conValue c = do
sig <- gets stSignature
case lookup c sig of
Just v -> return v
Nothing -> fail $ "panic: unbound con " ++ show c
getSubst :: TC Env
getSubst = asks envSubst
withSubst :: Env -> TC a -> TC a
withSubst sub = local $ \e -> e { envSubst = sub }