ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Translation.ReflectedToAbstract

2 types
1 class
15 values

PackageAgda-2.7.0.1
Exports18
LanguageHaskell2010
LicenceMIT
SourceReflectedToAbstract.hs

typetype Vars = [(Name, Type)]

type

type MonadReflectedToAbstract (m :: Type -> Type) = (MonadReader Vars m, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m)

valuewithName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a

Adds a new unique name to the current context. NOTE: See chooseName in Agda.Syntax.Translation.AbstractToConcrete for similar logic. NOTE: See freshConcreteName in Agda.Syntax.Scope.Monad also for similar logic.

valuewithVar

:: MonadReflectedToAbstract m
=> String
-> Type
-> Name -> m a
-> m a

valuewithNames

:: MonadReflectedToAbstract m
=> [String]
-> [Name] -> m a
-> m a

valuewithVars

:: MonadReflectedToAbstract m
=> [(String, Type)]
-> [Name] -> m a
-> m a

valueaskVar :: MonadReflectedToAbstract m => Int -> m (Maybe (Name, Type))

Returns the name and type of the variable with the given de Bruijn index.

valueaskName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)

classclass ToAbstract r where

Associated types

type family AbsOfRef r

Methods

toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r)

Instances14ToAbstract, …

ToAbstract LiteralDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract SortDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract TermDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract (QNamed Clause)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract (List1 (QNamed Clause))Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract [QNamed Clause]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract r => ToAbstract (Arg r)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract r => ToAbstract (Abs r)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract r => ToAbstract [Arg r]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract (Expr, Elim)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract (Expr, Elims)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract r => ToAbstract (Named name r)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ReflectedToAbstract

valuetoAbstract_

:: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m)
=> r
-> m (AbsOfRef r)

Translate reflected syntax to abstract, using the names from the current typechecking context.

valuetoAbstractWithoutImplicit

:: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m)
=> r
-> m (AbsOfRef r)

Drop implicit arguments unless --show-implicit is on.

valuemkMetaInfo :: ReadTCState m => m MetaInfo

valuemkDef :: HasConstInfo m => QName -> m Expr

valuemkApp :: Expr -> Expr -> Expr

valuemkVar :: MonadReflectedToAbstract m => Int -> m (Name, Type)

valuemkVarName :: MonadReflectedToAbstract m => Int -> m Name

valueannotatePattern

:: MonadReflectedToAbstract m
=> Int
-> Type
-> Pattern
-> m Pattern

valuecheckClauseTelescopeBindings

:: MonadReflectedToAbstract m
=> [(Text, Arg Type)]
-> [Arg Pattern]
-> m ()

Check that all variables in the telescope are bound in the left-hand side. Since we check the telescope by attaching type annotations to the pattern variables there needs to be somewhere to put the annotation. Also, since the lhs is where the variables are actually bound, missing a binding for a variable that's used later in the telescope causes unbound variable panic (see #5044).