diff options
Diffstat (limited to 'test/mono/test_extra.lem')
| -rw-r--r-- | test/mono/test_extra.lem | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/mono/test_extra.lem b/test/mono/test_extra.lem new file mode 100644 index 00000000..a567257c --- /dev/null +++ b/test/mono/test_extra.lem @@ -0,0 +1,17 @@ +open import Pervasives_extra +open import Sail_instr_kinds +open import Sail_values +open import Sail_operators_mwords +open import Prompt_monad +open import State + +let undefined_int () = (0:ii) +val undefined_bitvector : forall 'a. Size 'a => integer -> mword 'a +let undefined_bitvector len = duplicate B0 len + +val uint : forall 'a. Size 'a => mword 'a -> integer +let uint = unsigned + +val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b +let slice v lo len = + subrange_vec_dec v (lo + len - 1) lo |
