pure
pure copied to clipboard
CakeML
A verified compiler for a lazy functional language
Lack of a module system results in significantly duplicated code between PureCake programs. A lightweight module system will help this considerably. This issue gives a high level overview of the...
Currently, EnvLang's `Box` expression is: ``` exp = ... | Var vname | Box exp | ... ``` but it should arguably be: ``` exp = ... | Var vname...
PureLang's equational theory simplifies some of its compiler proofs considerably. We should introduce a theory for ThunkLang, to simplify verification of its future passes. ThunkLang is call-by-value, so (untyped) step-indexed...
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.
Alluded to in #40, ThunkLang passes are unusual: `pure_to_thunk` first `Force`s all variables (which are thunks), then `thunk_let_force` attempts to detect eager variables (those that are `seq`ed) and un-`Force` them....
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:...
Currently PureLang's equational theory and its results are distributed over various files. We should restructure this carefully: - `pure_exp_relTheory`: definition of applicative bisimulation and associated theorems - `pure_howeTheory`: Howe's construction...
The compiler should support debug output, printing expressions so we can see the effects of optimisations and plan improvements. For PureLang we have `compiler/parsing/sexp` - at least ThunkLang should implement...
Some theories are unused. These should be checked to see if anything is worth keeping around - if not, they should be deleted. These seem to include the following, but...
Infinite coinductive values are defined in `pure_valueTheory`, but no longer necessary. However, they can't be removed easily because some value-based results are lifted to weak-head results (e.g. using `eval_eq_imp_app_similarity`). The...