{-# OPTIONS_GHC -Wunused-imports #-}
-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -dno-suppress-type-signatures -ddump-to-file -dno-typeable-binds #-}

-- | Extract used definitions from terms.

module Agda.Syntax.Internal.Defs where

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Utils.ExpandCase
import Agda.Utils.StrictEndo
import Agda.Utils.Impossible

-- | Get list of definitions, throw an error if any metavariable is encountered.
getDefListNoMetas :: Term -> [QName]
getDefListNoMetas :: Term -> [QName]
getDefListNoMetas Term
a =
  (MetaId -> Maybe Term)
-> (QName -> Endo [QName]) -> Term -> Endo [QName]
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs (\MetaId
_ -> Maybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__) (\QName
x -> ([QName] -> [QName]) -> Endo [QName]
forall a. (a -> a) -> Endo a
Endo \[QName]
xs -> QName
xQName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:[QName]
xs) Term
a Endo [QName] -> [QName] -> [QName]
forall a. Endo a -> a -> a
`appEndo` []

-- | 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 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 @Endo [QName]@ or @Set QName@. Do not use @[QName]@
  --   because of obvious quadratic slowdown.
  --   Note that @emb@ can also choose to discard a used definition
  --   by mapping to the unit of the monoid.
  getDefs :: (Monoid m, ExpandCase m) => (MetaId -> Maybe Term) -> (QName -> m) -> a -> m

  -- {-# INLINE getDefs #-}
  -- default getDefs ::
  --      (Foldable f, GetDefs b, f b ~ a, Monoid m, ExpandCase m)
  --   => (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
  -- getDefs ms ds = foldMap (getDefs ms ds)

instance GetDefs Clause where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Clause -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Clause
cl =
    ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Maybe Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Maybe Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds (Clause -> Maybe Term
clauseBody Clause
cl)

instance GetDefs Term where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Term
t = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Term
t of
    Def QName
d Elims
vs   -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ QName -> m
ds QName
d m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elims
vs
    Con ConHead
_ ConInfo
_ Elims
vs -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elims
vs
    Lit Literal
l      -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    Var Int
i Elims
vs   -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elims
vs
    Lam ArgInfo
_ Abs Term
v    -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Abs Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Abs Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Abs Term
v
    Pi Dom Type
a Abs Type
b     -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Dom Type -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Dom Type -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Dom Type
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Abs Type -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Abs Type -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Abs Type
b
    Sort Sort
s     -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s
    Level Level
l    -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Level -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Level -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Level
l
    MetaV MetaId
x Elims
vs -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> MetaId -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> MetaId -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds MetaId
x m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elims
vs
    DontCare Term
v -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Term
v
    Dummy{}    -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty

instance GetDefs MetaId where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> MetaId -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds MetaId
x = (MetaId -> Maybe Term) -> (QName -> m) -> Maybe Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Maybe Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds (MetaId -> Maybe Term
ms MetaId
x)

instance GetDefs Type where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Type -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Type
a = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Type
a of
    El Sort
s Term
t -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Term
t

instance GetDefs Sort where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Sort
s of
    Univ Univ
_ Level
l       -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Level -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Level -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Level
l
    Inf Univ
_ Integer
_        -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    Sort
SizeUniv       -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    Sort
LockUniv       -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    Sort
LevelUniv      -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    Sort
IntervalUniv   -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Dom' Term Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Dom' Term Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Dom' Term Term
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Abs Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Abs Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Abs Sort
s2
    FunSort Sort
s1 Sort
s2  -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s2
    UnivSort Sort
s     -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Sort -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Sort
s
    MetaS MetaId
x Elims
es     -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> MetaId -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> MetaId -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds MetaId
x m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elims
es
    DefS QName
d Elims
es      -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ QName -> m
ds QName
d m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elims -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elims
es
    DummyS{}       -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty

instance GetDefs Level where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Level -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Level
l = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Level
l of Max Integer
_ [PlusLevel' Term]
ls -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> [PlusLevel' Term] -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> [PlusLevel' Term] -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds [PlusLevel' Term]
ls

instance GetDefs PlusLevel where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> PlusLevel' Term -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds PlusLevel' Term
l = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case PlusLevel' Term
l of Plus Integer
_ Term
l -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Term -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Term
l

-- collection instances
instance GetDefs a => GetDefs (Maybe a) where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Maybe a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Maybe a
ma = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Maybe a
ma of
    Maybe a
Nothing -> m -> Result m
ret m
forall a. Monoid a => a
mempty
    Just a
a  -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
a

instance GetDefs a => GetDefs [a] where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> [a] -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds = [a] -> m
go where
    go :: [a] -> m
go [a]
as = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case [a]
as of
      []   -> m -> Result m
ret m
forall a. Monoid a => a
mempty
      a
a:[a]
as -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> [a] -> m
go [a]
as

instance GetDefs a => GetDefs (Elim' a) where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Elim' a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Elim' a
e = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Elim' a
e of
    Apply Arg a
t      -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> Arg a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Arg a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Arg a
t
    Proj ProjOrigin
_ QName
_     -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ m
forall a. Monoid a => a
mempty
    IApply a
l a
r a
t -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
l m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
r m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
t

instance GetDefs a => GetDefs (Arg a) where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Arg a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Arg a
a = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Arg a
a of
    Arg ArgInfo
_ a
t -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
t

instance GetDefs a => GetDefs (Dom a) where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Dom a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Dom a
d = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Dom a
d of
    Dom ArgInfo
_ Maybe NamedName
_ Bool
_ Maybe Term
_ Maybe (RewDom' Term)
_ a
t -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
t

instance GetDefs a => GetDefs (Abs a) where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Abs a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds Abs a
a = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case Abs a
a of
    Abs ArgName
_ a
t   -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
t
    NoAbs ArgName
_ a
t -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
t

instance (GetDefs a, GetDefs b) => GetDefs (a,b) where
  {-# INLINE getDefs #-}
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> (a, b) -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds (a, b)
ab = ((m -> Result m) -> Result m) -> m
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \m -> Result m
ret -> case (a, b)
ab of (a
a,b
b) -> m -> Result m
ret (m -> Result m) -> m -> Result m
forall a b. (a -> b) -> a -> b
$ (MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds a
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (MetaId -> Maybe Term) -> (QName -> m) -> b -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> b -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds b
b

instance GetDefs Telescope where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> Telescope -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds = (MetaId -> Maybe Term)
-> (QName -> m) -> [Dom (ArgName, Type)] -> m
forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term)
-> (QName -> m) -> [Dom (ArgName, Type)] -> m
forall a m.
(GetDefs a, Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> a -> m
getDefs MetaId -> Maybe Term
ms QName -> m
ds ([Dom (ArgName, Type)] -> m)
-> (Telescope -> [Dom (ArgName, Type)]) -> Telescope -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList

-- no defs here
instance {-# OVERLAPPING #-} GetDefs String where
  getDefs :: forall m.
(Monoid m, ExpandCase m) =>
(MetaId -> Maybe Term) -> (QName -> m) -> ArgName -> m
getDefs MetaId -> Maybe Term
_ QName -> m
_ ArgName
_ = m
forall a. Monoid a => a
mempty