Agda.Syntax.Translation.ReflectedToAbstract

Documentation

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

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

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))

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

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

class ToAbstract r where

Minimal complete definition

Nothing

Associated Types

type AbsOfRef r

Methods

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

default toAbstract :: (Traversable t, ToAbstract s, t s ~ r, t (AbsOfRef s) ~ AbsOfRef r) => MonadReflectedToAbstract m => r -> m (AbsOfRef r)

Instances

ToAbstract Literal

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Literal

Methods

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

ToAbstract Pattern

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern

Methods

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

ToAbstract Sort

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort

Methods

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

ToAbstract Term

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term

Methods

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

ToAbstract (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause)

Methods

toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause))

ToAbstract r => ToAbstract (Arg r)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Arg r)

Methods

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

ToAbstract r => ToAbstract (Abs r)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Abs r)

Methods

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

ToAbstract (List1 (QNamed Clause))

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (List1 (QNamed Clause))

Methods

toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause)))

ToAbstract [QNamed Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [QNamed Clause]

Methods

toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause])

ToAbstract r => ToAbstract [Arg r]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [Arg r]

Methods

toAbstract :: MonadReflectedToAbstract m => [Arg r] -> m (AbsOfRef [Arg r])

ToAbstract r => ToAbstract (Named name r)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Named name r)

Methods

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

ToAbstract (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim)

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim))

ToAbstract (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims)

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims))

(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name))

toAbstract_ :: (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.

toAbstractWithoutImplicit :: (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.

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 ()

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).