blob: 136f680e229163c9446415a53659a99a8c9f2e14 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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
type ty0
instance (Size ty0) let size = 0 end
declare isabelle target_rep type ty1 = `0`
val undefined_int : forall 'rv 'e. unit -> monad 'rv integer 'e
let undefined_int () = return 0
val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
let undefined_bitvector len = return (zeros(len))
val undefined_unit : forall 'rv 'e. unit -> monad 'rv unit 'e
let undefined_unit () = return ()
val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
let internal_pick xs = return (List_extra.head xs)
|
