| Safe Haskell | None |
|---|
DDC.Core.Lite
Description
Disciple Core Lite.
This is a desugared version of Disciple Core that has all the polymorphism of System-F2 along with algebraic data types. It does not yet support user-defined data types, but has Units, Ints, Pairs and Lists baked in.
Lite exposes arithmetic primops like add, but no store or
control primops. Code written in Lite cannot corrupt the heap, assuming
the implementation of the Salt primitives it uses (and compiler) is
correct.
- profile :: Profile Name
- saltOfLiteModule :: Show a => Platform -> Config -> DataDefs Name -> KindEnv Name -> TypeEnv Name -> Module (AnTEC a Name) Name -> Either (Error a) (Module a Name)
- data Error a
- data Name
- = NameVar String
- | NameCon String
- | NameEffectTyCon EffectTyCon
- | NameDataTyCon DataTyCon
- | NamePrimDaCon PrimDaCon
- | NamePrimTyCon PrimTyCon
- | NamePrimArith PrimArith
- | NamePrimCast PrimCast
- | NameLitBool Bool
- | NameLitNat Integer
- | NameLitInt Integer
- | NameLitWord Integer Int
- data DataTyCon
- data PrimTyCon
- data PrimDaCon
- data PrimArith
- = PrimArithNeg
- | PrimArithAdd
- | PrimArithSub
- | PrimArithMul
- | PrimArithDiv
- | PrimArithRem
- | PrimArithEq
- | PrimArithNeq
- | PrimArithGt
- | PrimArithGe
- | PrimArithLt
- | PrimArithLe
- | PrimArithAnd
- | PrimArithOr
- | PrimArithShl
- | PrimArithShr
- | PrimArithBAnd
- | PrimArithBOr
- | PrimArithBXOr
- data PrimCast
- readName :: String -> Maybe Name
- lexModuleString :: String -> Int -> String -> [Token (Tok Name)]
- lexExpString :: String -> Int -> String -> [Token (Tok Name)]
Language profile
Conversion
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 | Lite module to convert. |
| -> Either (Error a) (Module a Name) | Salt module. |
Convert a Disciple Core Lite module to Disciple Core Salt.
Case expressions on algebraic data values are converted into ones that just check the tag, while data constructors are unfolded into explicit allocation and field initialization primops.
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.
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
| ErrorMainHasNoMain | The |
| ErrorMalformed String | Found unexpected AST node, like |
| ErrorMistyped (Exp (AnTEC a Name) Name) | The program is definately not well typed. |
| ErrorNotNormalized String | The program wasn't in a-normal form. |
| ErrorBotAnnot | The program has bottom (missing) type annotations. |
| ErrorUnexpectedSum | Found an unexpected type sum. |
| ErrorInvalidBinder Name | An invalid name used in a binding position |
| ErrorInvalidBound (Bound Name) | An invalid name used in a bound position |
| ErrorInvalidAlt | An invalid name used for the constructor of an alternative. |
Names
Names of things used in Disciple Core Lite.
Constructors
| NameVar String | User defined variables. |
| NameCon String | A user defined constructor. |
| NameEffectTyCon EffectTyCon | Baked in effect type constructors. |
| NameDataTyCon DataTyCon | Baked in data type constructors. |
| NamePrimDaCon PrimDaCon | A primitive data constructor. |
| NamePrimTyCon PrimTyCon | A primitive type constructor. |
| NamePrimArith PrimArith | Primitive arithmetic, logic, comparison and bit-wise operators. |
| NamePrimCast PrimCast | Primitive casting between numeric types. |
| NameLitBool Bool | An unboxed boolean literal |
| NameLitNat Integer | An unboxed natural literal. |
| NameLitInt Integer | An unboxed integer literal. |
| NameLitWord Integer Int | An unboxed word literal |
Baked-in data type constructors.
Constructors
| DataTyConUnit |
|
| DataTyConBool |
|
| DataTyConNat |
|
| DataTyConInt |
|
| DataTyConPair |
|
| DataTyConList |
|
Primitive type constructors.
Constructors
| PrimTyConVoid |
|
| PrimTyConBool |
|
| PrimTyConNat |
|
| PrimTyConInt |
|
| PrimTyConWord Int |
|
| PrimTyConFloat Int |
|
| PrimTyConTag |
|
| PrimTyConAddr |
|
| PrimTyConPtr |
|
| PrimTyConString |
These are primitive until we can define our own unboxed types. |
Baked-in data constructors.
Constructors
| PrimDaConUnit | Unit data constructor |
| PrimDaConBoolU |
|
| PrimDaConNatU |
|
| PrimDaConIntU |
|
| PrimDaConPr |
|
| PrimDaConNil |
|
| PrimDaConCons |
|
Primitive arithmetic, logic, and comparison opretors. We expect the backend/machine to be able to implement these directly.
For the Shift Right operator, the type that it is used at determines whether it is an arithmetic (with sign-extension) or logical (no sign-extension) shift.
Constructors
| PrimArithNeg | Negation |
| PrimArithAdd | Addition |
| PrimArithSub | Subtraction |
| PrimArithMul | Multiplication |
| PrimArithDiv | Division |
| PrimArithRem | Remainder |
| PrimArithEq | Equality |
| PrimArithNeq | Negated Equality |
| PrimArithGt | Greater Than |
| PrimArithGe | Greater Than or Equal |
| PrimArithLt | Less Than |
| PrimArithLe | Less Than or Equal |
| PrimArithAnd | Boolean And |
| PrimArithOr | Boolean Or |
| PrimArithShl | Shift Left |
| PrimArithShr | Shift Right |
| PrimArithBAnd | Bit-wise And |
| PrimArithBOr | Bit-wise Or |
| PrimArithBXOr | Bit-wise eXclusive Or |
Primitive cast between two types.
The exact set of available casts is determined by the target platform.
For example, you can only promote a Nat# to a Word32# on a 32-bit
system. On a 64-bit system the Nat# type is 64-bits wide, so casting it
to a Word32# would be a truncation.
Constructors
| PrimCastPromote | Promote a value to one of similar or larger width, without loss of precision. |
| PrimCastTruncate | Truncate a value to a new width, possibly losing precision. |