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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract

Contents

Description

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

Synopsis

Documentation

data Expr Source #

Expressions after scope checking (operators parsed, names resolved).

Constructors

Var Name

Bound variable.

Def QName

Constant: axiom, function, data or record type.

Proj ProjOrigin AmbiguousQName

Projection (overloaded).

Con AmbiguousQName

Constructor (overloaded).

PatternSyn QName

Pattern synonym.

Macro QName

Macro.

Lit Literal

Literal.

QuestionMark MetaInfo InteractionId

Meta variable for interaction. The InteractionId is usually identical with the metaNumber of MetaInfo. However, if you want to print an interaction meta as just ? instead of ?n, you should set the metaNumber to Nothing while keeping the InteractionId.

Underscore MetaInfo

Meta variable for hidden argument (must be inferred locally).

Dot ExprInfo Expr

.e, for postfix projection.

App ExprInfo Expr (NamedArg Expr)

Ordinary (binary) application.

WithApp ExprInfo Expr [Expr]

With application.

Lam ExprInfo LamBinding Expr

λ bs → e.

AbsurdLam ExprInfo Hiding

λ() or λ{}.

ExtendedLam ExprInfo DefInfo QName [Clause] 
Pi ExprInfo Telescope Expr

Dependent function space Γ → A.

Fun ExprInfo (Arg Expr) Expr

Non-dependent function space.

Set ExprInfo Integer

Set, Set1, Set2, ...

Prop ExprInfo

Prop (no longer supported, used as dummy type).

Let ExprInfo [LetBinding] Expr

let bs in e.

ETel Telescope

Only used when printing telescopes.

Rec ExprInfo RecordAssigns

Record construction.

RecUpdate ExprInfo Expr Assigns

Record update.

ScopedExpr ScopeInfo Expr

Scope annotation.

QuoteGoal ExprInfo Name Expr

Binds Name to current type in Expr.

QuoteContext ExprInfo

Returns the current context.

Quote ExprInfo

Quote an identifier QName.

QuoteTerm ExprInfo

Quote a term.

Unquote ExprInfo

The splicing construct: unquote ...

Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]
tactic e x1 .. xn | y1 | .. | yn
DontCare Expr

For printing DontCare from Syntax.Internal.

Instances

Eq Expr Source #

Does not compare ScopeInfo fields. Does not distinguish between prefix and postfix projections.

Methods

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

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

Show Expr Source # 

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

KillRange Expr Source # 
HasRange Expr Source # 

Methods

getRange :: Expr -> Range Source #

Underscore Expr Source # 
IsProjP Expr Source # 
SubstExpr Assign Source # 

Methods

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

SubstExpr Expr Source # 

Methods

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

AllNames Expr Source # 

Methods

allNames :: Expr -> Seq QName Source #

ExprLike Expr Source # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr Source #

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

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

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

ExpandPatternSynonyms Pattern Source # 
PrettyTCM Expr Source # 

Methods

prettyTCM :: Expr -> TCM Doc Source #

IsFlexiblePattern Pattern Source # 
UniverseBi Declaration Pattern Source # 
UniverseBi Declaration Expr Source # 

Methods

universeBi :: Declaration -> [Expr] #

ToConcrete Pattern Pattern Source # 
ToConcrete LHSCore Pattern Source # 
ToConcrete Expr Expr Source # 
ToAbstract Literal Expr Source # 
ToAbstract Sort Expr Source # 
ToAbstract Term Expr Source # 
Reify MetaId Expr Source # 
Reify Literal Expr Source # 
Reify Level Expr Source # 
Reify Sort Expr Source # 
Reify Type Expr Source # 
Reify Term Expr Source # 
Reify Expr Expr Source # 
Reify DisplayTerm Expr Source # 
ToAbstract Expr Expr Source # 
ToAbstract OldQName Expr Source # 
ToAbstract Pattern (Names, Pattern) Source # 
ToAbstract [Arg Term] [NamedArg Expr] Source # 
ToAbstract (Pattern' Expr) (Pattern' Expr) Source # 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # 
ToAbstract (Expr, Elims) Expr Source # 
ToAbstract (Expr, Elim) Expr Source # 

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

data Axiom Source #

Is a type signature a postulate or a function signature?

Constructors

FunSig

A function signature.

NoFunSig

Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally).

Instances

Eq Axiom Source # 

Methods

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

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

Ord Axiom Source # 

Methods

compare :: Axiom -> Axiom -> Ordering #

(<) :: Axiom -> Axiom -> Bool #

(<=) :: Axiom -> Axiom -> Bool #

(>) :: Axiom -> Axiom -> Bool #

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

max :: Axiom -> Axiom -> Axiom #

min :: Axiom -> Axiom -> Axiom #

Show Axiom Source # 

Methods

showsPrec :: Int -> Axiom -> ShowS #

show :: Axiom -> String #

showList :: [Axiom] -> ShowS #

type Ren a = [(a, a)] Source #

Renaming (generic).

data Declaration Source #

Constructors

Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr

Type signature (can be irrelevant, but not hidden).

The fourth argument contains an optional assignment of polarities to arguments.

Field DefInfo QName (Arg Expr)

record field

Primitive DefInfo QName Expr

primitive function

Mutual MutualInfo [Declaration]

a bunch of mutually recursive definitions

Section ModuleInfo ModuleName [TypedBindings] [Declaration] 
Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective

The ImportDirective is for highlighting purposes.

Import ModuleInfo ModuleName ImportDirective

The ImportDirective is for highlighting purposes.

Pragma Range Pragma 
Open ModuleInfo ModuleName ImportDirective

only retained for highlighting purposes

FunDef DefInfo QName Delayed [Clause]

sequence of function clauses

DataSig DefInfo QName Telescope Expr

lone data signature ^ the LamBindings are DomainFree and binds the parameters of the datatype.

DataDef DefInfo QName [LamBinding] [Constructor]

the LamBindings are DomainFree and binds the parameters of the datatype.

RecSig DefInfo QName Telescope Expr

lone record signature

RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe Bool) (Maybe QName) [LamBinding] Expr [Declaration]

The Expr gives the constructor type telescope, (x1 : A1)..(xn : An) -> Prop, and the optional name is the constructor's name.

PatternSynDef QName [Arg Name] (Pattern' Void)

Only for highlighting purposes

UnquoteDecl MutualInfo [DefInfo] [QName] Expr 
UnquoteDef [DefInfo] [QName] Expr 
ScopedDecl ScopeInfo [Declaration]

scope annotation

Instances

Eq Declaration Source #

Does not compare ScopeInfo fields.

Show Declaration Source # 
KillRange Declaration Source # 
HasRange Declaration Source # 
GetDefInfo Declaration Source # 
AnyAbstract Declaration Source # 
AllNames Declaration Source # 
ExprLike Declaration Source # 
ShowHead Declaration Source # 
UniverseBi Declaration RString Source # 
UniverseBi Declaration AmbiguousQName Source # 
UniverseBi Declaration ModuleName Source # 
UniverseBi Declaration QName Source # 

Methods

universeBi :: Declaration -> [QName] #

UniverseBi Declaration ModuleInfo Source # 
UniverseBi Declaration Pattern Source # 
UniverseBi Declaration TypedBinding Source # 
UniverseBi Declaration LamBinding Source # 
UniverseBi Declaration LetBinding Source # 
UniverseBi Declaration Declaration Source # 
UniverseBi Declaration Expr Source # 

Methods

universeBi :: Declaration -> [Expr] #

ToAbstract NiceDeclaration Declaration Source # 
UniverseBi Declaration (Pattern' Void) Source # 
ToConcrete Declaration [Declaration] Source # 
ToConcrete (Constr Constructor) Declaration Source # 
ToAbstract [Declaration] [Declaration] Source # 

class GetDefInfo a where Source #

Minimal complete definition

getDefInfo

data LetBinding Source #

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo Name Expr Expr
LetBind info rel name type defn
LetPatBind LetInfo Pattern Expr

Irrefutable pattern binding.

LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective

LetApply mi newM (oldM args) renamings dir. The ImportDirective is for highlighting purposes.

LetOpen ModuleInfo ModuleName ImportDirective

only for highlighting and abstractToConcrete

LetDeclaredVariable Name

Only used for highlighting. Refers to the first occurrence of x in let x : A; x = e.

Instances

Eq LetBinding Source # 
Show LetBinding Source # 
KillRange LetBinding Source # 
HasRange LetBinding Source # 
SubstExpr LetBinding Source # 
AllNames LetBinding Source # 
ExprLike LetBinding Source # 
UniverseBi Declaration LetBinding Source # 
ToConcrete LetBinding [Declaration] Source # 
ToAbstract LetDef [LetBinding] Source # 
ToAbstract LetDefs [LetBinding] Source # 
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree ArgInfo Name

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

DomainFull TypedBindings

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

data TypedBindings Source #

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

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

Instances

Eq TypedBindings Source # 
Show TypedBindings Source # 
KillRange TypedBindings Source # 
HasRange TypedBindings Source # 
LensHiding TypedBindings Source # 
SubstExpr TypedBindings Source # 
AllNames TypedBindings Source # 
ExprLike TypedBindings Source # 
Reify Telescope Telescope Source # 
ToAbstract TypedBindings TypedBindings Source # 
ToConcrete TypedBindings [TypedBindings] Source # 
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings Source # 

data TypedBinding Source #

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

  1. We would have to typecheck the type A several times.
  2. If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

TBind Range [WithHiding Name] Expr

As in telescope (x y z : A) or type (x y z : A) -> B.

TLet Range [LetBinding]

E.g. (let x = e) or (let open M).

Instances

data Clause' lhs Source #

We could throw away where clauses at this point and translate them to let. It's not obvious how to remember that the let was really a where clause though, so for the time being we keep it here.

Constructors

Clause 

Fields

Instances

Functor Clause' Source # 

Methods

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

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

Foldable Clause' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: Clause' a -> Bool #

length :: Clause' a -> Int #

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

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

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

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

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

Traversable Clause' Source # 

Methods

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

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

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

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

AllNames Clause Source # 
LHSToSpine Clause SpineClause Source #

Clause instance.

Reify NamedClause Clause Source # 
ToAbstract Clause Clause Source # 
Eq lhs => Eq (Clause' lhs) Source # 

Methods

(==) :: Clause' lhs -> Clause' lhs -> Bool #

(/=) :: Clause' lhs -> Clause' lhs -> Bool #

Show lhs => Show (Clause' lhs) Source # 

Methods

showsPrec :: Int -> Clause' lhs -> ShowS #

show :: Clause' lhs -> String #

showList :: [Clause' lhs] -> ShowS #

KillRange a => KillRange (Clause' a) Source # 
HasRange a => HasRange (Clause' a) Source # 

Methods

getRange :: Clause' a -> Range Source #

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

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a) Source #

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

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

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

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

data RHS Source #

Constructors

RHS 

Fields

AbsurdRHS 
WithRHS QName [Expr] [Clause]

The QName is the name of the with function.

RewriteRHS 

Fields

data SpineLHS Source #

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as ProjP d.

Constructors

SpineLHS 

Fields

data LHS Source #

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

LHS 

Fields

Instances

Eq LHS Source # 

Methods

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

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

Show LHS Source # 

Methods

showsPrec :: Int -> LHS -> ShowS #

show :: LHS -> String #

showList :: [LHS] -> ShowS #

KillRange LHS Source # 
HasRange LHS Source # 

Methods

getRange :: LHS -> Range Source #

AllNames Clause Source # 
ExprLike LHS Source # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS Source #

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

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

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

LHSToSpine LHS SpineLHS Source #

LHS instance.

LHSToSpine Clause SpineClause Source #

Clause instance.

ToConcrete LHS LHS Source # 
Reify NamedClause Clause Source # 
ToAbstract Clause Clause Source # 
ToAbstract LeftHandSide LHS Source # 
ToAbstract (QNamed Clause) Clause Source # 
Reify (QNamed Clause) Clause Source # 
ToAbstract [QNamed Clause] [Clause] Source # 

data LHSCore' e Source #

The lhs minus with-patterns in projection-application view. Parameterised over the type e of dot patterns.

Constructors

LHSHead

The head applied to ordinary patterns.

Fields

LHSProj

Projection

Fields

Instances

Functor LHSCore' Source # 

Methods

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

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

Foldable LHSCore' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: LHSCore' a -> Bool #

length :: LHSCore' a -> Int #

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

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

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

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

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

Traversable LHSCore' Source # 

Methods

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

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

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

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

ToConcrete LHSCore Pattern Source # 
ToAbstract LHSCore (LHSCore' Expr) Source # 
Eq e => Eq (LHSCore' e) Source # 

Methods

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

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

Show e => Show (LHSCore' e) Source # 

Methods

showsPrec :: Int -> LHSCore' e -> ShowS #

show :: LHSCore' e -> String #

showList :: [LHSCore' e] -> ShowS #

KillRange e => KillRange (LHSCore' e) Source # 
HasRange (LHSCore' e) Source # 

Methods

getRange :: LHSCore' e -> Range Source #

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

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source #

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

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

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

ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # 

class LHSToSpine a b where Source #

Convert a focused lhs to spine view and back.

Minimal complete definition

lhsToSpine, spineToLhs

Methods

lhsToSpine :: a -> b Source #

spineToLhs :: b -> a Source #

Instances

LHSToSpine LHS SpineLHS Source #

LHS instance.

LHSToSpine Clause SpineClause Source #

Clause instance.

LHSToSpine a b => LHSToSpine [a] [b] Source #

List instance (for clauses).

Methods

lhsToSpine :: [a] -> [b] Source #

spineToLhs :: [b] -> [a] Source #

lhsCoreApp :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source #

Add applicative patterns (non-projection patterns) to the right.

lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e Source #

Add projection and applicative patterns to the right.

lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e] Source #

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern Source #

Used in AbstractToConcrete.

Patterns

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP Name 
ConP ConPatInfo AmbiguousQName [NamedArg (Pattern' e)] 
ProjP PatInfo ProjOrigin AmbiguousQName

Destructor pattern d.

DefP PatInfo AmbiguousQName [NamedArg (Pattern' e)]

Defined pattern: function definition f ps. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.

WildP PatInfo

Underscore pattern entered by user. Or generated at type checking for implicit arguments.

AsP PatInfo Name (Pattern' e) 
DotP PatInfo Origin e 
AbsurdP PatInfo 
LitP Literal 
PatternSynP PatInfo QName [NamedArg (Pattern' e)] 
RecP PatInfo [FieldAssignment' (Pattern' e)] 

Instances

Functor Pattern' Source # 

Methods

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

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

Foldable Pattern' Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool #

length :: Pattern' a -> Int #

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

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

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

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

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

Traversable Pattern' Source # 

Methods

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

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

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

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

ExpandPatternSynonyms Pattern Source # 
IsFlexiblePattern Pattern Source # 
UniverseBi Declaration Pattern Source # 
ToConcrete Pattern Pattern Source # 
UniverseBi Declaration (Pattern' Void) Source # 
ToAbstract Pattern (Pattern' Expr) Source # 
ToAbstract Pattern (Names, Pattern) Source # 
Eq e => Eq (Pattern' e) Source # 

Methods

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

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

Show e => Show (Pattern' e) Source # 

Methods

showsPrec :: Int -> Pattern' e -> ShowS #

show :: Pattern' e -> String #

showList :: [Pattern' e] -> ShowS #

KillRange e => KillRange (Pattern' e) Source # 
SetRange (Pattern' a) Source # 

Methods

setRange :: Range -> Pattern' a -> Pattern' a Source #

HasRange (Pattern' e) Source # 

Methods

getRange :: Pattern' e -> Range Source #

IsProjP (Pattern' e) Source # 
IsProjP e => MaybePostfixProjP (Pattern' e) Source # 
ExprLike a => ExprLike (Pattern' a) Source # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source #

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

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

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

NamesIn (Pattern' a) Source # 

Methods

namesIn :: Pattern' a -> Set QName Source #

ToAbstract (Pattern' Expr) (Pattern' Expr) Source # 

class AllNames a where Source #

Extracts all the names which are declared in a Declaration. This does not include open public or let expressions, but it does include local modules, where clauses and the names of extended lambdas.

Minimal complete definition

allNames

Methods

allNames :: a -> Seq QName Source #

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

Precondition: The declaration has to be a (scoped) Axiom.

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Minimal complete definition

anyAbstract

Methods

anyAbstract :: a -> Bool Source #

nameExpr :: AbstractName -> Expr Source #

Turn an AbstractName to an expression.

class SubstExpr a where Source #

Minimal complete definition

substExpr

Methods

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

Instances

SubstExpr Name Source # 

Methods

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

SubstExpr ModuleName Source # 
SubstExpr TypedBinding Source # 
SubstExpr TypedBindings Source # 
SubstExpr LetBinding Source # 
SubstExpr Assign Source # 

Methods

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

SubstExpr Expr Source # 

Methods

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

SubstExpr a => SubstExpr [a] Source # 

Methods

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

SubstExpr a => SubstExpr (Arg a) Source # 

Methods

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

(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source # 

Methods

substExpr :: [(Name, Expr)] -> Either a b -> Either a b Source #

(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source # 

Methods

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

SubstExpr a => SubstExpr (Named name a) Source # 

Methods

substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #

insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) Source #