module Agda.Syntax.Concrete
(
Expr(..)
, OpApp(..), fromOrdinary
, module Agda.Syntax.Concrete.Name
, appView, AppView(..)
, LamBinding
, LamBinding'(..)
, TypedBindings
, TypedBindings'(..)
, TypedBinding
, TypedBinding'(..)
, ColoredTypedBinding(..)
, BoundName(..), mkBoundName_, mkBoundName
, Telescope
, countTelVars
, Declaration(..)
, ModuleApplication(..)
, TypeSignature
, TypeSignatureOrInstanceBlock
, Constructor
, ImportDirective(..), UsingOrHiding(..), ImportedName(..)
, Renaming(..), AsName(..)
, defaultImportDir
, OpenShortHand(..), RewriteEqn, WithExpr
, LHS(..), Pattern(..), LHSCore(..)
, RHS, RHS'(..), WhereClause, WhereClause'(..)
, Pragma(..)
, Module
, ThingWithFixity(..)
, topLevelModuleName
, patternHead, patternNames
, mapLhsOriginalPattern
, Color
, Arg
, NamedArg
, ArgInfo
)
where
import Control.DeepSeq
import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.List
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Name
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
type Color = Expr
type Arg a = Common.Arg Color a
type NamedArg a = Common.NamedArg Color a
type ArgInfo = Common.ArgInfo Color
data OpApp e
= SyntaxBindingLambda !Range [LamBinding] e
| Ordinary e
deriving (Typeable, Functor, Foldable, Traversable)
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 [NamedArg (OpApp Expr)]
| WithApp !Range Expr [Expr]
| HiddenArg !Range (Named_ Expr)
| InstanceArg !Range (Named_ 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
| QuoteContext !Range Name Expr
| Quote !Range
| QuoteTerm !Range
| Tactic !Range Expr [Expr]
| Unquote !Range
| DontCare Expr
| Equal !Range Expr Expr
deriving (Typeable)
instance NFData Expr
data Pattern
= IdentP QName
| QuoteP !Range
| AppP Pattern (NamedArg Pattern)
| RawAppP !Range [Pattern]
| OpAppP !Range QName [NamedArg Pattern]
| HiddenP !Range (Named_ Pattern)
| InstanceP !Range (Named_ Pattern)
| ParenP !Range Pattern
| WildP !Range
| AbsurdP !Range
| AsP !Range Name Pattern
| DotP !Range Expr
| LitP Literal
deriving (Typeable)
instance NFData Pattern
type LamBinding = LamBinding' TypedBindings
data LamBinding' a
= DomainFree ArgInfo BoundName
| DomainFull a
deriving (Typeable, Functor, Foldable, Traversable)
type TypedBindings = TypedBindings' TypedBinding
data TypedBindings' a = TypedBindings !Range (Arg a)
deriving (Typeable, Functor, Foldable, Traversable)
data BoundName = BName
{ boundName :: Name
, boundLabel :: Name
, bnameFixity :: Fixity'
}
deriving (Typeable)
mkBoundName_ :: Name -> BoundName
mkBoundName_ x = mkBoundName x defaultFixity'
mkBoundName :: Name -> Fixity' -> BoundName
mkBoundName x f = BName x x f
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
= TBind !Range [BoundName] e
| TLet !Range [Declaration]
deriving (Typeable, Functor, Foldable, Traversable)
data ColoredTypedBinding = WithColors [Color] TypedBinding
type Telescope = [TypedBindings]
countTelVars :: Telescope -> Nat
countTelVars tel =
sum [ case unArg b of
TBind _ xs _ -> genericLength xs
TLet{} -> 0
| TypedBindings _ b <- tel ]
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)
instance NFData LHSCore
type RHS = RHS' Expr
data RHS' e
= AbsurdRHS
| RHS e
deriving (Typeable, Functor, Foldable, Traversable)
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
= NoWhere
| AnyWhere decls
| SomeWhere Name decls
deriving (Typeable, Functor, Foldable, Traversable)
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 TypeSignatureOrInstanceBlock = Declaration
type Constructor = TypeSignature
data Declaration
= TypeSig ArgInfo 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 (Ranged Induction)) (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]
| Infix Fixity [Name]
| Syntax Name Notation
| PatternSyn !Range Name [Arg Name] Pattern
| Mutual !Range [Declaration]
| Abstract !Range [Declaration]
| Private !Range [Declaration]
| InstanceB !Range [Declaration]
| Postulate !Range [TypeSignatureOrInstanceBlock]
| 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]
| UnquoteDecl !Range Name Expr
| Pragma Pragma
deriving (Typeable)
data ModuleApplication
= SectionApp Range [TypedBindings] Expr
| RecordModuleIFS Range QName
deriving (Typeable)
data OpenShortHand = DoOpen | DontOpen
deriving (Typeable, Eq, Show)
data Pragma
= OptionsPragma !Range [String]
| BuiltinPragma !Range String Expr
| RewritePragma !Range QName
| CompiledDataPragma !Range QName String [String]
| CompiledTypePragma !Range QName String
| CompiledPragma !Range QName String
| CompiledExportPragma !Range QName String
| CompiledEpicPragma !Range QName String
| CompiledJSPragma !Range QName String
| StaticPragma !Range QName
| ImportPragma !Range String
| ImpossiblePragma !Range
| EtaPragma !Range QName
| TerminationCheckPragma !Range (TerminationCheck Name)
deriving (Typeable)
type Module = ([Pragma], [Declaration])
topLevelModuleName :: Module -> TopLevelModuleName
topLevelModuleName (_, []) = __IMPOSSIBLE__
topLevelModuleName (_, ds) = case last ds of
Module _ n _ _ -> toTopLevelModuleName n
_ -> __IMPOSSIBLE__
mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
mapLhsOriginalPattern f lhs@Ellipsis{} = lhs
mapLhsOriginalPattern f lhs@LHS{ lhsOriginalPattern = p } =
lhs { lhsOriginalPattern = f p }
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) = noColorArg Hidden Relevant e
arg (InstanceArg _ e) = noColorArg Instance Relevant e
arg e = noColorArg 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
QuoteP _ -> 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 . namedArg) ps
HiddenP _ (namedPat) -> patternNames (namedThing namedPat)
ParenP _ p -> patternNames p
WildP _ -> []
AbsurdP _ -> []
AsP _ x p -> patternNames p
DotP{} -> []
LitP _ -> []
QuoteP _ -> []
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
QuoteContext r _ _ -> r
Quote r -> r
QuoteTerm r -> r
Unquote r -> r
Tactic r _ _ -> r
DontCare{} -> noRange
Equal r _ _ -> r
instance HasRange TypedBindings where
getRange (TypedBindings r _) = r
instance HasRange TypedBinding where
getRange (TBind r _ _) = r
getRange (TLet r _) = r
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 (InstanceB 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 (UnquoteDecl 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 (RewritePragma r _) = r
getRange (CompiledDataPragma r _ _ _) = r
getRange (CompiledTypePragma r _ _) = r
getRange (CompiledPragma r _ _) = r
getRange (CompiledExportPragma 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 (TerminationCheckPragma 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 (QuoteP r) = r
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 l f) = killRange3 BName n l f
instance KillRange Declaration where
killRange (TypeSig i n e) = killRange2 (TypeSig i) 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 (InstanceB _ d) = killRange1 (InstanceB 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 (UnquoteDecl _ x t) = killRange2 (UnquoteDecl noRange) x t
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 (QuoteContext _ n e) = killRange2 (QuoteContext noRange) n e
killRange (Quote _) = Quote noRange
killRange (QuoteTerm _) = QuoteTerm noRange
killRange (Unquote _) = Unquote noRange
killRange (Tactic _ t es) = killRange2 (Tactic noRange) t es
killRange (DontCare e) = killRange1 DontCare e
killRange (Equal _ x y) = Equal noRange x y
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 i b) = killRange2 DomainFree i 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
killRange (QuoteP _) = QuoteP noRange
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s
killRange (BuiltinPragma _ s e) = killRange1 (BuiltinPragma noRange s) e
killRange (RewritePragma _ q) = killRange1 (RewritePragma noRange) q
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 (CompiledExportPragma _ q s) = killRange1 (\q -> CompiledExportPragma 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 (TerminationCheckPragma _ t) = TerminationCheckPragma noRange (killRange t)
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 (TLet r ds) = killRange2 TLet r ds
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