packages feed

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 }