Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete

Contents

Description

The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.

Synopsis

Expressions

data Expr Source #

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 (Arg 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, ..

PropN Range Integer

ex: Prop0, Prop1, ..

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.

Generalized Expr 
Instances
Data Expr Source # 
Instance details

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 Expr 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

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

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

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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 #

KillRange AsName 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

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange AsName 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

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range Source #

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

IsExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete InteractionId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete NamedMeta Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract HoleContent HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RHS AbstractRHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LHSCore (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pattern (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Show (RHS' Expr) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS' Expr -> ShowS

show :: RHS' Expr -> String

showList :: [RHS' Expr] -> ShowS

Show (TypedBinding' Expr) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding' Expr -> ShowS

show :: TypedBinding' Expr -> String

showList :: [TypedBinding' Expr] -> ShowS

Show (LamBinding' TypedBinding) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ToAbstract (Pattern' Expr) (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data OpApp e Source #

Constructors

SyntaxBindingLambda Range [LamBinding] e

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

Ordinary e 
Instances
Functor OpApp Source # 
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

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)

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

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)

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

NFData a => NFData (OpApp a) Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpApp a -> ()

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range Source #

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

data AppView Source #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr] 

Bindings

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

DomainFree (NamedArg BoundName)

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

DomainFull a

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

Instances
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

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)

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Concrete

Methods

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

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

toConstr :: LamBinding' a -> Constr

dataTypeOf :: LamBinding' a -> DataType

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

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

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

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

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

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

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

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

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

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

Show (LamBinding' TypedBinding) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamBinding' a -> ()

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

Constructors

TBind Range [NamedArg BoundName] e

Binding (x1 ... xn : A).

TLet Range [Declaration]

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

Instances
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

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)

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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)

Show (TypedBinding' Expr) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> TypedBinding' Expr -> ShowS

show :: TypedBinding' Expr -> String

showList :: [TypedBinding' Expr] -> ShowS

Show (LamBinding' TypedBinding) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: TypedBinding' a -> ()

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

data FieldAssignment' a Source #

Constructors

FieldAssignment 

Fields

Instances
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

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)

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

SubstExpr Assign Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

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

Defined in Agda.Syntax.Concrete

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

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

Defined in Agda.Syntax.Concrete

Methods

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

show :: FieldAssignment' a -> String

showList :: [FieldAssignment' a] -> ShowS

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: FieldAssignment' a -> ()

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

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 #

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

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

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

Defined in Agda.Syntax.Abstract.Pattern

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 #

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

Defined in Agda.Syntax.Internal.Names

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

Defined in Agda.TypeChecking.Patterns.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data ModuleAssignment Source #

Instances
Data ModuleAssignment Source # 
Instance details

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

Show ModuleAssignment 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ModuleAssignment -> ShowS

show :: ModuleAssignment -> String

showList :: [ModuleAssignment] -> ShowS

NFData ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleAssignment -> ()

Pretty ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data BoundName Source #

Constructors

BName 
Instances
Eq BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Data BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

toConstr :: BoundName -> Constr

dataTypeOf :: BoundName -> DataType

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

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

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

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

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

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

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

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

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

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

Show BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> BoundName -> ShowS

show :: BoundName -> String

showList :: [BoundName] -> ShowS

NFData BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: BoundName -> ()

Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToConcrete BindName BoundName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract (NewName BoundName) BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Telescope = [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

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 Name Expr

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

Generalize Range [TypeSignature]

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

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] Expr [TypeSignatureOrInstanceBlock] 
DataDef Range Induction Name [LamBinding] [TypeSignatureOrInstanceBlock] 
RecordSig Range Name [LamBinding] Expr

lone record signature in mutual block

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

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 Telescope [Declaration] 
UnquoteDecl Range [Name] Expr 
UnquoteDef Range [Name] Expr 
Pragma Pragma 
Instances
Data Declaration Source # 
Instance details

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

NFData Declaration Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Declaration -> ()

Pretty Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete WhereDeclarations WhereClause Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LetBinding [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Declaration [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Show (WhereClause' [Declaration]) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> WhereClause' [Declaration] -> ShowS

show :: WhereClause' [Declaration] -> String

showList :: [WhereClause' [Declaration]] -> ShowS

ToConcrete (Constr Constructor) Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract (TopLevel [Declaration]) TopLevelInfo 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

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract [Declaration] [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data ModuleApplication Source #

Instances
Data ModuleApplication Source # 
Instance details

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

NFData ModuleApplication Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleApplication -> ()

Pretty ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ToConcrete ModuleApplication ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

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)

NFData AsName Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

Methods

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

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

toConstr :: AsName' a -> Constr

dataTypeOf :: AsName' a -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

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

show :: AsName' a -> String

showList :: [AsName' a] -> ShowS

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

Defined in Agda.Syntax.Concrete

Data OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

toConstr :: OpenShortHand -> Constr

dataTypeOf :: OpenShortHand -> DataType

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

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

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

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

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

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

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

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

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

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

Show OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

showsPrec :: Int -> OpenShortHand -> ShowS

show :: OpenShortHand -> String

showList :: [OpenShortHand] -> ShowS

Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

NFData LHS Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: LHS -> ()

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 #

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range Source #

HasEllipsis LHS Source #

Does the lhs contain an ellipsis?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool Source #

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ToConcrete LHS LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete SpineLHS LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data Pattern Source #

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}
EqualP Range [(Expr, Expr)]

i = i1 i.e. cubical face lattice generator

EllipsisP Range

..., only as left-most pattern.

WithP Range Pattern

| p, for with-patterns.

Instances
Data Pattern Source # 
Instance details

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

NFData Pattern Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Pattern -> ()

Pretty Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

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 #

IsWithP Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

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

IsExpr Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

ToConcrete Pattern Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LHSCore Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Instances
Show LHSCore 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

Pretty LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LHSCore (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LamClause Source #

Constructors

LamClause 

Fields

Instances
Data LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

toConstr :: LamClause -> Constr

dataTypeOf :: LamClause -> DataType

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

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

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

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

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

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

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

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

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

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

Show LamClause 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> LamClause -> ShowS

show :: LamClause -> String

showList :: [LamClause] -> ShowS

NFData LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamClause -> ()

Pretty LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

data RHS' e Source #

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e 
Instances
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

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)

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 #

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

ToAbstract RHS AbstractRHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

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)

Show (RHS' Expr) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS' Expr -> ShowS

show :: RHS' Expr -> String

showList :: [RHS' Expr] -> ShowS

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: RHS' a -> ()

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

data WhereClause' decls Source #

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' 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

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)

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToConcrete WhereDeclarations WhereClause Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Concrete

Methods

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

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

toConstr :: WhereClause' decls -> Constr

dataTypeOf :: WhereClause' decls -> DataType

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

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

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

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

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

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

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

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

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

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

Show (WhereClause' [Declaration]) 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> WhereClause' [Declaration] -> ShowS

show :: WhereClause' [Declaration] -> String

showList :: [WhereClause' [Declaration]] -> ShowS

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: WhereClause' a -> ()

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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 #

Constructors

DoBind Range Pattern Expr [LamClause]
p ← e where cs
DoThen Expr 
DoLet Range [Declaration] 
Instances
Data DoStmt Source # 
Instance details

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

Show DoStmt 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> DoStmt -> ShowS

show :: DoStmt -> String

showList :: [DoStmt] -> ShowS

NFData DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: DoStmt -> ()

Pretty DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

ExprLike DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

data Pragma Source #

Constructors

OptionsPragma Range [String] 
BuiltinPragma Range String QName 
RewritePragma Range [QName] 
ForeignPragma Range String String

first string is backend name

CompilePragma Range String QName String

first string is backend name

StaticPragma Range QName 
InlinePragma Range Bool QName

INLINE or NOINLINE

ImpossiblePragma Range

Throws an internal error in the scope checker.

EtaPragma Range QName

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

WarningOnUsage Range QName String

Applies to the named function

InjectivePragma Range QName

Mark a definition as injective for the pattern matching unifier.

DisplayPragma Range Pattern Expr

Display lhs as rhs (modifies the printer).

CatchallPragma Range

Applies to the following function clause.

TerminationCheckPragma Range (TerminationCheck Name)

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

NoPositivityCheckPragma Range

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

PolarityPragma Range Name [Occurrence] 
NoUniverseCheckPragma Range

Applies to the following data/record type.

Instances
Data Pragma Source # 
Instance details

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

NFData Pragma Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Pragma -> ()

Pretty Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToConcrete RangeAndPragma Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract Pragma [Pragma] Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 
Instances
Functor ThingWithFixity Source # 
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

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)

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

Defined in Agda.Syntax.Fixity

Methods

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

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

toConstr :: ThingWithFixity x -> Constr

dataTypeOf :: ThingWithFixity x -> DataType

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Fixity

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

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

data HoleContent' e Source #

Extended content of an interaction hole.

Constructors

HoleContentExpr e
e
HoleContentRewrite [e]
rewrite e0 | ... | en
Instances
Functor HoleContent' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable HoleContent' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

toList :: HoleContent' a -> [a]

null :: HoleContent' a -> Bool

length :: HoleContent' a -> Int

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

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

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

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

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

Traversable HoleContent' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

ToAbstract HoleContent HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

topLevelModuleName :: Module -> TopLevelModuleName Source #

Computes the top-level module name.

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

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

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