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

Agda.Syntax.Concrete

Description

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

Synopsis

Expressions

data Expr Source #

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName

ex: x

Lit 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: (| e1 | e2 | .. | en |) or (|)

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

DoubleDot Range Expr

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

ETel Telescope

only used for printing telescopes

Quote Range

ex: quote, should be applied to a name

QuoteTerm Range

ex: quoteTerm, should be applied to a term

Tactic Range Expr

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

Unquote Range

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

DontCare Expr

to print irrelevant things

Equal Range Expr Expr

ex: a = b, used internally in the parser

Ellipsis Range

..., used internally to parse patterns.

Generalized Expr 

Instances

Instances details
Eq Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

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

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

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

ToConcrete InteractionId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

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 #

Scope check an expression.

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

EncodeTCM (OutputForm Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: OutputForm Expr Expr -> TCM Value Source #

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

Instances details
Functor OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: OpApp a -> [a] #

null :: OpApp a -> Bool #

length :: OpApp a -> Int #

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

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

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

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

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

Traversable OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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) Source # 
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] 

isPattern :: Expr -> Maybe Pattern Source #

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

Bindings

data Binder' a Source #

A Binder x@p, the pattern is optional

Constructors

Binder 

Instances

Instances details
Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable Binder' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: Binder' a -> [a] #

null :: Binder' a -> Bool #

length :: Binder' a -> Int #

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

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

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

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

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

Traversable Binder' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

NFData Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> () #

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

Methods

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

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

Data a => Data (Binder' 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) -> Binder' a -> c (Binder' a) #

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

toConstr :: Binder' a -> Constr #

dataTypeOf :: Binder' a -> DataType #

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

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

show :: Binder' a -> String #

showList :: [Binder' a] -> ShowS #

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete a b => ToConcrete (Binder' a) (Binder' b) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

DomainFree (NamedArg Binder)

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

DomainFull a

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

Instances

Instances details
Functor LamBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Foldable LamBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: LamBinding' a -> [a] #

null :: LamBinding' a -> Bool #

length :: LamBinding' a -> Int #

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

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

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

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

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

Traversable LamBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

ToConcrete LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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) 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 Binder] e

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

TLet Range [Declaration]

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

Instances

Instances details
Functor TypedBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Foldable TypedBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: TypedBinding' a -> [a] #

null :: TypedBinding' a -> Bool #

length :: TypedBinding' a -> Int #

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

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

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

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

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

Traversable TypedBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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) 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

Instances details
Functor FieldAssignment' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable FieldAssignment' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: FieldAssignment' a -> [a] #

null :: FieldAssignment' a -> Bool #

length :: FieldAssignment' a -> Int #

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

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

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

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

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

Traversable FieldAssignment' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

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 :: forall r r'. (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

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

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

Defined in Agda.Syntax.Abstract.Views

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

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

Instances details
Eq ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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 #

Instances

Instances details
Eq BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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.Pretty

NFData BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: BoundName -> () #

NFData Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> () #

Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

KillRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToConcrete BindName BoundName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 TacticAttribute Name Expr 
FieldSig IsInstance TacticAttribute Name (Arg 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 Range [FieldSignature] 
FunClause LHS RHS WhereClause Bool 
DataSig Range Name [LamBinding] Expr

lone data signature in mutual block

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

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

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

Instances details
Eq Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

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, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Instances details
Eq ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Instances details
Functor AsName' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable AsName' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: AsName' a -> [a] #

null :: AsName' a -> Bool #

length :: AsName' a -> Int #

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

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

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

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

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

Traversable AsName' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

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

Instances details
Eq LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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 Source # 
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

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

Instances details
Eq Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

IsWithP Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

HasEllipsis Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

IsEllipsis Pattern Source #

Is the pattern just ...?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

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

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pattern (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete (Maybe Pattern) (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Instances details
Eq LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Data LHSCore 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) -> LHSCore -> c LHSCore #

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

toConstr :: LHSCore -> Constr #

dataTypeOf :: LHSCore -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> LHSCore -> LHSCore #

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

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

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

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

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

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

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

Show LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

observeHiding :: Expr -> WithHiding Expr Source #

Observe the hiding status of an expression

data LamClause Source #

Constructors

LamClause 

Fields

Instances

Instances details
Eq LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Instances details
Functor RHS' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Show RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

Foldable RHS' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: RHS' a -> [a] #

null :: RHS' a -> Bool #

length :: RHS' a -> Int #

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

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

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

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

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

Traversable RHS' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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) 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

Instances details
Functor WhereClause' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Show WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Foldable WhereClause' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: WhereClause' a -> [a] #

null :: WhereClause' a -> Bool #

length :: WhereClause' a -> Int #

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

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

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

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

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

Traversable WhereClause' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

Data 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 :: forall r r'. (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) 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

Instances details
Eq DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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 RString QName 
RewritePragma Range Range [QName]

Second Range is for REWRITE keyword.

ForeignPragma Range RString String

first string is backend name

CompilePragma Range RString QName String

first string is backend name

StaticPragma Range QName 
InlinePragma Range Bool QName

INLINE or NOINLINE

ImpossiblePragma Range

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

WarningOnImport Range String

Applies to the current module

InjectivePragma Range QName

Mark a definition as injective for the pattern matching unifier.

DisplayPragma Range Pattern Expr

Display lhs as rhs (modifies the printer).

CatchallPragma Range

Applies to the following function clause.

TerminationCheckPragma Range (TerminationCheck Name)

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

NoCoverageCheckPragma Range

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

NoPositivityCheckPragma Range

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

PolarityPragma Range Name [Occurrence] 
NoUniverseCheckPragma Range

Applies to the following data/record type.

Instances

Instances details
Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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 :: forall r r'. (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 Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Instances details
Functor ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

Foldable ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

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

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

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

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

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

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

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

toList :: ThingWithFixity a -> [a] #

null :: ThingWithFixity a -> Bool #

length :: ThingWithFixity a -> Int #

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

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

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

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

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

Traversable ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

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

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

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 :: forall r r'. (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

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

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

LensFixity (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

data HoleContent' qn p e Source #

Extended content of an interaction hole.

Constructors

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

Instances

Instances details
ToAbstract HoleContent HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Functor (HoleContent' qn p) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable (HoleContent' qn p) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Traversable (HoleContent' qn p) Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

topLevelModuleName :: Module -> TopLevelModuleName Source #

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]) 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.