Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Abstract

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 Type = Expr Source #

Types are just expressions. Use this type synonym for hinting that an expression should be a type.

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

data Expr Source #

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

Constructors

Var Name

Bound variable.

Def' QName Suffix

Constant: axiom, function, data or record type, with a possible suffix.

Proj ProjOrigin AmbiguousQName

Projection (overloaded).

Con AmbiguousQName

Constructor (overloaded).

PatternSyn AmbiguousQName

Pattern synonym.

Macro QName

Macro.

Lit ExprInfo 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 AppInfo 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 Erased QName (List1 Clause) 
Pi ExprInfo Telescope1 Type

Dependent function space Γ → A.

Generalized (Set QName) Type

Like a Pi, but the ordering is not known

Fun ExprInfo (Arg Type) Type

Non-dependent function space.

Let ExprInfo (List1 LetBinding) Expr

let bs in e.

Rec ExprInfo RecordAssigns

Record construction.

RecUpdate ExprInfo Expr Assigns

Record update.

ScopedExpr ScopeInfo Expr

Scope annotation.

Quote ExprInfo

Quote an identifier QName.

QuoteTerm ExprInfo

Quote a term.

Unquote ExprInfo

The splicing construct: unquote ...

DontCare Expr

For printing DontCare from Syntax.Internal.

Instances

Instances details
SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Underscore Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range Source #

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr Source #

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

Reify Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr Source #

Methods

reify :: MonadReify m => Expr -> m (ReifiesTo Expr) Source #

reifyWhen :: MonadReify m => Bool -> Expr -> m (ReifiesTo Expr) Source #

PrettyTCM Expr Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Expr -> m Doc Source #

PrettyTCM Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Pattern -> m Doc Source #

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #

Generic Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Expr :: Type -> Type

Methods

from :: Expr -> Rep Expr x

to :: Rep Expr x -> Expr

Show Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

NFData Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Expr -> ()

Eq Expr Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

Methods

toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source #

bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToAbstract (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) Source #

ToAbstract (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #

type ConOfAbs Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ReifiesTo Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Rep Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Generalized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "Fun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "Rec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordAssigns)) :+: (C1 ('MetaCons "RecUpdate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assigns))) :+: C1 ('MetaCons "ScopedExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "Quote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "QuoteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo))) :+: (C1 ('MetaCons "Unquote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "DontCare" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))
type ConOfAbs (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfRef (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range Source #

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS Source #

Generic LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LHS :: Type -> Type

Methods

from :: LHS -> Rep LHS x

to :: Rep LHS x -> LHS

Show LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

NFData LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHS -> ()

Eq LHS Source #

Ignore Range' when comparing LHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore)))

data Binder' a Source #

Constructors

Binder 

Fields

Instances

Instances details
Foldable Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

fold :: Monoid m => Binder' m -> m

foldMap :: Monoid m => (a -> m) -> Binder' a -> m

foldMap' :: Monoid m => (a -> m) -> Binder' a -> m

foldr :: (a -> b -> b) -> b -> Binder' a -> b

foldr' :: (a -> b -> b) -> b -> Binder' a -> b

foldl :: (b -> a -> b) -> b -> Binder' a -> b

foldl' :: (b -> a -> b) -> b -> Binder' a -> b

foldr1 :: (a -> a -> a) -> Binder' a -> a

foldl1 :: (a -> a -> a) -> Binder' a -> a

toList :: Binder' a -> [a]

null :: Binder' a -> Bool

length :: Binder' a -> Int

elem :: Eq a => a -> Binder' a -> Bool

maximum :: Ord a => Binder' a -> a

minimum :: Ord a => Binder' a -> a

sum :: Num a => Binder' a -> a

product :: Num a => Binder' a -> a

Traversable Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a)

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

sequence :: Monad m => Binder' (m a) -> m (Binder' a)

Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

fmap :: (a -> b) -> Binder' a -> Binder' b

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

HasRange a => HasRange (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range Source #

KillRange a => KillRange (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete a => ToConcrete (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a) Source #

Generic (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Binder' a) :: Type -> Type

Methods

from :: Binder' a -> Rep (Binder' a) x

to :: Rep (Binder' a) x -> Binder' a

Show a => Show (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Binder' a -> ShowS

show :: Binder' a -> String

showList :: [Binder' a] -> ShowS

NFData a => NFData (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Binder' a -> ()

Eq a => Eq (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: Binder' a -> Binder' a -> Bool

(/=) :: Binder' a -> Binder' a -> Bool

type ConOfAbs (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree TacticAttr (NamedArg Binder)

. x or {x} or .x or {x = y} or x@p or (p)

DomainFull TypedBinding

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

Instances

Instances details
ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding Source #

Generic LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LamBinding :: Type -> Type

Methods

from :: LamBinding -> Rep LamBinding x

to :: Rep LamBinding x -> LamBinding

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

NFData LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LamBinding -> ()

Eq LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "DomainFree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Binder))) :+: C1 ('MetaCons "DomainFull" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBinding)))

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 TypedBindingInfo (List1 (NamedArg Binder)) Type

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

TLet Range (List1 LetBinding)

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

Instances

Instances details
ExprLike TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding Source #

PrettyTCM TypedBinding Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Generic TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBinding :: Type -> Type

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

NFData TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBinding -> ()

Eq TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "TBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBindingInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding))))

data Declaration Source #

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Type

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

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

Generalize (Set QName) DefInfo ArgInfo QName Type

First argument is set of generalizable variables used in the type.

Field DefInfo QName (Arg Type)

record field

Primitive DefInfo QName (Arg Type)

primitive function

Mutual MutualInfo [Declaration]

a bunch of mutually recursive definitions

Section Range Erased ModuleName GeneralizeTelescope [Declaration] 
Apply ModuleInfo Erased 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 
FunDef DefInfo QName [Clause]

sequence of function clauses

DataSig DefInfo Erased QName GeneralizeTelescope Type

lone data signature

DataDef DefInfo QName UniverseCheck DataDefParams [Constructor] 
RecSig DefInfo Erased QName GeneralizeTelescope Type

lone record signature

RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]

The Type gives the constructor type telescope, (x1 : A1)..(xn : An) -> Dummy, and the optional name is the constructor's name. The optional Range' is for the pattern attribute.

PatternSynDef QName [Arg BindName] (Pattern' Void)

Only for highlighting purposes

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

scope annotation

UnfoldingDecl Range [QName]

Only for highlighting the unfolded names

Instances

Instances details
AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool Source #

DeclaredNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration Source #

ShowHead Declaration Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Decl

Methods

showHead :: Declaration -> String Source #

Generic Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Declaration :: Type -> Type

Methods

from :: Declaration -> Rep Declaration x

to :: Rep Declaration x -> Declaration

Show Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

NFData Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Declaration -> ()

Eq Declaration Source #

Does not compare ScopeInfo fields.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) Source #

type ConOfAbs Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Occurrence])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: (C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))) :+: ((C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))))) :+: (((C1 ('MetaCons "FunDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: (C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg BindName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void)))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "UnquoteData" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "UnfoldingDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])))))))
type ConOfAbs (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data ModuleApplication Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]

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

RecordModuleInstance ModuleName
M {{...}}

Instances

Instances details
ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication Source #

Generic ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ModuleApplication :: Type -> Type

Show ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

NFData ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ModuleApplication -> ()

Eq ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "SectionApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Expr]))) :+: C1 ('MetaCons "RecordModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)))

data RHS Source #

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 [WithExpr] (List1 Clause)

The QName is the name of the with function.

RewriteRHS 

Fields

Instances

Instances details
DeclaredNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range Source #

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS Source #

Generic RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep RHS :: Type -> Type

Methods

from :: RHS -> Rep RHS x

to :: Rep RHS x -> RHS

Show RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

NFData RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: RHS -> ()

Eq RHS Source #

Ignore rhsConcrete when comparing RHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) ((C1 ('MetaCons "RHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "rhsExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "rhsConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "AbsurdRHS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithRHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithExpr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause)))) :+: C1 ('MetaCons "RewriteRHS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rewriteExprs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RewriteEqn]) :*: S1 ('MetaSel ('Just "rewriteStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "rewriteRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: S1 ('MetaSel ('Just "rewriteWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations)))))

data Pragma Source #

Constructors

OptionsPragma [String] 
BuiltinPragma RString ResolvedName

ResolvedName is not UnknownName. Name can be ambiguous e.g. for built-in constructors.

BuiltinNoDefPragma RString KindOfName QName

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

RewritePragma Range [QName]

Range is range of REWRITE keyword.

CompilePragma RString QName String 
StaticPragma QName 
EtaPragma QName

For coinductive records, use pragma instead of regular eta-equality definition (as it is might make Agda loop).

InjectivePragma QName 
InlinePragma Bool QName 
NotProjectionLikePragma QName 
DisplayPragma QName [NamedArg Pattern] Expr 

Instances

Instances details
DeclaredNames Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Generic Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Pragma :: Type -> Type

Methods

from :: Pragma -> Rep Pragma x

to :: Rep Pragma x -> Pragma

Show Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

NFData Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pragma -> ()

Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type Rep Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (((C1 ('MetaCons "OptionsPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "BuiltinPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName))) :+: (C1 ('MetaCons "BuiltinNoDefPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "RewritePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: C1 ('MetaCons "CompilePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))) :+: ((C1 ('MetaCons "StaticPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "EtaPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InjectivePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: (C1 ('MetaCons "InlinePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "NotProjectionLikePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "DisplayPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

data ScopeCopyInfo Source #

Instances

Instances details
Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Generic ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ScopeCopyInfo :: Type -> Type

Show ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ScopeCopyInfo -> ShowS

show :: ScopeCopyInfo -> String

showList :: [ScopeCopyInfo] -> ShowS

NFData ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ScopeCopyInfo -> ()

Eq ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "ScopeCopyInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "renModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren ModuleName)) :*: S1 ('MetaSel ('Just "renNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren QName))))

type Ren a = Map a (List1 a) Source #

Renaming (generic).

data ProblemEq Source #

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Instances

Instances details
KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq Source #

Generic ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq :: Type -> Type

Methods

from :: ProblemEq -> Rep ProblemEq x

to :: Rep ProblemEq x -> ProblemEq

Show ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS

show :: ProblemEq -> String

showList :: [ProblemEq] -> ShowS

NFData ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> ()

Eq ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: ProblemEq -> ProblemEq -> Bool

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

type SubstArg ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

data TypedBindingInfo Source #

Extra information that is attached to a typed binding, that plays a role during type checking but strictly speaking is not part of the name : type" relation which a makes up a binding.

Constructors

TypedBindingInfo 

Fields

  • tbTacticAttr :: TacticAttr

    Does this binding have a tactic annotation?

  • tbFinite :: Bool

    Does this binding correspond to a Partial binder, rather than to a Pi binder? Must be present here to be reflected into abstract syntax later (and to be printed to the user later).

Instances

Instances details
ExprLike TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Generic TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBindingInfo :: Type -> Type

Show TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> TypedBindingInfo -> ShowS

show :: TypedBindingInfo -> String

showList :: [TypedBindingInfo] -> ShowS

NFData TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBindingInfo -> ()

Eq TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "TypedBindingInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tbTacticAttr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr) :*: S1 ('MetaSel ('Just "tbFinite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

type NAPs e = [NamedArg (Pattern' e)] Source #

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName 
ConP ConPatInfo AmbiguousQName (NAPs e) 
ProjP PatInfo ProjOrigin AmbiguousQName

Destructor pattern d.

DefP PatInfo AmbiguousQName (NAPs 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 BindName (Pattern' e) 
DotP PatInfo e

Dot pattern .e

AbsurdP PatInfo 
LitP PatInfo Literal 
PatternSynP PatInfo AmbiguousQName (NAPs e) 
RecP PatInfo [FieldAssignment' (Pattern' e)] 
EqualP PatInfo [(e, e)] 
WithP PatInfo (Pattern' e)

| p, for with-patterns.

AnnP PatInfo e (Pattern' e)

Pattern with type annotation

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

PrettyTCM Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Pattern -> m Doc Source #

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #

Foldable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

foldMap :: Monoid m => (a -> m) -> Pattern' a -> 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 # 
Instance details

Defined in Agda.Syntax.Abstract

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)

Functor Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

IsProjP (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

APatternLike (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a) Source #

Methods

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

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

ExprLike a => ExprLike (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

IsWithP (Pattern' e) Source #

Check for with-pattern.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

isWithP :: Pattern' e -> Maybe (Pattern' e) Source #

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #

HasRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range Source #

KillRange e => KillRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

Methods

toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source #

bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) Source #

ExpandPatternSynonyms (Pattern' e) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

EmbPrj a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Pattern' a -> S Int32 Source #

icod_ :: Pattern' a -> S Int32 Source #

value :: Int32 -> R (Pattern' a) Source #

Generic (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Pattern' e) :: Type -> Type

Methods

from :: Pattern' e -> Rep (Pattern' e) x

to :: Rep (Pattern' e) x -> Pattern' e

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: Pattern' e -> String

showList :: [Pattern' e] -> ShowS

NFData e => NFData (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pattern' e -> ()

Eq e => Eq (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #

type ConOfAbs Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ADotT (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Pattern' a) = a
type ConOfAbs (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Rep (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: ((C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo))) :+: (C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))) :+: C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e))))) :+: ((C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: (C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))))) :+: ((C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])) :+: C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(e, e)]))) :+: (C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))))
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

newtype BindName Source #

A name in a binding position: we also compare the nameConcrete when comparing the binders for equality.

With --caching on we compare abstract syntax to determine if we can reuse previous typechecking results: during that comparison two names can have the same nameId but be semantically different, e.g. in {_ : A} -> .. vs. {r : A} -> ...

Constructors

BindName 

Fields

Instances

Instances details
ExprLike BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName Source #

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32 Source #

icod_ :: BindName -> S Int32 Source #

value :: Int32 -> R BindName Source #

Show BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> BindName -> ShowS

show :: BindName -> String

showList :: [BindName] -> ShowS

NFData BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: BindName -> ()

Eq BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: BindName -> BindName -> Bool

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

Ord BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

compare :: BindName -> BindName -> Ordering

(<) :: BindName -> BindName -> Bool

(<=) :: BindName -> BindName -> Bool

(>) :: BindName -> BindName -> Bool

(>=) :: BindName -> BindName -> Bool

max :: BindName -> BindName -> BindName

min :: BindName -> BindName -> BindName

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) Source #

Methods

toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName)) Source #

bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b Source #

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a) Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #

type ConOfAbs BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe BindName) = Maybe Name
type ConOfAbs (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LetBinding Source #

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo BindName Type Expr
LetBind info rel name type defn
LetPatBind LetInfo Pattern Expr

Irrefutable pattern binding.

LetApply ModuleInfo Erased 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 BindName

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

Instances

Instances details
ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding Source #

Generic LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LetBinding :: Type -> Type

Methods

from :: LetBinding -> Rep LetBinding x

to :: Rep LetBinding x -> LetBinding

Show LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LetBinding -> ShowS

show :: LetBinding -> String

showList :: [LetBinding] -> ShowS

NFData LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LetBinding -> ()

Eq LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)))))

data GeneralizeTelescope Source #

Constructors

GeneralizeTel 

Fields

Instances

Instances details
ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Generic GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep GeneralizeTelescope :: Type -> Type

Show GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> GeneralizeTelescope -> ShowS

show :: GeneralizeTelescope -> String

showList :: [GeneralizeTelescope] -> ShowS

NFData GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: GeneralizeTelescope -> ()

Eq GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "GeneralizeTel" 'PrefixI 'True) (S1 ('MetaSel ('Just "generalizeTelVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "generalizeTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope)))

data DataDefParams Source #

Constructors

DataDefParams 

Fields

Instances

Instances details
ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Generic DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep DataDefParams :: Type -> Type

Show DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> DataDefParams -> ShowS

show :: DataDefParams -> String

showList :: [DataDefParams] -> ShowS

NFData DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: DataDefParams -> ()

Eq DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "DataDefParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "dataDefGeneralizedParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :*: S1 ('MetaSel ('Just "dataDefParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding])))

type TacticAttr = Maybe (Ranged Expr) Source #

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

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Foldable Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

foldMap :: Monoid m => (a -> m) -> Clause' a -> 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 # 
Instance details

Defined in Agda.Syntax.Abstract

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)

Functor Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract.Views

HasRange a => HasRange (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range Source #

KillRange a => KillRange (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a) Source #

Generic (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Clause' lhs) :: Type -> Type

Methods

from :: Clause' lhs -> Rep (Clause' lhs) x

to :: Rep (Clause' lhs) x -> Clause' lhs

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: Clause' lhs -> String

showList :: [Clause' lhs] -> ShowS

NFData lhs => NFData (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Clause' lhs -> ()

Eq lhs => Eq (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) ((S1 ('MetaSel ('Just "clauseLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 lhs) :*: S1 ('MetaSel ('Just "clauseStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "clauseRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Just "clauseWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations) :*: S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data WhereDeclarations Source #

Constructors

WhereDecls 

Fields

Instances

Instances details
DeclaredNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations Source #

Null WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Generic WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep WhereDeclarations :: Type -> Type

Show WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> WhereDeclarations -> ShowS

show :: WhereDeclarations -> String

showList :: [WhereDeclarations] -> ShowS

NFData WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: WhereDeclarations -> ()

Eq WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: (S1 ('MetaSel ('Just "whereAnywhere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration)))))

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

Instances

Instances details
ExprLike SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS Source #

Generic SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep SpineLHS :: Type -> Type

Methods

from :: SpineLHS -> Rep SpineLHS x

to :: Rep SpineLHS x -> SpineLHS

Show SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> SpineLHS -> ShowS

show :: SpineLHS -> String

showList :: [SpineLHS] -> ShowS

NFData SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: SpineLHS -> ()

Eq SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]))))

data LHSCore' e Source #

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

Constructors

LHSHead

The head applied to ordinary patterns.

Fields

LHSProj

Projection.

Fields

LHSWith

With patterns.

Fields

Instances

Instances details
ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

Foldable LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

foldMap :: Monoid m => (a -> m) -> LHSCore' a -> 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 # 
Instance details

Defined in Agda.Syntax.Abstract

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)

Functor LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

HasRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range Source #

KillRange e => KillRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) Source #

Generic (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (LHSCore' e) :: Type -> Type

Methods

from :: LHSCore' e -> Rep (LHSCore' e) x

to :: Rep (LHSCore' e) x -> LHSCore' e

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: LHSCore' e -> String

showList :: [LHSCore' e] -> ShowS

NFData e => NFData (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHSCore' e -> ()

Eq e => Eq (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Rep (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "LHSHead" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])) :+: (C1 ('MetaCons "LHSProj" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDestructor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: (S1 ('MetaSel ('Just "lhsFocus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg (LHSCore' e))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))) :+: C1 ('MetaCons "LHSWith" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsHead") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LHSCore' e)) :*: (S1 ('MetaSel ('Just "lhsWithPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg (Pattern' e)]) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])))))

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool Source #

Instances

Instances details
AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool Source #

AnyAbstract a => AnyAbstract [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: [a] -> Bool Source #

class NameToExpr a where Source #

Turn a name into an expression.

Methods

nameToExpr :: a -> Expr Source #

Instances

Instances details
NameToExpr AbstractName Source #

Turn an AbstractName into an expression.

Instance details

Defined in Agda.Syntax.Abstract

NameToExpr ResolvedName Source #

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

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

default substExpr :: (Functor t, SubstExpr b, t b ~ a) => [(Name, Expr)] -> a -> a Source #

Instances

Instances details
SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr Name Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr a => SubstExpr (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

data DeclarationSpine Source #

Declaration spines. Used in debugging to make it easy to see where constructors such as ScopedDecl and Mutual are placed.

Instances

Instances details
Show DeclarationSpine Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> DeclarationSpine -> ShowS

show :: DeclarationSpine -> String

showList :: [DeclarationSpine] -> ShowS

data ClauseSpine Source #

Clause spines.

Instances

Instances details
Show ClauseSpine Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ClauseSpine -> ShowS

show :: ClauseSpine -> String

showList :: [ClauseSpine] -> ShowS

data RHSSpine Source #

Right-hand side spines.

Instances

Instances details
Show RHSSpine Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> RHSSpine -> ShowS

show :: RHSSpine -> String

showList :: [RHSSpine] -> ShowS

data WhereDeclarationsSpine Source #

Spines corresponding to WhereDeclarations values.

Constructors

WhereDeclsS (Maybe DeclarationSpine) 

Instances

Instances details
Show WhereDeclarationsSpine Source # 
Instance details

Defined in Agda.Syntax.Abstract

pattern Def :: QName -> Expr Source #

Pattern synonym for regular Def.

generalized :: Set QName -> Type -> Type Source #

Smart constructor for Generalized.

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

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

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

declarationSpine :: Declaration -> DeclarationSpine Source #

The declaration spine corresponding to a declaration.

clauseSpine :: Clause -> ClauseSpine Source #

The clause spine corresponding to a clause.

rhsSpine :: RHS -> RHSSpine Source #

The right-hand side spine corresponding to a right-hand side.

Orphan instances

KillRange Suffix Source # 
Instance details