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 Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe String)
- | RawApp Range [Expr]
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))]
- | WithApp Range Expr [Expr]
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range [LamBinding] Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range [LamClause]
- | Fun Range Expr Expr
- | Pi Telescope Expr
- | Set Range
- | Prop Range
- | SetN Range Integer
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range [Declaration] (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range Expr
- | DoBlock Range [DoStmt]
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | ETel Telescope
- | QuoteGoal Range Name Expr
- | QuoteContext Range
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr [Expr]
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
- data OpApp e
- = SyntaxBindingLambda Range [LamBinding] e
- | Ordinary e
- fromOrdinary :: e -> OpApp e -> e
- module Agda.Syntax.Concrete.Name
- appView :: Expr -> AppView
- data AppView = AppView Expr [NamedArg Expr]
- type LamBinding = LamBinding' TypedBindings
- data LamBinding' a
- type TypedBindings = TypedBindings' TypedBinding
- data TypedBindings' a = TypedBindings Range (Arg a)
- type TypedBinding = TypedBinding' Expr
- data TypedBinding' e
- = TBind Range [WithHiding BoundName] e
- | TLet Range [Declaration]
- type RecordAssignment = Either FieldAssignment ModuleAssignment
- type RecordAssignments = [RecordAssignment]
- type FieldAssignment = FieldAssignment' Expr
- data FieldAssignment' a = FieldAssignment {
- _nameFieldA :: Name
- _exprFieldA :: a
- nameFieldA :: Lens' Name (FieldAssignment' a)
- exprFieldA :: Lens' a (FieldAssignment' a)
- data ModuleAssignment = ModuleAssignment {}
- data BoundName = BName {
- boundName :: Name
- boundLabel :: Name
- bnameFixity :: Fixity'
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type Telescope = [TypedBindings]
- countTelVars :: Telescope -> Nat
- data Declaration
- = TypeSig ArgInfo Name Expr
- | Field IsInstance Name (Arg Expr)
- | FunClause LHS RHS WhereClause Bool
- | DataSig Range Induction Name [LamBinding] Expr
- | Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name [LamBinding] Expr
- | Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] (Maybe Expr) [Declaration]
- | Infix Fixity [Name]
- | Syntax Name Notation
- | PatternSyn Range Name [Arg Name] Pattern
- | Mutual Range [Declaration]
- | Abstract Range [Declaration]
- | Private Range Origin [Declaration]
- | InstanceB Range [Declaration]
- | Macro Range [Declaration]
- | Postulate Range [TypeSignatureOrInstanceBlock]
- | Primitive Range [TypeSignature]
- | Open Range QName ImportDirective
- | Import Range QName (Maybe AsName) !OpenShortHand ImportDirective
- | ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective
- | Module Range QName [TypedBindings] [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
- data AsName = AsName {}
- data OpenShortHand
- type RewriteEqn = Expr
- type WithExpr = Expr
- data LHS = LHS {}
- data Pattern
- = IdentP QName
- | QuoteP Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP Range [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 Literal
- | RecP Range [FieldAssignment' Pattern]
- | EllipsisP Range
- | WithP Range Pattern
- data LHSCore
- data LamClause = LamClause {
- lamLHS :: LHS
- lamRHS :: RHS
- lamWhere :: WhereClause
- 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 String QName
- | RewritePragma Range [QName]
- | CompiledDataPragma Range QName String [String]
- | CompiledTypePragma Range QName String
- | CompiledPragma Range QName String
- | CompiledExportPragma Range QName String
- | CompiledJSPragma Range QName String
- | CompiledUHCPragma Range QName String
- | CompiledDataUHCPragma Range QName String [String]
- | HaskellCodePragma Range String
- | ForeignPragma Range String String
- | CompilePragma Range String QName String
- | StaticPragma Range QName
- | InjectivePragma Range QName
- | InlinePragma Range Bool QName
- | ImportPragma Range String
- | ImportUHCPragma Range String
- | ImpossiblePragma Range
- | EtaPragma Range QName
- | TerminationCheckPragma Range (TerminationCheck Name)
- | WarningOnUsage Range QName String
- | CatchallPragma Range
- | DisplayPragma Range Pattern Expr
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
- type Module = ([Pragma], [Declaration])
- data ThingWithFixity x = ThingWithFixity x Fixity'
- type HoleContent = HoleContent' Expr
- data HoleContent' e
- = HoleContentExpr e
- | HoleContentRewrite [e]
- topLevelModuleName :: Module -> TopLevelModuleName
- spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
Expressions
Concrete expressions. Should represent exactly what the user wrote.
Ident QName | ex: |
Lit Literal | ex: |
QuestionMark Range (Maybe Nat) | ex: |
Underscore Range (Maybe String) | ex: |
RawApp Range [Expr] | before parsing operators |
App Range Expr (NamedArg Expr) | ex: |
OpApp Range QName (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))] | ex: |
WithApp Range Expr [Expr] | ex: |
HiddenArg Range (Named_ Expr) | ex: |
InstanceArg Range (Named_ Expr) | ex: |
Lam Range [LamBinding] Expr | ex: |
AbsurdLam Range Hiding | ex: |
ExtendedLam Range [LamClause] | ex: |
Fun Range Expr Expr | ex: |
Pi Telescope Expr | ex: |
Set Range | ex: |
Prop Range | ex: |
SetN Range Integer | ex: |
Rec Range RecordAssignments | ex: |
RecUpdate Range Expr [FieldAssignment] | ex: |
Let Range [Declaration] (Maybe Expr) | ex: |
Paren Range Expr | ex: |
IdiomBrackets Range Expr | ex: |
DoBlock Range [DoStmt] | ex: |
Absurd Range | ex: |
As Range Name Expr | ex: |
Dot Range Expr | ex: |
ETel Telescope | only used for printing telescopes |
QuoteGoal Range Name Expr | ex: |
QuoteContext Range | ex: |
Quote Range | ex: |
QuoteTerm Range | ex: |
Tactic Range Expr [Expr] | tactic solve | subgoal1 | .. | subgoalN |
Unquote Range | ex: |
DontCare Expr | to print irrelevant things |
Equal Range Expr Expr | ex: |
Ellipsis Range |
|
Instances
SyntaxBindingLambda Range [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 # 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 # minimum :: Ord a => OpApp a -> a # | |
Traversable OpApp Source # | |
Data e => Data (OpApp e) Source # | |
Defined in Agda.Syntax.Concrete gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpApp e -> c (OpApp e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e) # toConstr :: OpApp e -> Constr # dataTypeOf :: OpApp e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e)) # gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r # gmapQr :: (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) # | |
NFData a => NFData (OpApp a) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Pretty (OpApp Expr) Source # | |
KillRange e => KillRange (OpApp e) Source # | |
Defined in Agda.Syntax.Concrete killRange :: KillRangeT (OpApp e) Source # | |
HasRange e => HasRange (OpApp e) Source # | |
ExprLike a => ExprLike (OpApp a) Source # | |
fromOrdinary :: e -> OpApp e -> e Source #
module Agda.Syntax.Concrete.Name
Bindings
type LamBinding = LamBinding' TypedBindings Source #
A lambda binding is either domain free or typed.
data LamBinding' a Source #
DomainFree ArgInfo BoundName | . |
DomainFull a | . |
Instances
data TypedBindings' a Source #
TypedBindings Range (Arg a) | . |
Instances
type TypedBinding = TypedBinding' Expr Source #
A typed binding.
data TypedBinding' e Source #
TBind Range [WithHiding BoundName] e | Binding |
TLet Range [Declaration] | Let binding |
Instances
type RecordAssignments = [RecordAssignment] Source #
type FieldAssignment = FieldAssignment' Expr Source #
data FieldAssignment' a Source #
FieldAssignment | |
|
Instances
nameFieldA :: Lens' Name (FieldAssignment' a) Source #
exprFieldA :: Lens' a (FieldAssignment' a) Source #
data ModuleAssignment Source #
Instances
BName | |
|
Instances
Eq BoundName Source # | |
Data BoundName Source # | |
Defined in Agda.Syntax.Concrete 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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r # gmapQ :: (forall d. Data d => d -> u) -> BoundName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BoundName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # | |
Show BoundName Source # | |
NFData BoundName Source # | |
Defined in Agda.Syntax.Concrete | |
Pretty BoundName Source # | |
KillRange BoundName Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange BoundName Source # | |
ToAbstract (NewName BoundName) Name Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
mkBoundName_ :: Name -> BoundName Source #
type Telescope = [TypedBindings] Source #
A telescope is a sequence of typed bindings. Bound variables are in scope in later types.
countTelVars :: Telescope -> Nat Source #
Declarations
data Declaration Source #
The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.
Instances
data ModuleApplication Source #
SectionApp Range [TypedBindings] Expr | tel. M args |
RecordModuleIFS 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.
Instances
Data AsName Source # | |
Defined in Agda.Syntax.Concrete gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AsName -> c AsName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AsName # toConstr :: AsName -> Constr # dataTypeOf :: AsName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AsName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AsName) # gmapT :: (forall b. Data b => b -> b) -> AsName -> AsName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AsName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AsName -> r # gmapQ :: (forall d. Data d => d -> u) -> AsName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AsName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AsName -> m AsName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName -> m AsName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName -> m AsName # | |
Show AsName Source # | |
NFData AsName Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
KillRange AsName Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange AsName Source # | |
data OpenShortHand Source #
Instances
type RewriteEqn = 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
Data LHS Source # | |
Defined in Agda.Syntax.Concrete 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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS # | |
Show LHS Source # | |
NFData LHS Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Pretty LHS Source # | |
KillRange LHS Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange LHS Source # | |
HasEllipsis LHS Source # | Does the lhs contain an ellipsis? |
Defined in Agda.Syntax.Concrete.Pattern hasEllipsis :: LHS -> Bool Source # | |
ExprLike LHS Source # | |
ToConcrete LHS LHS Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
ToConcrete SpineLHS LHS Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
Concrete patterns. No literals in patterns at the moment.
IdentP QName |
|
QuoteP Range | quote |
AppP Pattern (NamedArg Pattern) |
|
RawAppP Range [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 Literal |
|
RecP Range [FieldAssignment' Pattern] | record {x = p; y = q} |
EllipsisP Range |
|
WithP Range Pattern |
|
Instances
Processed (operator-parsed) intermediate form of the core f ps
of LHS
.
Corresponds to lhsOriginalPattern
.
LamClause | |
|
Instances
Data LamClause Source # | |
Defined in Agda.Syntax.Concrete 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 :: (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 # | |
NFData LamClause Source # | |
Defined in Agda.Syntax.Concrete | |
Pretty LamClause Source # | |
KillRange LamClause Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange LamClause Source # | |
ExprLike LamClause Source # | |
Instances
Functor RHS' Source # | |
Show RHS Source # | |
Foldable RHS' Source # | |
Defined in Agda.Syntax.Concrete fold :: Monoid m => RHS' m -> 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 # | |
Pretty RHS Source # | |
KillRange RHS Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange RHS Source # | |
ToAbstract RHS AbstractRHS Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract toAbstract :: RHS -> ScopeM AbstractRHS Source # | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source # | |
Data e => Data (RHS' e) Source # | |
Defined in Agda.Syntax.Concrete gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS' e -> c (RHS' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e) # toConstr :: RHS' e -> Constr # dataTypeOf :: RHS' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e)) # gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r # gmapQr :: (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 | |
ExprLike a => ExprLike (RHS' a) Source # | |
type WhereClause = WhereClause' [Declaration] Source #
data WhereClause' decls Source #
NoWhere | No |
AnyWhere decls | Ordinary |
SomeWhere Name Access decls | Named where: |
Instances
An expression followed by a where clause. Currently only used to give better a better error message in interaction.
Instances
Data DoStmt Source # | |
Defined in Agda.Syntax.Concrete gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoStmt -> c DoStmt # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoStmt # toConstr :: DoStmt -> Constr # dataTypeOf :: DoStmt -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoStmt) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoStmt) # gmapT :: (forall b. Data b => b -> b) -> DoStmt -> DoStmt # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r # gmapQr :: (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 # | |
NFData DoStmt Source # | |
Defined in Agda.Syntax.Concrete | |
Pretty DoStmt Source # | |
KillRange DoStmt Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange DoStmt Source # | |
ExprLike DoStmt Source # | |
Instances
Data Pragma Source # | |
Defined in Agda.Syntax.Concrete gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma # toConstr :: Pragma -> Constr # dataTypeOf :: Pragma -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) # gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # | |
Show Pragma Source # | |
NFData Pragma Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Pretty Pragma Source # | |
KillRange Pragma Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange Pragma Source # | |
ToConcrete RangeAndPragma Pragma Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete toConcrete :: RangeAndPragma -> AbsToCon Pragma Source # bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b Source # | |
ToAbstract Pragma [Pragma] Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
type Module = ([Pragma], [Declaration]) Source #
Modules: Top-level pragmas plus other top-level declarations.
data ThingWithFixity x Source #
Decorating something with Fixity'
.
Instances
type HoleContent = HoleContent' Expr Source #
data HoleContent' e Source #
Extended content of an interaction hole.
HoleContentExpr e | e |
HoleContentRewrite [e] | rewrite e0 | ... | en |
Instances
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.