1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
default Order dec
$include <prelude.sail>
struct My_struct = {
field1 : int,
field2 : bit,
}
val struct_field2 : My_struct -> bit
function struct_field2(s) = {
s.field2
}
val struct_update_field2 : (My_struct, bit) -> My_struct
function struct_update_field2(s, b) = {
{ s with field2 = b }
}
val struct_update_both_fields : (My_struct, int, bit) -> My_struct
function struct_update_both_fields(s, i, b) = {
{ s with field1 = i, field2 = b }
}
val mk_struct : (int, bit) -> My_struct
function mk_struct(i, b) = {
struct {
field1 = i,
field2 = b
}
}
val undef_struct : bit -> My_struct
function undef_struct (x) = {
(undefined_My_struct(): My_struct)
}
function match_struct(value : My_struct) -> int = {
match value {
struct { _, field2 = bitzero } => 0,
struct { field1, field2 = bitone } => field1
}
}
struct My_mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
va : option(bits('vasize)),
pa : 'pa,
translation : 'ts,
size : int('n),
value : option(bits(8 * 'n)),
tag : option(bool),
}
|
