module Agda.Syntax.Concrete
(
Expr(..)
, OpApp(..), fromOrdinary
, module Agda.Syntax.Concrete.Name
, appView, AppView(..)
, LamBinding(..)
, TypedBindings(..)
, TypedBinding(..)
, BoundName(..), mkBoundName_
, Telescope
, Declaration(..)
, ModuleApplication(..)
, TypeSignature
, Constructor
, ImportDirective(..), UsingOrHiding(..), ImportedName(..)
, Renaming(..), AsName(..)
, defaultImportDir
, OpenShortHand(..), RewriteEqn, WithExpr
, LHS(..), Pattern(..), LHSCore(..)
, RHS(..), WhereClause(..)
, Pragma(..)
, Module
, ThingWithFixity(..)
, topLevelModuleName
, patternHead, patternNames
)
where
import Data.Typeable (Typeable)
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, 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 String)
| RawApp !Range [Expr]
| App !Range Expr (NamedArg Expr)
| OpApp !Range QName [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 Integer
| 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 Pattern
= IdentP QName
| AppP Pattern (NamedArg Pattern)
| RawAppP !Range [Pattern]
| OpAppP !Range QName [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 LamBinding
= DomainFree Hiding Relevance BoundName
| DomainFull TypedBindings
deriving (Typeable)
data TypedBindings = TypedBindings !Range (Arg TypedBinding)
deriving (Typeable)
data BoundName = BName { boundName :: Name
, bnameFixity :: Fixity'
}
deriving (Typeable)
mkBoundName_ :: Name -> BoundName
mkBoundName_ x = BName x defaultFixity'
data TypedBinding
= TBind !Range [BoundName] Expr
| TNoBind Expr
deriving (Typeable)
type Telescope = [TypedBindings]
data LHS = LHS { lhsOriginalPattern :: Pattern
, lhsWithPattern :: [Pattern]
, lhsRewriteEqn :: [RewriteEqn]
, lhsWithExpr :: [WithExpr]
}
| Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
deriving (Typeable)
type RewriteEqn = Expr
type WithExpr = Expr
data LHSCore
= LHSHead { lhsDefName :: Name
, lhsPats :: [NamedArg Pattern]
}
| LHSProj { lhsDestructor :: QName
, lhsPatsLeft :: [NamedArg Pattern]
, lhsFocus :: NamedArg LHSCore
, lhsPatsRight :: [NamedArg Pattern]
}
deriving (Typeable)
data RHS = AbsurdRHS
| RHS Expr
deriving (Typeable)
data WhereClause = NoWhere | AnyWhere [Declaration] | SomeWhere Name [Declaration]
deriving (Typeable)
data ImportDirective
= ImportDirective
{ importDirRange :: !Range
, usingOrHiding :: UsingOrHiding
, renaming :: [Renaming]
, publicOpen :: Bool
}
deriving (Typeable)
defaultImportDir :: ImportDirective
defaultImportDir = ImportDirective noRange (Hiding []) [] False
data UsingOrHiding
= Hiding [ImportedName]
| Using [ImportedName]
deriving (Typeable)
data ImportedName = ImportedModule { importedName :: Name }
| ImportedName { importedName :: Name }
deriving (Typeable, 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 AsName = AsName { asName :: Name
, asRange :: Range
}
deriving (Typeable, Show)
type TypeSignature = Declaration
type Constructor = 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 Induction) (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]
| Infix Fixity [Name]
| Syntax Name Notation
| PatternSyn !Range Name [Name] Pattern
| 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 ModuleApplication = SectionApp Range [TypedBindings] Expr
| RecordModuleIFS Range QName
deriving (Typeable)
data OpenShortHand = DoOpen | DontOpen
deriving (Typeable, 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
| NoTerminationCheckPragma !Range
deriving (Typeable)
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 (InstanceArg _ e) = Arg Instance 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 $ unqualify 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, namedArg p']
RawAppP _ ps -> concatMap patternNames ps
OpAppP _ name ps -> unqualify 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 (PatternSyn r _ _ _) = r
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 LHSCore where
getRange (LHSHead f ps) = fuseRange f ps
getRange (LHSProj d ps1 lhscore ps2) = d `fuseRange` ps1 `fuseRange` lhscore `fuseRange` ps2
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
getRange (NoTerminationCheckPragma 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
instance KillRange AsName where
killRange (AsName n _) = killRange1 (flip AsName noRange) n
instance KillRange BoundName where
killRange (BName n f) = killRange2 BName n f
instance KillRange Declaration where
killRange (TypeSig r n e) = killRange2 (TypeSig r) n e
killRange (Field n a) = killRange2 Field n a
killRange (FunClause l r w) = killRange3 FunClause l r w
killRange (DataSig _ i n l e) = killRange4 (DataSig noRange) i n l e
killRange (Data _ i n l e c) = killRange4 (Data noRange i) n l e c
killRange (RecordSig _ n l e) = killRange3 (RecordSig noRange) n l e
killRange (Record _ n mi mn k e d)= killRange6 (Record noRange) n mi mn k e d
killRange (Infix f n) = killRange2 Infix f n
killRange (Syntax n no) = killRange1 (\n -> Syntax n no) n
killRange (PatternSyn _ n ns p) = killRange3 (PatternSyn noRange) n ns p
killRange (Mutual _ d) = killRange1 (Mutual noRange) d
killRange (Abstract _ d) = killRange1 (Abstract noRange) d
killRange (Private _ d) = killRange1 (Private noRange) d
killRange (Postulate _ t) = killRange1 (Postulate noRange) t
killRange (Primitive _ t) = killRange1 (Primitive noRange) t
killRange (Open _ q i) = killRange2 (Open noRange) q i
killRange (Import _ q a o i) = killRange3 (\q a -> Import noRange q a o) q a i
killRange (ModuleMacro _ n m o i) = killRange3 (\n m -> ModuleMacro noRange n m o) n m i
killRange (Module _ q t d) = killRange3 (Module noRange) q t d
killRange (Pragma p) = killRange1 Pragma p
instance KillRange Expr where
killRange (Ident q) = killRange1 Ident q
killRange (Lit l) = killRange1 Lit l
killRange (QuestionMark _ n) = QuestionMark noRange n
killRange (Underscore _ n) = Underscore noRange n
killRange (RawApp _ e) = killRange1 (RawApp noRange) e
killRange (App _ e a) = killRange2 (App noRange) e a
killRange (OpApp _ n o) = killRange2 (OpApp noRange) n o
killRange (WithApp _ e es) = killRange2 (WithApp noRange) e es
killRange (HiddenArg _ n) = killRange1 (HiddenArg noRange) n
killRange (InstanceArg _ n) = killRange1 (InstanceArg noRange) n
killRange (Lam _ l e) = killRange2 (Lam noRange) l e
killRange (AbsurdLam _ h) = killRange1 (AbsurdLam noRange) h
killRange (ExtendedLam _ lrw) = killRange1 (ExtendedLam noRange) lrw
killRange (Fun _ e1 e2) = killRange2 (Fun noRange) e1 e2
killRange (Pi t e) = killRange2 Pi t e
killRange (Set _) = Set noRange
killRange (Prop _) = Prop noRange
killRange (SetN _ n) = SetN noRange n
killRange (Rec _ ne) = killRange1 (Rec noRange) ne
killRange (RecUpdate _ e ne) = killRange2 (RecUpdate noRange) e ne
killRange (Let _ d e) = killRange2 (Let noRange) d e
killRange (Paren _ e) = killRange1 (Paren noRange) e
killRange (Absurd _) = Absurd noRange
killRange (As _ n e) = killRange2 (As noRange) n e
killRange (Dot _ e) = killRange1 (Dot noRange) e
killRange (ETel t) = killRange1 ETel t
killRange (QuoteGoal _ n e) = killRange2 (QuoteGoal noRange) n e
killRange (Quote _) = Quote noRange
killRange (QuoteTerm _) = QuoteTerm noRange
killRange (Unquote _) = Unquote noRange
killRange (DontCare e) = killRange1 DontCare e
instance KillRange ImportDirective where
killRange (ImportDirective _ u r p) =
killRange2 (\u r -> ImportDirective noRange u r p) u r
instance KillRange ImportedName where
killRange (ImportedModule n) = killRange1 ImportedModule n
killRange (ImportedName n) = killRange1 ImportedName n
instance KillRange LamBinding where
killRange (DomainFree h r b) = killRange2 (\h -> DomainFree h r) h b
killRange (DomainFull t) = killRange1 DomainFull t
instance KillRange LHS where
killRange (LHS p ps r w) = killRange4 LHS p ps r w
killRange (Ellipsis _ p r w) = killRange3 (Ellipsis noRange) p r w
instance KillRange ModuleApplication where
killRange (SectionApp _ t e) = killRange2 (SectionApp noRange) t e
killRange (RecordModuleIFS _ q) = killRange1 (RecordModuleIFS noRange) q
instance KillRange e => KillRange (OpApp e) where
killRange (SyntaxBindingLambda _ l e) = killRange2 (SyntaxBindingLambda noRange) l e
killRange (Ordinary e) = killRange1 Ordinary e
instance KillRange Pattern where
killRange (IdentP q) = killRange1 IdentP q
killRange (AppP p n) = killRange2 AppP p n
killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p
killRange (OpAppP _ n p) = killRange2 (OpAppP noRange) n p
killRange (HiddenP _ n) = killRange1 (HiddenP noRange) n
killRange (InstanceP _ n) = killRange1 (InstanceP noRange) n
killRange (ParenP _ p) = killRange1 (ParenP noRange) p
killRange (WildP _) = WildP noRange
killRange (AbsurdP _) = AbsurdP noRange
killRange (AsP _ n p) = killRange2 (AsP noRange) n p
killRange (DotP _ e) = killRange1 (DotP noRange) e
killRange (LitP l) = killRange1 LitP l
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s
killRange (BuiltinPragma _ s e) = killRange1 (BuiltinPragma noRange s) e
killRange (CompiledDataPragma _ q s ss) = killRange1 (\q -> CompiledDataPragma noRange q s ss) q
killRange (CompiledTypePragma _ q s) = killRange1 (\q -> CompiledTypePragma noRange q s) q
killRange (CompiledPragma _ q s) = killRange1 (\q -> CompiledPragma noRange q s) q
killRange (CompiledEpicPragma _ q s) = killRange1 (\q -> CompiledEpicPragma noRange q s) q
killRange (CompiledJSPragma _ q s) = killRange1 (\q -> CompiledJSPragma noRange q s) q
killRange (StaticPragma _ q) = killRange1 (StaticPragma noRange) q
killRange (ImportPragma _ s) = ImportPragma noRange s
killRange (ImpossiblePragma _) = ImpossiblePragma noRange
killRange (EtaPragma _ q) = killRange1 (EtaPragma noRange) q
killRange (NoTerminationCheckPragma _) = NoTerminationCheckPragma noRange
instance KillRange Renaming where
killRange (Renaming i n _) = killRange2 (\i n -> Renaming i n noRange) i n
instance KillRange RHS where
killRange AbsurdRHS = AbsurdRHS
killRange (RHS e) = killRange1 RHS e
instance KillRange TypedBinding where
killRange (TBind _ b e) = killRange2 (TBind noRange) b e
killRange (TNoBind e) = killRange1 TNoBind e
instance KillRange TypedBindings where
killRange (TypedBindings _ t) = killRange1 (TypedBindings noRange) t
instance KillRange UsingOrHiding where
killRange (Hiding i) = killRange1 Hiding i
killRange (Using i) = killRange1 Using i
instance KillRange WhereClause where
killRange NoWhere = NoWhere
killRange (AnyWhere d) = killRange1 AnyWhere d
killRange (SomeWhere n d) = killRange2 SomeWhere n d