module Agda.Syntax.Abstract.Views where

import Prelude hiding (null)

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

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

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

import Agda.Utils.Either
import Agda.Utils.List1 (List1)
import Agda.Utils.List1 qualified as 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 -> b) -> AppView' a -> AppView' b)
-> (forall a b. a -> AppView' b -> AppView' a) -> Functor AppView'
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
$cfmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
fmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
$c<$ :: forall a b. a -> AppView' b -> AppView' a
<$ :: forall a b. a -> AppView' b -> AppView' a
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 :: Type -> AppView
appView = ((AppInfo, Type) -> Type) -> AppView' (AppInfo, Type) -> AppView
forall a b. (a -> b) -> AppView' a -> AppView' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AppInfo, Type) -> Type
forall a b. (a, b) -> b
snd (AppView' (AppInfo, Type) -> AppView)
-> (Type -> AppView' (AppInfo, Type)) -> Type -> AppView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> AppView' (AppInfo, Type)
appView'

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

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

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

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

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

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

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

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

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

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

-- | Remove top 'ScopedExpr' wrappers.
unScope :: Expr -> Expr
unScope :: Type -> Type
unScope (ScopedExpr ScopeInfo
scope Type
e) = Type -> Type
unScope Type
e
unScope (QuestionMark MetaInfo
i InteractionId
ii)  = MetaInfo -> InteractionId -> Type
QuestionMark (MetaInfo
i {metaScope = empty}) InteractionId
ii
unScope (Underscore MetaInfo
i)       = MetaInfo -> Type
Underscore (MetaInfo
i {metaScope = empty})
unScope Type
e                    = Type
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 = (Type -> Type) -> a -> a
forall a. ExprLike a => (Type -> Type) -> a -> a
mapExpr Type -> Type
unScope

class DeepUnscopeDecls t where
  deepUnscopeDecls :: t A.Declaration -> t A.Declaration

instance DeepUnscopeDecls [] where
  deepUnscopeDecls :: [A.Declaration] -> [A.Declaration]
  deepUnscopeDecls :: [Declaration] -> [Declaration]
deepUnscopeDecls = (Declaration -> [Declaration]) -> [Declaration] -> [Declaration]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (List1 Declaration -> [Item (List1 Declaration)]
List1 Declaration -> [Declaration]
forall l. IsList l => l -> [Item l]
List1.toList (List1 Declaration -> [Declaration])
-> (Declaration -> List1 Declaration)
-> Declaration
-> [Declaration]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> List1 Declaration
deepUnscopeDecl)

instance DeepUnscopeDecls List1 where
  deepUnscopeDecls :: List1 A.Declaration -> List1 A.Declaration
  deepUnscopeDecls :: List1 Declaration -> List1 Declaration
deepUnscopeDecls = (Declaration -> List1 Declaration)
-> List1 Declaration -> List1 Declaration
forall a b. (a -> List1 b) -> List1 a -> List1 b
List1.concatMap1 Declaration -> List1 Declaration
deepUnscopeDecl
    -- Want to use foldMap1 here, but it requires base >= 4.18 (GHC 9.6)

deepUnscopeDecl :: A.Declaration -> List1 A.Declaration
deepUnscopeDecl :: Declaration -> List1 Declaration
deepUnscopeDecl = \case
  A.ScopedDecl ScopeInfo
_ List1 Declaration
ds           -> List1 Declaration -> List1 Declaration
forall (t :: * -> *).
DeepUnscopeDecls t =>
t Declaration -> t Declaration
deepUnscopeDecls List1 Declaration
ds
  A.Mutual MutualInfo
i List1 Declaration
ds               -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ MutualInfo -> List1 Declaration -> Declaration
A.Mutual MutualInfo
i (List1 Declaration -> List1 Declaration
forall (t :: * -> *).
DeepUnscopeDecls t =>
t Declaration -> t Declaration
deepUnscopeDecls List1 Declaration
ds)
  A.Section Range
i Erased
e ModuleName
m GeneralizeTelescope
tel [Declaration]
ds      -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section Range
i Erased
e ModuleName
m (GeneralizeTelescope -> GeneralizeTelescope
forall a. ExprLike a => a -> a
deepUnscope GeneralizeTelescope
tel)
                                   ([Declaration] -> [Declaration]
forall (t :: * -> *).
DeepUnscopeDecls t =>
t Declaration -> t Declaration
deepUnscopeDecls [Declaration]
ds)
  A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
bs Type
e [Declaration]
ds -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Type
-> [Declaration]
-> Declaration
A.RecDef DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir (DataDefParams -> DataDefParams
forall a. ExprLike a => a -> a
deepUnscope DataDefParams
bs)
                                     (Type -> Type
forall a. ExprLike a => a -> a
deepUnscope Type
e)
                                     ([Declaration] -> [Declaration]
forall (t :: * -> *).
DeepUnscopeDecls t =>
t Declaration -> t Declaration
deepUnscopeDecls [Declaration]
ds)
  Declaration
d                           -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Declaration -> Declaration
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 = (a' -> m a') -> a -> m a
(a' -> m a') -> f a' -> m (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((a' -> m a') -> a -> m a)
-> ((Type -> m Type -> m Type) -> a' -> m a')
-> (Type -> m Type -> m Type)
-> a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> m Type -> m Type) -> a' -> m a'
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a'
recurseExpr

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

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

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

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

  foldExpr :: forall m. FoldExprFn m Expr
  foldExpr :: forall m. FoldExprFn m Type
foldExpr Type -> m
f Type
e =
    case Type
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
_ Type
e                  -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      App AppInfo
_ Type
e NamedArg Type
e'               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` NamedArg Type -> m
FoldExprRecFn m
fold NamedArg Type
e'
      WithApp ExprInfo
_ Type
e List1 Type
es           -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` List1 Type -> m
FoldExprRecFn m
fold List1 Type
es
      Lam ExprInfo
_ LamBinding
b Type
e                -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` LamBinding -> m
FoldExprRecFn m
fold LamBinding
b m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      AbsurdLam{}              -> m
m
      ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ List1 Clause
cs   -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` List1 Clause -> m
FoldExprRecFn m
fold List1 Clause
cs
      Pi ExprInfo
_ Telescope1
tel Type
e               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Telescope1 -> m
FoldExprRecFn m
fold Telescope1
tel m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      Generalized Set1 QName
_ Type
e          -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      Fun ExprInfo
_ Arg Type
e Type
e'               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Arg Type -> m
FoldExprRecFn m
fold Arg Type
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e'
      Let ExprInfo
_ List1 LetBinding
bs Type
e               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` List1 LetBinding -> m
FoldExprRecFn m
fold List1 LetBinding
bs m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      Rec KwRange
_ ExprInfo
_ RecordAssigns
as               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` RecordAssigns -> m
FoldExprRecFn m
fold RecordAssigns
as
      RecUpdate KwRange
_ ExprInfo
_ Type
e Assigns
as       -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Assigns -> m
FoldExprRecFn m
fold Assigns
as
      RecWhere KwRange
_ ExprInfo
_ [LetBinding]
e Assigns
as        -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` [LetBinding] -> m
FoldExprRecFn m
fold [LetBinding]
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Assigns -> m
FoldExprRecFn m
fold Assigns
as
      RecUpdateWhere KwRange
_ ExprInfo
_ Type
e [LetBinding]
x Assigns
y -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` [LetBinding] -> m
FoldExprRecFn m
fold [LetBinding]
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Assigns -> m
FoldExprRecFn m
fold Assigns
y
      ScopedExpr ScopeInfo
_ Type
e           -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      Quote{}                  -> m
m
      QuoteTerm{}              -> m
m
      Unquote{}                -> m
m
      DontCare Type
e               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
      Qualified ModuleName
_ Type
e            -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Type -> m
FoldExprRecFn m
fold Type
e
   where
     m :: m
m = Type -> m
f Type
e
     fold :: FoldExprRecFn m
     fold :: FoldExprRecFn m
fold = (Type -> m) -> a -> m
forall m. FoldExprFn m a
forall a m. ExprLike a => FoldExprFn m a
foldExpr Type -> m
f

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  traverseExpr :: forall m. TraverseExprFn m LetBinding
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m LetBinding
traverseExpr Type -> m Type
f LetBinding
e = do
    let
      trav :: TraverseExprRecFn m
      trav :: TraverseExprRecFn m
trav a
e = (Type -> m Type) -> a -> m a
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m a
traverseExpr Type -> m Type
f a
e
    case LetBinding
e of
      LetBind LetInfo
li ArgInfo
ai BindName
x Type
e Type
e'  -> LetInfo -> ArgInfo -> BindName -> Type -> Type -> LetBinding
LetBind LetInfo
li ArgInfo
ai BindName
x (Type -> Type -> LetBinding) -> m Type -> m (Type -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
TraverseExprRecFn m
trav Type
e m (Type -> LetBinding) -> m Type -> m LetBinding
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
TraverseExprRecFn m
trav Type
e'
      LetAxiom LetInfo
li ArgInfo
ai BindName
x Type
e    -> LetInfo -> ArgInfo -> BindName -> Type -> LetBinding
LetAxiom LetInfo
li ArgInfo
ai BindName
x (Type -> LetBinding) -> m Type -> m LetBinding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
TraverseExprRecFn m
trav Type
e
      LetPatBind LetInfo
li ArgInfo
ai Pattern
p Type
e  -> LetInfo -> ArgInfo -> Pattern -> Type -> LetBinding
LetPatBind LetInfo
li ArgInfo
ai (Pattern -> Type -> LetBinding)
-> m Pattern -> m (Type -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> m Pattern
TraverseExprRecFn m
trav Pattern
p m (Type -> LetBinding) -> m Type -> m LetBinding
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
TraverseExprRecFn m
trav Type
e
      LetApply{}            -> LetBinding -> m LetBinding
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetOpen{}             -> LetBinding -> m LetBinding
forall a. a -> m a
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 Type -> m Type -> m Type
f (Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Catchall
ca) = a
-> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause' a
forall lhs.
lhs
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Catchall
-> Clause' lhs
Clause (a
 -> [ProblemEq]
 -> RHS
 -> WhereDeclarations
 -> Catchall
 -> Clause' a)
-> m a
-> m ([ProblemEq]
      -> RHS -> WhereDeclarations -> Catchall -> Clause' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
RecurseExprRecFn m
rec a
lhs m ([ProblemEq]
   -> RHS -> WhereDeclarations -> Catchall -> Clause' a)
-> m [ProblemEq]
-> m (RHS -> WhereDeclarations -> Catchall -> Clause' a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [ProblemEq] -> m [ProblemEq]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ProblemEq]
spats m (RHS -> WhereDeclarations -> Catchall -> Clause' a)
-> m RHS -> m (WhereDeclarations -> Catchall -> Clause' a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RHS -> m RHS
RecurseExprRecFn m
rec RHS
rhs m (WhereDeclarations -> Catchall -> Clause' a)
-> m WhereDeclarations -> m (Catchall -> Clause' a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> WhereDeclarations -> m WhereDeclarations
RecurseExprRecFn m
rec WhereDeclarations
ds m (Catchall -> Clause' a) -> m Catchall -> m (Clause' a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Catchall -> m Catchall
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Catchall
ca
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec = (Type -> m Type -> m Type) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Type -> m Type -> m Type
f

instance ExprLike RHS where
  recurseExpr :: forall m. RecurseExprFn m RHS
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m RHS
recurseExpr Type -> m Type -> m Type
f RHS
rhs =
    case RHS
rhs of
      RHS Type
e Maybe Expr
c                 -> Type -> Maybe Expr -> RHS
RHS (Type -> Maybe Expr -> RHS) -> m Type -> m (Maybe Expr -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
RecurseExprRecFn m
rec Type
e m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Expr -> m (Maybe Expr)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
c
      AbsurdRHS{}             -> RHS -> m RHS
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RHS
rhs
      WithRHS QName
x List1 WithExpr
es List1 Clause
cs         -> QName -> List1 WithExpr -> List1 Clause -> RHS
WithRHS QName
x (List1 WithExpr -> List1 Clause -> RHS)
-> m (List1 WithExpr) -> m (List1 Clause -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 WithExpr -> m (List1 WithExpr)
RecurseExprRecFn m
rec List1 WithExpr
es m (List1 Clause -> RHS) -> m (List1 Clause) -> m RHS
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> List1 Clause -> m (List1 Clause)
RecurseExprRecFn m
rec List1 Clause
cs
      RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
ds -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
RewriteRHS ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS)
-> m [RewriteEqn]
-> m ([ProblemEq] -> RHS -> WhereDeclarations -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RewriteEqn] -> m [RewriteEqn]
RecurseExprRecFn m
rec [RewriteEqn]
xes m ([ProblemEq] -> RHS -> WhereDeclarations -> RHS)
-> m [ProblemEq] -> m (RHS -> WhereDeclarations -> RHS)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [ProblemEq] -> m [ProblemEq]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ProblemEq]
spats m (RHS -> WhereDeclarations -> RHS)
-> m RHS -> m (WhereDeclarations -> RHS)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RHS -> m RHS
RecurseExprRecFn m
rec RHS
rhs m (WhereDeclarations -> RHS) -> m WhereDeclarations -> m RHS
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> WhereDeclarations -> m WhereDeclarations
RecurseExprRecFn m
rec WhereDeclarations
ds
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = (Type -> m Type -> m Type) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Type -> m Type -> m Type
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 Type -> m Type -> m Type
f = \case
    Rewrite List1 (qn, e)
es    -> List1 (qn, e) -> RewriteEqn' qn nm p e
forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite (List1 (qn, e) -> RewriteEqn' qn nm p e)
-> m (List1 (qn, e)) -> m (RewriteEqn' qn nm p e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Type -> m Type) -> List1 (qn, e) -> m (List1 (qn, e))
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m (List1 (qn, e))
recurseExpr Type -> m Type -> m Type
f List1 (qn, e)
es
    Invert qn
qn List1 (Named nm (p, e))
pes -> qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
forall qn nm p e.
qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
Invert (qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
-> m qn -> m (List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Type -> m Type) -> qn -> m qn
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m qn
recurseExpr Type -> m Type -> m Type
f qn
qn m (List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
-> m (List1 (Named nm (p, e))) -> m (RewriteEqn' qn nm p e)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> m Type -> m Type)
-> List1 (Named nm (p, e)) -> m (List1 (Named nm (p, e)))
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m (List1 (Named nm (p, e)))
recurseExpr Type -> m Type -> m Type
f List1 (Named nm (p, e))
pes
    LeftLet List1 (p, e)
pes   -> List1 (p, e) -> RewriteEqn' qn nm p e
forall qn nm p e. List1 (p, e) -> RewriteEqn' qn nm p e
LeftLet (List1 (p, e) -> RewriteEqn' qn nm p e)
-> m (List1 (p, e)) -> m (RewriteEqn' qn nm p e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Type -> m Type) -> List1 (p, e) -> m (List1 (p, e))
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m (List1 (p, e))
recurseExpr Type -> m Type -> m Type
f List1 (p, e)
pes

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

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

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

instance ExprLike LHS where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m LHS
recurseExpr Type -> m Type -> m Type
f (LHS LHSInfo
i LHSCore
p) = LHSInfo -> LHSCore -> LHS
LHS LHSInfo
i (LHSCore -> LHS) -> m LHSCore -> m LHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Type -> m Type) -> LHSCore -> m LHSCore
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m LHSCore
recurseExpr Type -> m Type -> m Type
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 Type -> m Type -> m Type
f (SpineLHS LHSInfo
i QName
x [NamedArg Pattern]
ps) = LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
i QName
x ([NamedArg Pattern] -> SpineLHS)
-> m [NamedArg Pattern] -> m SpineLHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Type -> m Type)
-> [NamedArg Pattern] -> m [NamedArg Pattern]
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m [NamedArg Pattern]
recurseExpr Type -> m Type -> m Type
f [NamedArg Pattern]
ps

instance ExprLike Declaration where
  recurseExpr :: forall m. RecurseExprFn m Declaration
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Declaration
recurseExpr Type -> m Type -> m Type
f Declaration
d =
    case Declaration
d of
      Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe PragmaPolarities
mp QName
x Type
e        -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Type
-> Declaration
Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe PragmaPolarities
mp QName
x (Type -> Declaration) -> m Type -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
RecurseExprRecFn m
rec Type
e
      Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Type
e      -> Set QName -> DefInfo -> ArgInfo -> QName -> Type -> Declaration
Generalize Set QName
s DefInfo
i ArgInfo
j QName
x (Type -> Declaration) -> m Type -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
RecurseExprRecFn m
rec Type
e
      Field DefInfo
i QName
x Arg Type
e               -> DefInfo -> QName -> Arg Type -> Declaration
Field DefInfo
i QName
x (Arg Type -> Declaration) -> m (Arg Type) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Type -> m (Arg Type)
RecurseExprRecFn m
rec Arg Type
e
      Primitive DefInfo
i QName
x Arg Type
e           -> DefInfo -> QName -> Arg Type -> Declaration
Primitive DefInfo
i QName
x (Arg Type -> Declaration) -> m (Arg Type) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Type -> m (Arg Type)
RecurseExprRecFn m
rec Arg Type
e
      Mutual MutualInfo
i List1 Declaration
ds               -> MutualInfo -> List1 Declaration -> Declaration
Mutual MutualInfo
i (List1 Declaration -> Declaration)
-> m (List1 Declaration) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Declaration -> m (List1 Declaration)
RecurseExprRecFn m
rec List1 Declaration
ds
      Section Range
i Erased
e ModuleName
m GeneralizeTelescope
tel [Declaration]
ds      -> Range
-> Erased
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section Range
i Erased
e ModuleName
m (GeneralizeTelescope -> [Declaration] -> Declaration)
-> m GeneralizeTelescope -> m ([Declaration] -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralizeTelescope -> m GeneralizeTelescope
RecurseExprRecFn m
rec GeneralizeTelescope
tel m ([Declaration] -> Declaration)
-> m [Declaration] -> m Declaration
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
ds
      Apply ModuleInfo
i Erased
e ModuleName
m ModuleApplication
a ScopeCopyInfo
ci ImportDirective
d        -> (\ModuleApplication
a -> ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply ModuleInfo
i Erased
e ModuleName
m ModuleApplication
a ScopeCopyInfo
ci ImportDirective
d) (ModuleApplication -> Declaration)
-> m ModuleApplication -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleApplication -> m ModuleApplication
RecurseExprRecFn m
rec ModuleApplication
a
      Import{}                  -> Declaration -> m Declaration
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Declaration
d
      Pragma Range
i Pragma
p                -> Range -> Pragma -> Declaration
Pragma Range
i (Pragma -> Declaration) -> m Pragma -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pragma -> m Pragma
RecurseExprRecFn m
rec Pragma
p
      Open{}                    -> Declaration -> m Declaration
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Declaration
d
      FunDef DefInfo
i QName
f List1 Clause
cs             -> DefInfo -> QName -> List1 Clause -> Declaration
FunDef DefInfo
i QName
f (List1 Clause -> Declaration) -> m (List1 Clause) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Clause -> m (List1 Clause)
RecurseExprRecFn m
rec List1 Clause
cs
      DataSig DefInfo
i Erased
er QName
d GeneralizeTelescope
tel Type
e      -> DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Type -> Declaration
DataSig DefInfo
i Erased
er QName
d (GeneralizeTelescope -> Type -> Declaration)
-> m GeneralizeTelescope -> m (Type -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralizeTelescope -> m GeneralizeTelescope
RecurseExprRecFn m
rec GeneralizeTelescope
tel m (Type -> Declaration) -> m Type -> m Declaration
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
RecurseExprRecFn m
rec Type
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 (DataDefParams -> [Declaration] -> Declaration)
-> m DataDefParams -> m ([Declaration] -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDefParams -> m DataDefParams
RecurseExprRecFn m
rec DataDefParams
bs m ([Declaration] -> Declaration)
-> m [Declaration] -> m Declaration
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
cs
      RecSig DefInfo
i Erased
er QName
r GeneralizeTelescope
tel Type
e       -> DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Type -> Declaration
RecSig DefInfo
i Erased
er QName
r (GeneralizeTelescope -> Type -> Declaration)
-> m GeneralizeTelescope -> m (Type -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralizeTelescope -> m GeneralizeTelescope
RecurseExprRecFn m
rec GeneralizeTelescope
tel m (Type -> Declaration) -> m Type -> m Declaration
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
RecurseExprRecFn m
rec Type
e
      RecDef DefInfo
i QName
r UniverseCheck
uc RecordDirectives
dir DataDefParams
bs Type
e [Declaration]
ds -> DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Type
-> [Declaration]
-> Declaration
RecDef DefInfo
i QName
r UniverseCheck
uc RecordDirectives
dir (DataDefParams -> Type -> [Declaration] -> Declaration)
-> m DataDefParams -> m (Type -> [Declaration] -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDefParams -> m DataDefParams
RecurseExprRecFn m
rec DataDefParams
bs m (Type -> [Declaration] -> Declaration)
-> m Type -> m ([Declaration] -> Declaration)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
RecurseExprRecFn m
rec Type
e m ([Declaration] -> Declaration)
-> m [Declaration] -> m Declaration
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
ds
      PatternSynDef QName
f [WithHiding BindName]
xs Pattern' Void
p      -> QName -> [WithHiding BindName] -> Pattern' Void -> Declaration
PatternSynDef QName
f [WithHiding BindName]
xs (Pattern' Void -> Declaration)
-> m (Pattern' Void) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' Void -> m (Pattern' Void)
RecurseExprRecFn m
rec Pattern' Void
p
      UnquoteDecl MutualInfo
i [DefInfo]
is [QName]
xs Type
e     -> MutualInfo -> [DefInfo] -> [QName] -> Type -> Declaration
UnquoteDecl MutualInfo
i [DefInfo]
is [QName]
xs (Type -> Declaration) -> m Type -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
RecurseExprRecFn m
rec Type
e
      UnquoteDef [DefInfo]
i [QName]
xs Type
e         -> [DefInfo] -> [QName] -> Type -> Declaration
UnquoteDef [DefInfo]
i [QName]
xs (Type -> Declaration) -> m Type -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
RecurseExprRecFn m
rec Type
e
      UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Type
e -> [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Type
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs (Type -> Declaration) -> m Type -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
RecurseExprRecFn m
rec Type
e
      ScopedDecl ScopeInfo
s List1 Declaration
ds           -> ScopeInfo -> List1 Declaration -> Declaration
ScopedDecl ScopeInfo
s (List1 Declaration -> Declaration)
-> m (List1 Declaration) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Declaration -> m (List1 Declaration)
RecurseExprRecFn m
rec List1 Declaration
ds
      UnfoldingDecl Range
r [QName]
ds        -> Range -> [QName] -> Declaration
UnfoldingDecl Range
r ([QName] -> Declaration) -> m [QName] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QName] -> m [QName]
RecurseExprRecFn m
rec [QName]
ds
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = (Type -> m Type -> m Type) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Type -> m Type -> m Type
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 = (b -> m) -> t b -> m
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> m
forall m. Collection KName m => b -> m
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 = (a -> m) -> (b -> m) -> Either a b -> m
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> m
forall m. Collection KName m => a -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames b -> m
forall m. Collection KName m => b -> m
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) = a -> m
forall m. Collection KName m => a -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames a
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> b -> m
forall m. Collection KName m => b -> m
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 = KName -> m
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 (Ranged HasEta0)
_ Maybe Range
_ RecordConName
c) = m
kc where
    kc :: m
kc = case RecordConName
c of
      NamedRecCon QName
c -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> KName -> m
forall a b. (a -> b) -> a -> b
$ KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
k QName
c
      FreshRecCon{} -> m
forall a. Monoid a => a
mempty
    k :: KindOfName
k  = KindOfName
-> (Ranged Induction -> KindOfName)
-> Maybe (Ranged Induction)
-> KindOfName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe KindOfName
ConName (Induction -> KindOfName
conKindOfName (Induction -> KindOfName)
-> (Ranged Induction -> Induction)
-> Ranged Induction
-> KindOfName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged Induction -> Induction
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 PragmaPolarities
_ QName
q Type
_           -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> (KindOfName -> KName) -> KindOfName -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
`WithKind` QName
q) (KindOfName -> m) -> KindOfName -> m
forall a b. (a -> b) -> a -> b
$
                                      case DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
defMacro DefInfo
di of
                                        IsMacro
MacroDef    -> KindOfName
MacroName
                                        IsMacro
NotMacroDef -> KindOfName
AxiomName
      Generalize Set QName
_ DefInfo
_ ArgInfo
_ QName
q Type
_         -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
GeneralizeName QName
q)
      Field DefInfo
_ QName
q Arg Type
_                  -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FldName QName
q)
      Primitive DefInfo
_ QName
q Arg Type
_              -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
PrimName QName
q)
      Mutual MutualInfo
_ List1 Declaration
decls               -> List1 Declaration -> m
forall m. Collection KName m => List1 Declaration -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames List1 Declaration
decls
      DataSig DefInfo
_ Erased
_ QName
q GeneralizeTelescope
_ Type
_            -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
q)
      DataDef DefInfo
_ QName
q UniverseCheck
_ DataDefParams
_ [Declaration]
decls        -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
q) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (Declaration -> m) -> [Declaration] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> m
con [Declaration]
decls
      RecSig DefInfo
_ Erased
_ QName
q GeneralizeTelescope
_ Type
_             -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
RecName QName
q)
      RecDef DefInfo
_ QName
q UniverseCheck
_ RecordDirectives
dir DataDefParams
_ Type
_ [Declaration]
decls   -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
RecName QName
q) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> RecordDirectives -> m
forall m. Collection KName m => RecordDirectives -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RecordDirectives
dir m -> m -> m
forall a. Semigroup a => a -> a -> a
<> [Declaration] -> m
forall m. Collection KName m => [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      PatternSynDef QName
q [WithHiding BindName]
_ Pattern' Void
_          -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
PatternSynName QName
q)
      UnquoteDecl MutualInfo
_ [DefInfo]
_ [QName]
qs Type
_         -> [KName] -> m
forall el coll. Collection el coll => [el] -> coll
fromList ([KName] -> m) -> [KName] -> m
forall a b. (a -> b) -> a -> b
$ (QName -> KName) -> [QName] -> [KName]
forall a b. (a -> b) -> [a] -> [b]
map (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
OtherDefName) [QName]
qs  -- could be Fun or Axiom
      UnquoteDef [DefInfo]
_ [QName]
qs Type
_            -> [KName] -> m
forall el coll. Collection el coll => [el] -> coll
fromList ([KName] -> m) -> [KName] -> m
forall a b. (a -> b) -> a -> b
$ (QName -> KName) -> [QName] -> [KName]
forall a b. (a -> b) -> [a] -> [b]
map (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FunName) [QName]
qs       -- cannot be Axiom
      UnquoteData [DefInfo]
_ QName
d UniverseCheck
_ [DefInfo]
_ [QName]
cs Type
_     -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
d) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> [KName] -> m
forall el coll. Collection el coll => [el] -> coll
fromList ((QName -> KName) -> [QName] -> [KName]
forall a b. (a -> b) -> [a] -> [b]
map (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
ConName) [QName]
cs) -- singleton _ <> map (WithKind ConName) cs
      FunDef DefInfo
_ QName
q List1 Clause
cls               -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FunName QName
q) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> List1 Clause -> m
forall m. Collection KName m => List1 Clause -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames List1 Clause
cls
      ScopedDecl ScopeInfo
_ List1 Declaration
decls           -> List1 Declaration -> m
forall m. Collection KName m => List1 Declaration -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames List1 Declaration
decls
      Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
decls        -> [Declaration] -> m
forall m. Collection KName m => [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      Pragma Range
_ Pragma
pragma              -> Pragma -> m
forall m. Collection KName m => Pragma -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames Pragma
pragma
      Apply{}                      -> m
forall a. Monoid a => a
mempty
      Import{}                     -> m
forall a. Monoid a => a
mempty
      Open{}                       -> m
forall a. Monoid a => a
mempty
      UnfoldingDecl{}              -> m
forall a. Monoid a => a
mempty
    where
    con :: Declaration -> m
con = \case
      Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe PragmaPolarities
_ QName
q Type
_ -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> KName -> m
forall a b. (a -> b) -> a -> b
$ KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
ConName QName
q
      Declaration
_ -> m
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 -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> KName -> m
forall a b. (a -> b) -> a -> b
$ KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
kind QName
x
    BuiltinPragma{}           -> m
forall a. Monoid a => a
mempty
    CompilePragma{}           -> m
forall a. Monoid a => a
mempty
    RewritePragma{}           -> m
forall a. Monoid a => a
mempty
    StaticPragma{}            -> m
forall a. Monoid a => a
mempty
    EtaPragma{}               -> m
forall a. Monoid a => a
mempty
    InjectivePragma{}         -> m
forall a. Monoid a => a
mempty
    InjectiveForInferencePragma{} -> m
forall a. Monoid a => a
mempty
    InlinePragma{}            -> m
forall a. Monoid a => a
mempty
    NotProjectionLikePragma{} -> m
forall a. Monoid a => a
mempty
    DisplayPragma{}           -> m
forall a. Monoid a => a
mempty
    OptionsPragma{}           -> m
forall a. Monoid a => a
mempty
    OverlapPragma{}           -> m
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 Catchall
_) = RHS -> m
forall m. Collection KName m => RHS -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RHS
rhs m -> m -> m
forall a. Semigroup a => a -> a -> a
<> WhereDeclarations -> m
forall m. Collection KName m => WhereDeclarations -> m
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) = Maybe Declaration -> m
forall m. Collection KName m => Maybe Declaration -> m
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 Type
_ Maybe Expr
_                   -> m
forall a. Monoid a => a
mempty
    RHS
AbsurdRHS                 -> m
forall a. Monoid a => a
mempty
    WithRHS QName
_q List1 WithExpr
_es List1 Clause
cls        -> List1 Clause -> m
forall m. Collection KName m => List1 Clause -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames List1 Clause
cls
    RewriteRHS [RewriteEqn]
_qes [ProblemEq]
_ RHS
rhs WhereDeclarations
cls -> RHS -> m
forall m. Collection KName m => RHS -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RHS
rhs m -> m -> m
forall a. Semigroup a => a -> a -> a
<> WhereDeclarations -> m
forall m. Collection KName m => WhereDeclarations -> m
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

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