Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Translation.ReflectedToAbstract

Synopsis

- 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
- 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))
- askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)
- class ToAbstract r where
  - type AbsOfRef r
  - toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r)
- toAbstract_ :: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) => r -> m (AbsOfRef r)
- toAbstractWithoutImplicit :: (ToAbstract r, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m, HasConstInfo m) => r -> m (AbsOfRef r)
- 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
- checkClauseTelescopeBindings :: MonadReflectedToAbstract m => [(Text, Arg Type)] -> [Arg Pattern] -> m ()

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

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

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 type AbsOfRef Literal = Expr

Methods

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

ToAbstract Pattern Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Pattern = Pattern

Methods

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

ToAbstract Sort Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Sort = Expr

Methods

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

ToAbstract Term Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Term = Expr

Methods

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

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

Methods

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

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)

Methods

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

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)

Methods

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

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

Methods

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

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

Methods

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

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

Methods

toAbstract :: MonadReflectedToAbstract m => [Arg r] -> m (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) |
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 type AbsOfRef (Expr, Elim) = Expr

Methods

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

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 type AbsOfRef (Expr, Elims) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (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) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (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.

mkMetaInfo :: ReadTCState m => m MetaInfo Source #

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

mkApp :: Expr -> Expr -> Expr Source #

mkVar :: MonadReflectedToAbstract m => Int -> m (Name, Type) Source #

mkVarName :: MonadReflectedToAbstract m => Int -> m Name Source #

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