Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete

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

Expressions

data Expr Source #

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

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Pretty Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc Source #

prettyPrec :: Int -> Expr -> Doc Source #

prettyList :: [Expr] -> Doc Source #

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc Source #

prettyPrec :: Int -> RHS -> Doc Source #

prettyList :: [RHS] -> Doc Source #

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #

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

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

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

IsExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range Source #

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

NFData AsName Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

NFData Expr Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Expr -> ()

Show Expr 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Show LamBinding 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show RHS 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

Show TypedBinding 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

Eq Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

EncodeTCM (OutputForm Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

type AbsOfCon Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data OpApp e Source #

Constructors

SyntaxBindingLambda Range (List1 LamBinding) e

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

Ordinary e 

Instances

Instances details
Functor OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable OpApp Source # 
Instance details

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 Source # 
Instance details

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)

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike a => ExprLike (OpApp a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange e => HasRange (OpApp e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range Source #

KillRange e => KillRange (OpApp e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData a => NFData (OpApp a) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpApp a -> ()

Show a => Show (OpApp a) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> OpApp a -> ShowS

show :: OpApp a -> String

showList :: [OpApp a] -> ShowS

Eq e => Eq (OpApp e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

fromOrdinary :: e -> OpApp e -> e Source #

data AppView Source #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr] 

isPattern :: Expr -> Maybe Pattern Source #

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

observeHiding :: Expr -> WithHiding Expr Source #

Observe the hiding status of an expression

observeRelevance :: Expr -> (Relevance, Expr) Source #

Observe the relevance status of an expression

observeModifiers :: Expr -> Arg Expr Source #

Observe various modifiers applied to an expression

exprToPatternWithHoles :: Expr -> Pattern Source #

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

Bindings

data Binder' a Source #

A Binder x@p, the pattern is optional

Constructors

Binder 

Instances

Instances details
HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> ()

Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable Binder' Source # 
Instance details

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' Source # 
Instance details

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)

Pretty a => Pretty (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Binder' a -> Doc Source #

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

prettyList :: [Binder' a] -> Doc Source #

ToAbstract (Binder' (NewName BoundName)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName)) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Show a => Show (Binder' a) 
Instance details

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) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon (Binder' (NewName BoundName)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

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

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Functor LamBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable LamBinding' Source # 
Instance details

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' Source # 
Instance details

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)

Show LamBinding 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

NFData a => NFData (LamBinding' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamBinding' a -> ()

Eq a => Eq (LamBinding' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

dropTypeAndModality :: LamBinding -> [LamBinding] Source #

Drop type annotations and lets from bindings.

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

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

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Functor TypedBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable TypedBinding' Source # 
Instance details

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' Source # 
Instance details

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)

Show LamBinding 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show TypedBinding 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

ExprLike a => ExprLike (TypedBinding' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

NFData a => NFData (TypedBinding' a) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: TypedBinding' a -> ()

Eq e => Eq (TypedBinding' e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data FieldAssignment' a Source #

Constructors

FieldAssignment 

Fields

Instances

Instances details
ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

Functor FieldAssignment' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable FieldAssignment' Source # 
Instance details

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' Source # 
Instance details

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)

SubstExpr a => SubstExpr (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

APatternLike a => APatternLike (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (FieldAssignment' a) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

DeclaredNames a => DeclaredNames (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike a => ExprLike (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Pretty a => Pretty (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

CPatternLike p => CPatternLike (FieldAssignment' p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

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

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

NamesIn a => NamesIn (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange a => HasRange (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange a => KillRange (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToConcrete a => ToConcrete (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract c => ToAbstract (FieldAssignment' c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

EmbPrj a => EmbPrj (FieldAssignment' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: FieldAssignment' a -> S Int32 Source #

icod_ :: FieldAssignment' a -> S Int32 Source #

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

NFData a => NFData (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: FieldAssignment' a -> ()

Show a => Show (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

show :: FieldAssignment' a -> String

showList :: [FieldAssignment' a] -> ShowS

Eq a => Eq (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (FieldAssignment' c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

nameFieldA :: forall a f. Functor f => (Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a) Source #

exprFieldA :: forall a f. Functor f => (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a) Source #

data ModuleAssignment Source #

Instances

Instances details
Pretty ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

NFData ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleAssignment -> ()

Show ModuleAssignment 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ModuleAssignment -> ShowS

show :: ModuleAssignment -> String

showList :: [ModuleAssignment] -> ShowS

Eq ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

type AbsOfCon ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data BoundName Source #

Constructors

BName 

Fields

Instances

Instances details
Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> ()

NFData BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: BoundName -> ()

Show BoundName 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> BoundName -> ShowS

show :: BoundName -> String

showList :: [BoundName] -> ShowS

Eq BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

ToAbstract (Binder' (NewName BoundName)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName)) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Binder' (NewName BoundName)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

newtype TacticAttribute' a Source #

Constructors

TacticAttribute 

Instances

Instances details
Functor TacticAttribute' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

(<$) :: a -> TacticAttribute' b -> TacticAttribute' a #

Foldable TacticAttribute' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: TacticAttribute' a -> [a]

null :: TacticAttribute' a -> Bool

length :: TacticAttribute' a -> Int

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

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

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

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

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

Traversable TacticAttribute' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

ExprLike a => ExprLike (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Pretty a => Pretty (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike a => ExprLike (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source #

foldExpr :: Monoid m => (Expr -> m) -> TacticAttribute' a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> TacticAttribute' a -> m (TacticAttribute' a) Source #

KillRange (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToConcrete a => ToConcrete (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Null (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData a => NFData (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: TacticAttribute' a -> ()

Show a => Show (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

show :: TacticAttribute' a -> String

showList :: [TacticAttribute' a] -> ShowS

Eq a => Eq (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

type ConOfAbs (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Telescope1 = List1 TypedBinding Source #

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

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

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

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

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

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

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

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

Declarations

data Declaration Source #

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 KwRange [TypeSignature]

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

Field KwRange [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 [RecordDirective] [LamBinding] [Declaration] 
Record Range Erased Name [RecordDirective] [LamBinding] Expr [Declaration] 
Infix Fixity (List1 Name) 
Syntax Name Notation

notation declaration for a name

PatternSyn Range Name [WithHiding Name] Pattern 
Mutual KwRange [Declaration] 
InterleavedMutual KwRange [Declaration] 
Abstract KwRange [Declaration] 
Private KwRange 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 KwRange [Declaration]

The KwRange here only refers to the range of the instance keyword. The range of the whole block InstanceB r ds is fuseRange r ds.

LoneConstructor KwRange [Declaration] 
Macro KwRange [Declaration] 
Postulate KwRange [TypeSignatureOrInstanceBlock] 
Primitive KwRange [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 KwRange [Declaration]
opaque ...
Unfolding KwRange [QName]
unfolding ...

Instances

Instances details
Pretty Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

FoldDecl Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

TraverseDecl Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Declaration -> ()

Show Declaration 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Show WhereClause 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> WhereClause -> ShowS

show :: WhereClause -> String

showList :: [WhereClause] -> ShowS

Eq Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

ToAbstract (TopLevel [Declaration]) Source #

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (TopLevel [Declaration]) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (TopLevel [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data RecordDirective Source #

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

Instances details
Pretty RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

EmbPrj RecordDirective Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

NFData RecordDirective Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: RecordDirective -> ()

Show RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> RecordDirective -> ShowS

show :: RecordDirective -> String

showList :: [RecordDirective] -> ShowS

Eq RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

data ModuleApplication Source #

Instances

Instances details
Pretty ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData ModuleApplication Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleApplication -> ()

Show ModuleApplication 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

Eq ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

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.

data AsName' a Source #

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

Instances details
HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData AsName Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

Functor AsName' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable AsName' Source # 
Instance details

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' Source # 
Instance details

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)

Show a => Show (AsName' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

show :: AsName' a -> String

showList :: [AsName' a] -> ShowS

Eq a => Eq (AsName' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AsName = AsName' (Either Expr Name) Source #

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

data OpenShortHand Source #

Constructors

DoOpen 
DontOpen 

Instances

Instances details
Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

NFData OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpenShortHand -> ()

Generic OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Associated Types

type Rep OpenShortHand 
Instance details

Defined in Agda.Syntax.Concrete

type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Agda.Syntax.Concrete" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DontOpen" 'PrefixI 'False) (U1 :: Type -> Type))
Show OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> OpenShortHand -> ShowS

show :: OpenShortHand -> String

showList :: [OpenShortHand] -> ShowS

Eq OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

type Rep OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

data LHS 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

Instances details
Pretty LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc Source #

prettyPrec :: Int -> LHS -> Doc Source #

prettyList :: [LHS] -> Doc Source #

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasEllipsis LHS Source #

Does the lhs contain an ellipsis?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool Source #

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range Source #

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData LHS Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: LHS -> ()

Show LHS 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

Eq LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

data Pattern Source #

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

Instances details
Pretty Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

IsExpr Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

CPatternLike Pattern Source # 
Instance details

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 #

HasEllipsis Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: Pattern -> Bool Source #

IsEllipsis Pattern Source #

Is the pattern just ...?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

isEllipsis :: Pattern -> Bool Source #

IsWithP Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

HasRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

NFData Pattern Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Pattern -> ()

Show Pattern 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

Eq Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LHSCore Source #

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

Constructors

LHSHead 
LHSProj 

Fields

LHSWith 

Fields

LHSEllipsis 

Fields

Instances

Instances details
Pretty LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Show LHSCore 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

Eq LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LamClause Source #

Constructors

LamClause 

Fields

Instances

Instances details
Pretty LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamClause -> ()

Show LamClause 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamClause -> ShowS

show :: LamClause -> String

showList :: [LamClause] -> ShowS

Eq LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

data RHS' e Source #

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e 

Instances

Instances details
Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc Source #

prettyPrec :: Int -> RHS -> Doc Source #

prettyList :: [RHS] -> Doc Source #

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Functor RHS' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable RHS' Source # 
Instance details

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' Source # 
Instance details

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)

Show RHS 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

ExprLike a => ExprLike (RHS' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

NFData a => NFData (RHS' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: RHS' a -> ()

Eq e => Eq (RHS' e) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type WhereClause = WhereClause' [Declaration] Source #

where block following a clause.

data WhereClause' decls Source #

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

Instances details
Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Functor WhereClause' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable WhereClause' Source # 
Instance details

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' Source # 
Instance details

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)

Show WhereClause 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> WhereClause -> ShowS

show :: WhereClause -> String

showList :: [WhereClause] -> ShowS

ExprLike a => ExprLike (WhereClause' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

FoldDecl a => FoldDecl (WhereClause' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

TraverseDecl a => TraverseDecl (WhereClause' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

Null (WhereClause' a) Source #

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

Instance details

Defined in Agda.Syntax.Concrete

NFData a => NFData (WhereClause' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: WhereClause' a -> ()

Eq decls => Eq (WhereClause' decls) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

data ExprWhere Source #

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 Source #

Instances

Instances details
Pretty DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: DoStmt -> ()

Show DoStmt 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> DoStmt -> ShowS

show :: DoStmt -> String

showList :: [DoStmt] -> ShowS

Eq DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

data Pragma Source #

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.

InjectiveForInferencePragma Range QName

Mark a definition as injective for the conversion checker

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

OverlapPragma Range [QName] OverlapMode

Applies to the given name(s), which must be instance names (checked by the type checker).

Instances

Instances details
Pretty Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

NFData Pragma Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Pragma -> ()

Show Pragma 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data Module Source #

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

Constructors

Mod 

Instances

Instances details
Show Module 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

Instances

Instances details
Functor ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

Foldable ThingWithFixity Source # 
Instance details

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 Source # 
Instance details

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)

LensFixity (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Pretty (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange x => KillRange (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Show x => Show (ThingWithFixity x) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

data HoleContent' qn nm p e Source #

Extended content of an interaction hole.

Constructors

HoleContentExpr e
e
HoleContentRewrite [RewriteEqn' qn nm p e]
(rewrite | invert) e0 | ... | en

Instances

Instances details
ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Functor (HoleContent' qn nm p) Source # 
Instance details

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 #

Foldable (HoleContent' qn nm p) Source # 
Instance details

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) Source # 
Instance details

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)

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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.