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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete

Contents

Description

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

Synopsis

Expressions

data Expr Source #

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName

ex: x

Lit Literal

ex: 1 or "foo"

QuestionMark Range (Maybe Nat)

ex: ? or {! ... !}

Underscore Range (Maybe String)

ex: _ or _A_5

RawApp Range [Expr]

before parsing operators

App Range Expr (NamedArg Expr)

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

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

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

WithApp Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg Range (Named_ Expr)

ex: {e} or {x=e}

InstanceArg Range (Named_ Expr)

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

Lam Range [LamBinding] Expr

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

AbsurdLam Range Hiding

ex: \ ()

ExtendedLam Range [(LHS, RHS, WhereClause, Bool)]

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

Fun Range Expr Expr

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

Pi Telescope Expr

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

Set Range

ex: Set

Prop Range

ex: Prop

SetN Range Integer

ex: Set0, Set1, ..

Rec Range RecordAssignments

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

RecUpdate Range Expr [FieldAssignment]

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

Let Range [Declaration] Expr

ex: let Ds in e

Paren Range Expr

ex: (e)

IdiomBrackets Range Expr

ex: (| e |)

Absurd Range

ex: () or {}, only in patterns

As Range Name Expr

ex: x@p, only in patterns

Dot Range Expr

ex: .p, only in patterns

ETel Telescope

only used for printing telescopes

QuoteGoal Range Name Expr

ex: quoteGoal x in e

QuoteContext Range

ex: quoteContext

Quote Range

ex: quote, should be applied to a name

QuoteTerm Range

ex: quoteTerm, should be applied to a term

Tactic Range Expr [Expr]
tactic solve | subgoal1 | .. | subgoalN
Unquote Range

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

DontCare Expr

to print irrelevant things

Equal Range Expr Expr

ex: a = b, used internally in the parser

Instances

Data Expr Source # 

Methods

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

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

toConstr :: Expr -> Constr #

dataTypeOf :: Expr -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData Expr Source #

Ranges are not forced.

Methods

rnf :: Expr -> () #

KillRange RHS Source # 
KillRange TypedBinding Source # 
KillRange TypedBindings Source # 
KillRange LamBinding Source # 
KillRange Expr Source # 
SetRange TypedBindings Source # 
HasRange RHS Source # 

Methods

getRange :: RHS -> Range Source #

HasRange TypedBinding Source # 
HasRange TypedBindings Source # 
HasRange LamBinding Source # 
HasRange Expr Source # 

Methods

getRange :: Expr -> Range Source #

LensRelevance TypedBindings Source # 
LensHiding TypedBindings Source # 
LensHiding LamBinding Source # 
IsExpr Expr Source # 
ExprLike TypedBindings Source # 
ExprLike LamBinding Source # 
ExprLike Expr Source # 

Methods

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

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

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

ExprLike FieldAssignment Source # 
ToConcrete InteractionId Expr Source # 
ToConcrete TypedBinding TypedBinding Source # 
ToConcrete Expr Expr Source # 
ToConcrete NamedMeta Expr Source # 
ToAbstract RHS AbstractRHS Source # 
ToAbstract TypedBinding TypedBinding Source # 
ToAbstract TypedBindings TypedBindings Source # 
ToAbstract LamBinding LamBinding Source # 
ToAbstract Expr Expr Source # 
ToConcrete TypedBindings [TypedBindings] Source # 
ToConcrete LamBinding [LamBinding] Source # 
ToAbstract LHSCore (LHSCore' Expr) Source # 
ToAbstract Pattern (Pattern' Expr) Source # 
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # 
ToAbstract (Pattern' Expr) (Pattern' Expr) Source # 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # 

data OpApp e Source #

Constructors

SyntaxBindingLambda Range [LamBinding] e

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

Ordinary e 

Instances

Functor OpApp Source # 

Methods

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

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

Foldable OpApp Source # 

Methods

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

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

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

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

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

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

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

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

toList :: OpApp a -> [a] #

null :: OpApp a -> Bool #

length :: OpApp a -> Int #

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

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

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

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

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

Traversable OpApp Source # 

Methods

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

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

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

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

Data e => Data (OpApp e) Source # 

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 a. (Data d, Data a) => c (t d a)) -> Maybe (c (OpApp e)) #

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

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

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

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

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

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

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

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

NFData a => NFData (OpApp a) Source #

Ranges are not forced.

Methods

rnf :: OpApp a -> () #

KillRange e => KillRange (OpApp e) Source # 
HasRange e => HasRange (OpApp e) Source # 

Methods

getRange :: OpApp e -> Range Source #

ExprLike a => ExprLike (OpApp a) Source # 

Methods

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

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

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

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

data AppView Source #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr] 

Bindings

type LamBinding = LamBinding' TypedBindings Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

DomainFree ArgInfo BoundName

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

DomainFull a

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

Instances

Functor LamBinding' Source # 

Methods

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

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

Foldable LamBinding' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: LamBinding' a -> Bool #

length :: LamBinding' a -> Int #

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

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

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

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

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

Traversable LamBinding' Source # 

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

KillRange LamBinding Source # 
HasRange LamBinding Source # 
LensHiding LamBinding Source # 
ExprLike LamBinding Source # 
ToAbstract LamBinding LamBinding Source # 
ToConcrete LamBinding [LamBinding] Source # 
Data a => Data (LamBinding' a) Source # 

Methods

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

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

toConstr :: LamBinding' a -> Constr #

dataTypeOf :: LamBinding' a -> DataType #

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

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

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

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

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

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

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

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

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

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

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

Methods

rnf :: LamBinding' a -> () #

type TypedBindings = TypedBindings' TypedBinding Source #

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

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

data TypedBindings' a Source #

Constructors

TypedBindings Range (Arg a)

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

Instances

Functor TypedBindings' Source # 

Methods

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

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

Foldable TypedBindings' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: TypedBindings' a -> Bool #

length :: TypedBindings' a -> Int #

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

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

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

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

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

Traversable TypedBindings' Source # 

Methods

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

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

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

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

KillRange TypedBindings Source # 
KillRange LamBinding Source # 
SetRange TypedBindings Source # 
HasRange TypedBindings Source # 
HasRange LamBinding Source # 
LensRelevance TypedBindings Source # 
LensHiding TypedBindings Source # 
LensHiding LamBinding Source # 
ExprLike TypedBindings Source # 
ExprLike LamBinding Source # 
ToAbstract TypedBindings TypedBindings Source # 
ToAbstract LamBinding LamBinding Source # 
ToConcrete TypedBindings [TypedBindings] Source # 
ToConcrete LamBinding [LamBinding] Source # 
Data a => Data (TypedBindings' a) Source # 

Methods

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

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

toConstr :: TypedBindings' a -> Constr #

dataTypeOf :: TypedBindings' a -> DataType #

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

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

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

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

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

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

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

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

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

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

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

Ranges are not forced.

Methods

rnf :: TypedBindings' a -> () #

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

Constructors

TBind Range [WithHiding BoundName] e

Binding (x1 ... xn : A).

TLet Range [Declaration]

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

Instances

Functor TypedBinding' Source # 

Methods

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

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

Foldable TypedBinding' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: TypedBinding' a -> Bool #

length :: TypedBinding' a -> Int #

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

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

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

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

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

Traversable TypedBinding' Source # 

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

KillRange TypedBinding Source # 
KillRange TypedBindings Source # 
KillRange LamBinding Source # 
SetRange TypedBindings Source # 
HasRange TypedBinding Source # 
HasRange TypedBindings Source # 
HasRange LamBinding Source # 
LensRelevance TypedBindings Source # 
LensHiding TypedBindings Source # 
LensHiding LamBinding Source # 
ExprLike TypedBindings Source # 
ExprLike LamBinding Source # 
ToConcrete TypedBinding TypedBinding Source # 
ToAbstract TypedBinding TypedBinding Source # 
ToAbstract TypedBindings TypedBindings Source # 
ToAbstract LamBinding LamBinding Source # 
ToConcrete TypedBindings [TypedBindings] Source # 
ToConcrete LamBinding [LamBinding] Source # 
Data e => Data (TypedBinding' e) Source # 

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 a. (Data d, Data a) => c (t d a)) -> Maybe (c (TypedBinding' e)) #

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

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

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

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

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

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

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

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

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

Ranges are not forced.

Methods

rnf :: TypedBinding' a -> () #

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

Methods

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

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

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

data FieldAssignment' a Source #

Constructors

FieldAssignment 

Fields

Instances

Functor FieldAssignment' Source # 

Methods

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

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

Foldable FieldAssignment' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: FieldAssignment' a -> Bool #

length :: FieldAssignment' a -> Int #

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

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

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

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

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

Traversable FieldAssignment' Source # 

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 # 
SubstExpr Assign Source # 

Methods

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

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

Methods

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

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

Eq a => Eq (FieldAssignment' a) Source # 
Data a => Data (FieldAssignment' a) Source # 

Methods

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

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

toConstr :: FieldAssignment' a -> Constr #

dataTypeOf :: FieldAssignment' a -> DataType #

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

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

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

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

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

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

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

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

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

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

Show a => Show (FieldAssignment' a) Source # 
NFData a => NFData (FieldAssignment' a) Source # 

Methods

rnf :: FieldAssignment' a -> () #

KillRange a => KillRange (FieldAssignment' a) Source # 
HasRange a => HasRange (FieldAssignment' a) Source # 
ExprLike a => ExprLike (FieldAssignment' a) Source # 
MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # 
NamesIn a => NamesIn (FieldAssignment' a) Source # 
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # 
ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) Source # 
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) Source # 

data ModuleAssignment Source #

Instances

Data ModuleAssignment Source # 

Methods

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

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

toConstr :: ModuleAssignment -> Constr #

dataTypeOf :: ModuleAssignment -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData ModuleAssignment Source # 

Methods

rnf :: ModuleAssignment -> () #

KillRange ModuleAssignment Source # 
HasRange ModuleAssignment Source # 
ExprLike ModuleAssignment Source # 
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 

data BoundName Source #

Constructors

BName 

Fields

Instances

Eq BoundName Source # 
Data BoundName Source # 

Methods

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

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

toConstr :: BoundName -> Constr #

dataTypeOf :: BoundName -> DataType #

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

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

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

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

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

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

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

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

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

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

Show BoundName Source # 
NFData BoundName Source # 

Methods

rnf :: BoundName -> () #

KillRange BoundName Source # 
HasRange BoundName Source # 
ToAbstract (NewName BoundName) Name Source # 

type Telescope = [TypedBindings] Source #

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

Declarations

data Declaration Source #

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

Constructors

TypeSig ArgInfo Name Expr

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

Field IsInstance Name (Arg Expr)

Record field, can be hidden and/or irrelevant.

FunClause LHS RHS WhereClause Bool 
DataSig Range Induction Name [LamBinding] Expr

lone data signature in mutual block

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

lone record signature in mutual block

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

The optional name is a name for the record constructor.

Infix Fixity [Name] 
Syntax Name Notation

notation declaration for a name

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

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

InstanceB Range [Declaration] 
Macro Range [Declaration] 
Postulate Range [TypeSignatureOrInstanceBlock] 
Primitive Range [TypeSignature] 
Open Range QName ImportDirective 
Import Range QName (Maybe AsName) !OpenShortHand ImportDirective 
ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective 
Module Range QName [TypedBindings] [Declaration] 
UnquoteDecl Range [Name] Expr 
UnquoteDef Range [Name] Expr 
Pragma Pragma 

Instances

Data Declaration Source # 

Methods

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

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

toConstr :: Declaration -> Constr #

dataTypeOf :: Declaration -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData Declaration Source #

Ranges are not forced.

Methods

rnf :: Declaration -> () #

KillRange Declaration Source # 
KillRange WhereClause Source # 
HasRange Declaration Source # 
HasRange WhereClause Source # 
ExprLike Declaration Source # 
ToConcrete LetBinding [Declaration] Source # 
ToConcrete Declaration [Declaration] Source # 
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # 
ToConcrete (Constr Constructor) Declaration Source # 
ToAbstract (TopLevel [Declaration]) TopLevelInfo Source #

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

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

data ModuleApplication Source #

Constructors

SectionApp Range [TypedBindings] Expr
tel. M args
RecordModuleIFS Range QName
M {{...}}

Instances

Data ModuleApplication Source # 

Methods

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

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

toConstr :: ModuleApplication -> Constr #

dataTypeOf :: ModuleApplication -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData ModuleApplication Source #

Ranges are not forced.

Methods

rnf :: ModuleApplication -> () #

KillRange ModuleApplication Source # 
HasRange ModuleApplication Source # 
ExprLike ModuleApplication Source # 
ToConcrete ModuleApplication 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 Source #

Constructors

AsName 

Fields

  • asName :: Name

    The "as" name.

  • asRange :: Range

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

Instances

Data AsName Source # 

Methods

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

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

toConstr :: AsName -> Constr #

dataTypeOf :: AsName -> DataType #

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

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

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

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

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

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

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

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

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

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

Show AsName Source # 
NFData AsName Source #

Ranges are not forced.

Methods

rnf :: AsName -> () #

KillRange AsName Source # 
HasRange AsName Source # 

data OpenShortHand Source #

Constructors

DoOpen 
DontOpen 

Instances

Eq OpenShortHand Source # 
Data OpenShortHand Source # 

Methods

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

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

toConstr :: OpenShortHand -> Constr #

dataTypeOf :: OpenShortHand -> DataType #

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

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

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

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

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

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

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

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

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

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

Show OpenShortHand Source # 

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, with-patterns, rewrite equations and with-expressions

Fields

Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]

new with-patterns, rewrite equations and with-expressions

Instances

Data LHS Source # 

Methods

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

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

toConstr :: LHS -> Constr #

dataTypeOf :: LHS -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData LHS Source #

Ranges are not forced.

Methods

rnf :: LHS -> () #

KillRange LHS Source # 
HasRange LHS Source # 

Methods

getRange :: LHS -> Range Source #

ExprLike LHS Source # 

Methods

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

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

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

ToConcrete LHS LHS Source # 
ToConcrete SpineLHS 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 [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 Origin Expr

.e (the Origin keeps track whether this dot pattern was written by the user or inserted by the system)

LitP Literal

0, 1, etc.

RecP Range [FieldAssignment' Pattern]
record {x = p; y = q}

Instances

Data Pattern Source # 

Methods

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

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

toConstr :: Pattern -> Constr #

dataTypeOf :: Pattern -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData Pattern Source #

Ranges are not forced.

Methods

rnf :: Pattern -> () #

KillRange Pattern Source # 
SetRange Pattern Source # 
HasRange Pattern Source # 
IsExpr Pattern Source # 
ToConcrete Pattern Pattern Source # 
ToConcrete LHSCore Pattern Source # 
ToAbstract Pattern (Pattern' Expr) Source # 

data LHSCore Source #

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

Constructors

LHSHead 
LHSProj 

Fields

data RHS' e Source #

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e 

Instances

Functor RHS' Source # 

Methods

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

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

Foldable RHS' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: RHS' a -> Bool #

length :: RHS' a -> Int #

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

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

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

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

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

Traversable RHS' Source # 

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

KillRange RHS Source # 
HasRange RHS Source # 

Methods

getRange :: RHS -> Range Source #

ToAbstract RHS AbstractRHS Source # 
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # 
Data e => Data (RHS' e) Source # 

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 a. (Data d, Data a) => c (t d a)) -> Maybe (c (RHS' e)) #

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

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

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

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

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

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

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

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

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

Methods

rnf :: RHS' a -> () #

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

Methods

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

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

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

data WhereClause' decls Source #

Constructors

NoWhere

No where clauses.

AnyWhere decls

Ordinary where.

SomeWhere Name Access decls

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

Instances

Functor WhereClause' Source # 

Methods

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

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

Foldable WhereClause' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: WhereClause' a -> Bool #

length :: WhereClause' a -> Int #

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

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

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

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

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

Traversable WhereClause' Source # 

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

KillRange WhereClause Source # 
HasRange WhereClause Source # 
Data decls => Data (WhereClause' decls) Source # 

Methods

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

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

toConstr :: WhereClause' decls -> Constr #

dataTypeOf :: WhereClause' decls -> DataType #

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

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

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

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

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

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

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

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

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

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

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

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.

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

Methods

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

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

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

data ExprWhere Source #

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

Constructors

ExprWhere Expr WhereClause 

data Pragma Source #

Instances

Data Pragma Source # 

Methods

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

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

toConstr :: Pragma -> Constr #

dataTypeOf :: Pragma -> DataType #

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

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

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

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

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

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

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

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

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

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

NFData Pragma Source #

Ranges are not forced.

Methods

rnf :: Pragma -> () #

KillRange Pragma Source # 
HasRange Pragma Source # 
ToConcrete RangeAndPragma Pragma Source # 
ToAbstract Pragma [Pragma] Source # 

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

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

data ThingWithFixity x Source #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

Instances

Functor ThingWithFixity Source # 

Methods

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

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

Foldable ThingWithFixity Source # 

Methods

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

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

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

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

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

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

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

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

toList :: ThingWithFixity a -> [a] #

null :: ThingWithFixity a -> Bool #

length :: ThingWithFixity a -> Int #

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

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

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

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

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

Traversable ThingWithFixity Source # 

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 # 

Methods

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

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

toConstr :: ThingWithFixity x -> Constr #

dataTypeOf :: ThingWithFixity x -> DataType #

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

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

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

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

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

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

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

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

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

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

Show x => Show (ThingWithFixity x) Source # 
KillRange x => KillRange (ThingWithFixity x) Source # 

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.

Pattern tools

patternNames :: Pattern -> [Name] Source #

Get all the identifiers in a pattern in left-to-right order.

patternQNames :: Pattern -> [QName] Source #

Get all the identifiers in a pattern in left-to-right order.

Lenses