Safe Haskell | None |
---|---|
Language | Haskell2010 |
The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.
Synopsis
- data Expr
- = Ident QName
- | Lit Range Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe String)
- | RawApp Range (List2 Expr)
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set Name) OpAppArgs
- | WithApp Range Expr [Expr]
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range (List1 LamBinding) Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range Erased (List1 LamClause)
- | Fun Range (Arg Expr) Expr
- | Pi Telescope1 Expr
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range (List1 Declaration) (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range [Expr]
- | DoBlock Range (List1 DoStmt)
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | DoubleDot Range Expr
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
- | KnownIdent NameKind QName
- | KnownOpApp NameKind Range QName (Set 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 = [NamedArg (MaybePlaceholder (OpApp e))]
- module Agda.Syntax.Concrete.Name
- data AppView = AppView Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- rawApp :: List1 Expr -> Expr
- rawAppP :: List1 Pattern -> Pattern
- isSingleIdentifierP :: Pattern -> Maybe Name
- removeParenP :: Pattern -> Pattern
- isPattern :: Expr -> Maybe Pattern
- isAbsurdP :: Pattern -> Maybe (Range, Hiding)
- isBinderP :: Pattern -> Maybe Binder
- 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
- 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
- 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 {}
- 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 Bool
- | 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
- type RecordDirectives = RecordDirectives' (Name, IsInstance)
- data ModuleApplication
- 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 {}
- type AsName = AsName' (Either Expr Name)
- data OpenShortHand
- type RewriteEqn = RewriteEqn' () Name Pattern Expr
- type WithExpr = Named Name (Arg Expr)
- data LHS = LHS {}
- data Pattern
- = IdentP Bool QName
- | QuoteP Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP Range (List2 Pattern)
- | OpAppP Range QName (Set Name) [NamedArg Pattern]
- | HiddenP Range (Named_ Pattern)
- | InstanceP Range (Named_ Pattern)
- | ParenP Range Pattern
- | WildP Range
- | AbsurdP Range
- | AsP Range Name Pattern
- | DotP Range Expr
- | LitP Range Literal
- | RecP Range [FieldAssignment' Pattern]
- | EqualP Range [(Expr, Expr)]
- | EllipsisP Range (Maybe Pattern)
- | WithP Range Pattern
- data LHSCore
- = LHSHead {
- lhsDefName :: QName
- lhsPats :: [NamedArg Pattern]
- | LHSProj { }
- | LHSWith { }
- | LHSEllipsis { }
- = LHSHead {
- data LamClause = LamClause {
- lamLHS :: [Pattern]
- lamRHS :: RHS
- lamCatchAll :: Bool
- type RHS = RHS' Expr
- data RHS' e
- type WhereClause = WhereClause' [Declaration]
- data WhereClause' decls
- data ExprWhere = ExprWhere Expr WhereClause
- data DoStmt
- data Pragma
- = OptionsPragma Range [String]
- | BuiltinPragma Range RString QName
- | RewritePragma Range Range [QName]
- | ForeignPragma Range RString String
- | CompilePragma Range RString QName String
- | StaticPragma Range QName
- | InlinePragma Range Bool QName
- | ImpossiblePragma Range [String]
- | EtaPragma Range QName
- | WarningOnUsage Range QName Text
- | WarningOnImport Range Text
- | InjectivePragma Range QName
- | InjectiveForInferencePragma Range QName
- | DisplayPragma Range Pattern Expr
- | CatchallPragma Range
- | TerminationCheckPragma Range (TerminationCheck Name)
- | NoCoverageCheckPragma Range
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [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
Concrete expressions. Should represent exactly what the user wrote.
Ident QName | ex: |
Lit Range Literal | ex: |
QuestionMark Range (Maybe Nat) | ex: |
Underscore Range (Maybe String) | ex: |
RawApp Range (List2 Expr) | before parsing operators |
App Range Expr (NamedArg Expr) | ex: |
OpApp Range QName (Set Name) OpAppArgs | ex: |
WithApp Range Expr [Expr] | ex: |
HiddenArg Range (Named_ Expr) | ex: |
InstanceArg Range (Named_ Expr) | ex: |
Lam Range (List1 LamBinding) Expr | ex: |
AbsurdLam Range Hiding | ex: |
ExtendedLam Range Erased (List1 LamClause) | ex: |
Fun Range (Arg Expr) Expr | ex: |
Pi Telescope1 Expr | ex: |
Rec Range RecordAssignments | ex: |
RecUpdate Range Expr [FieldAssignment] | ex: |
Let Range (List1 Declaration) (Maybe Expr) | ex: |
Paren Range Expr | ex: |
IdiomBrackets Range [Expr] | ex: |
DoBlock Range (List1 DoStmt) | ex: |
Absurd Range | ex: |
As Range Name Expr | ex: |
Dot Range Expr | ex: |
DoubleDot Range Expr | ex: |
Quote Range | ex: |
QuoteTerm Range | ex: |
Tactic Range Expr | ex: |
Unquote Range | ex: |
DontCare Expr | to print irrelevant things |
Equal Range Expr Expr | ex: |
Ellipsis Range |
|
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 (Set Name) OpAppArgs | An operator application coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing). |
Generalized Expr |
Instances
SyntaxBindingLambda Range (List1 LamBinding) e | An abstraction inside a special syntax declaration (see Issue 358 why we introduce this). |
Ordinary e |
Instances
Functor OpApp Source # | |
Foldable OpApp Source # | |
Defined in Agda.Syntax.Concrete fold :: Monoid m => OpApp m -> m foldMap :: Monoid m => (a -> m) -> OpApp a -> m foldMap' :: Monoid m => (a -> m) -> OpApp a -> m foldr :: (a -> b -> b) -> b -> OpApp a -> b foldr' :: (a -> b -> b) -> b -> OpApp a -> b foldl :: (b -> a -> b) -> b -> OpApp a -> b foldl' :: (b -> a -> b) -> b -> OpApp a -> b foldr1 :: (a -> a -> a) -> OpApp a -> a foldl1 :: (a -> a -> a) -> OpApp a -> a elem :: Eq a => a -> OpApp a -> Bool maximum :: Ord a => OpApp a -> a | |
Traversable OpApp Source # | |
Pretty (OpApp Expr) Source # | |
ExprLike a => ExprLike (OpApp a) Source # | |
HasRange e => HasRange (OpApp e) Source # | |
KillRange e => KillRange (OpApp e) Source # | |
Defined in Agda.Syntax.Concrete killRange :: KillRangeT (OpApp e) Source # | |
NFData a => NFData (OpApp a) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Show a => Show (OpApp a) | |
Eq e => Eq (OpApp e) Source # | |
fromOrdinary :: e -> OpApp e -> e Source #
type OpAppArgs = OpAppArgs' Expr Source #
type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))] Source #
module Agda.Syntax.Concrete.Name
removeParenP :: Pattern -> Pattern Source #
isPattern :: Expr -> Maybe Pattern Source #
Turn an expression into a pattern. Fails if the expression is not a valid pattern.
observeHiding :: Expr -> WithHiding Expr Source #
Observe the hiding status of an expression
exprToPatternWithHoles :: Expr -> Pattern Source #
Turn an expression into a pattern, turning non-pattern subexpressions into WildP
.
Bindings
A Binder x@p
, the pattern is optional
Binder | |
|
Instances
HasRange Binder Source # | |
KillRange Binder Source # | |
Defined in Agda.Syntax.Concrete | |
NFData Binder Source # | |
Defined in Agda.Syntax.Concrete | |
Functor Binder' Source # | |
Foldable Binder' Source # | |
Defined in Agda.Syntax.Concrete fold :: Monoid m => Binder' m -> m foldMap :: Monoid m => (a -> m) -> Binder' a -> m foldMap' :: Monoid m => (a -> m) -> Binder' a -> m foldr :: (a -> b -> b) -> b -> Binder' a -> b foldr' :: (a -> b -> b) -> b -> Binder' a -> b foldl :: (b -> a -> b) -> b -> Binder' a -> b foldl' :: (b -> a -> b) -> b -> Binder' a -> b foldr1 :: (a -> a -> a) -> Binder' a -> a foldl1 :: (a -> a -> a) -> Binder' a -> a elem :: Eq a => a -> Binder' a -> Bool maximum :: Ord a => Binder' a -> a minimum :: Ord a => Binder' a -> a | |
Traversable Binder' Source # | |
Pretty a => Pretty (Binder' a) Source # | |
ToAbstract (Binder' (NewName BoundName)) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
Show a => Show (Binder' a) | |
Eq a => Eq (Binder' a) Source # | |
type AbsOfCon (Binder' (NewName BoundName)) Source # | |
type LamBinding = LamBinding' TypedBinding Source #
A lambda binding is either domain free or typed.
data LamBinding' a Source #
DomainFree (NamedArg Binder) | . |
DomainFull a | . |
Instances
LensHiding LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |||||
Pretty LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source # | |||||
ExprLike LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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 # | |||||
Defined in Agda.Syntax.Concrete getRange :: LamBinding -> Range Source # | |||||
KillRange LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
ToAbstract LamBinding Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source # | |||||
Functor LamBinding' Source # | |||||
Defined in Agda.Syntax.Concrete fmap :: (a -> b) -> LamBinding' a -> LamBinding' b (<$) :: a -> LamBinding' b -> LamBinding' a # | |||||
Foldable LamBinding' Source # | |||||
Defined in Agda.Syntax.Concrete fold :: Monoid m => LamBinding' m -> m foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m foldMap' :: Monoid m => (a -> m) -> LamBinding' a -> m foldr :: (a -> b -> b) -> b -> LamBinding' a -> b foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b foldl :: (b -> a -> b) -> b -> LamBinding' a -> b foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b foldr1 :: (a -> a -> a) -> LamBinding' a -> a foldl1 :: (a -> a -> a) -> LamBinding' a -> a toList :: LamBinding' a -> [a] null :: LamBinding' a -> Bool length :: LamBinding' a -> Int elem :: Eq a => a -> LamBinding' a -> Bool maximum :: Ord a => LamBinding' a -> a minimum :: Ord a => LamBinding' a -> a sum :: Num a => LamBinding' a -> a product :: Num a => LamBinding' a -> a | |||||
Traversable LamBinding' Source # | |||||
Defined in Agda.Syntax.Concrete traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) | |||||
Show LamBinding | |||||
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS | |||||
NFData a => NFData (LamBinding' a) Source # | |||||
Defined in Agda.Syntax.Concrete rnf :: LamBinding' a -> () | |||||
Eq a => Eq (LamBinding' a) Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: LamBinding' a -> LamBinding' a -> Bool (/=) :: LamBinding' a -> LamBinding' a -> Bool | |||||
type AbsOfCon LamBinding Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
dropTypeAndModality :: LamBinding -> [LamBinding] Source #
Drop type annotations and lets from bindings.
type TypedBinding = TypedBinding' Expr Source #
A typed binding.
data TypedBinding' e Source #
TBind Range (List1 (NamedArg Binder)) e | Binding |
TLet Range (List1 Declaration) | Let binding |
Instances
LensHiding LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |||||
LensHiding TypedBinding Source # | |||||
Defined in Agda.Syntax.Concrete getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |||||
LensRelevance TypedBinding Source # | |||||
Defined in Agda.Syntax.Concrete getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source # | |||||
Pretty LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source # | |||||
Pretty TypedBinding Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source # | |||||
ExprLike LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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 # | |||||
Defined in Agda.Syntax.Concrete getRange :: LamBinding -> Range Source # | |||||
HasRange TypedBinding Source # | |||||
Defined in Agda.Syntax.Concrete getRange :: TypedBinding -> Range Source # | |||||
KillRange LamBinding Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
KillRange TypedBinding Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
SetRange TypedBinding Source # | |||||
Defined in Agda.Syntax.Concrete setRange :: Range -> TypedBinding -> TypedBinding Source # | |||||
ToAbstract LamBinding Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source # | |||||
ToAbstract TypedBinding Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source # | |||||
Functor TypedBinding' Source # | |||||
Defined in Agda.Syntax.Concrete fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b (<$) :: a -> TypedBinding' b -> TypedBinding' a # | |||||
Foldable TypedBinding' Source # | |||||
Defined in Agda.Syntax.Concrete fold :: Monoid m => TypedBinding' m -> m foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m foldMap' :: Monoid m => (a -> m) -> TypedBinding' a -> m foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b foldr1 :: (a -> a -> a) -> TypedBinding' a -> a foldl1 :: (a -> a -> a) -> TypedBinding' a -> a toList :: TypedBinding' a -> [a] null :: TypedBinding' a -> Bool length :: TypedBinding' a -> Int elem :: Eq a => a -> TypedBinding' a -> Bool maximum :: Ord a => TypedBinding' a -> a minimum :: Ord a => TypedBinding' a -> a sum :: Num a => TypedBinding' a -> a product :: Num a => TypedBinding' a -> a | |||||
Traversable TypedBinding' Source # | |||||
Defined in Agda.Syntax.Concrete traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b) sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a) mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b) sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a) | |||||
Show LamBinding | |||||
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS | |||||
Show TypedBinding | |||||
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> TypedBinding -> ShowS show :: TypedBinding -> String showList :: [TypedBinding] -> ShowS | |||||
ExprLike a => ExprLike (TypedBinding' a) Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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. | ||||
Defined in Agda.Syntax.Concrete rnf :: TypedBinding' a -> () | |||||
Eq e => Eq (TypedBinding' e) Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: TypedBinding' e -> TypedBinding' e -> Bool (/=) :: TypedBinding' e -> TypedBinding' e -> Bool | |||||
type AbsOfCon LamBinding Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type AbsOfCon TypedBinding Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
type RecordAssignment = Either FieldAssignment ModuleAssignment Source #
type RecordAssignments = [RecordAssignment] Source #
type FieldAssignment = FieldAssignment' Expr Source #
data FieldAssignment' a Source #
FieldAssignment | |
|
Instances
ExprLike FieldAssignment Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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 # | |||||
Defined in Agda.Syntax.Concrete fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b (<$) :: a -> FieldAssignment' b -> FieldAssignment' a # | |||||
Foldable FieldAssignment' Source # | |||||
Defined in Agda.Syntax.Concrete fold :: Monoid m => FieldAssignment' m -> m foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m foldMap' :: Monoid m => (a -> m) -> FieldAssignment' a -> m foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a toList :: FieldAssignment' a -> [a] null :: FieldAssignment' a -> Bool length :: FieldAssignment' a -> Int elem :: Eq a => a -> FieldAssignment' a -> Bool maximum :: Ord a => FieldAssignment' a -> a minimum :: Ord a => FieldAssignment' a -> a sum :: Num a => FieldAssignment' a -> a product :: Num a => FieldAssignment' a -> a | |||||
Traversable FieldAssignment' Source # | |||||
Defined in Agda.Syntax.Concrete traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b) sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a) mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b) sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a) | |||||
SubstExpr a => SubstExpr (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Abstract substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source # | |||||
APatternLike a => APatternLike (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern
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 # | |||||
Defined in Agda.Syntax.Abstract.Pattern mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source # | |||||
DeclaredNames a => DeclaredNames (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => FieldAssignment' a -> m Source # | |||||
ExprLike a => ExprLike (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views 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 # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: FieldAssignment' a -> Doc Source # prettyPrec :: Int -> FieldAssignment' a -> Doc Source # prettyList :: [FieldAssignment' a] -> Doc Source # | |||||
CPatternLike p => CPatternLike (FieldAssignment' p) Source # | |||||
Defined in Agda.Syntax.Concrete.Pattern 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 # | |||||
Defined in Agda.Syntax.Internal.Names namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FieldAssignment' a -> m Source # | |||||
HasRange a => HasRange (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Concrete getRange :: FieldAssignment' a -> Range Source # | |||||
KillRange a => KillRange (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Concrete killRange :: KillRangeT (FieldAssignment' a) Source # | |||||
ToConcrete a => ToConcrete (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a)) Source # bindToConcrete :: FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> AbsToCon b) -> AbsToCon b Source # | |||||
ToAbstract c => ToAbstract (FieldAssignment' c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: FieldAssignment' c -> ScopeM (AbsOfCon (FieldAssignment' c)) Source # | |||||
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Abstract expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) Source # | |||||
EmbPrj a => EmbPrj (FieldAssignment' a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: FieldAssignment' a -> S Int32 Source # icod_ :: FieldAssignment' a -> S Int32 Source # value :: Int32 -> R (FieldAssignment' a) Source # | |||||
NFData a => NFData (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Concrete rnf :: FieldAssignment' a -> () | |||||
Show a => Show (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Concrete showsPrec :: Int -> FieldAssignment' a -> ShowS show :: FieldAssignment' a -> String showList :: [FieldAssignment' a] -> ShowS | |||||
Eq a => Eq (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: FieldAssignment' a -> FieldAssignment' a -> Bool (/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool | |||||
PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern patToExpr :: FieldAssignment' p -> Reader Hiding (FieldAssignment' e) Source # | |||||
type ADotT (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
type ConOfAbs (FieldAssignment' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (FieldAssignment' c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
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 #
Instances
Pretty ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: ModuleAssignment -> Doc Source # prettyPrec :: Int -> ModuleAssignment -> Doc Source # prettyList :: [ModuleAssignment] -> Doc Source # | |||||
ExprLike ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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 # | |||||
Defined in Agda.Syntax.Concrete getRange :: ModuleAssignment -> Range Source # | |||||
KillRange ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
ToAbstract ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
NFData ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Concrete rnf :: ModuleAssignment -> () | |||||
Show ModuleAssignment | |||||
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> ModuleAssignment -> ShowS show :: ModuleAssignment -> String showList :: [ModuleAssignment] -> ShowS | |||||
Eq ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: ModuleAssignment -> ModuleAssignment -> Bool (/=) :: ModuleAssignment -> ModuleAssignment -> Bool | |||||
type AbsOfCon ModuleAssignment Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
BName | |
|
Instances
Pretty BoundName Source # | |
HasRange Binder Source # | |
HasRange BoundName Source # | |
KillRange Binder Source # | |
Defined in Agda.Syntax.Concrete | |
KillRange BoundName Source # | |
Defined in Agda.Syntax.Concrete | |
NFData Binder Source # | |
Defined in Agda.Syntax.Concrete | |
NFData BoundName Source # | |
Defined in Agda.Syntax.Concrete | |
Show BoundName | |
Eq BoundName Source # | |
ToAbstract (Binder' (NewName BoundName)) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
ToAbstract (NewName BoundName) Source # | |
type AbsOfCon (Binder' (NewName BoundName)) Source # | |
type AbsOfCon (NewName BoundName) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
mkBoundName_ :: Name -> BoundName Source #
type TacticAttribute = TacticAttribute' Expr Source #
newtype TacticAttribute' a Source #
Instances
Functor TacticAttribute' Source # | |||||
Defined in Agda.Syntax.Concrete fmap :: (a -> b) -> TacticAttribute' a -> TacticAttribute' b (<$) :: a -> TacticAttribute' b -> TacticAttribute' a # | |||||
Foldable TacticAttribute' Source # | |||||
Defined in Agda.Syntax.Concrete fold :: Monoid m => TacticAttribute' m -> m foldMap :: Monoid m => (a -> m) -> TacticAttribute' a -> m foldMap' :: Monoid m => (a -> m) -> TacticAttribute' a -> m foldr :: (a -> b -> b) -> b -> TacticAttribute' a -> b foldr' :: (a -> b -> b) -> b -> TacticAttribute' a -> b foldl :: (b -> a -> b) -> b -> TacticAttribute' a -> b foldl' :: (b -> a -> b) -> b -> TacticAttribute' a -> b foldr1 :: (a -> a -> a) -> TacticAttribute' a -> a foldl1 :: (a -> a -> a) -> TacticAttribute' a -> a toList :: TacticAttribute' a -> [a] null :: TacticAttribute' a -> Bool length :: TacticAttribute' a -> Int elem :: Eq a => a -> TacticAttribute' a -> Bool maximum :: Ord a => TacticAttribute' a -> a minimum :: Ord a => TacticAttribute' a -> a sum :: Num a => TacticAttribute' a -> a product :: Num a => TacticAttribute' a -> a | |||||
Traversable TacticAttribute' Source # | |||||
Defined in Agda.Syntax.Concrete traverse :: Applicative f => (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b) sequenceA :: Applicative f => TacticAttribute' (f a) -> f (TacticAttribute' a) mapM :: Monad m => (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b) sequence :: Monad m => TacticAttribute' (m a) -> m (TacticAttribute' a) | |||||
ExprLike a => ExprLike (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views 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 # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: TacticAttribute' a -> Doc Source # prettyPrec :: Int -> TacticAttribute' a -> Doc Source # prettyList :: [TacticAttribute' a] -> Doc Source # | |||||
ExprLike a => ExprLike (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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 # | |||||
KillRange (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Concrete killRange :: KillRangeT (TacticAttribute' a) Source # | |||||
ToConcrete a => ToConcrete (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: TacticAttribute' a -> AbsToCon (ConOfAbs (TacticAttribute' a)) Source # bindToConcrete :: TacticAttribute' a -> (ConOfAbs (TacticAttribute' a) -> AbsToCon b) -> AbsToCon b Source # | |||||
Null (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Concrete empty :: TacticAttribute' a Source # null :: TacticAttribute' a -> Bool Source # | |||||
NFData a => NFData (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Concrete rnf :: TacticAttribute' a -> () | |||||
Show a => Show (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Concrete showsPrec :: Int -> TacticAttribute' a -> ShowS show :: TacticAttribute' a -> String showList :: [TacticAttribute' a] -> ShowS | |||||
Eq a => Eq (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: TacticAttribute' a -> TacticAttribute' a -> Bool (/=) :: TacticAttribute' a -> TacticAttribute' a -> Bool | |||||
type ConOfAbs (TacticAttribute' a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete |
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.
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 Bool | |
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 |
InstanceB KwRange [Declaration] | The |
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
Pretty Declaration Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source # | |||||
Pretty WhereClause Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |||||
ExprLike Declaration Source # | |||||
Defined in Agda.Syntax.Concrete.Generic 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 # | |||||
Defined in Agda.Syntax.Concrete.Generic foldDecl :: Monoid m => (Declaration -> m) -> Declaration -> m Source # | |||||
TraverseDecl Declaration Source # | |||||
Defined in Agda.Syntax.Concrete.Generic preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> Declaration -> m Declaration Source # | |||||
HasRange Declaration Source # | |||||
Defined in Agda.Syntax.Concrete getRange :: Declaration -> Range Source # | |||||
HasRange WhereClause Source # | |||||
Defined in Agda.Syntax.Concrete getRange :: WhereClause -> Range Source # | |||||
KillRange Declaration Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
KillRange WhereClause Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
NFData Declaration Source # | |||||
Defined in Agda.Syntax.Concrete rnf :: Declaration -> () | |||||
Show Declaration | |||||
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> Declaration -> ShowS show :: Declaration -> String showList :: [Declaration] -> ShowS | |||||
Show WhereClause | |||||
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> WhereClause -> ShowS show :: WhereClause -> String showList :: [WhereClause] -> ShowS | |||||
Eq Declaration Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: Declaration -> Declaration -> Bool (/=) :: Declaration -> Declaration -> Bool | |||||
ToAbstract (TopLevel [Declaration]) Source # | Top-level declarations are always
| ||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source # | |||||
type AbsOfCon (TopLevel [Declaration]) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
isPragma :: CMaybe Pragma m => Declaration -> m Source #
Return Pragma
if Declaration
is Pragma
.
data RecordDirective Source #
Isolated record directives parsed as Declarations
Induction (Ranged Induction) | Range of keyword |
Constructor Name IsInstance | |
Eta (Ranged HasEta0) | Range of |
PatternOrCopattern Range | If declaration |
Instances
Pretty RecordDirective Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: RecordDirective -> Doc Source # prettyPrec :: Int -> RecordDirective -> Doc Source # prettyList :: [RecordDirective] -> Doc Source # | |
HasRange RecordDirective Source # | |
Defined in Agda.Syntax.Concrete getRange :: RecordDirective -> Range Source # | |
KillRange RecordDirective Source # | |
Defined in Agda.Syntax.Concrete | |
EmbPrj RecordDirective Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: RecordDirective -> S Int32 Source # icod_ :: RecordDirective -> S Int32 Source # value :: Int32 -> R RecordDirective Source # | |
NFData RecordDirective Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete rnf :: RecordDirective -> () | |
Show RecordDirective Source # | |
Defined in Agda.Syntax.Concrete showsPrec :: Int -> RecordDirective -> ShowS show :: RecordDirective -> String showList :: [RecordDirective] -> ShowS | |
Eq RecordDirective Source # | |
Defined in Agda.Syntax.Concrete (==) :: RecordDirective -> RecordDirective -> Bool (/=) :: RecordDirective -> RecordDirective -> Bool |
type RecordDirectives = RecordDirectives' (Name, IsInstance) Source #
data ModuleApplication Source #
SectionApp Range Telescope Expr | tel. M args |
RecordModuleInstance Range QName | M {{...}} |
Instances
Pretty ModuleApplication Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: ModuleApplication -> Doc Source # prettyPrec :: Int -> ModuleApplication -> Doc Source # prettyList :: [ModuleApplication] -> Doc Source # | |
ExprLike ModuleApplication Source # | |
Defined in Agda.Syntax.Concrete.Generic 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 # | |
Defined in Agda.Syntax.Concrete getRange :: ModuleApplication -> Range Source # | |
KillRange ModuleApplication Source # | |
Defined in Agda.Syntax.Concrete | |
NFData ModuleApplication Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete rnf :: ModuleApplication -> () | |
Show ModuleApplication | |
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> ModuleApplication -> ShowS show :: ModuleApplication -> String showList :: [ModuleApplication] -> ShowS | |
Eq ModuleApplication Source # | |
Defined in Agda.Syntax.Concrete (==) :: ModuleApplication -> ModuleApplication -> Bool (/=) :: ModuleApplication -> ModuleApplication -> Bool |
type TypeSignature = Declaration Source #
Just type signatures.
type TypeSignatureOrInstanceBlock = Declaration Source #
Just type signatures or instance blocks.
type ImportDirective = ImportDirective' Name Name Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
type ImportedName = ImportedName' Name Name Source #
An imported name can be a module or a defined name.
type HidingDirective = HidingDirective' Name Name Source #
The content of the as
-clause of the import statement.
Instances
HasRange AsName Source # | |
KillRange AsName Source # | |
Defined in Agda.Syntax.Concrete | |
NFData AsName Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Functor AsName' Source # | |
Foldable AsName' Source # | |
Defined in Agda.Syntax.Concrete fold :: Monoid m => AsName' m -> m foldMap :: Monoid m => (a -> m) -> AsName' a -> m foldMap' :: Monoid m => (a -> m) -> AsName' a -> m foldr :: (a -> b -> b) -> b -> AsName' a -> b foldr' :: (a -> b -> b) -> b -> AsName' a -> b foldl :: (b -> a -> b) -> b -> AsName' a -> b foldl' :: (b -> a -> b) -> b -> AsName' a -> b foldr1 :: (a -> a -> a) -> AsName' a -> a foldl1 :: (a -> a -> a) -> AsName' a -> a elem :: Eq a => a -> AsName' a -> Bool maximum :: Ord a => AsName' a -> a minimum :: Ord a => AsName' a -> a | |
Traversable AsName' Source # | |
Show a => Show (AsName' a) Source # | |
Eq a => Eq (AsName' a) Source # | |
data OpenShortHand Source #
Instances
Pretty OpenShortHand Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source # | |||||
NFData OpenShortHand Source # | |||||
Defined in Agda.Syntax.Concrete rnf :: OpenShortHand -> () | |||||
Generic OpenShortHand Source # | |||||
Defined in Agda.Syntax.Concrete
from :: OpenShortHand -> Rep OpenShortHand x to :: Rep OpenShortHand x -> OpenShortHand | |||||
Show OpenShortHand Source # | |||||
Defined in Agda.Syntax.Concrete showsPrec :: Int -> OpenShortHand -> ShowS show :: OpenShortHand -> String showList :: [OpenShortHand] -> ShowS | |||||
Eq OpenShortHand Source # | |||||
Defined in Agda.Syntax.Concrete (==) :: OpenShortHand -> OpenShortHand -> Bool (/=) :: OpenShortHand -> OpenShortHand -> Bool | |||||
type Rep OpenShortHand Source # | |||||
Defined in Agda.Syntax.Concrete type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DontOpen" 'PrefixI 'False) (U1 :: Type -> Type)) |
type RewriteEqn = RewriteEqn' () Name Pattern Expr Source #
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.
LHS | Original pattern (including with-patterns), rewrite equations and with-expressions. |
|
Instances
Pretty LHS Source # | |
ExprLike LHS Source # | |
HasEllipsis LHS Source # | Does the lhs contain an ellipsis? |
Defined in Agda.Syntax.Concrete.Pattern hasEllipsis :: LHS -> Bool Source # | |
HasRange LHS Source # | |
KillRange LHS Source # | |
Defined in Agda.Syntax.Concrete | |
NFData LHS Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Show LHS | |
Eq LHS Source # | |
Concrete patterns. No literals in patterns at the moment.
IdentP Bool QName |
If the boolean is
|
QuoteP Range | quote |
AppP Pattern (NamedArg Pattern) |
|
RawAppP Range (List2 Pattern) |
|
OpAppP Range QName (Set Name) [NamedArg Pattern] | eg: |
HiddenP Range (Named_ Pattern) |
|
InstanceP Range (Named_ Pattern) |
|
ParenP Range Pattern | (p) |
WildP Range | _ |
AbsurdP Range | () |
AsP Range Name Pattern |
|
DotP Range Expr | .e |
LitP Range Literal |
|
RecP Range [FieldAssignment' Pattern] | record {x = p; y = q} |
EqualP Range [(Expr, Expr)] |
|
EllipsisP Range (Maybe Pattern) |
|
WithP Range Pattern |
|
Instances
Pretty Pattern Source # | |||||
IsExpr Pattern Source # | |||||
CPatternLike Pattern Source # | |||||
Defined in Agda.Syntax.Concrete.Pattern 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 # | |||||
Defined in Agda.Syntax.Concrete.Pattern hasEllipsis :: Pattern -> Bool Source # | |||||
IsEllipsis Pattern Source # | Is the pattern just | ||||
Defined in Agda.Syntax.Concrete.Pattern isEllipsis :: Pattern -> Bool Source # | |||||
IsWithP Pattern Source # | |||||
HasRange Pattern Source # | |||||
KillRange Pattern Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
SetRange Pattern Source # | |||||
ToAbstract HoleContent Source # | Content of interaction hole. | ||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source # | |||||
ToAbstract Pattern Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
ToAbstract RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |||||
NFData Pattern Source # | Ranges are not forced. | ||||
Defined in Agda.Syntax.Concrete | |||||
Show Pattern | |||||
Eq Pattern Source # | |||||
type AbsOfCon HoleContent Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type AbsOfCon Pattern Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type AbsOfCon RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Processed (operator-parsed) intermediate form of the core f ps
of LHS
.
Corresponds to lhsOriginalPattern
.
LHSHead | |
| |
LHSProj | |
LHSWith | |
LHSEllipsis | |
|
Instances
Pretty LHSCore Source # | |||||
HasRange LHSCore Source # | |||||
ToAbstract LHSCore Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
Show LHSCore | |||||
Eq LHSCore Source # | |||||
type AbsOfCon LHSCore Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Instances
Pretty RHS Source # | |||||
HasRange RHS Source # | |||||
KillRange RHS Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
ToAbstract RHS Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
Functor RHS' Source # | |||||
Foldable RHS' Source # | |||||
Defined in Agda.Syntax.Concrete fold :: Monoid m => RHS' m -> m foldMap :: Monoid m => (a -> m) -> RHS' a -> m foldMap' :: Monoid m => (a -> m) -> RHS' a -> m foldr :: (a -> b -> b) -> b -> RHS' a -> b foldr' :: (a -> b -> b) -> b -> RHS' a -> b foldl :: (b -> a -> b) -> b -> RHS' a -> b foldl' :: (b -> a -> b) -> b -> RHS' a -> b foldr1 :: (a -> a -> a) -> RHS' a -> a foldl1 :: (a -> a -> a) -> RHS' a -> a elem :: Eq a => a -> RHS' a -> Bool maximum :: Ord a => RHS' a -> a | |||||
Traversable RHS' Source # | |||||
Show RHS | |||||
ExprLike a => ExprLike (RHS' a) Source # | |||||
NFData a => NFData (RHS' a) Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
Eq e => Eq (RHS' e) Source # | |||||
type AbsOfCon RHS Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
type WhereClause = WhereClause' [Declaration] Source #
where
block following a clause.
data WhereClause' decls Source #
NoWhere | No |
AnyWhere Range decls | Ordinary |
SomeWhere Range Erased Name Access decls | Named where: |
Instances
Pretty WhereClause Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |
HasRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete getRange :: WhereClause -> Range Source # | |
KillRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete | |
Functor WhereClause' Source # | |
Defined in Agda.Syntax.Concrete fmap :: (a -> b) -> WhereClause' a -> WhereClause' b (<$) :: a -> WhereClause' b -> WhereClause' a # | |
Foldable WhereClause' Source # | |
Defined in Agda.Syntax.Concrete fold :: Monoid m => WhereClause' m -> m foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m foldMap' :: Monoid m => (a -> m) -> WhereClause' a -> m foldr :: (a -> b -> b) -> b -> WhereClause' a -> b foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b foldl :: (b -> a -> b) -> b -> WhereClause' a -> b foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b foldr1 :: (a -> a -> a) -> WhereClause' a -> a foldl1 :: (a -> a -> a) -> WhereClause' a -> a toList :: WhereClause' a -> [a] null :: WhereClause' a -> Bool length :: WhereClause' a -> Int elem :: Eq a => a -> WhereClause' a -> Bool maximum :: Ord a => WhereClause' a -> a minimum :: Ord a => WhereClause' a -> a sum :: Num a => WhereClause' a -> a product :: Num a => WhereClause' a -> a | |
Traversable WhereClause' Source # | |
Defined in Agda.Syntax.Concrete traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) | |
Show WhereClause | |
Defined in Agda.Syntax.Concrete.Pretty showsPrec :: Int -> WhereClause -> ShowS show :: WhereClause -> String showList :: [WhereClause] -> ShowS | |
ExprLike a => ExprLike (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete.Generic 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 # | |
Defined in Agda.Syntax.Concrete.Generic foldDecl :: Monoid m => (Declaration -> m) -> WhereClause' a -> m Source # | |
TraverseDecl a => TraverseDecl (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete.Generic preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> WhereClause' a -> m (WhereClause' a) Source # | |
Null (WhereClause' a) Source # | A |
Defined in Agda.Syntax.Concrete empty :: WhereClause' a Source # null :: WhereClause' a -> Bool Source # | |
NFData a => NFData (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete rnf :: WhereClause' a -> () | |
Eq decls => Eq (WhereClause' decls) Source # | |
Defined in Agda.Syntax.Concrete (==) :: WhereClause' decls -> WhereClause' decls -> Bool (/=) :: WhereClause' decls -> WhereClause' decls -> Bool |
An expression followed by a where clause. Currently only used to give better a better error message in interaction.
OptionsPragma Range [String] | |
BuiltinPragma Range RString QName | |
RewritePragma Range Range [QName] | Second Range is for REWRITE keyword. |
ForeignPragma Range RString String | first string is backend name |
CompilePragma Range RString QName String | first string is backend name |
StaticPragma Range QName | |
InlinePragma Range Bool QName | INLINE or NOINLINE |
ImpossiblePragma Range [String] | Throws an internal error in the scope checker.
The |
EtaPragma Range QName | For coinductive records, use pragma instead of regular
|
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 [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
Pretty Pragma Source # | |||||
HasRange Pragma Source # | |||||
KillRange Pragma Source # | |||||
Defined in Agda.Syntax.Concrete | |||||
ToAbstract Pragma Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
NFData Pragma Source # | Ranges are not forced. | ||||
Defined in Agda.Syntax.Concrete | |||||
Show Pragma | |||||
Eq Pragma Source # | |||||
type AbsOfCon Pragma Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Modules: Top-level pragmas plus other top-level declarations.
Mod | |
|
data ThingWithFixity x Source #
Decorating something with Fixity'
.
Instances
Functor ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b (<$) :: a -> ThingWithFixity b -> ThingWithFixity a # | |
Foldable ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity fold :: Monoid m => ThingWithFixity m -> m foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a toList :: ThingWithFixity a -> [a] null :: ThingWithFixity a -> Bool length :: ThingWithFixity a -> Int elem :: Eq a => a -> ThingWithFixity a -> Bool maximum :: Ord a => ThingWithFixity a -> a minimum :: Ord a => ThingWithFixity a -> a sum :: Num a => ThingWithFixity a -> a product :: Num a => ThingWithFixity a -> a | |
Traversable ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) | |
LensFixity (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity lensFixity :: Lens' (ThingWithFixity a) Fixity Source # | |
LensFixity' (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity lensFixity' :: Lens' (ThingWithFixity a) Fixity' Source # | |
Pretty (ThingWithFixity Name) Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source # | |
KillRange x => KillRange (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity killRange :: KillRangeT (ThingWithFixity x) Source # | |
Show x => Show (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity showsPrec :: Int -> ThingWithFixity x -> ShowS show :: ThingWithFixity x -> String showList :: [ThingWithFixity x] -> ShowS |
type HoleContent = HoleContent' () Name Pattern Expr Source #
data HoleContent' qn nm p e Source #
Extended content of an interaction hole.
HoleContentExpr e | e |
HoleContentRewrite [RewriteEqn' qn nm p e] | (rewrite | invert) e0 | ... | en |
Instances
ToAbstract HoleContent Source # | Content of interaction hole. | ||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source # | |||||
Functor (HoleContent' qn nm p) Source # | |||||
Defined in Agda.Syntax.Concrete fmap :: (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b (<$) :: a -> HoleContent' qn nm p b -> HoleContent' qn nm p a # | |||||
Foldable (HoleContent' qn nm p) Source # | |||||
Defined in Agda.Syntax.Concrete fold :: Monoid m => HoleContent' qn nm p m -> m foldMap :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m foldMap' :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m foldr :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b foldr' :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b foldl :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b foldl' :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b foldr1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a foldl1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a toList :: HoleContent' qn nm p a -> [a] null :: HoleContent' qn nm p a -> Bool length :: HoleContent' qn nm p a -> Int elem :: Eq a => a -> HoleContent' qn nm p a -> Bool maximum :: Ord a => HoleContent' qn nm p a -> a minimum :: Ord a => HoleContent' qn nm p a -> a sum :: Num a => HoleContent' qn nm p a -> a product :: Num a => HoleContent' qn nm p a -> a | |||||
Traversable (HoleContent' qn nm p) Source # | |||||
Defined in Agda.Syntax.Concrete traverse :: Applicative f => (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b) sequenceA :: Applicative f => HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a) mapM :: Monad m => (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b) sequence :: Monad m => HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a) | |||||
type AbsOfCon HoleContent Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
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.