| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Translation.ReflectedToAbstract
Synopsis
- type Vars = [(Name, Type)]
- type MonadReflectedToAbstract m = (MonadReader Vars m, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m)
- withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a
- withVar :: MonadReflectedToAbstract m => String -> Type -> (Name -> m a) -> m a
- withNames :: MonadReflectedToAbstract m => [String] -> ([Name] -> m a) -> m a
- withVars :: MonadReflectedToAbstract m => [(String, Type)] -> ([Name] -> m a) -> m a
- askVar :: MonadReflectedToAbstract m => Int -> m (Maybe (Name, Type))
- askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)
- class ToAbstract r where
- type AbsOfRef r
- toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r)
- toAbstract_ :: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) => r -> m (AbsOfRef r)
- toAbstractWithoutImplicit :: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) => r -> m (AbsOfRef r)
- mkMetaInfo :: ReadTCState m => m MetaInfo
- mkDef :: HasConstInfo m => QName -> m Expr
- mkApp :: Expr -> Expr -> Expr
- mkVar :: MonadReflectedToAbstract m => Int -> m (Name, Type)
- mkVarName :: MonadReflectedToAbstract m => Int -> m Name
- annotatePattern :: MonadReflectedToAbstract m => Int -> Type -> Pattern -> m Pattern
- checkClauseTelescopeBindings :: MonadReflectedToAbstract m => [(Text, Arg Type)] -> [Arg Pattern] -> m ()
Documentation
type MonadReflectedToAbstract m = (MonadReader Vars m, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) Source #
withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a Source #
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.
askVar :: MonadReflectedToAbstract m => Int -> m (Maybe (Name, Type)) Source #
Returns the name and type of the variable with the given de Bruijn index.
class ToAbstract r where Source #
Minimal complete definition
Nothing
Methods
toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r) Source #
default toAbstract :: (Traversable t, ToAbstract s, t s ~ r, t (AbsOfRef s) ~ AbsOfRef r) => MonadReflectedToAbstract m => r -> m (AbsOfRef r) Source #
Instances
toAbstract_ :: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) => r -> m (AbsOfRef r) Source #
Translate reflected syntax to abstract, using the names from the current typechecking context.
toAbstractWithoutImplicit :: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) => r -> m (AbsOfRef r) Source #
Drop implicit arguments unless --show-implicit is on.
mkMetaInfo :: ReadTCState m => m MetaInfo Source #
annotatePattern :: MonadReflectedToAbstract m => Int -> Type -> Pattern -> m Pattern Source #
checkClauseTelescopeBindings :: MonadReflectedToAbstract m => [(Text, Arg Type)] -> [Arg Pattern] -> m () Source #
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).