Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Translation.ReflectedToAbstract

Synopsis

Documentation

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

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 #

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern Source #

ToAbstract Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort Source #

ToAbstract Term Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term Source #

ToAbstract (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type 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 #

ToAbstract r => ToAbstract (Abs r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type 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 #

ToAbstract [QNamed Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type 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 #

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 #

ToAbstract (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type 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 #

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.

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