Safe Haskell | None |
---|---|
Language | Haskell98 |
Definitions of Source Tetra primitive names and operators.
- data PrimType
- readPrimType :: String -> Maybe PrimType
- data PrimTyCon :: *
- kindPrimTyCon :: PrimType ~ GTPrim l => PrimTyCon -> GType l
- pattern KData :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern KRegion :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern KEffect :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TImpl :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t
- pattern TSusp :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t
- pattern TRead :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t
- pattern TWrite :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t
- pattern TAlloc :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t
- pattern TBool :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TNat :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TInt :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TSize :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TWord :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t
- pattern TFloat :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t
- pattern TTextLit :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- data PrimTyConTetra
- kindPrimTyConTetra :: (~#) * * (GTPrim l) PrimType => PrimTyConTetra -> GType l
- data PrimVal
- readPrimVal :: String -> Maybe PrimVal
- data PrimArith :: *
- typePrimArith :: (Anon l, GTPrim l ~ PrimType) => l -> PrimArith -> GType l
- data PrimCast :: *
- typePrimCast :: (Anon l, GTPrim l ~ PrimType) => l -> PrimCast -> GType l
- data OpVector :: *
- typeOpVector :: forall l. (Anon l, GTPrim l ~ PrimType) => l -> OpVector -> GType l
- data OpFun :: *
- typeOpFun :: (Anon l, GTPrim l ~ PrimType) => l -> OpFun -> GType l
- data OpError :: * = OpErrorDefault
- typeOpError :: ((~#) * * (GTPrim l) PrimType, Anon l) => l -> OpError -> GType l
- makeXErrorDefault :: (GXBoundCon l ~ DaConBound, GXPrim l ~ PrimVal, GTPrim l ~ PrimType) => Text -> Integer -> GExp l
- data PrimLit
- = PrimLitBool !Bool
- | PrimLitNat !Integer
- | PrimLitInt !Integer
- | PrimLitSize !Integer
- | PrimLitWord !Integer !Int
- | PrimLitFloat !Double !Int
- | PrimLitChar !Char
- | PrimLitTextLit !Text
- readPrimLit :: String -> Maybe PrimLit
- primLitOfLiteral :: Literal -> PrimLit
- pattern PTrue :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t
- pattern PFalse :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t
Primitive Types
Primitive types.
PrimTypeSoCon !SoCon | Primitive sort constructors. |
PrimTypeKiCon !KiCon | Primitive kind constructors. |
PrimTypeTwCon !TwCon | Primitive witness type constructors. |
PrimTypeTcCon !TcCon | Other type constructors at the spec level. |
PrimTypeTyCon !PrimTyCon | Primitive machine type constructors. |
PrimTypeTyConTetra !PrimTyConTetra | Primtiive type constructors specific to the Tetra fragment. |
Primitive machine type constructors.
Primitive type constructors.
PrimTyConVoid |
|
PrimTyConBool |
|
PrimTyConNat |
|
PrimTyConInt |
|
PrimTyConSize |
|
PrimTyConWord Int |
|
PrimTyConFloat Int |
|
PrimTyConVec Int |
|
PrimTyConAddr |
|
PrimTyConPtr |
|
PrimTyConTextLit |
|
PrimTyConTag |
|
kindPrimTyCon :: PrimType ~ GTPrim l => PrimTyCon -> GType l Source #
Yield the kind of a type constructor.
pattern KData :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #
Representation of the Data kind.
pattern KRegion :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #
Representation of the Region kind.
pattern KEffect :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #
Representation of the Effect kind.
pattern TImpl :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t Source #
Representation of an implication type.
pattern TSusp :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t Source #
Representation of a suspension type.
pattern TRead :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t Source #
Representation of a read effect.
pattern TWrite :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t Source #
Representation of a write effect.
pattern TAlloc :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t Source #
Representation of a alloc effect.
pattern TWord :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t Source #
Primitive WordN
type of the given width.
pattern TFloat :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t Source #
Primitive FloatN
type of the given width.
pattern TTextLit :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #
Primitive TextLit
type.
Primitive tetra type constructors.
data PrimTyConTetra Source #
Primitive type constructors specific to the Tetra language fragment.
PrimTyConTetraTuple !Int |
|
PrimTyConTetraVector |
|
PrimTyConTetraF |
|
PrimTyConTetraC |
|
PrimTyConTetraU |
|
kindPrimTyConTetra :: (~#) * * (GTPrim l) PrimType => PrimTyConTetra -> GType l Source #
Take the kind of a baked-in data constructor.
Primitive values
Primitive values.
PrimValLit !PrimLit | Primitive literals. |
PrimValArith !PrimArith | Primitive arithmetic operators. |
PrimValCast !PrimCast | Primitive numeric casting operators. |
PrimValError !OpError | Primitive error handling. |
PrimValVector !OpVector | Primitive vector operators. |
PrimValFun !OpFun | Primitive function operators. |
Primitive arithmetic operators.
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.
PrimArithNeg | Negation |
PrimArithAdd | Addition |
PrimArithSub | Subtraction |
PrimArithMul | Multiplication |
PrimArithDiv | Division |
PrimArithMod | Modulus |
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 |
typePrimArith :: (Anon l, GTPrim l ~ PrimType) => l -> PrimArith -> GType l Source #
Take the type of a primitive arithmetic operator.
Primitive casting operators.
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.
PrimCastConvert | Convert a value to a new representation with the same precision. |
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. |
typePrimCast :: (Anon l, GTPrim l ~ PrimType) => l -> PrimCast -> GType l Source #
Take the type of a primitive arithmetic operator.
Primitive vector operators.
Vector operators.
OpVectorAlloc | Allocate a new vector of a given length number of elements. |
OpVectorLength | Get the length of a vector, in elements. |
OpVectorRead | Read a value from a vector. |
OpVectorWrite | Write a value to a vector. |
typeOpVector :: forall l. (Anon l, GTPrim l ~ PrimType) => l -> OpVector -> GType l Source #
Take the type of a primitive vector operator.
Primitive function operators.
Operators for building function values and closures. The implicit versions work on functions of type (a -> b), while the explicit versions use expliciy closure types like C# (a -> b).
OpFunCurry Int | Partially apply a supecombinator to some arguments, producing an implicitly typed closure. |
OpFunApply Int | Apply an implicitly typed closure to some more arguments. |
OpFunCReify | Reify a function into an explicit functional value. |
OpFunCCurry Int | Apply an explicit functional value to some arguments, producing an explicitly typed closure. |
OpFunCExtend Int | Extend an explicitly typed closure with more arguments, producing a new closure. |
OpFunCApply Int | Apply an explicitly typed closure to some arguments, possibly evaluating the contained function. |
typeOpFun :: (Anon l, GTPrim l ~ PrimType) => l -> OpFun -> GType l Source #
Take the type of a primitive function operator.
Primitive error handling
Operators for runtime error reporting.
OpErrorDefault | Raise an error due to inexhaustive case expressions. |
typeOpError :: ((~#) * * (GTPrim l) PrimType, Anon l) => l -> OpError -> GType l Source #
Take the type of a primitive error function.
makeXErrorDefault :: (GXBoundCon l ~ DaConBound, GXPrim l ~ PrimVal, GTPrim l ~ PrimType) => Text -> Integer -> GExp l Source #
Primitive literals
PrimLitBool !Bool | A boolean literal. |
PrimLitNat !Integer | A natural literal, with enough precision to count every heap object. |
PrimLitInt !Integer | An integer literal, with enough precision to count every heap object. |
PrimLitSize !Integer | An unsigned size literal, with enough precision to count every addressable byte of memory. |
PrimLitWord !Integer !Int | A word literal, with the given number of bits precison. |
PrimLitFloat !Double !Int | A floating point literal, with the given number of bits precision. |
PrimLitChar !Char | A character literal. |
PrimLitTextLit !Text | Text literals (UTF-8 encoded) |
primLitOfLiteral :: Literal -> PrimLit Source #
Convert a literal to a Tetra name.
pattern PTrue :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t Source #
pattern PFalse :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t Source #