blob: 2dc8dd134f98ef72b63fae68e7a6b4ba2ce05691 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_state
let undefined_int () = return (0:ii)
let undefined_unit () = return ()
val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e
let undefined_bitvector len = return (of_bools (repeat [false] len))
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
|
