cakeml

cakeml copied to clipboard

Update CakeML tutorial to use monadic translator

1

Currently the CakeML tutorial, i.e. the files under [tutorial/solutions](https://github.com/CakeML/cakeml/tree/master/tutorial/solutions) and particularly [wordfreqProgScript.sml](https://github.com/CakeML/cakeml/blob/master/tutorial/solutions/wordfreqProgScript.sml), is based on CF proofs. Since the monadic translator, which is described in [Proof-Producing Synthesis of CakeML with...

myreen

Implement make_ex in CakeML

1

Following #350 we now have a small SML program to generate the tutorial exercises, currently at `tutorial/solutions/make_ex.sml`. This issue is to re-implement this program in CakeML instead (including automatically generating...

xrchz

Update code base to use Theorem, Definition, Inductive, Type etc

1

The [latest HOL](https://github.com/HOL-Theorem-Prover/HOL/releases/tag/kananaskis-13) has support for nice user facing syntax. This issue is about updating the entire code base to use the new syntax. Two steps: 1. update all definitions,...

myreen

xsimpl is sometimes unsafe

1

Consider the goal ``` W8ARRAY av a ==>> W8ARRAY av a * &(?loc. av = Loc loc) ``` This goal is easily provable, but applying `xsimpl` reduces it to the...

IlmariReissumies

Implement lexer on mlstrings

3

The CakeML lexer operates on a `char list`. Therefore the first thing the CakeML compiler does after reading in its input string is `explode` the string into a list. This...

xrchz

Efficient peep-hole optimisation for DataLang

1

Peep-hole optimisation is an interesting optimisation that the CakeML compiler lacks at present. This issue is about adding a peep-hole optimiser to the CakeML compiler, in particular, to the DataLang...

myreen

Verify a more sophisticated pattern-match compiler

3

This issue is about optimizing the compilation of pattern-matching expressions and improving the exhaustiveness checking for patterns. Two strategies for pattern-matching compilation backtracking and decision trees, described : - Backtracking...

aceawan

Implement lexer on a stream

2

This issue is to make the lexer take an input stream, and add some facility for turning strings into input streams. This probably subsumes #353 although is probably harder.

xrchz

Remove accumulator-based functions from the semantics

2

Ideally, auxiliary functions used in the semantics should have the simplest possible presentation, and not use accumulators. E.g. `pat_bindings` currently has type `pat -> list varN -> list varN` but...

charguer

Loops can be encoded using tail-ref functions. Yet, they are incredibly useful in the surface language. Especially for describing algorithms. Many graph algorithms take the form `while not (queue.is_empty()) do...

charguer