Agda-2.6.4.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

Quote Range

ex: quote, should be applied to a name

QuoteTerm Range

ex: quoteTerm, should be applied to a term

Tactic Range Expr

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

Unquote Range

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

DontCare Expr

to print irrelevant things

Equal Range Expr Expr

ex: a = b, used internally in the parser

Ellipsis Range

..., used internally to parse patterns.

KnownIdent NameKind QName

An identifier coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).

KnownOpApp NameKind Range QName (Set Name) OpAppArgs

An operator application coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).

Generalized Expr 

Instances

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Pretty Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

IsExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range Source #

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Show Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

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

Eq Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

EncodeTCM (OutputForm Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

type AbsOfCon Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data OpApp e Source #

Constructors

SyntaxBindingLambda Range (List1 LamBinding) e

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

Ordinary e 

Instances

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

Functor OpApp Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range Source #

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

Defined in Agda.Syntax.Concrete

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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

data AppView Source #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr] 

isPattern :: Expr -> Maybe Pattern Source #

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

observeHiding :: Expr -> WithHiding Expr Source #

Observe the hiding status of an expression

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

Observe the relevance status of an expression

observeModifiers :: Expr -> Arg Expr Source #

Observe various modifiers applied to an expression

exprToPatternWithHoles :: Expr -> Pattern Source #

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

Bindings

data Binder' a Source #

A Binder x@p, the pattern is optional

Constructors

Binder 

Instances

Instances details
HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

NFData Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> () #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 #

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

DomainFree (NamedArg Binder)

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

DomainFull a

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

Instances

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamBinding' a -> () #

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

Defined in Agda.Syntax.Concrete

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

dropTypeAndModality :: LamBinding -> [LamBinding] Source #

Drop type annotations and lets from bindings.

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

Constructors

TBind Range (List1 (NamedArg Binder)) e

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

TLet Range (List1 Declaration)

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

Instances

Instances details
LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

LensRelevance TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Functor TypedBinding' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: TypedBinding' a -> () #

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

Defined in Agda.Syntax.Concrete

type AbsOfCon LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data FieldAssignment' a Source #

Constructors

FieldAssignment 

Fields

Instances

Instances details
ExprLike FieldAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

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

Functor FieldAssignment' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

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

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (FieldAssignment' a) 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract.Views

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

Defined in Agda.Syntax.Abstract.Views

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete.Pattern

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

Defined in Agda.Syntax.Internal.Names

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

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.TypeChecking.Patterns.Abstract

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

Defined in Agda.TypeChecking.Serialise.Instances.Common

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

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

Defined in Agda.Syntax.Concrete

type ADotT (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (FieldAssignment' c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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

data ModuleAssignment Source #

Instances

Instances details
Pretty ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Show ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

NFData ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: ModuleAssignment -> () #

Eq ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete

type AbsOfCon ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data BoundName Source #

Instances

Instances details
Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Show BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

NFData Binder Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: Binder -> () #

NFData BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: BoundName -> () #

Eq BoundName 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)) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Telescope1 = List1 TypedBinding Source #

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

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

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

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

Smart constructor for Pi: check whether the Telescope is empty

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

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

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

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

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

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

Declarations

data Declaration Source #

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

Constructors

TypeSig ArgInfo TacticAttribute Name Expr

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

FieldSig IsInstance TacticAttribute Name (Arg Expr) 
Generalize Range [TypeSignature]

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

Field Range [FieldSignature] 
FunClause LHS RHS WhereClause Bool 
DataSig Range Erased Name [LamBinding] Expr

lone data signature in mutual block

Data Range Erased Name [LamBinding] Expr [TypeSignatureOrInstanceBlock] 
DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock] 
RecordSig Range Erased Name [LamBinding] Expr

lone record signature in mutual block

RecordDef Range Name RecordDirectives [LamBinding] [Declaration] 
Record Range Erased 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 Erased Name ModuleApplication !OpenShortHand ImportDirective 
Module Range Erased QName Telescope [Declaration] 
UnquoteDecl Range [Name] Expr
unquoteDecl xs = e
UnquoteDef Range [Name] Expr
unquoteDef xs = e
UnquoteData Range Name [Name] Expr
unquoteDecl data d constructor xs = e
Pragma Pragma 
Opaque Range [Declaration]
opaque ...
Unfolding Range [QName]
unfolding ...

Instances

Instances details
Pretty Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

FoldDecl Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

TraverseDecl Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Eq Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract (TopLevel [Declaration]) Source #

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (TopLevel [Declaration]) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

isRecordDirective :: Declaration -> Maybe RecordDirective Source #

Extract a record directive

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

Defined in Agda.Syntax.Concrete

KillRange RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Eq RecordDirective Source # 
Instance details

Defined in Agda.Syntax.Concrete

data ModuleApplication Source #

type TypeSignature = Declaration Source #

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration Source #

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name Source #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

type ImportedName = ImportedName' Name Name Source #

An imported name can be a module or a defined name.

data AsName' a Source #

The content of the as-clause of the import statement.

Constructors

AsName 

Fields

  • asName :: a

    The "as" name.

  • asRange :: Range

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

Instances

Instances details
HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Functor AsName' Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

NFData AsName Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> () #

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

Defined in Agda.Syntax.Concrete

Methods

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

show :: AsName' a -> String #

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

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

Defined in Agda.Syntax.Concrete

Methods

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

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

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

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

data OpenShortHand Source #

Constructors

DoOpen 
DontOpen 

Instances

Instances details
Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Generic OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Associated Types

type Rep OpenShortHand 
Instance details

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

NFData OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: OpenShortHand -> () #

Eq OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

type Rep OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

data LHS Source #

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

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

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

Constructors

LHS

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

Fields

Instances

Instances details
Pretty LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasEllipsis LHS Source #

Does the lhs contain an ellipsis?

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

hasEllipsis :: LHS -> Bool Source #

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range Source #

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Eq LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

data Pattern Source #

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP Bool QName

c or x

If the boolean is False, then the QName must not refer to a constructor or a pattern synonym. The value False is used when a hidden argument pun is expanded.

QuoteP Range
quote
AppP Pattern (NamedArg Pattern)

p p' or p {x = p'}

RawAppP Range (List2 Pattern)

p1..pn before parsing operators

OpAppP Range QName (Set Name) [NamedArg Pattern]

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

HiddenP Range (Named_ Pattern)

{p} or {x = p}

InstanceP Range (Named_ Pattern)

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

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

x@p unused

DotP Range Expr
.e
LitP Range Literal

0, 1, etc.

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

i = i1 i.e. cubical face lattice generator

EllipsisP Range (Maybe Pattern)

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

WithP Range Pattern

| p, for with-patterns.

Instances

Instances details
Pretty Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

IsExpr Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Operators.Parser

CPatternLike Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

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

IsWithP Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

HasRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

SetRange Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Eq Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LHSCore Source #

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

Constructors

LHSHead 
LHSProj 

Fields

LHSWith 

Fields

LHSEllipsis 

Fields

Instances

Instances details
Pretty LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Show LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Eq LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LamClause Source #

Constructors

LamClause 

Fields

Instances

Instances details
Pretty LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Show LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

NFData LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: LamClause -> () #

Eq LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

data RHS' e Source #

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e 

Instances

Instances details
Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range Source #

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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 #

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: RHS' a -> () #

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

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type WhereClause = WhereClause' [Declaration] Source #

where block following a clause.

data WhereClause' decls Source #

Constructors

NoWhere

No where clauses.

AnyWhere Range decls

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

SomeWhere Range Erased Name Access decls

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

Instances

Instances details
Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

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

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

Defined in Agda.Syntax.Concrete.Generic

Null (WhereClause' a) Source #

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

Instance details

Defined in Agda.Syntax.Concrete

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

Defined in Agda.Syntax.Concrete

Methods

rnf :: WhereClause' a -> () #

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

Defined in Agda.Syntax.Concrete

Methods

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

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

data ExprWhere Source #

An expression followed by a where clause. Currently only used to give better a better error message in interaction.

Constructors

ExprWhere Expr WhereClause 

data DoStmt Source #

Instances

Instances details
Pretty DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ExprLike DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

HasRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Show DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

NFData DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: DoStmt -> () #

Eq DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

data Pragma Source #

Constructors

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

Second Range is for REWRITE keyword.

ForeignPragma Range RString String

first string is backend name

CompilePragma Range RString QName String

first string is backend name

StaticPragma Range QName 
InlinePragma Range Bool QName

INLINE or NOINLINE

ImpossiblePragma Range [String]

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

EtaPragma Range QName

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

WarningOnUsage Range QName Text

Applies to the named function

WarningOnImport Range Text

Applies to the current module

InjectivePragma Range QName

Mark a definition as injective for the pattern matching unifier.

DisplayPragma Range Pattern Expr

Display lhs as rhs (modifies the printer).

CatchallPragma Range

Applies to the following function clause.

TerminationCheckPragma Range (TerminationCheck Name)

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

NoCoverageCheckPragma Range

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

NoPositivityCheckPragma Range

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

PolarityPragma Range Name [Occurrence] 
NoUniverseCheckPragma Range

Applies to the following data/record type.

NotProjectionLikePragma Range QName

Applies to the stated function

Instances

Instances details
Pretty Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

HasRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

ToAbstract Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete

Methods

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

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

type AbsOfCon Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data Module Source #

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

Constructors

Mod 

Instances

Instances details
Show Module Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

Instances

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

Functor ThingWithFixity Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

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

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

LensFixity (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

LensFixity' (ThingWithFixity a) Source # 
Instance details

Defined in Agda.Syntax.Fixity

Pretty (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Fixity

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

Defined in Agda.Syntax.Fixity

data HoleContent' qn nm p e Source #

Extended content of an interaction hole.

Constructors

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

Instances

Instances details
ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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 #

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

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