{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Syntax.Concrete
(
Expr(..)
, OpApp(..), fromOrdinary
, module Agda.Syntax.Concrete.Name
, appView, AppView(..)
, isSingleIdentifierP, removeSingletonRawAppP
, isPattern, isAbsurdP, isBinderP
, Binder'(..)
, Binder
, mkBinder_
, mkBinder
, LamBinding
, LamBinding'(..)
, TypedBinding
, TypedBinding'(..)
, RecordAssignment
, RecordAssignments
, FieldAssignment, FieldAssignment'(..), nameFieldA, exprFieldA
, ModuleAssignment(..)
, BoundName(..), mkBoundName_, mkBoundName
, TacticAttribute
, Telescope
, countTelVars
, lamBindingsToTelescope
, makePi
, Declaration(..)
, ModuleApplication(..)
, TypeSignature
, TypeSignatureOrInstanceBlock
, ImportDirective, Using, ImportedName
, Renaming
, AsName'(..), AsName
, OpenShortHand(..), RewriteEqn, WithExpr
, LHS(..), Pattern(..), LHSCore(..)
, observeHiding
, LamClause(..)
, RHS, RHS'(..), WhereClause, WhereClause'(..), ExprWhere(..)
, DoStmt(..)
, Pragma(..)
, Module
, ThingWithFixity(..)
, HoleContent, HoleContent'(..)
, topLevelModuleName
, spanAllowedBeforeModule
)
where
import Prelude hiding (null)
import Control.DeepSeq
import Data.Foldable (Foldable)
import Data.Traversable (Traversable, forM, mapM)
import Data.List hiding (null)
import Data.Set (Set)
import Data.Data (Data)
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 qualified Agda.Syntax.Abstract.Name as A
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.Either ( maybeLeft )
import Agda.Utils.Lens
import Agda.Utils.Null
import Agda.Utils.Impossible
data OpApp e
= SyntaxBindingLambda Range [LamBinding] e
| Ordinary e
deriving (Data, Functor, Foldable, Traversable, Eq)
fromOrdinary :: e -> OpApp e -> e
fromOrdinary d (Ordinary e) = e
fromOrdinary d _ = d
data FieldAssignment' a = FieldAssignment { _nameFieldA :: Name, _exprFieldA :: a }
deriving (Data, Functor, Foldable, Traversable, Show, Eq)
type FieldAssignment = FieldAssignment' Expr
data ModuleAssignment = ModuleAssignment
{ _qnameModA :: QName
, _exprModA :: [Expr]
, _importDirModA :: ImportDirective
}
deriving (Data, Eq)
type RecordAssignment = Either FieldAssignment ModuleAssignment
type RecordAssignments = [RecordAssignment]
nameFieldA :: Lens' Name (FieldAssignment' a)
nameFieldA f r = f (_nameFieldA r) <&> \x -> r { _nameFieldA = x }
exprFieldA :: Lens' a (FieldAssignment' a)
exprFieldA f r = f (_exprFieldA r) <&> \x -> r { _exprFieldA = x }
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 (Set A.Name)
[NamedArg
(MaybePlaceholder (OpApp Expr))]
| WithApp Range Expr [Expr]
| HiddenArg Range (Named_ Expr)
| InstanceArg Range (Named_ Expr)
| Lam Range [LamBinding] Expr
| AbsurdLam Range Hiding
| ExtendedLam Range [LamClause]
| Fun Range (Arg Expr) Expr
| Pi Telescope Expr
| Set Range
| Prop Range
| SetN Range Integer
| PropN Range Integer
| Rec Range RecordAssignments
| RecUpdate Range Expr [FieldAssignment]
| Let Range [Declaration] (Maybe Expr)
| Paren Range Expr
| IdiomBrackets Range [Expr]
| DoBlock Range [DoStmt]
| Absurd Range
| As Range Name Expr
| Dot Range Expr
| ETel Telescope
| Quote Range
| QuoteTerm Range
| Tactic Range Expr
| Unquote Range
| DontCare Expr
| Equal Range Expr Expr
| Ellipsis Range
| Generalized Expr
deriving (Data, Eq)
data Pattern
= IdentP QName
| QuoteP Range
| AppP Pattern (NamedArg Pattern)
| RawAppP Range [Pattern]
| OpAppP Range QName (Set A.Name)
[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
| RecP Range [FieldAssignment' Pattern]
| EqualP Range [(Expr,Expr)]
| EllipsisP Range
| WithP Range Pattern
deriving (Data, Eq)
data DoStmt
= DoBind Range Pattern Expr [LamClause]
| DoThen Expr
| DoLet Range [Declaration]
deriving (Data, Eq)
data Binder' a = Binder
{ binderPattern :: Maybe Pattern
, binderName :: a
} deriving (Data, Eq, Functor, Foldable, Traversable)
type Binder = Binder' BoundName
mkBinder_ :: Name -> Binder
mkBinder_ = mkBinder . mkBoundName_
mkBinder :: a -> Binder' a
mkBinder = Binder Nothing
type LamBinding = LamBinding' TypedBinding
data LamBinding' a
= DomainFree (NamedArg Binder)
| DomainFull a
deriving (Data, Functor, Foldable, Traversable, Eq)
data BoundName = BName
{ boundName :: Name
, bnameFixity :: Fixity'
, bnameTactic :: TacticAttribute
}
deriving (Data, Eq)
type TacticAttribute = Maybe Expr
mkBoundName_ :: Name -> BoundName
mkBoundName_ x = mkBoundName x noFixity'
mkBoundName :: Name -> Fixity' -> BoundName
mkBoundName x f = BName x f Nothing
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
= TBind Range [NamedArg Binder] e
| TLet Range [Declaration]
deriving (Data, Functor, Foldable, Traversable, Eq)
type Telescope = [TypedBinding]
countTelVars :: Telescope -> Nat
countTelVars tel =
sum [ case b of
TBind _ xs _ -> genericLength xs
TLet{} -> 0
| b <- tel ]
lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
lamBindingsToTelescope r = map $ \case
DomainFull ty -> ty
DomainFree nm -> TBind r [nm] $ Underscore r Nothing
makePi :: Telescope -> Expr -> Expr
makePi [] e = e
makePi bs e = Pi bs e
data LHS = LHS
{ lhsOriginalPattern :: Pattern
, lhsRewriteEqn :: [RewriteEqn]
, lhsWithExpr :: [WithHiding WithExpr]
, lhsExpandedEllipsis :: ExpandedEllipsis
}
deriving (Data, Eq)
type RewriteEqn = RewriteEqn' () Pattern Expr
type WithExpr = Expr
data LHSCore
= LHSHead { lhsDefName :: QName
, lhsPats :: [NamedArg Pattern]
}
| LHSProj { lhsDestructor :: QName
, lhsPatsLeft :: [NamedArg Pattern]
, lhsFocus :: NamedArg LHSCore
, lhsPats :: [NamedArg Pattern]
}
| LHSWith { lhsHead :: LHSCore
, lhsWithPatterns :: [Pattern]
, lhsPats :: [NamedArg Pattern]
}
deriving (Data, Eq)
type RHS = RHS' Expr
data RHS' e
= AbsurdRHS
| RHS e
deriving (Data, Functor, Foldable, Traversable, Eq)
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
= NoWhere
| AnyWhere decls
| SomeWhere Name Access decls
deriving (Data, Functor, Foldable, Traversable, Eq)
data LamClause = LamClause { lamLHS :: LHS
, lamRHS :: RHS
, lamWhere :: WhereClause
, lamCatchAll :: Bool }
deriving (Data, Eq)
data ExprWhere = ExprWhere Expr WhereClause
type ImportDirective = ImportDirective' Name Name
type Using = Using' Name Name
type Renaming = Renaming' Name Name
type ImportedName = ImportedName' Name Name
data AsName' a = AsName
{ asName :: a
, asRange :: Range
}
deriving (Data, Show, Functor, Foldable, Traversable, Eq)
type AsName = AsName' (Either Expr Name)
type TypeSignature = Declaration
type FieldSignature = Declaration
type TypeSignatureOrInstanceBlock = Declaration
data Declaration
= TypeSig ArgInfo TacticAttribute Name Expr
| FieldSig IsInstance TacticAttribute Name (Arg Expr)
| Generalize Range [TypeSignature]
| Field Range [FieldSignature]
| FunClause LHS RHS WhereClause Bool
| DataSig Range Name [LamBinding] Expr
| Data Range Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
| DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
| RecordSig Range Name [LamBinding] Expr
| RecordDef Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
| Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] Expr [Declaration]
| Infix Fixity [Name]
| Syntax Name Notation
| PatternSyn Range Name [Arg Name] Pattern
| Mutual Range [Declaration]
| Abstract Range [Declaration]
| Private Range Origin [Declaration]
| InstanceB Range [Declaration]
| Macro 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 Telescope [Declaration]
| UnquoteDecl Range [Name] Expr
| UnquoteDef Range [Name] Expr
| Pragma Pragma
deriving (Data, Eq)
data ModuleApplication
= SectionApp Range Telescope Expr
| RecordModuleInstance Range QName
deriving (Data, Eq)
data OpenShortHand = DoOpen | DontOpen
deriving (Data, Eq, Show)
data Pragma
= OptionsPragma Range [String]
| BuiltinPragma Range String QName
| RewritePragma Range [QName]
| ForeignPragma Range String String
| CompilePragma Range String QName String
| StaticPragma Range QName
| InlinePragma Range Bool QName
| ImpossiblePragma Range
| EtaPragma Range QName
| WarningOnUsage Range QName String
| WarningOnImport Range String
| InjectivePragma Range QName
| DisplayPragma Range Pattern Expr
| CatchallPragma Range
| TerminationCheckPragma Range (TerminationCheck Name)
| NoCoverageCheckPragma Range
| NoPositivityCheckPragma Range
| PolarityPragma Range Name [Occurrence]
| NoUniverseCheckPragma Range
deriving (Data, Eq)
type Module = ([Pragma], [Declaration])
topLevelModuleName :: Module -> TopLevelModuleName
topLevelModuleName (_, []) = __IMPOSSIBLE__
topLevelModuleName (_, ds) = case spanAllowedBeforeModule ds of
(_, Module _ n _ _ : _) -> toTopLevelModuleName n
_ -> __IMPOSSIBLE__
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
spanAllowedBeforeModule = span isAllowedBeforeModule
where
isAllowedBeforeModule (Pragma OptionsPragma{}) = True
isAllowedBeforeModule (Pragma BuiltinPragma{}) = True
isAllowedBeforeModule (Private _ _ ds) = all isAllowedBeforeModule ds
isAllowedBeforeModule Import{} = True
isAllowedBeforeModule ModuleMacro{} = True
isAllowedBeforeModule Open{} = True
isAllowedBeforeModule _ = False
data HoleContent' qn p e
= HoleContentExpr e
| HoleContentRewrite [RewriteEqn' qn p e]
deriving (Functor, Foldable, Traversable)
type HoleContent = HoleContent' () Pattern Expr
data AppView = AppView Expr [NamedArg Expr]
appView :: Expr -> AppView
appView e =
case e of
App r e1 e2 -> vApp (appView e1) e2
RawApp _ (e:es) -> AppView e $ map arg es
_ -> AppView e []
where
vApp (AppView e es) arg = AppView e (es ++ [arg])
arg (HiddenArg _ e) = hide $ defaultArg e
arg (InstanceArg _ e) = makeInstance $ defaultArg e
arg e = defaultArg (unnamed e)
isSingleIdentifierP :: Pattern -> Maybe Name
isSingleIdentifierP p = case removeSingletonRawAppP p of
IdentP (QName x) -> Just x
WildP r -> Just $ noName r
_ -> Nothing
removeSingletonRawAppP :: Pattern -> Pattern
removeSingletonRawAppP p = case p of
RawAppP _ [p'] -> removeSingletonRawAppP p'
ParenP _ p' -> removeSingletonRawAppP p'
_ -> p
observeHiding :: Expr -> WithHiding Expr
observeHiding = \case
RawApp _ [e] -> observeHiding e
HiddenArg _ (Named Nothing e) -> WithHiding Hidden e
InstanceArg _ (Named Nothing e) -> WithHiding (Instance NoOverlap) e
e -> WithHiding NotHidden e
isPattern :: Expr -> Maybe Pattern
isPattern = \case
Ident x -> return $ IdentP x
App _ e1 e2 -> AppP <$> isPattern e1 <*> mapM (mapM isPattern) e2
Paren r e -> ParenP r <$> isPattern e
Underscore r _ -> return $ WildP r
Absurd r -> return $ AbsurdP r
As r x e -> pushUnderBracesP r (AsP r x) <$> isPattern e
Dot r e -> return $ pushUnderBracesE r (DotP r) e
Lit l -> return $ LitP l
HiddenArg r e -> HiddenP r <$> mapM isPattern e
InstanceArg r e -> InstanceP r <$> mapM isPattern e
RawApp r es -> RawAppP r <$> mapM isPattern es
Quote r -> return $ QuoteP r
Equal r e1 e2 -> return $ EqualP r [(e1, e2)]
Ellipsis r -> return $ EllipsisP r
Rec r es -> do
fs <- mapM maybeLeft es
RecP r <$> mapM (mapM isPattern) fs
WithApp r e es -> do
p <- isPattern e
ps <- forM es $ \ e -> do
p <- isPattern e
pure $ defaultNamedArg $ WithP (getRange e) p
return $ foldl AppP p ps
_ -> Nothing
where
pushUnderBracesP :: Range -> (Pattern -> Pattern) -> (Pattern -> Pattern)
pushUnderBracesP r f = \case
HiddenP _ p -> HiddenP r (fmap f p)
InstanceP _ p -> InstanceP r (fmap f p)
p -> f p
pushUnderBracesE :: Range -> (Expr -> Pattern) -> (Expr -> Pattern)
pushUnderBracesE r f = \case
HiddenArg _ p -> HiddenP r (fmap f p)
InstanceArg _ p -> InstanceP r (fmap f p)
p -> f p
isAbsurdP :: Pattern -> Maybe (Range, Hiding)
isAbsurdP = \case
AbsurdP r -> pure (r, NotHidden)
AsP _ _ p -> isAbsurdP p
ParenP _ p -> isAbsurdP p
RawAppP _ [p] -> isAbsurdP p
HiddenP _ np -> (Hidden <$) <$> isAbsurdP (namedThing np)
InstanceP _ np -> (Instance YesOverlap <$) <$> isAbsurdP (namedThing np)
_ -> Nothing
isBinderP :: Pattern -> Maybe Binder
isBinderP = \case
IdentP qn -> mkBinder_ <$> isUnqualified qn
WildP r -> pure $ mkBinder_ (Name r InScope [Hole])
AsP r n p -> pure $ Binder (Just p) (mkBoundName_ n)
ParenP r p -> pure $ Binder (Just p) (mkBoundName_ $ Name r InScope [Hole])
_ -> Nothing
instance Null (WhereClause' a) where
empty = NoWhere
null NoWhere = True
null AnyWhere{} = False
null SomeWhere{} = False
instance LensHiding LamBinding where
getHiding (DomainFree x) = getHiding x
getHiding (DomainFull a) = getHiding a
mapHiding f (DomainFree x) = DomainFree $ mapHiding f x
mapHiding f (DomainFull a) = DomainFull $ mapHiding f a
instance LensHiding TypedBinding where
getHiding (TBind _ (x : _) _) = getHiding x
getHiding (TBind _ [] _) = __IMPOSSIBLE__
getHiding TLet{} = mempty
mapHiding f (TBind r xs e) = TBind r ((map . mapHiding) f xs) e
mapHiding f b@TLet{} = b
instance LensRelevance TypedBinding where
getRelevance (TBind _ (x : _) _) = getRelevance x
getRelevance (TBind _ [] _) = __IMPOSSIBLE__
getRelevance TLet{} = mempty
mapRelevance f (TBind r xs e) = TBind r ((map . mapRelevance) f xs) e
mapRelevance f b@TLet{} = b
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
PropN r _ -> r
Let r _ _ -> r
Paren r _ -> r
IdiomBrackets r _ -> r
DoBlock 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
Quote r -> r
QuoteTerm r -> r
Unquote r -> r
Tactic r _ -> r
DontCare{} -> noRange
Equal r _ _ -> r
Ellipsis r -> r
Generalized e -> getRange e
instance HasRange Binder where
getRange (Binder a b) = fuseRange a b
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 (RecordModuleInstance r _) = r
instance HasRange a => HasRange (FieldAssignment' a) where
getRange (FieldAssignment a b) = fuseRange a b
instance HasRange ModuleAssignment where
getRange (ModuleAssignment a b c) = fuseRange a b `fuseRange` c
instance HasRange Declaration where
getRange (TypeSig _ _ x t) = fuseRange x t
getRange (FieldSig _ _ x t) = fuseRange x t
getRange (Field r _) = r
getRange (FunClause lhs rhs wh _) = fuseRange lhs rhs `fuseRange` wh
getRange (DataSig r _ _ _) = r
getRange (Data r _ _ _ _) = r
getRange (DataDef r _ _ _) = r
getRange (RecordSig r _ _ _) = r
getRange (RecordDef r _ _ _ _ _ _) = r
getRange (Record r _ _ _ _ _ _ _) = r
getRange (Mutual r _) = r
getRange (Abstract r _) = r
getRange (Generalize r _) = r
getRange (Open r _ _) = r
getRange (ModuleMacro r _ _ _ _) = r
getRange (Import r _ _ _ _) = r
getRange (InstanceB r _) = r
getRange (Macro 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 (UnquoteDef r _ _) = r
getRange (Pragma p) = getRange p
instance HasRange LHS where
getRange (LHS p eqns ws ell) = p `fuseRange` eqns `fuseRange` ws
instance HasRange LHSCore where
getRange (LHSHead f ps) = fuseRange f ps
getRange (LHSProj d ps1 lhscore ps2) = d `fuseRange` ps1 `fuseRange` lhscore `fuseRange` ps2
getRange (LHSWith f wps ps) = f `fuseRange` wps `fuseRange` ps
instance HasRange RHS where
getRange AbsurdRHS = noRange
getRange (RHS e) = getRange e
instance HasRange LamClause where
getRange (LamClause lhs rhs wh _) = getRange (lhs, rhs, wh)
instance HasRange DoStmt where
getRange (DoBind r _ _ _) = r
getRange (DoThen e) = getRange e
getRange (DoLet r _) = r
instance HasRange Pragma where
getRange (OptionsPragma r _) = r
getRange (BuiltinPragma r _ _) = r
getRange (RewritePragma r _) = r
getRange (CompilePragma r _ _ _) = r
getRange (ForeignPragma r _ _) = r
getRange (StaticPragma r _) = r
getRange (InjectivePragma r _) = r
getRange (InlinePragma r _ _) = r
getRange (ImpossiblePragma r) = r
getRange (EtaPragma r _) = r
getRange (TerminationCheckPragma r _) = r
getRange (NoCoverageCheckPragma r) = r
getRange (WarningOnUsage r _ _) = r
getRange (WarningOnImport r _) = r
getRange (CatchallPragma r) = r
getRange (DisplayPragma r _ _) = r
getRange (NoPositivityCheckPragma r) = r
getRange (PolarityPragma r _ _) = r
getRange (NoUniverseCheckPragma r) = 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
getRange (RecP r _) = r
getRange (EqualP r _) = r
getRange (EllipsisP r) = r
getRange (WithP r _) = r
instance SetRange Pattern where
setRange r (IdentP x) = IdentP (setRange r x)
setRange r (AppP p q) = AppP (setRange r p) (setRange r q)
setRange r (OpAppP _ x ns ps) = OpAppP r x ns ps
setRange r (RawAppP _ ps) = RawAppP r ps
setRange r (ParenP _ p) = ParenP r p
setRange r (WildP _) = WildP r
setRange r (AsP _ x p) = AsP r (setRange r x) p
setRange r (AbsurdP _) = AbsurdP r
setRange r (LitP l) = LitP (setRange r l)
setRange r (QuoteP _) = QuoteP r
setRange r (HiddenP _ p) = HiddenP r p
setRange r (InstanceP _ p) = InstanceP r p
setRange r (DotP _ e) = DotP r e
setRange r (RecP _ fs) = RecP r fs
setRange r (EqualP _ es) = EqualP r es
setRange r (EllipsisP _) = EllipsisP r
setRange r (WithP _ p) = WithP r p
instance SetRange TypedBinding where
setRange r (TBind _ xs e) = TBind r xs e
setRange r (TLet _ ds) = TLet r ds
instance KillRange a => KillRange (FieldAssignment' a) where
killRange (FieldAssignment a b) = killRange2 FieldAssignment a b
instance KillRange ModuleAssignment where
killRange (ModuleAssignment a b c) = killRange3 ModuleAssignment a b c
instance KillRange AsName where
killRange (AsName n _) = killRange1 (flip AsName noRange) n
instance KillRange Binder where
killRange (Binder a b) = killRange2 Binder a b
instance KillRange BoundName where
killRange (BName n f t) = killRange3 BName n f t
instance KillRange Declaration where
killRange (TypeSig i t n e) = killRange3 (TypeSig i) t n e
killRange (FieldSig i t n e) = killRange4 FieldSig i t n e
killRange (Generalize r ds ) = killRange1 (Generalize noRange) ds
killRange (Field r fs) = killRange1 (Field noRange) fs
killRange (FunClause l r w ca) = killRange4 FunClause l r w ca
killRange (DataSig _ n l e) = killRange3 (DataSig noRange) n l e
killRange (Data _ n l e c) = killRange4 (Data noRange) n l e c
killRange (DataDef _ n l c) = killRange3 (DataDef noRange) n l c
killRange (RecordSig _ n l e) = killRange3 (RecordSig noRange) n l e
killRange (RecordDef _ n mi mb mn k d) = killRange6 (RecordDef noRange) n mi mb mn k d
killRange (Record _ n mi mb mn k e d) = killRange7 (Record noRange) n mi mb 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 _ o d) = killRange2 (Private noRange) o d
killRange (InstanceB _ d) = killRange1 (InstanceB noRange) d
killRange (Macro _ d) = killRange1 (Macro 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 (UnquoteDef _ x t) = killRange2 (UnquoteDef 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 ns o) = killRange3 (OpApp noRange) n ns 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 (PropN _ n) = PropN 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 (IdiomBrackets _ es) = killRange1 (IdiomBrackets noRange) es
killRange (DoBlock _ ss) = killRange1 (DoBlock noRange) ss
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 (Quote _) = Quote noRange
killRange (QuoteTerm _) = QuoteTerm noRange
killRange (Unquote _) = Unquote noRange
killRange (Tactic _ t) = killRange1 (Tactic noRange) t
killRange (DontCare e) = killRange1 DontCare e
killRange (Equal _ x y) = Equal noRange x y
killRange (Ellipsis _) = Ellipsis noRange
killRange (Generalized e) = killRange1 Generalized e
instance KillRange LamBinding where
killRange (DomainFree b) = killRange1 DomainFree b
killRange (DomainFull t) = killRange1 DomainFull t
instance KillRange LHS where
killRange (LHS p r w e) = killRange4 LHS p r w e
instance KillRange LamClause where
killRange (LamClause a b c d) = killRange4 LamClause a b c d
instance KillRange DoStmt where
killRange (DoBind r p e w) = killRange4 DoBind r p e w
killRange (DoThen e) = killRange1 DoThen e
killRange (DoLet r ds) = killRange2 DoLet r ds
instance KillRange ModuleApplication where
killRange (SectionApp _ t e) = killRange2 (SectionApp noRange) t e
killRange (RecordModuleInstance _ q) = killRange1 (RecordModuleInstance 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 ps) = killRange2 AppP p ps
killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p
killRange (OpAppP _ n ns p) = killRange3 (OpAppP noRange) n ns 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
killRange (RecP _ fs) = killRange1 (RecP noRange) fs
killRange (EqualP _ es) = killRange1 (EqualP noRange) es
killRange (EllipsisP _) = EllipsisP noRange
killRange (WithP _ p) = killRange1 (WithP noRange) p
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s
killRange (BuiltinPragma _ s e) = killRange1 (BuiltinPragma noRange s) e
killRange (RewritePragma _ qs) = killRange1 (RewritePragma noRange) qs
killRange (StaticPragma _ q) = killRange1 (StaticPragma noRange) q
killRange (InjectivePragma _ q) = killRange1 (InjectivePragma noRange) q
killRange (InlinePragma _ b q) = killRange1 (InlinePragma noRange b) q
killRange (CompilePragma _ b q s) = killRange1 (\ q -> CompilePragma noRange b q s) q
killRange (ForeignPragma _ b s) = ForeignPragma noRange b s
killRange (ImpossiblePragma _) = ImpossiblePragma noRange
killRange (TerminationCheckPragma _ t) = TerminationCheckPragma noRange (killRange t)
killRange (NoCoverageCheckPragma _) = NoCoverageCheckPragma noRange
killRange (WarningOnUsage _ nm str) = WarningOnUsage noRange (killRange nm) str
killRange (WarningOnImport _ str) = WarningOnImport noRange str
killRange (CatchallPragma _) = CatchallPragma noRange
killRange (DisplayPragma _ lhs rhs) = killRange2 (DisplayPragma noRange) lhs rhs
killRange (EtaPragma _ q) = killRange1 (EtaPragma noRange) q
killRange (NoPositivityCheckPragma _) = NoPositivityCheckPragma noRange
killRange (PolarityPragma _ q occs) = killRange1 (\q -> PolarityPragma noRange q occs) q
killRange (NoUniverseCheckPragma _) = NoUniverseCheckPragma noRange
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 WhereClause where
killRange NoWhere = NoWhere
killRange (AnyWhere d) = killRange1 AnyWhere d
killRange (SomeWhere n a d) = killRange3 SomeWhere n a d
instance NFData Expr where
rnf (Ident a) = rnf a
rnf (Lit a) = rnf a
rnf (QuestionMark _ a) = rnf a
rnf (Underscore _ a) = rnf a
rnf (RawApp _ a) = rnf a
rnf (App _ a b) = rnf a `seq` rnf b
rnf (OpApp _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (WithApp _ a b) = rnf a `seq` rnf b
rnf (HiddenArg _ a) = rnf a
rnf (InstanceArg _ a) = rnf a
rnf (Lam _ a b) = rnf a `seq` rnf b
rnf (AbsurdLam _ a) = rnf a
rnf (ExtendedLam _ a) = rnf a
rnf (Fun _ a b) = rnf a `seq` rnf b
rnf (Pi a b) = rnf a `seq` rnf b
rnf (Set _) = ()
rnf (Prop _) = ()
rnf (SetN _ a) = rnf a
rnf (PropN _ a) = rnf a
rnf (Rec _ a) = rnf a
rnf (RecUpdate _ a b) = rnf a `seq` rnf b
rnf (Let _ a b) = rnf a `seq` rnf b
rnf (Paren _ a) = rnf a
rnf (IdiomBrackets _ a)= rnf a
rnf (DoBlock _ a) = rnf a
rnf (Absurd _) = ()
rnf (As _ a b) = rnf a `seq` rnf b
rnf (Dot _ a) = rnf a
rnf (ETel a) = rnf a
rnf (Quote _) = ()
rnf (QuoteTerm _) = ()
rnf (Tactic _ a) = rnf a
rnf (Unquote _) = ()
rnf (DontCare a) = rnf a
rnf (Equal _ a b) = rnf a `seq` rnf b
rnf (Ellipsis _) = ()
rnf (Generalized e) = rnf e
instance NFData Pattern where
rnf (IdentP a) = rnf a
rnf (QuoteP _) = ()
rnf (AppP a b) = rnf a `seq` rnf b
rnf (RawAppP _ a) = rnf a
rnf (OpAppP _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (HiddenP _ a) = rnf a
rnf (InstanceP _ a) = rnf a
rnf (ParenP _ a) = rnf a
rnf (WildP _) = ()
rnf (AbsurdP _) = ()
rnf (AsP _ a b) = rnf a `seq` rnf b
rnf (DotP _ a) = rnf a
rnf (LitP a) = rnf a
rnf (RecP _ a) = rnf a
rnf (EqualP _ es) = rnf es
rnf (EllipsisP _) = ()
rnf (WithP _ a) = rnf a
instance NFData Declaration where
rnf (TypeSig a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
rnf (FieldSig a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
rnf (Generalize _ a) = rnf a
rnf (Field _ fs) = rnf fs
rnf (FunClause a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
rnf (DataSig _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (Data _ a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
rnf (DataDef _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (RecordSig _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (RecordDef _ a b c d e f) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e `seq` rnf f
rnf (Record _ a b c d e f g) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e `seq` rnf f `seq` rnf g
rnf (Infix a b) = rnf a `seq` rnf b
rnf (Syntax a b) = rnf a `seq` rnf b
rnf (PatternSyn _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (Mutual _ a) = rnf a
rnf (Abstract _ a) = rnf a
rnf (Private _ _ a) = rnf a
rnf (InstanceB _ a) = rnf a
rnf (Macro _ a) = rnf a
rnf (Postulate _ a) = rnf a
rnf (Primitive _ a) = rnf a
rnf (Open _ a b) = rnf a `seq` rnf b
rnf (Import _ a b _ c) = rnf a `seq` rnf b `seq` rnf c
rnf (ModuleMacro _ a b _ c) = rnf a `seq` rnf b `seq` rnf c
rnf (Module _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (UnquoteDecl _ a b) = rnf a `seq` rnf b
rnf (UnquoteDef _ a b) = rnf a `seq` rnf b
rnf (Pragma a) = rnf a
instance NFData Pragma where
rnf (OptionsPragma _ a) = rnf a
rnf (BuiltinPragma _ a b) = rnf a `seq` rnf b
rnf (RewritePragma _ a) = rnf a
rnf (CompilePragma _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (ForeignPragma _ b s) = rnf b `seq` rnf s
rnf (StaticPragma _ a) = rnf a
rnf (InjectivePragma _ a) = rnf a
rnf (InlinePragma _ _ a) = rnf a
rnf (ImpossiblePragma _) = ()
rnf (EtaPragma _ a) = rnf a
rnf (TerminationCheckPragma _ a) = rnf a
rnf (NoCoverageCheckPragma _) = ()
rnf (WarningOnUsage _ a b) = rnf a `seq` rnf b
rnf (WarningOnImport _ a) = rnf a
rnf (CatchallPragma _) = ()
rnf (DisplayPragma _ a b) = rnf a `seq` rnf b
rnf (NoPositivityCheckPragma _) = ()
rnf (PolarityPragma _ a b) = rnf a `seq` rnf b
rnf (NoUniverseCheckPragma _) = ()
instance NFData AsName where
rnf (AsName a _) = rnf a
instance NFData a => NFData (TypedBinding' a) where
rnf (TBind _ a b) = rnf a `seq` rnf b
rnf (TLet _ a) = rnf a
instance NFData ModuleApplication where
rnf (SectionApp _ a b) = rnf a `seq` rnf b
rnf (RecordModuleInstance _ a) = rnf a
instance NFData a => NFData (OpApp a) where
rnf (SyntaxBindingLambda _ a b) = rnf a `seq` rnf b
rnf (Ordinary a) = rnf a
instance NFData LHS where
rnf (LHS a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
instance NFData a => NFData (FieldAssignment' a) where
rnf (FieldAssignment a b) = rnf a `seq` rnf b
instance NFData ModuleAssignment where
rnf (ModuleAssignment a b c) = rnf a `seq` rnf b `seq` rnf c
instance NFData a => NFData (WhereClause' a) where
rnf NoWhere = ()
rnf (AnyWhere a) = rnf a
rnf (SomeWhere a b c) = rnf a `seq` rnf b `seq` rnf c
instance NFData LamClause where
rnf (LamClause a b c d) = rnf (a, b, c, d)
instance NFData a => NFData (LamBinding' a) where
rnf (DomainFree a) = rnf a
rnf (DomainFull a) = rnf a
instance NFData Binder where
rnf (Binder a b) = rnf a `seq` rnf b
instance NFData BoundName where
rnf (BName a b c) = rnf a `seq` rnf b `seq` rnf c
instance NFData a => NFData (RHS' a) where
rnf AbsurdRHS = ()
rnf (RHS a) = rnf a
instance NFData DoStmt where
rnf (DoBind _ p e w) = rnf (p, e, w)
rnf (DoThen e) = rnf e
rnf (DoLet _ ds) = rnf ds