module Agda.Syntax.Concrete.Generic where
import Control.Applicative
import Data.Traversable
import Data.Monoid
import Data.Foldable
import Agda.Syntax.Common hiding (Arg)
import Agda.Syntax.Concrete
#include "undefined.h"
import Agda.Utils.Impossible
class ExprLike a where
mapExpr :: (Expr -> Expr) -> a -> a
traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a
foldExpr :: Monoid m => (Expr -> m) -> a -> m
traverseExpr = __IMPOSSIBLE__
foldExpr = __IMPOSSIBLE__
instance ExprLike Name where
mapExpr f = id
instance ExprLike QName where
mapExpr f = id
instance ExprLike a => ExprLike (Named name a) where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance ExprLike a => ExprLike (Arg a) where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance ExprLike a => ExprLike [a] where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance ExprLike a => ExprLike (Maybe a) where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance ExprLike a => ExprLike (TypedBinding' a) where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance ExprLike a => ExprLike (RHS' a) where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance ExprLike a => ExprLike (WhereClause' a) where
mapExpr = fmap . mapExpr
traverseExpr = traverse . traverseExpr
foldExpr = foldMap . foldExpr
instance (ExprLike a, ExprLike b) => ExprLike (a, b) where
mapExpr f (x, y) = (mapExpr f x, mapExpr f y)
traverseExpr f (x, y) = (,) <$> traverseExpr f x <*> traverseExpr f y
foldExpr f (x, y) = foldExpr f x `mappend` foldExpr f y
instance (ExprLike a, ExprLike b, ExprLike c) => ExprLike (a, b, c) where
mapExpr f (x, y, z) = (mapExpr f x, mapExpr f y, mapExpr f z)
traverseExpr f (x, y, z) = (,,) <$> traverseExpr f x <*> traverseExpr f y <*> traverseExpr f z
foldExpr f (x, y, z) = foldExpr f x `mappend` foldExpr f y `mappend` foldExpr f z
instance ExprLike Expr where
mapExpr f e0 = case e0 of
Ident{} -> f $ e0
Lit{} -> f $ e0
QuestionMark{} -> f $ e0
Underscore{} -> f $ e0
RawApp r es -> f $ RawApp r $ mapE es
App r e es -> f $ App r (mapE e) $ mapE es
OpApp r q ns es -> f $ OpApp r q ns $ mapE es
WithApp r e es -> f $ WithApp r (mapE e) $ mapE es
HiddenArg r e -> f $ HiddenArg r $ mapE e
InstanceArg r e -> f $ InstanceArg r $ mapE e
Lam r bs e -> f $ Lam r (mapE bs) $ mapE e
AbsurdLam{} -> f $ e0
ExtendedLam r cs -> f $ ExtendedLam r $ mapE cs
Fun r a b -> f $ Fun r (mapE a) $ mapE b
Pi tel e -> f $ Pi (mapE tel) $ mapE e
Set{} -> f $ e0
Prop{} -> f $ e0
SetN{} -> f $ e0
Rec r es -> f $ Rec r $ mapE es
RecUpdate r e es -> f $ RecUpdate r (mapE e) $ mapE es
Let r ds e -> f $ Let r (mapE ds) $ mapE e
Paren r e -> f $ Paren r $ mapE e
Absurd{} -> f $ e0
As r x e -> f $ As r x $ mapE e
Dot r e -> f $ Dot r $ mapE e
ETel tel -> f $ ETel $ mapE tel
QuoteGoal r x e -> f $ QuoteGoal r x $ mapE e
QuoteContext r x e -> f $ QuoteContext r x $ mapE e
Tactic r e es -> f $ Tactic r (mapE e) $ mapE es
Quote{} -> f $ e0
QuoteTerm{} -> f $ e0
Unquote{} -> f $ e0
DontCare e -> f $ DontCare $ mapE e
Equal{} -> f $ e0
where mapE e = mapExpr f e
instance ExprLike a => ExprLike (OpApp a) where
mapExpr f e0 = case e0 of
SyntaxBindingLambda r bs e -> SyntaxBindingLambda r (mapE bs) $ mapE e
Ordinary e -> Ordinary $ mapE e
where mapE e = mapExpr f e
instance ExprLike LamBinding where
mapExpr f e0 = case e0 of
DomainFree{} -> e0
DomainFull bs -> DomainFull $ mapE bs
where mapE e = mapExpr f e
instance ExprLike TypedBindings where
mapExpr f e0 = case e0 of
TypedBindings r b -> TypedBindings r $ mapE b
where mapE e = mapExpr f e
instance ExprLike LHS where
mapExpr f e0 = case e0 of
LHS ps wps res wes -> LHS ps wps (mapE res) $ mapE wes
Ellipsis r ps res wes -> Ellipsis r ps (mapE res) $ mapE wes
where mapE e = mapExpr f e
instance ExprLike ModuleApplication where
mapExpr f e0 = case e0 of
SectionApp r bs e -> SectionApp r (mapE bs) $ mapE e
RecordModuleIFS{} -> e0
where mapE e = mapExpr f e
instance ExprLike Declaration where
mapExpr f e0 = case e0 of
TypeSig ai x e -> TypeSig ai x $ mapE e
Field x e -> Field x $ mapE e
FunClause lhs rhs wh -> FunClause (mapE lhs) (mapE rhs) $ mapE wh
DataSig r ind x bs e -> DataSig r ind x (mapE bs) $ mapE e
Data r ind n bs e cs -> Data r ind n (mapE bs) (mapE e) $ mapE cs
RecordSig r ind bs e -> RecordSig r ind (mapE bs) $ mapE e
Record r n ind c tel e ds -> Record r n ind c (mapE tel) (mapE e) $ mapE ds
Infix{} -> e0
Syntax{} -> e0
PatternSyn{} -> e0
Mutual r ds -> Mutual r $ mapE ds
Abstract r ds -> Abstract r $ mapE ds
Private r ds -> Private r $ mapE ds
InstanceB r ds -> InstanceB r $ mapE ds
Postulate r ds -> Postulate r $ mapE ds
Primitive r ds -> Primitive r $ mapE ds
Open{} -> e0
Import{} -> e0
ModuleMacro r n es op dir -> ModuleMacro r n (mapE es) op dir
Module r n tel ds -> Module r n (mapE tel) $ mapE ds
UnquoteDecl r x e -> UnquoteDecl r x (mapE e)
Pragma{} -> e0
where mapE e = mapExpr f e