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

Safe Haskell | Safe-Inferred
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

- class SubstExpr a where
  - substExpr :: [(Name, Expr)] -> a -> a
- type PatternSynDefns = Map QName PatternSynDefn
- type PatternSynDefn = ([Arg Name], Pattern' Void)
- class NameToExpr a where
  - nameToExpr :: a -> Expr
- class AnyAbstract a where
  - anyAbstract :: a -> Bool
- type HoleContent = HoleContent' () BindName Pattern Expr
- type Patterns = [NamedArg Pattern]
- type Pattern = Pattern' Expr
- type NAPs1 e = List1 (NamedArg (Pattern' e))
- type NAPs e = [NamedArg (Pattern' e)]
- 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 LHSCore = LHSCore' Expr
- 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)]
    }
- data LHS = LHS {
  - lhsInfo :: LHSInfo
  - lhsCore :: LHSCore
  }
- data SpineLHS = SpineLHS {
  - spLhsInfo :: LHSInfo
  - spLhsDefName :: QName
  - spLhsPats :: [NamedArg Pattern]
  }
- data RHS
  - = RHS {
    - rhsExpr :: Expr
    - rhsConcrete :: Maybe Expr
    }
  - | AbsurdRHS
  - | WithRHS QName [WithExpr] [Clause]
  - | RewriteRHS {
    - rewriteExprs :: [RewriteEqn]
    - rewriteStrippedPats :: [ProblemEq]
    - rewriteRHS :: RHS
    - rewriteWhereDecls :: WhereDeclarations
    }
- type WithExpr = WithExpr' Expr
- type WithExpr' e = Named BindName (Arg e)
- type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
- type SpineClause = Clause' SpineLHS
- type Clause = Clause' LHS
- data WhereDeclarations = WhereDecls {
  - whereModule :: Maybe ModuleName
  - whereDecls :: Maybe Declaration
  }
- data Clause' lhs = Clause {
  - clauseLHS :: lhs
  - clauseStrippedPats :: [ProblemEq]
  - clauseRHS :: RHS
  - clauseWhereDecls :: WhereDeclarations
  - clauseCatchall :: Bool
  }
- data ProblemEq = ProblemEq {
  - problemInPat :: Pattern
  - problemInst :: Term
  - problemType :: Dom Type
  }
- data DataDefParams = DataDefParams {
  - dataDefGeneralizedParams :: Set Name
  - dataDefParams :: [LamBinding]
  }
- data GeneralizeTelescope = GeneralizeTel {
  - generalizeTelVars :: Map QName Name
  - generalizeTel :: Telescope
  }
- type Telescope = [TypedBinding]
- type Telescope1 = List1 TypedBinding
- data TypedBinding
  - = TBind Range TacticAttr (List1 (NamedArg Binder)) Expr
  - | TLet Range (List1 LetBinding)
- data LamBinding
  - = DomainFree TacticAttr (NamedArg Binder)
  - | DomainFull TypedBinding
- type Binder = Binder' BindName
- data Binder' a = Binder {
  - binderPattern :: Maybe Pattern
  - binderName :: a
  }
- type TacticAttr = Maybe Expr
- type Field = TypeSignature
- type Constructor = TypeSignature
- type TypeSignature = Declaration
- data LetBinding
  - = LetBind LetInfo ArgInfo BindName Expr Expr
  - | LetPatBind LetInfo Pattern Expr
  - | LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
  - | LetOpen ModuleInfo ModuleName ImportDirective
  - | LetDeclaredVariable BindName
- 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
  - | DisplayPragma QName [NamedArg Pattern] Expr
- data ModuleApplication
  - = SectionApp Telescope ModuleName [NamedArg Expr]
  - | RecordModuleInstance ModuleName
- type ImportedName = ImportedName' QName ModuleName
- type Renaming = Renaming' QName ModuleName
- type ImportDirective = ImportDirective' QName ModuleName
- type DefInfo = DefInfo' Expr
- data Declaration
  - = Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Expr
  - | Generalize (Set QName) DefInfo ArgInfo QName Expr
  - | Field DefInfo QName (Arg Expr)
  - | Primitive DefInfo QName (Arg Expr)
  - | Mutual MutualInfo [Declaration]
  - | Section Range ModuleName GeneralizeTelescope [Declaration]
  - | Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
  - | Import ModuleInfo ModuleName ImportDirective
  - | Pragma Range Pragma
  - | Open ModuleInfo ModuleName ImportDirective
  - | FunDef DefInfo QName Delayed [Clause]
  - | DataSig DefInfo QName GeneralizeTelescope Expr
  - | DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
  - | RecSig DefInfo QName GeneralizeTelescope Expr
  - | RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Expr [Declaration]
  - | PatternSynDef QName [Arg BindName] (Pattern' Void)
  - | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
  - | UnquoteDef [DefInfo] [QName] Expr
  - | ScopedDecl ScopeInfo [Declaration]
- type RecordDirectives = RecordDirectives' QName
- data ScopeCopyInfo = ScopeCopyInfo {
  - renModules :: Ren ModuleName
  - renNames :: Ren QName
  }
- type Ren a = Map a (List1 a)
- type RecordAssigns = [RecordAssign]
- type RecordAssign = Either Assign ModuleName
- type Assigns = [Assign]
- type Assign = FieldAssignment' Expr
- 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 Expr
  - | Generalized (Set QName) Expr
  - | Fun ExprInfo (Arg Expr) Expr
  - | Let ExprInfo (List1 LetBinding) Expr
  - | ETel Telescope
  - | Rec ExprInfo RecordAssigns
  - | RecUpdate ExprInfo Expr Assigns
  - | ScopedExpr ScopeInfo Expr
  - | Quote ExprInfo
  - | QuoteTerm ExprInfo
  - | Unquote ExprInfo
  - | DontCare Expr
- type Args = [NamedArg Expr]
- newtype BindName = BindName {
  - unBind :: Name
  }
- pattern Def :: QName -> Expr
- mkBindName :: Name -> BindName
- generalized :: Set QName -> Expr -> Expr
- initCopyInfo :: ScopeCopyInfo
- mkBinder :: a -> Binder' a
- mkBinder_ :: Name -> Binder
- extractPattern :: Binder' a -> Maybe (Pattern, a)
- mkDomainFree :: NamedArg Binder -> LamBinding
- mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
- mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
- mkPi :: ExprInfo -> Telescope -> Expr -> Expr
- noDataDefParams :: DataDefParams
- noWhereDecls :: WhereDeclarations
- axiomName :: Declaration -> QName
- app :: Expr -> [NamedArg Expr] -> Expr
- mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
- patternToExpr :: Pattern -> Expr
- lambdaLiftExpr :: [Name] -> Expr -> Expr
- insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
- module Agda.Syntax.Abstract.Name

# Documentation

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

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

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

#### Instances

Instances details

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

type PatternSynDefns = Map QName PatternSynDefn Source #

type PatternSynDefn = ([Arg Name], Pattern' Void) 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 #

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 #

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

type Patterns = [NamedArg Pattern] Source #

type Pattern = Pattern' Expr Source #

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

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

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName |
ConP ConPatInfo AmbiguousQName (NAPs e) |
ProjP PatInfo ProjOrigin AmbiguousQName | Destructor pattern `d`.
DefP PatInfo AmbiguousQName (NAPs e) | Defined pattern: function definition `f ps`. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.
WildP PatInfo | Underscore pattern entered by user. Or generated at type checking for implicit arguments.
AsP PatInfo BindName (Pattern' e) |
DotP PatInfo e | Dot pattern `.e`
AbsurdP PatInfo |
LitP PatInfo Literal |
PatternSynP PatInfo AmbiguousQName (NAPs e) |
RecP PatInfo [FieldAssignment' (Pattern' e)] |
EqualP PatInfo [(e, e)] |
WithP PatInfo (Pattern' e) | `| p`, for with-patterns.
AnnP PatInfo e (Pattern' e) | Pattern with type annotation

#### Instances

Instances details

MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ToConcrete Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Pattern Source # Methods toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern) Source # bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b 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 Source #

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool Source #

length :: Pattern' a -> Int Source #

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

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

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

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

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

Traversable Pattern' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) Source # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) Source # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) Source # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) Source #
Functor Pattern' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b Source # (<$) :: a -> Pattern' b -> Pattern' a Source #
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) Source #

Methods

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

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

ExprLike a => ExprLike (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views 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 namesIn' :: Monoid m => (QName -> 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) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (Pattern' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Pattern' Expr) Source # 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 #
Data e => Data (Pattern' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' e -> c (Pattern' e) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' e) Source #

toConstr :: Pattern' e -> Constr Source #

dataTypeOf :: Pattern' e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Pattern' e)) Source #

gmapT :: (forall b. Data b => b -> b) -> Pattern' e -> Pattern' e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Pattern' e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) Source #

Generic (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Pattern' e) :: Type -> Type Source # Methods from :: Pattern' e -> Rep (Pattern' e) x Source # to :: Rep (Pattern' e) x -> Pattern' e Source #
Show e => Show (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pattern' e -> ShowS Source # show :: Pattern' e -> String Source # showList :: [Pattern' e] -> ShowS Source #
NFData e => NFData (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pattern' e -> () Source #
Eq e => Eq (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pattern' e -> Pattern' e -> Bool Source # (/=) :: Pattern' e -> Pattern' e -> Bool Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 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 Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: ((C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo))) :+: (C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))) :+: C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e))))) :+: ((C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: (C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))))) :+: ((C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])) :+: C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(e, e)]))) :+: (C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))))

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

type LHSCore = LHSCore' Expr 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 Source # 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 Source #

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

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

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

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

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

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

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

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

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

null :: LHSCore' a -> Bool Source #

length :: LHSCore' a -> Int Source #

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

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

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

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

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

Traversable LHSCore' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) Source # sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) Source # mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) Source # sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a) Source #
Functor LHSCore' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> LHSCore' a -> LHSCore' b Source # (<$) :: a -> LHSCore' b -> LHSCore' a Source #
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) Source # Methods toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #
Data e => Data (LHSCore' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore' e -> c (LHSCore' e) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LHSCore' e) Source #

toConstr :: LHSCore' e -> Constr Source #

dataTypeOf :: LHSCore' e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LHSCore' e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (LHSCore' e)) Source #

gmapT :: (forall b. Data b => b -> b) -> LHSCore' e -> LHSCore' e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LHSCore' e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore' e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) Source #

Generic (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (LHSCore' e) :: Type -> Type Source # Methods from :: LHSCore' e -> Rep (LHSCore' e) x Source # to :: Rep (LHSCore' e) x -> LHSCore' e Source #
Show e => Show (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHSCore' e -> ShowS Source # show :: LHSCore' e -> String Source # showList :: [LHSCore' e] -> ShowS Source #
NFData e => NFData (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHSCore' e -> () Source #
Eq e => Eq (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHSCore' e -> LHSCore' e -> Bool Source # (/=) :: LHSCore' e -> LHSCore' e -> Bool Source #
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 Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "LHSHead" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])) :+: (C1 ('MetaCons "LHSProj" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDestructor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: (S1 ('MetaSel ('Just "lhsFocus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg (LHSCore' e))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))) :+: C1 ('MetaCons "LHSWith" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsHead") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LHSCore' e)) :*: (S1 ('MetaSel ('Just "lhsWithPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg (Pattern' e)]) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])))))

data LHS Source #

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

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 Source # Methods toConcrete :: LHS -> AbsToCon (ConOfAbs LHS) Source # bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b Source #
Data LHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS Source #

toConstr :: LHS -> Constr Source #

dataTypeOf :: LHS -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) Source #

gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS Source #

Generic LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LHS :: Type -> Type Source # Methods from :: LHS -> Rep LHS x Source # to :: Rep LHS x -> LHS Source #
Show LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHS -> ShowS Source # show :: LHS -> String Source # showList :: [LHS] -> ShowS Source #
NFData LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHS -> () Source #
Eq LHS Source # | Ignore `Range` when comparing `LHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHS -> LHS -> Bool Source # (/=) :: LHS -> LHS -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 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 Source # Methods toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS) Source # bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b Source #
Data SpineLHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpineLHS -> c SpineLHS Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpineLHS Source #

toConstr :: SpineLHS -> Constr Source #

dataTypeOf :: SpineLHS -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpineLHS) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpineLHS) Source #

gmapT :: (forall b. Data b => b -> b) -> SpineLHS -> SpineLHS Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> SpineLHS -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SpineLHS -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS Source #

Generic SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep SpineLHS :: Type -> Type Source # Methods from :: SpineLHS -> Rep SpineLHS x Source # to :: Rep SpineLHS x -> SpineLHS Source #
Show SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> SpineLHS -> ShowS Source # show :: SpineLHS -> String Source # showList :: [SpineLHS] -> ShowS Source #
NFData SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: SpineLHS -> () Source #
Eq SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: SpineLHS -> SpineLHS -> Bool Source # (/=) :: SpineLHS -> SpineLHS -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]))))

data 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] [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 Source # Methods toConcrete :: RHS -> AbsToCon (ConOfAbs RHS) Source # bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b Source #
Data RHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS -> c RHS Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RHS Source #

toConstr :: RHS -> Constr Source #

dataTypeOf :: RHS -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RHS) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RHS) Source #

gmapT :: (forall b. Data b => b -> b) -> RHS -> RHS Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> RHS -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS -> m RHS Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS Source #

Generic RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep RHS :: Type -> Type Source # Methods from :: RHS -> Rep RHS x Source # to :: Rep RHS x -> RHS Source #
Show RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHS -> ShowS Source # show :: RHS -> String Source # showList :: [RHS] -> ShowS Source #
NFData RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: RHS -> () Source #
Eq RHS Source # | Ignore `rhsConcrete` when comparing `RHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: RHS -> RHS -> Bool Source # (/=) :: RHS -> RHS -> Bool Source #
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 Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((C1 ('MetaCons "RHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "rhsExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "rhsConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "AbsurdRHS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithRHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithExpr]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: C1 ('MetaCons "RewriteRHS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rewriteExprs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RewriteEqn]) :*: S1 ('MetaSel ('Just "rewriteStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "rewriteRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: S1 ('MetaSel ('Just "rewriteWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations)))))

type WithExpr = WithExpr' Expr Source #

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

type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #

type SpineClause = Clause' SpineLHS Source #

type Clause = Clause' LHS Source #

data WhereDeclarations Source #

Constructors

WhereDecls |

Fields

- whereModule :: Maybe ModuleName
- 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 Source # 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 #
Data WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereDeclarations -> c WhereDeclarations Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WhereDeclarations Source #

toConstr :: WhereDeclarations -> Constr Source #

dataTypeOf :: WhereDeclarations -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c WhereDeclarations) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c WhereDeclarations) Source #

gmapT :: (forall b. Data b => b -> b) -> WhereDeclarations -> WhereDeclarations Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WhereDeclarations -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereDeclarations -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations Source #

Generic WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep WhereDeclarations :: Type -> Type Source # Methods from :: WhereDeclarations -> Rep WhereDeclarations x Source # to :: Rep WhereDeclarations x -> WhereDeclarations Source #
Show WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarations -> ShowS Source # show :: WhereDeclarations -> String Source # showList :: [WhereDeclarations] -> ShowS Source #
NFData WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: WhereDeclarations -> () Source #
Eq WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: WhereDeclarations -> WhereDeclarations -> Bool Source # (/=) :: WhereDeclarations -> WhereDeclarations -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration))))

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

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

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

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

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

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

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

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

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

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

null :: Clause' a -> Bool Source #

length :: Clause' a -> Int Source #

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

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

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

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

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

Traversable Clause' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) Source # sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) Source # mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) Source # sequence :: Monad m => Clause' (m a) -> m (Clause' a) Source #
Functor Clause' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Clause' a -> Clause' b Source # (<$) :: a -> Clause' b -> Clause' a Source #
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) Source # Methods toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a)) Source # bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b Source #
Data lhs => Data (Clause' lhs) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause' lhs -> c (Clause' lhs) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Clause' lhs) Source #

toConstr :: Clause' lhs -> Constr Source #

dataTypeOf :: Clause' lhs -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Clause' lhs)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Clause' lhs)) Source #

gmapT :: (forall b. Data b => b -> b) -> Clause' lhs -> Clause' lhs Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Clause' lhs -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause' lhs -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) Source #

Generic (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Clause' lhs) :: Type -> Type Source # Methods from :: Clause' lhs -> Rep (Clause' lhs) x Source # to :: Rep (Clause' lhs) x -> Clause' lhs Source #
Show lhs => Show (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Clause' lhs -> ShowS Source # show :: Clause' lhs -> String Source # showList :: [Clause' lhs] -> ShowS Source #
NFData lhs => NFData (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Clause' lhs -> () Source #
Eq lhs => Eq (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Clause' lhs -> Clause' lhs -> Bool Source # (/=) :: Clause' lhs -> Clause' lhs -> Bool Source #
type ConOfAbs (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = [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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 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 Source # Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #
Data ProblemEq Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq Source #

toConstr :: ProblemEq -> Constr Source #

dataTypeOf :: ProblemEq -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) Source #

gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq Source #

Generic ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ProblemEq :: Type -> Type Source # Methods from :: ProblemEq -> Rep ProblemEq x Source # to :: Rep ProblemEq x -> ProblemEq Source #
Show ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ProblemEq -> ShowS Source # show :: ProblemEq -> String Source # showList :: [ProblemEq] -> ShowS Source #
NFData ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ProblemEq -> () Source #
Eq ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ProblemEq -> ProblemEq -> Bool Source # (/=) :: ProblemEq -> ProblemEq -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 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 #
Data DataDefParams Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDefParams -> c DataDefParams Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDefParams Source #

toConstr :: DataDefParams -> Constr Source #

dataTypeOf :: DataDefParams -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDefParams) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDefParams) Source #

gmapT :: (forall b. Data b => b -> b) -> DataDefParams -> DataDefParams Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DataDefParams -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDefParams -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams Source #

Generic DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep DataDefParams :: Type -> Type Source # Methods from :: DataDefParams -> Rep DataDefParams x Source # to :: Rep DataDefParams x -> DataDefParams Source #
Show DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DataDefParams -> ShowS Source # show :: DataDefParams -> String Source # showList :: [DataDefParams] -> ShowS Source #
NFData DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: DataDefParams -> () Source #
Eq DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: DataDefParams -> DataDefParams -> Bool Source # (/=) :: DataDefParams -> DataDefParams -> Bool Source #
type Rep DataDefParams Source # |

Instance details

Defined in Agda.Syntax.Abstract

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

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 #
Data GeneralizeTelescope Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizeTelescope -> c GeneralizeTelescope Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizeTelescope Source #

toConstr :: GeneralizeTelescope -> Constr Source #

dataTypeOf :: GeneralizeTelescope -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizeTelescope) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizeTelescope) Source #

gmapT :: (forall b. Data b => b -> b) -> GeneralizeTelescope -> GeneralizeTelescope Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> GeneralizeTelescope -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizeTelescope -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope Source #

Generic GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep GeneralizeTelescope :: Type -> Type Source # Methods from :: GeneralizeTelescope -> Rep GeneralizeTelescope x Source # to :: Rep GeneralizeTelescope x -> GeneralizeTelescope Source #
Show GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> GeneralizeTelescope -> ShowS Source # show :: GeneralizeTelescope -> String Source # showList :: [GeneralizeTelescope] -> ShowS Source #
NFData GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: GeneralizeTelescope -> () Source #
Eq GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool Source # (/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool Source #
type Rep GeneralizeTelescope Source # |

Instance details

Defined in Agda.Syntax.Abstract

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

type Telescope = [TypedBinding] Source #

type Telescope1 = List1 TypedBinding Source #

data TypedBinding Source #

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

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

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

Constructors

TBind Range TacticAttr (List1 (NamedArg Binder)) Expr | 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 Source # 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 #
Data TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding -> c TypedBinding Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypedBinding Source #

toConstr :: TypedBinding -> Constr Source #

dataTypeOf :: TypedBinding -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypedBinding) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypedBinding) Source #

gmapT :: (forall b. Data b => b -> b) -> TypedBinding -> TypedBinding Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TypedBinding -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding Source #

Generic TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep TypedBinding :: Type -> Type Source # Methods from :: TypedBinding -> Rep TypedBinding x Source # to :: Rep TypedBinding x -> TypedBinding Source #
Show TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBinding -> ShowS Source # show :: TypedBinding -> String Source # showList :: [TypedBinding] -> ShowS Source #
NFData TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: TypedBinding -> () Source #
Eq TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: TypedBinding -> TypedBinding -> Bool Source # (/=) :: TypedBinding -> TypedBinding -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 TacticAttr)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding))))

data 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 Source # Methods toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source # bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b Source #
Data LamBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding -> c LamBinding Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamBinding Source #

toConstr :: LamBinding -> Constr Source #

dataTypeOf :: LamBinding -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamBinding) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamBinding) Source #

gmapT :: (forall b. Data b => b -> b) -> LamBinding -> LamBinding Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LamBinding -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding Source #

Generic LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LamBinding :: Type -> Type Source # Methods from :: LamBinding -> Rep LamBinding x Source # to :: Rep LamBinding x -> LamBinding Source #
Show LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
NFData LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LamBinding -> () Source #
Eq LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LamBinding -> LamBinding -> Bool Source # (/=) :: LamBinding -> LamBinding -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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)))

type Binder = Binder' BindName Source #

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

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

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

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

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

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

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

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

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

toList :: Binder' a -> [a] Source #

null :: Binder' a -> Bool Source #

length :: Binder' a -> Int Source #

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

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

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

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

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

Traversable Binder' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) Source # sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) Source # mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) Source # sequence :: Monad m => Binder' (m a) -> m (Binder' a) Source #
Functor Binder' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Binder' a -> Binder' b Source # (<$) :: a -> Binder' b -> Binder' a Source #
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) Source # Methods toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a)) Source # bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b Source #
Data a => Data (Binder' a) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder' a -> c (Binder' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder' a) Source #

toConstr :: Binder' a -> Constr Source #

dataTypeOf :: Binder' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Binder' a -> Binder' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Binder' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) Source #

Generic (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Binder' a) :: Type -> Type Source # Methods from :: Binder' a -> Rep (Binder' a) x Source # to :: Rep (Binder' a) x -> Binder' a Source #
Show a => Show (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Binder' a -> ShowS Source # show :: Binder' a -> String Source # showList :: [Binder' a] -> ShowS Source #
NFData a => NFData (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Binder' a -> () Source #
Eq a => Eq (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Binder' a -> Binder' a -> Bool Source # (/=) :: Binder' a -> Binder' a -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 TacticAttr = Maybe Expr Source #

type Field = TypeSignature Source #

type Constructor = TypeSignature Source #

type TypeSignature = Declaration Source #

Only `Axiom`s.

data LetBinding Source #

Bindings that are valid in a `let`.

Constructors

LetBind LetInfo ArgInfo BindName Expr Expr

    LetBind info rel name type defn

LetPatBind LetInfo Pattern Expr | Irrefutable pattern binding.
LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective | `LetApply mi newM (oldM args) renamings dir`. The `ImportDirective` is for highlighting purposes.
LetOpen ModuleInfo ModuleName ImportDirective | only for highlighting and abstractToConcrete
LetDeclaredVariable BindName | Only used for highlighting. Refers to the first occurrence of `x` in `let x : A; x = e`. | LetGeneralize DefInfo ArgInfo Expr

#### 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 Source # Methods toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source # bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b Source #
Data LetBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetBinding -> c LetBinding Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBinding Source #

toConstr :: LetBinding -> Constr Source #

dataTypeOf :: LetBinding -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetBinding) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetBinding) Source #

gmapT :: (forall b. Data b => b -> b) -> LetBinding -> LetBinding Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LetBinding -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBinding -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding Source #

Generic LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LetBinding :: Type -> Type Source # Methods from :: LetBinding -> Rep LetBinding x Source # to :: Rep LetBinding x -> LetBinding Source #
Show LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LetBinding -> ShowS Source # show :: LetBinding -> String Source # showList :: [LetBinding] -> ShowS Source #
NFData LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LetBinding -> () Source #
Eq LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LetBinding -> LetBinding -> Bool Source # (/=) :: LetBinding -> LetBinding -> Bool Source #
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 Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)))))

data 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 |
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 #
Data Pragma Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma Source #

toConstr :: Pragma -> Constr Source #

dataTypeOf :: Pragma -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) Source #

gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma Source #

Generic Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Pragma :: Type -> Type Source # Methods from :: Pragma -> Rep Pragma x Source # to :: Rep Pragma x -> Pragma Source #
Show Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
NFData Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pragma -> () Source #
Eq Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pragma -> Pragma -> Bool Source # (/=) :: Pragma -> Pragma -> Bool Source #
type Rep Pragma Source # |

Instance details

Defined in Agda.Syntax.Abstract

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

data 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 Source # Methods toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source # bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b Source #
Data ModuleApplication Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleApplication -> c ModuleApplication Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication Source #

toConstr :: ModuleApplication -> Constr Source #

dataTypeOf :: ModuleApplication -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication) Source #

gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication Source #

Generic ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ModuleApplication :: Type -> Type Source # Methods from :: ModuleApplication -> Rep ModuleApplication x Source # to :: Rep ModuleApplication x -> ModuleApplication Source #
Show ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ModuleApplication -> ShowS Source # show :: ModuleApplication -> String Source # showList :: [ModuleApplication] -> ShowS Source #
NFData ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ModuleApplication -> () Source #
Eq ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ModuleApplication -> ModuleApplication -> Bool Source # (/=) :: ModuleApplication -> ModuleApplication -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 ImportedName = ImportedName' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type ImportDirective = ImportDirective' QName ModuleName Source #

type DefInfo = DefInfo' Expr Source #

data Declaration Source #

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Expr | Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments.
Generalize (Set QName) DefInfo ArgInfo QName Expr | First argument is set of generalizable variables used in the type.
Field DefInfo QName (Arg Expr) | record field
Primitive DefInfo QName (Arg Expr) | primitive function
Mutual MutualInfo [Declaration] | a bunch of mutually recursive definitions
Section Range ModuleName GeneralizeTelescope [Declaration] |
Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective | The `ImportDirective` is for highlighting purposes.
Import ModuleInfo ModuleName ImportDirective | The `ImportDirective` is for highlighting purposes.
Pragma Range Pragma |
Open ModuleInfo ModuleName ImportDirective | only retained for highlighting purposes
FunDef DefInfo QName Delayed [Clause] | sequence of function clauses
DataSig DefInfo QName GeneralizeTelescope Expr | lone data signature
DataDef DefInfo QName UniverseCheck DataDefParams [Constructor] |
RecSig DefInfo QName GeneralizeTelescope Expr | lone record signature
RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Expr [Declaration] | The `Expr` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Prop`, 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 |
ScopedDecl ScopeInfo [Declaration] | scope annotation

#### 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 Source # 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 #
Data Declaration Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration Source #

toConstr :: Declaration -> Constr Source #

dataTypeOf :: Declaration -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) Source #

gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration Source #

Generic Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Declaration :: Type -> Type Source # Methods from :: Declaration -> Rep Declaration x Source # to :: Rep Declaration x -> Declaration Source #
Show Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Declaration -> ShowS Source # show :: Declaration -> String Source # showList :: [Declaration] -> ShowS Source #
NFData Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Declaration -> () Source #
Eq Declaration Source # | Does not compare `ScopeInfo` fields.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Declaration -> Declaration -> Bool Source # (/=) :: Declaration -> Declaration -> Bool Source #
ToConcrete (Constr Constructor) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Constr Constructor) Source # 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 Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Occurrence])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))))) :+: ((C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: (C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)))))) :+: (((C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "FunDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Delayed) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))) :+: (C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg BindName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void))))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))))))

type ConOfAbs (Constr Constructor) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

type RecordDirectives = RecordDirectives' QName Source #

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo |

Fields

- renModules :: Ren ModuleName
- renNames :: Ren QName

#### Instances

Instances details

KillRange ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo Source #
Pretty ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
Data ScopeCopyInfo Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopeCopyInfo -> c ScopeCopyInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeCopyInfo Source #

toConstr :: ScopeCopyInfo -> Constr Source #

dataTypeOf :: ScopeCopyInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ScopeCopyInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ScopeCopyInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ScopeCopyInfo -> ScopeCopyInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ScopeCopyInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeCopyInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo Source #

Generic ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ScopeCopyInfo :: Type -> Type Source # Methods from :: ScopeCopyInfo -> Rep ScopeCopyInfo x Source # to :: Rep ScopeCopyInfo x -> ScopeCopyInfo Source #
Show ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS Source # show :: ScopeCopyInfo -> String Source # showList :: [ScopeCopyInfo] -> ShowS Source #
NFData ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ScopeCopyInfo -> () Source #
Eq ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool Source # (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool Source #
type Rep ScopeCopyInfo Source # |

Instance details

Defined in Agda.Syntax.Abstract

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

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

Renaming (generic).

type RecordAssigns = [RecordAssign] Source #

type RecordAssign = Either Assign ModuleName Source #

type Assigns = [Assign] Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment `f = e`.

data Expr Source #

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

Constructors

Var Name | Bound variable.
Def' QName Suffix | Constant: axiom, function, data or record type, with a possible suffix.
Proj ProjOrigin AmbiguousQName | Projection (overloaded).
Con AmbiguousQName | Constructor (overloaded).
PatternSyn AmbiguousQName | Pattern synonym.
Macro QName | Macro.
Lit ExprInfo Literal | Literal.
QuestionMark MetaInfo InteractionId | Meta variable for interaction. The `InteractionId` is usually identical with the `metaNumber` of `MetaInfo`. However, if you want to print an interaction meta as just `?` instead of `?n`, you should set the `metaNumber` to `Nothing` while keeping the `InteractionId`.
Underscore MetaInfo | Meta variable for hidden argument (must be inferred locally).
Dot ExprInfo Expr | `.e`, for postfix projection.
App AppInfo Expr (NamedArg Expr) | Ordinary (binary) application.
WithApp ExprInfo Expr [Expr] | With application.
Lam ExprInfo LamBinding Expr | `λ bs → e`.
AbsurdLam ExprInfo Hiding | `λ()` or `λ{}`.
ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) |
Pi ExprInfo Telescope1 Expr | Dependent function space `Γ → A`.
Generalized (Set QName) Expr | Like a Pi, but the ordering is not known
Fun ExprInfo (Arg Expr) Expr | Non-dependent function space.
Let ExprInfo (List1 LetBinding) Expr | `let bs in e`.
ETel Telescope | Only used when printing telescopes.
Rec ExprInfo RecordAssigns | Record construction.
RecUpdate ExprInfo Expr Assigns | Record update.
ScopedExpr ScopeInfo Expr | Scope annotation.
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 Source # 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 Source # 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 Source # 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 Source # Methods reify :: MonadReify m => Expr -> m (ReifiesTo Expr) Source # reifyWhen :: MonadReify m => Bool -> Expr -> m (ReifiesTo Expr) Source #
PrettyTCM Expr Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
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 #
Data Expr Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr Source #

toConstr :: Expr -> Constr Source #

dataTypeOf :: Expr -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) Source #

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source #

Generic Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Expr :: Type -> Type Source # Methods from :: Expr -> Rep Expr x Source # to :: Rep Expr x -> Expr Source #
Show Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
NFData Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Expr -> () Source #
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 Source # (/=) :: Expr -> Expr -> Bool Source #
ToConcrete (Maybe Pattern) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe Pattern) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
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) Source # 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) Source # 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) Source # 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 Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "Generalized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "Fun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "ETel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope))))) :+: ((C1 ('MetaCons "Rec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordAssigns)) :+: (C1 ('MetaCons "RecUpdate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assigns))) :+: C1 ('MetaCons "ScopedExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "Quote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "QuoteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo))) :+: (C1 ('MetaCons "Unquote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "DontCare" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

type ConOfAbs (Maybe Pattern) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfRef (Expr, Elim) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, 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 Args = [NamedArg 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 Source # 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 #
Data BindName Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindName -> c BindName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindName Source #

toConstr :: BindName -> Constr Source #

dataTypeOf :: BindName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindName) Source #

gmapT :: (forall b. Data b => b -> b) -> BindName -> BindName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> BindName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BindName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindName -> m BindName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName Source #

Show BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> BindName -> ShowS Source # show :: BindName -> String Source # showList :: [BindName] -> ShowS Source #
NFData BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: BindName -> () Source #
Eq BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: BindName -> BindName -> Bool Source # (/=) :: BindName -> BindName -> Bool Source #
Ord BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods compare :: BindName -> BindName -> Ordering Source # (<) :: BindName -> BindName -> Bool Source # (<=) :: BindName -> BindName -> Bool Source # (>) :: BindName -> BindName -> Bool Source # (>=) :: BindName -> BindName -> Bool Source # max :: BindName -> BindName -> BindName Source # min :: BindName -> BindName -> BindName Source #
ToConcrete (Maybe BindName) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe BindName) Source # Methods toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName)) Source # bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b Source #
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (RewriteEqn' qn BindName p a) Source # 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) Source # 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

pattern Def :: QName -> Expr Source #

Pattern synonym for regular Def

mkBindName :: Name -> BindName Source #

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

Smart constructor for Generalized

initCopyInfo :: ScopeCopyInfo Source #

mkBinder :: a -> Binder' a Source #

mkBinder_ :: Name -> Binder Source #

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

mkDomainFree :: NamedArg Binder -> LamBinding Source #

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

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

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

noDataDefParams :: DataDefParams Source #

noWhereDecls :: WhereDeclarations Source #

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

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

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

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

patternToExpr :: Pattern -> Expr Source #

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

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

module Agda.Syntax.Abstract.Name

# Orphan instances

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