blob: fba8d9b75440f004e1acb3b7567b43ccffc011ee (
plain)
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
121
122
|
open import Pervasives_extra
(*open import Sail_impl_base*)
open import Sail_values
open import Prompt_monad
open import Prompt
open import State_monad
open import {isabelle} `State_monad_extras`
(* State monad wrapper around prompt monad *)
val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
let rec liftState ra s = match s with
| (Done a) -> returnS a
| (Read_mem rk a sz k) -> bindS (read_memS rk a sz) (fun v -> liftState ra (k v))
| (Write_memv descr k) -> bindS (write_mem_valS descr) (fun v -> liftState ra (k v))
| (Read_reg descr k) -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
| (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
| (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
| (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
| (Barrier _ k) -> liftState ra k
| (Fail descr) -> failS descr
| (Error descr) -> failS descr
| (Exception e) -> throwS e
end
(* TODO
val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
let rec iter_aux i f xs = match xs with
| x :: xs -> f i x >> iter_aux (i + 1) f xs
| [] -> return ()
end
val iteri : forall 'regs 'e 'a. (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
let iteri f xs = iter_aux 0 f xs
val iter : forall 'regs 'e 'a. ('a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
let iter f xs = iteri (fun _ x -> f x) xs
val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec foreachM_inc (i,stop,by) vars body =
if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
else return vars
val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec foreachM_dec (i,stop,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
foreachM_dec (i - by,stop,by) vars body
else return vars
val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
let rec while_PP vars cond body =
if cond vars then while_PP (body vars) cond body else vars
val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec while_PM vars cond body s =
if cond vars then
bind (body vars) (fun vars s' -> while_PM vars cond body s') s
else return vars s
val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
('vars -> 'vars) -> M 'regs 'vars 'e
let rec while_MP vars cond body s =
bind
(cond vars)
(fun cond_val s' ->
if cond_val then while_MP (body vars) cond body s' else return vars s') s
val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec while_MM vars cond body s =
bind
(cond vars)
(fun cond_val s' ->
if cond_val then
bind
(body vars)
(fun vars s'' -> while_MM vars cond body s'') s'
else return vars s') s
val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
let rec until_PP vars cond body =
let vars = body vars in
if (cond vars) then vars else until_PP (body vars) cond body
val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec until_PM vars cond body s =
bind
(body vars)
(fun vars s' ->
if (cond vars) then return vars s' else until_PM vars cond body s') s
val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
('vars -> 'vars) -> M 'regs 'vars 'e
let rec until_MP vars cond body s =
let vars = body vars in
bind
(cond vars)
(fun cond_val s' ->
if cond_val then return vars s' else until_MP vars cond body s') s
val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
let rec until_MM vars cond body s =
bind
(body vars)
(fun vars s' ->
bind
(cond vars)
(fun cond_val s''->
if cond_val then return vars s'' else until_MM vars cond body s'') s') s
*)
|
