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 Literal

ex: 1 or "foo"

QuestionMark Range (Maybe Nat)

ex: ? or {! ... !}

Underscore Range (Maybe String)

ex: _ or _A_5

RawApp Range [Expr]

before parsing operators

App Range Expr (NamedArg Expr)

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

OpApp Range QName (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))]

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 [LamBinding] Expr

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

AbsurdLam Range Hiding

ex: \ ()

ExtendedLam Range [LamClause]

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

Fun Range Expr Expr

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

Pi Telescope Expr

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

Set Range

ex: Set

Prop Range

ex: Prop

SetN Range Integer

ex: Set0, Set1, ..

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 [Declaration] (Maybe Expr)

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

Paren Range Expr

ex: (e)

IdiomBrackets Range Expr

ex: (| e |)

DoBlock Range [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

ETel Telescope

only used for printing telescopes

QuoteGoal Range Name Expr

ex: quoteGoal x in e

QuoteContext Range

ex: quoteContext

Quote Range

ex: quote, should be applied to a name

QuoteTerm Range

ex: quoteTerm, should be applied to a term

Tactic Range Expr [Expr]

tactic solve | subgoal1 | .. | subgoalN

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.

Instances

Data Expr

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr

toConstr :: Expr -> Constr

dataTypeOf :: Expr -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r

gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr

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

Show TypedBindings

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBindings -> ShowS

show :: TypedBindings -> String

showList :: [TypedBindings] -> ShowS

Show LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show Expr

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

NFData Expr

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: Expr -> ()

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

Pretty TypedBindings

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBindings -> Doc

prettyPrec :: Int -> TypedBindings -> Doc

prettyList :: [TypedBindings] -> Doc

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty Expr

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc

prettyPrec :: Int -> Expr -> Doc

prettyList :: [Expr] -> Doc

KillRange RHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RHS

KillRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBinding

KillRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBindings

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

KillRange Expr

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Expr

SetRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBindings -> TypedBindings

HasRange RHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range

HasRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBindings -> Range

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

HasRange Expr

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range

LensRelevance TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensHiding TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

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

IsExpr Expr

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

exprView :: Expr -> ExprView Expr

unExprView :: ExprView Expr -> Expr

ExprLike TypedBindings

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Expr

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike FieldAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete InteractionId Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: InteractionId -> AbsToCon Expr

bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b

ToConcrete TypedBinding TypedBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: TypedBinding -> AbsToCon TypedBinding0

bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b

ToConcrete Expr Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Expr -> AbsToCon Expr0

bindToConcrete :: Expr -> (Expr0 -> AbsToCon b) -> AbsToCon b

ToConcrete NamedMeta Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: NamedMeta -> AbsToCon Expr

bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b

ToAbstract HoleContent HoleContent

Content of interaction hole.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: HoleContent0 -> ScopeM HoleContent

ToAbstract RHS AbstractRHS

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: RHS -> ScopeM AbstractRHS

ToAbstract TypedBinding TypedBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: TypedBinding0 -> ScopeM TypedBinding

ToAbstract TypedBindings TypedBindings

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: TypedBindings0 -> ScopeM TypedBindings

ToAbstract LamBinding LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: LamBinding0 -> ScopeM LamBinding

ToAbstract Expr Expr

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: Expr0 -> ScopeM Expr

ToConcrete TypedBindings [TypedBindings]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings0]

bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding0]

bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b

ToAbstract LHSCore (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

ToAbstract Pattern (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

Pretty (OpApp Expr)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpApp Expr -> Doc

prettyPrec :: Int -> OpApp Expr -> Doc

prettyList :: [OpApp Expr] -> Doc

ToAbstract (Pattern' Expr) (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

data OpApp e

Constructors

SyntaxBindingLambda Range [LamBinding] e

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

Ordinary e

Instances

Functor OpApp

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable OpApp

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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)

Data e => Data (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpApp e -> c (OpApp e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e)

toConstr :: OpApp e -> Constr

dataTypeOf :: OpApp e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e))

gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r

gmapQ :: (forall d. Data d => d -> u) -> OpApp e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpApp e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e)

NFData a => NFData (OpApp a)

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: 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

KillRange e => KillRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (OpApp e)

HasRange e => HasRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range

ExprLike a => ExprLike (OpApp a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

fromOrdinary :: e -> OpApp e -> e

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView

data AppView

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr]

Bindings

type LamBinding = LamBinding' TypedBindings

A lambda binding is either domain free or typed.

data LamBinding' a

Constructors

DomainFree ArgInfo BoundName

. x or {x} or .x or .{x} or {.x}

DomainFull a

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

Instances

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

Foldable LamBinding'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

toList :: LamBinding' a -> [a]

null :: LamBinding' a -> Bool

length :: LamBinding' a -> Int

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

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

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

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

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

Traversable LamBinding'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

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

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToAbstract LamBinding LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: LamBinding0 -> ScopeM LamBinding

ToConcrete LamBinding [LamBinding]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding0]

bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b

Data a => Data (LamBinding' a)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding' a -> c (LamBinding' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LamBinding' a)

toConstr :: LamBinding' a -> Constr

dataTypeOf :: LamBinding' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LamBinding' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LamBinding' a))

gmapT :: (forall b. Data b => b -> b) -> LamBinding' a -> LamBinding' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r

gmapQ :: (forall d. Data d => d -> u) -> LamBinding' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a)

NFData a => NFData (LamBinding' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamBinding' a -> ()

type TypedBindings = TypedBindings' TypedBinding

A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.

If the individual binding contains hiding information as well, the Hiding in TypedBindings must be the unit NotHidden.

data TypedBindings' a

Constructors

TypedBindings Range (Arg a)

. (xs : e) or {xs : e} or something like (x {y} _ : e).

Instances

Functor TypedBindings'

Defined in Agda.Syntax.Concrete

Methods

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

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

Show TypedBindings

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBindings -> ShowS

show :: TypedBindings -> String

showList :: [TypedBindings] -> ShowS

Show LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Foldable TypedBindings'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

toList :: TypedBindings' a -> [a]

null :: TypedBindings' a -> Bool

length :: TypedBindings' a -> Int

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

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

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

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

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

Traversable TypedBindings'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

Pretty TypedBindings

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBindings -> Doc

prettyPrec :: Int -> TypedBindings -> Doc

prettyList :: [TypedBindings] -> Doc

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

KillRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBindings

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

SetRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBindings -> TypedBindings

HasRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBindings -> Range

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

LensRelevance TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensHiding TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

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

ExprLike TypedBindings

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToAbstract TypedBindings TypedBindings

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: TypedBindings0 -> ScopeM TypedBindings

ToAbstract LamBinding LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: LamBinding0 -> ScopeM LamBinding

ToConcrete TypedBindings [TypedBindings]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings0]

bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding0]

bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b

Data a => Data (TypedBindings' a)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBindings' a -> c (TypedBindings' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedBindings' a)

toConstr :: TypedBindings' a -> Constr

dataTypeOf :: TypedBindings' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedBindings' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypedBindings' a))

gmapT :: (forall b. Data b => b -> b) -> TypedBindings' a -> TypedBindings' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBindings' a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBindings' a -> r

gmapQ :: (forall d. Data d => d -> u) -> TypedBindings' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBindings' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBindings' a -> m (TypedBindings' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBindings' a -> m (TypedBindings' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBindings' a -> m (TypedBindings' a)

NFData a => NFData (TypedBindings' a)

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: TypedBindings' a -> ()

type TypedBinding = TypedBinding' Expr

A typed binding.

data TypedBinding' e

Constructors

TBind Range [WithHiding BoundName] e

Binding (x1 ... xn : A).

TLet Range [Declaration]

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

Instances

Functor TypedBinding'

Defined in Agda.Syntax.Concrete

Methods

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

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

Show TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

Show TypedBindings

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBindings -> ShowS

show :: TypedBindings -> String

showList :: [TypedBindings] -> ShowS

Show LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Foldable TypedBinding'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => TypedBinding' m -> 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)

Pretty TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

Pretty TypedBindings

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBindings -> Doc

prettyPrec :: Int -> TypedBindings -> Doc

prettyList :: [TypedBindings] -> Doc

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

KillRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBinding

KillRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBindings

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

SetRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBindings -> TypedBindings

HasRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range

HasRange TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBindings -> Range

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

LensRelevance TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensHiding TypedBindings

Defined in Agda.Syntax.Concrete

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Defined in Agda.Syntax.Concrete

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

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

ExprLike TypedBindings

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike LamBinding

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete TypedBinding TypedBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: TypedBinding -> AbsToCon TypedBinding0

bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b

ToAbstract TypedBinding TypedBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: TypedBinding0 -> ScopeM TypedBinding

ToAbstract TypedBindings TypedBindings

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: TypedBindings0 -> ScopeM TypedBindings

ToAbstract LamBinding LamBinding

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: LamBinding0 -> ScopeM LamBinding

ToConcrete TypedBindings [TypedBindings]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings0]

bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding0]

bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b

Data e => Data (TypedBinding' e)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding' e -> c (TypedBinding' e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedBinding' e)

toConstr :: TypedBinding' e -> Constr

dataTypeOf :: TypedBinding' e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedBinding' e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (TypedBinding' e))

gmapT :: (forall b. Data b => b -> b) -> TypedBinding' e -> TypedBinding' e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r

gmapQ :: (forall d. Data d => d -> u) -> TypedBinding' e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding' e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e)

NFData a => NFData (TypedBinding' a)

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: TypedBinding' a -> ()

ExprLike a => ExprLike (TypedBinding' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

type RecordAssignment = Either FieldAssignment ModuleAssignment

type RecordAssignments = [RecordAssignment]

type FieldAssignment = FieldAssignment' Expr

data FieldAssignment' a

Constructors

FieldAssignment

Fields

• _nameFieldA :: Name
• _exprFieldA :: a

Instances

Functor FieldAssignment'

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable FieldAssignment'

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => FieldAssignment' m -> 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)

ExprLike FieldAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

SubstExpr Assign

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Assign -> Assign

APatternLike a b => APatternLike a (FieldAssignment' b)

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

Eq a => Eq (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

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

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

Data a => Data (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FieldAssignment' a -> c (FieldAssignment' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FieldAssignment' a)

toConstr :: FieldAssignment' a -> Constr

dataTypeOf :: FieldAssignment' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FieldAssignment' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FieldAssignment' a))

gmapT :: (forall b. Data b => b -> b) -> FieldAssignment' a -> FieldAssignment' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r

gmapQ :: (forall d. Data d => d -> u) -> FieldAssignment' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FieldAssignment' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (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 -> ()

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

KillRange a => KillRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (FieldAssignment' a)

HasRange a => HasRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

getRange :: FieldAssignment' a -> Range

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)

ExprLike a => ExprLike (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

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

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

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

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a)

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> 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)

NamesIn a => NamesIn (FieldAssignment' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: FieldAssignment' a -> Set QName

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

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

ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

nameFieldA :: Lens' Name (FieldAssignment' a)

exprFieldA :: Lens' a (FieldAssignment' a)

data ModuleAssignment

Constructors

ModuleAssignment

Fields

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

Instances

Data ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleAssignment -> c ModuleAssignment

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleAssignment

toConstr :: ModuleAssignment -> Constr

dataTypeOf :: ModuleAssignment -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleAssignment)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleAssignment)

gmapT :: (forall b. Data b => b -> b) -> ModuleAssignment -> ModuleAssignment

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r

gmapQ :: (forall d. Data d => d -> u) -> ModuleAssignment -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleAssignment -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment

NFData ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleAssignment -> ()

Pretty ModuleAssignment

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleAssignment -> Doc

prettyPrec :: Int -> ModuleAssignment -> Doc

prettyList :: [ModuleAssignment] -> Doc

KillRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleAssignment

HasRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleAssignment -> Range

ExprLike ModuleAssignment

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToAbstract ModuleAssignment (ModuleName, [LetBinding])

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding])

data BoundName

Constructors

BName

Fields

• boundName :: Name
• boundLabel :: Name

  for implicit function types the label matters and can't be alpha-renamed

• bnameFixity :: Fixity'

Instances

Eq BoundName

Defined in Agda.Syntax.Concrete

Methods

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

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

Data BoundName

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoundName -> c BoundName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoundName

toConstr :: BoundName -> Constr

dataTypeOf :: BoundName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoundName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoundName)

gmapT :: (forall b. Data b => b -> b) -> BoundName -> BoundName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r

gmapQ :: (forall d. Data d => d -> u) -> BoundName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BoundName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName

Show BoundName

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> BoundName -> ShowS

show :: BoundName -> String

showList :: [BoundName] -> ShowS

NFData BoundName

Defined in Agda.Syntax.Concrete

Methods

rnf :: BoundName -> ()

Pretty BoundName

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: BoundName -> Doc

prettyPrec :: Int -> BoundName -> Doc

prettyList :: [BoundName] -> Doc

KillRange BoundName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT BoundName

HasRange BoundName

Defined in Agda.Syntax.Concrete

Methods

getRange :: BoundName -> Range

ToAbstract (NewName BoundName) Name

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewName BoundName -> ScopeM Name

mkBoundName_ :: Name -> BoundName

mkBoundName :: Name -> Fixity' -> BoundName

type Telescope = [TypedBindings]

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

countTelVars :: Telescope -> Nat

Declarations

data Declaration

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

Constructors

TypeSig ArgInfo Name Expr

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

Field IsInstance Name (Arg Expr)

Record field, can be hidden and/or irrelevant.

FunClause LHS RHS WhereClause Bool

DataSig Range Induction Name [LamBinding] Expr

lone data signature in mutual block

Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]

RecordSig Range Name [LamBinding] Expr

lone record signature in mutual block

Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] (Maybe Expr) [Declaration]

The optional name is a name for the record constructor.

Infix Fixity [Name]

Syntax Name Notation

notation declaration for a name

PatternSyn Range Name [Arg Name] Pattern

Mutual 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]

Macro Range [Declaration]

Postulate Range [TypeSignatureOrInstanceBlock]

Primitive Range [TypeSignature]

Open Range QName ImportDirective

Import Range QName (Maybe AsName) !OpenShortHand ImportDirective

ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective

Module Range QName [TypedBindings] [Declaration]

UnquoteDecl Range [Name] Expr

UnquoteDef Range [Name] Expr

Pragma Pragma

Instances

Data Declaration

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration

toConstr :: Declaration -> Constr

dataTypeOf :: Declaration -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration)

gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r

gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration

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

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: Declaration -> ()

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

KillRange Declaration

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Declaration

KillRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT WhereClause

HasRange Declaration

Defined in Agda.Syntax.Concrete

Methods

getRange :: Declaration -> Range

HasRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range

ExprLike Declaration

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete WhereDeclarations WhereClause

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: WhereDeclarations -> AbsToCon WhereClause

bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b

ToConcrete LetBinding [Declaration]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LetBinding -> AbsToCon [Declaration]

bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToConcrete Declaration [Declaration]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Declaration -> AbsToCon [Declaration0]

bindToConcrete :: Declaration -> ([Declaration0] -> AbsToCon b) -> AbsToCon b

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

ToConcrete (Constr Constructor) Declaration

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Constr Constructor -> AbsToCon Declaration

bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b

ToAbstract (TopLevel [Declaration]) TopLevelInfo

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

Methods

toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Clause' a -> AbsToCon [Declaration]

bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToAbstract [Declaration] [Declaration]

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: [Declaration0] -> ScopeM [Declaration]

data ModuleApplication

Constructors

SectionApp Range [TypedBindings] Expr

tel. M args

RecordModuleIFS Range QName

M {{...}}

Instances

Data ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleApplication -> c ModuleApplication

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication

toConstr :: ModuleApplication -> Constr

dataTypeOf :: ModuleApplication -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication)

gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r

gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m 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 -> ()

Pretty ModuleApplication

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleApplication -> Doc

prettyPrec :: Int -> ModuleApplication -> Doc

prettyList :: [ModuleApplication] -> Doc

KillRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleApplication

HasRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleApplication -> Range

ExprLike ModuleApplication

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete ModuleApplication ModuleApplication

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: ModuleApplication -> AbsToCon ModuleApplication0

bindToConcrete :: ModuleApplication -> (ModuleApplication0 -> AbsToCon b) -> AbsToCon b

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

data AsName

Constructors

AsName

Fields

• asName :: Name

  The "as" name.

• asRange :: Range

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

Instances

Data AsName

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AsName -> c AsName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AsName

toConstr :: AsName -> Constr

dataTypeOf :: AsName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AsName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AsName)

gmapT :: (forall b. Data b => b -> b) -> AsName -> AsName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AsName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AsName -> r

gmapQ :: (forall d. Data d => d -> u) -> AsName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AsName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AsName -> m AsName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName -> m AsName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName -> m AsName

Show AsName

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> AsName -> ShowS

show :: AsName -> String

showList :: [AsName] -> ShowS

NFData AsName

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

KillRange AsName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT AsName

HasRange AsName

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range

data OpenShortHand

Constructors

DoOpen

DontOpen

Instances

Eq OpenShortHand

Defined in Agda.Syntax.Concrete

Methods

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

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

Data OpenShortHand

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpenShortHand -> c OpenShortHand

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpenShortHand

toConstr :: OpenShortHand -> Constr

dataTypeOf :: OpenShortHand -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpenShortHand)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpenShortHand)

gmapT :: (forall b. Data b => b -> b) -> OpenShortHand -> OpenShortHand

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r

gmapQ :: (forall d. Data d => d -> u) -> OpenShortHand -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpenShortHand -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand

Show OpenShortHand

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> OpenShortHand -> ShowS

show :: OpenShortHand -> String

showList :: [OpenShortHand] -> ShowS

Pretty OpenShortHand

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpenShortHand -> Doc

prettyPrec :: Int -> OpenShortHand -> Doc

prettyList :: [OpenShortHand] -> Doc

type RewriteEqn = Expr

type WithExpr = 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 (many)

• lhsWithExpr :: [WithExpr]

  with e (many)

Instances

Data LHS

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS

toConstr :: LHS -> Constr

dataTypeOf :: LHS -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS)

gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r

gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS

Show LHS

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 -> ()

Pretty LHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc

prettyPrec :: Int -> LHS -> Doc

prettyList :: [LHS] -> Doc

KillRange LHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LHS

HasRange LHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range

HasEllipsis LHS

Does the lhs contain an ellipsis?

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool

ExprLike LHS

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete LHS LHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LHS -> AbsToCon LHS0

bindToConcrete :: LHS -> (LHS0 -> AbsToCon b) -> AbsToCon b

ToConcrete SpineLHS LHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: SpineLHS -> AbsToCon LHS

bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b

data Pattern

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName

c or x

QuoteP Range

quote

AppP Pattern (NamedArg Pattern)

p p' or p {x = p'}

RawAppP Range [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 Literal

0, 1, etc.

RecP Range [FieldAssignment' Pattern]

record {x = p; y = q}

EllipsisP Range

..., only as left-most pattern.

WithP Range Pattern

| p, for with-patterns.

Instances

Data Pattern

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern -> c Pattern

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pattern

toConstr :: Pattern -> Constr

dataTypeOf :: Pattern -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pattern)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pattern)

gmapT :: (forall b. Data b => b -> b) -> Pattern -> Pattern

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r

gmapQ :: (forall d. Data d => d -> u) -> Pattern -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern

Show Pattern

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 -> ()

Pretty Pattern

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pattern -> Doc

prettyPrec :: Int -> Pattern -> Doc

prettyList :: [Pattern] -> Doc

KillRange Pattern

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pattern

SetRange Pattern

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> Pattern -> Pattern

HasRange Pattern

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pattern -> Range

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

IsWithP Pattern

Defined in Agda.Syntax.Concrete.Pattern

Methods

isWithP :: Pattern -> Maybe 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

IsExpr Pattern

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

exprView :: Pattern -> ExprView Pattern

unExprView :: ExprView Pattern -> Pattern

ToConcrete Pattern Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Pattern -> AbsToCon Pattern0

bindToConcrete :: Pattern -> (Pattern0 -> AbsToCon b) -> AbsToCon b

ToConcrete LHSCore Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: LHSCore -> AbsToCon Pattern

bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b

ToAbstract Pattern (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: Pattern -> ScopeM (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

Instances

Show LHSCore

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

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 (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

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

data LamClause

Constructors

LamClause

Fields

• lamLHS :: LHS
• lamRHS :: RHS
• lamWhere :: WhereClause

  always NoWhere (see parser)

• lamCatchAll :: Bool

Instances

Data LamClause

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamClause -> c LamClause

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamClause

toConstr :: LamClause -> Constr

dataTypeOf :: LamClause -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamClause)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamClause)

gmapT :: (forall b. Data b => b -> b) -> LamClause -> LamClause

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r

gmapQ :: (forall d. Data d => d -> u) -> LamClause -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LamClause -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause

NFData LamClause

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamClause -> ()

Pretty LamClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamClause -> Doc

prettyPrec :: Int -> LamClause -> Doc

prettyList :: [LamClause] -> Doc

KillRange LamClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamClause

HasRange LamClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamClause -> Range

ExprLike LamClause

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

type RHS = RHS' Expr

data RHS' e

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e

Instances

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

Foldable RHS'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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)

Pretty RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

KillRange RHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RHS

HasRange RHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range

ToAbstract RHS AbstractRHS

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: RHS -> ScopeM AbstractRHS

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

Data e => Data (RHS' e)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS' e -> c (RHS' e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e)

toConstr :: RHS' e -> Constr

dataTypeOf :: RHS' e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e))

gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r

gmapQ :: (forall d. Data d => d -> u) -> RHS' e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS' e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e)

NFData a => NFData (RHS' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: RHS' a -> ()

ExprLike a => ExprLike (RHS' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

type WhereClause = WhereClause' [Declaration]

data WhereClause' decls

Constructors

NoWhere

No where clauses.

AnyWhere decls

Ordinary where.

SomeWhere Name Access decls

Named where: module M where. The Access flag applies to the Name (not the module contents!) and is propagated from the parent function.

Instances

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

Foldable WhereClause'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

toList :: WhereClause' a -> [a]

null :: WhereClause' a -> Bool

length :: WhereClause' a -> Int

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

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

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

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

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

Traversable WhereClause'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

Pretty WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

KillRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT WhereClause

HasRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range

ToConcrete WhereDeclarations WhereClause

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: WhereDeclarations -> AbsToCon WhereClause

bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b

Data decls => Data (WhereClause' decls)

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereClause' decls -> c (WhereClause' decls)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WhereClause' decls)

toConstr :: WhereClause' decls -> Constr

dataTypeOf :: WhereClause' decls -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WhereClause' decls))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WhereClause' decls))

gmapT :: (forall b. Data b => b -> b) -> WhereClause' decls -> WhereClause' decls

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r

gmapQ :: (forall d. Data d => d -> u) -> WhereClause' decls -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereClause' decls -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls)

NFData a => NFData (WhereClause' a)

Defined in Agda.Syntax.Concrete

Methods

rnf :: 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

ExprLike a => ExprLike (WhereClause' a)

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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 [Declaration]

Instances

Data DoStmt

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoStmt -> c DoStmt

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoStmt

toConstr :: DoStmt -> Constr

dataTypeOf :: DoStmt -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoStmt)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoStmt)

gmapT :: (forall b. Data b => b -> b) -> DoStmt -> DoStmt

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r

gmapQ :: (forall d. Data d => d -> u) -> DoStmt -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DoStmt -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt

NFData DoStmt

Defined in Agda.Syntax.Concrete

Methods

rnf :: DoStmt -> ()

Pretty DoStmt

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: DoStmt -> Doc

prettyPrec :: Int -> DoStmt -> Doc

prettyList :: [DoStmt] -> Doc

KillRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT DoStmt

HasRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

getRange :: DoStmt -> Range

ExprLike DoStmt

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

data Pragma

Constructors

OptionsPragma Range [String]

BuiltinPragma Range String QName

RewritePragma Range [QName]

CompiledDataPragma Range QName String [String]

CompiledTypePragma Range QName String

CompiledPragma Range QName String

CompiledExportPragma Range QName String

CompiledJSPragma Range QName String

CompiledUHCPragma Range QName String

CompiledDataUHCPragma Range QName String [String]

HaskellCodePragma Range String

ForeignPragma Range String String

first string is backend name

CompilePragma Range String QName String

first string is backend name

StaticPragma Range QName

InjectivePragma Range QName

InlinePragma Range Bool QName

INLINE or NOINLINE

ImportPragma Range String

Invariant: The string must be a valid Haskell module name.

ImportUHCPragma Range String

same as above, but for the UHC backend

ImpossiblePragma Range

Throws an internal error in the scope checker.

EtaPragma Range QName

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

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.

WarningOnUsage Range QName String

Applies to the named function

CatchallPragma Range

Applies to the following function clause.

DisplayPragma Range Pattern Expr

NoPositivityCheckPragma Range

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

PolarityPragma Range Name [Occurrence]

Instances

Data Pragma

Defined in Agda.Syntax.Concrete

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma

toConstr :: Pragma -> Constr

dataTypeOf :: Pragma -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma)

gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r

gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma

Show Pragma

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 -> ()

Pretty Pragma

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pragma -> Doc

prettyPrec :: Int -> Pragma -> Doc

prettyList :: [Pragma] -> Doc

KillRange Pragma

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pragma

HasRange Pragma

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pragma -> Range

ToConcrete RangeAndPragma Pragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: RangeAndPragma -> AbsToCon Pragma

bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b

ToAbstract Pragma [Pragma]

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: Pragma0 -> ScopeM [Pragma]

type Module = ([Pragma], [Declaration])

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

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

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

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

Foldable ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

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

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

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

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

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

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

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

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

toList :: ThingWithFixity a -> [a]

null :: ThingWithFixity a -> Bool

length :: ThingWithFixity a -> Int

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

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

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

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

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

Traversable ThingWithFixity

Defined in Agda.Syntax.Fixity

Methods

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

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

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

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

Data x => Data (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x)

toConstr :: ThingWithFixity x -> Constr

dataTypeOf :: ThingWithFixity x -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x))

gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r

gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x)

Show x => Show (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

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)

type HoleContent = HoleContent' Expr

data HoleContent' e

Extended content of an interaction hole.

Constructors

HoleContentExpr e

e

HoleContentRewrite [e]

rewrite e0 | ... | en

Instances

Functor HoleContent'

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable HoleContent'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

toList :: HoleContent' a -> [a]

null :: HoleContent' a -> Bool

length :: HoleContent' a -> Int

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

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

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

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

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

Traversable HoleContent'

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

ToAbstract HoleContent HoleContent

Content of interaction hole.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: HoleContent0 -> ScopeM HoleContent

topLevelModuleName :: Module -> TopLevelModuleName

Computes the top-level module name.

Precondition: The Module has to be well-formed. This means that there are only allowed declarations before the first module declaration, typically import declarations. See spanAllowedBeforeModule.

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

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