module Agda.Syntax.Abstract.Views where

import Prelude hiding (null)

import Control.Applicative ( Const(Const), getConst )
import Control.Arrow (first)
import Control.Monad.Identity

import Data.Foldable (foldMap)
import qualified Data.DList as DL
import Data.Semigroup ((<>))
import Data.Void

import Agda.Syntax.Common
import Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete (FieldAssignment', exprFieldA)
import Agda.Syntax.Info
import Agda.Syntax.Scope.Base (KindOfName(..), conKindOfName, WithKind(..))

import Agda.Utils.Either
import Agda.Utils.List1 (List1)
import Agda.Utils.Null
import Agda.Utils.Singleton

import Agda.Utils.Impossible


data AppView' arg = Application Expr [NamedArg arg]
  deriving (forall a b. a -> AppView' b -> AppView' a
forall a b. (a -> b) -> AppView' a -> AppView' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> AppView' b -> AppView' a
$c<$ :: forall a b. a -> AppView' b -> AppView' a
fmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
$cfmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
Functor)

type AppView = AppView' Expr

-- | Gather applications to expose head and spine.
--
--   Note: everything is an application, possibly of itself to 0 arguments
appView :: Expr -> AppView
appView :: Expr -> AppView
appView = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> AppView' (AppInfo, Expr)
appView'

appView' :: Expr -> AppView' (AppInfo, Expr)
appView' :: Expr -> AppView' (AppInfo, Expr)
appView' Expr
e = [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
f (forall a. DList a -> [a]
DL.toList DList (NamedArg (AppInfo, Expr))
es)
  where
  ([NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
f, DList (NamedArg (AppInfo, Expr))
es) = forall {arg}.
Expr
-> ([NamedArg arg] -> AppView' arg,
    DList (NamedArg (AppInfo, Expr)))
appView'' Expr
e

  appView'' :: Expr
-> ([NamedArg arg] -> AppView' arg,
    DList (NamedArg (AppInfo, Expr)))
appView'' Expr
e = case Expr
e of
    App AppInfo
i Expr
e1 NamedArg Expr
e2
      | Dot ExprInfo
_ Expr
e2' <- Expr -> Expr
unScope forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Expr
e2
      , Just Expr
f <- Expr -> Maybe Expr
maybeProjTurnPostfix Expr
e2'
      , forall a. LensHiding a => a -> Hiding
getHiding NamedArg Expr
e2 forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden -- Jesper, 2018-12-13: postfix projections shouldn't be hidden
      -> (forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application Expr
f, forall el coll. Singleton el coll => el -> coll
singleton (forall a. a -> NamedArg a
defaultNamedArg (AppInfo
i, Expr
e1)))
    App AppInfo
i Expr
e1 NamedArg Expr
arg | ([NamedArg arg] -> AppView' arg
f, DList (NamedArg (AppInfo, Expr))
es) <- Expr
-> ([NamedArg arg] -> AppView' arg,
    DList (NamedArg (AppInfo, Expr)))
appView'' Expr
e1 ->
      ([NamedArg arg] -> AppView' arg
f, DList (NamedArg (AppInfo, Expr))
es forall a. DList a -> a -> DList a
`DL.snoc` (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (AppInfo
i,) NamedArg Expr
arg)
    ScopedExpr ScopeInfo
_ Expr
e -> Expr
-> ([NamedArg arg] -> AppView' arg,
    DList (NamedArg (AppInfo, Expr)))
appView'' Expr
e
    Expr
_              -> (forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application Expr
e, forall a. Monoid a => a
mempty)

maybeProjTurnPostfix :: Expr -> Maybe Expr
maybeProjTurnPostfix :: Expr -> Maybe Expr
maybeProjTurnPostfix Expr
e =
  case Expr
e of
    ScopedExpr ScopeInfo
i Expr
e' -> ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Expr
maybeProjTurnPostfix Expr
e'
    Proj ProjOrigin
_ AmbiguousQName
x        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
ProjPostfix AmbiguousQName
x
    Expr
_               -> forall a. Maybe a
Nothing

unAppView :: AppView -> Expr
unAppView :: AppView -> Expr
unAppView (Application Expr
h [NamedArg Expr]
es) =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
defaultAppInfo_) Expr
h [NamedArg Expr]
es

-- | Collects plain lambdas.
data LamView = LamView [LamBinding] Expr

lamView :: Expr -> LamView
lamView :: Expr -> LamView
lamView (Lam ExprInfo
i LamBinding
b Expr
e) = LamBinding -> LamView -> LamView
cons LamBinding
b forall a b. (a -> b) -> a -> b
$ Expr -> LamView
lamView Expr
e
  where cons :: LamBinding -> LamView -> LamView
cons LamBinding
b (LamView [LamBinding]
bs Expr
e) = [LamBinding] -> Expr -> LamView
LamView (LamBinding
b forall a. a -> [a] -> [a]
: [LamBinding]
bs) Expr
e
lamView (ScopedExpr ScopeInfo
_ Expr
e) = Expr -> LamView
lamView Expr
e
lamView Expr
e = [LamBinding] -> Expr -> LamView
LamView [] Expr
e

-- | Collect @A.Pi@s.
data PiView = PiView [(ExprInfo, Telescope1)] Type

piView :: Expr -> PiView
piView :: Expr -> PiView
piView = \case
   Pi ExprInfo
i Telescope1
tel Expr
b -> PiView -> PiView
cons forall a b. (a -> b) -> a -> b
$ Expr -> PiView
piView Expr
b
     where cons :: PiView -> PiView
cons (PiView [(ExprInfo, Telescope1)]
tels Expr
t) = [(ExprInfo, Telescope1)] -> Expr -> PiView
PiView ((ExprInfo
i,Telescope1
tel) forall a. a -> [a] -> [a]
: [(ExprInfo, Telescope1)]
tels) Expr
t
   Expr
e -> [(ExprInfo, Telescope1)] -> Expr -> PiView
PiView [] Expr
e

unPiView :: PiView -> Expr
unPiView :: PiView -> Expr
unPiView (PiView [(ExprInfo, Telescope1)]
tels Expr
t) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ExprInfo -> Telescope1 -> Expr -> Expr
Pi) Expr
t [(ExprInfo, Telescope1)]
tels

-- | Gather top-level 'AsP'atterns and 'AnnP'atterns to expose underlying pattern.
asView :: A.Pattern -> ([Name], [A.Expr], A.Pattern)
asView :: Pattern -> ([Name], [Expr], Pattern)
asView (A.AsP PatInfo
_ BindName
x Pattern
p)  = (\([Name]
asb, [Expr]
ann, Pattern
p) -> (BindName -> Name
unBind BindName
x forall a. a -> [a] -> [a]
: [Name]
asb, [Expr]
ann, Pattern
p)) forall a b. (a -> b) -> a -> b
$ Pattern -> ([Name], [Expr], Pattern)
asView Pattern
p
asView (A.AnnP PatInfo
_ Expr
a Pattern
p) = (\([Name]
asb, [Expr]
ann, Pattern
p) -> ([Name]
asb, Expr
a forall a. a -> [a] -> [a]
: [Expr]
ann, Pattern
p))        forall a b. (a -> b) -> a -> b
$ Pattern -> ([Name], [Expr], Pattern)
asView Pattern
p
asView Pattern
p              = ([], [], Pattern
p)

-- | Remove top 'ScopedExpr' wrappers.
unScope :: Expr -> Expr
unScope :: Expr -> Expr
unScope (ScopedExpr ScopeInfo
scope Expr
e) = Expr -> Expr
unScope Expr
e
unScope (QuestionMark MetaInfo
i InteractionId
ii)  = MetaInfo -> InteractionId -> Expr
QuestionMark (MetaInfo
i {metaScope :: ScopeInfo
metaScope = forall a. Null a => a
empty}) InteractionId
ii
unScope (Underscore MetaInfo
i)       = MetaInfo -> Expr
Underscore (MetaInfo
i {metaScope :: ScopeInfo
metaScope = forall a. Null a => a
empty})
unScope Expr
e                    = Expr
e

-- | Remove 'ScopedExpr' wrappers everywhere.
--
--   NB: Unless the implementation of 'ExprLike' for clauses
--   has been finished, this does not work for clauses yet.
deepUnscope :: ExprLike a => a -> a
deepUnscope :: forall a. ExprLike a => a -> a
deepUnscope = forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
unScope

deepUnscopeDecls :: [A.Declaration] -> [A.Declaration]
deepUnscopeDecls :: [Declaration] -> [Declaration]
deepUnscopeDecls = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Declaration -> [Declaration]
deepUnscopeDecl

deepUnscopeDecl :: A.Declaration -> [A.Declaration]
deepUnscopeDecl :: Declaration -> [Declaration]
deepUnscopeDecl (A.ScopedDecl ScopeInfo
_ [Declaration]
ds)              = [Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds
deepUnscopeDecl (A.Mutual MutualInfo
i [Declaration]
ds)                  = [MutualInfo -> [Declaration] -> Declaration
A.Mutual MutualInfo
i ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds)]
deepUnscopeDecl (A.Section Range
i ModuleName
m GeneralizeTelescope
tel [Declaration]
ds)           = [Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section Range
i ModuleName
m (forall a. ExprLike a => a -> a
deepUnscope GeneralizeTelescope
tel) ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds)]
deepUnscopeDecl (A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
bs Expr
e [Declaration]
ds) =
  [ DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir (forall a. ExprLike a => a -> a
deepUnscope DataDefParams
bs) (forall a. ExprLike a => a -> a
deepUnscope Expr
e) ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds) ]
deepUnscopeDecl Declaration
d                                = [forall a. ExprLike a => a -> a
deepUnscope Declaration
d]

-- * Traversal
---------------------------------------------------------------------------

-- Type aliases to abbreviate the quantified foralls which we use to avoid
-- giving in to NoMonoLocalBinds.
type RecurseExprFn m a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a
type RecurseExprRecFn m = forall a. ExprLike a => a -> m a

type FoldExprFn m a = Monoid m => (Expr -> m) -> a -> m
type FoldExprRecFn m = forall a. ExprLike a => a -> m

type TraverseExprFn m a = (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m a
type TraverseExprRecFn m = forall a. ExprLike a => a -> m a

-- | Apply an expression rewriting to every subexpression, inside-out.
--   See "Agda.Syntax.Internal.Generic".
class ExprLike a where
  -- | The first expression is pre-traversal, the second one post-traversal.
  recurseExpr :: RecurseExprFn m a
  default recurseExpr :: (Traversable f, ExprLike a', a ~ f a', Applicative m)
                      => (Expr -> m Expr -> m Expr) -> a -> m a
  recurseExpr = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr

  foldExpr :: FoldExprFn m a
  foldExpr Expr -> m
f = forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr (\ Expr
pre Const m Expr
post -> forall {k} a (b :: k). a -> Const a b
Const (Expr -> m
f Expr
pre) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Const m Expr
post)

  traverseExpr :: TraverseExprFn m a
  traverseExpr Expr -> m Expr
f = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr (\ Expr
pre m Expr
post -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Expr
post)

  mapExpr :: (Expr -> Expr) -> (a -> a)
  mapExpr Expr -> Expr
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
f)

instance ExprLike Expr where
  recurseExpr :: forall m. RecurseExprFn m Expr
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Expr
recurseExpr Expr -> m Expr -> m Expr
f Expr
e0 = Expr -> m Expr -> m Expr
f Expr
e0 forall a b. (a -> b) -> a -> b
$ do
    let
      recurse :: RecurseExprRecFn m
      recurse :: RecurseExprRecFn m
recurse a
e = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e
    case Expr
e0 of
      Var{}                      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Def'{}                     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Proj{}                     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Con{}                      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Lit{}                      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      QuestionMark{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Underscore{}               -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Dot ExprInfo
ei Expr
e                   -> ExprInfo -> Expr -> Expr
Dot ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e
      App AppInfo
ei Expr
e NamedArg Expr
arg               -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse NamedArg Expr
arg
      WithApp ExprInfo
ei Expr
e [Expr]
es            -> ExprInfo -> Expr -> [Expr] -> Expr
WithApp ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse [Expr]
es
      Lam ExprInfo
ei LamBinding
b Expr
e                 -> ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse LamBinding
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Expr
e
      AbsurdLam{}                -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      ExtendedLam ExprInfo
ei DefInfo
di Erased
er QName
x List1 Clause
cls -> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
ExtendedLam ExprInfo
ei DefInfo
di Erased
er QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse List1 Clause
cls
      Pi ExprInfo
ei Telescope1
tel Expr
e                -> ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Telescope1
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Expr
e
      Generalized  Set QName
s Expr
e           -> Set QName -> Expr -> Expr
Generalized Set QName
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e
      Fun ExprInfo
ei Arg Expr
arg Expr
e               -> ExprInfo -> Arg Expr -> Expr -> Expr
Fun ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Arg Expr
arg forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Expr
e
      Let ExprInfo
ei List1 LetBinding
bs Expr
e                -> ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse List1 LetBinding
bs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Expr
e
      Rec ExprInfo
ei RecordAssigns
bs                  -> ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse RecordAssigns
bs
      RecUpdate ExprInfo
ei Expr
e Assigns
bs          -> ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Assigns
bs
      ScopedExpr ScopeInfo
sc Expr
e            -> ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
sc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e
      Quote{}                    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      QuoteTerm{}                -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Unquote{}                  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      DontCare Expr
e                 -> Expr -> Expr
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e
      PatternSyn{}               -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Macro{}                    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0

  foldExpr :: forall m. FoldExprFn m Expr
  foldExpr :: forall m. FoldExprFn m Expr
foldExpr Expr -> m
f Expr
e =
    case Expr
e of
      Var{}                  -> m
m
      Def'{}                 -> m
m
      Proj{}                 -> m
m
      Con{}                  -> m
m
      PatternSyn{}           -> m
m
      Macro{}                -> m
m
      Lit{}                  -> m
m
      QuestionMark{}         -> m
m
      Underscore{}           -> m
m
      Dot ExprInfo
_ Expr
e                -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      App AppInfo
_ Expr
e NamedArg Expr
e'             -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold NamedArg Expr
e'
      WithApp ExprInfo
_ Expr
e [Expr]
es         -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold [Expr]
es
      Lam ExprInfo
_ LamBinding
b Expr
e              -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold LamBinding
b forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      AbsurdLam{}            -> m
m
      ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ List1 Clause
cs -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold List1 Clause
cs
      Pi ExprInfo
_ Telescope1
tel Expr
e             -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Telescope1
tel forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      Generalized Set QName
_ Expr
e        -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      Fun ExprInfo
_ Arg Expr
e Expr
e'             -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Arg Expr
e forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e'
      Let ExprInfo
_ List1 LetBinding
bs Expr
e             -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold List1 LetBinding
bs forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      Rec ExprInfo
_ RecordAssigns
as               -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold RecordAssigns
as
      RecUpdate ExprInfo
_ Expr
e Assigns
as       -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Assigns
as
      ScopedExpr ScopeInfo
_ Expr
e         -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      Quote{}                -> m
m
      QuoteTerm{}            -> m
m
      Unquote{}              -> m
m
      DontCare Expr
e             -> m
m forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
   where
     m :: m
m = Expr -> m
f Expr
e
     fold :: FoldExprRecFn m
     fold :: FoldExprRecFn m
fold = forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f

  traverseExpr :: forall m. TraverseExprFn m Expr
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m Expr
traverseExpr Expr -> m Expr
f Expr
e = do
    let
      trav :: TraverseExprRecFn m
      trav :: TraverseExprRecFn m
trav a
e = forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f a
e
    case Expr
e of
      Var{}                      -> Expr -> m Expr
f Expr
e
      Def'{}                     -> Expr -> m Expr
f Expr
e
      Proj{}                     -> Expr -> m Expr
f Expr
e
      Con{}                      -> Expr -> m Expr
f Expr
e
      Lit{}                      -> Expr -> m Expr
f Expr
e
      QuestionMark{}             -> Expr -> m Expr
f Expr
e
      Underscore{}               -> Expr -> m Expr
f Expr
e
      Dot ExprInfo
ei Expr
e                   -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> Expr -> Expr
Dot ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e
      App AppInfo
ei Expr
e NamedArg Expr
arg               -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav NamedArg Expr
arg
      WithApp ExprInfo
ei Expr
e [Expr]
es            -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> Expr -> [Expr] -> Expr
WithApp ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav [Expr]
es
      Lam ExprInfo
ei LamBinding
b Expr
e                 -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav LamBinding
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Expr
e
      AbsurdLam{}                -> Expr -> m Expr
f Expr
e
      ExtendedLam ExprInfo
ei DefInfo
di Erased
re QName
x List1 Clause
cls -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
ExtendedLam ExprInfo
ei DefInfo
di Erased
re QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav List1 Clause
cls
      Pi ExprInfo
ei Telescope1
tel Expr
e                -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Telescope1
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Expr
e
      Generalized Set QName
s Expr
e            -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Set QName -> Expr -> Expr
Generalized Set QName
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e
      Fun ExprInfo
ei Arg Expr
arg Expr
e               -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> Arg Expr -> Expr -> Expr
Fun ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Arg Expr
arg forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Expr
e
      Let ExprInfo
ei List1 LetBinding
bs Expr
e                -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav List1 LetBinding
bs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Expr
e
      Rec ExprInfo
ei RecordAssigns
bs                  -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav RecordAssigns
bs
      RecUpdate ExprInfo
ei Expr
e Assigns
bs          -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
ei forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Assigns
bs
      ScopedExpr ScopeInfo
sc Expr
e            -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
sc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e
      Quote{}                    -> Expr -> m Expr
f Expr
e
      QuoteTerm{}                -> Expr -> m Expr
f Expr
e
      Unquote{}                  -> Expr -> m Expr
f Expr
e
      DontCare Expr
e                 -> Expr -> m Expr
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> Expr
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e
      PatternSyn{}               -> Expr -> m Expr
f Expr
e
      Macro{}                    -> Expr -> m Expr
f Expr
e

instance ExprLike a => ExprLike (Arg a)
instance ExprLike a => ExprLike (Maybe a)
instance ExprLike a => ExprLike (Named x a)
instance ExprLike a => ExprLike [a]
instance ExprLike a => ExprLike (List1 a)

instance (ExprLike a, ExprLike b) => ExprLike (a, b) where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (a, b)
recurseExpr Expr -> m Expr -> m Expr
f (a
x, b
y) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f b
y

instance ExprLike Void where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Void
recurseExpr Expr -> m Expr -> m Expr
f = forall a. Void -> a
absurd

instance ExprLike a => ExprLike (FieldAssignment' a) where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (FieldAssignment' a)
recurseExpr = forall a. Lens' a (FieldAssignment' a)
exprFieldA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr

instance (ExprLike a, ExprLike b) => ExprLike (Either a b) where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (Either a b)
recurseExpr Expr -> m Expr -> m Expr
f = forall (f :: * -> *) a c b d.
Functor f =>
(a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
traverseEither (forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f)
                                 (forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f)

instance ExprLike BindName where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m BindName
recurseExpr Expr -> m Expr -> m Expr
f = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance ExprLike ModuleName where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m ModuleName
recurseExpr Expr -> m Expr -> m Expr
f = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance ExprLike QName where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m QName
recurseExpr Expr -> m Expr -> m Expr
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance ExprLike LamBinding where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m LamBinding
recurseExpr Expr -> m Expr -> m Expr
f LamBinding
e =
    case LamBinding
e of
      DomainFree Maybe Expr
t NamedArg Binder
x -> Maybe Expr -> NamedArg Binder -> LamBinding
DomainFree forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f Maybe Expr
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure NamedArg Binder
x
      DomainFull TypedBinding
bs  -> TypedBinding -> LamBinding
DomainFull forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f TypedBinding
bs
  foldExpr :: forall m. FoldExprFn m LamBinding
foldExpr Expr -> m
f LamBinding
e =
    case LamBinding
e of
      DomainFree Maybe Expr
t NamedArg Binder
_ -> forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f Maybe Expr
t
      DomainFull TypedBinding
bs -> forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f TypedBinding
bs
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m LamBinding
traverseExpr Expr -> m Expr
f LamBinding
e =
    case LamBinding
e of
      DomainFree Maybe Expr
t NamedArg Binder
x -> Maybe Expr -> NamedArg Binder -> LamBinding
DomainFree forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f Maybe Expr
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure NamedArg Binder
x
      DomainFull TypedBinding
bs  -> TypedBinding -> LamBinding
DomainFull forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f TypedBinding
bs

instance ExprLike GeneralizeTelescope where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m GeneralizeTelescope
recurseExpr  Expr -> m Expr -> m Expr
f (GeneralizeTel Map QName Name
s Telescope
tel) = Map QName Name -> Telescope -> GeneralizeTelescope
GeneralizeTel Map QName Name
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f Telescope
tel
  foldExpr :: forall m. FoldExprFn m GeneralizeTelescope
foldExpr     Expr -> m
f (GeneralizeTel Map QName Name
s Telescope
tel) = forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f Telescope
tel
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m GeneralizeTelescope
traverseExpr Expr -> m Expr
f (GeneralizeTel Map QName Name
s Telescope
tel) = Map QName Name -> Telescope -> GeneralizeTelescope
GeneralizeTel Map QName Name
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f Telescope
tel

instance ExprLike DataDefParams where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m DataDefParams
recurseExpr  Expr -> m Expr -> m Expr
f (DataDefParams Set Name
s [LamBinding]
tel) = Set Name -> [LamBinding] -> DataDefParams
DataDefParams Set Name
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f [LamBinding]
tel
  foldExpr :: forall m. FoldExprFn m DataDefParams
foldExpr     Expr -> m
f (DataDefParams Set Name
s [LamBinding]
tel) = forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f [LamBinding]
tel
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m DataDefParams
traverseExpr Expr -> m Expr
f (DataDefParams Set Name
s [LamBinding]
tel) = Set Name -> [LamBinding] -> DataDefParams
DataDefParams Set Name
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f [LamBinding]
tel

instance ExprLike TypedBindingInfo where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m TypedBindingInfo
recurseExpr Expr -> m Expr -> m Expr
f (TypedBindingInfo Maybe Expr
s Bool
t)  = Maybe Expr -> Bool -> TypedBindingInfo
TypedBindingInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f Maybe Expr
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
t
  foldExpr :: forall m. FoldExprFn m TypedBindingInfo
foldExpr Expr -> m
f (TypedBindingInfo Maybe Expr
s Bool
t)     = forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f Maybe Expr
s
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m TypedBindingInfo
traverseExpr Expr -> m Expr
f (TypedBindingInfo Maybe Expr
s Bool
t) = Maybe Expr -> Bool -> TypedBindingInfo
TypedBindingInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f Maybe Expr
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
t

instance ExprLike TypedBinding where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m TypedBinding
recurseExpr Expr -> m Expr -> m Expr
f TypedBinding
e =
    case TypedBinding
e of
      TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e -> Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f TypedBindingInfo
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure List1 (NamedArg Binder)
xs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f Expr
e
      TLet Range
r List1 LetBinding
ds      -> Range -> List1 LetBinding -> TypedBinding
TLet Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f List1 LetBinding
ds
  foldExpr :: forall m. FoldExprFn m TypedBinding
foldExpr Expr -> m
f TypedBinding
e =
    case TypedBinding
e of
      TBind Range
_ TypedBindingInfo
t List1 (NamedArg Binder)
_ Expr
e -> forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f TypedBindingInfo
t forall a. Monoid a => a -> a -> a
`mappend` forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f Expr
e
      TLet Range
_ List1 LetBinding
ds     -> forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f List1 LetBinding
ds
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m TypedBinding
traverseExpr Expr -> m Expr
f TypedBinding
e =
    case TypedBinding
e of
      TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e -> Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f TypedBindingInfo
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure List1 (NamedArg Binder)
xs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f Expr
e
      TLet Range
r List1 LetBinding
ds      -> Range -> List1 LetBinding -> TypedBinding
TLet Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f List1 LetBinding
ds

instance ExprLike LetBinding where
  recurseExpr :: forall m. RecurseExprFn m LetBinding
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m LetBinding
recurseExpr Expr -> m Expr -> m Expr
f LetBinding
e = do
    let
      recurse :: RecurseExprRecFn m
      recurse :: RecurseExprRecFn m
recurse a
e = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e
    case LetBinding
e of
      LetBind LetInfo
li ArgInfo
ai BindName
x Expr
e Expr
e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
li ArgInfo
ai BindName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Expr
e'
      LetPatBind LetInfo
li Pattern
p Expr
e     -> LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
li forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
recurse Pattern
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
recurse Expr
e
      LetApply{}            -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetOpen{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetDeclaredVariable BindName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e

  foldExpr :: forall m. FoldExprFn m LetBinding
  foldExpr :: forall m. FoldExprFn m LetBinding
foldExpr Expr -> m
f LetBinding
e =
    case LetBinding
e of
      LetBind LetInfo
_ ArgInfo
_ BindName
_ Expr
e Expr
e'    -> FoldExprRecFn m
fold Expr
e forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e'
      LetPatBind LetInfo
_ Pattern
p Expr
e      -> FoldExprRecFn m
fold Pattern
p forall a. Monoid a => a -> a -> a
`mappend` FoldExprRecFn m
fold Expr
e
      LetApply{}            -> forall a. Monoid a => a
mempty
      LetOpen{}             -> forall a. Monoid a => a
mempty
      LetDeclaredVariable BindName
_ -> forall a. Monoid a => a
mempty
    where
      fold :: FoldExprRecFn m
      fold :: FoldExprRecFn m
fold a
e = forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f a
e

  traverseExpr :: forall m. TraverseExprFn m LetBinding
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m LetBinding
traverseExpr Expr -> m Expr
f LetBinding
e = do
    let
      trav :: TraverseExprRecFn m
      trav :: TraverseExprRecFn m
trav a
e = forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
traverseExpr Expr -> m Expr
f a
e
    case LetBinding
e of
      LetBind LetInfo
li ArgInfo
ai BindName
x Expr
e Expr
e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
li ArgInfo
ai BindName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Expr
e'
      LetPatBind LetInfo
li Pattern
p Expr
e     -> LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
li forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraverseExprRecFn m
trav Pattern
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TraverseExprRecFn m
trav Expr
e
      LetApply{}            -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetOpen{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetDeclaredVariable BindName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e

instance ExprLike a => ExprLike (Pattern' a) where

instance ExprLike a => ExprLike (Clause' a) where
  recurseExpr :: forall m. RecurseExprFn m (Clause' a)
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (Clause' a)
recurseExpr Expr -> m Expr -> m Expr
f (Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
ca) = forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
Clause forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec a
lhs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure [ProblemEq]
spats forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec RHS
rhs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec WhereDeclarations
ds forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
ca
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f

instance ExprLike RHS where
  recurseExpr :: forall m. RecurseExprFn m RHS
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m RHS
recurseExpr Expr -> m Expr -> m Expr
f RHS
rhs =
    case RHS
rhs of
      RHS Expr
e Maybe Expr
c                 -> Expr -> Maybe Expr -> RHS
RHS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
c
      AbsurdRHS{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RHS
rhs
      WithRHS QName
x [WithExpr]
es [Clause]
cs         -> QName -> [WithExpr] -> [Clause] -> RHS
WithRHS QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec [WithExpr]
es forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec [Clause]
cs
      RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
ds -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
RewriteRHS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec [RewriteEqn]
xes forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure [ProblemEq]
spats forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec RHS
rhs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec WhereDeclarations
ds
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e

instance (ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (RewriteEqn' qn nm p e)
recurseExpr Expr -> m Expr -> m Expr
f = \case
    Rewrite List1 (qn, e)
es    -> forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f List1 (qn, e)
es
    Invert qn
qn List1 (Named nm (p, e))
pes -> forall qn nm p e.
qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
Invert forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f qn
qn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f List1 (Named nm (p, e))
pes

instance ExprLike WhereDeclarations where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m WhereDeclarations
recurseExpr Expr -> m Expr -> m Expr
f (WhereDecls Maybe ModuleName
a Bool
b Maybe Declaration
c) = Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
WhereDecls Maybe ModuleName
a Bool
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f Maybe Declaration
c

instance ExprLike ModuleApplication where
  recurseExpr :: forall m. RecurseExprFn m ModuleApplication
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m ModuleApplication
recurseExpr Expr -> m Expr -> m Expr
f ModuleApplication
a =
    case ModuleApplication
a of
      SectionApp Telescope
tel ModuleName
m [NamedArg Expr]
es -> Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
SectionApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Telescope
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec ModuleName
m forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec [NamedArg Expr]
es
      RecordModuleInstance{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleApplication
a
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e

instance ExprLike Pragma where
  recurseExpr :: forall m. RecurseExprFn m Pragma
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Pragma
recurseExpr Expr -> m Expr -> m Expr
f Pragma
p =
    case Pragma
p of
      BuiltinPragma RString
s ResolvedName
x           -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      OptionsPragma{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      BuiltinNoDefPragma{}        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      RewritePragma{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      CompilePragma{}             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      StaticPragma{}              -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      InjectivePragma{}           -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      InlinePragma{}              -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      EtaPragma{}                 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      NotProjectionLikePragma{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      DisplayPragma QName
f [NamedArg Pattern]
xs Expr
e        -> QName -> [NamedArg Pattern] -> Expr -> Pragma
DisplayPragma QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec [NamedArg Pattern]
xs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec Expr
e
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e

instance ExprLike LHS where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m LHS
recurseExpr Expr -> m Expr -> m Expr
f (LHS LHSInfo
i LHSCore
p) = LHSInfo -> LHSCore -> LHS
LHS LHSInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f LHSCore
p

instance ExprLike a => ExprLike (LHSCore' a)   where
instance ExprLike a => ExprLike (WithHiding a) where

instance ExprLike SpineLHS where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m SpineLHS
recurseExpr Expr -> m Expr -> m Expr
f (SpineLHS LHSInfo
i QName
x [NamedArg Pattern]
ps) = LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
i QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f [NamedArg Pattern]
ps

instance ExprLike Declaration where
  recurseExpr :: forall m. RecurseExprFn m Declaration
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Declaration
recurseExpr Expr -> m Expr -> m Expr
f Declaration
d =
    case Declaration
d of
      Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe [Occurrence]
mp QName
x Expr
e        -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe [Occurrence]
mp QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Expr
e
      Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Expr
e      -> Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
Generalize Set QName
s DefInfo
i ArgInfo
j QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Expr
e
      Field DefInfo
i QName
x Arg Expr
e               -> DefInfo -> QName -> Arg Expr -> Declaration
Field DefInfo
i QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Arg Expr
e
      Primitive DefInfo
i QName
x Arg Expr
e           -> DefInfo -> QName -> Arg Expr -> Declaration
Primitive DefInfo
i QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Arg Expr
e
      Mutual MutualInfo
i [Declaration]
ds               -> MutualInfo -> [Declaration] -> Declaration
Mutual MutualInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec [Declaration]
ds
      Section Range
i ModuleName
m GeneralizeTelescope
tel [Declaration]
ds        -> Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section Range
i ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec GeneralizeTelescope
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec [Declaration]
ds
      Apply ModuleInfo
i ModuleName
m ModuleApplication
a ScopeCopyInfo
ci ImportDirective
d          -> (\ ModuleApplication
a -> ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply ModuleInfo
i ModuleName
m ModuleApplication
a ScopeCopyInfo
ci ImportDirective
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec ModuleApplication
a
      Import{}                  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Declaration
d
      Pragma Range
i Pragma
p                -> Range -> Pragma -> Declaration
Pragma Range
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Pragma
p
      Open{}                    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Declaration
d
      FunDef DefInfo
i QName
f Delayed
d [Clause]
cs           -> DefInfo -> QName -> Delayed -> [Clause] -> Declaration
FunDef DefInfo
i QName
f Delayed
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec [Clause]
cs
      DataSig DefInfo
i QName
d GeneralizeTelescope
tel Expr
e         -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i QName
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec GeneralizeTelescope
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec Expr
e
      DataDef DefInfo
i QName
d UniverseCheck
uc DataDefParams
bs [Declaration]
cs      -> DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
d UniverseCheck
uc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec DataDefParams
bs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec [Declaration]
cs
      RecSig DefInfo
i QName
r GeneralizeTelescope
tel Expr
e          -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig DefInfo
i QName
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec GeneralizeTelescope
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec Expr
e
      RecDef DefInfo
i QName
r UniverseCheck
uc RecordDirectives
dir DataDefParams
bs Expr
e [Declaration]
ds -> DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
RecDef DefInfo
i QName
r UniverseCheck
uc RecordDirectives
dir forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec DataDefParams
bs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RecurseExprRecFn m
rec [Declaration]
ds
      PatternSynDef QName
f [Arg BindName]
xs Pattern' Void
p      -> QName -> [Arg BindName] -> Pattern' Void -> Declaration
PatternSynDef QName
f [Arg BindName]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Pattern' Void
p
      UnquoteDecl MutualInfo
i [DefInfo]
is [QName]
xs Expr
e     -> MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDecl MutualInfo
i [DefInfo]
is [QName]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Expr
e
      UnquoteDef [DefInfo]
i [QName]
xs Expr
e         -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDef [DefInfo]
i [QName]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Expr
e
      UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e -> [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec Expr
e
      ScopedDecl ScopeInfo
s [Declaration]
ds           -> ScopeInfo -> [Declaration] -> Declaration
ScopedDecl ScopeInfo
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecurseExprRecFn m
rec [Declaration]
ds
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e


-- * Getting all declared names
---------------------------------------------------------------------------

type KName = WithKind QName

-- | Extracts "all" names which are declared in a 'Declaration'.
--
-- Includes: local modules and @where@ clauses.
-- Excludes: @open public@, @let@, @with@ function names, extended lambdas.

class DeclaredNames a where
  declaredNames :: Collection KName m => a -> m

  default declaredNames
     :: (Foldable t, DeclaredNames b, t b ~ a)
     => Collection KName m => a -> m
  declaredNames = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames

instance DeclaredNames a => DeclaredNames [a]
instance DeclaredNames a => DeclaredNames (List1 a)
instance DeclaredNames a => DeclaredNames (Maybe a)
instance DeclaredNames a => DeclaredNames (Arg a)
instance DeclaredNames a => DeclaredNames (Named name a)
instance DeclaredNames a => DeclaredNames (FieldAssignment' a)

instance (DeclaredNames a, DeclaredNames b) => DeclaredNames (Either a b) where
  declaredNames :: forall m. Collection KName m => Either a b -> m
declaredNames = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames

instance (DeclaredNames a, DeclaredNames b) => DeclaredNames (a,b) where
  declaredNames :: forall m. Collection KName m => (a, b) -> m
declaredNames (a
a,b
b) = forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames a
a forall a. Semigroup a => a -> a -> a
<> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames b
b

instance DeclaredNames KName where
  declaredNames :: forall m. Collection KName m => KName -> m
declaredNames = forall el coll. Singleton el coll => el -> coll
singleton

instance DeclaredNames RecordDirectives where
  declaredNames :: forall m. Collection KName m => RecordDirectives -> m
declaredNames (RecordDirectives Maybe (Ranged Induction)
i Maybe HasEta0
_ Maybe Range
_ Maybe QName
c) = m
kc where
    kc :: m
kc = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (forall el coll. Singleton el coll => el -> coll
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
k) Maybe QName
c
    k :: KindOfName
k  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe KindOfName
ConName (Induction -> KindOfName
conKindOfName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ranged a -> a
rangedThing) Maybe (Ranged Induction)
i

instance DeclaredNames Declaration where
  declaredNames :: forall m. Collection KName m => Declaration -> m
declaredNames = \case
      Axiom KindOfName
_ DefInfo
di ArgInfo
_ Maybe [Occurrence]
_ QName
q Expr
_           -> forall el coll. Singleton el coll => el -> coll
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. KindOfName -> a -> WithKind a
`WithKind` QName
q) forall a b. (a -> b) -> a -> b
$
                                      case forall t. DefInfo' t -> IsMacro
defMacro DefInfo
di of
                                        IsMacro
MacroDef    -> KindOfName
MacroName
                                        IsMacro
NotMacroDef -> KindOfName
AxiomName
      Generalize Set QName
_ DefInfo
_ ArgInfo
_ QName
q Expr
_         -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
GeneralizeName QName
q)
      Field DefInfo
_ QName
q Arg Expr
_                  -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FldName QName
q)
      Primitive DefInfo
_ QName
q Arg Expr
_              -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
PrimName QName
q)
      Mutual MutualInfo
_ [Declaration]
decls               -> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      DataSig DefInfo
_ QName
q GeneralizeTelescope
_ Expr
_              -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
q)
      DataDef DefInfo
_ QName
q UniverseCheck
_ DataDefParams
_ [Declaration]
decls        -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
q) forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> m
con [Declaration]
decls
      RecSig DefInfo
_ QName
q GeneralizeTelescope
_ Expr
_               -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
RecName QName
q)
      RecDef DefInfo
_ QName
q UniverseCheck
_ RecordDirectives
dir DataDefParams
_ Expr
_ [Declaration]
decls   -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
RecName QName
q) forall a. Semigroup a => a -> a -> a
<> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RecordDirectives
dir forall a. Semigroup a => a -> a -> a
<> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      PatternSynDef QName
q [Arg BindName]
_ Pattern' Void
_          -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
PatternSynName QName
q)
      UnquoteDecl MutualInfo
_ [DefInfo]
_ [QName]
qs Expr
_         -> forall el coll. Collection el coll => [el] -> coll
fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
OtherDefName) [QName]
qs  -- could be Fun or Axiom
      UnquoteDef [DefInfo]
_ [QName]
qs Expr
_            -> forall el coll. Collection el coll => [el] -> coll
fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FunName) [QName]
qs       -- cannot be Axiom
      UnquoteData [DefInfo]
_ QName
d UniverseCheck
_ [DefInfo]
_ [QName]
cs Expr
_     -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
d) forall a. Semigroup a => a -> a -> a
<> (forall el coll. Collection el coll => [el] -> coll
fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
ConName) [QName]
cs) -- singleton _ <> map (WithKind ConName) cs
      FunDef DefInfo
_ QName
q Delayed
_ [Clause]
cls             -> forall el coll. Singleton el coll => el -> coll
singleton (forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FunName QName
q) forall a. Semigroup a => a -> a -> a
<> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Clause]
cls
      ScopedDecl ScopeInfo
_ [Declaration]
decls           -> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
decls          -> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      Pragma Range
_ Pragma
pragma              -> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames Pragma
pragma
      Apply{}                      -> forall a. Monoid a => a
mempty
      Import{}                     -> forall a. Monoid a => a
mempty
      Open{}                       -> forall a. Monoid a => a
mempty
    where
    con :: Declaration -> m
con = \case
      Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
q Expr
_ -> forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
ConName QName
q
      Declaration
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

instance DeclaredNames Pragma where
  declaredNames :: forall m. Collection KName m => Pragma -> m
declaredNames = \case
    BuiltinNoDefPragma RString
_b KindOfName
kind QName
x -> forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
kind QName
x
    BuiltinPragma{}           -> forall a. Monoid a => a
mempty
    CompilePragma{}           -> forall a. Monoid a => a
mempty
    RewritePragma{}           -> forall a. Monoid a => a
mempty
    StaticPragma{}            -> forall a. Monoid a => a
mempty
    EtaPragma{}               -> forall a. Monoid a => a
mempty
    InjectivePragma{}         -> forall a. Monoid a => a
mempty
    InlinePragma{}            -> forall a. Monoid a => a
mempty
    NotProjectionLikePragma{} -> forall a. Monoid a => a
mempty
    DisplayPragma{}           -> forall a. Monoid a => a
mempty
    OptionsPragma{}           -> forall a. Monoid a => a
mempty

instance DeclaredNames Clause where
  declaredNames :: forall m. Collection KName m => Clause -> m
declaredNames (Clause LHS
_ [ProblemEq]
_ RHS
rhs WhereDeclarations
decls Bool
_) = forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RHS
rhs forall a. Semigroup a => a -> a -> a
<> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames WhereDeclarations
decls

instance DeclaredNames WhereDeclarations where
  declaredNames :: forall m. Collection KName m => WhereDeclarations -> m
declaredNames (WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
ds) = forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames Maybe Declaration
ds

instance DeclaredNames RHS where
  declaredNames :: forall m. Collection KName m => RHS -> m
declaredNames = \case
    RHS Expr
_ Maybe Expr
_                   -> forall a. Monoid a => a
mempty
    RHS
AbsurdRHS                 -> forall a. Monoid a => a
mempty
    WithRHS QName
_q [WithExpr]
_es [Clause]
cls        -> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Clause]
cls
    RewriteRHS [RewriteEqn]
_qes [ProblemEq]
_ RHS
rhs WhereDeclarations
cls -> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RHS
rhs forall a. Semigroup a => a -> a -> a
<> forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames WhereDeclarations
cls

-- Andreas, 2020-04-13: Migration from Agda.Syntax.Abstract.AllNames
--
-- Since we are not interested in names of extended lambdas, we do not
-- traverse into expression.
--
-- However, we keep this code (originally Agda.Syntax.Abstract.AllNames) around
-- should arise a need to collect extended lambda names.

-- instance (DeclaredNames a, DeclaredNames b, DeclaredNames c) => DeclaredNames (a,b,c) where
--   declaredNames (a,b,c) = declaredNames a <> declaredNames b <> declaredNames c

-- instance DeclaredNames RHS where
--   declaredNames = \case
--     RHS e _                  -> declaredNames e
--     AbsurdRHS{}              -> mempty
--     WithRHS q _ cls          -> singleton (WithKind FunName q) <> declaredNames cls
--     RewriteRHS qes _ rhs cls -> declaredNames (qes, rhs, cls)

-- instance DeclaredNames ModuleName where
--   declaredNames _ = mempty

-- instance (DeclaredNames qn, DeclaredNames e) => DeclaredNames (RewriteEqn' qn p e) where
--   declaredNames = \case
--     Rewrite es    -> declaredNames es
--     Invert qn pes -> declaredNames qn <> declaredNames pes

-- instance DeclaredNames Expr where
--   declaredNames = \case
--     Var{}                 -> mempty
--     Def{}                 -> mempty
--     Proj{}                -> mempty
--     Con{}                 -> mempty
--     Lit{}                 -> mempty
--     QuestionMark{}        -> mempty
--     Underscore{}          -> mempty
--     Dot _ e               -> declaredNames e
--     App _ e1 e2           -> declaredNames e1 <> declaredNames e2
--     WithApp _ e es        -> declaredNames e <> declaredNames es
--     Lam _ b e             -> declaredNames b <> declaredNames e
--     AbsurdLam{}           -> mempty
--     ExtendedLam _ _ q cls -> singleton (WithKind FunName q) <> declaredNames cls
--     Pi _ tel e            -> declaredNames tel <> declaredNames e
--     Generalized s e       -> declaredNames e  -- NOT: fromList (map (WithKind GeneralizeName) $ Set.toList s) <> declaredNames e
--     Fun _ e1 e2           -> declaredNames e1 <> declaredNames e2
--     Set{}                 -> mempty
--     Prop{}                -> mempty
--     Let _ lbs e           -> declaredNames lbs <> declaredNames e
--     Rec _ fields          -> declaredNames fields
--     RecUpdate _ e fs      -> declaredNames e <> declaredNames fs
--     ScopedExpr _ e        -> declaredNames e
--     Quote{}               -> mempty
--     QuoteTerm{}           -> mempty
--     Unquote{}             -> mempty
--     DontCare{}            -> mempty
--     PatternSyn{}          -> mempty
--     Macro{}               -> mempty

-- instance DeclaredNames LamBinding where
--   declaredNames DomainFree{}       = mempty
--   declaredNames (DomainFull binds) = declaredNames binds

-- instance DeclaredNames TypedBinding where
--   declaredNames (TBind _ t _ e) = declaredNames (t, e)
--   declaredNames (TLet _ lbs)    = declaredNames lbs

-- instance DeclaredNames LetBinding where
--   declaredNames (LetBind _ _ _ e1 e2)   = declaredNames e1 <> declaredNames e2
--   declaredNames (LetPatBind _ _ e)      = declaredNames e
--   declaredNames (LetApply _ _ app _ _)  = declaredNames app
--   declaredNames LetOpen{}               = mempty
--   declaredNames (LetDeclaredVariable _) = mempty

-- instance DeclaredNames ModuleApplication where
--   declaredNames (SectionApp bindss _ es) = declaredNames bindss <> declaredNames es
--   declaredNames RecordModuleInstance{}   = mempty