haskell-core-semantics
haskell-core-semantics copied to clipboard
kframework
Haskell's Core in K.
It might be a while until we implement a neat solution for equality that captures precisely what's going on in Haskell. Until then, let's implement a primitive equality using the...
At this point we can start testing our K operational semantics by adding some hand-written GHC Core programs. To use `ktest` for testing, we should specify the designated output in...
Our primary goal is to implement the operational semantics in K. The following rules from the [Eisenberg spec](https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf) need to be implemented. - [x] S_Var - [x] S_App - [x]...
We have defined the `DataCon` sort in the K grammar as ``` syntax DataCon ::= "dataCon" "(" Name ")" ``` where `Name` is just `Id`. With this, constructor names consisting...