Safe Haskell | None |
---|---|
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 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.
Constructors
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
Constructors
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 Methods 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 Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpApp e -> c (OpApp e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e) # toConstr :: OpApp e -> Constr # dataTypeOf :: OpApp e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e)) # gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r # gmapQr :: (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 Methods 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 #
Constructors
DomainFree ArgInfo BoundName | . |
DomainFull a | . |
Instances
data TypedBindings' a Source #
Constructors
TypedBindings Range (Arg a) | . |
Instances
type TypedBinding = TypedBinding' Expr Source #
A typed binding.
data TypedBinding' e Source #
Constructors
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 #
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
Eq 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 :: (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 Methods | |
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.
Constructors
Instances
data ModuleApplication Source #
Constructors
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.
Constructors
AsName | |
Instances
Data AsName 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 -> 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 Methods | |
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.
Constructors
LHS | Original pattern (including with-patterns), rewrite equations and with-expressions. |
Fields
|
Instances
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 :: (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 | |
Pretty LHS Source # | |
KillRange LHS Source # | |
Defined in Agda.Syntax.Concrete Methods | |
HasRange LHS Source # | |
HasEllipsis LHS Source # | Does the lhs contain an ellipsis? |
Defined in Agda.Syntax.Concrete.Pattern Methods 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.
Constructors
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
.
Constructors
LamClause | |
Fields
|
Instances
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 :: (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 Methods | |
HasRange LamClause Source # | |
ExprLike LamClause Source # | |
Instances
Functor RHS' Source # | |
Show RHS # | |
Foldable RHS' Source # | |
Defined in Agda.Syntax.Concrete Methods 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 Methods | |
HasRange RHS Source # | |
ToAbstract RHS AbstractRHS Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS Source # | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods 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 Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS' e -> c (RHS' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e) # toConstr :: RHS' e -> Constr # dataTypeOf :: RHS' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e)) # gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r # gmapQr :: (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 #
Constructors
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.
Constructors
ExprWhere Expr WhereClause |
Constructors
DoBind Range Pattern Expr [LamClause] | p ← e where cs |
DoThen Expr | |
DoLet Range [Declaration] |
Instances
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 # 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 Methods | |
HasRange DoStmt Source # | |
ExprLike DoStmt Source # | |
Constructors
Instances
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 # 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 # | |
NFData Pragma Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
Pretty Pragma Source # | |
KillRange Pragma Source # | |
Defined in Agda.Syntax.Concrete Methods | |
HasRange Pragma Source # | |
ToConcrete RangeAndPragma Pragma Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods 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'
.
Constructors
ThingWithFixity x Fixity' |
Instances
type HoleContent = HoleContent' Expr Source #
data HoleContent' e Source #
Extended content of an interaction hole.
Constructors
HoleContentExpr e | e |
HoleContentRewrite [e] | rewrite e0 | ... | en |
Instances
topLevelModuleName :: Module -> TopLevelModuleName Source #
Computes the top-level module name.
Precondition: The Module
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.