Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Abstract

Contents

Orphan instances

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

type Type = Expr
app :: Expr -> [NamedArg Expr] -> Expr
type Constructor = TypeSignature
data Expr
- = Var Name
- | Def' QName Suffix
- | Proj ProjOrigin AmbiguousQName
- | Con AmbiguousQName
- | PatternSyn AmbiguousQName
- | Macro QName
- | Lit ExprInfo Literal
- | QuestionMark MetaInfo InteractionId
- | Underscore MetaInfo
- | Dot ExprInfo Expr
- | App AppInfo Expr (NamedArg Expr)
- | WithApp ExprInfo Expr [Expr]
- | Lam ExprInfo LamBinding Expr
- | AbsurdLam ExprInfo Hiding
- | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
- | Pi ExprInfo Telescope1 Type
- | Generalized (Set QName) Type
- | Fun ExprInfo (Arg Type) Type
- | Let ExprInfo (List1 LetBinding) Expr
- | Rec ExprInfo RecordAssigns
- | RecUpdate ExprInfo Expr Assigns
- | ScopedExpr ScopeInfo Expr
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | DontCare Expr
type Clause = Clause' LHS
data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool
}
data Pragma
- = OptionsPragma [String]
- | BuiltinPragma RString ResolvedName
- | BuiltinNoDefPragma RString KindOfName QName
- | RewritePragma Range [QName]
- | CompilePragma RString QName String
- | StaticPragma QName
- | EtaPragma QName
- | InjectivePragma QName
- | InlinePragma Bool QName
- | NotProjectionLikePragma QName
- | DisplayPragma QName [NamedArg Pattern] Expr
data Declaration
- = Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Type
- | Generalize (Set QName) DefInfo ArgInfo QName Type
- | Field DefInfo QName (Arg Type)
- | Primitive DefInfo QName (Arg Type)
- | Mutual MutualInfo [Declaration]
- | Section Range Erased ModuleName GeneralizeTelescope [Declaration]
- | Apply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | Import ModuleInfo ModuleName ImportDirective
- | Pragma Range Pragma
- | Open ModuleInfo ModuleName ImportDirective
- | FunDef DefInfo QName [Clause]
- | DataSig DefInfo Erased QName GeneralizeTelescope Type
- | DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
- | RecSig DefInfo Erased QName GeneralizeTelescope Type
- | RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
- | PatternSynDef QName [Arg BindName] (Pattern' Void)
- | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
- | UnquoteDef [DefInfo] [QName] Expr
- | UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
- | ScopedDecl ScopeInfo [Declaration]
- | UnfoldingDecl Range [QName]
data Pattern' e
- = VarP BindName
- | ConP ConPatInfo AmbiguousQName (NAPs e)
- | ProjP PatInfo ProjOrigin AmbiguousQName
- | DefP PatInfo AmbiguousQName (NAPs e)
- | WildP PatInfo
- | AsP PatInfo BindName (Pattern' e)
- | DotP PatInfo e
- | AbsurdP PatInfo
- | LitP PatInfo Literal
- | PatternSynP PatInfo AmbiguousQName (NAPs e)
- | RecP PatInfo [FieldAssignment' (Pattern' e)]
- | EqualP PatInfo [(e, e)]
- | WithP PatInfo (Pattern' e)
- | AnnP PatInfo e (Pattern' e)
type Telescope = [TypedBinding]
type Pattern = Pattern' Expr
type Assign = FieldAssignment' Expr
pattern Def :: QName -> Expr
data LHS = LHS {
- lhsInfo :: LHSInfo
- lhsCore :: LHSCore
}
data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
}
type Binder = Binder' BindName
mkBinder_ :: Name -> Binder
mkBinder :: a -> Binder' a
data LamBinding
- = DomainFree TacticAttr (NamedArg Binder)
- | DomainFull TypedBinding
data TypedBinding
- = TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type
- | TLet Range (List1 LetBinding)
type Telescope1 = List1 TypedBinding
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
type RecordDirectives = RecordDirectives' QName
data ModuleApplication
- = SectionApp Telescope ModuleName [NamedArg Expr]
- | RecordModuleInstance ModuleName
type TypeSignature = Declaration
type ImportDirective = ImportDirective' QName ModuleName
type ImportedName = ImportedName' QName ModuleName
type Renaming = Renaming' QName ModuleName
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
type WithExpr = WithExpr' Expr
type LHSCore = LHSCore' Expr
data RHS
- = RHS {
  - rhsExpr :: Expr
  - rhsConcrete :: Maybe Expr
  }
- | AbsurdRHS
- | WithRHS QName [WithExpr] (List1 Clause)
- | RewriteRHS {
  - rewriteExprs :: [RewriteEqn]
  - rewriteStrippedPats :: [ProblemEq]
  - rewriteRHS :: RHS
  - rewriteWhereDecls :: WhereDeclarations
  }
type HoleContent = HoleContent' () BindName Pattern Expr
data ScopeCopyInfo = ScopeCopyInfo {
- renModules :: Ren ModuleName
- renNames :: Ren QName
}
type Args = [NamedArg Expr]
type Ren a = Map a (List1 a)
type PatternSynDefn = ([Arg Name], Pattern' Void)
type PatternSynDefns = Map QName PatternSynDefn
data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
}
data TypedBindingInfo = TypedBindingInfo {
- tbTacticAttr :: TacticAttr
- tbFinite :: Bool
}
type Field = TypeSignature
data LHSCore' e
- = LHSHead {
  - lhsDefName :: QName
  - lhsPats :: [NamedArg (Pattern' e)]
  }
- | LHSProj {
  - lhsDestructor :: AmbiguousQName
  - lhsFocus :: NamedArg (LHSCore' e)
  - lhsPats :: [NamedArg (Pattern' e)]
  }
- | LHSWith {
  - lhsHead :: LHSCore' e
  - lhsWithPatterns :: [Arg (Pattern' e)]
  - lhsPats :: [NamedArg (Pattern' e)]
  }
type NAPs e = [NamedArg (Pattern' e)]
type DefInfo = DefInfo' Expr
newtype BindName = BindName {
- unBind :: Name
}
mkBindName :: Name -> BindName
data LetBinding
- = LetBind LetInfo ArgInfo BindName Type Expr
- | LetPatBind LetInfo Pattern Expr
- | LetApply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | LetOpen ModuleInfo ModuleName ImportDirective
- | LetDeclaredVariable BindName
type RecordAssigns = [RecordAssign]
type Assigns = [Assign]
generalized :: Set QName -> Type -> Type
type RecordAssign = Either Assign ModuleName
initCopyInfo :: ScopeCopyInfo
data GeneralizeTelescope = GeneralizeTel {
- generalizeTelVars :: Map QName Name
- generalizeTel :: Telescope
}
data DataDefParams = DataDefParams {
- dataDefGeneralizedParams :: Set Name
- dataDefParams :: [LamBinding]
}
type TacticAttr = Maybe (Ranged Expr)
extractPattern :: Binder' a -> Maybe (Pattern, a)
mkDomainFree :: NamedArg Binder -> LamBinding
defaultTbInfo :: TypedBindingInfo
mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
mkPi :: ExprInfo -> Telescope -> Type -> Type
noDataDefParams :: DataDefParams
data WhereDeclarations = WhereDecls {
- whereModule :: Maybe ModuleName
- whereAnywhere :: Bool
- whereDecls :: Maybe Declaration
}
noWhereDecls :: WhereDeclarations
type SpineClause = Clause' SpineLHS
data SpineLHS = SpineLHS {
- spLhsInfo :: LHSInfo
- spLhsDefName :: QName
- spLhsPats :: [NamedArg Pattern]
}
type WithExpr' e = Named BindName (Arg e)
type NAPs1 e = List1 (NamedArg (Pattern' e))
type Patterns = [NamedArg Pattern]
axiomName :: Declaration -> QName
class AnyAbstract a where
- anyAbstract :: a -> Bool
class NameToExpr a where
- nameToExpr :: a -> Expr
patternToExpr :: Pattern -> Expr
lambdaLiftExpr :: [Name] -> Expr -> Expr
class SubstExpr a where
- substExpr :: [(Name, Expr)] -> a -> a
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
data DeclarationSpine
- = AxiomS
- | GeneralizeS
- | FieldS
- | PrimitiveS
- | MutualS [DeclarationSpine]
- | SectionS [DeclarationSpine]
- | ApplyS
- | ImportS
- | PragmaS
- | OpenS
- | FunDefS [ClauseSpine]
- | DataSigS
- | DataDefS
- | RecSigS
- | RecDefS [DeclarationSpine]
- | PatternSynDefS
- | UnquoteDeclS
- | UnquoteDefS
- | UnquoteDataS
- | ScopedDeclS [DeclarationSpine]
- | UnfoldingDeclS
data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
data RHSSpine
- = RHSS
- | AbsurdRHSS
- | WithRHSS (List1 ClauseSpine)
- | RewriteRHSS RHSSpine WhereDeclarationsSpine
data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
declarationSpine :: Declaration -> DeclarationSpine
clauseSpine :: Clause -> ClauseSpine
rhsSpine :: RHS -> RHSSpine
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
module Agda.Syntax.Abstract.Name

Documentation

type Type = Expr Source #

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

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

type Constructor = TypeSignature Source #

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

Methods

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

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

Methods

recurseExpr :: RecurseExprFn m Expr Source #

foldExpr :: FoldExprFn m Expr Source #

traverseExpr :: TraverseExprFn m Expr Source #

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

Underscore Expr Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

underscore :: Expr Source #

isUnderscore :: Expr -> Bool Source #

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

Methods

killRange :: KillRangeT Expr Source #

ToConcrete Expr Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Expr = Expr

Methods

toConcrete :: Expr -> AbsToCon (ConOfAbs Expr) Source #

bindToConcrete :: Expr -> (ConOfAbs Expr -> AbsToCon b) -> AbsToCon b Source #

ToConcrete LHSCore Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source #

bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b Source #

ToConcrete Pattern Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern

Methods

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

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

Reify Expr Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Expr = Expr

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

Instance details

Defined in Agda.Syntax.Abstract

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)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern

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

Methods

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

ToAbstract (Expr, Elim) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim)
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #

ToAbstract (Expr, Elims) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims)
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

Methods

toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

type ConOfAbs Expr Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Expr = Expr

type ConOfAbs LHSCore Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore = Pattern

type ConOfAbs Pattern Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern = Pattern

type ReifiesTo Expr Source #

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Expr = Expr

type Rep Expr Source #

Instance details

Defined in Agda.Syntax.Abstract

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, Elim) = Expr

type AbsOfRef (Expr, Elims) Source #

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type Clause = Clause' LHS 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 clauseLHS :: lhs clauseStrippedPats :: [ProblemEq] Only in with-clauses where we inherit some already checked patterns from the parent. These live in the context of the parent clause left-hand side. clauseRHS :: RHS clauseWhereDecls :: WhereDeclarations clauseCatchall :: Bool

Instances

Instances details

DeclaredNames Clause Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Clause -> m Source #

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

Methods

lhsToSpine :: Clause -> SpineClause Source #

spineToLhs :: SpineClause -> Clause Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (Clause' a) Source #

foldExpr :: FoldExprFn m (Clause' a) Source #

traverseExpr :: TraverseExprFn m (Clause' a) Source #

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

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

Methods

killRange :: KillRangeT (Clause' a) Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = List1 Declaration

Methods

toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a)) Source #

bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b Source #

Generic (Clause' lhs) Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Clause' lhs)

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))))

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 ConOfAbs (Clause' a) = List1 Declaration

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

Methods

declaredNames :: Collection KName m => Pragma -> m Source #

ExprLike Pragma Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m Pragma Source #

foldExpr :: FoldExprFn m Pragma Source #

traverseExpr :: TraverseExprFn m Pragma Source #

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

Generic Pragma Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Pragma

Instance details

Defined in Agda.Syntax.Abstract

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

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

Methods

declaredNames :: Collection KName m => Declaration -> m Source #

ExprLike Declaration Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m Declaration Source #

foldExpr :: FoldExprFn m Declaration Source #

traverseExpr :: TraverseExprFn m Declaration Source #

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

HasRange Declaration Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Declaration -> Range Source #

KillRange Declaration Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Declaration Source #

ToConcrete Declaration Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Declaration = [Declaration]

Methods

toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration) Source #

bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b 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

Instance details

Defined in Agda.Syntax.Abstract

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)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

Methods

toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source #

bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source #

type ConOfAbs Declaration Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Declaration = [Declaration]

type Rep Declaration Source #

Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs (Constr Constructor) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Constr Constructor) = Declaration

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
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern

Methods

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

bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b 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

Methods

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

APatternLike (Pattern' a) Source #

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a)
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Pattern' a) = a

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

Methods

recurseExpr :: RecurseExprFn m (Pattern' a) Source #

foldExpr :: FoldExprFn m (Pattern' a) Source #

traverseExpr :: TraverseExprFn m (Pattern' a) Source #

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

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

Methods

killRange :: KillRangeT (Pattern' e) Source #

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)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr

Methods

toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) Source #

ExpandPatternSynonyms (Pattern' e) Source #

Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #

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)

Instance details

Defined in Agda.Syntax.Abstract

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

Methods

toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

type ConOfAbs Pattern Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern = Pattern

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 AbsOfCon (Pattern' Expr) = Pattern' Expr

type Rep (Pattern' e) Source #

Instance details

Defined in Agda.Syntax.Abstract

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type Telescope = [TypedBinding] Source #

type Pattern = Pattern' Expr Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

pattern Def :: QName -> Expr Source #

Pattern synonym for regular Def.

data LHS Source #

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

Constructors

LHS
Fields lhsInfo :: LHSInfo Range. lhsCore :: LHSCore Copatterns.

Instances

Instances details

DeclaredNames Clause Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Clause -> m Source #

ExprLike LHS Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m LHS Source #

foldExpr :: FoldExprFn m LHS Source #

traverseExpr :: TraverseExprFn m LHS Source #

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

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

Methods

killRange :: KillRangeT LHS Source #

ToConcrete LHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHS = LHS

Methods

toConcrete :: LHS -> AbsToCon (ConOfAbs LHS) Source #

bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b Source #

Generic LHS Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LHS
Instance details Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

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

Methods

lhsToSpine :: Clause -> SpineClause Source #

spineToLhs :: SpineClause -> Clause Source #

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: LHS -> SpineLHS Source #

spineToLhs :: SpineLHS -> LHS Source #

type ConOfAbs LHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHS = LHS

type Rep LHS Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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 binderPattern :: Maybe Pattern binderName :: a

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

Methods

killRange :: KillRangeT (Binder' a) Source #

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

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)

Methods

toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a)) Source #

bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b Source #

Generic (Binder' a) Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Binder' a)

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

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 ConOfAbs (Binder' a) = Binder' (ConOfAbs a)

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

type Binder = Binder' BindName Source #

mkBinder_ :: Name -> Binder Source #

mkBinder :: a -> Binder' a Source #

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

Methods

recurseExpr :: RecurseExprFn m LamBinding Source #

foldExpr :: FoldExprFn m LamBinding Source #

traverseExpr :: TraverseExprFn m LamBinding Source #

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

LensHiding LamBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getHiding :: LamBinding -> Hiding Source #

setHiding :: Hiding -> LamBinding -> LamBinding Source #

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

HasRange LamBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LamBinding -> Range Source #

KillRange LamBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LamBinding Source #

ToConcrete LamBinding Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LamBinding = Maybe LamBinding

Methods

toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source #

bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b Source #

Generic LamBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LamBinding

Instance details

Defined in Agda.Syntax.Abstract

type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

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 ConOfAbs LamBinding = Maybe LamBinding

type Rep LamBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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:

We would have to typecheck the type A several times.
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

Methods

recurseExpr :: RecurseExprFn m TypedBinding Source #

foldExpr :: FoldExprFn m TypedBinding Source #

traverseExpr :: TraverseExprFn m TypedBinding Source #

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

LensHiding TypedBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getHiding :: TypedBinding -> Hiding Source #

setHiding :: Hiding -> TypedBinding -> TypedBinding Source #

mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #

HasRange TypedBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: TypedBinding -> Range Source #

KillRange TypedBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT TypedBinding Source #

ToConcrete TypedBinding Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs TypedBinding = Maybe TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding) Source #

bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b Source #

PrettyTCM TypedBinding Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Generic TypedBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBinding

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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))))

Methods

from :: TypedBinding -> Rep TypedBinding x #

to :: Rep TypedBinding x -> TypedBinding #

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 ConOfAbs TypedBinding = Maybe TypedBinding

type Rep TypedBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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))))

type Telescope1 = List1 TypedBinding Source #

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

mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding Source #

type RecordDirectives = RecordDirectives' QName Source #

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

Methods

recurseExpr :: RecurseExprFn m ModuleApplication Source #

foldExpr :: FoldExprFn m ModuleApplication Source #

traverseExpr :: TraverseExprFn m ModuleApplication Source #

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

KillRange ModuleApplication Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ModuleApplication Source #

ToConcrete ModuleApplication Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleApplication = ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source #

bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b Source #

Generic ModuleApplication Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ModuleApplication

Instance details

Defined in Agda.Syntax.Abstract

type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

Methods

from :: ModuleApplication -> Rep ModuleApplication x #

to :: Rep ModuleApplication x -> ModuleApplication #

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

Methods

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

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

type ConOfAbs ModuleApplication Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ModuleApplication = ModuleApplication

type Rep ModuleApplication Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

type TypeSignature = Declaration Source #

Only Axioms.

type ImportDirective = ImportDirective' QName ModuleName Source #

type ImportedName = ImportedName' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #

type WithExpr = WithExpr' Expr Source #

type LHSCore = LHSCore' Expr Source #

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 rewriteExprs :: [RewriteEqn] The `QName`s are the names of the generated with functions, one for each `Expr`. rewriteStrippedPats :: [ProblemEq] The patterns stripped by with-desugaring. These are only present if this rewrite follows a with. rewriteRHS :: RHS The RHS should not be another `RewriteRHS`. rewriteWhereDecls :: WhereDeclarations The where clauses are attached to the `RewriteRHS` by

Instances

Instances details

DeclaredNames RHS Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => RHS -> m Source #

ExprLike RHS Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m RHS Source #

foldExpr :: FoldExprFn m RHS Source #

traverseExpr :: TraverseExprFn m RHS Source #

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

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

Methods

killRange :: KillRangeT RHS Source #

ToConcrete RHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])

Methods

toConcrete :: RHS -> AbsToCon (ConOfAbs RHS) Source #

bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b Source #

Generic RHS Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep RHS

Instance details

Defined in Agda.Syntax.Abstract

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 ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])

type Rep RHS Source #

Instance details

Defined in Agda.Syntax.Abstract

type HoleContent = HoleContent' () BindName Pattern Expr Source #

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo
Fields renModules :: Ren ModuleName renNames :: Ren QName

Instances

Instances details

Pretty ScopeCopyInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

pretty :: ScopeCopyInfo -> Doc Source #

prettyPrec :: Int -> ScopeCopyInfo -> Doc Source #

prettyList :: [ScopeCopyInfo] -> Doc Source #

KillRange ScopeCopyInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ScopeCopyInfo Source #

Generic ScopeCopyInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ScopeCopyInfo

Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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))))

Methods

from :: ScopeCopyInfo -> Rep ScopeCopyInfo x #

to :: Rep ScopeCopyInfo x -> ScopeCopyInfo #

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

Methods

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

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

type Rep ScopeCopyInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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 Args = [NamedArg Expr] Source #

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

Renaming (generic).

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

type PatternSynDefns = Map QName PatternSynDefn Source #

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.

Constructors

ProblemEq
Fields problemInPat :: Pattern problemInst :: Term problemType :: Dom Type

Instances

Instances details

KillRange ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ProblemEq Source #

PrettyTCM ProblemEq Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst ProblemEq Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term

Methods

applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #

Generic ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))))

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 SubstArg ProblemEq = Term

type Rep ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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

Methods

recurseExpr :: RecurseExprFn m TypedBindingInfo Source #

foldExpr :: FoldExprFn m TypedBindingInfo Source #

traverseExpr :: TraverseExprFn m TypedBindingInfo Source #

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

KillRange TypedBindingInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT TypedBindingInfo Source #

Generic TypedBindingInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBindingInfo

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

Methods

from :: TypedBindingInfo -> Rep TypedBindingInfo x #

to :: Rep TypedBindingInfo x -> TypedBindingInfo #

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

Methods

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

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

type Rep TypedBindingInfo Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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 Field = TypeSignature Source #

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 lhsDefName :: QName Head `f`. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSProj	Projection.
Fields lhsDestructor :: AmbiguousQName Record projection identifier. lhsFocus :: NamedArg (LHSCore' e) Main argument of projection. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSWith	With patterns.
Fields lhsHead :: LHSCore' e E.g. the `LHSHead`. lhsWithPatterns :: [Arg (Pattern' e)] Applied to with patterns `\| p1 \| ... \| pn`. These patterns are not prefixed with `WithP`! lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.

Instances

Instances details

ToConcrete LHSCore Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source #

bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b 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

Methods

recurseExpr :: RecurseExprFn m (LHSCore' a) Source #

foldExpr :: FoldExprFn m (LHSCore' a) Source #

traverseExpr :: TraverseExprFn m (LHSCore' a) Source #

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

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

Methods

killRange :: KillRangeT (LHSCore' e) Source #

ToAbstract (LHSCore' Expr) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

Methods

toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #

Generic (LHSCore' e) Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (LHSCore' e)

Instance details

Defined in Agda.Syntax.Abstract

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 ConOfAbs LHSCore = Pattern

type AbsOfCon (LHSCore' Expr) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

type Rep (LHSCore' e) Source #

Instance details

Defined in Agda.Syntax.Abstract

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

type DefInfo = DefInfo' Expr Source #

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 unBind :: Name

Instances

Instances details

ExprLike BindName Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m BindName Source #

foldExpr :: FoldExprFn m BindName Source #

traverseExpr :: TraverseExprFn m BindName Source #

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

HasRange BindName Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: BindName -> Range Source #

KillRange BindName Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT BindName Source #

SetRange BindName Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> BindName -> BindName Source #

ToConcrete BindName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs BindName = BoundName

Methods

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

bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b 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)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe BindName) = Maybe Name

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)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)

Methods

toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source #

bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b Source #

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

Methods

toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

type ConOfAbs BindName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs BindName = BoundName

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 ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

mkBindName :: Name -> BindName Source #

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

Methods

recurseExpr :: RecurseExprFn m LetBinding Source #

foldExpr :: FoldExprFn m LetBinding Source #

traverseExpr :: TraverseExprFn m LetBinding Source #

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

HasRange LetBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LetBinding -> Range Source #

KillRange LetBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LetBinding Source #

ToConcrete LetBinding Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LetBinding = [Declaration]

Methods

toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source #

bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b Source #

Generic LetBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LetBinding

Instance details

Defined in Agda.Syntax.Abstract

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 ConOfAbs LetBinding = [Declaration]

type Rep LetBinding Source #

Instance details

Defined in Agda.Syntax.Abstract

type RecordAssigns = [RecordAssign] Source #

type Assigns = [Assign] Source #

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

Smart constructor for Generalized.

type RecordAssign = Either Assign ModuleName Source #

initCopyInfo :: ScopeCopyInfo Source #

data GeneralizeTelescope Source #

Constructors

GeneralizeTel
Fields generalizeTelVars :: Map QName Name Maps generalize variables to the corresponding bound variable (to be introduced by the generalisation). generalizeTel :: Telescope

Instances

Instances details

ExprLike GeneralizeTelescope Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m GeneralizeTelescope Source #

foldExpr :: FoldExprFn m GeneralizeTelescope Source #

traverseExpr :: TraverseExprFn m GeneralizeTelescope Source #

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

KillRange GeneralizeTelescope Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT GeneralizeTelescope Source #

Generic GeneralizeTelescope Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep GeneralizeTelescope

Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))

Methods

from :: GeneralizeTelescope -> Rep GeneralizeTelescope x #

to :: Rep GeneralizeTelescope x -> GeneralizeTelescope #

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

Methods

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

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

type Rep GeneralizeTelescope Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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 dataDefGeneralizedParams :: Set Name We don't yet know the position of generalized parameters from the data sig, so we keep these in a set on the side. dataDefParams :: [LamBinding]

Instances

Instances details

ExprLike DataDefParams Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m DataDefParams Source #

foldExpr :: FoldExprFn m DataDefParams Source #

traverseExpr :: TraverseExprFn m DataDefParams Source #

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

KillRange DataDefParams Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT DataDefParams Source #

Generic DataDefParams Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep DataDefParams

Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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])))

Methods

from :: DataDefParams -> Rep DataDefParams x #

to :: Rep DataDefParams x -> DataDefParams #

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

Methods

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

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

type Rep DataDefParams Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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 #

extractPattern :: Binder' a -> Maybe (Pattern, a) Source #

mkDomainFree :: NamedArg Binder -> LamBinding Source #

defaultTbInfo :: TypedBindingInfo Source #

mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding Source #

mkPi :: ExprInfo -> Telescope -> Type -> Type Source #

noDataDefParams :: DataDefParams Source #

data WhereDeclarations Source #

Constructors

WhereDecls
Fields whereModule :: Maybe ModuleName whereAnywhere :: Bool is it an ordinary unnamed `where`? whereDecls :: Maybe Declaration The declaration is a `Section`.

Instances

Instances details

DeclaredNames WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => WhereDeclarations -> m Source #

ExprLike WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m WhereDeclarations Source #

foldExpr :: FoldExprFn m WhereDeclarations Source #

traverseExpr :: TraverseExprFn m WhereDeclarations Source #

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

HasRange WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: WhereDeclarations -> Range Source #

KillRange WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT WhereDeclarations Source #

ToConcrete WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs WhereDeclarations = WhereClause

Methods

toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations) Source #

bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b Source #

Null WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

empty :: WhereDeclarations Source #

null :: WhereDeclarations -> Bool Source #

Generic WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep WhereDeclarations

Instance details

Defined in Agda.Syntax.Abstract

type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))))

Methods

from :: WhereDeclarations -> Rep WhereDeclarations x #

to :: Rep WhereDeclarations x -> WhereDeclarations #

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

Methods

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

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

type ConOfAbs WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs WhereDeclarations = WhereClause

type Rep WhereDeclarations Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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)))))

noWhereDecls :: WhereDeclarations Source #

type SpineClause = Clause' SpineLHS Source #

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 spLhsInfo :: LHSInfo Range. spLhsDefName :: QName Name of function we are defining. spLhsPats :: [NamedArg Pattern] Elimination by pattern, projections, with-patterns.

Instances

Instances details

ExprLike SpineLHS Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m SpineLHS Source #

foldExpr :: FoldExprFn m SpineLHS Source #

traverseExpr :: TraverseExprFn m SpineLHS Source #

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

HasRange SpineLHS Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: SpineLHS -> Range Source #

KillRange SpineLHS Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT SpineLHS Source #

ToConcrete SpineLHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs SpineLHS = LHS

Methods

toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS) Source #

bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b Source #

Generic SpineLHS Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep SpineLHS

Instance details

Defined in Agda.Syntax.Abstract

type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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]))))

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

Methods

lhsToSpine :: Clause -> SpineClause Source #

spineToLhs :: SpineClause -> Clause Source #

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: LHS -> SpineLHS Source #

spineToLhs :: SpineLHS -> LHS Source #

type ConOfAbs SpineLHS Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs SpineLHS = LHS

type Rep SpineLHS Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.4.1-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]))))

type WithExpr' e = Named BindName (Arg e) Source #

type NAPs1 e = List1 (NamedArg (Pattern' e)) Source #

type Patterns = [NamedArg Pattern] Source #

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

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

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

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 Methods nameToExpr :: AbstractName -> Expr Source #
NameToExpr ResolvedName Source #	Turn a `ResolvedName` into an expression. Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source #

patternToExpr :: Pattern -> Expr Source #

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

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

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

default substExpr :: forall (t :: Type -> Type) b. (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 Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
SubstExpr Name Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, 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 Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source #
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 #

insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) 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.

Constructors

ClauseS RHSSpine WhereDeclarationsSpine

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.

Constructors

RHSS
AbsurdRHSS
WithRHSS (List1 ClauseSpine)
RewriteRHSS RHSSpine WhereDeclarationsSpine

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 Methods showsPrec :: Int -> WhereDeclarationsSpine -> ShowS # show :: WhereDeclarationsSpine -> String # showList :: [WhereDeclarationsSpine] -> ShowS #

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.

whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine Source #

The spine corresponding to a WhereDeclarations value.

module Agda.Syntax.Abstract.Name

Orphan instances

KillRange Suffix Source #
Instance details Methods killRange :: KillRangeT Suffix Source #

AxiomS
GeneralizeS
FieldS
PrimitiveS
MutualS [DeclarationSpine]
SectionS [DeclarationSpine]
ApplyS
ImportS
PragmaS
OpenS
FunDefS [ClauseSpine]
DataSigS
DataDefS
RecSigS
RecDefS [DeclarationSpine]
PatternSynDefS
UnquoteDeclS
UnquoteDefS
UnquoteDataS
ScopedDeclS [DeclarationSpine]
UnfoldingDeclS