diff options
| author | Brian Campbell | 2018-02-08 15:03:34 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-02-08 15:03:42 +0000 |
| commit | 579cd897d7873436ba6cfb3469b185bf6b321dac (patch) | |
| tree | 1ca652f246135f2ad4973acbb5051a2c79e0d411 /lib | |
| parent | 45519ae89ceef4c838cdd52e2bbaa4174e63f27d (diff) | |
Add (most of) the bitvector cast insertion transformation
to help Lem go from a general type `bits('n)` to a specific type `bits(16)`
at a case split, and the other way around for a returned value.
Doesn't handle function clause patterns yet
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/mono_rewrites.sail | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 1af9b17f..167a2fdd 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -27,6 +27,10 @@ val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure function extsv(v) = exts_vec(sizeof('m),v) +/* This is generated internally to deal with case splits which reveal the size + of a bitvector */ +val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure + /* Definitions for the rewrites */ val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure |