-- | 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' :: (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
  { GetDefsEnv b -> MetaId -> Maybe Term
lookupMeta :: MetaId -> Maybe Term
  , 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) (Writer b) (QName -> b) -> GetDefsM b ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (GetDefsEnv b -> QName -> b)
-> ReaderT (GetDefsEnv b) (Writer b) (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) (Writer b) (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) (Writer b) (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 :: 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 :: 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 :: MetaId -> m ()
getDefs MetaId
x = MetaId -> m ()
forall (m :: * -> *). MonadGetDefs m => MetaId -> m ()
doMeta MetaId
x

instance GetDefs Type where
  getDefs :: 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 :: 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 :: 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 :: 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 :: (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