{-# LANGUAGE TypeFamilies #-}
module Agda.Syntax.Internal.Defs where
import Control.Monad.Reader
import Control.Monad.Writer
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Agda.Syntax.Common
import Agda.Syntax.Internal
getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
getDefs' lookup emb = execWriter . (`runReaderT` GetDefsEnv lookup emb) . getDefs
type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b)
data GetDefsEnv b = GetDefsEnv
{ lookupMeta :: MetaId -> Maybe Term
, embDef :: QName -> b
}
class Monad m => MonadGetDefs m where
doDef :: QName -> m ()
doMeta :: MetaId -> m ()
instance Monoid b => MonadGetDefs (GetDefsM b) where
doDef d = tell . ($ d) =<< asks embDef
doMeta x = getDefs . ($ x) =<< asks lookupMeta
class GetDefs a where
getDefs :: MonadGetDefs m => a -> m ()
default getDefs :: (MonadGetDefs m, Foldable f, GetDefs b, f b ~ a) => a -> m ()
getDefs = Fold.mapM_ getDefs
instance GetDefs Clause where
getDefs = getDefs . clauseBody
instance GetDefs Term where
getDefs v = case v of
Def d vs -> doDef d >> getDefs vs
Con _ _ vs -> getDefs vs
Lit l -> return ()
Var i vs -> getDefs vs
Lam _ v -> getDefs v
Pi a b -> getDefs a >> getDefs b
Sort s -> getDefs s
Level l -> getDefs l
MetaV x vs -> getDefs x >> getDefs vs
DontCare v -> getDefs v
instance GetDefs MetaId where
getDefs x = doMeta x
instance GetDefs Type where
getDefs (El s t) = getDefs s >> getDefs t
instance GetDefs Sort where
getDefs s = case s of
Type l -> getDefs l
Prop -> return ()
Inf -> return ()
SizeUniv -> return ()
PiSort s s' -> getDefs s >> getDefs s'
UnivSort s -> getDefs s
MetaS x es -> getDefs x >> getDefs es
instance GetDefs Level where
getDefs (Max ls) = getDefs ls
instance GetDefs PlusLevel where
getDefs ClosedLevel{} = return ()
getDefs (Plus _ l) = getDefs l
instance GetDefs LevelAtom where
getDefs a = case a of
MetaLevel x vs -> getDefs x >> getDefs vs
BlockedLevel _ v -> getDefs v
NeutralLevel _ v -> getDefs v
UnreducedLevel v -> getDefs v
instance GetDefs a => GetDefs (Maybe a) where
instance GetDefs a => GetDefs [a] where
instance GetDefs a => GetDefs (Elim' a) where
instance GetDefs a => GetDefs (Arg a) where
instance GetDefs a => GetDefs (Dom a) where
instance GetDefs a => GetDefs (Abs a) where
instance (GetDefs a, GetDefs b) => GetDefs (a,b) where
getDefs (a,b) = getDefs a >> getDefs b