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

Agda.Syntax.Concrete

Description

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

Synopsis

Expressions

data Expr Source #

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName

ex: x

Lit Range Literal

ex: 1 or "foo"

QuestionMark Range (Maybe Nat)

ex: ? or {! ... !}

Underscore Range (Maybe String)

ex: _ or _A_5

RawApp Range (List2 Expr)

before parsing operators

App Range Expr (NamedArg Expr)

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

OpApp Range QName (Set Name) OpAppArgs

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

WithApp Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg Range (Named_ Expr)

ex: {e} or {x=e}

InstanceArg Range (Named_ Expr)

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

Lam Range (List1 LamBinding) Expr

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

AbsurdLam Range Hiding

ex: \ ()

ExtendedLam Range Erased (List1 LamClause)

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

Fun Range (Arg Expr) Expr

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

Pi Telescope1 Expr

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

Rec Range RecordAssignments

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

RecUpdate Range Expr [FieldAssignment]

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

Let Range (List1 Declaration) (Maybe Expr)

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

Paren Range Expr

ex: (e)

IdiomBrackets Range [Expr]

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

DoBlock Range (List1 DoStmt)

ex: do x <- m1; m2

Absurd Range

ex: () or {}, only in patterns

As Range Name Expr

ex: x@p, only in patterns

Dot Range Expr

ex: .p, only in patterns

DoubleDot Range Expr

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

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 #

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

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

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent Source #

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS Source #

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn Source #

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding Source #

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding Source #

ToAbstract Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr Source #

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) Source #

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) Source #

EncodeTCM (OutputForm Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data OpApp e Source #

Constructors

SyntaxBindingLambda Range (List1 LamBinding) e

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

Ordinary e 

Instances

Instances details
Functor OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Foldable OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

toList :: OpApp a -> [a] #

null :: OpApp a -> Bool #

length :: OpApp a -> Int #

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

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

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

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

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

Traversable OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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 #

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

traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a) 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.

exprToPatternWithHoles :: Expr -> Pattern Source #

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

Bindings

data Binder' a Source #

A Binder x@p, the pattern is optional

Constructors

Binder 

Instances

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

DomainFree (NamedArg Binder)

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

DomainFull a

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

Instances

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

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding Source #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

dropTypeAndModality :: LamBinding -> [LamBinding] Source #

Drop type annotations and lets from bindings.

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

Constructors

TBind Range (List1 (NamedArg Binder)) e

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

TLet Range (List1 Declaration)

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

Instances

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

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding Source #

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding Source #

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 #

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

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

type AbsOfCon TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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

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

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract.Views

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

Defined in Agda.Syntax.Abstract.Views

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (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

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> FieldAssignment' a -> m Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a) Source #

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

Defined in Agda.TypeChecking.Patterns.Abstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (FieldAssignment' c) Source #

type ADotT (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (FieldAssignment' c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon ModuleAssignment Source #

type AbsOfCon ModuleAssignment 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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

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

ToAbstract (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) Source #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Telescope1 = List1 TypedBinding Source #

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

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

We can try to get a Telescope from a [LamBinding]. If we have a type annotation already, we're happy. Otherwise we manufacture a binder with an underscore for the type.

makePi :: Telescope -> Expr -> Expr Source #

Smart constructor for Pi: check whether the Telescope is empty

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

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

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

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

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

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

Declarations

data RecordDirective Source #

Isolated record directives parsed as Declarations

Constructors

Induction (Ranged Induction)

Range of keyword [co]inductive.

Constructor Name IsInstance 
Eta (Ranged HasEta0)

Range of [no-]eta-equality keyword.

PatternOrCopattern Range

If declaration pattern is present, give its range.

Instances

Instances details
Eq RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

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

toConstr :: RecordDirective -> Constr #

dataTypeOf :: RecordDirective -> DataType #

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

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

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

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

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

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

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

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

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

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

Show RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

NFData RecordDirective Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: RecordDirective -> () #

KillRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

isRecordDirective :: Declaration -> Maybe RecordDirective Source #

Extract a record directive

data Declaration Source #

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

Constructors

TypeSig ArgInfo TacticAttribute Name Expr

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

FieldSig IsInstance TacticAttribute Name (Arg Expr) 
Generalize 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 RecordDirectives [LamBinding] [Declaration] 
Record Range Name RecordDirectives [LamBinding] Expr [Declaration] 
RecordDirective RecordDirective

Should not survive beyond the parser

Infix Fixity (List1 Name) 
Syntax Name Notation

notation declaration for a name

PatternSyn Range Name [Arg Name] Pattern 
Mutual Range [Declaration] 
InterleavedMutual Range [Declaration] 
Abstract Range [Declaration] 
Private Range Origin [Declaration]

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

InstanceB Range [Declaration]

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

LoneConstructor Range [Declaration] 
Macro Range [Declaration] 
Postulate Range [TypeSignatureOrInstanceBlock] 
Primitive Range [TypeSignature] 
Open Range QName ImportDirective 
Import Range QName (Maybe AsName) !OpenShortHand ImportDirective 
ModuleMacro Range 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 # 
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

ToAbstract (TopLevel [Declaration]) Source #

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (TopLevel [Declaration]) Source #

type AbsOfCon (TopLevel [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

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

Generic OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Associated Types

type Rep OpenShortHand :: Type -> Type #

NFData OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpenShortHand -> () #

Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

type Rep OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

data LHS Source #

Left hand sides can be written in infix style. For example:

n + suc m = suc (n + m)
(f ∘ g) x = f (g x)

We use fixity information to see which name is actually defined.

Constructors

LHS

Original pattern (including with-patterns), rewrite equations and with-expressions.

Fields

Instances

Instances details
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 #

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

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

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

p1..pn before parsing operators

OpAppP Range QName (Set Name) [NamedArg Pattern]

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

HiddenP Range (Named_ Pattern)

{p} or {x = p}

InstanceP Range (Named_ Pattern)

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

ParenP Range Pattern
(p)
WildP Range
_
AbsurdP Range
()
AsP Range Name Pattern

x@p unused

DotP Range Expr
.e
LitP Range Literal

0, 1, etc.

RecP Range [FieldAssignment' Pattern]
record {x = p; y = q}
EqualP Range [(Expr, Expr)]

i = i1 i.e. cubical face lattice generator

EllipsisP Range (Maybe Pattern)

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

WithP Range Pattern

| p, for with-patterns.

Instances

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

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent Source #

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn Source #

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern Source #

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LHSCore Source #

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

Constructors

LHSHead 
LHSProj 

Fields

LHSWith 

Fields

LHSEllipsis 

Fields

Instances

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore Source #

type AbsOfCon LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

observeHiding :: Expr -> WithHiding Expr Source #

Observe the hiding status of an expression

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

Observe the relevance status of an expression

observeModifiers :: Expr -> Arg Expr Source #

Observe various modifiers applied to an expression

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 #

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

traverseExpr :: Monad m => (Expr -> m Expr) -> LamClause -> m LamClause 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 Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS Source #

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 #

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

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

type AbsOfCon RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type WhereClause = WhereClause' [Declaration] Source #

where block following a clause.

data WhereClause' decls Source #

Constructors

NoWhere

No where clauses.

AnyWhere Range decls

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

SomeWhere Range Name Access decls

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

Instances

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

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 #

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

traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) 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 #

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 #

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

traverseExpr :: Monad m => (Expr -> m Expr) -> DoStmt -> m DoStmt 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 [String]

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

EtaPragma Range QName

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

WarningOnUsage Range QName Text

Applies to the named function

WarningOnImport Range Text

Applies to the current module

InjectivePragma Range QName

Mark a definition as injective for the pattern matching unifier.

DisplayPragma Range Pattern Expr

Display lhs as rhs (modifies the printer).

CatchallPragma Range

Applies to the following function clause.

TerminationCheckPragma Range (TerminationCheck Name)

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

NoCoverageCheckPragma Range

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

NoPositivityCheckPragma Range

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

PolarityPragma Range Name [Occurrence] 
NoUniverseCheckPragma Range

Applies to the following data/record type.

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

ToAbstract Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma Source #

type AbsOfCon Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data Module Source #

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

Constructors

Mod 

Instances

Instances details
Show Module Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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 nm p e Source #

Extended content of an interaction hole.

Constructors

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

Instances

Instances details
ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent Source #

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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.