search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
969 stars 85 forks source link

Add word shifts to basis #274

Open SOwens opened 7 years ago

SOwens commented 7 years ago

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 programs that shift words in the surface syntax.

Ideally, we'd like to add >> and << as 2 argument CakeML functions, but the Shift op is a unary op with the amount to shift built into the operator. We either need to make Shift a binary op, or we have to add a restricted form of shifting where >> is defined in the basis as a function of two arguments that does a case split on the 2nd to pick out which Shift to actually do.

tanyongkiam commented 7 years ago

By the way, the bootstrap translation currently uses these custom rewrites (that were recently moved into miscTheory):

https://github.com/CakeML/cakeml/blob/master/miscScript.sml#L2568

So these should translate fine for the basis if we are going for that route.

xrchz commented 7 years ago

Maybe this interacts with #171

tanyongkiam commented 3 weeks ago

Related to #246 (we should just have variable length shifts throughout the compiler)