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

type Args = [NamedArg Expr] #

data Expr #

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 #

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

Methods

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

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

Show Expr # 

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

KillRange Expr # 
HasRange Expr # 

Methods

getRange :: Expr -> Range #

Underscore Expr # 
IsProjP Expr # 
SubstExpr Assign # 

Methods

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

SubstExpr Expr # 

Methods

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

AllNames Expr # 

Methods

allNames :: Expr -> Seq QName #

ExprLike Expr # 

Methods

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

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

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

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

ExpandPatternSynonyms Pattern # 
PrettyTCM Expr # 

Methods

prettyTCM :: Expr -> TCM Doc #

IsFlexiblePattern Pattern # 
UniverseBi Declaration Pattern # 
UniverseBi Declaration Expr # 

Methods

universeBi :: Declaration -> [Expr] #

ToConcrete Pattern Pattern # 
ToConcrete LHSCore Pattern # 
ToConcrete Expr Expr # 
ToAbstract Literal Expr # 
ToAbstract Sort Expr # 
ToAbstract Term Expr # 
Reify MetaId Expr # 

Methods

reify :: MetaId -> TCM Expr #

reifyWhen :: Bool -> MetaId -> TCM Expr #

Reify Literal Expr # 
Reify Level Expr # 

Methods

reify :: Level -> TCM Expr #

reifyWhen :: Bool -> Level -> TCM Expr #

Reify Sort Expr # 

Methods

reify :: Sort -> TCM Expr #

reifyWhen :: Bool -> Sort -> TCM Expr #

Reify Type Expr # 

Methods

reify :: Type -> TCM Expr #

reifyWhen :: Bool -> Type -> TCM Expr #

Reify Term Expr # 

Methods

reify :: Term -> TCM Expr #

reifyWhen :: Bool -> Term -> TCM Expr #

Reify Expr Expr # 

Methods

reify :: Expr -> TCM Expr #

reifyWhen :: Bool -> Expr -> TCM Expr #

Reify DisplayTerm Expr # 
ToAbstract Expr Expr # 

Methods

toAbstract :: Expr -> ScopeM Expr #

ToAbstract OldQName Expr # 
ToAbstract Pattern (Names, Pattern) # 
ToAbstract [Arg Term] [NamedArg Expr] # 
ToAbstract (Pattern' Expr) (Pattern' Expr) # 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) # 
ToAbstract (Expr, Elims) Expr # 
ToAbstract (Expr, Elim) Expr # 

type Assign = FieldAssignment' Expr #

Record field assignment f = e.

type Assigns = [Assign] #

data Axiom #

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 # 

Methods

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

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

Ord Axiom # 

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 # 

Methods

showsPrec :: Int -> Axiom -> ShowS #

show :: Axiom -> String #

showList :: [Axiom] -> ShowS #

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

Renaming (generic).

data Declaration #

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 #

Does not compare ScopeInfo fields.

Show Declaration # 
KillRange Declaration # 
HasRange Declaration # 
GetDefInfo Declaration # 
AnyAbstract Declaration # 
AllNames Declaration # 
ExprLike Declaration # 

Methods

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

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

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

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

ShowHead Declaration # 
UniverseBi Declaration RString # 
UniverseBi Declaration AmbiguousQName # 
UniverseBi Declaration ModuleName # 
UniverseBi Declaration QName # 

Methods

universeBi :: Declaration -> [QName] #

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

Methods

universeBi :: Declaration -> [Expr] #

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

class GetDefInfo a where #

Minimal complete definition

getDefInfo

Methods

getDefInfo :: a -> Maybe DefInfo #

data LetBinding #

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.

data TypedBindings #

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

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

Instances

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

data TypedBinding #

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

data Clause' lhs #

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

Methods

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

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

Foldable Clause' # 

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

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 # 

Methods

allNames :: Clause -> Seq QName #

LHSToSpine Clause SpineClause #

Clause instance.

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

Methods

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

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

Show lhs => Show (Clause' lhs) # 

Methods

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

show :: Clause' lhs -> String #

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

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

Methods

getRange :: Clause' a -> Range #

ExprLike a => ExprLike (Clause' a) # 

Methods

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

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

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

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

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

data RHS #

Constructors

RHS 

Fields

AbsurdRHS 
WithRHS QName [Expr] [Clause]

The QName is the name of the with function.

RewriteRHS 

Fields

Instances

Eq RHS # 

Methods

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

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

Show RHS # 

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

KillRange RHS # 
HasRange RHS # 

Methods

getRange :: RHS -> Range #

AllNames RHS # 

Methods

allNames :: RHS -> Seq QName #

ExprLike RHS # 

Methods

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

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

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

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

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

Methods

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

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

data SpineLHS #

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 #

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

Constructors

LHS 

Fields

Instances

Eq LHS # 

Methods

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

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

Show LHS # 

Methods

showsPrec :: Int -> LHS -> ShowS #

show :: LHS -> String #

showList :: [LHS] -> ShowS #

KillRange LHS # 
HasRange LHS # 

Methods

getRange :: LHS -> Range #

AllNames Clause # 

Methods

allNames :: Clause -> Seq QName #

ExprLike LHS # 

Methods

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

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

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

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

LHSToSpine LHS SpineLHS #

LHS instance.

LHSToSpine Clause SpineClause #

Clause instance.

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

data LHSCore' e #

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

Methods

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

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

Foldable LHSCore' # 

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

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 # 
ToAbstract LHSCore (LHSCore' Expr) # 
Eq e => Eq (LHSCore' e) # 

Methods

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

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

Show e => Show (LHSCore' e) # 

Methods

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

show :: LHSCore' e -> String #

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

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

Methods

getRange :: LHSCore' e -> Range #

ExprLike a => ExprLike (LHSCore' a) # 

Methods

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

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

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

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

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

class LHSToSpine a b where #

Convert a focused lhs to spine view and back.

Minimal complete definition

lhsToSpine, spineToLhs

Methods

lhsToSpine :: a -> b #

spineToLhs :: b -> a #

Instances

LHSToSpine LHS SpineLHS #

LHS instance.

LHSToSpine Clause SpineClause #

Clause instance.

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

List instance (for clauses).

Methods

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

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

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

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

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

Add projection and applicative patterns to the right.

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

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern #

Used in AbstractToConcrete.

Patterns

data Pattern' e #

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

Methods

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

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

Foldable Pattern' # 

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

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 # 
IsFlexiblePattern Pattern # 
UniverseBi Declaration Pattern # 
ToConcrete Pattern Pattern # 
UniverseBi Declaration (Pattern' Void) # 
ToAbstract Pattern (Pattern' Expr) # 
ToAbstract Pattern (Names, Pattern) # 
Eq e => Eq (Pattern' e) # 

Methods

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

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

Show e => Show (Pattern' e) # 

Methods

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

show :: Pattern' e -> String #

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

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

Methods

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

HasRange (Pattern' e) # 

Methods

getRange :: Pattern' e -> Range #

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

Methods

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

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

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

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

NamesIn (Pattern' a) # 

Methods

namesIn :: Pattern' a -> Set QName #

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

class AllNames a where #

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 #

axiomName :: Declaration -> QName #

The name defined by the given axiom.

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

class AnyAbstract a where #

Are we in an abstract block?

In that case some definition is abstract.

Minimal complete definition

anyAbstract

Methods

anyAbstract :: a -> Bool #

Instances

nameExpr :: AbstractName -> Expr #

Turn an AbstractName to an expression.

app :: Expr -> [NamedArg Expr] -> Expr #

class SubstExpr a where #

Minimal complete definition

substExpr

Methods

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

Instances

SubstExpr Name # 

Methods

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

SubstExpr ModuleName # 

Methods

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

SubstExpr TypedBinding # 
SubstExpr TypedBindings # 
SubstExpr LetBinding # 

Methods

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

SubstExpr Assign # 

Methods

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

SubstExpr Expr # 

Methods

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

SubstExpr a => SubstExpr [a] # 

Methods

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

SubstExpr a => SubstExpr (Arg a) # 

Methods

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

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

Methods

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

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

Methods

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

SubstExpr a => SubstExpr (Named name a) # 

Methods

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

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