module Agda.Syntax.Concrete
(
Expr(..)
, OpApp(..), fromOrdinary
, module Agda.Syntax.Concrete.Name
, appView, AppView(..)
, LamBinding(..)
, TypedBindings(..)
, TypedBinding(..)
, BoundName(..), mkBoundName_
, Telescope
, Declaration(..)
, ModuleApplication(..)
, TypeSignature
, Constructor
, Field
, ImportDirective(..), UsingOrHiding(..), ImportedName(..)
, Renaming(..), AsName(..)
, defaultImportDir
, OpenShortHand(..)
, LHS(..), Pattern(..)
, RHS(..), WhereClause(..)
, Pragma(..)
, Module
, ThingWithFixity(..)
, topLevelModuleName
, patternHead, patternNames
)
where
import Data.Generics (Typeable, Data)
import Data.Foldable hiding (concatMap)
import Data.Traversable
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Name
import Agda.Utils.Impossible
#include "../undefined.h"
data OpApp e
= SyntaxBindingLambda !Range [LamBinding] e
| Ordinary e
deriving (Typeable, Data, Functor)
fromOrdinary :: e -> OpApp e -> e
fromOrdinary d (Ordinary e) = e
fromOrdinary d _ = d
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 [OpApp Expr]
| WithApp !Range Expr [Expr]
| HiddenArg !Range (Named String Expr)
| InstanceArg !Range (Named String Expr)
| Lam !Range [LamBinding] Expr
| AbsurdLam !Range Hiding
| ExtendedLam !Range [(LHS,RHS,WhereClause)]
| Fun !Range Expr Expr
| Pi Telescope Expr
| Set !Range
| Prop !Range
| SetN !Range Nat
| Rec !Range [(Name, Expr)]
| RecUpdate !Range Expr [(Name, Expr)]
| Let !Range [Declaration] Expr
| Paren !Range Expr
| Absurd !Range
| As !Range Name Expr
| Dot !Range Expr
| ETel Telescope
| QuoteGoal !Range Name Expr
| Quote !Range
| QuoteTerm !Range
| Unquote !Range
| DontCare Expr
deriving (Typeable, Data)
data Pattern
= IdentP QName
| AppP Pattern (NamedArg Pattern)
| RawAppP !Range [Pattern]
| OpAppP !Range Name [Pattern]
| HiddenP !Range (Named String Pattern)
| InstanceP !Range (Named String Pattern)
| ParenP !Range Pattern
| WildP !Range
| AbsurdP !Range
| AsP !Range Name Pattern
| DotP !Range Expr
| LitP Literal
deriving (Typeable, Data)
data LamBinding
= DomainFree Hiding Relevance BoundName
| DomainFull TypedBindings
deriving (Typeable, Data)
data TypedBindings = TypedBindings !Range (Arg TypedBinding)
deriving (Typeable, Data)
data BoundName = BName { boundName :: Name
, bnameFixity :: Fixity'
}
deriving (Typeable, Data)
mkBoundName_ :: Name -> BoundName
mkBoundName_ x = BName x defaultFixity'
data TypedBinding
= TBind !Range [BoundName] Expr
| TNoBind Expr
deriving (Typeable, Data)
type Telescope = [TypedBindings]
data LHS = LHS { lhsOriginalPattern :: Pattern
, lhsWithPattern :: [Pattern]
, lhsRewriteEqn :: [RewriteEqn]
, lhsWithExpr :: [WithExpr]
}
| Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
deriving (Typeable, Data)
type RewriteEqn = Expr
type WithExpr = Expr
data RHS = AbsurdRHS
| RHS Expr
deriving (Typeable, Data)
data WhereClause = NoWhere | AnyWhere [Declaration] | SomeWhere Name [Declaration]
deriving (Typeable, Data)
data ImportDirective
= ImportDirective
{ importDirRange :: !Range
, usingOrHiding :: UsingOrHiding
, renaming :: [Renaming]
, publicOpen :: Bool
}
deriving (Typeable, Data)
defaultImportDir :: ImportDirective
defaultImportDir = ImportDirective noRange (Hiding []) [] False
data UsingOrHiding
= Hiding [ImportedName]
| Using [ImportedName]
deriving (Typeable, Data)
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 (Typeable, Data)
data AsName = AsName { asName :: Name
, asRange :: Range
}
deriving (Typeable, Data, Show)
type TypeSignature = Declaration
type Constructor = TypeSignature
type Field = TypeSignature
data Declaration
= TypeSig Relevance Name Expr
| Field Name (Arg Expr)
| FunClause LHS RHS WhereClause
| DataSig !Range Induction Name [LamBinding] Expr
| Data !Range Induction Name [LamBinding] (Maybe Expr) [Constructor]
| RecordSig !Range Name [LamBinding] Expr
| Record !Range Name (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]
| Infix Fixity [Name]
| Syntax Name Notation
| 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 ModuleApplication OpenShortHand ImportDirective
| Module !Range QName [TypedBindings] [Declaration]
| Pragma Pragma
deriving (Typeable, Data)
data ModuleApplication = SectionApp Range [TypedBindings] Expr
| RecordModuleIFS Range QName
deriving (Typeable, Data)
data OpenShortHand = DoOpen | DontOpen
deriving (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
| CompiledEpicPragma !Range QName String
| CompiledJSPragma !Range QName String
| StaticPragma !Range QName
| ImportPragma !Range String
| ImpossiblePragma !Range
| EtaPragma !Range QName
deriving (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 Relevant e
arg e = Arg NotHidden Relevant (unnamed e)
appView e = AppView e []
patternHead :: Pattern -> Maybe Name
patternHead p =
case p of
IdentP x -> return $ unqualify x
AppP p p' -> patternHead p
RawAppP _ [] -> __IMPOSSIBLE__
RawAppP _ (p:_) -> patternHead p
OpAppP _ name ps -> return $ name
HiddenP _ (namedPat) -> patternHead (namedThing namedPat)
ParenP _ p -> patternHead p
WildP _ -> Nothing
AbsurdP _ -> Nothing
AsP _ x p -> patternHead p
DotP{} -> Nothing
LitP (LitQName _ x) -> Nothing
LitP _ -> Nothing
InstanceP _ (namedPat) -> patternHead (namedThing namedPat)
patternNames :: Pattern -> [Name]
patternNames p =
case p of
IdentP x -> [unqualify x]
AppP p p' -> concatMap patternNames [p, namedThing $ unArg p']
RawAppP _ ps -> concatMap patternNames ps
OpAppP _ name ps -> name : concatMap patternNames ps
HiddenP _ (namedPat) -> patternNames (namedThing namedPat)
ParenP _ p -> patternNames p
WildP _ -> []
AbsurdP _ -> []
AsP _ x p -> patternNames p
DotP{} -> []
LitP _ -> []
InstanceP _ (namedPat) -> patternNames (namedThing namedPat)
instance HasRange e => HasRange (OpApp e) where
getRange e = case e of
Ordinary e -> getRange e
SyntaxBindingLambda r _ _ -> r
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
ExtendedLam 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
InstanceArg r _ -> r
Rec r _ -> r
RecUpdate r _ _ -> r
ETel tel -> getRange tel
QuoteGoal r _ _ -> r
Quote r -> r
QuoteTerm r -> r
Unquote r -> r
DontCare{} -> noRange
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 ModuleApplication where
getRange (SectionApp r _ _) = r
getRange (RecordModuleIFS r _) = r
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 (DataSig r _ _ _ _) = r
getRange (Data r _ _ _ _ _) = r
getRange (RecordSig 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 (Syntax n _) = getRange n
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 (CompiledEpicPragma r _ _) = r
getRange (CompiledJSPragma r _ _) = r
getRange (StaticPragma r _) = r
getRange (ImportPragma r _) = r
getRange (ImpossiblePragma r) = r
getRange (EtaPragma 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 (InstanceP r _) = r
getRange (DotP r _) = r