blob: 6bc304a8cee680ba90072ff204858e14b649ccbd (
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
|
open import Pervasives_extra
open import Sail_values
open import State_monad
open import {isabelle} `State_monad_lemmas`
val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
let rec iterS_aux i f xs = match xs with
| x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
| [] -> returnS ()
end
declare {isabelle} termination_argument iterS_aux = automatic
val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
let iteriS f xs = iterS_aux 0 f xs
val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
let iterS f xs = iteriS (fun _ x -> f x) xs
val foreachS : forall 'a 'rv 'vars 'e.
list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
let rec foreachS xs vars body = match xs with
| [] -> returnS vars
| x :: xs ->
body x vars >>$= fun vars ->
foreachS xs vars body
end
declare {isabelle} termination_argument foreachS = automatic
val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e
let bool_of_bitU_fail = function
| B0 -> returnS false
| B1 -> returnS true
| BU -> failS "bool_of_bitU"
end
val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
let bool_of_bitU_oracleS = function
| B0 -> returnS false
| B1 -> returnS true
| BU -> undefined_boolS ()
end
val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
let bools_of_bits_oracleS bits =
foreachS bits []
(fun b bools ->
bool_of_bitU_oracleS b >>$= (fun b ->
returnS (bools ++ [b])))
val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
let of_bits_oracleS bits =
bools_of_bits_oracleS bits >>$= (fun bs ->
returnS (of_bools bs))
val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
let mword_oracleS () =
bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
returnS (wordFromBitlist bs))
val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
let rec whileS vars cond body s =
(cond vars >>$= (fun cond_val s' ->
if cond_val then
(body vars >>$= (fun vars s'' -> whileS vars cond body s'')) s'
else returnS vars s')) s
val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
let rec untilS vars cond body s =
(body vars >>$= (fun vars s' ->
(cond vars >>$= (fun cond_val s'' ->
if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
|
