Agda.Syntax.Abstract

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

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

Methods

killRange :: KillRangeT Expr

HasRange Expr

Methods

getRange :: Expr -> Range

Underscore Expr

Methods

underscore :: Expr

isUnderscore :: Expr -> Bool

IsProjP Expr

Methods

isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName)

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

Methods

expandPatternSynonyms :: Pattern -> TCM Pattern

PrettyTCM Expr

Methods

prettyTCM :: Expr -> TCM Doc

IsFlexiblePattern Pattern

Methods

maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Pattern -> TCM Bool

UniverseBi Declaration Pattern

Methods

universeBi :: Declaration -> [Pattern]

UniverseBi Declaration Expr

Methods

universeBi :: Declaration -> [Expr]

ToConcrete Pattern Pattern

Methods

toConcrete :: Pattern -> AbsToCon Pattern

bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete LHSCore Pattern

Methods

toConcrete :: LHSCore -> AbsToCon Pattern

bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete Expr Expr

Methods

toConcrete :: Expr -> AbsToCon Expr

bindToConcrete :: Expr -> (Expr -> AbsToCon b) -> AbsToCon b

ToAbstract Literal Expr

Methods

toAbstract :: Literal -> WithNames Expr

ToAbstract Sort Expr

Methods

toAbstract :: Sort -> WithNames Expr

ToAbstract Term Expr

Methods

toAbstract :: Term -> WithNames Expr

Reify MetaId Expr

Methods

reify :: MetaId -> TCM Expr

reifyWhen :: Bool -> MetaId -> TCM Expr

Reify Literal Expr

Methods

reify :: Literal -> TCM Expr

reifyWhen :: Bool -> Literal -> TCM 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

Methods

reify :: DisplayTerm -> TCM Expr

reifyWhen :: Bool -> DisplayTerm -> TCM Expr

ToAbstract Expr Expr

Methods

toAbstract :: Expr -> ScopeM Expr

ToAbstract OldQName Expr

Methods

toAbstract :: OldQName -> ScopeM Expr

ToAbstract Pattern (Names, Pattern)

Methods

toAbstract :: Pattern -> WithNames (Names, Pattern)

ToAbstract [Arg Term] [NamedArg Expr]

Methods

toAbstract :: [Arg Term] -> WithNames [NamedArg Expr]

ToAbstract (Pattern' Expr) (Pattern' Expr)

Methods

toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

Methods

toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr)

ToAbstract (Expr, Elims) Expr

Methods

toAbstract :: (Expr, Elims) -> WithNames Expr

ToAbstract (Expr, Elim) Expr

Methods

toAbstract :: (Expr, Elim) -> WithNames Expr

type Assign = FieldAssignment' Expr

Record field assignment f = e.

type Assigns = [Assign]

type RecordAssign = Either Assign ModuleName

type RecordAssigns = [RecordAssign]

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 ScopeCopyInfo

Constructors

ScopeCopyInfo

Fields

• renModules :: Ren ModuleName
• renNames :: Ren QName

Instances

Eq ScopeCopyInfo

Methods

(==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool

(/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool

Show ScopeCopyInfo

Methods

showsPrec :: Int -> ScopeCopyInfo -> ShowS

show :: ScopeCopyInfo -> String

showList :: [ScopeCopyInfo] -> ShowS

Pretty ScopeCopyInfo

Methods

pretty :: ScopeCopyInfo -> Doc

prettyPrec :: Int -> ScopeCopyInfo -> Doc

KillRange ScopeCopyInfo

Methods

killRange :: KillRangeT ScopeCopyInfo

initCopyInfo :: ScopeCopyInfo

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.

Methods

(==) :: Declaration -> Declaration -> Bool

(/=) :: Declaration -> Declaration -> Bool

Show Declaration

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

KillRange Declaration

Methods

killRange :: KillRangeT Declaration

HasRange Declaration

Methods

getRange :: Declaration -> Range

GetDefInfo Declaration

Methods

getDefInfo :: Declaration -> Maybe DefInfo

AnyAbstract Declaration

Methods

anyAbstract :: Declaration -> Bool

AllNames Declaration

Methods

allNames :: Declaration -> Seq QName

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

Methods

showHead :: Declaration -> String

UniverseBi Declaration RString

Methods

universeBi :: Declaration -> [RString]

UniverseBi Declaration AmbiguousQName

Methods

universeBi :: Declaration -> [AmbiguousQName]

UniverseBi Declaration ModuleName

Methods

universeBi :: Declaration -> [ModuleName]

UniverseBi Declaration QName

Methods

universeBi :: Declaration -> [QName]

UniverseBi Declaration ModuleInfo

Methods

universeBi :: Declaration -> [ModuleInfo]

UniverseBi Declaration Pattern

Methods

universeBi :: Declaration -> [Pattern]

UniverseBi Declaration TypedBinding

Methods

universeBi :: Declaration -> [TypedBinding]

UniverseBi Declaration LamBinding

Methods

universeBi :: Declaration -> [LamBinding]

UniverseBi Declaration LetBinding

Methods

universeBi :: Declaration -> [LetBinding]

UniverseBi Declaration Declaration

Methods

universeBi :: Declaration -> [Declaration]

UniverseBi Declaration Expr

Methods

universeBi :: Declaration -> [Expr]

ToAbstract NiceDeclaration Declaration

Methods

toAbstract :: NiceDeclaration -> ScopeM Declaration

UniverseBi Declaration (Pattern' Void)

Methods

universeBi :: Declaration -> [Pattern' Void]

ToConcrete Declaration [Declaration]

Methods

toConcrete :: Declaration -> AbsToCon [Declaration]

bindToConcrete :: Declaration -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToConcrete (Constr Constructor) Declaration

Methods

toConcrete :: Constr Constructor -> AbsToCon Declaration

bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b

ToAbstract [Declaration] [Declaration]

Methods

toAbstract :: [Declaration] -> ScopeM [Declaration]

class GetDefInfo a where

Minimal complete definition

getDefInfo

Methods

getDefInfo :: a -> Maybe DefInfo

Instances

GetDefInfo Declaration

Methods

getDefInfo :: Declaration -> Maybe DefInfo

type ImportDirective = ImportDirective' QName ModuleName

type Renaming = Renaming' QName ModuleName

type ImportedName = ImportedName' QName ModuleName

data ModuleApplication

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]

tel. M args: applies M to args and abstracts tel.

RecordModuleIFS ModuleName

M {{...}}

Instances

Eq ModuleApplication

Methods

(==) :: ModuleApplication -> ModuleApplication -> Bool

(/=) :: ModuleApplication -> ModuleApplication -> Bool

Show ModuleApplication

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

KillRange ModuleApplication

Methods

killRange :: KillRangeT ModuleApplication

AllNames ModuleApplication

Methods

allNames :: ModuleApplication -> Seq QName

ExprLike ModuleApplication

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

ToConcrete ModuleApplication ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon ModuleApplication

bindToConcrete :: ModuleApplication -> (ModuleApplication -> AbsToCon b) -> AbsToCon b

data Pragma

Constructors

OptionsPragma [String]

BuiltinPragma String Expr

BuiltinNoDefPragma String QName

Builtins that do not come with a definition, but declare a name for an Agda concept.

RewritePragma QName

CompiledPragma QName String

CompiledExportPragma QName String

CompiledDeclareDataPragma QName String

CompiledTypePragma QName String

CompiledDataPragma QName String [String]

CompiledEpicPragma QName String

CompiledJSPragma QName String

CompiledUHCPragma QName String

CompiledDataUHCPragma QName String [String]

StaticPragma QName

InlinePragma QName

DisplayPragma QName [NamedArg Pattern] Expr

Instances

Eq Pragma

Methods

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

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

Show Pragma

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

ExprLike Pragma

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> Pragma -> Pragma

ToAbstract Pragma [Pragma]

Methods

toAbstract :: Pragma -> ScopeM [Pragma]

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.

Instances

Eq LetBinding

Methods

(==) :: LetBinding -> LetBinding -> Bool

(/=) :: LetBinding -> LetBinding -> Bool

Show LetBinding

Methods

showsPrec :: Int -> LetBinding -> ShowS

show :: LetBinding -> String

showList :: [LetBinding] -> ShowS

KillRange LetBinding

Methods

killRange :: KillRangeT LetBinding

HasRange LetBinding

Methods

getRange :: LetBinding -> Range

SubstExpr LetBinding

Methods

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

AllNames LetBinding

Methods

allNames :: LetBinding -> Seq QName

ExprLike LetBinding

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding

UniverseBi Declaration LetBinding

Methods

universeBi :: Declaration -> [LetBinding]

ToConcrete LetBinding [Declaration]

Methods

toConcrete :: LetBinding -> AbsToCon [Declaration]

bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToAbstract LetDef [LetBinding]

Methods

toAbstract :: LetDef -> ScopeM [LetBinding]

ToAbstract LetDefs [LetBinding]

Methods

toAbstract :: LetDefs -> ScopeM [LetBinding]

ToAbstract ModuleAssignment (ModuleName, [LetBinding])

Methods

toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding])

type TypeSignature = Declaration

Only Axioms.

type Constructor = TypeSignature

type Field = TypeSignature

data LamBinding

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)

Instances

Eq LamBinding

Methods

(==) :: LamBinding -> LamBinding -> Bool

(/=) :: LamBinding -> LamBinding -> Bool

Show LamBinding

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

KillRange LamBinding

Methods

killRange :: KillRangeT LamBinding

HasRange LamBinding

Methods

getRange :: LamBinding -> Range

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

AllNames LamBinding

Methods

allNames :: LamBinding -> Seq QName

ExprLike LamBinding

Methods

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

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

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

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

UniverseBi Declaration LamBinding

Methods

universeBi :: Declaration -> [LamBinding]

ToAbstract LamBinding LamBinding

Methods

toAbstract :: LamBinding -> ScopeM LamBinding

ToConcrete LamBinding [LamBinding]

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding]

bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b

data TypedBindings

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

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

Instances

Eq TypedBindings

Methods

(==) :: TypedBindings -> TypedBindings -> Bool

(/=) :: TypedBindings -> TypedBindings -> Bool

Show TypedBindings

Methods

showsPrec :: Int -> TypedBindings -> ShowS

show :: TypedBindings -> String

showList :: [TypedBindings] -> ShowS

KillRange TypedBindings

Methods

killRange :: KillRangeT TypedBindings

HasRange TypedBindings

Methods

getRange :: TypedBindings -> Range

LensHiding TypedBindings

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

SubstExpr TypedBindings

Methods

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

AllNames TypedBindings

Methods

allNames :: TypedBindings -> Seq QName

ExprLike TypedBindings

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings

Reify Telescope Telescope

Methods

reify :: Telescope -> TCM Telescope

reifyWhen :: Bool -> Telescope -> TCM Telescope

ToAbstract TypedBindings TypedBindings

Methods

toAbstract :: TypedBindings -> ScopeM TypedBindings

ToConcrete TypedBindings [TypedBindings]

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings]

bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings

Methods

toAbstract :: (Dom r, Name) -> WithNames 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).

Instances

Eq TypedBinding

Methods

(==) :: TypedBinding -> TypedBinding -> Bool

(/=) :: TypedBinding -> TypedBinding -> Bool

Show TypedBinding

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

KillRange TypedBinding

Methods

killRange :: KillRangeT TypedBinding

HasRange TypedBinding

Methods

getRange :: TypedBinding -> Range

SubstExpr TypedBinding

Methods

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

AllNames TypedBinding

Methods

allNames :: TypedBinding -> Seq QName

ExprLike TypedBinding

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding

PrettyTCM TypedBinding

Methods

prettyTCM :: TypedBinding -> TCM Doc

UniverseBi Declaration TypedBinding

Methods

universeBi :: Declaration -> [TypedBinding]

ToConcrete TypedBinding TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon TypedBinding

bindToConcrete :: TypedBinding -> (TypedBinding -> AbsToCon b) -> AbsToCon b

ToAbstract TypedBinding TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM TypedBinding

type Telescope = [TypedBindings]

data NamedDotPattern

Constructors

NamedDot Name Term Type

Instances

Eq NamedDotPattern

Methods

(==) :: NamedDotPattern -> NamedDotPattern -> Bool

(/=) :: NamedDotPattern -> NamedDotPattern -> Bool

Show NamedDotPattern

Methods

showsPrec :: Int -> NamedDotPattern -> ShowS

show :: NamedDotPattern -> String

showList :: [NamedDotPattern] -> ShowS

KillRange NamedDotPattern

Methods

killRange :: KillRangeT NamedDotPattern

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

• clauseLHS :: lhs
• clauseNamedDots :: [NamedDotPattern]

  Only in with-clauses where we inherit some already checked dot patterns from the parent. These live in the context of the parent clause left-hand side.

• clauseRHS :: RHS
• clauseWhereDecls :: [Declaration]
• clauseCatchall :: Bool

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.

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

Reify NamedClause Clause

Methods

reify :: NamedClause -> TCM Clause

reifyWhen :: Bool -> NamedClause -> TCM Clause

ToAbstract Clause Clause

Methods

toAbstract :: Clause -> ScopeM 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)

Methods

killRange :: KillRangeT (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

Methods

toAbstract :: QNamed Clause -> WithNames Clause

Reify (QNamed Clause) Clause

Methods

reify :: QNamed Clause -> TCM Clause

reifyWhen :: Bool -> QNamed Clause -> TCM Clause

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

Methods

toConcrete :: Clause' a -> AbsToCon [Declaration]

bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToAbstract [QNamed Clause] [Clause]

Methods

toAbstract :: [QNamed Clause] -> WithNames [Clause]

type Clause = Clause' LHS

type SpineClause = Clause' SpineLHS

data RHS

Constructors

RHS

Fields

• rhsExpr :: Expr
• rhsConcrete :: Maybe Expr

  We store the original concrete expression in case we have to reproduce it during interactive case splitting. Nothing for internally generated rhss.

AbsurdRHS

WithRHS QName [Expr] [Clause]

The QName is the name of the with function.

RewriteRHS

Fields

• rewriteExprs :: [(QName, Expr)]

  The QNames are the names of the generated with functions, one for each Expr.

• rewriteRHS :: RHS

  The RHS should not be another RewriteRHS.

• rewriteWhereDecls :: [Declaration]

  The where clauses are attached to the RewriteRHS by

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

Methods

killRange :: KillRangeT 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

Methods

toAbstract :: AbstractRHS -> ScopeM 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

• spLhsInfo :: LHSInfo

  Range.

• spLhsDefName :: QName

  Name of function we are defining.

• spLhsPats :: [NamedArg Pattern]

  Function parameters (patterns).

• spLhsWithPats :: [Pattern]

  with patterns (after |).

Instances

Eq SpineLHS

Methods

(==) :: SpineLHS -> SpineLHS -> Bool

(/=) :: SpineLHS -> SpineLHS -> Bool

Show SpineLHS

Methods

showsPrec :: Int -> SpineLHS -> ShowS

show :: SpineLHS -> String

showList :: [SpineLHS] -> ShowS

KillRange SpineLHS

Methods

killRange :: KillRangeT SpineLHS

HasRange SpineLHS

Methods

getRange :: SpineLHS -> Range

ExprLike SpineLHS

Methods

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

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

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

mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS

LHSToSpine LHS SpineLHS

LHS instance.

Methods

lhsToSpine :: LHS -> SpineLHS

spineToLhs :: SpineLHS -> LHS

LHSToSpine Clause SpineClause

Clause instance.

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

ToConcrete SpineLHS LHS

Methods

toConcrete :: SpineLHS -> AbsToCon LHS

bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b

data LHS

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

Constructors

LHS

Fields

• lhsInfo :: LHSInfo

  Range.

• lhsCore :: LHSCore

  Copatterns.

• lhsWithPats :: [Pattern]

  with patterns (after |).

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

Methods

killRange :: KillRangeT 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.

Methods

lhsToSpine :: LHS -> SpineLHS

spineToLhs :: SpineLHS -> LHS

LHSToSpine Clause SpineClause

Clause instance.

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

ToConcrete LHS LHS

Methods

toConcrete :: LHS -> AbsToCon LHS

bindToConcrete :: LHS -> (LHS -> AbsToCon b) -> AbsToCon b

Reify NamedClause Clause

Methods

reify :: NamedClause -> TCM Clause

reifyWhen :: Bool -> NamedClause -> TCM Clause

ToAbstract Clause Clause

Methods

toAbstract :: Clause -> ScopeM Clause

ToAbstract LeftHandSide LHS

Methods

toAbstract :: LeftHandSide -> ScopeM LHS

ToAbstract (QNamed Clause) Clause

Methods

toAbstract :: QNamed Clause -> WithNames Clause

Reify (QNamed Clause) Clause

Methods

reify :: QNamed Clause -> TCM Clause

reifyWhen :: Bool -> QNamed Clause -> TCM Clause

ToAbstract [QNamed Clause] [Clause]

Methods

toAbstract :: [QNamed Clause] -> WithNames [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

• lhsDefName :: QName

  Head f.

• lhsPats :: [NamedArg (Pattern' e)]

  Applied to patterns ps.

LHSProj

Projection

Fields

• lhsDestructor :: AmbiguousQName

  Record projection identifier.

• lhsFocus :: NamedArg (LHSCore' e)

  Main branch.

• lhsPatsRight :: [NamedArg (Pattern' e)]

  Further applied to patterns.

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

Methods

toConcrete :: LHSCore -> AbsToCon Pattern

bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b

ToAbstract LHSCore (LHSCore' Expr)

Methods

toAbstract :: LHSCore -> ScopeM (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)

Methods

killRange :: KillRangeT (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)

Methods

toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr)

type LHSCore = 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.

Methods

lhsToSpine :: LHS -> SpineLHS

spineToLhs :: SpineLHS -> LHS

LHSToSpine Clause SpineClause

Clause instance.

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

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

List instance (for clauses).

Methods

lhsToSpine :: [a] -> [b]

spineToLhs :: [b] -> [a]

lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]

spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e

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.

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore

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

Methods

expandPatternSynonyms :: Pattern -> TCM Pattern

IsFlexiblePattern Pattern

Methods

maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Pattern -> TCM Bool

UniverseBi Declaration Pattern

Methods

universeBi :: Declaration -> [Pattern]

ToConcrete Pattern Pattern

Methods

toConcrete :: Pattern -> AbsToCon Pattern

bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b

UniverseBi Declaration (Pattern' Void)

Methods

universeBi :: Declaration -> [Pattern' Void]

ToAbstract Pattern (Pattern' Expr)

Methods

toAbstract :: Pattern -> ScopeM (Pattern' Expr)

ToAbstract Pattern (Names, Pattern)

Methods

toAbstract :: Pattern -> WithNames (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)

Methods

killRange :: KillRangeT (Pattern' e)

SetRange (Pattern' a)

Methods

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

HasRange (Pattern' e)

Methods

getRange :: Pattern' e -> Range

IsProjP (Pattern' e)

Methods

isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)

IsProjP e => MaybePostfixProjP (Pattern' e)

Methods

maybePostfixProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)

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)

Methods

toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr)

type Pattern = Pattern' Expr

type Patterns = [NamedArg Pattern]

class MaybePostfixProjP a where

Minimal complete definition

maybePostfixProjP

Methods

maybePostfixProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)

Instances

MaybePostfixProjP a => MaybePostfixProjP (Arg a)

Methods

maybePostfixProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName)

IsProjP e => MaybePostfixProjP (Pattern' e)

Methods

maybePostfixProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)

MaybePostfixProjP a => MaybePostfixProjP (Named n a)

Methods

maybePostfixProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName)

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

Instances

AllNames QName

Methods

allNames :: QName -> Seq QName

AllNames RHS

Methods

allNames :: RHS -> Seq QName

AllNames Clause

Methods

allNames :: Clause -> Seq QName

AllNames TypedBinding

Methods

allNames :: TypedBinding -> Seq QName

AllNames TypedBindings

Methods

allNames :: TypedBindings -> Seq QName

AllNames LamBinding

Methods

allNames :: LamBinding -> Seq QName

AllNames LetBinding

Methods

allNames :: LetBinding -> Seq QName

AllNames ModuleApplication

Methods

allNames :: ModuleApplication -> Seq QName

AllNames Declaration

Methods

allNames :: Declaration -> Seq QName

AllNames Expr

Methods

allNames :: Expr -> Seq QName

AllNames CallInfo

Methods

allNames :: CallInfo -> Seq QName

AllNames CallPath

Methods

allNames :: CallPath -> Seq QName

AllNames a => AllNames [a]

Methods

allNames :: [a] -> Seq QName

AllNames a => AllNames (Maybe a)

Methods

allNames :: Maybe a -> Seq QName

AllNames a => AllNames (Arg a)

Methods

allNames :: Arg a -> Seq QName

(AllNames a, AllNames b) => AllNames (a, b)

Methods

allNames :: (a, b) -> Seq QName

AllNames a => AllNames (Named name a)

Methods

allNames :: Named name 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

AnyAbstract Declaration

Methods

anyAbstract :: Declaration -> Bool

AnyAbstract a => AnyAbstract [a]

Methods

anyAbstract :: [a] -> Bool

nameExpr :: AbstractName -> Expr

Turn an AbstractName to an expression.

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

mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr

patternToExpr :: Pattern -> Expr

type PatternSynDefn = ([Arg Name], Pattern' Void)

type PatternSynDefns = Map QName PatternSynDefn

lambdaLiftExpr :: [Name] -> Expr -> Expr

substPattern :: [(Name, Pattern)] -> Pattern -> Pattern

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

Methods

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

SubstExpr TypedBindings

Methods

substExpr :: [(Name, Expr)] -> TypedBindings -> 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])

module Agda.Syntax.Abstract.Name