module Agda.Syntax.Abstract.Views where
import Control.Applicative
import Control.Arrow (first)
import Control.Monad.Identity
import Data.Traversable
import Agda.Syntax.Position
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
import Agda.Syntax.Abstract as A
import Agda.Syntax.Info
data AppView = Application Expr [NamedArg Expr]
appView :: Expr -> AppView
appView e =
case e of
App i e1 arg | Application hd es <- appView e1
-> Application hd $ es ++ [arg]
ScopedExpr _ e -> appView e
_ -> Application e []
unAppView :: AppView -> Expr
unAppView (Application h es) =
foldl (App (ExprRange noRange)) h es
asView :: A.Pattern -> ([Name], A.Pattern)
asView (A.AsP _ x p) = first (x :) $ asView p
asView p = ([], p)
isSet :: Expr -> Bool
isSet (ScopedExpr _ e) = isSet e
isSet (App _ e _) = isSet e
isSet (Set{}) = True
isSet _ = False
unScope :: Expr -> Expr
unScope (ScopedExpr scope e) = unScope e
unScope e = e
deepUnScope :: Expr -> Expr
deepUnScope = mapExpr unScope
class ExprLike a where
traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m a
mapExpr :: (Expr -> Expr) -> (a -> a)
mapExpr f e = runIdentity $ traverseExpr (Identity . f) e
instance ExprLike Expr where
traverseExpr f e = do
let trav e = traverseExpr f e
case e of
Var{} -> f e
Def{} -> f e
Con{} -> f e
Lit{} -> f e
QuestionMark{} -> f e
Underscore{} -> f e
App ei e arg -> f =<< App ei <$> trav e <*> trav arg
WithApp ei e es -> f =<< WithApp ei <$> trav e <*> trav es
Lam ei b e -> f =<< Lam ei <$> trav b <*> trav e
AbsurdLam{} -> f e
ExtendedLam ei di x cls -> f =<< ExtendedLam ei di x <$> trav cls
Pi ei tel e -> f =<< Pi ei <$> trav tel <*> trav e
Fun ei arg e -> f =<< Fun ei <$> trav arg <*> trav e
Set{} -> f e
Prop{} -> f e
Let ei bs e -> f =<< Let ei <$> trav bs <*> trav e
ETel tel -> f =<< ETel <$> trav tel
Rec ei bs -> f =<< Rec ei <$> trav bs
RecUpdate ei e bs -> f =<< RecUpdate ei <$> trav e <*> trav bs
ScopedExpr sc e -> f =<< ScopedExpr sc <$> trav e
QuoteGoal ei n e -> f =<< QuoteGoal ei n <$> trav e
QuoteContext ei n e -> f =<< QuoteContext ei n <$> trav e
Quote{} -> f e
QuoteTerm{} -> f e
Unquote{} -> f e
DontCare e -> f =<< DontCare <$> trav e
PatternSyn{} -> f e
instance ExprLike a => ExprLike (Common.Arg c a) where
traverseExpr = traverse . traverseExpr
instance ExprLike a => ExprLike (Named x a) where
traverseExpr = traverse . traverseExpr
instance ExprLike a => ExprLike [a] where
traverseExpr = traverse . traverseExpr
instance ExprLike a => ExprLike (x, a) where
traverseExpr f (x, e) = (x,) <$> traverseExpr f e
instance ExprLike LamBinding where
traverseExpr f e =
case e of
DomainFree{} -> return e
DomainFull bs -> DomainFull <$> traverseExpr f bs
instance ExprLike TypedBindings where
traverseExpr f (TypedBindings r b) = TypedBindings r <$> traverseExpr f b
instance ExprLike TypedBinding where
traverseExpr f e =
case e of
TBind r xs e -> TBind r xs <$> traverseExpr f e
TLet r ds -> TLet r <$> traverseExpr f ds
instance ExprLike LetBinding where
traverseExpr f e = do
let trav e = traverseExpr f e
case e of
LetBind li ai x e e' -> LetBind li ai x <$> trav e <*> trav e'
LetPatBind li p e -> LetPatBind li <$> trav p <*> trav e
LetApply{} -> return e
LetOpen{} -> return e
instance ExprLike (Pattern' a) where
traverseExpr f e = return e
instance ExprLike (Clause' a) where
traverseExpr f e = return e