Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Concrete

Contents

Expressions
Bindings
Declarations

Description

The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.

Synopsis

data Expr
- = Ident QName
- | Lit Range Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe String)
- | RawApp Range (List2 Expr)
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set Name) OpAppArgs
- | WithApp Range Expr [Expr]
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range (List1 LamBinding) Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range Erased (List1 LamClause)
- | Fun Range (Arg Expr) Expr
- | Pi Telescope1 Expr
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range (List1 Declaration) (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range [Expr]
- | DoBlock Range (List1 DoStmt)
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | DoubleDot Range Expr
- | ETel Telescope
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
- | Generalized Expr
data OpApp e
- = SyntaxBindingLambda Range (List1 LamBinding) e
- | Ordinary e
fromOrdinary :: e -> OpApp e -> e
type OpAppArgs = OpAppArgs' Expr
type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))]
module Agda.Syntax.Concrete.Name
data AppView = AppView Expr [NamedArg Expr]
appView :: Expr -> AppView
unAppView :: AppView -> Expr
rawApp :: List1 Expr -> Expr
rawAppP :: List1 Pattern -> Pattern
isSingleIdentifierP :: Pattern -> Maybe Name
removeParenP :: Pattern -> Pattern
isPattern :: Expr -> Maybe Pattern
isAbsurdP :: Pattern -> Maybe (Range, Hiding)
isBinderP :: Pattern -> Maybe Binder
exprToPatternWithHoles :: Expr -> Pattern
returnExpr :: Expr -> Maybe Expr
data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
}
type Binder = Binder' BoundName
mkBinder_ :: Name -> Binder
mkBinder :: a -> Binder' a
type LamBinding = LamBinding' TypedBinding
data LamBinding' a
- = DomainFree (NamedArg Binder)
- | DomainFull a
dropTypeAndModality :: LamBinding -> [LamBinding]
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
- = TBind Range (List1 (NamedArg Binder)) e
- | TLet Range (List1 Declaration)
type RecordAssignment = Either FieldAssignment ModuleAssignment
type RecordAssignments = [RecordAssignment]
type FieldAssignment = FieldAssignment' Expr
data FieldAssignment' a = FieldAssignment {
- _nameFieldA :: Name
- _exprFieldA :: a
}
nameFieldA :: Lens' Name (FieldAssignment' a)
exprFieldA :: Lens' a (FieldAssignment' a)
data ModuleAssignment = ModuleAssignment {
- _qnameModA :: QName
- _exprModA :: [Expr]
- _importDirModA :: ImportDirective
}
data BoundName = BName {
- boundName :: Name
- bnameFixity :: Fixity'
- bnameTactic :: TacticAttribute
}
mkBoundName_ :: Name -> BoundName
mkBoundName :: Name -> Fixity' -> BoundName
type TacticAttribute = Maybe Expr
type Telescope = [TypedBinding]
type Telescope1 = List1 TypedBinding
lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
makePi :: Telescope -> Expr -> Expr
mkLam :: Range -> [LamBinding] -> Expr -> Expr
mkLet :: Range -> [Declaration] -> Expr -> Expr
mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e)
data RecordDirective
- = Induction (Ranged Induction)
- | Constructor Name IsInstance
- | Eta (Ranged HasEta0)
- | PatternOrCopattern Range
isRecordDirective :: Declaration -> Maybe RecordDirective
type RecordDirectives = RecordDirectives' (Name, IsInstance)
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 RecordDirectives [LamBinding] [Declaration]
- | Record Range Name RecordDirectives [LamBinding] Expr [Declaration]
- | RecordDirective RecordDirective
- | Infix Fixity (List1 Name)
- | Syntax Name Notation
- | PatternSyn Range Name [Arg Name] Pattern
- | Mutual Range [Declaration]
- | InterleavedMutual Range [Declaration]
- | Abstract Range [Declaration]
- | Private Range Origin [Declaration]
- | InstanceB Range [Declaration]
- | LoneConstructor 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
data ModuleApplication
- = SectionApp Range Telescope Expr
- | RecordModuleInstance Range QName
type TypeSignature = Declaration
type TypeSignatureOrInstanceBlock = Declaration
type ImportDirective = ImportDirective' Name Name
type Using = Using' Name Name
type ImportedName = ImportedName' Name Name
type Renaming = Renaming' Name Name
type RenamingDirective = RenamingDirective' Name Name
type HidingDirective = HidingDirective' Name Name
data AsName' a = AsName {
- asName :: a
- asRange :: Range
}
type AsName = AsName' (Either Expr Name)
data OpenShortHand
- = DoOpen
- | DontOpen
type RewriteEqn = RewriteEqn' () Name Pattern Expr
type WithExpr = Named Name (Arg Expr)
data LHS = LHS {
- lhsOriginalPattern :: Pattern
- lhsRewriteEqn :: [RewriteEqn]
- lhsWithExpr :: [WithExpr]
}
data Pattern
- = IdentP QName
- | QuoteP Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP Range (List2 Pattern)
- | OpAppP Range QName (Set 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 Range Literal
- | RecP Range [FieldAssignment' Pattern]
- | EqualP Range [(Expr, Expr)]
- | EllipsisP Range (Maybe Pattern)
- | WithP Range Pattern
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]
  }
- | LHSEllipsis {
  - lhsEllipsisRange :: Range
  - lhsEllipsisPat :: LHSCore
  }
observeHiding :: Expr -> WithHiding Expr
observeRelevance :: Expr -> (Relevance, Expr)
observeModifiers :: Expr -> Arg Expr
data LamClause = LamClause {
- lamLHS :: [Pattern]
- lamRHS :: RHS
- lamCatchAll :: Bool
}
type RHS = RHS' Expr
data RHS' e
- = AbsurdRHS
- | RHS e
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
- = NoWhere
- | AnyWhere Range decls
- | SomeWhere Range Name Access decls
data ExprWhere = ExprWhere Expr WhereClause
data DoStmt
- = DoBind Range Pattern Expr [LamClause]
- | DoThen Expr
- | DoLet Range (List1 Declaration)
data Pragma
- = OptionsPragma Range [String]
- | BuiltinPragma Range RString QName
- | RewritePragma Range Range [QName]
- | ForeignPragma Range RString String
- | CompilePragma Range RString QName String
- | StaticPragma Range QName
- | InlinePragma Range Bool QName
- | ImpossiblePragma Range [String]
- | EtaPragma Range QName
- | WarningOnUsage Range QName Text
- | WarningOnImport Range Text
- | InjectivePragma Range QName
- | DisplayPragma Range Pattern Expr
- | CatchallPragma Range
- | TerminationCheckPragma Range (TerminationCheck Name)
- | NoCoverageCheckPragma Range
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
- | NoUniverseCheckPragma Range
data Module = Mod {
- modPragmas :: [Pragma]
- modDecls :: [Declaration]
}
data ThingWithFixity x = ThingWithFixity x Fixity'
type HoleContent = HoleContent' () Name Pattern Expr
data HoleContent' qn nm p e
- = HoleContentExpr e
- | HoleContentRewrite [RewriteEqn' qn nm p e]
topLevelModuleName :: Module -> TopLevelModuleName
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])

Expressions

data Expr Source #

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName	ex: `x`
Lit Range Literal	ex: `1` or `"foo"`
QuestionMark Range (Maybe Nat)	ex: `?` or `{! ... !}`
Underscore Range (Maybe String)	ex: `_` or `_A_5`
RawApp Range (List2 Expr)	before parsing operators
App Range Expr (NamedArg Expr)	ex: `e e`, `e {e}`, or `e {x = e}`
OpApp Range QName (Set Name) OpAppArgs	ex: `e + e` The `QName` is possibly ambiguous, but it must correspond to one of the names in the set.
WithApp Range Expr [Expr]	ex: `e \| e1 \| .. \| en`
HiddenArg Range (Named_ Expr)	ex: `{e}` or `{x=e}`
InstanceArg Range (Named_ Expr)	ex: `{{e}}` or `{{x=e}}`
Lam Range (List1 LamBinding) Expr	ex: `\x {y} -> e` or `\(x:A){y:B} -> e`
AbsurdLam Range Hiding	ex: `\ ()`
ExtendedLam Range Erased (List1 LamClause)	ex: `\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }`
Fun Range (Arg Expr) Expr	ex: `e -> e` or `.e -> e` (NYI: `{e} -> e`)
Pi Telescope1 Expr	ex: `(xs:e) -> e` or `{xs:e} -> e`
Rec Range RecordAssignments	ex: `record {x = a; y = b}`, or `record { x = a; M1; M2 }`
RecUpdate Range Expr [FieldAssignment]	ex: `record e {x = a; y = b}`
Let Range (List1 Declaration) (Maybe Expr)	ex: `let Ds in e`, missing body when parsing do-notation let
Paren Range Expr	ex: `(e)`
IdiomBrackets Range [Expr]	ex: `(\| e1 \| e2 \| .. \| en \|)` or `(\|)`
DoBlock Range (List1 DoStmt)	ex: `do x <- m1; m2`
Absurd Range	ex: `()` or `{}`, only in patterns
As Range Name Expr	ex: `x@p`, only in patterns
Dot Range Expr	ex: `.p`, only in patterns
DoubleDot Range Expr	ex: `..A`, used for parsing `..A -> B`
ETel Telescope	only used for printing telescopes
Quote Range	ex: `quote`, should be applied to a name
QuoteTerm Range	ex: `quoteTerm`, should be applied to a term
Tactic Range Expr	ex: `@(tactic t)`, used to declare tactic arguments
Unquote Range	ex: `unquote`, should be applied to a term of type `Term`
DontCare Expr	to print irrelevant things
Equal Range Expr Expr	ex: `a = b`, used internally in the parser
Ellipsis Range	`...`, used internally to parse patterns.
Generalized Expr

Instances

Instances details

LensHiding LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
LensHiding TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
LensRelevance TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source #
ExprLike Expr Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Expr -> Expr Source # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr Source #
ExprLike FieldAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment Source #
ExprLike LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source #
IsExpr Expr Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Expr -> ExprView Expr Source # unExprView :: ExprView Expr -> Expr Source # patternView :: Expr -> Maybe Pattern Source #
HasRange AsName Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range Source #
HasRange Expr Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Expr -> Range Source #
HasRange LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source #
HasRange RHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range Source #
HasRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source #
KillRange AsName Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName Source #
KillRange Expr Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Expr Source #
KillRange LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding Source #
KillRange RHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS Source #
KillRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding Source #
SetRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source #
ToAbstract Expr Source #	Scope check an expression.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Expr Source # Methods toAbstract :: Expr -> ScopeM (AbsOfCon Expr) Source #
ToAbstract HoleContent Source #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon HoleContent Source # Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #
ToAbstract LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LamBinding Source # Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #
ToAbstract RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RHS Source # Methods toAbstract :: RHS -> ScopeM (AbsOfCon RHS) Source #
ToAbstract RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RewriteEqn Source # Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #
ToAbstract TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon TypedBinding Source # Methods toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source #
Pretty Expr Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Expr -> Doc Source # prettyPrec :: Int -> Expr -> Doc Source # prettyList :: [Expr] -> Doc Source #
Pretty LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
Pretty RHS Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RHS -> Doc Source # prettyPrec :: Int -> RHS -> Doc Source # prettyList :: [RHS] -> Doc Source #
Pretty TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source #
Data Expr Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr # toConstr :: Expr -> Constr # dataTypeOf :: Expr -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) # gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #
Show Expr Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Show LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Show RHS Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
Show TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
NFData AsName Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () #
NFData Expr Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Expr -> () #
Eq Expr Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
ToAbstract (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (LHSCore' Expr) Source # Methods toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #
ToAbstract (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Pattern' Expr) Source # Methods toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) Source #
Pretty (OpApp Expr) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpApp Expr -> Doc Source # prettyPrec :: Int -> OpApp Expr -> Doc Source # prettyList :: [OpApp Expr] -> Doc Source #
EncodeTCM (OutputForm Expr Expr) Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: OutputForm Expr Expr -> TCM Value Source #
type AbsOfCon Expr Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Expr = Expr
type AbsOfCon HoleContent Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent
type AbsOfCon LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding
type AbsOfCon RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RHS = AbstractRHS
type AbsOfCon RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr
type AbsOfCon TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon TypedBinding = Maybe TypedBinding
type AbsOfCon (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr
type AbsOfCon (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr

data OpApp e Source #

Constructors

SyntaxBindingLambda Range (List1 LamBinding) e	An abstraction inside a special syntax declaration (see Issue 358 why we introduce this).
Ordinary e

Instances

Instances details

Foldable OpApp Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => OpApp m -> m # foldMap :: Monoid m => (a -> m) -> OpApp a -> m # foldMap' :: Monoid m => (a -> m) -> OpApp a -> m # foldr :: (a -> b -> b) -> b -> OpApp a -> b # foldr' :: (a -> b -> b) -> b -> OpApp a -> b # foldl :: (b -> a -> b) -> b -> OpApp a -> b # foldl' :: (b -> a -> b) -> b -> OpApp a -> b # foldr1 :: (a -> a -> a) -> OpApp a -> a # foldl1 :: (a -> a -> a) -> OpApp a -> a # toList :: OpApp a -> [a] # null :: OpApp a -> Bool # length :: OpApp a -> Int # elem :: Eq a => a -> OpApp a -> Bool # maximum :: Ord a => OpApp a -> a # minimum :: Ord a => OpApp a -> a # sum :: Num a => OpApp a -> a # product :: Num a => OpApp a -> a #
Traversable OpApp Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> OpApp a -> f (OpApp b) # sequenceA :: Applicative f => OpApp (f a) -> f (OpApp a) # mapM :: Monad m => (a -> m b) -> OpApp a -> m (OpApp b) # sequence :: Monad m => OpApp (m a) -> m (OpApp a) #
Functor OpApp Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> OpApp a -> OpApp b # (<$) :: a -> OpApp b -> OpApp a #
ExprLike a => ExprLike (OpApp a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a Source # foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a) Source #
HasRange e => HasRange (OpApp e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: OpApp e -> Range Source #
KillRange e => KillRange (OpApp e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source #
Pretty (OpApp Expr) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpApp Expr -> Doc Source # prettyPrec :: Int -> OpApp Expr -> Doc Source # prettyList :: [OpApp Expr] -> Doc Source #
Data e => Data (OpApp e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpApp e -> c (OpApp e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e) # toConstr :: OpApp e -> Constr # dataTypeOf :: OpApp e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e)) # gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r # gmapQ :: (forall d. Data d => d -> u) -> OpApp e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> OpApp e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) #
Show a => Show (OpApp a) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> OpApp a -> ShowS # show :: OpApp a -> String # showList :: [OpApp a] -> ShowS #
NFData a => NFData (OpApp a) Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: OpApp a -> () #
Eq e => Eq (OpApp e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: OpApp e -> OpApp e -> Bool # (/=) :: OpApp e -> OpApp e -> Bool #

fromOrdinary :: e -> OpApp e -> e Source #

type OpAppArgs = OpAppArgs' Expr Source #

type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))] Source #

module Agda.Syntax.Concrete.Name

data AppView Source #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr]

appView :: Expr -> AppView Source #

unAppView :: AppView -> Expr Source #

rawApp :: List1 Expr -> Expr Source #

rawAppP :: List1 Pattern -> Pattern Source #

isSingleIdentifierP :: Pattern -> Maybe Name Source #

removeParenP :: Pattern -> Pattern Source #

isPattern :: Expr -> Maybe Pattern Source #

Turn an expression into a pattern. Fails if the expression is not a valid pattern.

isAbsurdP :: Pattern -> Maybe (Range, Hiding) Source #

isBinderP :: Pattern -> Maybe Binder Source #

exprToPatternWithHoles :: Expr -> Pattern Source #

Turn an expression into a pattern, turning non-pattern subexpressions into WildP.

returnExpr :: Expr -> Maybe Expr Source #

Bindings

data Binder' a Source #

A Binder x@p, the pattern is optional

Constructors

Binder
Fields binderPattern :: Maybe Pattern binderName :: a

Instances

Instances details

HasRange Binder Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Binder -> Range Source #
KillRange Binder Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Binder Source #
Foldable Binder' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => Binder' m -> m # foldMap :: Monoid m => (a -> m) -> Binder' a -> m # foldMap' :: Monoid m => (a -> m) -> Binder' a -> m # foldr :: (a -> b -> b) -> b -> Binder' a -> b # foldr' :: (a -> b -> b) -> b -> Binder' a -> b # foldl :: (b -> a -> b) -> b -> Binder' a -> b # foldl' :: (b -> a -> b) -> b -> Binder' a -> b # foldr1 :: (a -> a -> a) -> Binder' a -> a # foldl1 :: (a -> a -> a) -> Binder' a -> a # toList :: Binder' a -> [a] # null :: Binder' a -> Bool # length :: Binder' a -> Int # elem :: Eq a => a -> Binder' a -> Bool # maximum :: Ord a => Binder' a -> a # minimum :: Ord a => Binder' a -> a # sum :: Num a => Binder' a -> a # product :: Num a => Binder' a -> a #
Traversable Binder' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) # sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) # mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) # sequence :: Monad m => Binder' (m a) -> m (Binder' a) #
Functor Binder' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> Binder' a -> Binder' b # (<$) :: a -> Binder' b -> Binder' a #
NFData Binder Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Binder -> () #
ToAbstract (Binder' (NewName BoundName)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Binder' (NewName BoundName)) Source # Methods toAbstract :: Binder' (NewName BoundName) -> ScopeM (AbsOfCon (Binder' (NewName BoundName))) Source #
Pretty a => Pretty (Binder' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Binder' a -> Doc Source # prettyPrec :: Int -> Binder' a -> Doc Source # prettyList :: [Binder' a] -> Doc Source #
Data a => Data (Binder' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder' a -> c (Binder' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder' a) # toConstr :: Binder' a -> Constr # dataTypeOf :: Binder' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder' a)) # gmapT :: (forall b. Data b => b -> b) -> Binder' a -> Binder' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Binder' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) #
Show a => Show (Binder' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Binder' a -> ShowS # show :: Binder' a -> String # showList :: [Binder' a] -> ShowS #
Eq a => Eq (Binder' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Binder' a -> Binder' a -> Bool # (/=) :: Binder' a -> Binder' a -> Bool #
type AbsOfCon (Binder' (NewName BoundName)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Binder' (NewName BoundName)) = Binder

type Binder = Binder' BoundName Source #

mkBinder_ :: Name -> Binder Source #

mkBinder :: a -> Binder' a Source #

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

DomainFree (NamedArg Binder)	. `x` or `{x}` or `.x` or `.{x}` or `{.x}` or `x@p` or `(p)`
DomainFull a	. `(xs : e)` or `{xs : e}`

Instances

Instances details

LensHiding LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
ExprLike LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source #
HasRange LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source #
KillRange LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding Source #
ToAbstract LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LamBinding Source # Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #
Pretty LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
Foldable LamBinding' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => LamBinding' m -> m # foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m # foldMap' :: Monoid m => (a -> m) -> LamBinding' a -> m # foldr :: (a -> b -> b) -> b -> LamBinding' a -> b # foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b # foldl :: (b -> a -> b) -> b -> LamBinding' a -> b # foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b # foldr1 :: (a -> a -> a) -> LamBinding' a -> a # foldl1 :: (a -> a -> a) -> LamBinding' a -> a # toList :: LamBinding' a -> [a] # null :: LamBinding' a -> Bool # length :: LamBinding' a -> Int # elem :: Eq a => a -> LamBinding' a -> Bool # maximum :: Ord a => LamBinding' a -> a # minimum :: Ord a => LamBinding' a -> a # sum :: Num a => LamBinding' a -> a # product :: Num a => LamBinding' a -> a #
Traversable LamBinding' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) # sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) # mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) # sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) #
Functor LamBinding' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b # (<$) :: a -> LamBinding' b -> LamBinding' a #
Show LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Data a => Data (LamBinding' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding' a -> c (LamBinding' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LamBinding' a) # toConstr :: LamBinding' a -> Constr # dataTypeOf :: LamBinding' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LamBinding' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LamBinding' a)) # gmapT :: (forall b. Data b => b -> b) -> LamBinding' a -> LamBinding' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r # gmapQ :: (forall d. Data d => d -> u) -> LamBinding' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) #
NFData a => NFData (LamBinding' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamBinding' a -> () #
Eq a => Eq (LamBinding' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LamBinding' a -> LamBinding' a -> Bool # (/=) :: LamBinding' a -> LamBinding' a -> Bool #
type AbsOfCon LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding

dropTypeAndModality :: LamBinding -> [LamBinding] Source #

Drop type annotations and lets from bindings.

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

Constructors

TBind Range (List1 (NamedArg Binder)) e	Binding `(x1@p1 ... xn@pn : A)`.
TLet Range (List1 Declaration)	Let binding `(let Ds)` or `(open M args)`.

Instances

Instances details

LensHiding LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
LensHiding TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
LensRelevance TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source #
ExprLike LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source #
HasRange LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source #
HasRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source #
KillRange LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding Source #
KillRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding Source #
SetRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source #
ToAbstract LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LamBinding Source # Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #
ToAbstract TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon TypedBinding Source # Methods toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source #
Pretty LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
Pretty TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source #
Foldable TypedBinding' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => TypedBinding' m -> m # foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m # foldMap' :: Monoid m => (a -> m) -> TypedBinding' a -> m # foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b # foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b # foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b # foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b # foldr1 :: (a -> a -> a) -> TypedBinding' a -> a # foldl1 :: (a -> a -> a) -> TypedBinding' a -> a # toList :: TypedBinding' a -> [a] # null :: TypedBinding' a -> Bool # length :: TypedBinding' a -> Int # elem :: Eq a => a -> TypedBinding' a -> Bool # maximum :: Ord a => TypedBinding' a -> a # minimum :: Ord a => TypedBinding' a -> a # sum :: Num a => TypedBinding' a -> a # product :: Num a => TypedBinding' a -> a #
Traversable TypedBinding' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b) # sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a) # mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b) # sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a) #
Functor TypedBinding' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b # (<$) :: a -> TypedBinding' b -> TypedBinding' a #
Show LamBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Show TypedBinding Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
ExprLike a => ExprLike (TypedBinding' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a Source # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a) Source #
Data e => Data (TypedBinding' e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding' e -> c (TypedBinding' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedBinding' e) # toConstr :: TypedBinding' e -> Constr # dataTypeOf :: TypedBinding' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedBinding' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (TypedBinding' e)) # gmapT :: (forall b. Data b => b -> b) -> TypedBinding' e -> TypedBinding' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedBinding' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) #
NFData a => NFData (TypedBinding' a) Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: TypedBinding' a -> () #
Eq e => Eq (TypedBinding' e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: TypedBinding' e -> TypedBinding' e -> Bool # (/=) :: TypedBinding' e -> TypedBinding' e -> Bool #
type AbsOfCon LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding
type AbsOfCon TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon TypedBinding = Maybe TypedBinding

type RecordAssignment = Either FieldAssignment ModuleAssignment Source #

type RecordAssignments = [RecordAssignment] Source #

type FieldAssignment = FieldAssignment' Expr Source #

data FieldAssignment' a Source #

Constructors

FieldAssignment
Fields _nameFieldA :: Name _exprFieldA :: a

Instances

Instances details

ExprLike FieldAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment Source #
Foldable FieldAssignment' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => FieldAssignment' m -> m # foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m # foldMap' :: Monoid m => (a -> m) -> FieldAssignment' a -> m # foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b # foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b # foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b # foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b # foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a # foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a # toList :: FieldAssignment' a -> [a] # null :: FieldAssignment' a -> Bool # length :: FieldAssignment' a -> Int # elem :: Eq a => a -> FieldAssignment' a -> Bool # maximum :: Ord a => FieldAssignment' a -> a # minimum :: Ord a => FieldAssignment' a -> a # sum :: Num a => FieldAssignment' a -> a # product :: Num a => FieldAssignment' a -> a #
Traversable FieldAssignment' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b) # sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a) # mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b) # sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a) #
Functor FieldAssignment' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b # (<$) :: a -> FieldAssignment' b -> FieldAssignment' a #
SubstExpr a => SubstExpr (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source #
APatternLike a => APatternLike (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (FieldAssignment' a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (FieldAssignment' a)) -> m -> m) -> FieldAssignment' a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> FieldAssignment' a -> m (FieldAssignment' a) Source #
MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source #
DeclaredNames a => DeclaredNames (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => FieldAssignment' a -> m Source #
ExprLike a => ExprLike (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (FieldAssignment' a) Source # foldExpr :: FoldExprFn m (FieldAssignment' a) Source # traverseExpr :: TraverseExprFn m (FieldAssignment' a) Source # mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a Source #
CPatternLike p => CPatternLike (FieldAssignment' p) Source #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #
NamesIn a => NamesIn (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn' :: Monoid m => (QName -> m) -> FieldAssignment' a -> m Source #
HasRange a => HasRange (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range Source #
KillRange a => KillRange (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) Source #
ToConcrete a => ToConcrete (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (FieldAssignment' a) Source # Methods toConcrete :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a)) Source # bindToConcrete :: FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c => ToAbstract (FieldAssignment' c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (FieldAssignment' c) Source # Methods toAbstract :: FieldAssignment' c -> ScopeM (AbsOfCon (FieldAssignment' c)) Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source #
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Int32 Source # icod_ :: FieldAssignment' a -> S Int32 Source # value :: Int32 -> R (FieldAssignment' a) Source #
Pretty a => Pretty (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: FieldAssignment' a -> Doc Source # prettyPrec :: Int -> FieldAssignment' a -> Doc Source # prettyList :: [FieldAssignment' a] -> Doc Source #
Data a => Data (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FieldAssignment' a -> c (FieldAssignment' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FieldAssignment' a) # toConstr :: FieldAssignment' a -> Constr # dataTypeOf :: FieldAssignment' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FieldAssignment' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FieldAssignment' a)) # gmapT :: (forall b. Data b => b -> b) -> FieldAssignment' a -> FieldAssignment' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r # gmapQ :: (forall d. Data d => d -> u) -> FieldAssignment' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FieldAssignment' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) #
Show a => Show (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> FieldAssignment' a -> ShowS # show :: FieldAssignment' a -> String # showList :: [FieldAssignment' a] -> ShowS #
NFData a => NFData (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: FieldAssignment' a -> () #
Eq a => Eq (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: FieldAssignment' a -> FieldAssignment' a -> Bool # (/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool #
type ADotT (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (FieldAssignment' a) = ADotT a
type ConOfAbs (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (FieldAssignment' a) = FieldAssignment' (ConOfAbs a)
type AbsOfCon (FieldAssignment' c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (FieldAssignment' c) = FieldAssignment' (AbsOfCon c)

nameFieldA :: Lens' Name (FieldAssignment' a) Source #

exprFieldA :: Lens' a (FieldAssignment' a) Source #

data ModuleAssignment Source #

Constructors

ModuleAssignment
Fields _qnameModA :: QName _exprModA :: [Expr] _importDirModA :: ImportDirective

Instances

Instances details

ExprLike ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment Source #
HasRange ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range Source #
KillRange ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleAssignment Source #
ToAbstract ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon ModuleAssignment Source # Methods toAbstract :: ModuleAssignment -> ScopeM (AbsOfCon ModuleAssignment) Source #
Pretty ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleAssignment -> Doc Source # prettyPrec :: Int -> ModuleAssignment -> Doc Source # prettyList :: [ModuleAssignment] -> Doc Source #
Data ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleAssignment -> c ModuleAssignment # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleAssignment # toConstr :: ModuleAssignment -> Constr # dataTypeOf :: ModuleAssignment -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleAssignment) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleAssignment) # gmapT :: (forall b. Data b => b -> b) -> ModuleAssignment -> ModuleAssignment # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleAssignment -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleAssignment -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment #
Show ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleAssignment -> ShowS # show :: ModuleAssignment -> String # showList :: [ModuleAssignment] -> ShowS #
NFData ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleAssignment -> () #
Eq ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: ModuleAssignment -> ModuleAssignment -> Bool # (/=) :: ModuleAssignment -> ModuleAssignment -> Bool #
type AbsOfCon ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon ModuleAssignment = (ModuleName, Maybe LetBinding)

data BoundName Source #

Constructors

BName
Fields boundName :: Name bnameFixity :: Fixity' bnameTactic :: TacticAttribute

Instances

Instances details

HasRange Binder Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Binder -> Range Source #
HasRange BoundName Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: BoundName -> Range Source #
KillRange Binder Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Binder Source #
KillRange BoundName Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT BoundName Source #
Pretty BoundName Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: BoundName -> Doc Source # prettyPrec :: Int -> BoundName -> Doc Source # prettyList :: [BoundName] -> Doc Source #
Data BoundName Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoundName -> c BoundName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoundName # toConstr :: BoundName -> Constr # dataTypeOf :: BoundName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoundName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoundName) # gmapT :: (forall b. Data b => b -> b) -> BoundName -> BoundName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r # gmapQ :: (forall d. Data d => d -> u) -> BoundName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BoundName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName #
Show BoundName Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> BoundName -> ShowS # show :: BoundName -> String # showList :: [BoundName] -> ShowS #
NFData Binder Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Binder -> () #
NFData BoundName Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: BoundName -> () #
Eq BoundName Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: BoundName -> BoundName -> Bool # (/=) :: BoundName -> BoundName -> Bool #
ToAbstract (Binder' (NewName BoundName)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Binder' (NewName BoundName)) Source # Methods toAbstract :: Binder' (NewName BoundName) -> ScopeM (AbsOfCon (Binder' (NewName BoundName))) Source #
ToAbstract (NewName BoundName) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (NewName BoundName) Source # Methods toAbstract :: NewName BoundName -> ScopeM (AbsOfCon (NewName BoundName)) Source #
type AbsOfCon (Binder' (NewName BoundName)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Binder' (NewName BoundName)) = Binder
type AbsOfCon (NewName BoundName) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (NewName BoundName) = BindName

mkBoundName_ :: Name -> BoundName Source #

mkBoundName :: Name -> Fixity' -> BoundName Source #

type TacticAttribute = Maybe Expr Source #

type Telescope = [TypedBinding] Source #

type Telescope1 = List1 TypedBinding Source #

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.

lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope Source #

We can try to get a Telescope from a [LamBinding]. If we have a type annotation already, we're happy. Otherwise we manufacture a binder with an underscore for the type.

makePi :: Telescope -> Expr -> Expr Source #

Smart constructor for Pi: check whether the Telescope is empty

mkLam :: Range -> [LamBinding] -> Expr -> Expr Source #

Smart constructor for Lam: check for non-zero bindings.

mkLet :: Range -> [Declaration] -> Expr -> Expr Source #

Smart constructor for Let: check for non-zero let bindings.

mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e) Source #

Smart constructor for TLet: check for non-zero let bindings.

Declarations

data RecordDirective Source #

Isolated record directives parsed as Declarations

Constructors

Induction (Ranged Induction)	Range of keyword `[co]inductive`.
Constructor Name IsInstance
Eta (Ranged HasEta0)	Range of `[no-]eta-equality` keyword.
PatternOrCopattern Range	If declaration `pattern` is present, give its range.

Instances

Instances details

HasRange RecordDirective Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RecordDirective -> Range Source #
KillRange RecordDirective Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RecordDirective Source #
Data RecordDirective Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RecordDirective -> c RecordDirective # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RecordDirective # toConstr :: RecordDirective -> Constr # dataTypeOf :: RecordDirective -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RecordDirective) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RecordDirective) # gmapT :: (forall b. Data b => b -> b) -> RecordDirective -> RecordDirective # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirective -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirective -> r # gmapQ :: (forall d. Data d => d -> u) -> RecordDirective -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RecordDirective -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RecordDirective -> m RecordDirective # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirective -> m RecordDirective # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirective -> m RecordDirective #
Show RecordDirective Source #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> RecordDirective -> ShowS # show :: RecordDirective -> String # showList :: [RecordDirective] -> ShowS #
NFData RecordDirective Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: RecordDirective -> () #
Eq RecordDirective Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: RecordDirective -> RecordDirective -> Bool # (/=) :: RecordDirective -> RecordDirective -> Bool #

isRecordDirective :: Declaration -> Maybe RecordDirective Source #

Extract a record directive

type RecordDirectives = RecordDirectives' (Name, IsInstance) Source #

data Declaration Source #

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.

Constructors

TypeSig ArgInfo TacticAttribute Name Expr	Axioms and functions can be irrelevant. (Hiding should be NotHidden)
FieldSig IsInstance TacticAttribute Name (Arg Expr)
Generalize Range [TypeSignature]	Variables to be generalized, can be hidden and/or irrelevant.
Field Range [FieldSignature]
FunClause LHS RHS WhereClause Bool
DataSig Range Name [LamBinding] Expr	lone data signature in mutual block
Data Range Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
RecordSig Range Name [LamBinding] Expr	lone record signature in mutual block
RecordDef Range Name RecordDirectives [LamBinding] [Declaration]
Record Range Name RecordDirectives [LamBinding] Expr [Declaration]
RecordDirective RecordDirective	Should not survive beyond the parser
Infix Fixity (List1 Name)
Syntax Name Notation	notation declaration for a name
PatternSyn Range Name [Arg Name] Pattern
Mutual Range [Declaration]
InterleavedMutual Range [Declaration]
Abstract Range [Declaration]
Private Range Origin [Declaration]	In Agda.Syntax.Concrete.Definitions we generate private blocks temporarily, which should be treated different that user-declared private blocks. Thus the `Origin`.
InstanceB Range [Declaration]	The `Range'` here (exceptionally) only refers to the range of the `instance` keyword. The range of the whole block `InstanceB r ds` is `fuseRange r ds`.
LoneConstructor 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

Instances

Instances details

ExprLike Declaration Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration Source #
HasRange Declaration Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range Source #
HasRange WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source #
KillRange Declaration Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Declaration Source #
KillRange WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause Source #
Pretty Declaration Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source #
Pretty WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source #
Data Declaration Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration # toConstr :: Declaration -> Constr # dataTypeOf :: Declaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) # gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration #
Show Declaration Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS #
Show WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS # show :: WhereClause -> String # showList :: [WhereClause] -> ShowS #
NFData Declaration Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Declaration -> () #
Eq Declaration Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Declaration -> Declaration -> Bool # (/=) :: Declaration -> Declaration -> Bool #
ToAbstract (TopLevel [Declaration]) Source #	Top-level declarations are always `(import\|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file`
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (TopLevel [Declaration]) Source # Methods toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source #
type AbsOfCon (TopLevel [Declaration]) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (TopLevel [Declaration]) = TopLevelInfo

data ModuleApplication Source #

Constructors

SectionApp Range Telescope Expr	tel. M args
RecordModuleInstance Range QName	M {{...}}

Instances

Instances details

ExprLike ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication Source #
HasRange ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleApplication -> Range Source #
KillRange ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleApplication Source #
Pretty ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleApplication -> Doc Source # prettyPrec :: Int -> ModuleApplication -> Doc Source # prettyList :: [ModuleApplication] -> Doc Source #
Data ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleApplication -> c ModuleApplication # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication # toConstr :: ModuleApplication -> Constr # dataTypeOf :: ModuleApplication -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication) # gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication #
Show ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleApplication -> ShowS # show :: ModuleApplication -> String # showList :: [ModuleApplication] -> ShowS #
NFData ModuleApplication Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleApplication -> () #
Eq ModuleApplication Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: ModuleApplication -> ModuleApplication -> Bool # (/=) :: ModuleApplication -> ModuleApplication -> Bool #

type TypeSignature = Declaration Source #

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration Source #

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name Source #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

type Using = Using' Name Name Source #

type ImportedName = ImportedName' Name Name Source #

An imported name can be a module or a defined name.

type Renaming = Renaming' Name Name Source #

type RenamingDirective = RenamingDirective' Name Name Source #

type HidingDirective = HidingDirective' Name Name Source #

data AsName' a Source #

The content of the as-clause of the import statement.

Constructors

AsName
Fields asName :: a The "as" name. asRange :: Range The range of the "as" keyword. Retained for highlighting purposes.

Instances

Instances details

HasRange AsName Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range Source #
KillRange AsName Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName Source #
Foldable AsName' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => AsName' m -> m # foldMap :: Monoid m => (a -> m) -> AsName' a -> m # foldMap' :: Monoid m => (a -> m) -> AsName' a -> m # foldr :: (a -> b -> b) -> b -> AsName' a -> b # foldr' :: (a -> b -> b) -> b -> AsName' a -> b # foldl :: (b -> a -> b) -> b -> AsName' a -> b # foldl' :: (b -> a -> b) -> b -> AsName' a -> b # foldr1 :: (a -> a -> a) -> AsName' a -> a # foldl1 :: (a -> a -> a) -> AsName' a -> a # toList :: AsName' a -> [a] # null :: AsName' a -> Bool # length :: AsName' a -> Int # elem :: Eq a => a -> AsName' a -> Bool # maximum :: Ord a => AsName' a -> a # minimum :: Ord a => AsName' a -> a # sum :: Num a => AsName' a -> a # product :: Num a => AsName' a -> a #
Traversable AsName' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> AsName' a -> f (AsName' b) # sequenceA :: Applicative f => AsName' (f a) -> f (AsName' a) # mapM :: Monad m => (a -> m b) -> AsName' a -> m (AsName' b) # sequence :: Monad m => AsName' (m a) -> m (AsName' a) #
Functor AsName' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> AsName' a -> AsName' b # (<$) :: a -> AsName' b -> AsName' a #
NFData AsName Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () #
Data a => Data (AsName' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AsName' a -> c (AsName' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AsName' a) # toConstr :: AsName' a -> Constr # dataTypeOf :: AsName' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AsName' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AsName' a)) # gmapT :: (forall b. Data b => b -> b) -> AsName' a -> AsName' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AsName' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AsName' a -> r # gmapQ :: (forall d. Data d => d -> u) -> AsName' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AsName' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) #
Show a => Show (AsName' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> AsName' a -> ShowS # show :: AsName' a -> String # showList :: [AsName' a] -> ShowS #
Eq a => Eq (AsName' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: AsName' a -> AsName' a -> Bool # (/=) :: AsName' a -> AsName' a -> Bool #

type AsName = AsName' (Either Expr Name) Source #

From the parser, we get an expression for the as-Name, which we have to parse into a Name.

data OpenShortHand Source #

Constructors

DoOpen
DontOpen

Instances

Instances details

Pretty OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source #
Data OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpenShortHand -> c OpenShortHand # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpenShortHand # toConstr :: OpenShortHand -> Constr # dataTypeOf :: OpenShortHand -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpenShortHand) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpenShortHand) # gmapT :: (forall b. Data b => b -> b) -> OpenShortHand -> OpenShortHand # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r # gmapQ :: (forall d. Data d => d -> u) -> OpenShortHand -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> OpenShortHand -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand #
Generic OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete Associated Types type Rep OpenShortHand :: Type -> Type # Methods from :: OpenShortHand -> Rep OpenShortHand x # to :: Rep OpenShortHand x -> OpenShortHand #
Show OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> OpenShortHand -> ShowS # show :: OpenShortHand -> String # showList :: [OpenShortHand] -> ShowS #
NFData OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: OpenShortHand -> () #
Eq OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: OpenShortHand -> OpenShortHand -> Bool # (/=) :: OpenShortHand -> OpenShortHand -> Bool #
type Rep OpenShortHand Source #
Instance details Defined in Agda.Syntax.Concrete type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "DoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DontOpen" 'PrefixI 'False) (U1 :: Type -> Type))

type RewriteEqn = RewriteEqn' () Name Pattern Expr Source #

type WithExpr = Named Name (Arg Expr) Source #

data LHS Source #

Left hand sides can be written in infix style. For example:

n + suc m = suc (n + m)
(f ∘ g) x = f (g x)

We use fixity information to see which name is actually defined.

Constructors

LHS	Original pattern (including with-patterns), rewrite equations and with-expressions.
Fields lhsOriginalPattern :: Pattern e.g. `f ps \| wps` lhsRewriteEqn :: [RewriteEqn] `(rewrite e \| with p <- e in eq)` (many) lhsWithExpr :: [WithExpr] `with e1 in eq \| {e2} \| ...` (many)

Instances

Instances details

ExprLike LHS Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LHS -> LHS Source # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS Source #
HasEllipsis LHS Source #	Does the lhs contain an ellipsis?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool Source #
HasRange LHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHS -> Range Source #
KillRange LHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LHS Source #
Pretty LHS Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LHS -> Doc Source # prettyPrec :: Int -> LHS -> Doc Source # prettyList :: [LHS] -> Doc Source #
Data LHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS # toConstr :: LHS -> Constr # dataTypeOf :: LHS -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) # gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS #
Show LHS Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LHS -> ShowS # show :: LHS -> String # showList :: [LHS] -> ShowS #
NFData LHS Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LHS -> () #
Eq LHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LHS -> LHS -> Bool # (/=) :: LHS -> LHS -> Bool #

data Pattern Source #

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName	`c` or `x`
QuoteP Range	quote
AppP Pattern (NamedArg Pattern)	`p p'` or `p {x = p'}`
RawAppP Range (List2 Pattern)	`p1..pn` before parsing operators
OpAppP Range QName (Set Name) [NamedArg Pattern]	eg: `p => p'` for operator `_=>_` The `QName` is possibly ambiguous, but it must correspond to one of the names in the set.
HiddenP Range (Named_ Pattern)	`{p}` or `{x = p}`
InstanceP Range (Named_ Pattern)	`{{p}}` or `{{x = p}}`
ParenP Range Pattern	(p)
WildP Range	_
AbsurdP Range	()
AsP Range Name Pattern	`x@p` unused
DotP Range Expr	.e
LitP Range Literal	`0`, `1`, etc.
RecP Range [FieldAssignment' Pattern]	record {x = p; y = q}
EqualP Range [(Expr, Expr)]	`i = i1` i.e. cubical face lattice generator
EllipsisP Range (Maybe Pattern)	`...`, only as left-most pattern. Second arg is `Nothing` before expansion, and `Just p` after expanding ellipsis to `p`.
WithP Range Pattern	`\| p`, for with-patterns.

Instances

Instances details

IsExpr Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Pattern -> ExprView Pattern Source # unExprView :: ExprView Pattern -> Pattern Source # patternView :: Pattern -> Maybe Pattern Source #
CPatternLike Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern Source #
HasEllipsis Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool Source #
IsEllipsis Pattern Source #	Is the pattern just `...`?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool Source #
IsWithP Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Pattern -> Maybe Pattern Source #
HasRange Pattern Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pattern -> Range Source #
KillRange Pattern Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pattern Source #
SetRange Pattern Source #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> Pattern -> Pattern Source #
ToAbstract HoleContent Source #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon HoleContent Source # Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #
ToAbstract Pattern Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Pattern Source # Methods toAbstract :: Pattern -> ScopeM (AbsOfCon Pattern) Source #
ToAbstract RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RewriteEqn Source # Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #
Pretty Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pattern -> Doc Source # prettyPrec :: Int -> Pattern -> Doc Source # prettyList :: [Pattern] -> Doc Source #
Data Pattern Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern -> c Pattern # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pattern # toConstr :: Pattern -> Constr # dataTypeOf :: Pattern -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pattern) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pattern) # gmapT :: (forall b. Data b => b -> b) -> Pattern -> Pattern # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r # gmapQ :: (forall d. Data d => d -> u) -> Pattern -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern #
Show Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #
NFData Pattern Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pattern -> () #
Eq Pattern Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Pattern -> Pattern -> Bool # (/=) :: Pattern -> Pattern -> Bool #
type AbsOfCon HoleContent Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent
type AbsOfCon Pattern Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Pattern = Pattern' Expr
type AbsOfCon RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

data LHSCore Source #

Processed (operator-parsed) intermediate form of the core f ps of LHS. Corresponds to lhsOriginalPattern.

Constructors

LHSHead
Fields lhsDefName :: QName f lhsPats :: [NamedArg Pattern] ps
LHSProj
Fields lhsDestructor :: QName Record projection. lhsPatsLeft :: [NamedArg Pattern] Patterns for record indices (currently none). lhsFocus :: NamedArg LHSCore Main argument. lhsPats :: [NamedArg Pattern] ps
LHSWith
Fields lhsHead :: LHSCore lhsWithPatterns :: [Pattern] Non-empty; at least one `(\| p)`. lhsPats :: [NamedArg Pattern] ps
LHSEllipsis
Fields lhsEllipsisRange :: Range lhsEllipsisPat :: LHSCore Pattern that was expanded from an ellipsis `...`.

Instances

Instances details

HasRange LHSCore Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHSCore -> Range Source #
ToAbstract LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LHSCore Source # Methods toAbstract :: LHSCore -> ScopeM (AbsOfCon LHSCore) Source #
Pretty LHSCore Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LHSCore -> Doc Source # prettyPrec :: Int -> LHSCore -> Doc Source # prettyList :: [LHSCore] -> Doc Source #
Data LHSCore Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore -> c LHSCore # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSCore # toConstr :: LHSCore -> Constr # dataTypeOf :: LHSCore -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHSCore) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHSCore) # gmapT :: (forall b. Data b => b -> b) -> LHSCore -> LHSCore # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore -> r # gmapQ :: (forall d. Data d => d -> u) -> LHSCore -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore -> m LHSCore # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore -> m LHSCore # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore -> m LHSCore #
Show LHSCore Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LHSCore -> ShowS # show :: LHSCore -> String # showList :: [LHSCore] -> ShowS #
Eq LHSCore Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LHSCore -> LHSCore -> Bool # (/=) :: LHSCore -> LHSCore -> Bool #
type AbsOfCon LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LHSCore = LHSCore' Expr

observeHiding :: Expr -> WithHiding Expr Source #

Observe the hiding status of an expression

observeRelevance :: Expr -> (Relevance, Expr) Source #

Observe the relevance status of an expression

observeModifiers :: Expr -> Arg Expr Source #

Observe various modifiers applied to an expression

data LamClause Source #

Constructors

LamClause
Fields lamLHS :: [Pattern] Possibly empty sequence. lamRHS :: RHS lamCatchAll :: Bool

Instances

Instances details

ExprLike LamClause Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamClause -> LamClause Source # foldExpr :: Monoid m => (Expr -> m) -> LamClause -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamClause -> m LamClause Source #
HasRange LamClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamClause -> Range Source #
KillRange LamClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamClause Source #
Pretty LamClause Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamClause -> Doc Source # prettyPrec :: Int -> LamClause -> Doc Source # prettyList :: [LamClause] -> Doc Source #
Data LamClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamClause -> c LamClause # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamClause # toConstr :: LamClause -> Constr # dataTypeOf :: LamClause -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamClause) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamClause) # gmapT :: (forall b. Data b => b -> b) -> LamClause -> LamClause # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r # gmapQ :: (forall d. Data d => d -> u) -> LamClause -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LamClause -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause #
Show LamClause Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamClause -> ShowS # show :: LamClause -> String # showList :: [LamClause] -> ShowS #
NFData LamClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamClause -> () #
Eq LamClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LamClause -> LamClause -> Bool # (/=) :: LamClause -> LamClause -> Bool #

type RHS = RHS' Expr Source #

data RHS' e Source #

Constructors

AbsurdRHS	No right hand side because of absurd match.
RHS e

Instances

Instances details

HasRange RHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range Source #
KillRange RHS Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS Source #
ToAbstract RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RHS Source # Methods toAbstract :: RHS -> ScopeM (AbsOfCon RHS) Source #
Pretty RHS Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RHS -> Doc Source # prettyPrec :: Int -> RHS -> Doc Source # prettyList :: [RHS] -> Doc Source #
Foldable RHS' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => RHS' m -> m # foldMap :: Monoid m => (a -> m) -> RHS' a -> m # foldMap' :: Monoid m => (a -> m) -> RHS' a -> m # foldr :: (a -> b -> b) -> b -> RHS' a -> b # foldr' :: (a -> b -> b) -> b -> RHS' a -> b # foldl :: (b -> a -> b) -> b -> RHS' a -> b # foldl' :: (b -> a -> b) -> b -> RHS' a -> b # foldr1 :: (a -> a -> a) -> RHS' a -> a # foldl1 :: (a -> a -> a) -> RHS' a -> a # toList :: RHS' a -> [a] # null :: RHS' a -> Bool # length :: RHS' a -> Int # elem :: Eq a => a -> RHS' a -> Bool # maximum :: Ord a => RHS' a -> a # minimum :: Ord a => RHS' a -> a # sum :: Num a => RHS' a -> a # product :: Num a => RHS' a -> a #
Traversable RHS' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> RHS' a -> f (RHS' b) # sequenceA :: Applicative f => RHS' (f a) -> f (RHS' a) # mapM :: Monad m => (a -> m b) -> RHS' a -> m (RHS' b) # sequence :: Monad m => RHS' (m a) -> m (RHS' a) #
Functor RHS' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> RHS' a -> RHS' b # (<$) :: a -> RHS' b -> RHS' a #
Show RHS Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
ExprLike a => ExprLike (RHS' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a Source # foldExpr :: Monoid m => (Expr -> m) -> RHS' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RHS' a -> m (RHS' a) Source #
Data e => Data (RHS' e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS' e -> c (RHS' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e) # toConstr :: RHS' e -> Constr # dataTypeOf :: RHS' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e)) # gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r # gmapQ :: (forall d. Data d => d -> u) -> RHS' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) #
NFData a => NFData (RHS' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: RHS' a -> () #
Eq e => Eq (RHS' e) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: RHS' e -> RHS' e -> Bool # (/=) :: RHS' e -> RHS' e -> Bool #
type AbsOfCon RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RHS = AbstractRHS

type WhereClause = WhereClause' [Declaration] Source #

where block following a clause.

data WhereClause' decls Source #

Constructors

NoWhere	No `where` clauses.
AnyWhere Range decls	Ordinary `where`. `Range'` of the `where` keyword. List of declarations can be empty.
SomeWhere Range Name Access decls	Named where: `module M where ds`. `Range'` of the keywords `module` and `where`. The `Access` flag applies to the `Name` (not the module contents!) and is propagated from the parent function. List of declarations can be empty.

Instances

Instances details

HasRange WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source #
KillRange WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause Source #
Pretty WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source #
Foldable WhereClause' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => WhereClause' m -> m # foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m # foldMap' :: Monoid m => (a -> m) -> WhereClause' a -> m # foldr :: (a -> b -> b) -> b -> WhereClause' a -> b # foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b # foldl :: (b -> a -> b) -> b -> WhereClause' a -> b # foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b # foldr1 :: (a -> a -> a) -> WhereClause' a -> a # foldl1 :: (a -> a -> a) -> WhereClause' a -> a # toList :: WhereClause' a -> [a] # null :: WhereClause' a -> Bool # length :: WhereClause' a -> Int # elem :: Eq a => a -> WhereClause' a -> Bool # maximum :: Ord a => WhereClause' a -> a # minimum :: Ord a => WhereClause' a -> a # sum :: Num a => WhereClause' a -> a # product :: Num a => WhereClause' a -> a #
Traversable WhereClause' Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) # sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) # mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) # sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) #
Functor WhereClause' Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b # (<$) :: a -> WhereClause' b -> WhereClause' a #
Show WhereClause Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS # show :: WhereClause -> String # showList :: [WhereClause] -> ShowS #
ExprLike a => ExprLike (WhereClause' a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a Source # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) Source #
Null (WhereClause' a) Source #	A `WhereClause` is `null` when the `where` keyword is absent. An empty list of declarations does not count as `null` here.
Instance details Defined in Agda.Syntax.Concrete Methods empty :: WhereClause' a Source # null :: WhereClause' a -> Bool Source #
Data decls => Data (WhereClause' decls) Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereClause' decls -> c (WhereClause' decls) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WhereClause' decls) # toConstr :: WhereClause' decls -> Constr # dataTypeOf :: WhereClause' decls -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WhereClause' decls)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WhereClause' decls)) # gmapT :: (forall b. Data b => b -> b) -> WhereClause' decls -> WhereClause' decls # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r # gmapQ :: (forall d. Data d => d -> u) -> WhereClause' decls -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereClause' decls -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) #
NFData a => NFData (WhereClause' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause' a -> () #
Eq decls => Eq (WhereClause' decls) Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: WhereClause' decls -> WhereClause' decls -> Bool # (/=) :: WhereClause' decls -> WhereClause' decls -> Bool #

data ExprWhere Source #

An expression followed by a where clause. Currently only used to give better a better error message in interaction.

Constructors

ExprWhere Expr WhereClause

data DoStmt Source #

Constructors

DoBind Range Pattern Expr [LamClause]	p ← e where cs
DoThen Expr
DoLet Range (List1 Declaration)

Instances

Instances details

ExprLike DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt Source # foldExpr :: Monoid m => (Expr -> m) -> DoStmt -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> DoStmt -> m DoStmt Source #
HasRange DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: DoStmt -> Range Source #
KillRange DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT DoStmt Source #
Pretty DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: DoStmt -> Doc Source # prettyPrec :: Int -> DoStmt -> Doc Source # prettyList :: [DoStmt] -> Doc Source #
Data DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoStmt -> c DoStmt # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoStmt # toConstr :: DoStmt -> Constr # dataTypeOf :: DoStmt -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoStmt) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoStmt) # gmapT :: (forall b. Data b => b -> b) -> DoStmt -> DoStmt # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r # gmapQ :: (forall d. Data d => d -> u) -> DoStmt -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DoStmt -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt #
Show DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> DoStmt -> ShowS # show :: DoStmt -> String # showList :: [DoStmt] -> ShowS #
NFData DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: DoStmt -> () #
Eq DoStmt Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: DoStmt -> DoStmt -> Bool # (/=) :: DoStmt -> DoStmt -> Bool #

data Pragma Source #

Constructors

OptionsPragma Range [String]
BuiltinPragma Range RString QName
RewritePragma Range Range [QName]	Second Range is for REWRITE keyword.
ForeignPragma Range RString String	first string is backend name
CompilePragma Range RString QName String	first string is backend name
StaticPragma Range QName
InlinePragma Range Bool QName	INLINE or NOINLINE
ImpossiblePragma Range [String]	Throws an internal error in the scope checker. The `String`s are words to be displayed with the error.
EtaPragma Range QName	For coinductive records, use pragma instead of regular `eta-equality` definition (as it is might make Agda loop).
WarningOnUsage Range QName Text	Applies to the named function
WarningOnImport Range Text	Applies to the current module
InjectivePragma Range QName	Mark a definition as injective for the pattern matching unifier.
DisplayPragma Range Pattern Expr	Display lhs as rhs (modifies the printer).
CatchallPragma Range	Applies to the following function clause.
TerminationCheckPragma Range (TerminationCheck Name)	Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.
NoCoverageCheckPragma Range	Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.
NoPositivityCheckPragma Range	Applies to the following data/record type or mutual block.
PolarityPragma Range Name [Occurrence]
NoUniverseCheckPragma Range	Applies to the following data/record type.

Instances

Instances details

HasRange Pragma Source #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pragma -> Range Source #
KillRange Pragma Source #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pragma Source #
ToAbstract Pragma Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Pragma Source # Methods toAbstract :: Pragma -> ScopeM (AbsOfCon Pragma) Source #
Pretty Pragma Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pragma -> Doc Source # prettyPrec :: Int -> Pragma -> Doc Source # prettyList :: [Pragma] -> Doc Source #
Data Pragma Source #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma # toConstr :: Pragma -> Constr # dataTypeOf :: Pragma -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) # gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma #
Show Pragma Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
NFData Pragma Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pragma -> () #
Eq Pragma Source #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Pragma -> Pragma -> Bool # (/=) :: Pragma -> Pragma -> Bool #
type AbsOfCon Pragma Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Pragma = [Pragma]

data Module Source #

Modules: Top-level pragmas plus other top-level declarations.

Constructors

Mod
Fields modPragmas :: [Pragma] modDecls :: [Declaration]

Instances

Instances details

Show Module Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Module -> ShowS # show :: Module -> String # showList :: [Module] -> ShowS #

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Instances details

Foldable ThingWithFixity Source #
Instance details Defined in Agda.Syntax.Fixity Methods fold :: Monoid m => ThingWithFixity m -> m # foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m # foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m # foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a # foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a # toList :: ThingWithFixity a -> [a] # null :: ThingWithFixity a -> Bool # length :: ThingWithFixity a -> Int # elem :: Eq a => a -> ThingWithFixity a -> Bool # maximum :: Ord a => ThingWithFixity a -> a # minimum :: Ord a => ThingWithFixity a -> a # sum :: Num a => ThingWithFixity a -> a # product :: Num a => ThingWithFixity a -> a #
Traversable ThingWithFixity Source #
Instance details Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) #
Functor ThingWithFixity Source #
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a #
LensFixity (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' Fixity (ThingWithFixity a) Source #
LensFixity' (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' Fixity' (ThingWithFixity a) Source #
KillRange x => KillRange (ThingWithFixity x) Source #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source #
Pretty (ThingWithFixity Name) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
Data x => Data (ThingWithFixity x) Source #
Instance details Defined in Agda.Syntax.Fixity Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) # toConstr :: ThingWithFixity x -> Constr # dataTypeOf :: ThingWithFixity x -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) # gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r # gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) #
Show x => Show (ThingWithFixity x) Source #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS # show :: ThingWithFixity x -> String # showList :: [ThingWithFixity x] -> ShowS #

type HoleContent = HoleContent' () Name Pattern Expr Source #

data HoleContent' qn nm p e Source #

Extended content of an interaction hole.

Constructors

HoleContentExpr e	e
HoleContentRewrite [RewriteEqn' qn nm p e]	(rewrite \| invert) e0 \| ... \| en

Instances

Instances details

ToAbstract HoleContent Source #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon HoleContent Source # Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #
Foldable (HoleContent' qn nm p) Source #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => HoleContent' qn nm p m -> m # foldMap :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m # foldMap' :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m # foldr :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b # foldr' :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b # foldl :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b # foldl' :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b # foldr1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a # foldl1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a # toList :: HoleContent' qn nm p a -> [a] # null :: HoleContent' qn nm p a -> Bool # length :: HoleContent' qn nm p a -> Int # elem :: Eq a => a -> HoleContent' qn nm p a -> Bool # maximum :: Ord a => HoleContent' qn nm p a -> a # minimum :: Ord a => HoleContent' qn nm p a -> a # sum :: Num a => HoleContent' qn nm p a -> a # product :: Num a => HoleContent' qn nm p a -> a #
Traversable (HoleContent' qn nm p) Source #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b) # sequenceA :: Applicative f => HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a) # mapM :: Monad m => (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b) # sequence :: Monad m => HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a) #
Functor (HoleContent' qn nm p) Source #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b # (<$) :: a -> HoleContent' qn nm p b -> HoleContent' qn nm p a #
type AbsOfCon HoleContent Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

topLevelModuleName :: Module -> TopLevelModuleName Source #

Computes the top-level module name.

Precondition: The Declaration has to be well-formed. This means that there are only allowed declarations before the first module declaration, typically import declarations. See spanAllowedBeforeModule.

spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration]) Source #

Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.