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 (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]
- | ForeignPragma Range String String
- | CompilePragma Range String QName String
- | StaticPragma Range QName
- | InlinePragma Range Bool QName
- | 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.
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 (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
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 | |
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) 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) | |
Show a => Show (OpApp a) | |
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
isSingleIdentifierP :: Pattern -> Maybe Name Source #
Bindings
type LamBinding = LamBinding' TypedBinding Source #
A lambda binding is either domain free or typed.
data LamBinding' a Source #
Constructors
DomainFree (NamedArg BoundName) | . |
DomainFull a | . |
Instances
Functor LamBinding' Source # | |
Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b (<$) :: a -> LamBinding' b -> LamBinding' a # | |
Foldable LamBinding' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => LamBinding' m -> 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) | |
Pretty LamBinding Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source # | |
KillRange LamBinding Source # | |
Defined in Agda.Syntax.Concrete Methods | |
HasRange LamBinding Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source # | |
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 # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # | |
ToConcrete LamBinding LamBinding Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon LamBinding0 Source # bindToConcrete :: LamBinding -> (LamBinding0 -> AbsToCon b) -> AbsToCon b Source # | |
ToAbstract LamBinding LamBinding Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding Source # | |
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 :: (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) | |
Show (LamBinding' TypedBinding) | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding' TypedBinding -> ShowS show :: LamBinding' TypedBinding -> String showList :: [LamBinding' TypedBinding] -> ShowS | |
NFData a => NFData (LamBinding' a) Source # | |
Defined in Agda.Syntax.Concrete Methods rnf :: LamBinding' a -> () |
type TypedBinding = TypedBinding' Expr Source #
A typed binding.
data TypedBinding' e Source #
Constructors
TBind Range [NamedArg BoundName] e | Binding |
TLet Range [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
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 # | |
ToConcrete BindName BoundName Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
ToAbstract (NewName BoundName) BindName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
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.
Constructors
Instances
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.
The content of the as
-clause of the import statement.
Constructors
AsName | |
Instances
Functor AsName' Source # | |
Foldable AsName' Source # | |
Defined in Agda.Syntax.Concrete Methods 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 Methods | |
HasRange AsName Source # | |
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 :: (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
Eq OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete | |
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 :: (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 | |
Show OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> OpenShortHand -> ShowS show :: OpenShortHand -> String showList :: [OpenShortHand] -> ShowS | |
Pretty OpenShortHand Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source # |
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} |
EqualP Range [(Expr, Expr)] |
|
EllipsisP Range |
|
WithP Range Pattern |
|
Instances
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 :: (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 | |
Pretty Pattern Source # | |
KillRange Pattern Source # | |
Defined in Agda.Syntax.Concrete Methods | |
SetRange Pattern Source # | |
HasRange 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 # | |
IsWithP 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 # | |
IsExpr Pattern Source # | |
ToConcrete Pattern Pattern Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
ToConcrete LHSCore Pattern Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
ToAbstract Pattern (Pattern' Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
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 | |
Show 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 # | |
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) 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) | |
Show (RHS' Expr) | |
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
Functor WhereClause' Source # | |
Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b (<$) :: a -> WhereClause' b -> WhereClause' a # | |
Foldable WhereClause' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => WhereClause' m -> 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) | |
Pretty WhereClause Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |
KillRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods | |
HasRange WhereClause Source # | |
Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |
ToConcrete WhereDeclarations WhereClause Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause Source # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b Source # | |
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 :: (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) | |
Show (WhereClause' [Declaration]) | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause' [Declaration] -> ShowS show :: WhereClause' [Declaration] -> String showList :: [WhereClause' [Declaration]] -> ShowS | |
NFData a => NFData (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause' a -> () | |
Null (WhereClause' a) Source # | A |
Defined in Agda.Syntax.Concrete | |
ExprLike a => ExprLike (WhereClause' a) Source # | |
Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) Source # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m Source # |
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 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 | |
Show 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
OptionsPragma Range [String] | |
BuiltinPragma Range String QName | |
RewritePragma Range [QName] | |
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 |
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 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 :: (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
Functor ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b (<$) :: a -> ThingWithFixity b -> ThingWithFixity a # | |
Foldable ThingWithFixity Source # | |
Defined in Agda.Syntax.Fixity Methods fold :: Monoid m => ThingWithFixity m -> 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) | |
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 :: (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 | |
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 # | |
KillRange x => KillRange (ThingWithFixity x) Source # | |
Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source # |
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
Functor HoleContent' Source # | |
Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> HoleContent' a -> HoleContent' b (<$) :: a -> HoleContent' b -> HoleContent' a # | |
Foldable HoleContent' Source # | |
Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => HoleContent' m -> m foldMap :: Monoid m => (a -> m) -> HoleContent' a -> m foldr :: (a -> b -> b) -> b -> HoleContent' a -> b foldr' :: (a -> b -> b) -> b -> HoleContent' a -> b foldl :: (b -> a -> b) -> b -> HoleContent' a -> b foldl' :: (b -> a -> b) -> b -> HoleContent' a -> b foldr1 :: (a -> a -> a) -> HoleContent' a -> a foldl1 :: (a -> a -> a) -> HoleContent' a -> a toList :: HoleContent' a -> [a] null :: HoleContent' a -> Bool length :: HoleContent' a -> Int elem :: Eq a => a -> HoleContent' a -> Bool maximum :: Ord a => HoleContent' a -> a minimum :: Ord a => HoleContent' a -> a sum :: Num a => HoleContent' a -> a product :: Num a => HoleContent' a -> a | |
Traversable HoleContent' Source # | |
Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> HoleContent' a -> f (HoleContent' b) sequenceA :: Applicative f => HoleContent' (f a) -> f (HoleContent' a) mapM :: Monad m => (a -> m b) -> HoleContent' a -> m (HoleContent' b) sequence :: Monad m => HoleContent' (m a) -> m (HoleContent' a) | |
ToAbstract HoleContent HoleContent Source # | Content of interaction hole. |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods |
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.