Safe Haskell | None |
---|---|
Language | Haskell98 |
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
:: 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.
ErrorCurry Error | |
ErrorMainHasNoMain | The |
ErrorMalformed | Found unexpected AST node, like |
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. |
| |
ErrorInvalidBinder | An invalid name used in a binding position |
ErrorInvalidBound | An invalid name used in a bound position |
| |
ErrorInvalidDaCon | An invalid data constructor name. |
| |
ErrorInvalidAlt | An invalid name used for the constructor of an alternative. |
ErrorInvalidScrut | Something that we can't destruct in a case expression. |
|