-- | 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 = forall w a. Writer w a -> w
execWriter forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` forall b. (MetaId -> Maybe Term) -> (QName -> b) -> GetDefsEnv b
GetDefsEnv MetaId -> Maybe Term
lookup QName -> b
emb) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ QName
d) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall b. GetDefsEnv b -> QName -> b
embDef
  doMeta :: MetaId -> GetDefsM b ()
doMeta MetaId
x = forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
getDefs forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ MetaId
x) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
getDefs

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

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

instance GetDefs Telescope where
  getDefs :: forall (m :: * -> *). MonadGetDefs m => Telescope -> m ()
getDefs = forall a (m :: * -> *). (GetDefs a, MonadGetDefs m) => a -> m ()
getDefs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList

-- no defs here

instance {-# OVERLAPPING #-} GetDefs String where
  getDefs :: forall (m :: * -> *). MonadGetDefs m => ArgName -> m ()
getDefs ArgName
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()