Agda.Syntax.Concrete

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.

Expressions

data Expr

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName

ex: x

Lit Range Literal

ex: 1 or "foo"

QuestionMark Range (Maybe Nat)

ex: ? or {! ... !}

Underscore Range (Maybe String)

ex: _ or _A_5

RawApp Range (List2 Expr)

before parsing operators

App Range Expr (NamedArg Expr)

ex: e e, e {e}, or e {x = e}

OpApp Range QName (Set Name) OpAppArgs

ex: e + e The QName is possibly ambiguous, but it must correspond to one of the names in the set.

WithApp Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg Range (Named_ Expr)

ex: {e} or {x=e}

InstanceArg Range (Named_ Expr)

ex: {{e}} or {{x=e}}

Lam Range (List1 LamBinding) Expr

ex: \x {y} -> e or \(x:A){y:B} -> e

AbsurdLam Range Hiding

ex: \ ()

ExtendedLam Range Erased (List1 LamClause)

ex: \ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }

Fun Range (Arg Expr) Expr

ex: e -> e or .e -> e (NYI: {e} -> e)

Pi Telescope1 Expr

ex: (xs:e) -> e or {xs:e} -> e

Rec Range RecordAssignments

ex: record {x = a; y = b}, or record { x = a; M1; M2 }

RecUpdate Range Expr [FieldAssignment]

ex: record e {x = a; y = b}

Let Range (List1 Declaration) (Maybe Expr)

ex: let Ds in e, missing body when parsing do-notation let

Paren Range Expr

ex: (e)

IdiomBrackets Range [Expr]

ex: (| e1 | e2 | .. | en |) or (|)

DoBlock Range (List1 DoStmt)

ex: do x <- m1; m2

Absurd Range

ex: () or {}, only in patterns

As Range Name Expr

ex: x@p, only in patterns

Dot Range Expr

ex: .p, only in patterns

DoubleDot Range Expr

ex: ..A, used for parsing ..A -> B

Quote Range

ex: quote, should be applied to a name

QuoteTerm Range

ex: quoteTerm, should be applied to a term

Tactic Range Expr

ex: @(tactic t), used to declare tactic arguments

Unquote Range

ex: unquote, should be applied to a term of type Term

DontCare Expr

to print irrelevant things

Equal Range Expr Expr

ex: a = b, used internally in the parser

Ellipsis Range

..., used internally to parse patterns.

KnownIdent NameKind QName

An identifier coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).

KnownOpApp NameKind Range QName (Set Name) OpAppArgs

An operator application coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).

Generalized Expr

Instances

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

LensHiding TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: TypedBinding -> Hiding

setHiding :: Hiding -> TypedBinding -> TypedBinding

mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding

LensRelevance TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRelevance :: TypedBinding -> Relevance

setRelevance :: Relevance -> TypedBinding -> TypedBinding

mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding

Pretty Expr

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc

prettyPrec :: Int -> Expr -> Doc

prettyList :: [Expr] -> Doc

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

Pretty TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

ExprLike Expr

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Expr -> Expr

foldExpr :: Monoid m => (Expr -> m) -> Expr -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr

ExprLike FieldAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

IsExpr Expr

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

exprView :: Expr -> ExprView Expr

unExprView :: ExprView Expr -> Expr

patternView :: Expr -> Maybe Pattern

HasRange AsName

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range

HasRange Expr

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

HasRange RHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range

KillRange AsName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT AsName

KillRange Expr

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Expr

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

KillRange RHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RHS

KillRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBinding

SetRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBinding -> TypedBinding

ToAbstract Expr

Scope check an expression.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr

Methods

toAbstract :: Expr -> ScopeM (AbsOfCon Expr)

ToAbstract HoleContent

Content of interaction hole.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent)

ToAbstract LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding

Methods

toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding)

ToAbstract RHS

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS

Methods

toAbstract :: RHS -> ScopeM (AbsOfCon RHS)

ToAbstract RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn

Methods

toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn)

ToAbstract TypedBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding)

Show Expr

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Show LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

Show TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

NFData AsName

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

NFData Expr

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: Expr -> ()

Eq Expr

Defined in Agda.Syntax.Concrete

Methods

(==) :: Expr -> Expr -> Bool

(/=) :: Expr -> Expr -> Bool

Pretty (OpApp Expr)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpApp Expr -> Doc

prettyPrec :: Int -> OpApp Expr -> Doc

prettyList :: [OpApp Expr] -> Doc

ToAbstract (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr)

Methods

toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr))

ToAbstract (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr)

Methods

toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr))

EncodeTCM (OutputForm Expr Expr)

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: OutputForm Expr Expr -> TCM Value

type AbsOfCon Expr

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Expr = Expr

type AbsOfCon HoleContent

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent = HoleContent

type AbsOfCon LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding = Maybe LamBinding

type AbsOfCon RHS

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RHS = AbstractRHS

type AbsOfCon RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

type AbsOfCon TypedBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding = Maybe TypedBinding

type AbsOfCon (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

type AbsOfCon (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Pattern' Expr) = Pattern' Expr

data OpApp e

Constructors

SyntaxBindingLambda Range (List1 LamBinding) e

An abstraction inside a special syntax declaration (see Issue 358 why we introduce this).

Ordinary e

Instances

Foldable OpApp

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => OpApp m -> m

foldMap :: Monoid m => (a -> m) -> OpApp a -> m

foldMap' :: Monoid m => (a -> m) -> OpApp a -> m

foldr :: (a -> b -> b) -> b -> OpApp a -> b

foldr' :: (a -> b -> b) -> b -> OpApp a -> b

foldl :: (b -> a -> b) -> b -> OpApp a -> b

foldl' :: (b -> a -> b) -> b -> OpApp a -> b

foldr1 :: (a -> a -> a) -> OpApp a -> a

foldl1 :: (a -> a -> a) -> OpApp a -> a

toList :: OpApp a -> [a]

null :: OpApp a -> Bool

length :: OpApp a -> Int

elem :: Eq a => a -> OpApp a -> Bool

maximum :: Ord a => OpApp a -> a

minimum :: Ord a => OpApp a -> a

sum :: Num a => OpApp a -> a

product :: Num a => OpApp a -> a

Traversable OpApp

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> OpApp a -> f (OpApp b)

sequenceA :: Applicative f => OpApp (f a) -> f (OpApp a)

mapM :: Monad m => (a -> m b) -> OpApp a -> m (OpApp b)

sequence :: Monad m => OpApp (m a) -> m (OpApp a)

Functor OpApp

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> OpApp a -> OpApp b

(<$) :: a -> OpApp b -> OpApp a

Pretty (OpApp Expr)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpApp Expr -> Doc

prettyPrec :: Int -> OpApp Expr -> Doc

prettyList :: [OpApp Expr] -> Doc

ExprLike a => ExprLike (OpApp a)

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a

foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a)

HasRange e => HasRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range

KillRange e => KillRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (OpApp e)

Show a => Show (OpApp a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> OpApp a -> ShowS

show :: OpApp a -> String

showList :: [OpApp a] -> ShowS

NFData a => NFData (OpApp a)

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpApp a -> ()

Eq e => Eq (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

(==) :: OpApp e -> OpApp e -> Bool

(/=) :: OpApp e -> OpApp e -> Bool

fromOrdinary :: e -> OpApp e -> e

type OpAppArgs = OpAppArgs' Expr

type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))]

module Agda.Syntax.Concrete.Name

data AppView

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr]

appView :: Expr -> AppView

unAppView :: AppView -> Expr

rawApp :: List1 Expr -> Expr

rawAppP :: List1 Pattern -> Pattern

isSingleIdentifierP :: Pattern -> Maybe Name

removeParenP :: Pattern -> Pattern

isPattern :: Expr -> Maybe Pattern

Turn an expression into a pattern. Fails if the expression is not a valid pattern.

isAbsurdP :: Pattern -> Maybe (Range, Hiding)

isBinderP :: Pattern -> Maybe Binder

observeHiding :: Expr -> WithHiding Expr

Observe the hiding status of an expression

observeRelevance :: Expr -> (Relevance, Expr)

Observe the relevance status of an expression

observeModifiers :: Expr -> Arg Expr

Observe various modifiers applied to an expression

exprToPatternWithHoles :: Expr -> Pattern

Turn an expression into a pattern, turning non-pattern subexpressions into WildP.

returnExpr :: Expr -> Maybe Expr

Bindings

data Binder' a

A Binder x@p, the pattern is optional

Constructors

Binder

Fields

• binderPattern :: Maybe Pattern
• binderName :: a

Instances

HasRange Binder

Defined in Agda.Syntax.Concrete

Methods

getRange :: Binder -> Range

KillRange Binder

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Binder

Foldable Binder'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => Binder' m -> m

foldMap :: Monoid m => (a -> m) -> Binder' a -> m

foldMap' :: Monoid m => (a -> m) -> Binder' a -> m

foldr :: (a -> b -> b) -> b -> Binder' a -> b

foldr' :: (a -> b -> b) -> b -> Binder' a -> b

foldl :: (b -> a -> b) -> b -> Binder' a -> b

foldl' :: (b -> a -> b) -> b -> Binder' a -> b

foldr1 :: (a -> a -> a) -> Binder' a -> a

foldl1 :: (a -> a -> a) -> Binder' a -> a

toList :: Binder' a -> [a]

null :: Binder' a -> Bool

length :: Binder' a -> Int

elem :: Eq a => a -> Binder' a -> Bool

maximum :: Ord a => Binder' a -> a

minimum :: Ord a => Binder' a -> a

sum :: Num a => Binder' a -> a

product :: Num a => Binder' a -> a

Traversable Binder'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b)

sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a)

mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b)

sequence :: Monad m => Binder' (m a) -> m (Binder' a)

Functor Binder'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> Binder' a -> Binder' b

(<$) :: a -> Binder' b -> Binder' a

NFData Binder

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> ()

Pretty a => Pretty (Binder' a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Binder' a -> Doc

prettyPrec :: Int -> Binder' a -> Doc

prettyList :: [Binder' a] -> Doc

ToAbstract (Binder' (NewName BoundName))

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName))

Methods

toAbstract :: Binder' (NewName BoundName) -> ScopeM (AbsOfCon (Binder' (NewName BoundName)))

Show a => Show (Binder' a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Binder' a -> ShowS

show :: Binder' a -> String

showList :: [Binder' a] -> ShowS

Eq a => Eq (Binder' a)

Defined in Agda.Syntax.Concrete

Methods

(==) :: Binder' a -> Binder' a -> Bool

(/=) :: Binder' a -> Binder' a -> Bool

type AbsOfCon (Binder' (NewName BoundName))

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Binder' (NewName BoundName)) = Binder

type Binder = Binder' BoundName

mkBinder_ :: Name -> Binder

mkBinder :: a -> Binder' a

type LamBinding = LamBinding' TypedBinding

A lambda binding is either domain free or typed.

data LamBinding' a

Constructors

DomainFree (NamedArg Binder)

. x or {x} or .x or .{x} or {.x} or x@p or (p)

DomainFull a

. (xs : e) or {xs : e}

Instances

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

ToAbstract LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding

Methods

toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding)

Foldable LamBinding'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => LamBinding' m -> m

foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m

foldMap' :: Monoid m => (a -> m) -> LamBinding' a -> m

foldr :: (a -> b -> b) -> b -> LamBinding' a -> b

foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b

foldl :: (b -> a -> b) -> b -> LamBinding' a -> b

foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b

foldr1 :: (a -> a -> a) -> LamBinding' a -> a

foldl1 :: (a -> a -> a) -> LamBinding' a -> a

toList :: LamBinding' a -> [a]

null :: LamBinding' a -> Bool

length :: LamBinding' a -> Int

elem :: Eq a => a -> LamBinding' a -> Bool

maximum :: Ord a => LamBinding' a -> a

minimum :: Ord a => LamBinding' a -> a

sum :: Num a => LamBinding' a -> a

product :: Num a => LamBinding' a -> a

Traversable LamBinding'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b)

sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a)

mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b)

sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a)

Functor LamBinding'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> LamBinding' a -> LamBinding' b

(<$) :: a -> LamBinding' b -> LamBinding' a

Show LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

NFData a => NFData (LamBinding' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamBinding' a -> ()

Eq a => Eq (LamBinding' a)

Defined in Agda.Syntax.Concrete

Methods

(==) :: LamBinding' a -> LamBinding' a -> Bool

(/=) :: LamBinding' a -> LamBinding' a -> Bool

type AbsOfCon LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding = Maybe LamBinding

dropTypeAndModality :: LamBinding -> [LamBinding]

Drop type annotations and lets from bindings.

type TypedBinding = TypedBinding' Expr

A typed binding.

data TypedBinding' e

Constructors

TBind Range (List1 (NamedArg Binder)) e

Binding (x1@p1 ... xn@pn : A).

TLet Range (List1 Declaration)

Let binding (let Ds) or (open M args).

Instances

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

LensHiding TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: TypedBinding -> Hiding

setHiding :: Hiding -> TypedBinding -> TypedBinding

mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding

LensRelevance TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRelevance :: TypedBinding -> Relevance

setRelevance :: Relevance -> TypedBinding -> TypedBinding

mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

KillRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBinding

SetRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBinding -> TypedBinding

ToAbstract LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding

Methods

toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding)

ToAbstract TypedBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding)

Foldable TypedBinding'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => TypedBinding' m -> m

foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m

foldMap' :: Monoid m => (a -> m) -> TypedBinding' a -> m

foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b

foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b

foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b

foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b

foldr1 :: (a -> a -> a) -> TypedBinding' a -> a

foldl1 :: (a -> a -> a) -> TypedBinding' a -> a

toList :: TypedBinding' a -> [a]

null :: TypedBinding' a -> Bool

length :: TypedBinding' a -> Int

elem :: Eq a => a -> TypedBinding' a -> Bool

maximum :: Ord a => TypedBinding' a -> a

minimum :: Ord a => TypedBinding' a -> a

sum :: Num a => TypedBinding' a -> a

product :: Num a => TypedBinding' a -> a

Traversable TypedBinding'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b)

sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a)

mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b)

sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a)

Functor TypedBinding'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b

(<$) :: a -> TypedBinding' b -> TypedBinding' a

Show LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

ExprLike a => ExprLike (TypedBinding' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a

foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a)

NFData a => NFData (TypedBinding' a)

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: TypedBinding' a -> ()

Eq e => Eq (TypedBinding' e)

Defined in Agda.Syntax.Concrete

Methods

(==) :: TypedBinding' e -> TypedBinding' e -> Bool

(/=) :: TypedBinding' e -> TypedBinding' e -> Bool

type AbsOfCon LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding = Maybe LamBinding

type AbsOfCon TypedBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding = Maybe TypedBinding

type RecordAssignment = Either FieldAssignment ModuleAssignment

type RecordAssignments = [RecordAssignment]

type FieldAssignment = FieldAssignment' Expr

data FieldAssignment' a

Constructors

FieldAssignment

Fields

• _nameFieldA :: Name
• _exprFieldA :: a

Instances

ExprLike FieldAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment

Foldable FieldAssignment'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => FieldAssignment' m -> m

foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m

foldMap' :: Monoid m => (a -> m) -> FieldAssignment' a -> m

foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b

foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b

foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b

foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b

foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a

foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a

toList :: FieldAssignment' a -> [a]

null :: FieldAssignment' a -> Bool

length :: FieldAssignment' a -> Int

elem :: Eq a => a -> FieldAssignment' a -> Bool

maximum :: Ord a => FieldAssignment' a -> a

minimum :: Ord a => FieldAssignment' a -> a

sum :: Num a => FieldAssignment' a -> a

product :: Num a => FieldAssignment' a -> a

Traversable FieldAssignment'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)

sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a)

mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)

sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a)

Functor FieldAssignment'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b

(<$) :: a -> FieldAssignment' b -> FieldAssignment' a

SubstExpr a => SubstExpr (FieldAssignment' a)

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a

APatternLike a => APatternLike (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (FieldAssignment' a)

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (FieldAssignment' a)) -> m -> m) -> FieldAssignment' a -> m

traverseAPatternM :: Monad m => (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> FieldAssignment' a -> m (FieldAssignment' a)

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a

DeclaredNames a => DeclaredNames (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => FieldAssignment' a -> m

ExprLike a => ExprLike (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (FieldAssignment' a)

foldExpr :: FoldExprFn m (FieldAssignment' a)

traverseExpr :: TraverseExprFn m (FieldAssignment' a)

mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a

Pretty a => Pretty (FieldAssignment' a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: FieldAssignment' a -> Doc

prettyPrec :: Int -> FieldAssignment' a -> Doc

prettyList :: [FieldAssignment' a] -> Doc

CPatternLike p => CPatternLike (FieldAssignment' p)

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p)

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p)

NamesIn a => NamesIn (FieldAssignment' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FieldAssignment' a -> m

HasRange a => HasRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

getRange :: FieldAssignment' a -> Range

KillRange a => KillRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (FieldAssignment' a)

ToConcrete a => ToConcrete (FieldAssignment' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a)

Methods

toConcrete :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a))

bindToConcrete :: FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> AbsToCon b) -> AbsToCon b

ToAbstract c => ToAbstract (FieldAssignment' c)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (FieldAssignment' c)

Methods

toAbstract :: FieldAssignment' c -> ScopeM (AbsOfCon (FieldAssignment' c))

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a)

EmbPrj a => EmbPrj (FieldAssignment' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FieldAssignment' a -> S Int32

icod_ :: FieldAssignment' a -> S Int32

value :: Int32 -> R (FieldAssignment' a)

Show a => Show (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> FieldAssignment' a -> ShowS

show :: FieldAssignment' a -> String

showList :: [FieldAssignment' a] -> ShowS

NFData a => NFData (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: FieldAssignment' a -> ()

Eq a => Eq (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

(==) :: FieldAssignment' a -> FieldAssignment' a -> Bool

(/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool

type ADotT (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (FieldAssignment' a) = ADotT a

type ConOfAbs (FieldAssignment' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (FieldAssignment' a) = FieldAssignment' (ConOfAbs a)

type AbsOfCon (FieldAssignment' c)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (FieldAssignment' c) = FieldAssignment' (AbsOfCon c)

nameFieldA :: Lens' (FieldAssignment' a) Name

exprFieldA :: Lens' (FieldAssignment' a) a

data ModuleAssignment

Constructors

ModuleAssignment

Fields

• _qnameModA :: QName
• _exprModA :: [Expr]
• _importDirModA :: ImportDirective

Instances

Pretty ModuleAssignment

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleAssignment -> Doc

prettyPrec :: Int -> ModuleAssignment -> Doc

prettyList :: [ModuleAssignment] -> Doc

ExprLike ModuleAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment

foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment

HasRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleAssignment -> Range

KillRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleAssignment

ToAbstract ModuleAssignment

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon ModuleAssignment

Methods

toAbstract :: ModuleAssignment -> ScopeM (AbsOfCon ModuleAssignment)

Show ModuleAssignment

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ModuleAssignment -> ShowS

show :: ModuleAssignment -> String

showList :: [ModuleAssignment] -> ShowS

NFData ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleAssignment -> ()

Eq ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

(==) :: ModuleAssignment -> ModuleAssignment -> Bool

(/=) :: ModuleAssignment -> ModuleAssignment -> Bool

type AbsOfCon ModuleAssignment

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon ModuleAssignment = (ModuleName, Maybe LetBinding)

data BoundName

Constructors

BName

Fields

• boundName :: Name
• bnameFixity :: Fixity'
• bnameTactic :: TacticAttribute
• bnameIsFinite :: Bool

Instances

Pretty BoundName

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: BoundName -> Doc

prettyPrec :: Int -> BoundName -> Doc

prettyList :: [BoundName] -> Doc

HasRange Binder

Defined in Agda.Syntax.Concrete

Methods

getRange :: Binder -> Range

HasRange BoundName

Defined in Agda.Syntax.Concrete

Methods

getRange :: BoundName -> Range

KillRange Binder

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Binder

KillRange BoundName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT BoundName

Show BoundName

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> BoundName -> ShowS

show :: BoundName -> String

showList :: [BoundName] -> ShowS

NFData Binder

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> ()

NFData BoundName

Defined in Agda.Syntax.Concrete

Methods

rnf :: BoundName -> ()

Eq BoundName

Defined in Agda.Syntax.Concrete

Methods

(==) :: BoundName -> BoundName -> Bool

(/=) :: BoundName -> BoundName -> Bool

ToAbstract (Binder' (NewName BoundName))

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName))

Methods

toAbstract :: Binder' (NewName BoundName) -> ScopeM (AbsOfCon (Binder' (NewName BoundName)))

ToAbstract (NewName BoundName)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName)

Methods

toAbstract :: NewName BoundName -> ScopeM (AbsOfCon (NewName BoundName))

type AbsOfCon (Binder' (NewName BoundName))

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Binder' (NewName BoundName)) = Binder

type AbsOfCon (NewName BoundName)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName BoundName) = BindName

mkBoundName_ :: Name -> BoundName

mkBoundName :: Name -> Fixity' -> BoundName

type TacticAttribute = Maybe (Ranged Expr)

type Telescope = [TypedBinding]

type Telescope1 = List1 TypedBinding

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.

lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope

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

Smart constructor for Pi: check whether the Telescope is empty

mkLam :: Range -> [LamBinding] -> Expr -> Expr

Smart constructor for Lam: check for non-zero bindings.

mkLet :: Range -> [Declaration] -> Expr -> Expr

Smart constructor for Let: check for non-zero let bindings.

mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e)

Smart constructor for TLet: check for non-zero let bindings.

Declarations

data Declaration

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.

Constructors

TypeSig ArgInfo TacticAttribute Name Expr

Axioms and functions can be irrelevant. (Hiding should be NotHidden)

FieldSig IsInstance TacticAttribute Name (Arg Expr)

Generalize Range [TypeSignature]

Variables to be generalized, can be hidden and/or irrelevant.

Field Range [FieldSignature]

FunClause LHS RHS WhereClause Bool

DataSig Range Erased Name [LamBinding] Expr

lone data signature in mutual block

Data Range Erased Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]

DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]

RecordSig Range Erased Name [LamBinding] Expr

lone record signature in mutual block

RecordDef Range Name RecordDirectives [LamBinding] [Declaration]

Record Range Erased Name RecordDirectives [LamBinding] Expr [Declaration]

RecordDirective RecordDirective

Should not survive beyond the parser

Infix Fixity (List1 Name)

Syntax Name Notation

notation declaration for a name

PatternSyn Range Name [Arg Name] Pattern

Mutual Range [Declaration]

InterleavedMutual Range [Declaration]

Abstract Range [Declaration]

Private Range Origin [Declaration]

In Agda.Syntax.Concrete.Definitions we generate private blocks temporarily, which should be treated different that user-declared private blocks. Thus the Origin.

InstanceB Range [Declaration]

The Range' here (exceptionally) only refers to the range of the instance keyword. The range of the whole block InstanceB r ds is fuseRange r ds.

LoneConstructor Range [Declaration]

Macro Range [Declaration]

Postulate Range [TypeSignatureOrInstanceBlock]

Primitive Range [TypeSignature]

Open Range QName ImportDirective

Import Range QName (Maybe AsName) !OpenShortHand ImportDirective

ModuleMacro Range Erased Name ModuleApplication !OpenShortHand ImportDirective

Module Range Erased QName Telescope [Declaration]

UnquoteDecl Range [Name] Expr

unquoteDecl xs = e

UnquoteDef Range [Name] Expr

unquoteDef xs = e

UnquoteData Range Name [Name] Expr

unquoteDecl data d constructor xs = e

Pragma Pragma

Opaque Range [Declaration]

opaque ...

Unfolding Range [QName]

unfolding ...

Instances

Pretty Declaration

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Declaration -> Doc

prettyPrec :: Int -> Declaration -> Doc

prettyList :: [Declaration] -> Doc

Pretty WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

ExprLike Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Declaration -> Declaration

foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration

FoldDecl Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> Declaration -> m

TraverseDecl Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> Declaration -> m Declaration

HasRange Declaration

Defined in Agda.Syntax.Concrete

Methods

getRange :: Declaration -> Range

HasRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range

KillRange Declaration

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Declaration

KillRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT WhereClause

Show Declaration

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Show WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> WhereClause -> ShowS

show :: WhereClause -> String

showList :: [WhereClause] -> ShowS

NFData Declaration

Defined in Agda.Syntax.Concrete

Methods

rnf :: Declaration -> ()

Eq Declaration

Defined in Agda.Syntax.Concrete

Methods

(==) :: Declaration -> Declaration -> Bool

(/=) :: Declaration -> Declaration -> Bool

ToAbstract (TopLevel [Declaration])

Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (TopLevel [Declaration])

Methods

toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration]))

type AbsOfCon (TopLevel [Declaration])

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (TopLevel [Declaration]) = TopLevelInfo

isPragma :: CMaybe Pragma m => Declaration -> m

Return Declaration if Declaration is Declaration.

isRecordDirective :: Declaration -> Maybe RecordDirective

Extract a record directive

data RecordDirective

Isolated record directives parsed as Declarations

Constructors

Induction (Ranged Induction)

Range of keyword [co]inductive.

Constructor Name IsInstance

Eta (Ranged HasEta0)

Range of [no-]eta-equality keyword.

PatternOrCopattern Range

If declaration pattern is present, give its range.

Instances

HasRange RecordDirective

Defined in Agda.Syntax.Concrete

Methods

getRange :: RecordDirective -> Range

KillRange RecordDirective

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RecordDirective

Show RecordDirective

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> RecordDirective -> ShowS

show :: RecordDirective -> String

showList :: [RecordDirective] -> ShowS

NFData RecordDirective

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: RecordDirective -> ()

Eq RecordDirective

Defined in Agda.Syntax.Concrete

Methods

(==) :: RecordDirective -> RecordDirective -> Bool

(/=) :: RecordDirective -> RecordDirective -> Bool

type RecordDirectives = RecordDirectives' (Name, IsInstance)

data ModuleApplication

Constructors

SectionApp Range Telescope Expr

tel. M args

RecordModuleInstance Range QName

M {{...}}

Instances

Pretty ModuleApplication

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleApplication -> Doc

prettyPrec :: Int -> ModuleApplication -> Doc

prettyList :: [ModuleApplication] -> Doc

ExprLike ModuleApplication

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication

HasRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleApplication -> Range

KillRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleApplication

Show ModuleApplication

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

NFData ModuleApplication

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleApplication -> ()

Eq ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

(==) :: ModuleApplication -> ModuleApplication -> Bool

(/=) :: ModuleApplication -> ModuleApplication -> Bool

type TypeSignature = Declaration

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

type Using = Using' Name Name

type ImportedName = ImportedName' Name Name

An imported name can be a module or a defined name.

type Renaming = Renaming' Name Name

type RenamingDirective = RenamingDirective' Name Name

type HidingDirective = HidingDirective' Name Name

data AsName' a

The content of the as-clause of the import statement.

Constructors

AsName

Fields

• asName :: a

  The "as" name.

• asRange :: Range

  The range of the "as" keyword. Retained for highlighting purposes.

Instances

HasRange AsName

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range

KillRange AsName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT AsName

Foldable AsName'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => AsName' m -> m

foldMap :: Monoid m => (a -> m) -> AsName' a -> m

foldMap' :: Monoid m => (a -> m) -> AsName' a -> m

foldr :: (a -> b -> b) -> b -> AsName' a -> b

foldr' :: (a -> b -> b) -> b -> AsName' a -> b

foldl :: (b -> a -> b) -> b -> AsName' a -> b

foldl' :: (b -> a -> b) -> b -> AsName' a -> b

foldr1 :: (a -> a -> a) -> AsName' a -> a

foldl1 :: (a -> a -> a) -> AsName' a -> a

toList :: AsName' a -> [a]

null :: AsName' a -> Bool

length :: AsName' a -> Int

elem :: Eq a => a -> AsName' a -> Bool

maximum :: Ord a => AsName' a -> a

minimum :: Ord a => AsName' a -> a

sum :: Num a => AsName' a -> a

product :: Num a => AsName' a -> a

Traversable AsName'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> AsName' a -> f (AsName' b)

sequenceA :: Applicative f => AsName' (f a) -> f (AsName' a)

mapM :: Monad m => (a -> m b) -> AsName' a -> m (AsName' b)

sequence :: Monad m => AsName' (m a) -> m (AsName' a)

Functor AsName'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> AsName' a -> AsName' b

(<$) :: a -> AsName' b -> AsName' a

NFData AsName

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

Show a => Show (AsName' a)

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> AsName' a -> ShowS

show :: AsName' a -> String

showList :: [AsName' a] -> ShowS

Eq a => Eq (AsName' a)

Defined in Agda.Syntax.Concrete

Methods

(==) :: AsName' a -> AsName' a -> Bool

(/=) :: AsName' a -> AsName' a -> Bool

type AsName = AsName' (Either Expr Name)

From the parser, we get an expression for the as-Name, which we have to parse into a Name.

data OpenShortHand

Constructors

DoOpen

DontOpen

Instances

Pretty OpenShortHand

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpenShortHand -> Doc

prettyPrec :: Int -> OpenShortHand -> Doc

prettyList :: [OpenShortHand] -> Doc

Generic OpenShortHand

Defined in Agda.Syntax.Concrete

Associated Types

type Rep OpenShortHand :: Type -> Type

Methods

from :: OpenShortHand -> Rep OpenShortHand x

to :: Rep OpenShortHand x -> OpenShortHand

Show OpenShortHand

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> OpenShortHand -> ShowS

show :: OpenShortHand -> String

showList :: [OpenShortHand] -> ShowS

NFData OpenShortHand

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpenShortHand -> ()

Eq OpenShortHand

Defined in Agda.Syntax.Concrete

Methods

(==) :: OpenShortHand -> OpenShortHand -> Bool

(/=) :: OpenShortHand -> OpenShortHand -> Bool

type Rep OpenShortHand

Defined in Agda.Syntax.Concrete

type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" 'False) (C1 ('MetaCons "DoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DontOpen" 'PrefixI 'False) (U1 :: Type -> Type))

type RewriteEqn = RewriteEqn' () Name Pattern Expr

type WithExpr = Named Name (Arg Expr)

data LHS

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

• lhsOriginalPattern :: Pattern

  e.g. f ps | wps

• lhsRewriteEqn :: [RewriteEqn]

  (rewrite e | with p <- e in eq) (many)

• lhsWithExpr :: [WithExpr]

  with e1 in eq | {e2} | ... (many)

Instances

Pretty LHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc

prettyPrec :: Int -> LHS -> Doc

prettyList :: [LHS] -> Doc

ExprLike LHS

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> LHS -> LHS

foldExpr :: Monoid m => (Expr -> m) -> LHS -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS

HasEllipsis LHS

Does the lhs contain an ellipsis?

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool

HasRange LHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range

KillRange LHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LHS

Show LHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

NFData LHS

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: LHS -> ()

Eq LHS

Defined in Agda.Syntax.Concrete

Methods

(==) :: LHS -> LHS -> Bool

(/=) :: LHS -> LHS -> Bool

data Pattern

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP Bool QName

c or x

If the boolean is False, then the QName must not refer to a constructor or a pattern synonym. The value False is used when a hidden argument pun is expanded.

QuoteP Range

quote

AppP Pattern (NamedArg Pattern)

p p' or p {x = p'}

RawAppP Range (List2 Pattern)

p1..pn before parsing operators

OpAppP Range QName (Set Name) [NamedArg Pattern]

eg: p => p' for operator _=>_ The QName is possibly ambiguous, but it must correspond to one of the names in the set.

HiddenP Range (Named_ Pattern)

{p} or {x = p}

InstanceP Range (Named_ Pattern)

{{p}} or {{x = p}}

ParenP Range Pattern

(p)

WildP Range

_

AbsurdP Range

()

AsP Range Name Pattern

x@p unused

DotP Range Expr

.e

LitP Range Literal

0, 1, etc.

RecP Range [FieldAssignment' Pattern]

record {x = p; y = q}

EqualP Range [(Expr, Expr)]

i = i1 i.e. cubical face lattice generator

EllipsisP Range (Maybe Pattern)

..., only as left-most pattern. Second arg is Nothing before expansion, and Just p after expanding ellipsis to p.

WithP Range Pattern

| p, for with-patterns.

Instances

Pretty Pattern

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pattern -> Doc

prettyPrec :: Int -> Pattern -> Doc

prettyList :: [Pattern] -> Doc

IsExpr Pattern

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

exprView :: Pattern -> ExprView Pattern

unExprView :: ExprView Pattern -> Pattern

patternView :: Pattern -> Maybe Pattern

CPatternLike Pattern

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern

HasEllipsis Pattern

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: Pattern -> Bool

IsEllipsis Pattern

Is the pattern just ...?

Defined in Agda.Syntax.Concrete.Pattern

Methods

isEllipsis :: Pattern -> Bool

IsWithP Pattern

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Pattern -> Maybe Pattern

HasRange Pattern

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pattern -> Range

KillRange Pattern

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pattern

SetRange Pattern

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> Pattern -> Pattern

ToAbstract HoleContent

Content of interaction hole.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent)

ToAbstract Pattern

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern

Methods

toAbstract :: Pattern -> ScopeM (AbsOfCon Pattern)

ToAbstract RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn

Methods

toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn)

Show Pattern

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

NFData Pattern

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: Pattern -> ()

Eq Pattern

Defined in Agda.Syntax.Concrete

Methods

(==) :: Pattern -> Pattern -> Bool

(/=) :: Pattern -> Pattern -> Bool

type AbsOfCon HoleContent

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent = HoleContent

type AbsOfCon Pattern

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Pattern = Pattern' Expr

type AbsOfCon RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

data LHSCore

Processed (operator-parsed) intermediate form of the core f ps of LHS. Corresponds to lhsOriginalPattern.

Constructors

LHSHead

Fields

• lhsDefName :: QName

  f

• lhsPats :: [NamedArg Pattern]

  ps

LHSProj

Fields

• lhsDestructor :: QName

  Record projection.

• lhsPatsLeft :: [NamedArg Pattern]

  Patterns for record indices (currently none).

• lhsFocus :: NamedArg LHSCore

  Main argument.

• lhsPats :: [NamedArg Pattern]

  ps

LHSWith

Fields

• lhsHead :: LHSCore
• lhsWithPatterns :: [Pattern]

  Non-empty; at least one (| p).

• lhsPats :: [NamedArg Pattern]

  ps

LHSEllipsis

Fields

• lhsEllipsisRange :: Range
• lhsEllipsisPat :: LHSCore

  Pattern that was expanded from an ellipsis ....

Instances

Pretty LHSCore

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHSCore -> Doc

prettyPrec :: Int -> LHSCore -> Doc

prettyList :: [LHSCore] -> Doc

HasRange LHSCore

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHSCore -> Range

ToAbstract LHSCore

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore

Methods

toAbstract :: LHSCore -> ScopeM (AbsOfCon LHSCore)

Show LHSCore

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

Eq LHSCore

Defined in Agda.Syntax.Concrete

Methods

(==) :: LHSCore -> LHSCore -> Bool

(/=) :: LHSCore -> LHSCore -> Bool

type AbsOfCon LHSCore

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LHSCore = LHSCore' Expr

data LamClause

Constructors

LamClause

Fields

• lamLHS :: [Pattern]

  Possibly empty sequence.

• lamRHS :: RHS
• lamCatchAll :: Bool

Instances

Pretty LamClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamClause -> Doc

prettyPrec :: Int -> LamClause -> Doc

prettyList :: [LamClause] -> Doc

ExprLike LamClause

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> LamClause -> LamClause

foldExpr :: Monoid m => (Expr -> m) -> LamClause -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> LamClause -> m LamClause

HasRange LamClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamClause -> Range

KillRange LamClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamClause

Show LamClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamClause -> ShowS

show :: LamClause -> String

showList :: [LamClause] -> ShowS

NFData LamClause

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamClause -> ()

Eq LamClause

Defined in Agda.Syntax.Concrete

Methods

(==) :: LamClause -> LamClause -> Bool

(/=) :: LamClause -> LamClause -> Bool

type RHS = RHS' Expr

data RHS' e

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e

Instances

Pretty RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

HasRange RHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range

KillRange RHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RHS

ToAbstract RHS

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS

Methods

toAbstract :: RHS -> ScopeM (AbsOfCon RHS)

Foldable RHS'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => RHS' m -> m

foldMap :: Monoid m => (a -> m) -> RHS' a -> m

foldMap' :: Monoid m => (a -> m) -> RHS' a -> m

foldr :: (a -> b -> b) -> b -> RHS' a -> b

foldr' :: (a -> b -> b) -> b -> RHS' a -> b

foldl :: (b -> a -> b) -> b -> RHS' a -> b

foldl' :: (b -> a -> b) -> b -> RHS' a -> b

foldr1 :: (a -> a -> a) -> RHS' a -> a

foldl1 :: (a -> a -> a) -> RHS' a -> a

toList :: RHS' a -> [a]

null :: RHS' a -> Bool

length :: RHS' a -> Int

elem :: Eq a => a -> RHS' a -> Bool

maximum :: Ord a => RHS' a -> a

minimum :: Ord a => RHS' a -> a

sum :: Num a => RHS' a -> a

product :: Num a => RHS' a -> a

Traversable RHS'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> RHS' a -> f (RHS' b)

sequenceA :: Applicative f => RHS' (f a) -> f (RHS' a)

mapM :: Monad m => (a -> m b) -> RHS' a -> m (RHS' b)

sequence :: Monad m => RHS' (m a) -> m (RHS' a)

Functor RHS'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> RHS' a -> RHS' b

(<$) :: a -> RHS' b -> RHS' a

Show RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

ExprLike a => ExprLike (RHS' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a

foldExpr :: Monoid m => (Expr -> m) -> RHS' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> RHS' a -> m (RHS' a)

NFData a => NFData (RHS' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: RHS' a -> ()

Eq e => Eq (RHS' e)

Defined in Agda.Syntax.Concrete

Methods

(==) :: RHS' e -> RHS' e -> Bool

(/=) :: RHS' e -> RHS' e -> Bool

type AbsOfCon RHS

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RHS = AbstractRHS

type WhereClause = WhereClause' [Declaration]

where block following a clause.

data WhereClause' decls

Constructors

NoWhere

No where clauses.

AnyWhere Range decls

Ordinary where. Range' of the where keyword. List of declarations can be empty.

SomeWhere Range Erased Name Access decls

Named where: module M where ds. Range' of the keywords module and where. The Access flag applies to the Name (not the module contents!) and is propagated from the parent function. List of declarations can be empty.

Instances

Pretty WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

HasRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range

KillRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT WhereClause

Foldable WhereClause'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => WhereClause' m -> m

foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m

foldMap' :: Monoid m => (a -> m) -> WhereClause' a -> m

foldr :: (a -> b -> b) -> b -> WhereClause' a -> b

foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b

foldl :: (b -> a -> b) -> b -> WhereClause' a -> b

foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b

foldr1 :: (a -> a -> a) -> WhereClause' a -> a

foldl1 :: (a -> a -> a) -> WhereClause' a -> a

toList :: WhereClause' a -> [a]

null :: WhereClause' a -> Bool

length :: WhereClause' a -> Int

elem :: Eq a => a -> WhereClause' a -> Bool

maximum :: Ord a => WhereClause' a -> a

minimum :: Ord a => WhereClause' a -> a

sum :: Num a => WhereClause' a -> a

product :: Num a => WhereClause' a -> a

Traversable WhereClause'

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b)

sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a)

mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b)

sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a)

Functor WhereClause'

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> WhereClause' a -> WhereClause' b

(<$) :: a -> WhereClause' b -> WhereClause' a

Show WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> WhereClause -> ShowS

show :: WhereClause -> String

showList :: [WhereClause] -> ShowS

ExprLike a => ExprLike (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a

foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a)

FoldDecl a => FoldDecl (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> WhereClause' a -> m

TraverseDecl a => TraverseDecl (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> WhereClause' a -> m (WhereClause' a)

Null (WhereClause' a)

A WhereClause is null when the where keyword is absent. An empty list of declarations does not count as null here.

Defined in Agda.Syntax.Concrete

Methods

empty :: WhereClause' a

null :: WhereClause' a -> Bool

NFData a => NFData (WhereClause' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: WhereClause' a -> ()

Eq decls => Eq (WhereClause' decls)

Defined in Agda.Syntax.Concrete

Methods

(==) :: WhereClause' decls -> WhereClause' decls -> Bool

(/=) :: WhereClause' decls -> WhereClause' decls -> Bool

data ExprWhere

An expression followed by a where clause. Currently only used to give better a better error message in interaction.

Constructors

ExprWhere Expr WhereClause

data DoStmt

Constructors

DoBind Range Pattern Expr [LamClause]

p ← e where cs

DoThen Expr

DoLet Range (List1 Declaration)

Instances

Pretty DoStmt

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: DoStmt -> Doc

prettyPrec :: Int -> DoStmt -> Doc

prettyList :: [DoStmt] -> Doc

ExprLike DoStmt

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt

foldExpr :: Monoid m => (Expr -> m) -> DoStmt -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> DoStmt -> m DoStmt

HasRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

getRange :: DoStmt -> Range

KillRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT DoStmt

Show DoStmt

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> DoStmt -> ShowS

show :: DoStmt -> String

showList :: [DoStmt] -> ShowS

NFData DoStmt

Defined in Agda.Syntax.Concrete

Methods

rnf :: DoStmt -> ()

Eq DoStmt

Defined in Agda.Syntax.Concrete

Methods

(==) :: DoStmt -> DoStmt -> Bool

(/=) :: DoStmt -> DoStmt -> Bool

data Pragma

Constructors

OptionsPragma Range [String]

BuiltinPragma Range RString QName

RewritePragma Range Range [QName]

Second Range is for REWRITE keyword.

ForeignPragma Range RString String

first string is backend name

CompilePragma Range RString QName String

first string is backend name

StaticPragma Range QName

InlinePragma Range Bool QName

INLINE or NOINLINE

ImpossiblePragma Range [String]

Throws an internal error in the scope checker. The Strings are words to be displayed with the error.

EtaPragma Range QName

For coinductive records, use pragma instead of regular eta-equality definition (as it is might make Agda loop).

WarningOnUsage Range QName Text

Applies to the named function

WarningOnImport Range Text

Applies to the current module

InjectivePragma Range QName

Mark a definition as injective for the pattern matching unifier.

DisplayPragma Range Pattern Expr

Display lhs as rhs (modifies the printer).

CatchallPragma Range

Applies to the following function clause.

TerminationCheckPragma Range (TerminationCheck Name)

Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.

NoCoverageCheckPragma Range

Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.

NoPositivityCheckPragma Range

Applies to the following data/record type or mutual block.

PolarityPragma Range Name [Occurrence]

NoUniverseCheckPragma Range

Applies to the following data/record type.

NotProjectionLikePragma Range QName

Applies to the stated function

Instances

Pretty Pragma

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pragma -> Doc

prettyPrec :: Int -> Pragma -> Doc

prettyList :: [Pragma] -> Doc

HasRange Pragma

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pragma -> Range

KillRange Pragma

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pragma

ToAbstract Pragma

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma

Methods

toAbstract :: Pragma -> ScopeM (AbsOfCon Pragma)

Show Pragma

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

NFData Pragma

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: Pragma -> ()

Eq Pragma

Defined in Agda.Syntax.Concrete

Methods

(==) :: Pragma -> Pragma -> Bool

(/=) :: Pragma -> Pragma -> Bool

type AbsOfCon Pragma

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Pragma = [Pragma]

data Module

Modules: Top-level pragmas plus other top-level declarations.

Constructors

Mod

Fields

• modPragmas :: [Pragma]
• modDecls :: [Declaration]

Instances

Show Module

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Foldable ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

fold :: Monoid m => ThingWithFixity m -> m

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m

foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m

foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b

foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b

foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b

foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b

foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a

foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a

toList :: ThingWithFixity a -> [a]

null :: ThingWithFixity a -> Bool

length :: ThingWithFixity a -> Int

elem :: Eq a => a -> ThingWithFixity a -> Bool

maximum :: Ord a => ThingWithFixity a -> a

minimum :: Ord a => ThingWithFixity a -> a

sum :: Num a => ThingWithFixity a -> a

product :: Num a => ThingWithFixity a -> a

Traversable ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)

sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a)

mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)

sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a)

Functor ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b

(<$) :: a -> ThingWithFixity b -> ThingWithFixity a

LensFixity (ThingWithFixity a)

Defined in Agda.Syntax.Fixity

Methods

lensFixity :: Lens' (ThingWithFixity a) Fixity

LensFixity' (ThingWithFixity a)

Defined in Agda.Syntax.Fixity

Methods

lensFixity' :: Lens' (ThingWithFixity a) Fixity'

Pretty (ThingWithFixity Name)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

KillRange x => KillRange (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

killRange :: KillRangeT (ThingWithFixity x)

Show x => Show (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

type HoleContent = HoleContent' () Name Pattern Expr

data HoleContent' qn nm p e

Extended content of an interaction hole.

Constructors

HoleContentExpr e

e

HoleContentRewrite [RewriteEqn' qn nm p e]

(rewrite | invert) e0 | ... | en

Instances

ToAbstract HoleContent

Content of interaction hole.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent)

Foldable (HoleContent' qn nm p)

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => HoleContent' qn nm p m -> m

foldMap :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m

foldMap' :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m

foldr :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b

foldr' :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b

foldl :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b

foldl' :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b

foldr1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a

foldl1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a

toList :: HoleContent' qn nm p a -> [a]

null :: HoleContent' qn nm p a -> Bool

length :: HoleContent' qn nm p a -> Int

elem :: Eq a => a -> HoleContent' qn nm p a -> Bool

maximum :: Ord a => HoleContent' qn nm p a -> a

minimum :: Ord a => HoleContent' qn nm p a -> a

sum :: Num a => HoleContent' qn nm p a -> a

product :: Num a => HoleContent' qn nm p a -> a

Traversable (HoleContent' qn nm p)

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)

sequenceA :: Applicative f => HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)

mapM :: Monad m => (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)

sequence :: Monad m => HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)

Functor (HoleContent' qn nm p)

Defined in Agda.Syntax.Concrete

Methods

fmap :: (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b

(<$) :: a -> HoleContent' qn nm p b -> HoleContent' qn nm p a

type AbsOfCon HoleContent

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent = HoleContent

spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])

Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.