Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 (Set1 Name) OpAppArgs
  - | WithApp Range Expr (List1 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 KwRange Range RecordAssignments
  - | RecUpdate KwRange 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 KwRange Expr
  - | DoubleDot KwRange Expr
  - | Quote Range
  - | QuoteTerm Range
  - | Tactic Range Expr
  - | Unquote Range
  - | DontCare Expr
  - | Equal Range Expr Expr
  - | Ellipsis Range
  - | KnownIdent NameKind QName
  - | KnownOpApp NameKind Range QName (Set1 Name) OpAppArgs
  - | Generalized Expr
- data OpApp e
  - = SyntaxBindingLambda Range (List1 LamBinding) e
  - | Ordinary e
- fromOrdinary :: e -> OpApp e -> e
- type OpAppArgs = OpAppArgs' Expr
- type OpAppArgs' e = List1 (NamedArg (MaybePlaceholder (OpApp e)))
- type OpAppArgs0 e = [NamedArg (MaybePlaceholder (OpApp e))]
- module Agda.Syntax.Concrete.Name
- data AppView = AppView Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- toNamedArg :: Expr -> NamedArg Expr
- unNamedArg :: NamedArg Expr -> 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
- observeHiding :: Expr -> WithHiding Expr
- observeRelevance :: Expr -> (Relevance, Expr)
- observeModifiers :: Expr -> Arg Expr
- exprToPatternWithHoles :: Expr -> Pattern
- returnExpr :: Expr -> Maybe Expr
- data Binder' a = Binder {
  - binderPattern :: Maybe Pattern
  - binderNameOrigin :: BinderNameOrigin
  - 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 :: forall a f. Functor f => (Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a)
- exprFieldA :: forall a f. Functor f => (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a)
- data ModuleAssignment = ModuleAssignment {
  - _qnameModA :: QName
  - _exprModA :: [Expr]
  - _importDirModA :: ImportDirective
  }
- data BoundName = BName {
  - boundName :: Name
  - bnameFixity :: Fixity'
  - bnameTactic :: TacticAttribute
  - bnameIsFinite :: Bool
  }
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type TacticAttribute = TacticAttribute' Expr
- newtype TacticAttribute' a = TacticAttribute {
  - theTacticAttribute :: Maybe (Ranged a)
  }
- 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 Declaration
  - = TypeSig ArgInfo TacticAttribute Name Expr
  - | FieldSig IsInstance TacticAttribute Name (Arg Expr)
  - | Generalize KwRange [TypeSignature]
  - | Field KwRange [FieldSignature]
  - | FunClause LHS RHS WhereClause Catchall
  - | DataSig Range Erased Name [LamBinding] Expr
  - | Data Range Erased Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
  - | DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
  - | RecordSig Range Erased Name [LamBinding] Expr
  - | RecordDef Range Name [RecordDirective] [LamBinding] [Declaration]
  - | Record Range Erased Name [RecordDirective] [LamBinding] Expr [Declaration]
  - | Infix Fixity (List1 Name)
  - | Syntax Name Notation
  - | PatternSyn Range Name [WithHiding Name] Pattern
  - | Mutual KwRange [Declaration]
  - | InterleavedMutual KwRange [Declaration]
  - | Abstract KwRange [Declaration]
  - | Private KwRange Origin [Declaration]
  - | InstanceB KwRange [Declaration]
  - | LoneConstructor KwRange [Declaration]
  - | Macro KwRange [Declaration]
  - | Postulate KwRange [TypeSignatureOrInstanceBlock]
  - | Primitive KwRange [TypeSignature]
  - | Open Range QName ImportDirective
  - | Import Range QName (Maybe AsName) !OpenShortHand ImportDirective
  - | ModuleMacro Range Erased Name ModuleApplication !OpenShortHand ImportDirective
  - | Module Range Erased QName Telescope [Declaration]
  - | UnquoteDecl Range [Name] Expr
  - | UnquoteDef Range [Name] Expr
  - | UnquoteData Range Name [Name] Expr
  - | Pragma Pragma
  - | Opaque KwRange [Declaration]
  - | Unfolding KwRange [QName]
- isPragma :: CMaybe Pragma m => Declaration -> m
- data RecordDirective
  - = Induction (Ranged Induction)
  - | Constructor Name IsInstance
  - | Eta (Ranged HasEta0)
  - | PatternOrCopattern Range
- type RecordDirectives = RecordDirectives' (Maybe (Name, IsInstance))
- data ModuleApplication
  - = SectionApp Range Telescope QName [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 Bool QName
  - | QuoteP Range
  - | AppP Pattern (NamedArg Pattern)
  - | RawAppP Range (List2 Pattern)
  - | OpAppP Range QName (Set1 Name) (List1 (NamedArg Pattern))
  - | HiddenP Range (Named_ Pattern)
  - | InstanceP Range (Named_ Pattern)
  - | ParenP Range Pattern
  - | WildP Range
  - | AbsurdP Range
  - | AsP Range Name Pattern
  - | DotP KwRange Range Expr
  - | LitP Range Literal
  - | RecP KwRange Range [FieldAssignment' Pattern]
  - | EqualP Range (List1 (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 :: List1 Pattern
    - lhsPats :: [NamedArg Pattern]
    }
  - | LHSEllipsis {
    - lhsEllipsisRange :: Range
    - lhsEllipsisPat :: LHSCore
    }
- data LamClause = LamClause {
  - lamLHS :: [Pattern]
  - lamRHS :: RHS
  - lamCatchall :: Catchall
  }
- type RHS = RHS' Expr
- data RHS' e
  - = AbsurdRHS
  - | RHS e
- type WhereClause = WhereClause' [Declaration]
- data WhereClause' decls
  - = NoWhere
  - | AnyWhere Range decls
  - | SomeWhere Range Erased Name Access decls
- data WhereClause_
  - = NoWhere_
  - | AnyWhere_
  - | SomeWhere_
- data ExprWhere = ExprWhere Expr WhereClause
- whereClause_ :: WhereClause' a -> 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 (Ranged BackendName) String
  - | CompilePragma Range (Ranged BackendName) 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
  - | InjectiveForInferencePragma Range QName
  - | DisplayPragma Range Pattern Expr
  - | CatchallPragma Range
  - | TerminationCheckPragma Range (TerminationCheck Name)
  - | NoCoverageCheckPragma Range
  - | NoPositivityCheckPragma Range
  - | PolarityPragma Range Name [Ranged Occurrence]
  - | NoUniverseCheckPragma Range
  - | NotProjectionLikePragma Range QName
  - | OverlapPragma Range [QName] OverlapMode
- 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]
- spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
- ungatherRecordDirectives :: RecordDirectives -> [RecordDirective]

# 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 (Set1 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 (List1 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 KwRange Range RecordAssignments | ex: `record {x = a; y = b}`, or `record { x = a; M1; M2 }` The `KwRange` is for the `record` keyword.
RecUpdate KwRange Range Expr [FieldAssignment] | ex: `record e {x = a; y = b}` The `KwRange` is for the `record` keyword.
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 KwRange Expr | ex: `.p`, only in patterns
DoubleDot KwRange Expr | ex: `..A`, used for parsing `..A -> B`
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.
KnownIdent NameKind QName | An identifier coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).
KnownOpApp NameKind Range QName (Set1 Name) OpAppArgs | An operator application coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).
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 #
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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Expr = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #

ToAbstract LamBinding Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding

Methods

toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #

ToAbstract RHS Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RHS

Methods

toAbstract :: RHS -> ScopeM (AbsOfCon RHS) Source #

ToAbstract RewriteEqn Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

Methods

toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #

ToAbstract TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon TypedBinding = Maybe TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source #

NFData AsName Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () Source #
NFData Expr Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Expr -> () Source #
Show Expr Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
Show LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
Show RHS Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS -> ShowS Source # show :: RHS -> String Source # showList :: [RHS] -> ShowS Source #
Show TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS Source # show :: TypedBinding -> String Source # showList :: [TypedBinding] -> ShowS Source #
Eq Expr Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Expr -> Expr -> Bool Source # (/=) :: Expr -> Expr -> Bool 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 #
ToAbstract (LHSCore' Expr) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

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) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr

Methods

toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) 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
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

Functor OpApp Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> OpApp a -> OpApp b Source # (<$) :: a -> OpApp b -> OpApp a Source #
Foldable OpApp Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => OpApp m -> m Source #

foldMap :: Monoid m => (a -> m) -> OpApp a -> m Source #

foldMap' :: Monoid m => (a -> m) -> OpApp a -> m Source #

foldr :: (a -> b -> b) -> b -> OpApp a -> b Source #

foldr' :: (a -> b -> b) -> b -> OpApp a -> b Source #

foldl :: (b -> a -> b) -> b -> OpApp a -> b Source #

foldl' :: (b -> a -> b) -> b -> OpApp a -> b Source #

foldr1 :: (a -> a -> a) -> OpApp a -> a Source #

foldl1 :: (a -> a -> a) -> OpApp a -> a Source #

toList :: OpApp a -> [a] Source #

null :: OpApp a -> Bool Source #

length :: OpApp a -> Int Source #

elem :: Eq a => a -> OpApp a -> Bool Source #

maximum :: Ord a => OpApp a -> a Source #

minimum :: Ord a => OpApp a -> a Source #

sum :: Num a => OpApp a -> a Source #

product :: Num a => OpApp a -> a Source #

Traversable OpApp Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> OpApp a -> f (OpApp b) Source # sequenceA :: Applicative f => OpApp (f a) -> f (OpApp a) Source # mapM :: Monad m => (a -> m b) -> OpApp a -> m (OpApp b) Source # sequence :: Monad m => OpApp (m a) -> m (OpApp a) 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 #
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 #
NFData a => NFData (OpApp a) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: OpApp a -> () Source #
Show a => Show (OpApp a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> OpApp a -> ShowS Source # show :: OpApp a -> String Source # showList :: [OpApp a] -> ShowS Source #
Eq e => Eq (OpApp e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: OpApp e -> OpApp e -> Bool Source # (/=) :: OpApp e -> OpApp e -> Bool Source #

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

type OpAppArgs = OpAppArgs' Expr Source #

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

type OpAppArgs0 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 #

toNamedArg :: Expr -> NamedArg Expr Source #

Parse outermost hiding information.

unNamedArg :: NamedArg Expr -> Expr Source #

Unparse hiding information.

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 #

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

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
- binderNameOrigin :: BinderNameOrigin
- 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 #
NFData Binder Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Binder -> () Source #
Functor Binder' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> Binder' a -> Binder' b Source # (<$) :: a -> Binder' b -> Binder' a Source #
Foldable Binder' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => Binder' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Binder' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Binder' a -> m Source #

foldr :: (a -> b -> b) -> b -> Binder' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Binder' a -> b Source #

foldl :: (b -> a -> b) -> b -> Binder' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Binder' a -> b Source #

foldr1 :: (a -> a -> a) -> Binder' a -> a Source #

foldl1 :: (a -> a -> a) -> Binder' a -> a Source #

toList :: Binder' a -> [a] Source #

null :: Binder' a -> Bool Source #

length :: Binder' a -> Int Source #

elem :: Eq a => a -> Binder' a -> Bool Source #

maximum :: Ord a => Binder' a -> a Source #

minimum :: Ord a => Binder' a -> a Source #

sum :: Num a => Binder' a -> a Source #

product :: Num a => Binder' a -> a Source #

Traversable Binder' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) Source # sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) Source # mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) Source # sequence :: Monad m => Binder' (m a) -> m (Binder' a) 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 #
Show a => Show (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Binder' a -> ShowS Source # show :: Binder' a -> String Source # showList :: [Binder' a] -> ShowS Source #
Eq a => Eq (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Binder' a -> Binder' a -> Bool Source # (/=) :: Binder' a -> Binder' a -> Bool Source #

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 #
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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding

Methods

toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #

Functor LamBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b Source # (<$) :: a -> LamBinding' b -> LamBinding' a Source #
Foldable LamBinding' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => LamBinding' m -> m Source #

foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> LamBinding' a -> m Source #

foldr :: (a -> b -> b) -> b -> LamBinding' a -> b Source #

foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b Source #

foldl :: (b -> a -> b) -> b -> LamBinding' a -> b Source #

foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b Source #

foldr1 :: (a -> a -> a) -> LamBinding' a -> a Source #

foldl1 :: (a -> a -> a) -> LamBinding' a -> a Source #

toList :: LamBinding' a -> [a] Source #

null :: LamBinding' a -> Bool Source #

length :: LamBinding' a -> Int Source #

elem :: Eq a => a -> LamBinding' a -> Bool Source #

maximum :: Ord a => LamBinding' a -> a Source #

minimum :: Ord a => LamBinding' a -> a Source #

sum :: Num a => LamBinding' a -> a Source #

product :: Num a => LamBinding' a -> a Source #

Traversable LamBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) Source # sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) Source # mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) Source # sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) Source #
Show LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
NFData a => NFData (LamBinding' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamBinding' a -> () Source #
Eq a => Eq (LamBinding' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LamBinding' a -> LamBinding' a -> Bool Source # (/=) :: LamBinding' a -> LamBinding' a -> Bool Source #
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 #
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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding

Methods

toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #

ToAbstract TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon TypedBinding = Maybe TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source #

Functor TypedBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b Source # (<$) :: a -> TypedBinding' b -> TypedBinding' a Source #
Foldable TypedBinding' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => TypedBinding' m -> m Source #

foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> TypedBinding' a -> m Source #

foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b Source #

foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b Source #

foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b Source #

foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b Source #

foldr1 :: (a -> a -> a) -> TypedBinding' a -> a Source #

foldl1 :: (a -> a -> a) -> TypedBinding' a -> a Source #

toList :: TypedBinding' a -> [a] Source #

null :: TypedBinding' a -> Bool Source #

length :: TypedBinding' a -> Int Source #

elem :: Eq a => a -> TypedBinding' a -> Bool Source #

maximum :: Ord a => TypedBinding' a -> a Source #

minimum :: Ord a => TypedBinding' a -> a Source #

sum :: Num a => TypedBinding' a -> a Source #

product :: Num a => TypedBinding' a -> a Source #

Traversable TypedBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b) Source # sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a) Source # mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b) Source # sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a) Source #
Show LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
Show TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS Source # show :: TypedBinding -> String Source # showList :: [TypedBinding] -> ShowS Source #
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 #
NFData a => NFData (TypedBinding' a) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: TypedBinding' a -> () Source #
Eq e => Eq (TypedBinding' e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: TypedBinding' e -> TypedBinding' e -> Bool Source # (/=) :: TypedBinding' e -> TypedBinding' e -> Bool Source #
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 #
Functor FieldAssignment' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b Source # (<$) :: a -> FieldAssignment' b -> FieldAssignment' a Source #
Foldable FieldAssignment' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => FieldAssignment' m -> m Source #

foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> FieldAssignment' a -> m Source #

foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b Source #

foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b Source #

foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b Source #

foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b Source #

foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a Source #

foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a Source #

toList :: FieldAssignment' a -> [a] Source #

null :: FieldAssignment' a -> Bool Source #

length :: FieldAssignment' a -> Int Source #

elem :: Eq a => a -> FieldAssignment' a -> Bool Source #

maximum :: Ord a => FieldAssignment' a -> a Source #

minimum :: Ord a => FieldAssignment' a -> a Source #

sum :: Num a => FieldAssignment' a -> a Source #

product :: Num a => FieldAssignment' a -> a Source #

Traversable FieldAssignment' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b) Source #

sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a) Source #

mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b) Source #

sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a) Source #

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) |
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (FieldAssignment' a) = ADotT a

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 #
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 #
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 namesAndMetasIn' :: Monoid m => (Either QName MetaId -> 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) |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (FieldAssignment' a) = FieldAssignment' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => FieldAssignment' a -> m (ConOfAbs (FieldAssignment' a)) Source #

bindToConcrete :: MonadToConcrete m => FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> m b) -> m b Source #

ToAbstract c => ToAbstract (FieldAssignment' c) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (FieldAssignment' c) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (FieldAssignment' c) = FieldAssignment' (AbsOfCon c)

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 Word32 Source # icod_ :: FieldAssignment' a -> S Word32 Source # value :: Word32 -> R (FieldAssignment' a) Source #
NFData a => NFData (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: FieldAssignment' a -> () Source #
Show a => Show (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> FieldAssignment' a -> ShowS Source # show :: FieldAssignment' a -> String Source # showList :: [FieldAssignment' a] -> ShowS Source #
Eq a => Eq (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: FieldAssignment' a -> FieldAssignment' a -> Bool Source # (/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool Source #
PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods patToExpr :: FieldAssignment' p -> Reader Hiding (FieldAssignment' e) Source #
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 :: forall a f. Functor f => (Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a) Source #

exprFieldA :: forall a f. Functor f => (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a) Source #

data ModuleAssignment Source #

Constructors

ModuleAssignment |

Fields

- _qnameModA :: QName
- _exprModA :: [Expr]
- _importDirModA :: ImportDirective

#### Instances

Instances details

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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon ModuleAssignment = (ModuleName, Maybe LetBinding)

Methods

toAbstract :: ModuleAssignment -> ScopeM (AbsOfCon ModuleAssignment) Source #

NFData ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleAssignment -> () Source #
Show ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleAssignment -> ShowS Source # show :: ModuleAssignment -> String Source # showList :: [ModuleAssignment] -> ShowS Source #
Eq ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: ModuleAssignment -> ModuleAssignment -> Bool Source # (/=) :: ModuleAssignment -> ModuleAssignment -> Bool Source #
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

  From `@tactic` attribute.

- bnameIsFinite :: Bool

  The `@finite` cannot be parsed, it comes from the builtin `Partial` only.

#### Instances

Instances details

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 #
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 #
NFData Binder Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Binder -> () Source #
NFData BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: BoundName -> () Source #
Show BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> BoundName -> ShowS Source # show :: BoundName -> String Source # showList :: [BoundName] -> ShowS Source #
Eq BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: BoundName -> BoundName -> Bool Source # (/=) :: BoundName -> BoundName -> Bool Source #

mkBoundName_ :: Name -> BoundName Source #

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

type TacticAttribute = TacticAttribute' Expr Source #

newtype TacticAttribute' a Source #

Constructors

TacticAttribute |

Fields

- theTacticAttribute :: Maybe (Ranged a)

#### Instances

Instances details

Functor TacticAttribute' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> TacticAttribute' a -> TacticAttribute' b Source # (<$) :: a -> TacticAttribute' b -> TacticAttribute' a Source #
Foldable TacticAttribute' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => TacticAttribute' m -> m Source #

foldMap :: Monoid m => (a -> m) -> TacticAttribute' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> TacticAttribute' a -> m Source #

foldr :: (a -> b -> b) -> b -> TacticAttribute' a -> b Source #

foldr' :: (a -> b -> b) -> b -> TacticAttribute' a -> b Source #

foldl :: (b -> a -> b) -> b -> TacticAttribute' a -> b Source #

foldl' :: (b -> a -> b) -> b -> TacticAttribute' a -> b Source #

foldr1 :: (a -> a -> a) -> TacticAttribute' a -> a Source #

foldl1 :: (a -> a -> a) -> TacticAttribute' a -> a Source #

toList :: TacticAttribute' a -> [a] Source #

null :: TacticAttribute' a -> Bool Source #

length :: TacticAttribute' a -> Int Source #

elem :: Eq a => a -> TacticAttribute' a -> Bool Source #

maximum :: Ord a => TacticAttribute' a -> a Source #

minimum :: Ord a => TacticAttribute' a -> a Source #

sum :: Num a => TacticAttribute' a -> a Source #

product :: Num a => TacticAttribute' a -> a Source #

Traversable TacticAttribute' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b) Source #

sequenceA :: Applicative f => TacticAttribute' (f a) -> f (TacticAttribute' a) Source #

mapM :: Monad m => (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b) Source #

sequence :: Monad m => TacticAttribute' (m a) -> m (TacticAttribute' a) Source #

ExprLike a => ExprLike (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (TacticAttribute' a) Source # foldExpr :: FoldExprFn m (TacticAttribute' a) Source # traverseExpr :: TraverseExprFn m (TacticAttribute' a) Source # mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source #
Pretty a => Pretty (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TacticAttribute' a -> Doc Source # prettyPrec :: Int -> TacticAttribute' a -> Doc Source # prettyList :: [TacticAttribute' a] -> Doc Source #
ExprLike a => ExprLike (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source # foldExpr :: Monoid m => (Expr -> m) -> TacticAttribute' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TacticAttribute' a -> m (TacticAttribute' a) Source #
HasRange (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TacticAttribute' a -> Range Source #
KillRange (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (TacticAttribute' a) Source #
ToConcrete a => ToConcrete (TacticAttribute' a) Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (TacticAttribute' a) |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (TacticAttribute' a) = TacticAttribute' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => TacticAttribute' a -> m (ConOfAbs (TacticAttribute' a)) Source #

bindToConcrete :: MonadToConcrete m => TacticAttribute' a -> (ConOfAbs (TacticAttribute' a) -> m b) -> m b Source #

Null (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods empty :: TacticAttribute' a Source # null :: TacticAttribute' a -> Bool Source #
NFData a => NFData (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: TacticAttribute' a -> () Source #
Show a => Show (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> TacticAttribute' a -> ShowS Source # show :: TacticAttribute' a -> String Source # showList :: [TacticAttribute' a] -> ShowS Source #
Eq a => Eq (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: TacticAttribute' a -> TacticAttribute' a -> Bool Source # (/=) :: TacticAttribute' a -> TacticAttribute' a -> Bool Source #
type ConOfAbs (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (TacticAttribute' a) = TacticAttribute' (ConOfAbs a)

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 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 KwRange [TypeSignature] | Variables to be generalized, can be hidden and/or irrelevant.
Field KwRange [FieldSignature] |
FunClause LHS RHS WhereClause Catchall |
DataSig Range Erased Name [LamBinding] Expr | lone data signature in mutual block
Data Range Erased Name [LamBinding] Expr [TypeSignatureOrInstanceBlock] |
DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock] |
RecordSig Range Erased Name [LamBinding] Expr | lone record signature in mutual block
RecordDef Range Name [RecordDirective] [LamBinding] [Declaration] |
Record Range Erased Name [RecordDirective] [LamBinding] Expr [Declaration] |
Infix Fixity (List1 Name) |
Syntax Name Notation | notation declaration for a name
PatternSyn Range Name [WithHiding Name] Pattern |
Mutual KwRange [Declaration] |
InterleavedMutual KwRange [Declaration] |
Abstract KwRange [Declaration] |
Private KwRange 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 KwRange [Declaration] | The `KwRange` here only refers to the range of the `instance` keyword. The range of the whole block `InstanceB r ds` is `fuseRange r ds`.
LoneConstructor KwRange [Declaration] |
Macro KwRange [Declaration] |
Postulate KwRange [TypeSignatureOrInstanceBlock] |
Primitive KwRange [TypeSignature] |
Open Range QName ImportDirective |
Import Range QName (Maybe AsName) !OpenShortHand ImportDirective |
ModuleMacro Range Erased Name ModuleApplication !OpenShortHand ImportDirective |
Module Range Erased QName Telescope [Declaration] |

UnquoteDecl Range [Name] Expr

    unquoteDecl xs = e

UnquoteDef Range [Name] Expr

    unquoteDef xs = e

UnquoteData Range Name [Name] Expr

    unquoteDecl data d constructor xs = e

Pragma Pragma |

Opaque KwRange [Declaration]

    opaque ...

Unfolding KwRange [QName]

    unfolding ...

#### Instances

Instances details

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 #
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 #
FoldDecl Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> Declaration -> m Source #
TraverseDecl Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> 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 #
NFData Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Declaration -> () Source #
Show Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Declaration -> ShowS Source # show :: Declaration -> String Source # showList :: [Declaration] -> ShowS Source #
Show WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS Source # show :: WhereClause -> String Source # showList :: [WhereClause] -> ShowS Source #
Eq Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Declaration -> Declaration -> Bool Source # (/=) :: Declaration -> Declaration -> Bool Source #
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]) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (TopLevel [Declaration]) = TopLevelInfo

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

isPragma :: CMaybe Pragma m => Declaration -> m Source #

Return `Pragma` if `Declaration` is `Pragma`.

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

Pretty RecordDirective Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RecordDirective -> Doc Source # prettyPrec :: Int -> RecordDirective -> Doc Source # prettyList :: [RecordDirective] -> Doc Source #
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 #
EmbPrj RecordDirective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: RecordDirective -> S Word32 Source # icod_ :: RecordDirective -> S Word32 Source # value :: Word32 -> R RecordDirective Source #
NFData RecordDirective Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: RecordDirective -> () Source #
Show RecordDirective Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> RecordDirective -> ShowS Source # show :: RecordDirective -> String Source # showList :: [RecordDirective] -> ShowS Source #
Eq RecordDirective Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: RecordDirective -> RecordDirective -> Bool Source # (/=) :: RecordDirective -> RecordDirective -> Bool Source #

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

data ModuleApplication Source #

Constructors

SectionApp Range Telescope QName [Expr] | `tel M exprs` where `M exprs` is a `RawApp` just after parsing.

RecordModuleInstance Range QName

    M {{...}}

#### Instances

Instances details

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 #
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 #
NFData ModuleApplication Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleApplication -> () Source #
Show ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleApplication -> ShowS Source # show :: ModuleApplication -> String Source # showList :: [ModuleApplication] -> ShowS Source #
Eq ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: ModuleApplication -> ModuleApplication -> Bool Source # (/=) :: ModuleApplication -> ModuleApplication -> Bool Source #

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 #
NFData AsName Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () Source #
Functor AsName' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> AsName' a -> AsName' b Source # (<$) :: a -> AsName' b -> AsName' a Source #
Foldable AsName' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => AsName' m -> m Source #

foldMap :: Monoid m => (a -> m) -> AsName' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> AsName' a -> m Source #

foldr :: (a -> b -> b) -> b -> AsName' a -> b Source #

foldr' :: (a -> b -> b) -> b -> AsName' a -> b Source #

foldl :: (b -> a -> b) -> b -> AsName' a -> b Source #

foldl' :: (b -> a -> b) -> b -> AsName' a -> b Source #

foldr1 :: (a -> a -> a) -> AsName' a -> a Source #

foldl1 :: (a -> a -> a) -> AsName' a -> a Source #

toList :: AsName' a -> [a] Source #

null :: AsName' a -> Bool Source #

length :: AsName' a -> Int Source #

elem :: Eq a => a -> AsName' a -> Bool Source #

maximum :: Ord a => AsName' a -> a Source #

minimum :: Ord a => AsName' a -> a Source #

sum :: Num a => AsName' a -> a Source #

product :: Num a => AsName' a -> a Source #

Traversable AsName' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> AsName' a -> f (AsName' b) Source # sequenceA :: Applicative f => AsName' (f a) -> f (AsName' a) Source # mapM :: Monad m => (a -> m b) -> AsName' a -> m (AsName' b) Source # sequence :: Monad m => AsName' (m a) -> m (AsName' a) Source #
Show a => Show (AsName' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> AsName' a -> ShowS Source # show :: AsName' a -> String Source # showList :: [AsName' a] -> ShowS Source #
Eq a => Eq (AsName' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: AsName' a -> AsName' a -> Bool Source # (/=) :: AsName' a -> AsName' a -> Bool Source #

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 #
NFData OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: OpenShortHand -> () Source #
Generic OpenShortHand Source # |

Instance details

Defined in Agda.Syntax.Concrete

Associated Types

type Rep OpenShortHand |
Instance details Defined in Agda.Syntax.Concrete type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DontOpen" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: OpenShortHand -> Rep OpenShortHand x Source #

to :: Rep OpenShortHand x -> OpenShortHand Source #

Show OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> OpenShortHand -> ShowS Source # show :: OpenShortHand -> String Source # showList :: [OpenShortHand] -> ShowS Source #
Eq OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: OpenShortHand -> OpenShortHand -> Bool Source # (/=) :: OpenShortHand -> OpenShortHand -> Bool Source #
type Rep OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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

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 #
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 #
PrettyTCM LHS Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => LHS -> m Doc Source #
NFData LHS Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LHS -> () Source #
Show LHS Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LHS -> ShowS Source # show :: LHS -> String Source # showList :: [LHS] -> ShowS Source #
Eq LHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LHS -> LHS -> Bool Source # (/=) :: LHS -> LHS -> Bool Source #

data Pattern Source #

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP Bool QName | `c` or `x` If the boolean is `False`, then the `QName` must not refer to a constructor or a pattern synonym. The value `False` is used when a hidden argument pun is expanded.

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 (Set1 Name) (List1 (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

DotP KwRange Range Expr | `.e`, the `KwRange` is for the dot, the `Range` for the whole thing (including the dot).
LitP Range Literal | `0`, `1`, etc.
RecP KwRange Range [FieldAssignment' Pattern] | `record {x = p; y = q}`. The `KwRange` is for the `record` keyword.
EqualP Range (List1 (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

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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #

ToAbstract Pattern Source # | Scope check a `Pattern` not belonging to a `DisplayForm`.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Pattern = Pattern' Expr

Methods

toAbstract :: Pattern -> ScopeM (AbsOfCon Pattern) Source #

ToAbstract RewriteEqn Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

Methods

toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #

NFData Pattern Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pattern -> () Source #
Show Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pattern -> ShowS Source # show :: Pattern -> String Source # showList :: [Pattern] -> ShowS Source #
Eq Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Pattern -> Pattern -> Bool Source # (/=) :: Pattern -> Pattern -> Bool Source #
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 :: List1 Pattern

  At least one `(| p)`.

- lhsPats :: [NamedArg Pattern]

      ps

LHSEllipsis |

Fields

- lhsEllipsisRange :: Range
- lhsEllipsisPat :: LHSCore

  Pattern that was expanded from an ellipsis `...`.

#### Instances

Instances details

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 #
HasRange LHSCore Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHSCore -> Range Source #
ToAbstract LHSCore Source # | Scope-check a `LHSCore` not of a `DisplayForm`.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LHSCore = LHSCore' Expr

Methods

toAbstract :: LHSCore -> ScopeM (AbsOfCon LHSCore) Source #

Show LHSCore Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LHSCore -> ShowS Source # show :: LHSCore -> String Source # showList :: [LHSCore] -> ShowS Source #
Eq LHSCore Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LHSCore -> LHSCore -> Bool Source # (/=) :: LHSCore -> LHSCore -> Bool Source #
type AbsOfCon LHSCore Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LHSCore = LHSCore' Expr

data LamClause Source #

Constructors

LamClause |

Fields

- lamLHS :: [Pattern]

  Possibly empty sequence.

- lamRHS :: RHS
- lamCatchall :: Catchall

#### Instances

Instances details

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 #
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 #
NFData LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamClause -> () Source #
Show LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamClause -> ShowS Source # show :: LamClause -> String Source # showList :: [LamClause] -> ShowS Source #
Eq LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: LamClause -> LamClause -> Bool Source # (/=) :: LamClause -> LamClause -> Bool Source #

type RHS = RHS' Expr Source #

data RHS' e Source #

Constructors

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

#### Instances

Instances details

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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RHS

Methods

toAbstract :: RHS -> ScopeM (AbsOfCon RHS) Source #

Functor RHS' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> RHS' a -> RHS' b Source # (<$) :: a -> RHS' b -> RHS' a Source #
Foldable RHS' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => RHS' m -> m Source #

foldMap :: Monoid m => (a -> m) -> RHS' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> RHS' a -> m Source #

foldr :: (a -> b -> b) -> b -> RHS' a -> b Source #

foldr' :: (a -> b -> b) -> b -> RHS' a -> b Source #

foldl :: (b -> a -> b) -> b -> RHS' a -> b Source #

foldl' :: (b -> a -> b) -> b -> RHS' a -> b Source #

foldr1 :: (a -> a -> a) -> RHS' a -> a Source #

foldl1 :: (a -> a -> a) -> RHS' a -> a Source #

toList :: RHS' a -> [a] Source #

null :: RHS' a -> Bool Source #

length :: RHS' a -> Int Source #

elem :: Eq a => a -> RHS' a -> Bool Source #

maximum :: Ord a => RHS' a -> a Source #

minimum :: Ord a => RHS' a -> a Source #

sum :: Num a => RHS' a -> a Source #

product :: Num a => RHS' a -> a Source #

Traversable RHS' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> RHS' a -> f (RHS' b) Source # sequenceA :: Applicative f => RHS' (f a) -> f (RHS' a) Source # mapM :: Monad m => (a -> m b) -> RHS' a -> m (RHS' b) Source # sequence :: Monad m => RHS' (m a) -> m (RHS' a) Source #
Show RHS Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS -> ShowS Source # show :: RHS -> String Source # showList :: [RHS] -> ShowS Source #
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 #
NFData a => NFData (RHS' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: RHS' a -> () Source #
Eq e => Eq (RHS' e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: RHS' e -> RHS' e -> Bool Source # (/=) :: RHS' e -> RHS' e -> Bool Source #
type AbsOfCon RHS Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RHS

type WhereClause = WhereClause' [Declaration] Source #

`where` block following a clause.

data WhereClause' decls Source #

The generalization `WhereClause'` is for the sake of Agda.Concrete.Generic.

Constructors

NoWhere | No `where` clauses.
AnyWhere Range decls | Ordinary `where`. `Range` of the `where` keyword. List of declarations can be empty.
SomeWhere Range Erased 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

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 #
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 #
Functor WhereClause' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b Source # (<$) :: a -> WhereClause' b -> WhereClause' a Source #
Foldable WhereClause' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => WhereClause' m -> m Source #

foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> WhereClause' a -> m Source #

foldr :: (a -> b -> b) -> b -> WhereClause' a -> b Source #

foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b Source #

foldl :: (b -> a -> b) -> b -> WhereClause' a -> b Source #

foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b Source #

foldr1 :: (a -> a -> a) -> WhereClause' a -> a Source #

foldl1 :: (a -> a -> a) -> WhereClause' a -> a Source #

toList :: WhereClause' a -> [a] Source #

null :: WhereClause' a -> Bool Source #

length :: WhereClause' a -> Int Source #

elem :: Eq a => a -> WhereClause' a -> Bool Source #

maximum :: Ord a => WhereClause' a -> a Source #

minimum :: Ord a => WhereClause' a -> a Source #

sum :: Num a => WhereClause' a -> a Source #

product :: Num a => WhereClause' a -> a Source #

Traversable WhereClause' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) Source # sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) Source # mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) Source # sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) Source #
Show WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS Source # show :: WhereClause -> String Source # showList :: [WhereClause] -> ShowS Source #
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 #
FoldDecl a => FoldDecl (WhereClause' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> WhereClause' a -> m Source #
TraverseDecl a => TraverseDecl (WhereClause' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> 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 #
NFData a => NFData (WhereClause' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause' a -> () Source #
Eq decls => Eq (WhereClause' decls) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: WhereClause' decls -> WhereClause' decls -> Bool Source # (/=) :: WhereClause' decls -> WhereClause' decls -> Bool Source #

data WhereClause_ Source #

Type of `where` block following a clause.

Constructors

NoWhere_ | No `where` clauses.
AnyWhere_ | Ordinary `where`.
SomeWhere_ | Named where: `module M where ...`.

#### Instances

Instances details

Null WhereClause_ Source # |
Instance details Defined in Agda.Syntax.Concrete Methods empty :: WhereClause_ Source # null :: WhereClause_ -> Bool Source #
NFData WhereClause_ Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause_ -> () Source #
Generic WhereClause_ Source # |

Instance details

Defined in Agda.Syntax.Concrete

Associated Types

type Rep WhereClause_ |
Instance details Defined in Agda.Syntax.Concrete type Rep WhereClause_ = D1 ('MetaData "WhereClause_" "Agda.Syntax.Concrete" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NoWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AnyWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SomeWhere_" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: WhereClause_ -> Rep WhereClause_ x Source #

to :: Rep WhereClause_ x -> WhereClause_ Source #

Eq WhereClause_ Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: WhereClause_ -> WhereClause_ -> Bool Source # (/=) :: WhereClause_ -> WhereClause_ -> Bool Source #
type Rep WhereClause_ Source # |
Instance details Defined in Agda.Syntax.Concrete type Rep WhereClause_ = D1 ('MetaData "WhereClause_" "Agda.Syntax.Concrete" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NoWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AnyWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SomeWhere_" 'PrefixI 'False) (U1 :: Type -> Type)))

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 |

whereClause_ :: WhereClause' a -> WhereClause_ Source #

data DoStmt Source #

Constructors

DoBind Range Pattern Expr [LamClause]

    p ← e where cs

DoThen Expr |
DoLet Range (List1 Declaration) |

#### Instances

Instances details

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 #
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 #
NFData DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: DoStmt -> () Source #
Show DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> DoStmt -> ShowS Source # show :: DoStmt -> String Source # showList :: [DoStmt] -> ShowS Source #
Eq DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: DoStmt -> DoStmt -> Bool Source # (/=) :: DoStmt -> DoStmt -> Bool Source #

data Pragma Source #

Constructors

OptionsPragma Range [String] |
BuiltinPragma Range RString QName |
RewritePragma Range Range [QName] | Second Range is for REWRITE keyword.
ForeignPragma Range (Ranged BackendName) String |
CompilePragma Range (Ranged BackendName) QName String |
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.
InjectiveForInferencePragma Range QName | Mark a definition as injective for the conversion checker
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 [Ranged Occurrence] |
NoUniverseCheckPragma Range | Applies to the following data/record type.
NotProjectionLikePragma Range QName | Applies to the stated function
OverlapPragma Range [QName] OverlapMode | Applies to the given name(s), which must be instance names (checked by the type checker).

#### Instances

Instances details

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 #
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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Pragma = [Pragma]

Methods

toAbstract :: Pragma -> ScopeM (AbsOfCon Pragma) Source #

NFData Pragma Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pragma -> () Source #
Show Pragma Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
Eq Pragma Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: Pragma -> Pragma -> Bool Source # (/=) :: Pragma -> Pragma -> Bool Source #
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 Source # show :: Module -> String Source # showList :: [Module] -> ShowS Source #

data ThingWithFixity x Source #

Decorating something with `Fixity'`.

Constructors

ThingWithFixity x Fixity' |

#### Instances

Instances details

Functor ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b Source # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a Source #
Foldable ThingWithFixity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

fold :: Monoid m => ThingWithFixity m -> m Source #

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m Source #

foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m Source #

foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

toList :: ThingWithFixity a -> [a] Source #

null :: ThingWithFixity a -> Bool Source #

length :: ThingWithFixity a -> Int Source #

elem :: Eq a => a -> ThingWithFixity a -> Bool Source #

maximum :: Ord a => ThingWithFixity a -> a Source #

minimum :: Ord a => ThingWithFixity a -> a Source #

sum :: Num a => ThingWithFixity a -> a Source #

product :: Num a => ThingWithFixity a -> a Source #

Traversable ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) Source # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) Source # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) Source # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) Source #
LensFixity (ThingWithFixity a) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' (ThingWithFixity a) Fixity Source #
LensFixity' (ThingWithFixity a) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' (ThingWithFixity a) Fixity' 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 #
KillRange x => KillRange (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source #
Show x => Show (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS Source # show :: ThingWithFixity x -> String Source # showList :: [ThingWithFixity x] -> ShowS Source #

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 |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #

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 Source # (<$) :: a -> HoleContent' qn nm p b -> HoleContent' qn nm p a Source #
Foldable (HoleContent' qn nm p) Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => HoleContent' qn nm p m -> m Source #

foldMap :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m Source #

foldMap' :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m Source #

foldr :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b Source #

foldr' :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b Source #

foldl :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b Source #

foldl' :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b Source #

foldr1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a Source #

foldl1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a Source #

toList :: HoleContent' qn nm p a -> [a] Source #

null :: HoleContent' qn nm p a -> Bool Source #

length :: HoleContent' qn nm p a -> Int Source #

elem :: Eq a => a -> HoleContent' qn nm p a -> Bool Source #

maximum :: Ord a => HoleContent' qn nm p a -> a Source #

minimum :: Ord a => HoleContent' qn nm p a -> a Source #

sum :: Num a => HoleContent' qn nm p a -> a Source #

product :: Num a => HoleContent' qn nm p a -> a Source #

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) Source #

sequenceA :: Applicative f => HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a) Source #

mapM :: Monad m => (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b) Source #

sequence :: Monad m => HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a) Source #

type AbsOfCon HoleContent Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

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.

ungatherRecordDirectives :: RecordDirectives -> [RecordDirective] Source #