Agda.Syntax.Translation.ReflectedToAbstract

Documentation

type Vars = [(Name, 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)

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 :: forall (t :: Type -> Type) s m. (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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Literal = Expr

Methods

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

ToAbstract Pattern

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Pattern = Pattern

Methods

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

ToAbstract Sort

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Sort = Expr

Methods

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

ToAbstract Term

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Term = Expr

Methods

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

ToAbstract (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (QNamed Clause) = 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)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Arg r) = NamedArg (AbsOfRef 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)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Abs r) = (AbsOfRef r, Name)

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (List1 (QNamed Clause)) = List1 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]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [QNamed Clause] = [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]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [Arg r] = [NamedArg (AbsOfRef 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)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Named name r) = Named name (AbsOfRef 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)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) = Expr

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)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

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)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

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