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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract

Description

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

Synopsis

- type HoleContent = HoleContent' Expr
- type Patterns = [NamedArg Pattern]
- type Pattern = Pattern' Expr
- 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 Literal
  - | PatternSynP PatInfo AmbiguousQName (NAPs e)
  - | RecP PatInfo [FieldAssignment' (Pattern' e)]
  - | EqualP PatInfo [(e, e)]
  - | WithP PatInfo (Pattern' e)
- type LHSCore = LHSCore' Expr
- data LHSCore' e
  - = LHSHead {
    - lhsDefName :: QName
    - lhsPats :: [NamedArg (Pattern' e)]
    }
  - | LHSProj {
    - lhsDestructor :: AmbiguousQName
    - lhsFocus :: NamedArg (LHSCore' e)
    - lhsPats :: [NamedArg (Pattern' e)]
    }
  - | LHSWith {
    - lhsHead :: LHSCore' e
    - lhsWithPatterns :: [Pattern' e]
    - lhsPats :: [NamedArg (Pattern' e)]
    }
- data LHS = LHS {
  - lhsInfo :: LHSInfo
  - lhsCore :: LHSCore
  }
- data SpineLHS = SpineLHS {
  - spLhsInfo :: LHSInfo
  - spLhsDefName :: QName
  - spLhsPats :: [NamedArg Pattern]
  }
- data RHS
  - = RHS {
    - rhsExpr :: Expr
    - rhsConcrete :: Maybe Expr
    }
  - | AbsurdRHS
  - | WithRHS QName [Expr] [Clause]
  - | RewriteRHS {
    - rewriteExprs :: [(QName, Expr)]
    - rewriteStrippedPats :: [ProblemEq]
    - rewriteRHS :: RHS
    - rewriteWhereDecls :: WhereDeclarations
    }
- type SpineClause = Clause' SpineLHS
- type Clause = Clause' LHS
- data WhereDeclarations = WhereDecls {
  - whereModule :: Maybe ModuleName
  - whereDecls :: [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]
- data TypedBinding
  - = TBind Range [NamedArg BindName] Expr
  - | TLet Range [LetBinding]
- data LamBinding
  - = DomainFree (NamedArg BindName)
  - | DomainFull TypedBinding
- type Field = TypeSignature
- type Constructor = TypeSignature
- type TypeSignature = Declaration
- data LetBinding
  - = LetBind LetInfo ArgInfo BindName Expr Expr
  - | LetPatBind LetInfo Pattern Expr
  - | LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
  - | LetOpen ModuleInfo ModuleName ImportDirective
  - | LetDeclaredVariable BindName
- data Pragma
  - = OptionsPragma [String]
  - | BuiltinPragma String ResolvedName
  - | BuiltinNoDefPragma String QName
  - | RewritePragma QName
  - | CompilePragma String QName String
  - | StaticPragma QName
  - | EtaPragma QName
  - | InjectivePragma QName
  - | InlinePragma Bool QName
  - | DisplayPragma QName [NamedArg Pattern] Expr
- data ModuleApplication
  - = SectionApp Telescope ModuleName [NamedArg Expr]
  - | RecordModuleInstance ModuleName
- type ImportedName = ImportedName' QName ModuleName
- type Renaming = Renaming' QName ModuleName
- type ImportDirective = ImportDirective' QName ModuleName
- class GetDefInfo a where
  - getDefInfo :: a -> Maybe DefInfo
- data Declaration
  - = Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr
  - | Generalize (Set QName) DefInfo ArgInfo QName Expr
  - | Field DefInfo QName (Arg Expr)
  - | Primitive DefInfo QName Expr
  - | Mutual MutualInfo [Declaration]
  - | Section ModuleInfo 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 (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) DataDefParams Expr [Declaration]
  - | PatternSynDef QName [Arg Name] (Pattern' Void)
  - | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
  - | UnquoteDef [DefInfo] [QName] Expr
  - | ScopedDecl ScopeInfo [Declaration]
- data ScopeCopyInfo = ScopeCopyInfo {
  - renModules :: Ren ModuleName
  - renNames :: Ren QName
  }
- type Ren a = [(a, a)]
- data Axiom
  - = FunSig
  - | NoFunSig
- type RecordAssigns = [RecordAssign]
- type RecordAssign = Either Assign ModuleName
- type Assigns = [Assign]
- type Assign = FieldAssignment' Expr
- data Expr
  - = Var Name
  - | Def QName
  - | Proj ProjOrigin AmbiguousQName
  - | Con AmbiguousQName
  - | PatternSyn AmbiguousQName
  - | Macro QName
  - | Lit 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 QName [Clause]
  - | Pi ExprInfo Telescope Expr
  - | Generalized (Set QName) Expr
  - | Fun ExprInfo (Arg Expr) Expr
  - | Set ExprInfo Integer
  - | Prop ExprInfo Integer
  - | Let ExprInfo [LetBinding] Expr
  - | ETel Telescope
  - | Rec ExprInfo RecordAssigns
  - | RecUpdate ExprInfo Expr Assigns
  - | ScopedExpr ScopeInfo Expr
  - | QuoteGoal ExprInfo Name Expr
  - | QuoteContext ExprInfo
  - | Quote ExprInfo
  - | QuoteTerm ExprInfo
  - | Unquote ExprInfo
  - | Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]
  - | DontCare Expr
- type Args = [NamedArg Expr]
- newtype BindName = BindName {
  - unBind :: Name
  }
- generalized :: Set QName -> Expr -> Expr
- initCopyInfo :: ScopeCopyInfo
- noDataDefParams :: DataDefParams
- noWhereDecls :: WhereDeclarations
- class SubstExpr a where
  - substExpr :: [(Name, Expr)] -> a -> a
- type PatternSynDefns = Map QName PatternSynDefn
- type PatternSynDefn = ([Arg Name], Pattern' Void)
- class NameToExpr a where
  - nameExpr :: a -> Expr
- class AnyAbstract a where
  - anyAbstract :: a -> Bool
- class AllNames a where
  - allNames :: a -> Seq QName
- 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])
- class IsNoName a where
  - isNoName :: a -> Bool
- class MkName a where
  - mkName :: Range -> NameId -> a -> Name
  - mkName_ :: NameId -> a -> Name
- class IsProjP a where
  - isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
- newtype AmbiguousQName = AmbQ {
  - unAmbQ :: NonemptyList QName
  }
- newtype ModuleName = MName {
  - mnameToList :: [Name]
  }
- data QNamed a = QNamed {
  - qname :: QName
  - qnamed :: a
  }
- data QName = QName {
  - qnameModule :: ModuleName
  - qnameName :: Name
  }
- data Name = Name {
  - nameId :: !NameId
  - nameConcrete :: Name
  - nameBindingSite :: Range
  - nameFixity :: Fixity'
  - nameIsRecordName :: Bool
  }
- uglyShowName :: Name -> String
- unambiguous :: QName -> AmbiguousQName
- headAmbQ :: AmbiguousQName -> QName
- isAmbiguous :: AmbiguousQName -> Bool
- getUnambiguous :: AmbiguousQName -> Maybe QName
- isAnonymousModuleName :: ModuleName -> Bool
- withRangesOf :: ModuleName -> [Name] -> ModuleName
- withRangesOfQ :: ModuleName -> QName -> ModuleName
- mnameFromList :: [Name] -> ModuleName
- noModuleName :: ModuleName
- commonParentModule :: ModuleName -> ModuleName -> ModuleName
- qnameToList :: QName -> [Name]
- qnameFromList :: [Name] -> QName
- qnameToMName :: QName -> ModuleName
- mnameToQName :: ModuleName -> QName
- showQNameId :: QName -> String
- qnameToConcrete :: QName -> QName
- mnameToConcrete :: ModuleName -> QName
- toTopLevelModuleName :: ModuleName -> TopLevelModuleName
- qualifyM :: ModuleName -> ModuleName -> ModuleName
- qualifyQ :: ModuleName -> QName -> QName
- qualify :: ModuleName -> Name -> QName
- qualify_ :: Name -> QName
- isOperator :: QName -> Bool
- isSubModuleOf :: ModuleName -> ModuleName -> Bool
- isInModule :: QName -> ModuleName -> Bool
- nextName :: Name -> Name
- sameRoot :: Name -> Name -> Bool

# Documentation

type HoleContent = HoleContent' Expr Source #

type Patterns = [NamedArg Pattern] Source #

type Pattern = Pattern' Expr Source #

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

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

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

Instances

Functor Pattern' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b Source # (<$) :: a -> Pattern' b -> Pattern' a Source #
Foldable Pattern' Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool Source #

length :: Pattern' a -> Int Source #

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

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

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

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

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

Traversable Pattern' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) Source # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) Source # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) Source # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) Source #
MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
IsFlexiblePattern Pattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern -> TCM Bool Source #
UniverseBi Declaration Pattern Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Pattern] Source #
ToConcrete Pattern Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Pattern -> AbsToCon Pattern0 Source # bindToConcrete :: Pattern -> (Pattern0 -> AbsToCon b) -> AbsToCon b Source #
UniverseBi Declaration (NamedArg Pattern) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source #
UniverseBi Declaration (Pattern' Void) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Pattern' Void] Source #
APatternLike a (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m Source # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #
ToAbstract Pattern (Pattern' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) Source #
ToAbstract Pattern (Names, Pattern) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Pattern0 -> WithNames (Names, Pattern) Source #
Eq e => Eq (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pattern' e -> Pattern' e -> Bool Source # (/=) :: Pattern' e -> Pattern' e -> Bool Source #
Data e => Data (Pattern' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Pattern' e -> Constr Source #

dataTypeOf :: Pattern' e -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show e => Show (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pattern' e -> ShowS Source # show :: Pattern' e -> String Source # showList :: [Pattern' e] -> ShowS Source #
KillRange e => KillRange (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source #
SetRange (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> Pattern' a -> Pattern' a Source #
HasRange (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Pattern' e -> Range Source #
IsProjP (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsWithP (Pattern' e) Source # | Check for with-pattern.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #
ExprLike a => ExprLike (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source # foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Int32 Source # icod_ :: Pattern' a -> S Int32 Source # value :: Int32 -> R (Pattern' a) Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Pattern' a -> Set QName Source #
ExpandPatternSynonyms (Pattern' e) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #
ToAbstract (Pattern' Expr) (Pattern' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern' Expr0 -> ScopeM (Pattern' Expr) Source #

type LHSCore = LHSCore' Expr Source #

data LHSCore' e Source #

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

Constructors

LHSHead | The head applied to ordinary patterns.

Fields

- lhsDefName :: QName

  Head `f`.

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

  Applied to patterns `ps`.

LHSProj | Projection.

Fields

- lhsDestructor :: AmbiguousQName

  Record projection identifier.

- lhsFocus :: NamedArg (LHSCore' e)

  Main argument of projection.

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

  Applied to patterns `ps`.

LHSWith | With patterns.

Fields

- lhsHead :: LHSCore' e

  E.g. the `LHSHead`.

- lhsWithPatterns :: [Pattern' e]

  Applied to with patterns `| p1 | ... | pn`. These patterns are not prefixed with `WithP`!

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

  Applied to patterns `ps`.

Instances

Functor LHSCore' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> LHSCore' a -> LHSCore' b Source # (<$) :: a -> LHSCore' b -> LHSCore' a Source #
Foldable LHSCore' Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

null :: LHSCore' a -> Bool Source #

length :: LHSCore' a -> Int Source #

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

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

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

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

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

Traversable LHSCore' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) Source # sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) Source # mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) Source # sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a) Source #
ToConcrete LHSCore Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHSCore -> AbsToCon Pattern Source # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
UniverseBi Declaration (NamedArg LHSCore) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source #
ToAbstract LHSCore (LHSCore' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) Source #
Eq e => Eq (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHSCore' e -> LHSCore' e -> Bool Source # (/=) :: LHSCore' e -> LHSCore' e -> Bool Source #
Data e => Data (LHSCore' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: LHSCore' e -> Constr Source #

dataTypeOf :: LHSCore' e -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show e => Show (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHSCore' e -> ShowS Source # show :: LHSCore' e -> String Source # showList :: [LHSCore' e] -> ShowS Source #
KillRange e => KillRange (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source #
HasRange (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHSCore' e -> Range Source #
ExprLike a => ExprLike (LHSCore' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source # foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore' Expr0 -> ScopeM (LHSCore' Expr) Source #

data LHS Source #

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

Constructors

LHS |

Fields

- lhsInfo :: LHSInfo

  Range.

- lhsCore :: LHSCore

  Copatterns.

Instances

Eq LHS Source # | Ignore `Range'` when comparing `LHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHS -> LHS -> Bool Source # (/=) :: LHS -> LHS -> Bool Source #
Data LHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: LHS -> Constr Source #

dataTypeOf :: LHS -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHS -> ShowS Source # show :: LHS -> String Source # showList :: [LHS] -> ShowS Source #
KillRange LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LHS Source #
HasRange LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHS -> Range Source #
AllNames Clause Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Clause -> Seq QName Source #
ExprLike LHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS Source # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHS -> m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
LHSToSpine LHS SpineLHS Source # | LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
LHSToSpine Clause SpineClause Source # | Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ToConcrete LHS LHS Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHS -> AbsToCon LHS0 Source # bindToConcrete :: LHS -> (LHS0 -> AbsToCon b) -> AbsToCon b Source #
Reify NamedClause Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: NamedClause -> TCM Clause Source # reifyWhen :: Bool -> NamedClause -> TCM Clause Source #
ToAbstract Clause Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Clause -> ScopeM Clause0 Source #
ToAbstract LeftHandSide LHS Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LeftHandSide -> ScopeM LHS Source #
ToAbstract (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: QNamed Clause0 -> WithNames Clause Source #
Reify (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause Source #
ToAbstract [QNamed Clause] [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [QNamed Clause0] -> WithNames [Clause] Source #
Reify (QNamed System) [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed System -> TCM [Clause] Source # reifyWhen :: Bool -> QNamed System -> TCM [Clause] Source #

data SpineLHS Source #

The lhs of a clause in spine view (inside-out). Projection patterns are contained in `spLhsPats`, represented as `ProjP d`.

Constructors

SpineLHS |

Fields

- spLhsInfo :: LHSInfo

  Range.

- spLhsDefName :: QName

  Name of function we are defining.

- spLhsPats :: [NamedArg Pattern]

  Elimination by pattern, projections, with-patterns.

Instances

Eq SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: SpineLHS -> SpineLHS -> Bool Source # (/=) :: SpineLHS -> SpineLHS -> Bool Source #
Data SpineLHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: SpineLHS -> Constr Source #

dataTypeOf :: SpineLHS -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> SpineLHS -> ShowS Source # show :: SpineLHS -> String Source # showList :: [SpineLHS] -> ShowS Source #
KillRange SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT SpineLHS Source #
HasRange SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: SpineLHS -> Range Source #
ExprLike SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS Source # foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> SpineLHS -> m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
LHSToSpine LHS SpineLHS Source # | LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
LHSToSpine Clause SpineClause Source # | Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ToConcrete SpineLHS LHS Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: SpineLHS -> AbsToCon LHS Source # bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b Source #

data RHS Source #

Constructors

RHS |

Fields

- rhsExpr :: Expr
- rhsConcrete :: Maybe Expr

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

AbsurdRHS |
WithRHS QName [Expr] [Clause] | The `QName` is the name of the with function.
RewriteRHS |

Fields

- rewriteExprs :: [(QName, Expr)]

  The `QName`s are the names of the generated with functions, one for each `Expr`.

- rewriteStrippedPats :: [ProblemEq]

  The patterns stripped by with-desugaring. These are only present if this rewrite follows a with.

- rewriteRHS :: RHS

  The RHS should not be another `RewriteRHS`.

- rewriteWhereDecls :: WhereDeclarations

  The where clauses are attached to the `RewriteRHS` by

Instances

Eq RHS Source # | Ignore `rhsConcrete` when comparing `RHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: RHS -> RHS -> Bool Source # (/=) :: RHS -> RHS -> Bool Source #
Data RHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: RHS -> Constr Source #

dataTypeOf :: RHS -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHS -> ShowS Source # show :: RHS -> String Source # showList :: [RHS] -> ShowS Source #
KillRange RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS Source #
HasRange RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: RHS -> Range Source #
AllNames RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: RHS -> Seq QName Source #
ExprLike RHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS Source # foldExpr :: Monoid m => (Expr -> m) -> RHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RHS -> m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
ToAbstract AbstractRHS RHS Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: AbstractRHS -> ScopeM RHS Source #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source #

type SpineClause = Clause' SpineLHS Source #

type Clause = Clause' LHS Source #

data WhereDeclarations Source #

Constructors

WhereDecls |

Fields

- whereModule :: Maybe ModuleName
- whereDecls :: [Declaration]

Instances

Eq WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: WhereDeclarations -> WhereDeclarations -> Bool Source # (/=) :: WhereDeclarations -> WhereDeclarations -> Bool Source #
Data WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: WhereDeclarations -> Constr Source #

dataTypeOf :: WhereDeclarations -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarations -> ShowS Source # show :: WhereDeclarations -> String Source # showList :: [WhereDeclarations] -> ShowS Source #
KillRange WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT WhereDeclarations Source #
HasRange WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range Source #
AllNames WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: WhereDeclarations -> Seq QName Source #
ExprLike WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> WhereDeclarations -> m WhereDeclarations Source #

foldExpr :: Monoid m => (Expr -> m) -> WhereDeclarations -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> WhereDeclarations -> m WhereDeclarations Source #

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

ToConcrete WhereDeclarations WhereClause Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause Source # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b Source #

data Clause' lhs Source #

We could throw away `where` clauses at this point and translate them to `let`. It's not obvious how to remember that the `let` was really a `where` clause though, so for the time being we keep it here.

Constructors

Clause |

Fields

- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]

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

- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool

Instances

Functor Clause' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Clause' a -> Clause' b Source # (<$) :: a -> Clause' b -> Clause' a Source #
Foldable Clause' Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

null :: Clause' a -> Bool Source #

length :: Clause' a -> Int Source #

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

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

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

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

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

Traversable Clause' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) Source # sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) Source # mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) Source # sequence :: Monad m => Clause' (m a) -> m (Clause' a) Source #
AllNames Clause Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Clause -> Seq QName Source #
LHSToSpine Clause SpineClause Source # | Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
Reify NamedClause Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: NamedClause -> TCM Clause Source # reifyWhen :: Bool -> NamedClause -> TCM Clause Source #
ToAbstract Clause Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Clause -> ScopeM Clause0 Source #
Eq lhs => Eq (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Clause' lhs -> Clause' lhs -> Bool Source # (/=) :: Clause' lhs -> Clause' lhs -> Bool Source #
Data lhs => Data (Clause' lhs) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Clause' lhs -> Constr Source #

dataTypeOf :: Clause' lhs -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show lhs => Show (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Clause' lhs -> ShowS Source # show :: Clause' lhs -> String Source # showList :: [Clause' lhs] -> ShowS Source #
KillRange a => KillRange (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source #
HasRange a => HasRange (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Clause' a -> Range Source #
ExprLike a => ExprLike (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a) Source # foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Clause' a -> m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source #
ToAbstract (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: QNamed Clause0 -> WithNames Clause Source #
Reify (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause Source #
ToAbstract [QNamed Clause] [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [QNamed Clause0] -> WithNames [Clause] Source #
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Clause' a -> AbsToCon [Declaration] Source # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
Reify (QNamed System) [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed System -> TCM [Clause] Source # reifyWhen :: Bool -> QNamed System -> TCM [Clause] Source #

data ProblemEq Source #

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

Constructors

ProblemEq |

Fields

- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type

Instances

Eq ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ProblemEq -> ProblemEq -> Bool Source # (/=) :: ProblemEq -> ProblemEq -> Bool Source #
Data ProblemEq Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: ProblemEq -> Constr Source #

dataTypeOf :: ProblemEq -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ProblemEq -> ShowS Source # show :: ProblemEq -> String Source # showList :: [ProblemEq] -> ShowS Source #
KillRange ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq Source #
PrettyTCM ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: ProblemEq -> TCM Doc Source #
Subst Term ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq Source #

data DataDefParams Source #

Constructors

DataDefParams |

Fields

- dataDefGeneralizedParams :: Set Name

  We don't yet know the position of generalized parameters from the data sig, so we keep these in a set on the side.

- dataDefParams :: [LamBinding]

Instances

Eq DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: DataDefParams -> DataDefParams -> Bool Source # (/=) :: DataDefParams -> DataDefParams -> Bool Source #
Data DataDefParams Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: DataDefParams -> Constr Source #

dataTypeOf :: DataDefParams -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DataDefParams -> ShowS Source # show :: DataDefParams -> String Source # showList :: [DataDefParams] -> ShowS Source #
KillRange DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT DataDefParams Source #
ExprLike DataDefParams Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> DataDefParams -> m DataDefParams Source #

foldExpr :: Monoid m => (Expr -> m) -> DataDefParams -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> DataDefParams -> m DataDefParams Source #

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

data GeneralizeTelescope Source #

Constructors

GeneralizeTel |

Fields

- generalizeTelVars :: Map QName Name

  Maps generalize variables to the corresponding bound variable (to be introduced by the generalisation).

- generalizeTel :: Telescope

Instances

Eq GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool Source # (/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool Source #
Data GeneralizeTelescope Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: GeneralizeTelescope -> Constr Source #

dataTypeOf :: GeneralizeTelescope -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> GeneralizeTelescope -> ShowS Source # show :: GeneralizeTelescope -> String Source # showList :: [GeneralizeTelescope] -> ShowS Source #
KillRange GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT GeneralizeTelescope Source #
ExprLike GeneralizeTelescope Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> GeneralizeTelescope -> m GeneralizeTelescope Source #

foldExpr :: Monoid m => (Expr -> m) -> GeneralizeTelescope -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> GeneralizeTelescope -> m GeneralizeTelescope Source #

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

type Telescope = [TypedBinding] Source #

data TypedBinding Source #

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

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

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

Constructors

TBind Range [NamedArg BindName] Expr | As in telescope `(x y z : A)` or type `(x y z : A) -> B`.
TLet Range [LetBinding] | E.g. `(let x = e)` or `(let open M)`.

Instances

Eq TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: TypedBinding -> TypedBinding -> Bool Source # (/=) :: TypedBinding -> TypedBinding -> Bool Source #
Data TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: TypedBinding -> Constr Source #

dataTypeOf :: TypedBinding -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBinding -> ShowS Source # show :: TypedBinding -> String Source # showList :: [TypedBinding] -> ShowS Source #
KillRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBinding Source #
HasRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source #
LensHiding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
SubstExpr TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> TypedBinding -> TypedBinding Source #
AllNames TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: TypedBinding -> Seq QName Source #
ExprLike TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> TypedBinding -> m TypedBinding Source #

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

PrettyTCM TypedBinding Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: TypedBinding -> TCM Doc Source #
UniverseBi Declaration TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [TypedBinding] Source #
ToConcrete TypedBinding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding0 Source # bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b Source #
Reify Telescope Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope Source # reifyWhen :: Bool -> Telescope0 -> TCM Telescope Source #
ToAbstract TypedBinding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBinding0 -> ScopeM TypedBinding Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Dom r, Name) -> WithNames TypedBinding Source #

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree (NamedArg BindName) | . `x` or `{x}` or `.x` or `{x = y}`
DomainFull TypedBinding | . `(xs:e)` or `{xs:e}` or `(let Ds)`

Instances

Eq LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LamBinding -> LamBinding -> Bool Source # (/=) :: LamBinding -> LamBinding -> Bool Source #
Data LamBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: LamBinding -> Constr Source #

dataTypeOf :: LamBinding -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
KillRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LamBinding Source #
HasRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source #
LensHiding LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
AllNames LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: LamBinding -> Seq QName Source #
ExprLike LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LamBinding -> m LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
UniverseBi Declaration LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [LamBinding] Source #
ToConcrete LamBinding LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon LamBinding0 Source # bindToConcrete :: LamBinding -> (LamBinding0 -> AbsToCon b) -> AbsToCon b Source #
ToAbstract LamBinding LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding Source #

type Field = TypeSignature Source #

type Constructor = TypeSignature Source #

type TypeSignature = Declaration Source #

Only `Axiom`s.

data LetBinding Source #

Bindings that are valid in a `let`.

Constructors

LetBind LetInfo ArgInfo BindName Expr Expr

    LetBind info rel name type defn

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

Instances

Eq LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LetBinding -> LetBinding -> Bool Source # (/=) :: LetBinding -> LetBinding -> Bool Source #
Data LetBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: LetBinding -> Constr Source #

dataTypeOf :: LetBinding -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LetBinding -> ShowS Source # show :: LetBinding -> String Source # showList :: [LetBinding] -> ShowS Source #
KillRange LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LetBinding Source #
HasRange LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source #
SubstExpr LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> LetBinding -> LetBinding Source #
AllNames LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: LetBinding -> Seq QName Source #
ExprLike LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LetBinding -> m LetBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LetBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LetBinding -> m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
UniverseBi Declaration LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [LetBinding] Source #
ToConcrete LetBinding [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LetBinding -> AbsToCon [Declaration] Source # bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) Source #

data Pragma Source #

Constructors

OptionsPragma [String] |
BuiltinPragma String ResolvedName | `ResolvedName` is not `UnknownName`. Name can be ambiguous e.g. for built-in constructors.
BuiltinNoDefPragma String QName | Builtins that do not come with a definition, but declare a name for an Agda concept.
RewritePragma QName |
CompilePragma String QName String |
StaticPragma QName |
EtaPragma QName | For coinductive records, use pragma instead of regular `eta-equality` definition (as it is might make Agda loop).
InjectivePragma QName |
InlinePragma Bool QName |
DisplayPragma QName [NamedArg Pattern] Expr |

Instances

Eq Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pragma -> Pragma -> Bool Source # (/=) :: Pragma -> Pragma -> Bool Source #
Data Pragma Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Pragma -> Constr Source #

dataTypeOf :: Pragma -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
ExprLike Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma Source # foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pragma -> m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
ToAbstract Pragma [Pragma] Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pragma0 -> ScopeM [Pragma] Source #

data ModuleApplication Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr] | `tel. M args`: applies `M` to `args` and abstracts `tel`.

RecordModuleInstance ModuleName

    M {{...}}

Instances

Eq ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ModuleApplication -> ModuleApplication -> Bool Source # (/=) :: ModuleApplication -> ModuleApplication -> Bool Source #
Data ModuleApplication Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: ModuleApplication -> Constr Source #

dataTypeOf :: ModuleApplication -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ModuleApplication -> ShowS Source # show :: ModuleApplication -> String Source # showList :: [ModuleApplication] -> ShowS Source #
KillRange ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ModuleApplication Source #
AllNames ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: ModuleApplication -> Seq QName Source #
ExprLike ModuleApplication Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication Source #

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

ToConcrete ModuleApplication ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleApplication -> AbsToCon ModuleApplication0 Source # bindToConcrete :: ModuleApplication -> (ModuleApplication0 -> AbsToCon b) -> AbsToCon b Source #

type ImportedName = ImportedName' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type ImportDirective = ImportDirective' QName ModuleName Source #

class GetDefInfo a where Source #

Methods

getDefInfo :: a -> Maybe DefInfo Source #

Instances

GetDefInfo Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getDefInfo :: Declaration -> Maybe DefInfo Source #

data Declaration Source #

Constructors

Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr | Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments.
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 Expr | primitive function
Mutual MutualInfo [Declaration] | a bunch of mutually recursive definitions
Section ModuleInfo ModuleName GeneralizeTelescope [Declaration] |
Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective | The `ImportDirective` is for highlighting purposes.
Import ModuleInfo ModuleName ImportDirective | The `ImportDirective` is for highlighting purposes.
Pragma Range Pragma |
Open ModuleInfo ModuleName ImportDirective | only retained for highlighting purposes
FunDef DefInfo QName Delayed [Clause] | sequence of function clauses
DataSig DefInfo QName GeneralizeTelescope Expr | lone data signature
DataDef DefInfo QName UniverseCheck DataDefParams [Constructor] | the `LamBinding`s are `DomainFree` and bind the parameters of the datatype.
RecSig DefInfo QName GeneralizeTelescope Expr | lone record signature
RecDef DefInfo QName UniverseCheck (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) DataDefParams Expr [Declaration] | The `LamBinding`s are `DomainFree` and bind the parameters of the datatype. The `Expr` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Prop`, and the optional name is the constructor's name.
PatternSynDef QName [Arg Name] (Pattern' Void) | Only for highlighting purposes
UnquoteDecl MutualInfo [DefInfo] [QName] Expr |
UnquoteDef [DefInfo] [QName] Expr |
ScopedDecl ScopeInfo [Declaration] | scope annotation

Instances

Eq Declaration Source # | Does not compare `ScopeInfo` fields.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Declaration -> Declaration -> Bool Source # (/=) :: Declaration -> Declaration -> Bool Source #
Data Declaration Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Declaration -> Constr Source #

dataTypeOf :: Declaration -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Declaration -> ShowS Source # show :: Declaration -> String Source # showList :: [Declaration] -> ShowS Source #
KillRange Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Declaration Source #
HasRange Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source #
GetDefInfo Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getDefInfo :: Declaration -> Maybe DefInfo Source #
AnyAbstract Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
AllNames Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Declaration -> Seq QName Source #
ExprLike Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Declaration -> m Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Declaration -> m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
ShowHead Declaration Source # |
Instance details Defined in Agda.TypeChecking.Rules.Decl Methods showHead :: Declaration -> String Source #
UniverseBi Declaration AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [AmbiguousQName] Source #
UniverseBi Declaration ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleName] Source #
UniverseBi Declaration QName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [QName] Source #
UniverseBi Declaration ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleInfo] Source #
UniverseBi Declaration Pattern Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Pattern] Source #
UniverseBi Declaration TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [TypedBinding] Source #
UniverseBi Declaration LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [LamBinding] Source #
UniverseBi Declaration LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [LetBinding] Source #
UniverseBi Declaration Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Declaration] Source #
UniverseBi Declaration Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Expr] Source #
ToAbstract NiceDeclaration Declaration Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NiceDeclaration -> ScopeM Declaration Source #
UniverseBi Declaration (NamedArg Pattern) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source #
UniverseBi Declaration (NamedArg LHSCore) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source #
UniverseBi Declaration (NamedArg Expr) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] Source #
UniverseBi Declaration (NamedArg BindName) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] Source #
UniverseBi Declaration (Pattern' Void) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Pattern' Void] Source #
ToConcrete Declaration [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Declaration -> AbsToCon [Declaration0] Source # bindToConcrete :: Declaration -> ([Declaration0] -> AbsToCon b) -> AbsToCon b Source #
ToConcrete (Constr Constructor) Declaration Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Constr Constructor -> AbsToCon Declaration Source # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b Source #
ToAbstract [Declaration] [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [Declaration0] -> ScopeM [Declaration] Source #

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo |

Fields

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

Instances

Eq ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool Source # (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool Source #
Data ScopeCopyInfo Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: ScopeCopyInfo -> Constr Source #

dataTypeOf :: ScopeCopyInfo -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS Source # show :: ScopeCopyInfo -> String Source # showList :: [ScopeCopyInfo] -> ShowS Source #
Pretty ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
KillRange ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo Source #

type Ren a = [(a, a)] Source #

Renaming (generic).

data Axiom Source #

Is a type signature a `postulate` or a function signature?

Constructors

FunSig | A function signature.
NoFunSig | Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally).

Instances

Eq Axiom Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Axiom -> Axiom -> Bool Source # (/=) :: Axiom -> Axiom -> Bool Source #
Data Axiom Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Axiom -> Constr Source #

dataTypeOf :: Axiom -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord Axiom Source # |
Instance details Defined in Agda.Syntax.Abstract Methods compare :: Axiom -> Axiom -> Ordering Source # (<) :: Axiom -> Axiom -> Bool Source # (<=) :: Axiom -> Axiom -> Bool Source # (>) :: Axiom -> Axiom -> Bool Source # (>=) :: Axiom -> Axiom -> Bool Source # max :: Axiom -> Axiom -> Axiom Source # min :: Axiom -> Axiom -> Axiom Source #
Show Axiom Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Axiom -> ShowS Source # show :: Axiom -> String Source # showList :: [Axiom] -> ShowS Source #

type RecordAssigns = [RecordAssign] Source #

type RecordAssign = Either Assign ModuleName Source #

type Assigns = [Assign] Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment `f = e`.

data Expr Source #

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

Constructors

Var Name | Bound variable.
Def QName | Constant: axiom, function, data or record type.
Proj ProjOrigin AmbiguousQName | Projection (overloaded).
Con AmbiguousQName | Constructor (overloaded).
PatternSyn AmbiguousQName | Pattern synonym.
Macro QName | Macro.
Lit Literal | Literal.
QuestionMark MetaInfo InteractionId | Meta variable for interaction. The `InteractionId` is usually identical with the `metaNumber` of `MetaInfo`. However, if you want to print an interaction meta as just `?` instead of `?n`, you should set the `metaNumber` to `Nothing` while keeping the `InteractionId`.
Underscore MetaInfo | Meta variable for hidden argument (must be inferred locally).
Dot ExprInfo Expr | `.e`, for postfix projection.
App AppInfo Expr (NamedArg Expr) | Ordinary (binary) application.
WithApp ExprInfo Expr [Expr] | With application.
Lam ExprInfo LamBinding Expr | `λ bs → e`.
AbsurdLam ExprInfo Hiding | `λ()` or `λ{}`.
ExtendedLam ExprInfo DefInfo QName [Clause] |
Pi ExprInfo Telescope Expr | Dependent function space `Γ → A`.
Generalized (Set QName) Expr | Like a Pi, but the ordering is not known
Fun ExprInfo (Arg Expr) Expr | Non-dependent function space.
Set ExprInfo Integer | `Set`, `Set1`, `Set2`, ...
Prop ExprInfo Integer | `Prop`, `Prop1`, `Prop2`, ...
Let ExprInfo [LetBinding] Expr | `let bs in e`.
ETel Telescope | Only used when printing telescopes.
Rec ExprInfo RecordAssigns | Record construction.
RecUpdate ExprInfo Expr Assigns | Record update.
ScopedExpr ScopeInfo Expr | Scope annotation.
QuoteGoal ExprInfo Name Expr | Binds `Name` to current type in `Expr`.
QuoteContext ExprInfo | Returns the current context.
Quote ExprInfo | Quote an identifier `QName`.
QuoteTerm ExprInfo | Quote a term.
Unquote ExprInfo | The splicing construct: unquote ...

Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]

    tactic e x1 .. xn | y1 | .. | yn

DontCare Expr | For printing `DontCare` from `Syntax.Internal`.

Instances

Eq Expr Source # | Does not compare `ScopeInfo` fields. Does not distinguish between prefix and postfix projections.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Expr -> Expr -> Bool Source # (/=) :: Expr -> Expr -> Bool Source #
Data Expr Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Expr -> Constr Source #

dataTypeOf :: Expr -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
KillRange Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Expr Source #
HasRange Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Expr -> Range Source #
Underscore Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #
IsProjP Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
SubstExpr Assign Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Assign -> Assign Source #
SubstExpr Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
AllNames Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Expr -> Seq QName Source #
ExprLike Expr Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr Source # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Expr -> m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
PrettyTCM Expr Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Expr -> TCM Doc Source #
IsFlexiblePattern Pattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern -> TCM Bool Source #
UniverseBi Declaration Pattern Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Pattern] Source #
UniverseBi Declaration Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Expr] Source #
ToAbstract Literal Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Literal -> WithNames Expr Source #
ToAbstract Sort Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Sort -> WithNames Expr Source #
ToAbstract Term Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Term -> WithNames Expr Source #
ToConcrete Pattern Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Pattern -> AbsToCon Pattern0 Source # bindToConcrete :: Pattern -> (Pattern0 -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LHSCore Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHSCore -> AbsToCon Pattern Source # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
ToConcrete Expr Expr Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Expr -> AbsToCon Expr0 Source # bindToConcrete :: Expr -> (Expr0 -> AbsToCon b) -> AbsToCon b Source #
Reify MetaId Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MetaId -> TCM Expr Source # reifyWhen :: Bool -> MetaId -> TCM Expr Source #
Reify Literal Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Literal -> TCM Expr Source # reifyWhen :: Bool -> Literal -> TCM Expr Source #
Reify Level Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Level -> TCM Expr Source # reifyWhen :: Bool -> Level -> TCM Expr Source #
Reify Sort Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Sort -> TCM Expr Source # reifyWhen :: Bool -> Sort -> TCM Expr Source #
Reify Type Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Reify Term Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Term -> TCM Expr Source # reifyWhen :: Bool -> Term -> TCM Expr Source #
Reify Expr Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Expr -> TCM Expr Source # reifyWhen :: Bool -> Expr -> TCM Expr Source #
Reify DisplayTerm Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: DisplayTerm -> TCM Expr Source # reifyWhen :: Bool -> DisplayTerm -> TCM Expr Source #
ToAbstract HoleContent HoleContent Source # | Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: HoleContent0 -> ScopeM HoleContent Source #
ToAbstract Expr Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Expr0 -> ScopeM Expr Source #
ToAbstract OldQName Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldQName -> ScopeM Expr Source #
UniverseBi Declaration (NamedArg Pattern) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source #
UniverseBi Declaration (NamedArg LHSCore) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source #
UniverseBi Declaration (NamedArg Expr) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] Source #
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source #
ToAbstract Pattern (Names, Pattern) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Pattern0 -> WithNames (Names, Pattern) Source #
Reify Constraint (OutputConstraint Expr Expr) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) Source # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) Source #
ToAbstract [Arg Term] [NamedArg Expr] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract (Pattern' Expr) (Pattern' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern' Expr0 -> ScopeM (Pattern' Expr) Source #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore' Expr0 -> ScopeM (LHSCore' Expr) Source #
ToAbstract (Expr, Elims) Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elims) -> WithNames Expr Source #
ToAbstract (Expr, Elim) Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elim) -> WithNames Expr Source #

type Args = [NamedArg Expr] Source #

newtype BindName Source #

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

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

Constructors

BindName |

Fields

- unBind :: Name

Instances

Eq BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: BindName -> BindName -> Bool Source # (/=) :: BindName -> BindName -> Bool Source #
Data BindName Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: BindName -> Constr Source #

dataTypeOf :: BindName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods compare :: BindName -> BindName -> Ordering Source # (<) :: BindName -> BindName -> Bool Source # (<=) :: BindName -> BindName -> Bool Source # (>) :: BindName -> BindName -> Bool Source # (>=) :: BindName -> BindName -> Bool Source # max :: BindName -> BindName -> BindName Source # min :: BindName -> BindName -> BindName Source #
Show BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> BindName -> ShowS Source # show :: BindName -> String Source # showList :: [BindName] -> ShowS Source #
KillRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT BindName Source #
SetRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> BindName -> BindName Source #
HasRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: BindName -> Range Source #
EmbPrj BindName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Int32 Source # icod_ :: BindName -> S Int32 Source # value :: Int32 -> R BindName Source #
ToConcrete BindName BoundName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: BindName -> AbsToCon BoundName Source # bindToConcrete :: BindName -> (BoundName -> AbsToCon b) -> AbsToCon b Source #
UniverseBi Declaration (NamedArg BindName) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] Source #
ToAbstract (NewName BoundName) BindName Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM BindName Source #

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

Smart constructor for Generalized

initCopyInfo :: ScopeCopyInfo Source #

noDataDefParams :: DataDefParams Source #

noWhereDecls :: WhereDeclarations Source #

class SubstExpr a where Source #

Methods

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

Instances

SubstExpr Name Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name0, Expr)] -> Name -> Name Source #
SubstExpr ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
SubstExpr TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> TypedBinding -> TypedBinding Source #
SubstExpr LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> LetBinding -> LetBinding Source #
SubstExpr Assign Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Assign -> Assign Source #
SubstExpr Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
SubstExpr a => SubstExpr [a] Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> [a] -> [a] Source #
SubstExpr a => SubstExpr (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Either a b -> Either a b Source #
(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> (a, b) -> (a, b) Source #
SubstExpr a => SubstExpr (Named name a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #

type PatternSynDefns = Map QName PatternSynDefn Source #

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

class NameToExpr a where Source #

Methods

nameExpr :: a -> Expr Source #

Instances

NameToExpr ResolvedName Source # | Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameExpr :: ResolvedName -> Expr Source #
NameToExpr AbstractName Source # | Turn an `AbstractName` to an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameExpr :: 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 # |
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
AnyAbstract a => AnyAbstract [a] Source # |
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: [a] -> Bool Source #

class AllNames a where Source #

Extracts all the names which are declared in a `Declaration`. This does not include open public or let expressions, but it does include local modules, where clauses and the names of extended lambdas.

Methods

allNames :: a -> Seq QName Source #

Instances

AllNames QName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: QName -> Seq QName Source #
AllNames RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: RHS -> Seq QName Source #
AllNames Clause Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Clause -> Seq QName Source #
AllNames WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: WhereDeclarations -> Seq QName Source #
AllNames TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: TypedBinding -> Seq QName Source #
AllNames LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: LamBinding -> Seq QName Source #
AllNames LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: LetBinding -> Seq QName Source #
AllNames ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: ModuleApplication -> Seq QName Source #
AllNames Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Declaration -> Seq QName Source #
AllNames Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Expr -> Seq QName Source #
AllNames CallInfo Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods allNames :: CallInfo -> Seq QName Source #
AllNames CallPath Source # |
Instance details Defined in Agda.Termination.Monad Methods allNames :: CallPath -> Seq QName Source #
AllNames a => AllNames [a] Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: [a] -> Seq QName Source #
AllNames a => AllNames (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Maybe a -> Seq QName Source #
AllNames a => AllNames (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Arg a -> Seq QName Source #
(AllNames a, AllNames b) => AllNames (a, b) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: (a, b) -> Seq QName Source #
AllNames a => AllNames (Named name a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Named name a -> Seq QName Source #

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

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

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

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

patternToExpr :: Pattern -> Expr Source #

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

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

class IsNoName a where Source #

Check whether a name is the empty name "_".

Methods

isNoName :: a -> Bool Source #

Instances

IsNoName ByteString Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: ByteString -> Bool Source #
IsNoName String Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: String -> Bool Source #
IsNoName QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: QName -> Bool Source #
IsNoName Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Name -> Bool Source #
IsNoName Name Source # | An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool Source #

class MkName a where Source #

Make a `Name` from some kind of string.

Minimal complete definition

mkName

Methods

mkName :: Range -> NameId -> a -> Name Source #

The `Range'` sets the definition site of the name, not the use site.

mkName_ :: NameId -> a -> Name Source #

Instances

MkName String Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods mkName :: Range -> NameId -> String -> Name Source # mkName_ :: NameId -> String -> Name Source #

class IsProjP a where Source #

Check whether we are a projection pattern.

Methods

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

Instances

IsProjP Void Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP a => IsProjP (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP a => IsProjP (Named n a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

newtype AmbiguousQName Source #

Ambiguous qualified names. Used for overloaded constructors.

Invariant: All the names in the list must have the same concrete, unqualified name. (This implies that they all have the same `Range'`).

Constructors

AmbQ |

Fields

- unAmbQ :: NonemptyList QName

Instances

Eq AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: AmbiguousQName -> AmbiguousQName -> Bool Source # (/=) :: AmbiguousQName -> AmbiguousQName -> Bool Source #
Data AmbiguousQName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: AmbiguousQName -> Constr Source #

dataTypeOf :: AmbiguousQName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord AmbiguousQName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: AmbiguousQName -> AmbiguousQName -> Ordering Source #

(<) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

(<=) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

(>) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

(>=) :: AmbiguousQName -> AmbiguousQName -> Bool Source #

max :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName Source #

min :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName Source #

Show AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> AmbiguousQName -> ShowS Source # show :: AmbiguousQName -> String Source # showList :: [AmbiguousQName] -> ShowS Source #
Pretty AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: AmbiguousQName -> Doc Source # prettyPrec :: Int -> AmbiguousQName -> Doc Source # prettyList :: [AmbiguousQName] -> Doc Source #
KillRange AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT AmbiguousQName Source #
HasRange AmbiguousQName Source # | The range of an `AmbiguousQName` is the range of any of its disambiguations (they are the same concrete name).
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range Source #
NumHoles AmbiguousQName Source # | We can have an instance for ambiguous names as all share a common concrete name.
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: AmbiguousQName -> Int Source #
EmbPrj AmbiguousQName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Int32 Source # icod_ :: AmbiguousQName -> S Int32 Source # value :: Int32 -> R AmbiguousQName Source #
NamesIn AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: AmbiguousQName -> Set QName Source #
UniverseBi Declaration AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [AmbiguousQName] Source #

newtype ModuleName Source #

A module name is just a qualified name.

The `SetRange` instance for module names sets all individual ranges to the given one.

Constructors

MName |

Fields

- mnameToList :: [Name]

Instances

Eq ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: ModuleName -> ModuleName -> Bool Source # (/=) :: ModuleName -> ModuleName -> Bool Source #
Data ModuleName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: ModuleName -> Constr Source #

dataTypeOf :: ModuleName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord ModuleName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: ModuleName -> ModuleName -> Ordering Source #

(<) :: ModuleName -> ModuleName -> Bool Source #

(<=) :: ModuleName -> ModuleName -> Bool Source #

(>) :: ModuleName -> ModuleName -> Bool Source #

(>=) :: ModuleName -> ModuleName -> Bool Source #

max :: ModuleName -> ModuleName -> ModuleName Source #

min :: ModuleName -> ModuleName -> ModuleName Source #

Show ModuleName Source # | Only use this `show` function in debugging! To convert an abstract `ModuleName` into a string use `prettyShow`.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> ModuleName -> ShowS Source # show :: ModuleName -> String Source # showList :: [ModuleName] -> ShowS Source #
NFData ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: ModuleName -> () Source #
Pretty ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source #
Sized ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: ModuleName -> Int Source #
KillRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT ModuleName Source #
KillRange Sections Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections Source #
SetRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source #
HasRange ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source #
SubstExpr ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
ExprLike ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleName -> m ModuleName Source # mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName Source #
EmbPrj ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Int32 Source # icod_ :: ModuleName -> S Int32 Source # value :: Int32 -> R ModuleName Source #
PrettyTCM ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ModuleName -> TCM Doc Source #
InstantiateFull ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ModuleName -> ReduceM ModuleName Source #
UniverseBi Declaration ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleName] Source #
ToConcrete ModuleName QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleName -> AbsToCon QName Source # bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b Source #
ToAbstract OldModuleName ModuleName Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldModuleName -> ScopeM ModuleName Source #
ToAbstract NewModuleQName ModuleName Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleQName -> ScopeM ModuleName Source #
ToAbstract NewModuleName ModuleName Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleName -> ScopeM ModuleName Source #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) Source #

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed |

Fields

- qname :: QName
- qnamed :: a

Instances

Functor QNamed Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods fmap :: (a -> b) -> QNamed a -> QNamed b Source # (<$) :: a -> QNamed b -> QNamed a Source #
Foldable QNamed Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

fold :: Monoid m => QNamed m -> m Source #

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

foldr :: (a -> b -> b) -> b -> QNamed a -> b Source #

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

foldl :: (b -> a -> b) -> b -> QNamed a -> b Source #

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

foldr1 :: (a -> a -> a) -> QNamed a -> a Source #

foldl1 :: (a -> a -> a) -> QNamed a -> a Source #

toList :: QNamed a -> [a] Source #

null :: QNamed a -> Bool Source #

length :: QNamed a -> Int Source #

elem :: Eq a => a -> QNamed a -> Bool Source #

maximum :: Ord a => QNamed a -> a Source #

minimum :: Ord a => QNamed a -> a Source #

sum :: Num a => QNamed a -> a Source #

product :: Num a => QNamed a -> a Source #

Traversable QNamed Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods traverse :: Applicative f => (a -> f b) -> QNamed a -> f (QNamed b) Source # sequenceA :: Applicative f => QNamed (f a) -> f (QNamed a) Source # mapM :: Monad m => (a -> m b) -> QNamed a -> m (QNamed b) Source # sequence :: Monad m => QNamed (m a) -> m (QNamed a) Source #
Show a => Show (QNamed a) Source # | Use `prettyShow` to print names to the user.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> QNamed a -> ShowS Source # show :: QNamed a -> String Source # showList :: [QNamed a] -> ShowS Source #
Pretty a => Pretty (QNamed a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QNamed a -> Doc Source # prettyPrec :: Int -> QNamed a -> Doc Source # prettyList :: [QNamed a] -> Doc Source #
PrettyTCM (QNamed Clause) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QNamed Clause -> TCM Doc Source #
ToAbstract (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: QNamed Clause0 -> WithNames Clause Source #
Reify (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause Source #
ToAbstract [QNamed Clause] [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [QNamed Clause0] -> WithNames [Clause] Source #
Reify (QNamed System) [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed System -> TCM [Clause] Source # reifyWhen :: Bool -> QNamed System -> TCM [Clause] Source #

data QName Source #

Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.

The `SetRange` instance for qualified names sets all individual ranges (including those of the module prefix) to the given one.

Constructors

QName |

Fields

- qnameModule :: ModuleName
- qnameName :: Name

Instances

Eq QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: QName -> QName -> Bool Source # (/=) :: QName -> QName -> Bool Source #
Data QName Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: QName -> Constr Source #

dataTypeOf :: QName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: QName -> QName -> Ordering Source # (<) :: QName -> QName -> Bool Source # (<=) :: QName -> QName -> Bool Source # (>) :: QName -> QName -> Bool Source # (>=) :: QName -> QName -> Bool Source # max :: QName -> QName -> QName Source # min :: QName -> QName -> QName Source #
Show QName Source # | Only use this `show` function in debugging! To convert an abstract `QName` into a string use `prettyShow`.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> QName -> ShowS Source # show :: QName -> String Source # showList :: [QName] -> ShowS Source #
Hashable QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods hashWithSalt :: Int -> QName -> Int Source # hash :: QName -> Int Source #
NFData QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: QName -> () Source #
Pretty QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
Sized QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: QName -> Int Source #
KillRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT QName Source #
KillRange RewriteRuleMap Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap Source #
KillRange Definitions Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions Source #
SetRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> QName -> QName Source #
HasRange QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: QName -> Range Source #
LensInScope QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope QName Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source #
NumHoles QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: QName -> Int Source #
TermLike QName Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source # foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #
AllNames QName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: QName -> Seq QName Source #
ExprLike QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName Source # foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName Source # mapExpr :: (Expr -> Expr) -> QName -> QName Source #
EmbPrj QName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
PrettyTCM QName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QName -> TCM Doc Source #
NamesIn QName Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: QName -> Set QName Source #
InstantiateFull QName Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: QName -> ReduceM QName Source #
Occurs QName Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> QName -> TCM QName Source # metaOccurs :: MetaId -> QName -> TCM () Source #
FromTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction QName) Source #
ToTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (QName -> Term) Source # toTermR :: TCM (QName -> ReduceM Term) Source #
PrimTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: QName -> TCM Term Source #
Unquote QName Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM QName Source #
UniverseBi Declaration QName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [QName] Source #
Subst Term QName Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods applySubst :: Substitution' Term -> QName -> QName Source #
ToConcrete QName QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: QName -> AbsToCon QName0 Source # bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b Source #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Conversion MOT (Exp O) Type Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion TOM (Arg Pattern) (Pat O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
(Show a, ToQName a) => ToAbstract (OldName a) QName Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldName a -> ScopeM QName Source #
ToConcrete (Maybe QName) (Maybe Name) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Maybe QName -> AbsToCon (Maybe Name) Source # bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b Source #

data Name Source #

A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.

Constructors

Name |

Fields

- nameId :: !NameId
- nameConcrete :: Name
- nameBindingSite :: Range
- nameFixity :: Fixity'
- nameIsRecordName :: Bool

Instances

Eq Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
Data Name Source # |

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: Name -> Constr Source #

dataTypeOf :: Name -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Show Name Source # | Only use this `show` function in debugging! To convert an abstract `Name` into a string use `prettyShow`.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
Hashable Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods hashWithSalt :: Int -> Name -> Int Source # hash :: Name -> Int Source #
NFData Name Source # | The range is not forced.
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: Name -> () Source #
Pretty Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: Name -> Doc Source # prettyPrec :: Int -> Name -> Doc Source # prettyList :: [Name] -> Doc Source #
KillRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT Name Source #
SetRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> Name -> Name Source #
HasRange Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: Name -> Range Source #
IsNoName Name Source # | An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool Source #
LensInScope Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope Name Source # isInScope :: Name -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> Name -> Name Source # setInScope :: Name -> Name Source # setNotInScope :: Name -> Name Source #
NumHoles Name Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: Name -> Int Source #
EmbPrj Name Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
PrettyTCM Name Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Name -> TCM Doc Source #
AddContext Name Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Name -> tcm a -> tcm a Source # contextSize :: Name -> Nat Source #
InstantiateFull Name Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Name -> ReduceM Name Source #
Subst Term Name Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Name -> Name Source #
ToConcrete Name Name Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Name -> AbsToCon Name0 Source # bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b Source #
Reify Name Name Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Name -> TCM Name Source # reifyWhen :: Bool -> Name -> TCM Name Source #
Suggest Name (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Name -> Abs b -> String Source #
ToAbstract Pattern (Names, Pattern) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Pattern0 -> WithNames (Names, Pattern) Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
ToAbstract (NewName Name) Name Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name Source #
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Abs r -> WithNames (a, Name) Source #
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Abs i -> TCM (Name, a) Source # reifyWhen :: Bool -> Abs i -> TCM (Name, a) Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Dom r, Name) -> WithNames TypedBinding Source #

uglyShowName :: Name -> String Source #

Useful for debugging scoping problems

unambiguous :: QName -> AmbiguousQName Source #

A singleton "ambiguous" name.

headAmbQ :: AmbiguousQName -> QName Source #

Get the first of the ambiguous names.

isAmbiguous :: AmbiguousQName -> Bool Source #

Is a name ambiguous.

getUnambiguous :: AmbiguousQName -> Maybe QName Source #

Get the name if unambiguous.

isAnonymousModuleName :: ModuleName -> Bool Source #

A module is anonymous if the qualification path ends in an underscore.

withRangesOf :: ModuleName -> [Name] -> ModuleName Source #

Sets the ranges of the individual names in the module name to match those of the corresponding concrete names. If the concrete names are fewer than the number of module name name parts, then the initial name parts get the range `noRange`.

`C.D.E `withRangesOf` [A, B]` returns `C.D.E` but with ranges set as follows:

- `C`: `noRange`.
- `D`: the range of `A`.
- `E`: the range of `B`.

Precondition: The number of module name name parts has to be at least as large as the length of the list.

withRangesOfQ :: ModuleName -> QName -> ModuleName Source #

Like `withRangesOf`, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.

mnameFromList :: [Name] -> ModuleName Source #

noModuleName :: ModuleName Source #

commonParentModule :: ModuleName -> ModuleName -> ModuleName Source #

qnameToList :: QName -> [Name] Source #

qnameFromList :: [Name] -> QName Source #

qnameToMName :: QName -> ModuleName Source #

mnameToQName :: ModuleName -> QName Source #

showQNameId :: QName -> String Source #

qnameToConcrete :: QName -> QName Source #

Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.

mnameToConcrete :: ModuleName -> QName Source #

toTopLevelModuleName :: ModuleName -> TopLevelModuleName Source #

Computes the `TopLevelModuleName` corresponding to the given module name, which is assumed to represent a top-level module name.

Precondition: The module name must be well-formed.

qualifyM :: ModuleName -> ModuleName -> ModuleName Source #

qualifyQ :: ModuleName -> QName -> QName Source #

qualify :: ModuleName -> Name -> QName Source #

qualify_ :: Name -> QName Source #

Convert a `Name` to a `QName` (add no module name).

isOperator :: QName -> Bool Source #

Is the name an operator?

isSubModuleOf :: ModuleName -> ModuleName -> Bool Source #

isInModule :: QName -> ModuleName -> Bool Source #

nextName :: Name -> Name Source #

Get the next version of the concrete name. For instance, `nextName "x" = "x₁"`. The name must not be a `NoName`.

sameRoot :: Name -> Name -> Bool Source #