pure
pure copied to clipboard
CakeML
A verified compiler for a lazy functional language
Add an `Annot` form to `cexp` as follows: ``` annot = Inline mlstring | ... cexp = ... | Annot annot cexp ``` This should desugar as follows: `exp_of (Annot...
Extend the parser to cope with Haskell-line inlining annotations. We should mirror the syntax described [here](https://wiki.haskell.org/Inlining_and_Specialisation) as much as possible.
The inliner should act on user annotations specifying inlining locations.
Augment inlining relation to handle `letrec`s in memory, and inline them by unrolling loops.
Currently `Case` desugars to a series of nested `let` expressions, e.g.: ``` exp_of (case x = e of C a b c -> k) => let x = exp_of e...
**Define TypeClassLang, a new source language with type classes.** TypeClassLang should have both typed and untyped variants - i.e. it can be in either "mode". This could be implemented by...
**Redirect parsing to target TypeClassLang** Aside from PureLang's existing constructs, this will need to handle: - `class` and `instance` declarations - contexts/type class constraints in types - TypeClassLang's new top-level...
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...
When testing compiler modifications we generally don't want to wait for a verified binary to be compiled in-logic. This issue is about creating an unverified binary pipeline. The idea is...
The top-level result for TypeClassLang should state: - given a well-annotated TypeClassLang program - there should be a valid translation to a PureLang program - which is itself well-typed (and...