Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.Syntax.Concrete
Contents
Description
The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.
Synopsis
- data Expr
- = Ident QName
- | Lit Range Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe String)
- | RawApp Range (List2 Expr)
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set Name) OpAppArgs
- | WithApp Range Expr [Expr]
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range (List1 LamBinding) Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range Erased (List1 LamClause)
- | Fun Range (Arg Expr) Expr
- | Pi Telescope1 Expr
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range (List1 Declaration) (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range [Expr]
- | DoBlock Range (List1 DoStmt)
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | DoubleDot Range Expr
- | ETel Telescope
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
- | Generalized Expr
- data OpApp e
- = SyntaxBindingLambda Range (List1 LamBinding) e
- | Ordinary e
- fromOrdinary :: e -> OpApp e -> e
- type OpAppArgs = OpAppArgs' Expr
- type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))]
- module Agda.Syntax.Concrete.Name
- data AppView = AppView Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- rawApp :: List1 Expr -> Expr
- rawAppP :: List1 Pattern -> Pattern
- isSingleIdentifierP :: Pattern -> Maybe Name
- removeParenP :: Pattern -> Pattern
- isPattern :: Expr -> Maybe Pattern
- isAbsurdP :: Pattern -> Maybe (Range, Hiding)
- isBinderP :: Pattern -> Maybe Binder
- exprToPatternWithHoles :: Expr -> Pattern
- returnExpr :: Expr -> Maybe Expr
- data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
- type Binder = Binder' BoundName
- mkBinder_ :: Name -> Binder
- mkBinder :: a -> Binder' a
- type LamBinding = LamBinding' TypedBinding
- data LamBinding' a
- = DomainFree (NamedArg Binder)
- | DomainFull a
- dropTypeAndModality :: LamBinding -> [LamBinding]
- type TypedBinding = TypedBinding' Expr
- data TypedBinding' e
- type RecordAssignment = Either FieldAssignment ModuleAssignment
- type RecordAssignments = [RecordAssignment]
- type FieldAssignment = FieldAssignment' Expr
- data FieldAssignment' a = FieldAssignment {
- _nameFieldA :: Name
- _exprFieldA :: a
- nameFieldA :: Lens' Name (FieldAssignment' a)
- exprFieldA :: Lens' a (FieldAssignment' a)
- data ModuleAssignment = ModuleAssignment {}
- data BoundName = BName {}
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type TacticAttribute = Maybe Expr
- type Telescope = [TypedBinding]
- type Telescope1 = List1 TypedBinding
- lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
- makePi :: Telescope -> Expr -> Expr
- mkLam :: Range -> [LamBinding] -> Expr -> Expr
- mkLet :: Range -> [Declaration] -> Expr -> Expr
- mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e)
- data RecordDirective
- isRecordDirective :: Declaration -> Maybe RecordDirective
- type RecordDirectives = RecordDirectives' (Name, IsInstance)
- data Declaration
- = TypeSig ArgInfo TacticAttribute Name Expr
- | FieldSig IsInstance TacticAttribute Name (Arg Expr)
- | Generalize Range [TypeSignature]
- | Field Range [FieldSignature]
- | FunClause LHS RHS WhereClause Bool
- | DataSig Range Name [LamBinding] Expr
- | Data Range Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
- | DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name [LamBinding] Expr
- | RecordDef Range Name RecordDirectives [LamBinding] [Declaration]
- | Record Range Name RecordDirectives [LamBinding] Expr [Declaration]
- | RecordDirective RecordDirective
- | Infix Fixity (List1 Name)
- | Syntax Name Notation
- | PatternSyn Range Name [Arg Name] Pattern
- | Mutual Range [Declaration]
- | InterleavedMutual Range [Declaration]
- | Abstract Range [Declaration]
- | Private Range Origin [Declaration]
- | InstanceB Range [Declaration]
- | LoneConstructor Range [Declaration]
- | Macro Range [Declaration]
- | Postulate Range [TypeSignatureOrInstanceBlock]
- | Primitive Range [TypeSignature]
- | Open Range QName ImportDirective
- | Import Range QName (Maybe AsName) !OpenShortHand ImportDirective
- | ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective
- | Module Range QName Telescope [Declaration]
- | UnquoteDecl Range [Name] Expr
- | UnquoteDef Range [Name] Expr
- | Pragma Pragma
- data ModuleApplication
- 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 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 {
- observeHiding :: Expr -> WithHiding Expr
- observeRelevance :: Expr -> (Relevance, Expr)
- observeModifiers :: Expr -> Arg Expr
- data LamClause = LamClause {
- lamLHS :: [Pattern]
- lamRHS :: RHS
- lamCatchAll :: Bool
- type RHS = RHS' Expr
- data RHS' e
- 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
- | DisplayPragma Range Pattern Expr
- | CatchallPragma Range
- | TerminationCheckPragma Range (TerminationCheck Name)
- | NoCoverageCheckPragma Range
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
- | NoUniverseCheckPragma Range
- data Module = Mod {
- modPragmas :: [Pragma]
- modDecls :: [Declaration]
- data ThingWithFixity x = ThingWithFixity x Fixity'
- type HoleContent = HoleContent' () Name Pattern Expr
- data HoleContent' qn nm p e
- = HoleContentExpr e
- | HoleContentRewrite [RewriteEqn' qn nm p e]
- topLevelModuleName :: Module -> TopLevelModuleName
- spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
Expressions
Concrete expressions. Should represent exactly what the user wrote.
Constructors
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: |
ETel Telescope | only used for printing telescopes |
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 |
|
Generalized Expr |
Instances
Constructors
SyntaxBindingLambda Range (List1 LamBinding) e | An abstraction inside a special syntax declaration (see Issue 358 why we introduce this). |
Ordinary e |
Instances
Foldable OpApp Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => OpApp m -> m foldMap :: Monoid m => (a -> m) -> OpApp a -> m foldMap' :: Monoid m => (a -> m) -> OpApp a -> m foldr :: (a -> b -> b) -> b -> OpApp a -> b foldr' :: (a -> b -> b) -> b -> OpApp a -> b foldl :: (b -> a -> b) -> b -> OpApp a -> b foldl' :: (b -> a -> b) -> b -> OpApp a -> b foldr1 :: (a -> a -> a) -> OpApp a -> a foldl1 :: (a -> a -> a) -> OpApp a -> a elem :: Eq a => a -> OpApp a -> Bool maximum :: Ord a => OpApp a -> a | |
Traversable OpApp Source # | |
Functor OpApp Source # | |
ExprLike a => ExprLike (OpApp a) Source # | |
HasRange e => HasRange (OpApp e) Source # | |
KillRange e => KillRange (OpApp e) Source # | |
Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source # | |
Pretty (OpApp Expr) Source # | |
Data e => Data (OpApp e) Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpApp e -> c (OpApp e) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e) dataTypeOf :: OpApp e -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e)) dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e)) gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r gmapQ :: (forall d. Data d => d -> u) -> OpApp e -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpApp e -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) | |
Show a => Show (OpApp a) | |
NFData a => NFData (OpApp a) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
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
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.
exprToPatternWithHoles :: Expr -> Pattern Source #
Turn an expression into a pattern, turning non-pattern subexpressions into WildP
.
returnExpr :: Expr -> Maybe Expr Source #
Bindings
A Binder x@p
, the pattern is optional
Constructors
Binder | |
Fields
|
Instances
HasRange Binder Source # | |
KillRange Binder Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Foldable Binder' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => Binder' m -> m foldMap :: Monoid m => (a -> m) -> Binder' a -> m foldMap' :: Monoid m => (a -> m) -> Binder' a -> m foldr :: (a -> b -> b) -> b -> Binder' a -> b foldr' :: (a -> b -> b) -> b -> Binder' a -> b foldl :: (b -> a -> b) -> b -> Binder' a -> b foldl' :: (b -> a -> b) -> b -> Binder' a -> b foldr1 :: (a -> a -> a) -> Binder' a -> a foldl1 :: (a -> a -> a) -> Binder' a -> a elem :: Eq a => a -> Binder' a -> Bool maximum :: Ord a => Binder' a -> a minimum :: Ord a => Binder' a -> a | |
Traversable Binder' Source # | |
Functor Binder' Source # | |
NFData Binder Source # | |
Defined in Agda.Syntax.Concrete | |
ToAbstract (Binder' (NewName BoundName)) Source # | |
Pretty a => Pretty (Binder' a) Source # | |
Data a => Data (Binder' a) Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder' a -> c (Binder' a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder' a) toConstr :: Binder' a -> Constr dataTypeOf :: Binder' a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder' a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder' a)) gmapT :: (forall b. Data b => b -> b) -> Binder' a -> Binder' a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r gmapQ :: (forall d. Data d => d -> u) -> Binder' a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder' a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) | |
Show a => Show (Binder' a) | |
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 #
Constructors
DomainFree (NamedArg Binder) | . |
DomainFull a | . |
Instances
LensHiding LamBinding Source # | |
Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
ExprLike LamBinding Source # | |
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 # | |
Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source # | |
KillRange LamBinding Source # | |
Defined in Agda.Syntax.Concrete Methods | |
ToAbstract LamBinding Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LamBinding Source # Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source # | |
Pretty LamBinding Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source # | |
Foldable LamBinding' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => LamBinding' m -> m foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m foldMap' :: Monoid m => (a -> m) -> LamBinding' a -> m foldr :: (a -> b -> b) -> b -> LamBinding' a -> b foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b foldl :: (b -> a -> b) -> b -> LamBinding' a -> b foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b foldr1 :: (a -> a -> a) -> LamBinding' a -> a foldl1 :: (a -> a -> a) -> LamBinding' a -> a toList :: LamBinding' a -> [a] null :: LamBinding' a -> Bool length :: LamBinding' a -> Int elem :: Eq a => a -> LamBinding' a -> Bool maximum :: Ord a => LamBinding' a -> a minimum :: Ord a => LamBinding' a -> a sum :: Num a => LamBinding' a -> a product :: Num a => LamBinding' a -> a | |
Traversable LamBinding' Source # | |
Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) | |
Functor LamBinding' Source # | |
Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b (<$) :: a -> LamBinding' b -> LamBinding' a # | |
Show LamBinding | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS | |
Data a => Data (LamBinding' a) Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding' a -> c (LamBinding' a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LamBinding' a) toConstr :: LamBinding' a -> Constr dataTypeOf :: LamBinding' a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LamBinding' a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LamBinding' a)) gmapT :: (forall b. Data b => b -> b) -> LamBinding' a -> LamBinding' a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r gmapQ :: (forall d. Data d => d -> u) -> LamBinding' a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding' a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) | |
NFData a => NFData (LamBinding' a) Source # | |
Defined in Agda.Syntax.Concrete Methods rnf :: LamBinding' a -> () | |
Eq a => Eq (LamBinding' a) Source # | |
Defined in Agda.Syntax.Concrete | |
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 #
Constructors
TBind Range (List1 (NamedArg Binder)) e | Binding |
TLet Range (List1 Declaration) | Let binding |
Instances
type RecordAssignment = Either FieldAssignment ModuleAssignment Source #
type RecordAssignments = [RecordAssignment] Source #
type FieldAssignment = FieldAssignment' Expr Source #
data FieldAssignment' a Source #
Constructors
FieldAssignment | |
Fields
|
Instances
nameFieldA :: Lens' Name (FieldAssignment' a) Source #
exprFieldA :: Lens' a (FieldAssignment' a) Source #
data ModuleAssignment Source #
Constructors
ModuleAssignment | |
Fields
|
Instances
Constructors
BName | |
Fields |
Instances
HasRange Binder Source # | |
HasRange BoundName Source # | |
KillRange Binder Source # | |
Defined in Agda.Syntax.Concrete Methods | |
KillRange BoundName Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Pretty BoundName Source # | |
Data BoundName Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoundName -> c BoundName gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoundName toConstr :: BoundName -> Constr dataTypeOf :: BoundName -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoundName) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoundName) gmapT :: (forall b. Data b => b -> b) -> BoundName -> BoundName gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r gmapQ :: (forall d. Data d => d -> u) -> BoundName -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BoundName -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName | |
Show BoundName | |
NFData Binder Source # | |
Defined in Agda.Syntax.Concrete | |
NFData BoundName Source # | |
Defined in Agda.Syntax.Concrete | |
Eq BoundName Source # | |
ToAbstract (Binder' (NewName BoundName)) Source # | |
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 = Maybe Expr Source #
type Telescope = [TypedBinding] Source #
type Telescope1 = List1 TypedBinding Source #
A telescope is a sequence of typed bindings. Bound variables are in scope in later types.
lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope Source #
We can try to get a Telescope
from a [LamBinding]
.
If we have a type annotation already, we're happy.
Otherwise we manufacture a binder with an underscore for the type.
makePi :: Telescope -> Expr -> Expr Source #
Smart constructor for Pi
: check whether the Telescope
is empty
mkLam :: Range -> [LamBinding] -> Expr -> Expr Source #
Smart constructor for Lam
: check for non-zero bindings.
mkLet :: Range -> [Declaration] -> Expr -> Expr Source #
Smart constructor for Let
: check for non-zero let bindings.
mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e) Source #
Smart constructor for TLet
: check for non-zero let bindings.
Declarations
data RecordDirective Source #
Isolated record directives parsed as Declarations
Constructors
Induction (Ranged Induction) | Range of keyword |
Constructor Name IsInstance | |
Eta (Ranged HasEta0) | Range of |
PatternOrCopattern Range | If declaration |
Instances
HasRange RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: RecordDirective -> Range Source # | |
KillRange RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Data RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RecordDirective -> c RecordDirective gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RecordDirective toConstr :: RecordDirective -> Constr dataTypeOf :: RecordDirective -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RecordDirective) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RecordDirective) gmapT :: (forall b. Data b => b -> b) -> RecordDirective -> RecordDirective gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirective -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirective -> r gmapQ :: (forall d. Data d => d -> u) -> RecordDirective -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RecordDirective -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RecordDirective -> m RecordDirective gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirective -> m RecordDirective gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirective -> m RecordDirective | |
Show RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> RecordDirective -> ShowS show :: RecordDirective -> String showList :: [RecordDirective] -> ShowS | |
NFData RecordDirective Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete Methods rnf :: RecordDirective -> () | |
Eq RecordDirective Source # | |
Defined in Agda.Syntax.Concrete Methods (==) :: RecordDirective -> RecordDirective -> Bool (/=) :: RecordDirective -> RecordDirective -> Bool |
isRecordDirective :: Declaration -> Maybe RecordDirective Source #
Extract a record directive
type RecordDirectives = RecordDirectives' (Name, IsInstance) Source #
data Declaration Source #
The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.
Constructors
Instances
ExprLike Declaration Source # | |
Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration Source # | |
HasRange Declaration Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range Source # | |
HasRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |
KillRange Declaration Source # | |
Defined in Agda.Syntax.Concrete Methods | |
KillRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Pretty Declaration Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source # | |
Pretty WhereClause Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |
Data Declaration Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration toConstr :: Declaration -> Constr dataTypeOf :: Declaration -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration | |
Show Declaration | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Declaration -> ShowS show :: Declaration -> String showList :: [Declaration] -> ShowS | |
Show WhereClause | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS show :: WhereClause -> String showList :: [WhereClause] -> ShowS | |
NFData Declaration Source # | |
Defined in Agda.Syntax.Concrete Methods rnf :: Declaration -> () | |
Eq Declaration Source # | |
Defined in Agda.Syntax.Concrete | |
ToAbstract (TopLevel [Declaration]) Source # | Top-level declarations are always
|
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (TopLevel [Declaration]) Source # Methods toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source # | |
type AbsOfCon (TopLevel [Declaration]) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
data ModuleApplication Source #
Constructors
SectionApp Range Telescope Expr | tel. M args |
RecordModuleInstance Range QName | M {{...}} |
Instances
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.
Constructors
AsName | |
Instances
HasRange AsName Source # | |
KillRange AsName Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Foldable AsName' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => AsName' m -> m foldMap :: Monoid m => (a -> m) -> AsName' a -> m foldMap' :: Monoid m => (a -> m) -> AsName' a -> m foldr :: (a -> b -> b) -> b -> AsName' a -> b foldr' :: (a -> b -> b) -> b -> AsName' a -> b foldl :: (b -> a -> b) -> b -> AsName' a -> b foldl' :: (b -> a -> b) -> b -> AsName' a -> b foldr1 :: (a -> a -> a) -> AsName' a -> a foldl1 :: (a -> a -> a) -> AsName' a -> a elem :: Eq a => a -> AsName' a -> Bool maximum :: Ord a => AsName' a -> a minimum :: Ord a => AsName' a -> a | |
Traversable AsName' Source # | |
Functor AsName' Source # | |
NFData AsName Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Data a => Data (AsName' a) Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AsName' a -> c (AsName' a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AsName' a) toConstr :: AsName' a -> Constr dataTypeOf :: AsName' a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AsName' a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AsName' a)) gmapT :: (forall b. Data b => b -> b) -> AsName' a -> AsName' a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AsName' a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AsName' a -> r gmapQ :: (forall d. Data d => d -> u) -> AsName' a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AsName' a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) | |
Show a => Show (AsName' a) Source # | |
Eq a => Eq (AsName' a) Source # | |
data OpenShortHand Source #
Instances
Pretty OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source # | |
Data OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpenShortHand -> c OpenShortHand gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpenShortHand toConstr :: OpenShortHand -> Constr dataTypeOf :: OpenShortHand -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpenShortHand) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpenShortHand) gmapT :: (forall b. Data b => b -> b) -> OpenShortHand -> OpenShortHand gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r gmapQ :: (forall d. Data d => d -> u) -> OpenShortHand -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpenShortHand -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand | |
Generic OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete Associated Types type Rep OpenShortHand :: Type -> Type | |
Show OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> OpenShortHand -> ShowS show :: OpenShortHand -> String showList :: [OpenShortHand] -> ShowS | |
NFData OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete Methods rnf :: OpenShortHand -> () | |
Eq OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete | |
type Rep OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" '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.
Constructors
LHS | Original pattern (including with-patterns), rewrite equations and with-expressions. |
Fields
|
Instances
ExprLike LHS Source # | |
HasEllipsis LHS Source # | Does the lhs contain an ellipsis? |
Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool Source # | |
HasRange LHS Source # | |
KillRange LHS Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Pretty LHS Source # | |
Data LHS Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS dataTypeOf :: LHS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS | |
Show LHS | |
NFData LHS Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Eq LHS Source # | |
Concrete patterns. No literals in patterns at the moment.
Constructors
IdentP QName |
|
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
IsExpr Pattern Source # | |
CPatternLike Pattern Source # | |
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 # | |
Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool Source # | |
IsEllipsis Pattern Source # | Is the pattern just |
Defined in Agda.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool Source # | |
IsWithP Pattern Source # | |
HasRange Pattern Source # | |
KillRange Pattern Source # | |
Defined in Agda.Syntax.Concrete Methods | |
SetRange Pattern Source # | |
ToAbstract HoleContent Source # | Content of interaction hole. |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon HoleContent Source # Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source # | |
ToAbstract Pattern Source # | |
ToAbstract RewriteEqn Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RewriteEqn Source # Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |
Pretty Pattern Source # | |
Data Pattern Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern -> c Pattern gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pattern dataTypeOf :: Pattern -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pattern) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pattern) gmapT :: (forall b. Data b => b -> b) -> Pattern -> Pattern gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r gmapQ :: (forall d. Data d => d -> u) -> Pattern -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern | |
Show Pattern | |
NFData Pattern Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
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
.
Constructors
LHSHead | |
Fields
| |
LHSProj | |
LHSWith | |
LHSEllipsis | |
Fields
|
Instances
HasRange LHSCore Source # | |
ToAbstract LHSCore Source # | |
Pretty LHSCore Source # | |
Data LHSCore Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore -> c LHSCore gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSCore dataTypeOf :: LHSCore -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHSCore) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHSCore) gmapT :: (forall b. Data b => b -> b) -> LHSCore -> LHSCore gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore -> r gmapQ :: (forall d. Data d => d -> u) -> LHSCore -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore -> m LHSCore gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore -> m LHSCore gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore -> m LHSCore | |
Show LHSCore | |
Eq LHSCore Source # | |
type AbsOfCon LHSCore Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
observeHiding :: Expr -> WithHiding Expr Source #
Observe the hiding status of an expression
Constructors
LamClause | |
Fields
|
Instances
ExprLike LamClause Source # | |
HasRange LamClause Source # | |
KillRange LamClause Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Pretty LamClause Source # | |
Data LamClause Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamClause -> c LamClause gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamClause toConstr :: LamClause -> Constr dataTypeOf :: LamClause -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamClause) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamClause) gmapT :: (forall b. Data b => b -> b) -> LamClause -> LamClause gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r gmapQ :: (forall d. Data d => d -> u) -> LamClause -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LamClause -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause | |
Show LamClause | |
NFData LamClause Source # | |
Defined in Agda.Syntax.Concrete | |
Eq LamClause Source # | |
Instances
HasRange RHS Source # | |
KillRange RHS Source # | |
Defined in Agda.Syntax.Concrete Methods | |
ToAbstract RHS Source # | |
Pretty RHS Source # | |
Foldable RHS' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => RHS' m -> m foldMap :: Monoid m => (a -> m) -> RHS' a -> m foldMap' :: Monoid m => (a -> m) -> RHS' a -> m foldr :: (a -> b -> b) -> b -> RHS' a -> b foldr' :: (a -> b -> b) -> b -> RHS' a -> b foldl :: (b -> a -> b) -> b -> RHS' a -> b foldl' :: (b -> a -> b) -> b -> RHS' a -> b foldr1 :: (a -> a -> a) -> RHS' a -> a foldl1 :: (a -> a -> a) -> RHS' a -> a elem :: Eq a => a -> RHS' a -> Bool maximum :: Ord a => RHS' a -> a | |
Traversable RHS' Source # | |
Functor RHS' Source # | |
Show RHS | |
ExprLike a => ExprLike (RHS' a) Source # | |
Data e => Data (RHS' e) Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS' e -> c (RHS' e) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e) dataTypeOf :: RHS' e -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e)) dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e)) gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r gmapQ :: (forall d. Data d => d -> u) -> RHS' e -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS' e -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) | |
NFData a => NFData (RHS' a) Source # | |
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 #
Constructors
NoWhere | No |
AnyWhere Range decls | Ordinary |
SomeWhere Range Name Access decls | Named where: |
Instances
HasRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |
KillRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Pretty WhereClause Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |
Foldable WhereClause' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => WhereClause' m -> m foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m foldMap' :: Monoid m => (a -> m) -> WhereClause' a -> m foldr :: (a -> b -> b) -> b -> WhereClause' a -> b foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b foldl :: (b -> a -> b) -> b -> WhereClause' a -> b foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b foldr1 :: (a -> a -> a) -> WhereClause' a -> a foldl1 :: (a -> a -> a) -> WhereClause' a -> a toList :: WhereClause' a -> [a] null :: WhereClause' a -> Bool length :: WhereClause' a -> Int elem :: Eq a => a -> WhereClause' a -> Bool maximum :: Ord a => WhereClause' a -> a minimum :: Ord a => WhereClause' a -> a sum :: Num a => WhereClause' a -> a product :: Num a => WhereClause' a -> a | |
Traversable WhereClause' Source # | |
Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) | |
Functor WhereClause' Source # | |
Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b (<$) :: a -> WhereClause' b -> WhereClause' a # | |
Show WhereClause | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS show :: WhereClause -> String showList :: [WhereClause] -> ShowS | |
ExprLike a => ExprLike (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a Source # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) Source # | |
Null (WhereClause' a) Source # | A |
Defined in Agda.Syntax.Concrete | |
Data decls => Data (WhereClause' decls) Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereClause' decls -> c (WhereClause' decls) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WhereClause' decls) toConstr :: WhereClause' decls -> Constr dataTypeOf :: WhereClause' decls -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WhereClause' decls)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WhereClause' decls)) gmapT :: (forall b. Data b => b -> b) -> WhereClause' decls -> WhereClause' decls gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r gmapQ :: (forall d. Data d => d -> u) -> WhereClause' decls -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereClause' decls -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) | |
NFData a => NFData (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause' a -> () | |
Eq decls => Eq (WhereClause' decls) Source # | |
Defined in Agda.Syntax.Concrete Methods (==) :: 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.
Constructors
ExprWhere Expr WhereClause |
Constructors
DoBind Range Pattern Expr [LamClause] | p ← e where cs |
DoThen Expr | |
DoLet Range (List1 Declaration) |
Instances
ExprLike DoStmt Source # | |
HasRange DoStmt Source # | |
KillRange DoStmt Source # | |
Defined in Agda.Syntax.Concrete Methods | |
Pretty DoStmt Source # | |
Data DoStmt Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoStmt -> c DoStmt gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoStmt dataTypeOf :: DoStmt -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoStmt) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoStmt) gmapT :: (forall b. Data b => b -> b) -> DoStmt -> DoStmt gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r gmapQ :: (forall d. Data d => d -> u) -> DoStmt -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DoStmt -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt | |
Show DoStmt | |
NFData DoStmt Source # | |
Defined in Agda.Syntax.Concrete | |
Eq DoStmt Source # | |
Constructors
OptionsPragma Range [String] | |
BuiltinPragma Range RString QName | |
RewritePragma Range Range [QName] | Second Range is for REWRITE keyword. |
ForeignPragma Range RString String | first string is backend name |
CompilePragma Range RString QName String | first string is backend name |
StaticPragma Range QName | |
InlinePragma Range Bool QName | INLINE or NOINLINE |
ImpossiblePragma Range [String] | Throws an internal error in the scope checker.
The |
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. |
DisplayPragma Range Pattern Expr | Display lhs as rhs (modifies the printer). |
CatchallPragma Range | Applies to the following function clause. |
TerminationCheckPragma Range (TerminationCheck Name) | Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block. |
NoCoverageCheckPragma Range | Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block. |
NoPositivityCheckPragma Range | Applies to the following data/record type or mutual block. |
PolarityPragma Range Name [Occurrence] | |
NoUniverseCheckPragma Range | Applies to the following data/record type. |
Instances
HasRange Pragma Source # | |
KillRange Pragma Source # | |
Defined in Agda.Syntax.Concrete Methods | |
ToAbstract Pragma Source # | |
Pretty Pragma Source # | |
Data Pragma Source # | |
Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma dataTypeOf :: Pragma -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma | |
Show Pragma | |
NFData Pragma Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Eq Pragma Source # | |
type AbsOfCon Pragma Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Modules: Top-level pragmas plus other top-level declarations.
Constructors
Mod | |
Fields
|
data ThingWithFixity x Source #
Decorating something with Fixity'
.
Constructors
ThingWithFixity x Fixity' |
Instances
Foldable ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity Methods fold :: Monoid m => ThingWithFixity m -> m foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a toList :: ThingWithFixity a -> [a] null :: ThingWithFixity a -> Bool length :: ThingWithFixity a -> Int elem :: Eq a => a -> ThingWithFixity a -> Bool maximum :: Ord a => ThingWithFixity a -> a minimum :: Ord a => ThingWithFixity a -> a sum :: Num a => ThingWithFixity a -> a product :: Num a => ThingWithFixity a -> a | |
Traversable ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) | |
Functor ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b (<$) :: a -> ThingWithFixity b -> ThingWithFixity a # | |
LensFixity (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' Fixity (ThingWithFixity a) Source # | |
LensFixity' (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' Fixity' (ThingWithFixity a) Source # | |
KillRange x => KillRange (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source # | |
Pretty (ThingWithFixity Name) Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source # | |
Data x => Data (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) toConstr :: ThingWithFixity x -> Constr dataTypeOf :: ThingWithFixity x -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) | |
Show x => Show (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS show :: ThingWithFixity x -> String showList :: [ThingWithFixity x] -> ShowS |
type HoleContent = HoleContent' () Name Pattern Expr Source #
data HoleContent' qn nm p e Source #
Extended content of an interaction hole.
Constructors
HoleContentExpr e | e |
HoleContentRewrite [RewriteEqn' qn nm p e] | (rewrite | invert) e0 | ... | en |
Instances
ToAbstract HoleContent Source # | Content of interaction hole. |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon HoleContent Source # Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source # | |
Foldable (HoleContent' qn nm p) Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => HoleContent' qn nm p m -> m foldMap :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m foldMap' :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m foldr :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b foldr' :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b foldl :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b foldl' :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b foldr1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a foldl1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a toList :: HoleContent' qn nm p a -> [a] null :: HoleContent' qn nm p a -> Bool length :: HoleContent' qn nm p a -> Int elem :: Eq a => a -> HoleContent' qn nm p a -> Bool maximum :: Ord a => HoleContent' qn nm p a -> a minimum :: Ord a => HoleContent' qn nm p a -> a sum :: Num a => HoleContent' qn nm p a -> a product :: Num a => HoleContent' qn nm p a -> a | |
Traversable (HoleContent' qn nm p) Source # | |
Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b) sequenceA :: Applicative f => HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a) mapM :: Monad m => (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b) sequence :: Monad m => HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a) | |
Functor (HoleContent' qn nm p) Source # | |
Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b (<$) :: a -> HoleContent' qn nm p b -> HoleContent' qn nm p a # | |
type AbsOfCon HoleContent Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
topLevelModuleName :: Module -> TopLevelModuleName Source #
Computes the top-level module name.
Precondition: The Declaration
has to be well-formed.
This means that there are only allowed declarations before the
first module declaration, typically import declarations.
See spanAllowedBeforeModule
.
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration]) Source #
Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.