    -- | Extract used definitions from terms.

    module Agda.Syntax.Internal.Defs where

    import Control.Monad.Reader
    import Control.Monad.Writer

    import qualified Data.Foldable as Fold

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    -- | @getDefs' lookup emb a@ extracts all used definitions
    --   (functions, data/record types) from @a@, embedded into a monoid via @emb@.
    --   Instantiations of meta variables are obtained via @lookup@.
    --
    --   Typical monoid instances would be @[QName]@ or @Set QName@.
    --   Note that @emb@ can also choose to discard a used definition
    --   by mapping to the unit of the monoid.
    getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
    getDefs' :: forall a b.
    (GetDefs a, Monoid b) =>
    (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
    getDefs' MetaId -> Maybe Term
    lookup QName -> b
    emb = Writer b () -> b
    forall w a. Writer w a -> w
    execWriter (Writer b () -> b) -> (a -> Writer b ()) -> a -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ReaderT (GetDefsEnv b) (WriterT b Identity) ()
    -> GetDefsEnv b -> Writer b ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` (MetaId -> Maybe Term) -> (QName -> b) -> GetDefsEnv b
    forall b. (MetaId -> Maybe Term) -> (QName -> b) -> GetDefsEnv b
    GetDefsEnv MetaId -> Maybe Term
    lookup QName -> b
    emb) (ReaderT (GetDefsEnv b) (WriterT b Identity) () -> Writer b ())
    -> (a -> ReaderT (GetDefsEnv b) (WriterT b Identity) ())
    -> a
    -> Writer b ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> ReaderT (GetDefsEnv b) (WriterT b Identity) ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs

    -- | Inputs to and outputs of @getDefs'@ are organized as a monad.
    type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b)

    data GetDefsEnv b = GetDefsEnv
      { forall b. GetDefsEnv b -> MetaId -> Maybe Term
    lookupMeta :: MetaId -> Maybe Term
      , forall b. GetDefsEnv b -> QName -> b
    embDef     :: QName -> b
      }

    -- | What it takes to get the used definitions.
    class Monad m => MonadGetDefs m where
      doDef  :: QName -> m ()
      doMeta :: MetaId -> m ()

    instance Monoid b => MonadGetDefs (GetDefsM b) where
      doDef :: QName -> GetDefsM b ()
    doDef  QName
    d = b -> GetDefsM b ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (b -> GetDefsM b ())
    -> ((QName -> b) -> b) -> (QName -> b) -> GetDefsM b ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((QName -> b) -> QName -> b
    forall a b. (a -> b) -> a -> b
    $ QName
    d) ((QName -> b) -> GetDefsM b ())
    -> ReaderT (GetDefsEnv b) (WriterT b Identity) (QName -> b)
    -> GetDefsM b ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (GetDefsEnv b -> QName -> b)
    -> ReaderT (GetDefsEnv b) (WriterT b Identity) (QName -> b)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks GetDefsEnv b -> QName -> b
    forall b. GetDefsEnv b -> QName -> b
    embDef
      doMeta :: MetaId -> GetDefsM b ()
    doMeta MetaId
    x = Maybe Term -> GetDefsM b ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs (Maybe Term -> GetDefsM b ())
    -> ((MetaId -> Maybe Term) -> Maybe Term)
    -> (MetaId -> Maybe Term)
    -> GetDefsM b ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((MetaId -> Maybe Term) -> MetaId -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ MetaId
    x) ((MetaId -> Maybe Term) -> GetDefsM b ())
    -> ReaderT
         (GetDefsEnv b) (WriterT b Identity) (MetaId -> Maybe Term)
    -> GetDefsM b ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (GetDefsEnv b -> MetaId -> Maybe Term)
    -> ReaderT
         (GetDefsEnv b) (WriterT b Identity) (MetaId -> Maybe Term)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks GetDefsEnv b -> MetaId -> Maybe Term
    forall b. GetDefsEnv b -> MetaId -> Maybe Term
    lookupMeta

    -- | Getting the used definitions.
    --
    -- Note: in contrast to 'Agda.Syntax.Internal.Generic.foldTerm'
    -- @getDefs@ also collects from sorts in terms.
    -- Thus, this is not an instance of @foldTerm@.

    class GetDefs a where
      getDefs :: MonadGetDefs m => a -> m ()

      default getDefs :: (MonadGetDefs m, Foldable f, GetDefs b, f b ~ a) => a -> m ()
      getDefs = (b -> m ()) -> f b -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    Fold.mapM_ b -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs

    instance GetDefs Clause where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => Clause -> m ()
    getDefs = Maybe Term -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs (Maybe Term -> m ()) -> (Clause -> Maybe Term) -> Clause -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Term
    clauseBody

    instance GetDefs Term where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => Term -> m ()
    getDefs = \case
        Def QName
    d Elims
    vs   -> QName -> m ()
    forall (m :: * -> *). MonadGetDefs m => QName -> m ()
    doDef QName
    d m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Elims -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Elims
    vs
        Con ConHead
    _ ConInfo
    _ Elims
    vs -> Elims -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Elims
    vs
        Lit Literal
    l      -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Var Int
    i Elims
    vs   -> Elims -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Elims
    vs
        Lam ArgInfo
    _ Abs Term
    v    -> Abs Term -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Abs Term
    v
        Pi Dom Type
    a Abs Type
    b     -> Dom Type -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Dom Type
    a m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Abs Type -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Abs Type
    b
        Sort Sort
    s     -> Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Sort
    s
        Level Level
    l    -> Level -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Level
    l
        MetaV MetaId
    x Elims
    vs -> MetaId -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs MetaId
    x m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Elims -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Elims
    vs
        DontCare Term
    v -> Term -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Term
    v
        Dummy{}    -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance GetDefs MetaId where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => MetaId -> m ()
    getDefs MetaId
    x = MetaId -> m ()
    forall (m :: * -> *). MonadGetDefs m => MetaId -> m ()
    doMeta MetaId
    x

    instance GetDefs Type where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => Type -> m ()
    getDefs (El Sort
    s Term
    t) = Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Sort
    s m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Term -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Term
    t

    instance GetDefs Sort where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => Sort -> m ()
    getDefs = \case
        Type Level
    l    -> Level -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Level
    l
        Prop Level
    l    -> Level -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Level
    l
        Inf IsFibrant
    _ Integer
    _   -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        SSet Level
    l    -> Level -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Level
    l
        Sort
    SizeUniv  -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Sort
    LockUniv  -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> Dom' Term Term -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Dom' Term Term
    a m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Sort
    s1 m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Abs Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Abs Sort
    s2
        FunSort Sort
    s1 Sort
    s2 -> Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Sort
    s1 m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Sort
    s2
        UnivSort Sort
    s  -> Sort -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Sort
    s
        MetaS MetaId
    x Elims
    es  -> MetaId -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs MetaId
    x m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Elims -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Elims
    es
        DefS QName
    d Elims
    es   -> QName -> m ()
    forall (m :: * -> *). MonadGetDefs m => QName -> m ()
    doDef QName
    d m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Elims -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Elims
    es
        DummyS{}    -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance GetDefs Level where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => Level -> m ()
    getDefs (Max Integer
    _ [PlusLevel' Term]
    ls) = [PlusLevel' Term] -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs [PlusLevel' Term]
    ls

    instance GetDefs PlusLevel where
      getDefs :: forall (m :: * -> *). MonadGetDefs m => PlusLevel' Term -> m ()
    getDefs (Plus Integer
    _ Term
    l)    = Term -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs Term
    l

    -- collection instances

    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 :: forall (m :: * -> *). MonadGetDefs m => (a, b) -> m ()
    getDefs (a
    a,b
    b) = a -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs a
    a m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> b -> m ()
    forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
    getDefs b
    b