Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Translation.ReflectedToAbstract

Synopsis

Documentation

type Vars = [(Name, Type)] Source #

type MonadReflectedToAbstract (m :: Type -> Type) = (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.

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Term Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (QNamed Clause) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Arg r) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Arg r) = NamedArg (AbsOfRef r)
ToAbstract r => ToAbstract (Abs r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Abs r) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Abs r) = (AbsOfRef r, Name)
ToAbstract (List1 (QNamed Clause)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (List1 (QNamed Clause)) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract [QNamed Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [QNamed Clause] 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r => ToAbstract [Arg r] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [Arg r] 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]
ToAbstract r => ToAbstract (Named name r) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Named name r) 
Instance details

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

ToAbstract (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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