myreen

At present, the compiler proofs are regression tested. This means the compiler generated code will always stay correct. However, the compiler and its configuration are not currently tested for quality....

The compiler generates some `Delay`s that are very simple. There ought to be a pass in EnvLang that does this: ``` Delay (Var v) --> Box v ``` This issue...

Inlining in PureLang

1

Here are some plans for the PureLang inliner. The PureLang inliner *implementation* is to carry *only* let bindings that it can inline. The relational proofs are allowed to be more...

Complete chain of ThunkLang optimisations

1

The following is the proposed sequence of optimisations for ThunkLang. The actual implementation might merge a few of these. 1. pure-to-thunk incorporates let-force (unlike now) 2. pull lam out of...

Type signature support

2

Type inferencer ignores type signatures. Example: ``` foo :: String -> Int -> UndefinedType -> [Bool] foo i = () main = Ret (foo 1) ```

The compiler accepts this: ``` l1 ++ l2 = case l1 of [] -> l2 h:t -> h : (t ++ l2) main = Ret () ``` But rejects any...

Impossible to define/raise user-defined exceptions

1

This works: ``` data Error = Fail main = Raise Subscript ``` While the following is rejected by the compiler: ``` data Error = Fail main = Raise Fail ```

Currently, EnvLang's `Box` expression is: ``` exp = ... | Var vname | Box exp | ... ``` but it should arguably be: ``` exp = ... | Var vname...

Make sure `case .. of True => ... | False => ...` compiles to `If ... ... ...`

2

Currently, `cexp` at source level doesn't have `If`. We need to make sure that the case expressions that really are `If` compile to `If` in CakeML.

Move backend relations to compiler/backend/languages/relations

1

This issue is about moving all syntactic relations to compiler/backend/languages/relations. In that directory: - each file should only have one syntactic relation it "exports" - each file has 3 sections:...