module Agda.Syntax.Abstract.Views where
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Abstract
import Agda.Syntax.Info
data AppView = Application Expr [NamedArg Expr]
appView :: Expr -> AppView
appView e =
case e of
App i e1 arg -> apply i (appView e1) arg
ScopedExpr _ e -> appView e
_ -> Application e []
where
apply i v arg =
case v of
Application hd es -> Application hd $ es ++ [arg]
unAppView :: AppView -> Expr
unAppView (Application h es) =
foldl (App (ExprRange noRange)) h es
isSet :: Expr -> Bool
isSet (ScopedExpr _ e) = isSet e
isSet (App _ e _) = isSet e
isSet (Set{}) = True
isSet _ = False