{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NoMonoLocalBinds          #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

module Agda.Syntax.Abstract.Views where

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

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 (emptyScopeInfo)

import Agda.Utils.Either

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

type AppView = AppView' Expr

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

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

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

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

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

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

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

-- | Check whether we are dealing with a universe.
isSet :: Expr -> Bool
isSet :: Expr -> Bool
isSet (ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Bool
isSet Expr
e
isSet (App AppInfo
_ Expr
e NamedArg Expr
_)      = Expr -> Bool
isSet Expr
e
isSet (Set{})          = Bool
True
isSet Expr
_                = Bool
False

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

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

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

deepUnscopeDecl :: A.Declaration -> [A.Declaration]
deepUnscopeDecl :: Declaration -> [Declaration]
deepUnscopeDecl (A.ScopedDecl ScopeInfo
_ [Declaration]
ds)              = [Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds
deepUnscopeDecl (A.Mutual MutualInfo
i [Declaration]
ds)                  = [MutualInfo -> [Declaration] -> Declaration
A.Mutual MutualInfo
i ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds)]
deepUnscopeDecl (A.Section ModuleInfo
i ModuleName
m GeneralizeTelescope
tel [Declaration]
ds)           = [ModuleInfo
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section ModuleInfo
i ModuleName
m (GeneralizeTelescope -> GeneralizeTelescope
forall a. ExprLike a => a -> a
deepUnscope GeneralizeTelescope
tel) ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds)]
deepUnscopeDecl (A.RecDef DefInfo
i QName
x UniverseCheck
uc Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe QName
c DataDefParams
bs Expr
e [Declaration]
ds) = [DefInfo
-> QName
-> UniverseCheck
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe QName
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
A.RecDef DefInfo
i QName
x UniverseCheck
uc Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe QName
c (DataDefParams -> DataDefParams
forall a. ExprLike a => a -> a
deepUnscope DataDefParams
bs) (Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e)
                                                                           ([Declaration] -> [Declaration]
deepUnscopeDecls [Declaration]
ds)]
deepUnscopeDecl Declaration
d                                = [Declaration -> Declaration
forall a. ExprLike a => a -> a
deepUnscope Declaration
d]

-- * Traversal

-- | 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 :: (Applicative m) => (Expr -> m Expr -> m Expr) -> a -> 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') -> f a' -> m (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a' -> m a') -> f a' -> m (f a'))
-> ((Expr -> m Expr -> m Expr) -> a' -> m a')
-> (Expr -> m Expr -> m Expr)
-> f a'
-> m (f a')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr -> m Expr) -> a' -> m a'
forall a (m :: * -> *).
(ExprLike a, Applicative m) =>
(Expr -> m Expr -> m Expr) -> a -> m a
recurseExpr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance ExprLike WhereDeclarations where
  recurseExpr :: (Expr -> m Expr -> m Expr)
-> WhereDeclarations -> m WhereDeclarations
recurseExpr Expr -> m Expr -> m Expr
f (WhereDecls Maybe ModuleName
a [Declaration]
b) = Maybe ModuleName -> [Declaration] -> WhereDeclarations
WhereDecls Maybe ModuleName
a ([Declaration] -> WhereDeclarations)
-> m [Declaration] -> m WhereDeclarations
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr -> m Expr) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(ExprLike a, Applicative m) =>
(Expr -> m Expr -> m Expr) -> a -> m a
recurseExpr Expr -> m Expr -> m Expr
f [Declaration]
b

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

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

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

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

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

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