cakeml

cakeml copied to clipboard

Translator should use a custom compset

5

Currently, it makes use of [simp] and EVAL in ml_progLib to control the EVALs that in ml_translatorLib

tanyongkiam

Add tail-recursion modulo cons (TMC) optimisation

4

This issue is about adding [tail-recursion modulo cons (TMC)](https://dl.acm.org/doi/10.1145/3571233) as a new optimisation to the CakeML compiler. The idea is to automatically transform non-tail-recursive functions such as fun append []...

myreen

The CakeML source language has arbitrary precision integers as the main integer type. These are implemented dynamically as either smallnums or bignums. A smallnum is used in case the value...

myreen

Implement bignum library at level of machine code for certain targets

1

The current version of the CakeML compiler has a bignum library that is generic for all targets and is implemented as part of `data_to_word`. Version 1 of the compiler had...

myreen

@myreen claims the translator now does this, although not using ThmSetData correctly (not storing only deltas) _Originally posted by @xrchz in https://github.com/CakeML/cakeml/issues/360#issuecomment-2470572325_

xrchz

Make CakeML build on the experimental kernel

9

The task here is to get the CakeML regression test to pass on HOL's experimental (and/or logging) kernels: the only difference should be in generated names, so this means making...

xrchz

Add word shifts to basis

3

Currently, the basis library doesn't include any shift operations in the Word8 or Word64 modules, and the parser can't generate Opapps with a Shift operation. Thus, the user cannot write...

SOwens

Support pattern matching in let declarations

3

Currently the grammar only supports a limited subset of declarations within `let` expressions (the `LetDec` non-terminal). It would be nice if these could be expanded to allow pattern-matching and wildcards....

xrchz

Support for multi-case functions defined by pattern matching

8

Function declarations currently only accept variables as arguments, but in SML one can do pattern matching with a declaration. CakeML AST does not support that, but the parser could generate...

xrchz

Add instructions for efficient Div and Mul by (powers of) 2

6

In `data_to_word` (i.e., the closLang ops).

xrchz