Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Translation.ReflectedToAbstract

Synopsis

type Names = [Name]
type MonadReflectedToAbstract m = (MonadReader Names m, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m)
withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a
askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)
class ToAbstract r a | r -> a where
- toAbstract :: MonadReflectedToAbstract m => r -> m a
toAbstract_ :: (ToAbstract r a, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) => r -> m a
toAbstractWithoutImplicit :: (ToAbstract r a, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) => r -> m a
mkDef :: HasConstInfo m => QName -> m Expr
mkSet :: Expr -> Expr
toAbstractPats :: MonadReflectedToAbstract m => [Arg Pattern] -> m (Names, [NamedArg Pattern])

Documentation

type Names = [Name] Source #

type MonadReflectedToAbstract m = (MonadReader Names m, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) Source #

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

Adds a new unique name to the current context.

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

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

class ToAbstract r a | r -> a where Source #

Methods

toAbstract :: MonadReflectedToAbstract m => r -> m a Source #

Instances

Instances details

ToAbstract Literal Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Literal -> m Expr Source #
ToAbstract Sort Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Sort -> m Expr Source #
ToAbstract Term Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Term -> m Expr Source #
ToAbstract Pattern (Names, Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Pattern0 -> m (Names, Pattern) Source #
ToAbstract (QNamed Clause) Clause Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => QNamed Clause0 -> m Clause Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source #
ToAbstract [QNamed Clause] [Clause] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause0] -> m [Clause] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (NamedArg a) Source #
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Abs r -> m (a, Name) Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m TypedBinding Source #
ToAbstract (Expr, Elims) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m Expr Source #
ToAbstract (Expr, Elim) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m Expr Source #
ToAbstract r a => ToAbstract (Named name r) (Named name a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Named name r -> m (Named name a) Source #

toAbstract_ :: (ToAbstract r a, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) => r -> m a Source #

Translate reflected syntax to abstract, using the names from the current typechecking context.

toAbstractWithoutImplicit :: (ToAbstract r a, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) => r -> m a Source #

Drop implicit arguments unless --show-implicit is on.

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

mkSet :: Expr -> Expr Source #

toAbstractPats :: MonadReflectedToAbstract m => [Arg Pattern] -> m (Names, [NamedArg Pattern]) Source #