Agda-2.5.2: 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 #

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

NFData Expr #

Ranges are not forced.

Methods

rnf :: Expr -> () #

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

Methods

getRange :: RHS -> Range #

HasRange TypedBinding # 
HasRange TypedBindings # 
HasRange LamBinding # 

Methods

getRange :: LamBinding -> Range #

HasRange Expr # 

Methods

getRange :: Expr -> Range #

LensRelevance TypedBindings # 
LensHiding TypedBindings # 
LensHiding LamBinding # 
ExprLike TypedBindings # 
ExprLike LamBinding # 

Methods

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

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

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

ExprLike Expr # 

Methods

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

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

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

ExprLike FieldAssignment # 
IsExpr Expr # 
ToConcrete InteractionId Expr # 
ToConcrete TypedBinding TypedBinding # 
ToConcrete Expr Expr # 
ToConcrete NamedMeta Expr # 
ToAbstract RHS AbstractRHS # 
ToAbstract TypedBinding TypedBinding # 
ToAbstract TypedBindings TypedBindings # 
ToAbstract LamBinding LamBinding # 
ToAbstract Expr Expr # 

Methods

toAbstract :: Expr -> ScopeM Expr #

ToConcrete TypedBindings [TypedBindings] # 
ToConcrete LamBinding [LamBinding] # 
ToAbstract LHSCore (LHSCore' Expr) # 
ToAbstract Pattern (Pattern' Expr) # 
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) # 

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration]) #

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #

ToAbstract (Pattern' Expr) (Pattern' Expr) # 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) # 

data OpApp e #

Constructors

SyntaxBindingLambda Range [LamBinding] e

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

Ordinary e 

Instances

Functor OpApp # 

Methods

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

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

Foldable OpApp # 

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 # 

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

NFData a => NFData (OpApp a) #

Ranges are not forced.

Methods

rnf :: OpApp a -> () #

KillRange e => KillRange (OpApp e) # 

Methods

killRange :: KillRangeT (OpApp e) #

HasRange e => HasRange (OpApp e) # 

Methods

getRange :: OpApp e -> Range #

ExprLike a => ExprLike (OpApp a) # 

Methods

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

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

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

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

data AppView #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr] 

Bindings

type LamBinding = LamBinding' TypedBindings #

A lambda binding is either domain free or typed.

data LamBinding' a #

Constructors

DomainFree ArgInfo BoundName

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

DomainFull a

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

Instances

Functor LamBinding' # 

Methods

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

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

Foldable LamBinding' # 

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

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 # 
HasRange LamBinding # 

Methods

getRange :: LamBinding -> Range #

LensHiding LamBinding # 
ExprLike LamBinding # 

Methods

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

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

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

ToAbstract LamBinding LamBinding # 
ToConcrete LamBinding [LamBinding] # 
NFData a => NFData (LamBinding' a) # 

Methods

rnf :: LamBinding' a -> () #

type TypedBindings = TypedBindings' TypedBinding #

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 #

Constructors

TypedBindings Range (Arg a)

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

Instances

Functor TypedBindings' # 

Methods

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

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

Foldable TypedBindings' # 

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

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 # 
KillRange LamBinding # 
SetRange TypedBindings # 
HasRange TypedBindings # 
HasRange LamBinding # 

Methods

getRange :: LamBinding -> Range #

LensRelevance TypedBindings # 
LensHiding TypedBindings # 
LensHiding LamBinding # 
ExprLike TypedBindings # 
ExprLike LamBinding # 

Methods

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

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

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

ToAbstract TypedBindings TypedBindings # 
ToAbstract LamBinding LamBinding # 
ToConcrete TypedBindings [TypedBindings] # 
ToConcrete LamBinding [LamBinding] # 
NFData a => NFData (TypedBindings' a) #

Ranges are not forced.

Methods

rnf :: TypedBindings' a -> () #

type TypedBinding = TypedBinding' Expr #

A typed binding.

data TypedBinding' e #

Constructors

TBind Range [WithHiding BoundName] e

Binding (x1 ... xn : A).

TLet Range [Declaration]

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

Instances

Functor TypedBinding' # 

Methods

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

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

Foldable TypedBinding' # 

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

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 # 
KillRange TypedBindings # 
KillRange LamBinding # 
SetRange TypedBindings # 
HasRange TypedBinding # 
HasRange TypedBindings # 
HasRange LamBinding # 

Methods

getRange :: LamBinding -> Range #

LensRelevance TypedBindings # 
LensHiding TypedBindings # 
LensHiding LamBinding # 
ExprLike TypedBindings # 
ExprLike LamBinding # 

Methods

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

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

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

ToConcrete TypedBinding TypedBinding # 
ToAbstract TypedBinding TypedBinding # 
ToAbstract TypedBindings TypedBindings # 
ToAbstract LamBinding LamBinding # 
ToConcrete TypedBindings [TypedBindings] # 
ToConcrete LamBinding [LamBinding] # 
NFData a => NFData (TypedBinding' a) #

Ranges are not forced.

Methods

rnf :: TypedBinding' a -> () #

ExprLike a => ExprLike (TypedBinding' a) # 

Methods

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

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

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

data FieldAssignment' a #

Constructors

FieldAssignment 

Fields

Instances

Functor FieldAssignment' # 

Methods

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

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

Foldable FieldAssignment' # 

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

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

Methods

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

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

Methods

rnf :: FieldAssignment' a -> () #

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

data BoundName #

Constructors

BName 

Fields

type Telescope = [TypedBindings] #

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

Declarations

data Declaration #

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

NFData Declaration #

Ranges are not forced.

Methods

rnf :: Declaration -> () #

KillRange Declaration # 
KillRange WhereClause # 
HasRange Declaration # 
HasRange WhereClause # 
ExprLike Declaration # 

Methods

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

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

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

ToConcrete LetBinding [Declaration] # 
ToConcrete Declaration [Declaration] # 
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) # 

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration]) #

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #

ToConcrete (Constr Constructor) Declaration # 
ToAbstract (TopLevel [Declaration]) TopLevelInfo #

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] # 
ToAbstract [Declaration] [Declaration] # 

type TypeSignature = Declaration #

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration #

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name #

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 #

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

data AsName #

Constructors

AsName 

Fields

  • asName :: Name

    The "as" name.

  • asRange :: Range

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

Instances

Show AsName # 
NFData AsName #

Ranges are not forced.

Methods

rnf :: AsName -> () #

KillRange AsName # 
HasRange AsName # 

Methods

getRange :: AsName -> Range #

type WithExpr = Expr #

data LHS #

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

NFData LHS #

Ranges are not forced.

Methods

rnf :: LHS -> () #

KillRange LHS # 
HasRange LHS # 

Methods

getRange :: LHS -> Range #

ExprLike LHS # 

Methods

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

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

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

ToConcrete LHS LHS # 
ToConcrete SpineLHS LHS # 

data Pattern #

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

0, 1, etc.

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

data LHSCore #

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

Constructors

LHSHead 
LHSProj 

Fields

type RHS = RHS' Expr #

data RHS' e #

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e 

Instances

Functor RHS' # 

Methods

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

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

Foldable RHS' # 

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

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 # 
HasRange RHS # 

Methods

getRange :: RHS -> Range #

ToAbstract RHS AbstractRHS # 
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) # 

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration]) #

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #

NFData a => NFData (RHS' a) # 

Methods

rnf :: RHS' a -> () #

ExprLike a => ExprLike (RHS' a) # 

Methods

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

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

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

data WhereClause' decls #

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

Methods

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

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

Foldable WhereClause' # 

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

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 # 
HasRange WhereClause # 
NFData a => NFData (WhereClause' a) # 

Methods

rnf :: WhereClause' a -> () #

Null (WhereClause' a) #

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

Methods

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

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

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

data ExprWhere #

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

Constructors

ExprWhere Expr WhereClause 

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

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

data ThingWithFixity x #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

Instances

Functor ThingWithFixity # 

Methods

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

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

Foldable ThingWithFixity # 

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 # 

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

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

topLevelModuleName :: Module -> TopLevelModuleName #

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

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

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

patternQNames :: Pattern -> [QName] #

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

Lenses