module Agda.Syntax.Abstract.Views where

import Prelude hiding (null)

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

import Data.Foldable (foldMap)
import qualified Data.DList as DL
import Data.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
$cfmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
fmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
$c<$ :: forall a b. a -> AppView' b -> AppView' a
<$ :: forall a b. a -> AppView' b -> AppView' a
Functor)

type AppView = AppView' Expr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance ExprLike a => ExprLike (Clause' a) where
  recurseExpr :: forall m. RecurseExprFn m (Clause' a)
  recurseExpr :: forall (m :: * -> *). RecurseExprFn m (Clause' a)
recurseExpr Type -> m Type -> m Type
f (Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds 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 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 -> Bool -> Clause' a)
-> m RHS -> m (WhereDeclarations -> Bool -> 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 -> Bool -> Clause' a)
-> m WhereDeclarations -> m (Bool -> 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 (Bool -> Clause' a) -> m Bool -> 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
<*> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
ca
    where
      rec :: RecurseExprRecFn m
      rec :: RecurseExprRecFn m
rec = (Type -> m Type -> m Type) -> a -> m a
forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
forall (m :: * -> *). RecurseExprFn m a
recurseExpr Type -> m Type -> m Type
f

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

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

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

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

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

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

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

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

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


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

type KName = WithKind QName

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

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

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

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

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

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

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

instance DeclaredNames RecordDirectives where
  declaredNames :: forall m. Collection KName m => RecordDirectives -> m
declaredNames (RecordDirectives Maybe (Ranged Induction)
i Maybe 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 Type
_           -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> (KindOfName -> KName) -> KindOfName -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
`WithKind` QName
q) (KindOfName -> m) -> KindOfName -> m
forall a b. (a -> b) -> a -> b
$
                                      case DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
defMacro DefInfo
di of
                                        IsMacro
MacroDef    -> KindOfName
MacroName
                                        IsMacro
NotMacroDef -> KindOfName
AxiomName
      Generalize Set QName
_ DefInfo
_ ArgInfo
_ QName
q Type
_         -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
GeneralizeName QName
q)
      Field DefInfo
_ QName
q Arg Type
_                  -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FldName QName
q)
      Primitive DefInfo
_ QName
q Arg Type
_              -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
PrimName QName
q)
      Mutual MutualInfo
_ [Declaration]
decls               -> [Declaration] -> m
forall m. Collection KName m => [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      DataSig DefInfo
_ Erased
_ QName
q GeneralizeTelescope
_ Type
_            -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
q)
      DataDef DefInfo
_ QName
q UniverseCheck
_ DataDefParams
_ [Declaration]
decls        -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
q) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (Declaration -> m) -> [Declaration] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> m
con [Declaration]
decls
      RecSig DefInfo
_ Erased
_ QName
q GeneralizeTelescope
_ Type
_             -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
RecName QName
q)
      RecDef DefInfo
_ QName
q UniverseCheck
_ RecordDirectives
dir DataDefParams
_ Type
_ [Declaration]
decls   -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
RecName QName
q) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> RecordDirectives -> m
forall m. Collection KName m => RecordDirectives -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames RecordDirectives
dir m -> m -> m
forall a. Semigroup a => a -> a -> a
<> [Declaration] -> m
forall m. Collection KName m => [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Declaration]
decls
      PatternSynDef QName
q [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 Type
_         -> [KName] -> m
forall el coll. Collection el coll => [el] -> coll
fromList ([KName] -> m) -> [KName] -> m
forall a b. (a -> b) -> a -> b
$ (QName -> KName) -> [QName] -> [KName]
forall a b. (a -> b) -> [a] -> [b]
map (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
OtherDefName) [QName]
qs  -- could be Fun or Axiom
      UnquoteDef [DefInfo]
_ [QName]
qs Type
_            -> [KName] -> m
forall el coll. Collection el coll => [el] -> coll
fromList ([KName] -> m) -> [KName] -> m
forall a b. (a -> b) -> a -> b
$ (QName -> KName) -> [QName] -> [KName]
forall a b. (a -> b) -> [a] -> [b]
map (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
FunName) [QName]
qs       -- cannot be Axiom
      UnquoteData [DefInfo]
_ QName
d UniverseCheck
_ [DefInfo]
_ [QName]
cs Type
_     -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
DataName QName
d) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> ([KName] -> m
forall el coll. Collection el coll => [el] -> coll
fromList ([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
ConName) [QName]
cs) -- singleton _ <> map (WithKind ConName) cs
      FunDef DefInfo
_ QName
q [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 m. Collection KName m => [Clause] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [Clause]
cls
      ScopedDecl ScopeInfo
_ [Declaration]
decls           -> [Declaration] -> m
forall m. Collection KName m => [Declaration] -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
declaredNames [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 [Occurrence]
_ QName
q Type
_ -> KName -> m
forall el coll. Singleton el coll => el -> coll
singleton (KName -> m) -> KName -> m
forall a b. (a -> b) -> a -> b
$ KindOfName -> QName -> KName
forall a. KindOfName -> a -> WithKind a
WithKind KindOfName
ConName QName
q
      Declaration
_ -> m
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

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

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

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