| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
DDC.Core.Tetra.Convert
Description
Conversion of Disciple Core Tetra to Disciple Core Salt.
- saltOfTetraModule :: Show a => Platform -> Config -> DataDefs Name -> KindEnv Name -> TypeEnv Name -> Module (AnTEC a Name) Name -> Either (Error a) (Module a Name)
- data Error a
- = ErrorCurry Error
- | ErrorMainHasNoMain
- | ErrorMalformed { }
- | ErrorMistyped { }
- | ErrorUnsupported { }
- | ErrorBotAnnot
- | ErrorUnexpectedSum
- | ErrorUnbound {
- errorBound :: Bound Name
- | ErrorInvalidBinder { }
- | ErrorInvalidBound {
- errorBound :: Bound Name
- | ErrorInvalidDaCon {
- errorDaCon :: DaCon Name (Type Name)
- | ErrorInvalidAlt { }
- | ErrorInvalidScrut {
- errorScrut :: Exp (AnTEC a Name) Name
Documentation
Arguments
| :: Show a | |
| => Platform | Platform specification. |
| -> Config | Runtime configuration. |
| -> DataDefs Name | Data type definitions. |
| -> KindEnv Name | Kind environment. |
| -> TypeEnv Name | Type environment. |
| -> Module (AnTEC a Name) Name | Tetra module to convert. |
| -> Either (Error a) (Module a Name) | Salt module. |
Convert a Core Tetra module to Core Salt.
The input module needs to be:
well typed,
fully named with no deBruijn indices,
have all functions defined at top-level,
have type annotations on every bound variable and constructor,
be a-normalised,
have saturated function applications,
not have over-applied function applications,
have all supers in prenex form, with type parameters before value parameters.
If not then Error.
The output code contains: debruijn indices. These then need to be eliminated before it will pass the Salt fragment checks.
Things that can go wrong during the conversion.
Constructors
| ErrorCurry Error | |
| ErrorMainHasNoMain | The |
| ErrorMalformed | Found unexpected AST node, like |
Fields | |
| ErrorMistyped | The program is definately not well typed. |
| ErrorUnsupported | The program wasn't normalised, or we don't support the feature. |
| ErrorBotAnnot | The program has bottom (missing) type annotations. |
| ErrorUnexpectedSum | Found an unexpected type sum. |
| ErrorUnbound | Found an unbound variable. |
Fields
| |
| ErrorInvalidBinder | An invalid name used in a binding position |
| ErrorInvalidBound | An invalid name used in a bound position |
Fields
| |
| ErrorInvalidDaCon | An invalid data constructor name. |
Fields
| |
| ErrorInvalidAlt | An invalid name used for the constructor of an alternative. |
| ErrorInvalidScrut | Something that we can't destruct in a case expression. |
Fields
| |