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

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 Vars = [(Name, Type)] Source #

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.

withVar :: MonadReflectedToAbstract m => String -> Type -> (Name -> m a) -> m a Source #

withNames :: MonadReflectedToAbstract m => [String] -> ([Name] -> m a) -> m a Source #

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

askVar :: MonadReflectedToAbstract m => Int -> m (Maybe (Name, Type)) Source #

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

askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name) Source #

class ToAbstract r where Source #

Minimal complete definition

Nothing

Associated Types

type AbsOfRef r Source #

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

Instances details

ToAbstract Literal Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Literal Source # Methods toAbstract :: MonadReflectedToAbstract m => Literal -> m (AbsOfRef Literal) Source #
ToAbstract Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Pattern Source # Methods toAbstract :: MonadReflectedToAbstract m => Pattern -> m (AbsOfRef Pattern) Source #
ToAbstract Sort Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Sort Source # Methods toAbstract :: MonadReflectedToAbstract m => Sort -> m (AbsOfRef Sort) Source #
ToAbstract Term Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Term Source # Methods toAbstract :: MonadReflectedToAbstract m => Term -> m (AbsOfRef Term) Source #
ToAbstract (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (QNamed Clause) Source # Methods toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause)) Source #
ToAbstract r => ToAbstract (Arg r) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Arg r) Source # Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (AbsOfRef (Arg r)) Source #
ToAbstract r => ToAbstract (Abs r) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Abs r) Source # Methods toAbstract :: MonadReflectedToAbstract m => Abs r -> m (AbsOfRef (Abs r)) Source #
ToAbstract (List1 (QNamed Clause)) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (List1 (QNamed Clause)) Source # Methods toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause))) Source #
ToAbstract [QNamed Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef [QNamed Clause] Source # Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause]) Source #
ToAbstract r => ToAbstract [Arg r] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef [Arg r] Source # Methods toAbstract :: MonadReflectedToAbstract m => [Arg r] -> m (AbsOfRef [Arg r]) Source #
ToAbstract r => ToAbstract (Named name r) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Named name r) Source # Methods toAbstract :: MonadReflectedToAbstract m => Named name r -> m (AbsOfRef (Named name r)) Source #
ToAbstract (Expr, Elim) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elim) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #
ToAbstract (Expr, Elims) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elims) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Dom r, Name) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source #

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 #

mkDef :: HasConstInfo m => QName -> m Expr Source #

mkApp :: Expr -> Expr -> Expr Source #

mkVar :: MonadReflectedToAbstract m => Int -> m (Name, Type) Source #

mkVarName :: MonadReflectedToAbstract m => Int -> m Name 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).