module Agda.Syntax.Abstract.Views where

import Prelude hiding (null)

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

import Data.Foldable (foldMap)
import Data.Semigroup ((<>))
import Data.Void

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

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

import Agda.Utils.Impossible


data AppView' arg = Application Expr [NamedArg arg]
  deriving ((forall a b. (a -> 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
<$ :: forall a b. a -> AppView' b -> AppView' a
$c<$ :: forall a b. a -> AppView' b -> AppView' a
fmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
$cfmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
Functor)

type AppView = AppView' Expr

-- | Gather applications to expose head and spine.
--
--   Note: everything is an application, possibly of itself to 0 arguments
appView :: Expr -> AppView
appView :: Expr -> AppView
appView = ((AppInfo, Expr) -> Expr) -> AppView' (AppInfo, Expr) -> AppView
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 =
  case Expr
e of
    App AppInfo
i Expr
e1 NamedArg Expr
e2
      | Dot ExprInfo
_ Expr
e2' <- Expr -> Expr
unScope (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
e2
      , Just Expr
f <- Expr -> Maybe Expr
maybeProjTurnPostfix Expr
e2'
      , NamedArg Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg 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 (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application Expr
f [(AppInfo, Expr) -> NamedArg (AppInfo, Expr)
forall a. a -> NamedArg a
defaultNamedArg (AppInfo
i, Expr
e1)]
    App AppInfo
i Expr
e1 NamedArg Expr
arg
      | Application Expr
hd [NamedArg (AppInfo, Expr)]
es <- Expr -> AppView' (AppInfo, Expr)
appView' Expr
e1
                   -> Expr -> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application Expr
hd ([NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr))
-> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
forall a b. (a -> b) -> a -> b
$ [NamedArg (AppInfo, Expr)]
es [NamedArg (AppInfo, Expr)]
-> [NamedArg (AppInfo, Expr)] -> [NamedArg (AppInfo, Expr)]
forall a. [a] -> [a] -> [a]
++ [((Named NamedName Expr -> Named_ (AppInfo, Expr))
-> NamedArg Expr -> NamedArg (AppInfo, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName Expr -> Named_ (AppInfo, Expr))
 -> NamedArg Expr -> NamedArg (AppInfo, Expr))
-> ((Expr -> (AppInfo, Expr))
    -> Named NamedName Expr -> Named_ (AppInfo, Expr))
-> (Expr -> (AppInfo, Expr))
-> NamedArg Expr
-> NamedArg (AppInfo, Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> (AppInfo, Expr))
-> Named NamedName Expr -> Named_ (AppInfo, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (AppInfo
i,) NamedArg Expr
arg]
    ScopedExpr ScopeInfo
_ Expr
e -> Expr -> AppView' (AppInfo, Expr)
appView' Expr
e
    Expr
_              -> Expr -> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application Expr
e []

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

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

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

lamView :: Expr -> LamView
lamView :: Expr -> LamView
lamView (Lam ExprInfo
i LamBinding
b Expr
e) = LamBinding -> LamView -> LamView
cons LamBinding
b (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

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

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

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

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

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

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

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

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

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

-- | Apply an expression rewriting to every subexpression, inside-out.
--   See "Agda.Syntax.Internal.Generic".
class ExprLike a where
  -- | The first expression is pre-traversal, the second one post-traversal.
  recurseExpr :: RecurseExprFn m a
  default recurseExpr :: (Traversable f, ExprLike a', a ~ f a', Applicative m)
                      => (Expr -> m Expr -> m Expr) -> a -> m a
  recurseExpr = (a' -> m a') -> a -> m a
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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
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
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 (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
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
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
recurseExpr Expr -> m Expr -> m Expr
f a
e
    case Expr
e0 of
      Var{}                      -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Def'{}                     -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Proj{}                     -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Con{}                      -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Lit{}                      -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      QuestionMark{}             -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Underscore{}               -> Expr -> m Expr
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 NamedArg Expr
arg               -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
ei (Expr -> NamedArg Expr -> Expr)
-> m Expr -> m (NamedArg Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e m (NamedArg Expr -> Expr) -> m (NamedArg Expr) -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamedArg Expr -> m (NamedArg Expr)
RecurseExprRecFn m
recurse NamedArg Expr
arg
      WithApp ExprInfo
ei Expr
e [Expr]
es            -> ExprInfo -> Expr -> [Expr] -> Expr
WithApp ExprInfo
ei (Expr -> [Expr] -> Expr) -> m Expr -> m ([Expr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e m ([Expr] -> Expr) -> m [Expr] -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Expr] -> m [Expr]
RecurseExprRecFn m
recurse [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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      ExtendedLam ExprInfo
ei DefInfo
di Erased
er QName
x List1 Clause
cls -> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
ExtendedLam ExprInfo
ei DefInfo
di Erased
er QName
x (List1 Clause -> Expr) -> m (List1 Clause) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Clause -> m (List1 Clause)
RecurseExprRecFn m
recurse List1 Clause
cls
      Pi ExprInfo
ei Telescope1
tel 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e
      Generalized  Set QName
s Expr
e           -> Set QName -> Expr -> Expr
Generalized Set 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e
      Let ExprInfo
ei List1 LetBinding
bs Expr
e                -> ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
ei (List1 LetBinding -> Expr -> Expr)
-> m (List1 LetBinding) -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 LetBinding -> m (List1 LetBinding)
RecurseExprRecFn m
recurse List1 LetBinding
bs m (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e
      ETel Telescope
tel                   -> Telescope -> Expr
ETel (Telescope -> Expr) -> m Telescope -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Telescope
RecurseExprRecFn m
recurse Telescope
tel
      Rec ExprInfo
ei RecordAssigns
bs                  -> ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
ei (RecordAssigns -> Expr) -> m RecordAssigns -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecordAssigns -> m RecordAssigns
RecurseExprRecFn m
recurse RecordAssigns
bs
      RecUpdate ExprInfo
ei Expr
e Assigns
bs          -> ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
ei (Expr -> Assigns -> Expr) -> m Expr -> m (Assigns -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e m (Assigns -> Expr) -> m Assigns -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Assigns -> m Assigns
RecurseExprRecFn m
recurse Assigns
bs
      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 (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      QuoteTerm{}                -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Unquote{}                  -> Expr -> m Expr
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 (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0
      Macro{}                    -> Expr -> m Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e0

  foldExpr :: forall m. FoldExprFn m Expr
  foldExpr :: forall m. FoldExprFn m Expr
foldExpr Expr -> m
f Expr
e =
    case Expr
e of
      Var{}                  -> m
m
      Def'{}                 -> m
m
      Proj{}                 -> m
m
      Con{}                  -> m
m
      PatternSyn{}           -> m
m
      Macro{}                -> m
m
      Lit{}                  -> m
m
      QuestionMark{}         -> m
m
      Underscore{}           -> m
m
      Dot ExprInfo
_ Expr
e                -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      App AppInfo
_ Expr
e NamedArg 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` NamedArg Expr -> m
FoldExprRecFn m
fold NamedArg Expr
e'
      WithApp ExprInfo
_ Expr
e [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` [Expr] -> m
FoldExprRecFn m
fold [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
_ List1 Clause
cs -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` List1 Clause -> m
FoldExprRecFn m
fold List1 Clause
cs
      Pi ExprInfo
_ Telescope1
tel 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 Set 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
_ List1 LetBinding
bs Expr
e             -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` List1 LetBinding -> m
FoldExprRecFn m
fold List1 LetBinding
bs m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Expr -> m
FoldExprRecFn m
fold Expr
e
      ETel Telescope
tel               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` Telescope -> m
FoldExprRecFn m
fold Telescope
tel
      Rec ExprInfo
_ RecordAssigns
as               -> m
m m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` RecordAssigns -> m
FoldExprRecFn m
fold RecordAssigns
as
      RecUpdate ExprInfo
_ Expr
e Assigns
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` Assigns -> m
FoldExprRecFn m
fold Assigns
as
      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
   where
     m :: m
m = Expr -> m
f Expr
e
     fold :: FoldExprRecFn m
     fold :: FoldExprRecFn m
fold = (Expr -> m) -> a -> m
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
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 NamedArg 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 -> NamedArg Expr -> Expr
App AppInfo
ei (Expr -> NamedArg Expr -> Expr)
-> m Expr -> m (NamedArg Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e m (NamedArg Expr -> Expr) -> m (NamedArg Expr) -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NamedArg Expr -> m (NamedArg Expr)
TraverseExprRecFn m
trav NamedArg Expr
arg
      WithApp ExprInfo
ei Expr
e [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 -> [Expr] -> Expr
WithApp ExprInfo
ei (Expr -> [Expr] -> Expr) -> m Expr -> m ([Expr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e m ([Expr] -> Expr) -> m [Expr] -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Expr] -> m [Expr]
TraverseExprRecFn m
trav [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 (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 List1 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 -> List1 Clause -> Expr
ExtendedLam ExprInfo
ei DefInfo
di Erased
re QName
x (List1 Clause -> Expr) -> m (List1 Clause) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Clause -> m (List1 Clause)
TraverseExprRecFn m
trav List1 Clause
cls
      Pi ExprInfo
ei Telescope1
tel 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e
      Generalized Set 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
=<< Set QName -> Expr -> Expr
Generalized Set 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e
      Let ExprInfo
ei List1 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 -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
ei (List1 LetBinding -> Expr -> Expr)
-> m (List1 LetBinding) -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 LetBinding -> m (List1 LetBinding)
TraverseExprRecFn m
trav List1 LetBinding
bs m (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e
      ETel Telescope
tel                   -> Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Telescope -> Expr
ETel (Telescope -> Expr) -> m Telescope -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Telescope
TraverseExprRecFn m
trav Telescope
tel
      Rec ExprInfo
ei RecordAssigns
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
=<< ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
ei (RecordAssigns -> Expr) -> m RecordAssigns -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecordAssigns -> m RecordAssigns
TraverseExprRecFn m
trav RecordAssigns
bs
      RecUpdate ExprInfo
ei Expr
e Assigns
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
=<< ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
ei (Expr -> Assigns -> Expr) -> m Expr -> m (Assigns -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e m (Assigns -> Expr) -> m Assigns -> m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Assigns -> m Assigns
TraverseExprRecFn m
trav Assigns
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

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

instance (ExprLike a, ExprLike b) => ExprLike (a, b) where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (a, b)
recurseExpr Expr -> m Expr -> m Expr
f (a
x, b
y) = (,) (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
recurseExpr Expr -> m Expr -> m Expr
f a
x m (b -> (a, b)) -> m b -> m (a, 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
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. Lens' a (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
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
recurseExpr Expr -> m Expr -> m Expr
f)
                                 ((Expr -> m Expr -> m Expr) -> b -> m b
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f)

instance ExprLike BindName where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m BindName
recurseExpr Expr -> m Expr -> m Expr
f = BindName -> m BindName
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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure

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

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

instance ExprLike DataDefParams where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m DataDefParams
recurseExpr  Expr -> m Expr -> m Expr
f (DataDefParams Set Name
s [LamBinding]
tel) = Set Name -> [LamBinding] -> DataDefParams
DataDefParams Set Name
s ([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
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 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
traverseExpr Expr -> m Expr
f [LamBinding]
tel

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

instance ExprLike LetBinding where
  recurseExpr :: forall m. RecurseExprFn m LetBinding
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m LetBinding
recurseExpr Expr -> m Expr -> m Expr
f LetBinding
e = do
    let
      recurse :: RecurseExprRecFn m
      recurse :: RecurseExprRecFn m
recurse a
e = (Expr -> m Expr -> m Expr) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
recurseExpr Expr -> m Expr -> m Expr
f a
e
    case LetBinding
e of
      LetBind LetInfo
li ArgInfo
ai BindName
x Expr
e Expr
e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
li ArgInfo
ai BindName
x (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
RecurseExprRecFn m
recurse Expr
e'
      LetPatBind LetInfo
li Pattern
p Expr
e     -> LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
li (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetOpen{}             -> LetBinding -> m LetBinding
forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetDeclaredVariable BindName
_ -> LetBinding -> m LetBinding
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'
      LetPatBind LetInfo
_ 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
      LetDeclaredVariable BindName
_ -> m
forall a. Monoid a => a
mempty
    where
      fold :: FoldExprRecFn m
      fold :: FoldExprRecFn m
fold a
e = (Expr -> m) -> a -> m
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
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
TraverseExprRecFn m
trav Expr
e'
      LetPatBind LetInfo
li Pattern
p Expr
e     -> LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
li (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetOpen{}             -> LetBinding -> m LetBinding
forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e
      LetDeclaredVariable BindName
_ -> LetBinding -> m LetBinding
forall (f :: * -> *) a. Applicative f => a -> f a
pure LetBinding
e

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

instance ExprLike a => ExprLike (Clause' a) where
  recurseExpr :: forall m. RecurseExprFn m (Clause' a)
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (Clause' a)
recurseExpr Expr -> m Expr -> m Expr
f (Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
ca) = a -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
Clause (a -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a)
-> m a
-> m ([ProblemEq] -> RHS -> WhereDeclarations -> Bool -> 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 -> Bool -> Clause' a)
-> m [ProblemEq]
-> m (RHS -> WhereDeclarations -> Bool -> Clause' a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [ProblemEq] -> m [ProblemEq]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ProblemEq]
spats m (RHS -> WhereDeclarations -> Bool -> Clause' a)
-> m RHS -> m (WhereDeclarations -> Bool -> Clause' a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RHS -> m RHS
RecurseExprRecFn m
rec RHS
rhs m (WhereDeclarations -> Bool -> Clause' a)
-> m WhereDeclarations -> m (Bool -> Clause' a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> WhereDeclarations -> m WhereDeclarations
RecurseExprRecFn m
rec WhereDeclarations
ds m (Bool -> Clause' a) -> m Bool -> m (Clause' a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> m Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
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
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Expr -> m (Maybe Expr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
c
      AbsurdRHS{}             -> RHS -> m RHS
forall (f :: * -> *) a. Applicative f => a -> f a
pure RHS
rhs
      WithRHS QName
x [WithExpr]
es [Clause]
cs         -> QName -> [WithExpr] -> [Clause] -> RHS
WithRHS QName
x ([WithExpr] -> [Clause] -> RHS)
-> m [WithExpr] -> m ([Clause] -> RHS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [WithExpr] -> m [WithExpr]
RecurseExprRecFn m
rec [WithExpr]
es m ([Clause] -> RHS) -> m [Clause] -> m RHS
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Clause] -> m [Clause]
RecurseExprRecFn m
rec [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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [ProblemEq] -> m [ProblemEq]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ProblemEq]
spats m (RHS -> WhereDeclarations -> RHS)
-> m RHS -> m (WhereDeclarations -> RHS)
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 (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
recurseExpr Expr -> m Expr -> m Expr
f a
e

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

instance ExprLike WhereDeclarations where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m WhereDeclarations
recurseExpr Expr -> m Expr -> m Expr
f (WhereDecls Maybe ModuleName
a Maybe Declaration
b) = Maybe ModuleName -> Maybe Declaration -> WhereDeclarations
WhereDecls Maybe ModuleName
a (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
recurseExpr Expr -> m Expr -> m Expr
f Maybe Declaration
b

instance ExprLike ModuleApplication where
  recurseExpr :: forall m. RecurseExprFn m ModuleApplication
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m ModuleApplication
recurseExpr Expr -> m Expr -> m Expr
f ModuleApplication
a =
    case ModuleApplication
a of
      SectionApp Telescope
tel ModuleName
m [NamedArg Expr]
es -> Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
SectionApp (Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication)
-> m Telescope
-> m (ModuleName -> [NamedArg Expr] -> ModuleApplication)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Telescope
RecurseExprRecFn m
rec Telescope
tel m (ModuleName -> [NamedArg Expr] -> ModuleApplication)
-> m ModuleName -> m ([NamedArg Expr] -> ModuleApplication)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ModuleName -> m ModuleName
RecurseExprRecFn m
rec ModuleName
m m ([NamedArg Expr] -> ModuleApplication)
-> m [NamedArg Expr] -> m ModuleApplication
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [NamedArg Expr] -> m [NamedArg Expr]
RecurseExprRecFn m
rec [NamedArg Expr]
es
      RecordModuleInstance{} -> ModuleApplication -> m ModuleApplication
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
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 (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      OptionsPragma{}             -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      BuiltinNoDefPragma{}        -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      RewritePragma{}             -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      CompilePragma{}             -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      StaticPragma{}              -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      InjectivePragma{}           -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      InlinePragma{}              -> Pragma -> m Pragma
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pragma
p
      EtaPragma{}                 -> Pragma -> m Pragma
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 (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
recurseExpr Expr -> m Expr -> m Expr
f a
e

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

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

instance ExprLike SpineLHS where
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m SpineLHS
recurseExpr Expr -> m Expr -> m Expr
f (SpineLHS LHSInfo
i QName
x [NamedArg Pattern]
ps) = LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
i QName
x ([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
recurseExpr Expr -> m Expr -> m Expr
f [NamedArg Pattern]
ps

instance ExprLike Declaration where
  recurseExpr :: forall m. RecurseExprFn m Declaration
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m Declaration
recurseExpr Expr -> m Expr -> m Expr
f Declaration
d =
    case Declaration
d of
      Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe [Occurrence]
mp QName
x Expr
e        -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
Axiom KindOfName
a DefInfo
d ArgInfo
i Maybe [Occurrence]
mp QName
x (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 [Declaration]
ds               -> MutualInfo -> [Declaration] -> Declaration
Mutual MutualInfo
i ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
ds
      Section Range
i ModuleName
m GeneralizeTelescope
tel [Declaration]
ds        -> Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section Range
i 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
ds
      Apply ModuleInfo
i ModuleName
m ModuleApplication
a ScopeCopyInfo
ci ImportDirective
d          -> (\ ModuleApplication
a -> ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply ModuleInfo
i ModuleName
m ModuleApplication
a ScopeCopyInfo
ci ImportDirective
d) (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure Declaration
d
      FunDef DefInfo
i QName
f Delayed
d [Clause]
cs           -> DefInfo -> QName -> Delayed -> [Clause] -> Declaration
FunDef DefInfo
i QName
f Delayed
d ([Clause] -> Declaration) -> m [Clause] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Clause] -> m [Clause]
RecurseExprRecFn m
rec [Clause]
cs
      DataSig DefInfo
i QName
d GeneralizeTelescope
tel Expr
e         -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i 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 (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 UniverseCheck
uc DataDefParams
bs [Declaration]
cs      -> DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
d UniverseCheck
uc (DataDefParams -> [Declaration] -> Declaration)
-> m DataDefParams -> m ([Declaration] -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDefParams -> m DataDefParams
RecurseExprRecFn m
rec DataDefParams
bs m ([Declaration] -> Declaration)
-> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
cs
      RecSig DefInfo
i QName
r GeneralizeTelescope
tel Expr
e          -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig DefInfo
i 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 (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 UniverseCheck
uc RecordDirectives
dir DataDefParams
bs Expr
e [Declaration]
ds -> DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
RecDef DefInfo
i QName
r UniverseCheck
uc RecordDirectives
dir (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
ds
      PatternSynDef QName
f [Arg BindName]
xs Pattern' Void
p      -> QName -> [Arg BindName] -> Pattern' Void -> Declaration
PatternSynDef QName
f [Arg BindName]
xs (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
      ScopedDecl ScopeInfo
s [Declaration]
ds           -> ScopeInfo -> [Declaration] -> Declaration
ScopedDecl ScopeInfo
s ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> m [Declaration]
RecurseExprRecFn m
rec [Declaration]
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
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 (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap 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 a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames 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 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 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 HasEta0
_ Maybe Range
_ Maybe QName
c) = m
kc where
    kc :: m
kc = m -> (QName -> m) -> Maybe QName -> m
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m
forall a. Monoid a => a
mempty (KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> (QName -> KName) -> QName -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
k) Maybe QName
c
    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 [Occurrence]
_ 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
_ [Declaration]
decls               -> [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      DataSig DefInfo
_ 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 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 (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> m
con [Declaration]
decls
      RecSig DefInfo
_ 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 UniverseCheck
_ 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 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 a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      PatternSynDef QName
q [Arg 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
      FunDef DefInfo
_ QName
q Delayed
_ [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
<> [Clause] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Clause]
cls
      ScopedDecl ScopeInfo
_ [Declaration]
decls           -> [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
decls          -> [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      Pragma Range
_ Pragma
pragma              -> 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
    where
    con :: Declaration -> m
con = \case
      Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ 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
    EtaPragma{}             -> m
forall a. Monoid a => a
mempty
    InjectivePragma{}       -> m
forall a. Monoid a => a
mempty
    InlinePragma{}          -> m
forall a. Monoid a => a
mempty
    DisplayPragma{}         -> m
forall a. Monoid a => a
mempty
    OptionsPragma{}         -> 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 Bool
_) = 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 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
_ Maybe Declaration
ds) = 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 [WithExpr]
_es [Clause]
cls        -> [Clause] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Clause]
cls
    RewriteRHS [RewriteEqn]
_qes [ProblemEq]
_ RHS
rhs WhereDeclarations
cls -> 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 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
--     ETel{}                -> __IMPOSSIBLE__
--     Rec _ fields          -> declaredNames fields
--     RecUpdate _ e fs      -> declaredNames e <> declaredNames fs
--     ScopedExpr _ e        -> declaredNames e
--     Quote{}               -> mempty
--     QuoteTerm{}           -> mempty
--     Unquote{}             -> mempty
--     DontCare{}            -> mempty
--     PatternSyn{}          -> mempty
--     Macro{}               -> mempty

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

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

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

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