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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
struct cr = {
CR0 : bits(4),
CR1 : bits(2),
CR2 : bits(2)
}
val _set_CR0 : (register(cr), bits(4)) -> unit effect {wreg}
val _get_CR0 : register(cr) -> bits(4) effect {rreg}
val _set_CR1 : (register(cr), bits(2)) -> unit effect {wreg}
val _get_CR1 : register(cr) -> bits(2) effect {rreg}
val _set_CR2 : (register(cr), bits(2)) -> unit effect {wreg}
val _get_CR2 : register(cr) -> bits(2) effect {rreg}
function _set_CR0 (cr_ref, v) = {
cr = _reg_deref(cr_ref);
cr.CR0 = v;
(*cr_ref) = cr;
}
function _get_CR0 cr = reg_deref(cr).CR0
function _set_CR1 (cr_ref, v) = {
cr = _reg_deref(cr_ref);
cr.CR1 = v;
(*cr_ref) = cr;
}
function _get_CR1 cr = reg_deref(cr).CR1
function _set_CR2 (cr_ref, v) = {
cr = _reg_deref(cr_ref);
cr.CR2 = v;
(*cr_ref) = cr;
}
function _get_CR2 cr = reg_deref(cr).CR2
overload _mod_CR0 = {_set_CR0, _get_CR0}
overload _mod_CR1 = {_set_CR1, _get_CR1}
overload _mod_CR2 = {_set_CR2, _get_CR2}
val _get_cr : register(cr) -> bits(8) effect {rreg}
function _get_cr cr_ref =
let cr = reg_deref(cr_ref) in cr.CR0 @ cr.CR1 @ cr.CR2
val _set_cr : (register(cr), bits(8)) -> unit effect {wreg}
function _set_cr (cr_ref, v) = {
cr = _reg_deref(cr_ref);
cr.CR0 = v[7 .. 4];
cr.CR1 = v[3 .. 2];
cr.CR2 = v[1 .. 0];
(*cr_ref) = cr
}
overload _mod_cr = {_set_cr, _get_cr}
register CR : cr
val main : unit -> unit effect {wreg, rreg}
function main () = {
CR->cr() = 0x00;
print_bits("CR = ", CR->cr());
CR->cr() = 0xCA;
print_bits("CR = ", CR->cr());
print_bits("CR.CR0 = ", CR->CR0());
print_bits("CR.CR1 = ", CR->CR1());
print_bits("CR.CR2 = ", CR->CR2());
CR->CR0() = 0xF;
print_bits("CR = ", CR->cr());
CR->CR2() = 0b00;
print_bits("CR = ", CR->cr());
()
}
|