Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Abstract
Contents
Description
The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).
Synopsis
- class SubstExpr a where
- 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
- data LHS = LHS {}
- data SpineLHS = SpineLHS {}
- data RHS
- 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
- data LamBinding
- 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
- 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
- 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 {}
- 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
Instances
SubstExpr Name Source # | |
SubstExpr ModuleName Source # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source # | |
SubstExpr Expr Source # | |
SubstExpr a => SubstExpr [a] Source # | |
SubstExpr a => SubstExpr (Maybe a) Source # | |
SubstExpr a => SubstExpr (List1 a) Source # | |
SubstExpr a => SubstExpr (Arg a) Source # | |
SubstExpr a => SubstExpr (FieldAssignment' a) Source # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source # | |
(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source # | |
(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source # | |
SubstExpr a => SubstExpr (Named name a) Source # | |
type PatternSynDefns = Map QName PatternSynDefn Source #
class NameToExpr a where Source #
Turn a name into an expression.
Methods
nameToExpr :: a -> Expr Source #
Instances
NameToExpr ResolvedName Source # | Turn a Assumes name is not |
Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source # | |
NameToExpr AbstractName Source # | Turn an |
Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> 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
AnyAbstract Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source # | |
AnyAbstract a => AnyAbstract [a] Source # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: [a] -> Bool Source # |
type HoleContent = HoleContent' () BindName Pattern Expr Source #
Parameterised over the type of dot patterns.
Constructors
VarP BindName | |
ConP ConPatInfo AmbiguousQName (NAPs e) | |
ProjP PatInfo ProjOrigin AmbiguousQName | Destructor pattern |
DefP PatInfo AmbiguousQName (NAPs e) | Defined pattern: function definition |
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 |
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) | Pattern with type annotation |
Instances
Functor Pattern' Source # | |
Foldable Pattern' Source # | |
Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Pattern' m -> m foldMap :: Monoid m => (a -> m) -> Pattern' a -> m foldMap' :: Monoid m => (a -> m) -> Pattern' a -> m foldr :: (a -> b -> b) -> b -> Pattern' a -> b foldr' :: (a -> b -> b) -> b -> Pattern' a -> b foldl :: (b -> a -> b) -> b -> Pattern' a -> b foldl' :: (b -> a -> b) -> b -> Pattern' a -> b foldr1 :: (a -> a -> a) -> Pattern' a -> a foldl1 :: (a -> a -> a) -> Pattern' a -> a elem :: Eq a => a -> Pattern' a -> Bool maximum :: Ord a => Pattern' a -> a minimum :: Ord a => Pattern' a -> a | |
Traversable Pattern' Source # | |
MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
ToConcrete Pattern Source # | |
IsFlexiblePattern Pattern Source # | |
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 # | |
Eq e => Eq (Pattern' e) Source # | |
Data e => Data (Pattern' e) Source # | |
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) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' e) toConstr :: Pattern' e -> Constr dataTypeOf :: Pattern' e -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' e)) dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Pattern' e)) gmapT :: (forall b. Data b => b -> b) -> Pattern' e -> Pattern' e gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r gmapQ :: (forall d. Data d => d -> u) -> Pattern' e -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' e -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) | |
Show e => Show (Pattern' e) Source # | |
Generic (Pattern' e) Source # | |
NFData e => NFData (Pattern' e) Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange e => KillRange (Pattern' e) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source # | |
SetRange (Pattern' a) Source # | |
HasRange (Pattern' e) Source # | |
IsProjP (Pattern' e) Source # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
IsWithP (Pattern' e) Source # | Check for with-pattern. |
ExprLike a => ExprLike (Pattern' a) Source # | |
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 # | |
APatternLike (Pattern' a) Source # | |
Defined in Agda.Syntax.Abstract.Pattern 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 # | |
EmbPrj a => EmbPrj (Pattern' a) Source # | |
NamesIn (Pattern' a) Source # | |
ToConcrete (Maybe Pattern) Source # | |
ExpandPatternSynonyms (Pattern' e) Source # | |
Defined in Agda.TypeChecking.Patterns.Abstract | |
ToAbstract (Pattern' Expr) Source # | |
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |
type ConOfAbs Pattern Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type Rep (Pattern' e) Source # | |
Defined in Agda.Syntax.Abstract type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 ADotT (Pattern' a) Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
type ConOfAbs (Maybe Pattern) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type AbsOfCon (Pattern' Expr) Source # | |
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
The lhs in projection-application and with-pattern view.
Parameterised over the type e
of dot patterns.
Constructors
LHSHead | The head applied to ordinary patterns. |
Fields
| |
LHSProj | Projection. |
Fields
| |
LHSWith | With patterns. |
Instances
Functor LHSCore' Source # | |
Foldable LHSCore' Source # | |
Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => LHSCore' m -> m foldMap :: Monoid m => (a -> m) -> LHSCore' a -> m foldMap' :: Monoid m => (a -> m) -> LHSCore' a -> m foldr :: (a -> b -> b) -> b -> LHSCore' a -> b foldr' :: (a -> b -> b) -> b -> LHSCore' a -> b foldl :: (b -> a -> b) -> b -> LHSCore' a -> b foldl' :: (b -> a -> b) -> b -> LHSCore' a -> b foldr1 :: (a -> a -> a) -> LHSCore' a -> a foldl1 :: (a -> a -> a) -> LHSCore' a -> a elem :: Eq a => a -> LHSCore' a -> Bool maximum :: Ord a => LHSCore' a -> a minimum :: Ord a => LHSCore' a -> a | |
Traversable LHSCore' Source # | |
ToConcrete LHSCore Source # | |
Eq e => Eq (LHSCore' e) Source # | |
Data e => Data (LHSCore' e) Source # | |
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) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LHSCore' e) toConstr :: LHSCore' e -> Constr dataTypeOf :: LHSCore' e -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LHSCore' e)) dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (LHSCore' e)) gmapT :: (forall b. Data b => b -> b) -> LHSCore' e -> LHSCore' e gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r gmapQ :: (forall d. Data d => d -> u) -> LHSCore' e -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore' e -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) | |
Show e => Show (LHSCore' e) Source # | |
Generic (LHSCore' e) Source # | |
NFData e => NFData (LHSCore' e) Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange e => KillRange (LHSCore' e) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source # | |
HasRange (LHSCore' e) Source # | |
ExprLike a => ExprLike (LHSCore' a) Source # | |
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 # | |
ToAbstract (LHSCore' Expr) Source # | |
type ConOfAbs LHSCore Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type Rep (LHSCore' e) Source # | |
Defined in Agda.Syntax.Abstract type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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)]))))) | |
type AbsOfCon (LHSCore' Expr) Source # | |
The lhs of a clause in focused (projection-application) view (outside-in).
Projection patters are represented as LHSProj
s.
Instances
Eq LHS Source # | |
Data LHS Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS dataTypeOf :: LHS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS | |
Show LHS Source # | |
Generic LHS Source # | |
NFData LHS Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange LHS Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange LHS Source # | |
DeclaredNames Clause Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source # | |
ExprLike LHS Source # | |
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LHS Source # foldExpr :: FoldExprFn m LHS Source # traverseExpr :: TraverseExprFn m LHS Source # | |
ToConcrete LHS Source # | |
LHSToSpine LHS SpineLHS Source # | LHS instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
LHSToSpine Clause SpineClause Source # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
type Rep LHS Source # | |
Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore))) | |
type ConOfAbs LHS Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
The lhs of a clause in spine view (inside-out).
Projection patterns are contained in spLhsPats
,
represented as ProjP d
.
Constructors
SpineLHS | |
Instances
Eq SpineLHS Source # | |
Data SpineLHS Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpineLHS toConstr :: SpineLHS -> Constr dataTypeOf :: SpineLHS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpineLHS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpineLHS) gmapT :: (forall b. Data b => b -> b) -> SpineLHS -> SpineLHS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r gmapQ :: (forall d. Data d => d -> u) -> SpineLHS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SpineLHS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS | |
Show SpineLHS Source # | |
Generic SpineLHS Source # | |
NFData SpineLHS Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange SpineLHS Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange SpineLHS Source # | |
ExprLike SpineLHS Source # | |
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m SpineLHS Source # foldExpr :: FoldExprFn m SpineLHS Source # | |
ToConcrete SpineLHS Source # | |
LHSToSpine LHS SpineLHS Source # | LHS instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
LHSToSpine Clause SpineClause Source # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
type Rep SpineLHS Source # | |
Defined in Agda.Syntax.Abstract type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern])))) | |
type ConOfAbs SpineLHS Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
Constructors
RHS | |
Fields
| |
AbsurdRHS | |
WithRHS QName [WithExpr] [Clause] | The |
RewriteRHS | |
Fields
|
Instances
Eq RHS Source # | Ignore |
Data RHS Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RHS dataTypeOf :: RHS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RHS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RHS) gmapT :: (forall b. Data b => b -> b) -> RHS -> RHS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r gmapQ :: (forall d. Data d => d -> u) -> RHS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS -> m RHS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS | |
Show RHS Source # | |
Generic RHS Source # | |
NFData RHS Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange RHS Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange RHS Source # | |
DeclaredNames RHS Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RHS -> m Source # | |
ExprLike RHS Source # | |
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m RHS Source # foldExpr :: FoldExprFn m RHS Source # traverseExpr :: TraverseExprFn m RHS Source # | |
ToConcrete RHS Source # | |
type Rep RHS Source # | |
Defined in Agda.Syntax.Abstract type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 ConOfAbs RHS Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #
type SpineClause = Clause' SpineLHS Source #
data WhereDeclarations Source #
Constructors
WhereDecls | |
Fields
|
Instances
We could throw away where
clauses at this point and translate them to
let
. It's not obvious how to remember that the let
was really a
where
clause though, so for the time being we keep it here.
Constructors
Clause | |
Fields
|
Instances
Functor Clause' Source # | |
Foldable Clause' Source # | |
Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Clause' m -> m foldMap :: Monoid m => (a -> m) -> Clause' a -> m foldMap' :: Monoid m => (a -> m) -> Clause' a -> m foldr :: (a -> b -> b) -> b -> Clause' a -> b foldr' :: (a -> b -> b) -> b -> Clause' a -> b foldl :: (b -> a -> b) -> b -> Clause' a -> b foldl' :: (b -> a -> b) -> b -> Clause' a -> b foldr1 :: (a -> a -> a) -> Clause' a -> a foldl1 :: (a -> a -> a) -> Clause' a -> a elem :: Eq a => a -> Clause' a -> Bool maximum :: Ord a => Clause' a -> a minimum :: Ord a => Clause' a -> a | |
Traversable Clause' Source # | |
DeclaredNames Clause Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source # | |
LHSToSpine Clause SpineClause Source # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
Eq lhs => Eq (Clause' lhs) Source # | |
Data lhs => Data (Clause' lhs) Source # | |
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) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Clause' lhs) toConstr :: Clause' lhs -> Constr dataTypeOf :: Clause' lhs -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Clause' lhs)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Clause' lhs)) gmapT :: (forall b. Data b => b -> b) -> Clause' lhs -> Clause' lhs gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r gmapQ :: (forall d. Data d => d -> u) -> Clause' lhs -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause' lhs -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) | |
Show lhs => Show (Clause' lhs) Source # | |
Generic (Clause' lhs) Source # | |
NFData lhs => NFData (Clause' lhs) Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange a => KillRange (Clause' a) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source # | |
HasRange a => HasRange (Clause' a) Source # | |
ExprLike a => ExprLike (Clause' a) Source # | |
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 # | |
(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # | |
type Rep (Clause' lhs) Source # | |
Defined in Agda.Syntax.Abstract type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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))))) | |
type ConOfAbs (Clause' a) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
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
|
Instances
Eq ProblemEq Source # | |
Data ProblemEq Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq toConstr :: ProblemEq -> Constr dataTypeOf :: ProblemEq -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq | |
Show ProblemEq Source # | |
Generic ProblemEq Source # | |
NFData ProblemEq Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange ProblemEq Source # | |
Defined in Agda.Syntax.Abstract Methods | |
Subst ProblemEq Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source # | |
PrettyTCM ProblemEq Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem | |
type Rep ProblemEq Source # | |
Defined in Agda.Syntax.Abstract type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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))))) | |
type SubstArg ProblemEq Source # | |
Defined in Agda.TypeChecking.Substitute |
data DataDefParams Source #
Constructors
DataDefParams | |
Fields
|
Instances
Eq DataDefParams Source # | |
Defined in Agda.Syntax.Abstract | |
Data DataDefParams Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDefParams toConstr :: DataDefParams -> Constr dataTypeOf :: DataDefParams -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDefParams) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDefParams) gmapT :: (forall b. Data b => b -> b) -> DataDefParams -> DataDefParams gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r gmapQ :: (forall d. Data d => d -> u) -> DataDefParams -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDefParams -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams | |
Show DataDefParams Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DataDefParams -> ShowS show :: DataDefParams -> String showList :: [DataDefParams] -> ShowS | |
Generic DataDefParams Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep DataDefParams :: Type -> Type | |
NFData DataDefParams Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: DataDefParams -> () | |
KillRange DataDefParams Source # | |
Defined in Agda.Syntax.Abstract Methods | |
ExprLike DataDefParams Source # | |
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 # | |
type Rep DataDefParams Source # | |
Defined in Agda.Syntax.Abstract type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
|
Instances
Eq GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract Methods (==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool (/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool | |
Data GeneralizeTelescope Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizeTelescope toConstr :: GeneralizeTelescope -> Constr dataTypeOf :: GeneralizeTelescope -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizeTelescope) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizeTelescope) gmapT :: (forall b. Data b => b -> b) -> GeneralizeTelescope -> GeneralizeTelescope gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r gmapQ :: (forall d. Data d => d -> u) -> GeneralizeTelescope -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizeTelescope -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope | |
Show GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> GeneralizeTelescope -> ShowS show :: GeneralizeTelescope -> String showList :: [GeneralizeTelescope] -> ShowS | |
Generic GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep GeneralizeTelescope :: Type -> Type Methods from :: GeneralizeTelescope -> Rep GeneralizeTelescope x to :: Rep GeneralizeTelescope x -> GeneralizeTelescope | |
NFData GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: GeneralizeTelescope -> () | |
KillRange GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract Methods | |
ExprLike GeneralizeTelescope Source # | |
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 # | |
type Rep GeneralizeTelescope Source # | |
Defined in Agda.Syntax.Abstract type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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:
- We would have to typecheck the type
A
several times. - If
A
contains a meta variable or hole, it would be duplicated by such a translation.
While 1. is only slightly inefficient, 2. would be an outright bug.
Duplicating A
could not be done naively, we would have to make sure
that the metas of the copy are aliases of the metas of the original.
Constructors
TBind Range TacticAttr (List1 (NamedArg Binder)) Expr | As in telescope |
TLet Range (List1 LetBinding) | E.g. |
Instances
Eq TypedBinding Source # | |
Defined in Agda.Syntax.Abstract | |
Data TypedBinding Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypedBinding toConstr :: TypedBinding -> Constr dataTypeOf :: TypedBinding -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypedBinding) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypedBinding) gmapT :: (forall b. Data b => b -> b) -> TypedBinding -> TypedBinding gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r gmapQ :: (forall d. Data d => d -> u) -> TypedBinding -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding | |
Show TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBinding -> ShowS show :: TypedBinding -> String showList :: [TypedBinding] -> ShowS | |
Generic TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep TypedBinding :: Type -> Type | |
NFData TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: TypedBinding -> () | |
KillRange TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source # | |
LensHiding TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |
ExprLike TypedBinding Source # | |
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 # | |
PrettyTCM TypedBinding Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source # | |
ToConcrete TypedBinding Source # | |
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 # | |
type Rep TypedBinding Source # | |
Defined in Agda.Syntax.Abstract type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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)))) | |
type ConOfAbs TypedBinding Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
data LamBinding Source #
A lambda binding is either domain free or typed.
Constructors
DomainFree TacticAttr (NamedArg Binder) | . |
DomainFull TypedBinding | . |
Instances
Eq LamBinding Source # | |
Defined in Agda.Syntax.Abstract | |
Data LamBinding Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamBinding toConstr :: LamBinding -> Constr dataTypeOf :: LamBinding -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamBinding) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamBinding) gmapT :: (forall b. Data b => b -> b) -> LamBinding -> LamBinding gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r gmapQ :: (forall d. Data d => d -> u) -> LamBinding -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding | |
Show LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LamBinding -> ShowS show :: LamBinding -> String showList :: [LamBinding] -> ShowS | |
Generic LamBinding Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep LamBinding :: Type -> Type | |
NFData LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: LamBinding -> () | |
KillRange LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source # | |
LensHiding LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
ExprLike LamBinding Source # | |
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 # | |
ToConcrete LamBinding Source # | |
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 # | |
type Rep LamBinding Source # | |
Defined in Agda.Syntax.Abstract type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 ConOfAbs LamBinding Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
Constructors
Binder | |
Fields
|
Instances
Functor Binder' Source # | |
Foldable Binder' Source # | |
Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Binder' m -> m foldMap :: Monoid m => (a -> m) -> Binder' a -> m foldMap' :: Monoid m => (a -> m) -> Binder' a -> m foldr :: (a -> b -> b) -> b -> Binder' a -> b foldr' :: (a -> b -> b) -> b -> Binder' a -> b foldl :: (b -> a -> b) -> b -> Binder' a -> b foldl' :: (b -> a -> b) -> b -> Binder' a -> b foldr1 :: (a -> a -> a) -> Binder' a -> a foldl1 :: (a -> a -> a) -> Binder' a -> a elem :: Eq a => a -> Binder' a -> Bool maximum :: Ord a => Binder' a -> a minimum :: Ord a => Binder' a -> a | |
Traversable Binder' Source # | |
Eq a => Eq (Binder' a) Source # | |
Data a => Data (Binder' a) Source # | |
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) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder' a) toConstr :: Binder' a -> Constr dataTypeOf :: Binder' a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder' a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder' a)) gmapT :: (forall b. Data b => b -> b) -> Binder' a -> Binder' a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r gmapQ :: (forall d. Data d => d -> u) -> Binder' a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder' a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) | |
Show a => Show (Binder' a) Source # | |
Generic (Binder' a) Source # | |
NFData a => NFData (Binder' a) Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange a => KillRange (Binder' a) Source # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source # | |
HasRange a => HasRange (Binder' a) Source # | |
ToConcrete a => ToConcrete (Binder' a) Source # | |
type Rep (Binder' a) Source # | |
Defined in Agda.Syntax.Abstract type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 ConOfAbs (Binder' a) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
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 |
|
LetOpen ModuleInfo ModuleName ImportDirective | only for highlighting and abstractToConcrete |
LetDeclaredVariable BindName | Only used for highlighting. Refers to the first occurrence of
|
Instances
Eq LetBinding Source # | |
Defined in Agda.Syntax.Abstract | |
Data LetBinding Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBinding toConstr :: LetBinding -> Constr dataTypeOf :: LetBinding -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetBinding) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetBinding) gmapT :: (forall b. Data b => b -> b) -> LetBinding -> LetBinding gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r gmapQ :: (forall d. Data d => d -> u) -> LetBinding -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBinding -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding | |
Show LetBinding Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LetBinding -> ShowS show :: LetBinding -> String showList :: [LetBinding] -> ShowS | |
Generic LetBinding Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep LetBinding :: Type -> Type | |
NFData LetBinding Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: LetBinding -> () | |
KillRange LetBinding Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange LetBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source # | |
ExprLike LetBinding Source # | |
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 # | |
ToConcrete LetBinding Source # | |
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 # | |
type Rep LetBinding Source # | |
Defined in Agda.Syntax.Abstract type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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))))) | |
type ConOfAbs LetBinding Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
Constructors
OptionsPragma [String] | |
BuiltinPragma RString ResolvedName |
|
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
|
InjectivePragma QName | |
InlinePragma Bool QName | |
DisplayPragma QName [NamedArg Pattern] Expr |
Instances
Eq Pragma Source # | |
Data Pragma Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma dataTypeOf :: Pragma -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma | |
Show Pragma Source # | |
Generic Pragma Source # | |
NFData Pragma Source # | |
Defined in Agda.Syntax.Abstract | |
DeclaredNames Pragma Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Pragma -> m Source # | |
ExprLike Pragma Source # | |
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Pragma Source # foldExpr :: FoldExprFn m Pragma Source # | |
type Rep Pragma Source # | |
Defined in Agda.Syntax.Abstract type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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] |
|
RecordModuleInstance ModuleName | M {{...}} |
Instances
Eq ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract Methods (==) :: ModuleApplication -> ModuleApplication -> Bool (/=) :: ModuleApplication -> ModuleApplication -> Bool | |
Data ModuleApplication Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication toConstr :: ModuleApplication -> Constr dataTypeOf :: ModuleApplication -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication) gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication | |
Show ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ModuleApplication -> ShowS show :: ModuleApplication -> String showList :: [ModuleApplication] -> ShowS | |
Generic ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep ModuleApplication :: Type -> Type Methods from :: ModuleApplication -> Rep ModuleApplication x to :: Rep ModuleApplication x -> ModuleApplication | |
NFData ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: ModuleApplication -> () | |
KillRange ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract Methods | |
ExprLike ModuleApplication Source # | |
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 # | |
ToConcrete ModuleApplication Source # | |
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 # | |
type Rep ModuleApplication Source # | |
Defined in Agda.Syntax.Abstract type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 ConOfAbs ModuleApplication Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
type ImportedName = ImportedName' QName ModuleName 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 |
Import ModuleInfo ModuleName ImportDirective | The |
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 |
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
Eq Declaration Source # | Does not compare |
Defined in Agda.Syntax.Abstract | |
Data Declaration Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration toConstr :: Declaration -> Constr dataTypeOf :: Declaration -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration | |
Show Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Declaration -> ShowS show :: Declaration -> String showList :: [Declaration] -> ShowS | |
Generic Declaration Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep Declaration :: Type -> Type | |
NFData Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: Declaration -> () | |
KillRange Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source # | |
AnyAbstract Declaration Source # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source # | |
DeclaredNames Declaration Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Declaration -> m Source # | |
ExprLike Declaration Source # | |
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 # | |
ToConcrete Declaration Source # | |
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 # | |
Defined in Agda.TypeChecking.Rules.Decl Methods showHead :: Declaration -> String Source # | |
ToConcrete (Constr Constructor) Source # | |
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 Rep Declaration Source # | |
Defined in Agda.Syntax.Abstract type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Declaration Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type ConOfAbs (Constr Constructor) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
data ScopeCopyInfo Source #
Constructors
ScopeCopyInfo | |
Fields
|
Instances
Eq ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract | |
Data ScopeCopyInfo Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeCopyInfo toConstr :: ScopeCopyInfo -> Constr dataTypeOf :: ScopeCopyInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ScopeCopyInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ScopeCopyInfo) gmapT :: (forall b. Data b => b -> b) -> ScopeCopyInfo -> ScopeCopyInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ScopeCopyInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeCopyInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo | |
Show ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS show :: ScopeCopyInfo -> String showList :: [ScopeCopyInfo] -> ShowS | |
Generic ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract Associated Types type Rep ScopeCopyInfo :: Type -> Type | |
NFData ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract Methods rnf :: ScopeCopyInfo -> () | |
Pretty ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source # | |
KillRange ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract Methods | |
type Rep ScopeCopyInfo Source # | |
Defined in Agda.Syntax.Abstract type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 RecordAssigns = [RecordAssign] Source #
type RecordAssign = Either Assign ModuleName Source #
type Assign = FieldAssignment' Expr Source #
Record field assignment f = e
.
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 |
Underscore MetaInfo | Meta variable for hidden argument (must be inferred locally). |
Dot ExprInfo Expr |
|
App AppInfo Expr (NamedArg Expr) | Ordinary (binary) application. |
WithApp ExprInfo Expr [Expr] | With application. |
Lam ExprInfo LamBinding Expr |
|
AbsurdLam ExprInfo Hiding |
|
ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) | |
Pi ExprInfo Telescope1 Expr | Dependent function space |
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 |
|
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 |
QuoteTerm ExprInfo | Quote a term. |
Unquote ExprInfo | The splicing construct: unquote ... |
DontCare Expr | For printing |
Instances
Eq Expr Source # | Does not compare |
Data Expr Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr dataTypeOf :: Expr -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr | |
Show Expr Source # | |
Generic Expr Source # | |
NFData Expr Source # | |
Defined in Agda.Syntax.Abstract | |
KillRange Expr Source # | |
Defined in Agda.Syntax.Abstract Methods | |
HasRange Expr Source # | |
Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract | |
IsProjP Expr Source # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
SubstExpr Expr Source # | |
ExprLike Expr Source # | |
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Expr Source # foldExpr :: FoldExprFn m Expr Source # | |
MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
PrettyTCM Expr Source # | |
Defined in Agda.TypeChecking.Pretty | |
ToConcrete Pattern Source # | |
ToConcrete LHSCore Source # | |
ToConcrete Expr Source # | |
Reify Expr Source # | |
IsFlexiblePattern Pattern Source # | |
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 # | |
PrettyTCM (NamedArg Expr) Source # | |
Defined in Agda.TypeChecking.Pretty | |
PrettyTCM (Arg Expr) Source # | |
Defined in Agda.TypeChecking.Pretty | |
ToConcrete (Maybe Pattern) Source # | |
ToAbstract (Expr, Elims) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source # | |
ToAbstract (Expr, Elim) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source # | |
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |
type Rep Expr Source # | |
Defined in Agda.Syntax.Abstract type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Pattern Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type ConOfAbs LHSCore Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type ConOfAbs Expr Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type ReifiesTo Expr Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
type ConOfAbs (Maybe Pattern) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type AbsOfRef (Expr, Elims) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
type AbsOfRef (Expr, Elim) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
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} -> ..
.
Instances
mkBindName :: Name -> BindName Source #
extractPattern :: Binder' a -> Maybe (Pattern, a) Source #
mkDomainFree :: NamedArg Binder -> LamBinding Source #
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding Source #
axiomName :: Declaration -> QName Source #
The name defined by the given axiom.
Precondition: The declaration has to be a (scoped) Axiom
.
patternToExpr :: Pattern -> Expr Source #
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) Source #
module Agda.Syntax.Abstract.Name