Safe Haskell | None |
---|
- data Name
- data PrimCon
- data PrimOp
- data Loc = Loc Int
- data Rgn = Rgn Int
- data Cap
- = CapGlobal
- | CapConst
- | CapMutable
- | CapDistinct Int
- | CapLazy
- | CapManifest
- readName :: String -> Maybe Name
- lexModuleString :: String -> Int -> String -> [Token (Tok Name)]
- lexExpString :: String -> Int -> String -> [Token (Tok Name)]
Documentation
Names of things recognised by the evaluator.
NameVar String | User variables. |
NameCon String | User constructors. |
NameInt Integer | Integer literals (which data constructors). |
NamePrimCon PrimCon | Primitive constructors (eg |
NamePrimOp PrimOp | Primitive operators (eg |
NameLoc Loc | Store locations. |
NameRgn Rgn | Region handles. |
NameCap Cap | Store capabilities. |
A primitive constructor.
PrimTyConInt |
|
PrimTyConPair |
|
PrimTyConList |
|
PrimDaConPr |
|
PrimDaConNil |
|
PrimDaConCons |
|
A primitive operator.
A store location.
These are pretty printed like L4#
.
A region handle.
These are pretty printed like R5#
.
These are primitive witnesses that guarantee the associated property of the program. Ostensibly, they are only introduced by the system at runtime, but for testing purposes we can also inject them into the source program.
CapGlobal | Witness that a region is global. Global regions live for the duration of the program and are not deallocated in a stack like manner. This lets us hide the use of such regions, and rely on the garbage collector to reclaim the space. |
CapConst | Witness that a region is constant. This lets us purify read and allocation effects on it, and prevents it from being Mutable. |
CapMutable | Witness that a region is mutable. This lets us update objects in the region, and prevents it from being Constant. |
CapDistinct Int | Witness that some regions are distinct This lets us perform aliasing based optimisations. |
CapLazy | Witness that a region is lazy. This lets is allocate thunks into the region, and prevents it from being Manifest. |
CapManifest | Witness that a region is manifest. This ensures there are no thunks in the region, which prevents it from being Lazy. |