module Agda.Syntax.Concrete
(
Expr(..)
, module Agda.Syntax.Concrete.Name
, appView, AppView(..)
, LamBinding(..)
, TypedBindings(..)
, TypedBinding(..)
, BoundName(..), mkBoundName_
, Telescope
, Declaration(..)
, TypeSignature
, Constructor
, Field
, ImportDirective(..), UsingOrHiding(..), ImportedName(..)
, Renaming(..), AsName(..)
, defaultImportDir
, OpenShortHand(..)
, LHS(..), Pattern(..)
, RHS(..), WhereClause(..)
, Pragma(..)
, Module
, topLevelModuleName
)
where
import Data.Generics hiding (Fixity, Infix)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Name
import Agda.Utils.Impossible
#include "../undefined.h"
data Expr
= Ident QName
| Lit Literal
| QuestionMark !Range (Maybe Nat)
| Underscore !Range (Maybe Nat)
| RawApp !Range [Expr]
| App !Range Expr (NamedArg Expr)
| OpApp !Range Name [Expr]
| WithApp !Range Expr [Expr]
| HiddenArg !Range (Named String Expr)
| Lam !Range [LamBinding] Expr
| AbsurdLam !Range Hiding
| Fun !Range Expr Expr
| Pi Telescope Expr
| Set !Range
| Prop !Range
| SetN !Range Nat
| Rec !Range [(Name, Expr)]
| Let !Range [Declaration] Expr
| Paren !Range Expr
| Absurd !Range
| As !Range Name Expr
| Dot !Range Expr
| ETel Telescope
deriving (Typeable, Data, Eq)
data Pattern
= IdentP QName
| AppP Pattern (NamedArg Pattern)
| RawAppP !Range [Pattern]
| OpAppP !Range Name [Pattern]
| HiddenP !Range (Named String Pattern)
| ParenP !Range Pattern
| WildP !Range
| AbsurdP !Range
| AsP !Range Name Pattern
| DotP !Range Expr
| LitP Literal
deriving (Typeable, Data, Eq)
data LamBinding
= DomainFree Hiding BoundName
| DomainFull TypedBindings
deriving (Typeable, Data, Eq)
data TypedBindings = TypedBindings !Range Hiding [TypedBinding]
deriving (Typeable, Data, Eq)
data BoundName = BName { boundName :: Name
, bnameFixity :: Fixity
}
deriving (Typeable, Data, Eq)
mkBoundName_ :: Name -> BoundName
mkBoundName_ x = BName x defaultFixity
data TypedBinding
= TBind !Range [BoundName] Expr
| TNoBind Expr
deriving (Typeable, Data, Eq)
type Telescope = [TypedBindings]
data LHS = LHS Pattern [Pattern] [RewriteEqn] [WithExpr]
| Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
deriving (Typeable, Data, Eq)
type RewriteEqn = Expr
type WithExpr = Expr
data RHS = AbsurdRHS
| RHS Expr
deriving (Typeable, Data, Eq)
data WhereClause = NoWhere | AnyWhere [Declaration] | SomeWhere Name [Declaration]
deriving (Typeable, Data, Eq)
data ImportDirective
= ImportDirective
{ importDirRange :: !Range
, usingOrHiding :: UsingOrHiding
, renaming :: [Renaming]
, publicOpen :: Bool
}
deriving (Typeable, Data, Eq)
defaultImportDir :: ImportDirective
defaultImportDir = ImportDirective noRange (Hiding []) [] False
data UsingOrHiding
= Hiding [ImportedName]
| Using [ImportedName]
deriving (Typeable, Data, Eq)
data ImportedName = ImportedModule { importedName :: Name }
| ImportedName { importedName :: Name }
deriving (Typeable, Data, Eq, Ord)
instance Show ImportedName where
show (ImportedModule x) = "module " ++ show x
show (ImportedName x) = show x
data Renaming = Renaming { renFrom :: ImportedName
, renTo :: Name
, renToRange :: Range
}
deriving (Eq, Typeable, Data)
data AsName = AsName { asName :: Name
, asRange :: Range
}
deriving (Eq, Typeable, Data)
type TypeSignature = Declaration
type Constructor = TypeSignature
type Field = TypeSignature
data Declaration
= TypeSig Name Expr
| Field Hiding Name Expr
| FunClause LHS RHS WhereClause
| Data !Range Induction Name [TypedBindings] Expr [Constructor]
| Record !Range Name (Maybe Name) [TypedBindings] Expr [Declaration]
| Infix Fixity [Name]
| Mutual !Range [Declaration]
| Abstract !Range [Declaration]
| Private !Range [Declaration]
| Postulate !Range [TypeSignature]
| Primitive !Range [TypeSignature]
| Open !Range QName ImportDirective
| Import !Range QName (Maybe AsName) OpenShortHand ImportDirective
| ModuleMacro !Range Name [TypedBindings] Expr OpenShortHand ImportDirective
| Module !Range QName [TypedBindings] [Declaration]
| Pragma Pragma
deriving (Eq, Typeable, Data)
data OpenShortHand = DoOpen | DontOpen
deriving (Eq, Typeable, Data, Show)
data Pragma = OptionsPragma !Range [String]
| BuiltinPragma !Range String Expr
| CompiledDataPragma !Range QName String [String]
| CompiledTypePragma !Range QName String
| CompiledPragma !Range QName String
| ImportPragma !Range String
| ImpossiblePragma !Range
deriving (Eq, Typeable, Data)
type Module = ([Pragma], [Declaration])
topLevelModuleName :: Module -> TopLevelModuleName
topLevelModuleName (_, []) = __IMPOSSIBLE__
topLevelModuleName (_, ds) = case last ds of
Module _ n _ _ -> toTopLevelModuleName n
_ -> __IMPOSSIBLE__
data AppView = AppView Expr [NamedArg Expr]
appView :: Expr -> AppView
appView (App r e1 e2) = vApp (appView e1) e2
where
vApp (AppView e es) arg = AppView e (es ++ [arg])
appView (RawApp _ (e:es)) = AppView e $ map arg es
where
arg (HiddenArg _ e) = Arg Hidden e
arg e = Arg NotHidden (unnamed e)
appView e = AppView e []
instance HasRange Expr where
getRange e =
case e of
Ident x -> getRange x
Lit x -> getRange x
QuestionMark r _ -> r
Underscore r _ -> r
App r _ _ -> r
RawApp r _ -> r
OpApp r _ _ -> r
WithApp r _ _ -> r
Lam r _ _ -> r
AbsurdLam r _ -> r
Fun r _ _ -> r
Pi b e -> fuseRange b e
Set r -> r
Prop r -> r
SetN r _ -> r
Let r _ _ -> r
Paren r _ -> r
As r _ _ -> r
Dot r _ -> r
Absurd r -> r
HiddenArg r _ -> r
Rec r _ -> r
ETel tel -> getRange tel
instance HasRange TypedBindings where
getRange (TypedBindings r _ _) = r
instance HasRange TypedBinding where
getRange (TBind r _ _) = r
getRange (TNoBind e) = getRange e
instance HasRange LamBinding where
getRange (DomainFree _ x) = getRange x
getRange (DomainFull b) = getRange b
instance HasRange BoundName where
getRange = getRange . boundName
instance HasRange WhereClause where
getRange NoWhere = noRange
getRange (AnyWhere ds) = getRange ds
getRange (SomeWhere _ ds) = getRange ds
instance HasRange Declaration where
getRange (TypeSig x t) = fuseRange x t
getRange (Field _ x t) = fuseRange x t
getRange (FunClause lhs rhs wh) = fuseRange lhs rhs `fuseRange` wh
getRange (Data r _ _ _ _ _) = r
getRange (Record r _ _ _ _ _) = r
getRange (Mutual r _) = r
getRange (Abstract r _) = r
getRange (Open r _ _) = r
getRange (ModuleMacro r _ _ _ _ _) = r
getRange (Import r _ _ _ _) = r
getRange (Private r _) = r
getRange (Postulate r _) = r
getRange (Primitive r _) = r
getRange (Module r _ _ _) = r
getRange (Infix f _) = getRange f
getRange (Pragma p) = getRange p
instance HasRange LHS where
getRange (LHS p ps eqns ws) = fuseRange p (fuseRange ps (eqns ++ ws))
getRange (Ellipsis r _ _ _) = r
instance HasRange RHS where
getRange AbsurdRHS = noRange
getRange (RHS e) = getRange e
instance HasRange Pragma where
getRange (OptionsPragma r _) = r
getRange (BuiltinPragma r _ _) = r
getRange (CompiledDataPragma r _ _ _) = r
getRange (CompiledTypePragma r _ _) = r
getRange (CompiledPragma r _ _) = r
getRange (ImportPragma r _) = r
getRange (ImpossiblePragma r) = r
instance HasRange UsingOrHiding where
getRange (Using xs) = getRange xs
getRange (Hiding xs) = getRange xs
instance HasRange ImportDirective where
getRange = importDirRange
instance HasRange ImportedName where
getRange (ImportedName x) = getRange x
getRange (ImportedModule x) = getRange x
instance HasRange Renaming where
getRange r = getRange (renFrom r, renTo r)
instance HasRange AsName where
getRange a = getRange (asRange a, asName a)
instance HasRange Pattern where
getRange (IdentP x) = getRange x
getRange (AppP p q) = fuseRange p q
getRange (OpAppP r _ _) = r
getRange (RawAppP r _) = r
getRange (ParenP r _) = r
getRange (WildP r) = r
getRange (AsP r _ _) = r
getRange (AbsurdP r) = r
getRange (LitP l) = getRange l
getRange (HiddenP r _) = r
getRange (DotP r _) = r