module Agda.Syntax.Abstract.Views where

import Prelude hiding (null)

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

import Data.Bifunctor (second)
import Data.Foldable (foldMap)
import Data.DList qualified 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 (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

-- | An 'Expr' viewed as application.
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:
--
--   1. Everything is an application, possibly of itself to 0 arguments.
--
--   2. If the returned head is a projection originating from a post-fix
--      projection, the 'ArgInfo' of the first argument might be incorrect.
--      (See issue #8300.)
--      For instance @x .f@ is valid postfix syntax for @f {{x}}@,
--      but 'appView' turns the former into @f x@.
--      The correct @f {{x}}@ is produced by 'Agda.TypeChecking.Rules.Term.appViewM'.
appView :: Expr -> AppView
appView :: Expr -> AppView
appView = ((AppInfo, Expr) -> Expr) -> AppView' (AppInfo, Expr) -> AppView
forall a b. (a -> b) -> AppView' a -> AppView' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AppInfo, Expr) -> Expr
forall a b. (a, b) -> b
snd (AppView' (AppInfo, Expr) -> AppView)
-> (Expr -> AppView' (AppInfo, Expr)) -> Expr -> AppView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> AppView' (AppInfo, Expr)
appView'

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

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

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

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

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

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

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

unPiView :: PiView -> Expr
unPiView :: PiView -> Expr
unPiView (PiView [(ExprInfo, Telescope1)]
tels Expr
t) = ((ExprInfo, Telescope1) -> Expr -> Expr)
-> Expr -> [(ExprInfo, Telescope1)] -> Expr
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 -> Expr -> Expr)
-> (ExprInfo, Telescope1) -> Expr -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ExprInfo -> Telescope1 -> Expr -> Expr
Pi) Expr
t [(ExprInfo, Telescope1)]
tels

-- | Gather top-level 'AsP'atterns 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 :: Expr -> Expr
unScope (ScopedExpr ScopeInfo
scope Expr
e) = Expr -> Expr
unScope Expr
e
unScope (QuestionMark MetaInfo
i InteractionId
ii)  = MetaInfo -> InteractionId -> Expr
QuestionMark (MetaInfo
i {metaScope = empty}) InteractionId
ii
unScope (Underscore MetaInfo
i)       = MetaInfo -> Expr
Underscore (MetaInfo
i {metaScope = empty})
unScope Expr
e                    = Expr
e

-- | Remove 'ScopedExpr' wrappers everywhere.
--
--   NB: Unless the implementation of 'ExprLike' for clauses
--   has been finished, this does not work for clauses yet.
deepUnscope :: ExprLike a => a -> a
deepUnscope :: forall a. ExprLike a => a -> a
deepUnscope = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
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 PositivityCheck
pc UniverseCheck
uc ForceRecordEta
eta RecordDirectives
dir DataDefParams
bs Expr
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
-> PositivityCheck
-> UniverseCheck
-> ForceRecordEta
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
A.RecDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc ForceRecordEta
eta RecordDirectives
dir (DataDefParams -> DataDefParams
forall a. ExprLike a => a -> a
deepUnscope DataDefParams
bs) (Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
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 = (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)
-> ((Expr -> m Expr -> m Expr) -> a' -> m a')
-> (Expr -> m Expr -> m Expr)
-> a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr -> m Expr) -> a' -> m a'
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a'
recurseExpr

  foldExpr :: FoldExprFn m a
  foldExpr Expr -> 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
. (Expr -> Const m Expr -> Const m Expr) -> a -> Const m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr (\ Expr
pre Const m Expr
post -> m -> Const m Expr
forall {k} a (b :: k). a -> Const a b
Const (Expr -> m
f Expr
pre) Const m Expr -> Const m Expr -> Const m Expr
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 Expr
post)

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

  mapExpr :: (Expr -> Expr) -> (a -> a)
  mapExpr Expr -> Expr
f = 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
. (Expr -> Identity Expr) -> a -> Identity a
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m a
traverseExpr (Expr -> Identity Expr
forall a. a -> Identity a
Identity (Expr -> Identity Expr) -> (Expr -> Expr) -> Expr -> Identity Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
f)

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

  foldExpr :: forall m. FoldExprFn m Expr
  foldExpr :: forall m. FoldExprFn m Expr
foldExpr Expr -> m
f Expr
e =
    case Expr
e of
      Var{}                    -> m
m
      Def'{}                   -> m
m
      Proj{}                   -> m
m
      Con{}                    -> m
m
      PatternSyn{}             -> m
m
      Macro{}                  -> m
m
      Lit{}                    -> m
m
      QuestionMark{}           -> m
m
      Underscore{}             -> m
m
      Dot ExprInfo
_ Expr
e                  -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      App AppInfo
_ Expr
e Arg (Named_ Expr)
e'               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Arg (Named_ Expr) -> m
FoldExprRecFn m
fold Arg (Named_ Expr)
e'
      WithApp ExprInfo
_ Expr
e NonEmpty Expr
es           -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` NonEmpty Expr -> m
FoldExprRecFn m
fold NonEmpty Expr
es
      Lam ExprInfo
_ LamBinding
b Expr
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` Expr -> m
FoldExprRecFn m
fold Expr
e
      AbsurdLam{}              -> m
m
      ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ NonEmpty Clause
cs   -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` NonEmpty Clause -> m
FoldExprRecFn m
fold NonEmpty Clause
cs
      Pi ExprInfo
_ Telescope1
tel Expr
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` Expr -> m
FoldExprRecFn m
fold Expr
e
      Generalized Set1 QName
_ Expr
e          -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      Fun ExprInfo
_ Arg Expr
e Expr
e'               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Arg Expr -> m
FoldExprRecFn m
fold Arg Expr
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e'
      Let ExprInfo
_ NonEmpty LetBinding
bs Expr
e               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` NonEmpty LetBinding -> m
FoldExprRecFn m
fold NonEmpty LetBinding
bs m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      Rec KwRange
_ ExprInfo
_ [RecordAssign]
as               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` [RecordAssign] -> m
FoldExprRecFn m
fold [RecordAssign]
as
      RecUpdate KwRange
_ ExprInfo
_ Expr
e [Assign]
as       -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` [Assign] -> m
FoldExprRecFn m
fold [Assign]
as
      RecWhere KwRange
_ ExprInfo
_ [LetBinding]
e [Assign]
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` [Assign] -> m
FoldExprRecFn m
fold [Assign]
as
      RecUpdateWhere KwRange
_ ExprInfo
_ Expr
e [LetBinding]
x [Assign]
y -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
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` [Assign] -> m
FoldExprRecFn m
fold [Assign]
y
      ScopedExpr ScopeInfo
_ Expr
e           -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      Quote{}                  -> m
m
      QuoteTerm{}              -> m
m
      Unquote{}                -> m
m
      DontCare Expr
e               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      Qualified ModuleName
_ Expr
e            -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      Highlighted Aspects
_ Expr
e          -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
   where
     m :: m
m = Expr -> m
f Expr
e
     fold :: FoldExprRecFn m
     fold :: FoldExprRecFn m
fold = (Expr -> m) -> a -> m
forall m. FoldExprFn m a
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f

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

instance ExprLike a => ExprLike (Arg a)
instance ExprLike a => ExprLike (Maybe a)
instance ExprLike a => ExprLike (Named x a)
instance ExprLike a => ExprLike (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 Expr -> m Expr -> m Expr
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
<$> (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
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
<*> (Expr -> m Expr -> m Expr) -> b -> m b
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m b
recurseExpr Expr -> m Expr -> m Expr
f b
y

instance ExprLike Void where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Void
recurseExpr Expr -> m Expr -> m Expr
f = 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))
-> ((Expr -> m Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr -> m Expr)
-> FieldAssignment' a
-> m (FieldAssignment' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr -> m Expr) -> 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 Expr -> m Expr -> m Expr
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 ((Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f)
                                 ((Expr -> m Expr -> m Expr) -> b -> m b
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m b
recurseExpr Expr -> m Expr -> m Expr
f)

instance ExprLike BindName where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m BindName
recurseExpr Expr -> m Expr -> m Expr
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 Expr -> m Expr -> m Expr
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 Expr -> m Expr -> m Expr
_ = 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 Expr -> m Expr -> m Expr
f LamBinding
e =
    case LamBinding
e of
      DomainFree TacticAttribute' Expr
t NamedArg Binder
x -> TacticAttribute' Expr -> NamedArg Binder -> LamBinding
DomainFree (TacticAttribute' Expr -> NamedArg Binder -> LamBinding)
-> m (TacticAttribute' Expr) -> m (NamedArg Binder -> LamBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr -> m Expr)
-> TacticAttribute' Expr -> m (TacticAttribute' Expr)
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m (TacticAttribute' Expr)
recurseExpr Expr -> m Expr -> m Expr
f TacticAttribute' Expr
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
<$> (Expr -> m Expr -> m Expr) -> TypedBinding -> m TypedBinding
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m TypedBinding
recurseExpr Expr -> m Expr -> m Expr
f TypedBinding
bs
  foldExpr :: forall m. FoldExprFn m LamBinding
foldExpr Expr -> m
f LamBinding
e =
    case LamBinding
e of
      DomainFree TacticAttribute' Expr
t NamedArg Binder
_ -> (Expr -> m) -> TacticAttribute' Expr -> m
forall m. FoldExprFn m (TacticAttribute' Expr)
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f TacticAttribute' Expr
t
      DomainFull TypedBinding
bs -> (Expr -> m) -> TypedBinding -> m
forall m. FoldExprFn m TypedBinding
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f TypedBinding
bs
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m LamBinding
traverseExpr Expr -> m Expr
f LamBinding
e =
    case LamBinding
e of
      DomainFree TacticAttribute' Expr
t NamedArg Binder
x -> TacticAttribute' Expr -> NamedArg Binder -> LamBinding
DomainFree (TacticAttribute' Expr -> NamedArg Binder -> LamBinding)
-> m (TacticAttribute' Expr) -> m (NamedArg Binder -> LamBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr)
-> TacticAttribute' Expr -> m (TacticAttribute' Expr)
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m (TacticAttribute' Expr)
traverseExpr Expr -> m Expr
f TacticAttribute' Expr
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
<$> (Expr -> m Expr) -> TypedBinding -> m TypedBinding
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m TypedBinding
traverseExpr Expr -> m Expr
f TypedBinding
bs

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

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

instance ExprLike TypedBindingInfo where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m TypedBindingInfo
recurseExpr Expr -> m Expr -> m Expr
f (TypedBindingInfo TacticAttribute' Expr
s Bool
t)  = TacticAttribute' Expr -> Bool -> TypedBindingInfo
TypedBindingInfo (TacticAttribute' Expr -> Bool -> TypedBindingInfo)
-> m (TacticAttribute' Expr) -> m (Bool -> TypedBindingInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr -> m Expr)
-> TacticAttribute' Expr -> m (TacticAttribute' Expr)
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m (TacticAttribute' Expr)
recurseExpr Expr -> m Expr -> m Expr
f TacticAttribute' Expr
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 Expr -> m
f (TypedBindingInfo TacticAttribute' Expr
s Bool
t)     = (Expr -> m) -> TacticAttribute' Expr -> m
forall m. FoldExprFn m (TacticAttribute' Expr)
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f TacticAttribute' Expr
s
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m TypedBindingInfo
traverseExpr Expr -> m Expr
f (TypedBindingInfo TacticAttribute' Expr
s Bool
t) = TacticAttribute' Expr -> Bool -> TypedBindingInfo
TypedBindingInfo (TacticAttribute' Expr -> Bool -> TypedBindingInfo)
-> m (TacticAttribute' Expr) -> m (Bool -> TypedBindingInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr)
-> TacticAttribute' Expr -> m (TacticAttribute' Expr)
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m (TacticAttribute' Expr)
traverseExpr Expr -> m Expr
f TacticAttribute' Expr
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 Expr -> m Expr -> m Expr
f TypedBinding
e =
    case TypedBinding
e of
      TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e -> Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r (TypedBindingInfo
 -> List1 (NamedArg Binder) -> Expr -> TypedBinding)
-> m TypedBindingInfo
-> m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr -> m Expr)
-> TypedBindingInfo -> m TypedBindingInfo
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m TypedBindingInfo
recurseExpr Expr -> m Expr -> m Expr
f TypedBindingInfo
t m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
-> m (List1 (NamedArg Binder)) -> m (Expr -> 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 (Expr -> TypedBinding) -> m Expr -> 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
<*> (Expr -> m Expr -> m Expr) -> Expr -> m Expr
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m Expr
recurseExpr Expr -> m Expr -> m Expr
f Expr
e
      TLet Range
r NonEmpty LetBinding
ds      -> Range -> NonEmpty LetBinding -> TypedBinding
TLet Range
r (NonEmpty LetBinding -> TypedBinding)
-> m (NonEmpty LetBinding) -> m TypedBinding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr -> m Expr)
-> NonEmpty LetBinding -> m (NonEmpty LetBinding)
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m (NonEmpty LetBinding)
recurseExpr Expr -> m Expr -> m Expr
f NonEmpty LetBinding
ds
  foldExpr :: forall m. FoldExprFn m TypedBinding
foldExpr Expr -> m
f TypedBinding
e =
    case TypedBinding
e of
      TBind Range
_ TypedBindingInfo
t List1 (NamedArg Binder)
_ Expr
e -> (Expr -> m) -> TypedBindingInfo -> m
forall m. FoldExprFn m TypedBindingInfo
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f TypedBindingInfo
t m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> Expr -> m
forall m. FoldExprFn m Expr
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f Expr
e
      TLet Range
_ NonEmpty LetBinding
ds     -> (Expr -> m) -> NonEmpty LetBinding -> m
forall m. FoldExprFn m (NonEmpty LetBinding)
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f NonEmpty LetBinding
ds
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m TypedBinding
traverseExpr Expr -> m Expr
f TypedBinding
e =
    case TypedBinding
e of
      TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e -> Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r (TypedBindingInfo
 -> List1 (NamedArg Binder) -> Expr -> TypedBinding)
-> m TypedBindingInfo
-> m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> TypedBindingInfo -> m TypedBindingInfo
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m TypedBindingInfo
traverseExpr Expr -> m Expr
f TypedBindingInfo
t m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
-> m (List1 (NamedArg Binder)) -> m (Expr -> 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 (Expr -> TypedBinding) -> m Expr -> 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
<*> (Expr -> m Expr) -> Expr -> m Expr
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m Expr
traverseExpr Expr -> m Expr
f Expr
e
      TLet Range
r NonEmpty LetBinding
ds      -> Range -> NonEmpty LetBinding -> TypedBinding
TLet Range
r (NonEmpty LetBinding -> TypedBinding)
-> m (NonEmpty LetBinding) -> m TypedBinding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> NonEmpty LetBinding -> m (NonEmpty LetBinding)
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m (NonEmpty LetBinding)
traverseExpr Expr -> m Expr
f NonEmpty LetBinding
ds

instance ExprLike LetBinding where
  recurseExpr :: forall m. RecurseExprFn m LetBinding
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m LetBinding
recurseExpr Expr -> m Expr -> m Expr
f LetBinding
e = do
    let
      recurse :: RecurseExprRecFn m
      recurse :: RecurseExprRecFn m
recurse a
e = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e
    case LetBinding
e of
      LetBind LetInfo
li ArgInfo
ai BindName
x Expr
e Expr
e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
li ArgInfo
ai BindName
x (Expr -> Expr -> LetBinding) -> m Expr -> m (Expr -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e m (Expr -> LetBinding) -> m Expr -> 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
<*> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e'
      LetAxiom LetInfo
li ArgInfo
ai BindName
x Expr
e    -> LetInfo -> ArgInfo -> BindName -> Expr -> LetBinding
LetAxiom LetInfo
li ArgInfo
ai BindName
x (Expr -> LetBinding) -> m Expr -> m LetBinding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e
      LetPatBind LetInfo
li ArgInfo
ai Pattern
p Expr
e  -> LetInfo -> ArgInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
li ArgInfo
ai (Pattern -> Expr -> LetBinding)
-> m Pattern -> m (Expr -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> m Pattern
RecurseExprRecFn m
recurse Pattern
p m (Expr -> LetBinding) -> m Expr -> 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
<*> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
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 Expr -> m
f LetBinding
e =
    case LetBinding
e of
      LetBind LetInfo
_ ArgInfo
_ BindName
_ Expr
e Expr
e'    -> Expr -> m
FoldExprRecFn m
fold Expr
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e'
      LetAxiom LetInfo
_ ArgInfo
_ BindName
_ Expr
e      -> Expr -> m
FoldExprRecFn m
fold Expr
e
      LetPatBind LetInfo
_ ArgInfo
_ Pattern
p Expr
e    -> Pattern -> m
FoldExprRecFn m
fold Pattern
p m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
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 = (Expr -> m) -> a -> m
forall m. FoldExprFn m a
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> m
f a
e

  traverseExpr :: forall m. TraverseExprFn m LetBinding
  traverseExpr :: forall (m :: * -> *). TraverseExprFn m LetBinding
traverseExpr Expr -> m Expr
f LetBinding
e = do
    let
      trav :: TraverseExprRecFn m
      trav :: TraverseExprRecFn m
trav a
e = (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
forall (m :: * -> *). TraverseExprFn m a
traverseExpr Expr -> m Expr
f a
e
    case LetBinding
e of
      LetBind LetInfo
li ArgInfo
ai BindName
x Expr
e Expr
e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
li ArgInfo
ai BindName
x (Expr -> Expr -> LetBinding) -> m Expr -> m (Expr -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e m (Expr -> LetBinding) -> m Expr -> 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
<*> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e'
      LetAxiom LetInfo
li ArgInfo
ai BindName
x Expr
e    -> LetInfo -> ArgInfo -> BindName -> Expr -> LetBinding
LetAxiom LetInfo
li ArgInfo
ai BindName
x (Expr -> LetBinding) -> m Expr -> m LetBinding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e
      LetPatBind LetInfo
li ArgInfo
ai Pattern
p Expr
e  -> LetInfo -> ArgInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
li ArgInfo
ai (Pattern -> Expr -> LetBinding)
-> m Pattern -> m (Expr -> LetBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> m Pattern
TraverseExprRecFn m
trav Pattern
p m (Expr -> LetBinding) -> m Expr -> 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
<*> Expr -> m Expr
TraverseExprRecFn m
trav Expr
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 Expr -> m Expr -> m Expr
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 = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f

instance ExprLike RHS where
  recurseExpr :: forall m. RecurseExprFn m RHS
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m RHS
recurseExpr Expr -> m Expr -> m Expr
f RHS
rhs =
    case RHS
rhs of
      RHS Expr
e Maybe Expr
c                 -> Expr -> Maybe Expr -> RHS
RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
rec Expr
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 NonEmpty WithExpr
es NonEmpty Clause
cs         -> QName -> NonEmpty WithExpr -> NonEmpty Clause -> RHS
WithRHS QName
x (NonEmpty WithExpr -> NonEmpty Clause -> RHS)
-> m (NonEmpty WithExpr) -> m (NonEmpty Clause -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty WithExpr -> m (NonEmpty WithExpr)
RecurseExprRecFn m
rec NonEmpty WithExpr
es m (NonEmpty Clause -> RHS) -> m (NonEmpty 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
<*> NonEmpty Clause -> m (NonEmpty Clause)
RecurseExprRecFn m
rec NonEmpty 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 = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e

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

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

instance ExprLike ModuleApplication where
  recurseExpr :: forall m. RecurseExprFn m ModuleApplication
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m ModuleApplication
recurseExpr Expr -> m Expr -> m Expr
f ModuleApplication
a =
    case ModuleApplication
a of
      SectionApp [TypedBinding]
tel ModuleName
m [Arg (Named_ Expr)]
es -> [TypedBinding]
-> ModuleName -> [Arg (Named_ Expr)] -> ModuleApplication
SectionApp ([TypedBinding]
 -> ModuleName -> [Arg (Named_ Expr)] -> ModuleApplication)
-> m [TypedBinding]
-> m (ModuleName -> [Arg (Named_ Expr)] -> ModuleApplication)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypedBinding] -> m [TypedBinding]
RecurseExprRecFn m
rec [TypedBinding]
tel m (ModuleName -> [Arg (Named_ Expr)] -> ModuleApplication)
-> m ModuleName -> m ([Arg (Named_ Expr)] -> 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 ([Arg (Named_ Expr)] -> ModuleApplication)
-> m [Arg (Named_ Expr)] -> 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
<*> [Arg (Named_ Expr)] -> m [Arg (Named_ Expr)]
RecurseExprRecFn m
rec [Arg (Named_ Expr)]
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 = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e

instance ExprLike Pragma where
  recurseExpr :: forall m. RecurseExprFn m Pragma
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Pragma
recurseExpr Expr -> m Expr -> m Expr
f Pragma
p =
    case Pragma
p of
      BuiltinPragma RString
s ResolvedName
x           -> 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
      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 Expr
e        -> QName -> [NamedArg Pattern] -> Expr -> Pragma
DisplayPragma QName
f ([NamedArg Pattern] -> Expr -> Pragma)
-> m [NamedArg Pattern] -> m (Expr -> 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 (Expr -> Pragma) -> m Expr -> 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
<*> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec a
e = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e

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

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

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

instance ExprLike Declaration where
  recurseExpr :: forall m. RecurseExprFn m Declaration
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Declaration
recurseExpr Expr -> m Expr -> m Expr
f Declaration
d =
    case Declaration
d of
      Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe PragmaPolarities
mp QName
x Expr
e        -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Expr
-> Declaration
Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe PragmaPolarities
mp QName
x (Expr -> Declaration) -> m Expr -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
      Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Expr
e      -> Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
Generalize Set QName
s DefInfo
i ArgInfo
j QName
x (Expr -> Declaration) -> m Expr -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
      Field DefInfo
i QName
x Arg Expr
e               -> DefInfo -> QName -> Arg Expr -> Declaration
Field DefInfo
i QName
x (Arg Expr -> Declaration) -> m (Arg Expr) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Expr -> m (Arg Expr)
RecurseExprRecFn m
rec Arg Expr
e
      Primitive DefInfo
i QName
x Arg Expr
e           -> DefInfo -> QName -> Arg Expr -> Declaration
Primitive DefInfo
i QName
x (Arg Expr -> Declaration) -> m (Arg Expr) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Expr -> m (Arg Expr)
RecurseExprRecFn m
rec Arg Expr
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 NonEmpty Clause
cs             -> DefInfo -> QName -> NonEmpty Clause -> Declaration
FunDef DefInfo
i QName
f (NonEmpty Clause -> Declaration)
-> m (NonEmpty Clause) -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty Clause -> m (NonEmpty Clause)
RecurseExprRecFn m
rec NonEmpty Clause
cs
      DataSig DefInfo
i Erased
er QName
d GeneralizeTelescope
tel Expr
e      -> DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i Erased
er QName
d (GeneralizeTelescope -> Expr -> Declaration)
-> m GeneralizeTelescope -> m (Expr -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralizeTelescope -> m GeneralizeTelescope
RecurseExprRecFn m
rec GeneralizeTelescope
tel m (Expr -> Declaration) -> m Expr -> 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
<*> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
      DataDef DefInfo
i QName
d PositivityCheck
pc UniverseCheck
uc DataDefParams
bs [Declaration]
cs   -> DefInfo
-> QName
-> PositivityCheck
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
d PositivityCheck
pc 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 Expr
e       -> DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig DefInfo
i Erased
er QName
r (GeneralizeTelescope -> Expr -> Declaration)
-> m GeneralizeTelescope -> m (Expr -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralizeTelescope -> m GeneralizeTelescope
RecurseExprRecFn m
rec GeneralizeTelescope
tel m (Expr -> Declaration) -> m Expr -> 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
<*> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
      RecDef DefInfo
i QName
r PositivityCheck
pc UniverseCheck
uc ForceRecordEta
eta RecordDirectives
dir DataDefParams
bs Expr
e [Declaration]
ds -> DefInfo
-> QName
-> PositivityCheck
-> UniverseCheck
-> ForceRecordEta
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
RecDef DefInfo
i QName
r PositivityCheck
pc UniverseCheck
uc ForceRecordEta
eta RecordDirectives
dir (DataDefParams -> Expr -> [Declaration] -> Declaration)
-> m DataDefParams -> m (Expr -> [Declaration] -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDefParams -> m DataDefParams
RecurseExprRecFn m
rec DataDefParams
bs m (Expr -> [Declaration] -> Declaration)
-> m Expr -> 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
<*> Expr -> m Expr
RecurseExprRecFn m
rec Expr
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 Expr
e     -> MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDecl MutualInfo
i [DefInfo]
is [QName]
xs (Expr -> Declaration) -> m Expr -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
      UnquoteDef [DefInfo]
i [QName]
xs Expr
e         -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDef [DefInfo]
i [QName]
xs (Expr -> Declaration) -> m Expr -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
rec Expr
e
      UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e -> [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs (Expr -> Declaration) -> m Expr -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
rec Expr
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 = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e


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

type KName = WithKind QName

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

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

  default declaredNames
     :: (Foldable t, DeclaredNames b, t b ~ a)
     => Collection KName m => a -> m
  declaredNames = (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 Expr
_           -> 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 Expr
_         -> 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 Expr
_                  -> 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 Expr
_              -> 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
_ Expr
_            -> 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 PositivityCheck
_ 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
_ Expr
_             -> 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 PositivityCheck
_ UniverseCheck
_ ForceRecordEta
_ RecordDirectives
dir DataDefParams
_ Expr
_ [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 Expr
_         -> [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 Expr
_            -> [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 Expr
_     -> 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 NonEmpty 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
<> NonEmpty Clause -> m
forall m. Collection KName m => NonEmpty Clause -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames NonEmpty 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 Expr
_ -> 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
    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 Expr
_ Maybe Expr
_                   -> m
forall a. Monoid a => a
mempty
    RHS
AbsurdRHS                 -> m
forall a. Monoid a => a
mempty
    WithRHS QName
_q NonEmpty WithExpr
_es NonEmpty Clause
cls        -> NonEmpty Clause -> m
forall m. Collection KName m => NonEmpty Clause -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames NonEmpty 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