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 (Arg Expr) Expr
- | Pi Telescope Expr
- | Set Range
- | Prop Range
- | SetN Range Integer
- | PropN 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
- | Generalized Expr
- 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]
- isSingleIdentifierP :: Pattern -> Maybe Name
- removeSingletonRawAppP :: Pattern -> Pattern
- type LamBinding = LamBinding' TypedBinding
- data LamBinding' a
- = DomainFree (NamedArg BoundName)
- | DomainFull a
- 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 {
- boundName :: Name
- bnameFixity :: Fixity'
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type Telescope = [TypedBinding]
- countTelVars :: Telescope -> Nat
- lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
- makePi :: Telescope -> Expr -> Expr
- data Declaration
- = TypeSig ArgInfo Name Expr
- | Generalize Range [TypeSignature]
- | Field IsInstance Name (Arg Expr)
- | FunClause LHS RHS WhereClause Bool
- | DataSig Range Induction Name [LamBinding] Expr
- | Data Range Induction Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
- | DataDef Range Induction Name [LamBinding] [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name [LamBinding] Expr
- | RecordDef Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
- | Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] 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 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
- data AsName' a = AsName {}
- type AsName = AsName' (Either Expr Name)
- 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]
- | EqualP Range [(Expr, Expr)]
- | 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
- | InlinePragma Range Bool QName
- | ImportPragma Range String
- | ImportUHCPragma Range String
- | ImpossiblePragma Range
- | EtaPragma Range QName
- | WarningOnUsage Range QName String
- | InjectivePragma Range QName
- | DisplayPragma Range Pattern Expr
- | CatchallPragma Range
- | TerminationCheckPragma Range (TerminationCheck Name)
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
- | NoUniverseCheckPragma Range
- 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 (Arg Expr) Expr | ex: |
Pi Telescope Expr | ex: |
Set Range | ex: |
Prop Range | ex: |
SetN Range Integer | ex: |
PropN 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 |
|
Generalized Expr |
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' TypedBinding Source #
A lambda binding is either domain free or typed.
data LamBinding' a Source #
DomainFree (NamedArg BoundName) | . |
DomainFull a | . |
Instances
type TypedBinding = TypedBinding' Expr Source #
A typed binding.
data TypedBinding' e Source #
TBind Range [NamedArg 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
mkBoundName_ :: Name -> BoundName Source #
type Telescope = [TypedBinding] Source #
A telescope is a sequence of typed bindings. Bound variables are in scope in later types.
countTelVars :: Telescope -> Nat Source #
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
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 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.
The content of the as
-clause of the import statement.
Instances
Functor AsName' Source # | |
Foldable AsName' Source # | |
Defined in Agda.Syntax.Concrete fold :: Monoid m => AsName' m -> m # foldMap :: Monoid m => (a -> m) -> AsName' a -> m # 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 # | |
NFData AsName Source # | Ranges are not forced. |
Defined in Agda.Syntax.Concrete | |
KillRange AsName Source # | |
Defined in Agda.Syntax.Concrete | |
HasRange AsName Source # | |
Data a => Data (AsName' a) Source # | |
Defined in Agda.Syntax.Concrete 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 :: (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 # | |
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} |
EqualP Range [(Expr, Expr)] |
|
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 # | |
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 | first string is backend name |
CompilePragma Range String QName String | first string is backend name |
StaticPragma Range QName | |
InlinePragma Range Bool QName | INLINE or NOINLINE |
ImportPragma Range String | Invariant: The string must be a valid Haskell module name. |
ImportUHCPragma Range String | same as above, but for the UHC backend |
ImpossiblePragma Range | Throws an internal error in the scope checker. |
EtaPragma Range QName | For coinductive records, use pragma instead of regular
|
WarningOnUsage Range QName String | Applies to the named function |
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. |
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
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.