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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
open import Pervasives
open import Vector
open import Arch
(* 'a is result type, 'e is error type *)
type M 's 'e 'a = 's -> (either 'a 'e * 's)
val return : forall 's 'e 'a. 'a -> M 's 'e 'a
let return a s = (Left a,s)
val bind : forall 's 'e 'a 'b. M 's 'e 'a -> ('a -> M 's 'e 'b) -> M 's 'e 'b
let bind m f s = match m s with
| (Left a,s') -> f a s'
| (Right error,s') -> (Right error,s')
end
val exit : forall 's 'e 'a. 'e -> M 's 'e 'a
let exit e s = (Right e,s)
let (>>=) = bind
let (>>) m n = m >>= fun _ -> n
val read_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> M state 'e (vector bit)
let read_reg_range reg (i,j) s =
let v = slice (read_regstate s reg) i j in
(Left v,s)
val read_reg_bit : forall 'e. register -> integer (*nat*) -> M state 'e bit
let read_reg_bit reg i s =
let v = access (read_regstate s reg) i in
(Left v,s)
val write_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> vector bit -> M state 'e unit
let write_reg_range (reg : register) (i,j) (v : vector bit) s =
let v' = update (read_regstate s reg) i j v in
let s' = write_regstate s reg v' in
(Left (),s')
val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> M state 'e unit
let write_reg_bit reg i bit s =
let v = read_regstate s reg in
let v' = update_pos v i bit in
let s' = write_regstate s reg v' in
(Left (),s')
val read_reg : forall 'e. register -> M state 'e (vector bit)
let read_reg reg s =
let v = read_regstate s reg in
(Left v,s)
val write_reg : forall 'e. register -> vector bit -> M state 'e unit
let write_reg reg v s =
let s' = write_regstate s reg v in
(Left (),s')
val foreach_inc : forall 's 'e 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
(integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
let rec foreach_inc (i,stop,by) vars body =
if i <= stop
then
let (_,vars) = body i vars in
foreach_inc (i + by,stop,by) vars body
else ((),vars)
val foreach_dec : forall 's 'e 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
(integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
let rec foreach_dec (i,stop,by) vars body =
if i >= stop
then
let (_,vars) = body i vars in
foreach_dec (i - by,stop,by) vars body
else ((),vars)
val foreachM_inc : forall 's 'e 'vars. (nat * nat * nat) -> 'vars ->
(nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars)
let rec foreachM_inc (i,stop,by) vars body =
if i <= stop
then
body i vars >>= fun (_,vars) ->
foreachM_inc (i + by,stop,by) vars body
else return ((),vars)
val foreachM_dec : forall 's 'e 'vars. (nat * nat * nat) -> 'vars ->
(nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars)
let rec foreachM_dec (i,stop,by) vars body =
if i >= stop
then
body i vars >>= fun (_,vars) ->
foreachM_dec (i - by,stop,by) vars body
else return ((),vars)
val read_reg_field : forall 'e. register -> register_field -> M state 'e (vector bit)
let read_reg_field reg rfield = read_reg_range reg (field_indices rfield)
val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit
let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit
let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)
val write_reg_field_bit : forall 'e. register -> register_field_bit -> bit -> M state 'e unit
let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit)
let length l = integerFromNat (length l)
let write_two_regs r1 r2 vec =
let size = length_reg r1 in
let start = get_start vec in
let vsize = length vec in
let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in
let r2_v =
(slice vec)
(if defaultDir then size - start else start - size)
(if defaultDir then vsize - start else start - vsize) in
write_reg r1 r1_v >> write_reg r2 r2_v
|
