blob: 6e242cafdfa15424db61834192d22d36690eea17 (
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
(*Require Import Sail_impl_base*)
Require Import Sail2_values.
Require Import Sail2_prompt_monad.
Require Import Sail2_prompt.
Require Import Sail2_state_monad.
Import ListNotations.
(*val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
Fixpoint iterS_aux {RV A E} i (f : Z -> A -> monadS RV unit E) (xs : list A) :=
match xs with
| x :: xs => f i x >>$ iterS_aux (i + 1) f xs
| [] => returnS tt
end.
(*val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
Definition iteriS {RV A E} (f : Z -> A -> monadS RV unit E) (xs : list A) : monadS RV unit E :=
iterS_aux 0 f xs.
(*val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
Definition iterS {RV A E} (f : A -> monadS RV unit E) (xs : list A) : monadS RV unit E :=
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*)
Fixpoint foreachS {A RV Vars E} (xs : list A) (vars : Vars) (body : A -> Vars -> monadS RV Vars E) : monadS RV Vars E :=
match xs with
| [] => returnS vars
| x :: xs =>
body x vars >>$= fun vars =>
foreachS xs vars body
end.
(*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*)
Definition genlistS {A RV E} (f : nat -> monadS RV A E) n : monadS RV (list A) E :=
let indices := List.seq 0 n in
foreachS indices [] (fun n xs => (f n >>$= (fun x => returnS (xs ++ [x])))).
(*val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e*)
Definition and_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
l >>$= (fun l => if l then r else returnS false).
(*val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e*)
Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
l >>$= (fun l => if l then returnS true else r).
Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFact (P b)} E) (y : monadS rv {b:bool & ArithFact (Q b)} E)
`{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))}
: monadS rv {b:bool & ArithFact (R b)} E.
refine (
x >>$= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then
fun p => y >>$= fun '(existT _ y _) => returnS (existT _ y _)
else fun p => returnS (existT _ false _)) p
).
* constructor. destruct H. destruct a0. change y with (andb true y). auto.
* constructor. destruct H. change false with (andb false false). apply fact.
assumption.
congruence.
Defined.
Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFact (P b)} E) (r : monadS rv {b : bool & ArithFact (Q b)} E)
`{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))}
: monadS rv {b : bool & ArithFact (R b)} E.
refine (
l >>$= fun '(existT _ l (Build_ArithFact _ p)) =>
(if l return P l -> _ then fun p => returnS (existT _ true _)
else fun p => r >>$= fun '(existT _ r _) => returnS (existT _ r _)) p
).
* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence.
* constructor. destruct H. destruct a0. change r with (orb false r). auto.
Defined.
(*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e*)
Definition bool_of_bitU_fail {RV E} (b : bitU) : monadS RV bool E :=
match b with
| B0 => returnS false
| B1 => returnS true
| BU => failS "bool_of_bitU"
end.
(*val bool_of_bitU_nondetS : forall 'rv 'e. bitU -> monadS 'rv bool 'e*)
Definition bool_of_bitU_nondetS {RV E} (b : bitU) : monadS RV bool E :=
match b with
| B0 => returnS false
| B1 => returnS true
| BU => undefined_boolS tt
end.
(*val bools_of_bits_nondetS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e*)
Definition bools_of_bits_nondetS {RV E} bits : monadS RV (list bool) E :=
foreachS bits []
(fun b bools =>
bool_of_bitU_nondetS b >>$= (fun b =>
returnS (bools ++ [b]))).
(*val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*)
Definition of_bits_nondetS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E :=
bools_of_bits_nondetS bits >>$= (fun bs =>
returnS (of_bools bs)).
(*val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*)
Definition of_bits_failS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E :=
maybe_failS "of_bits" (of_bits bits).
(*val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
let mword_nondetS () =
bools_of_bits_nondetS (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
*)
(*val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e*)
Definition choose_boolsS {RV E} n : monadS RV (list bool) E :=
genlistS (fun _ => choose_boolS tt) n.
(* TODO: Replace by chooseS and prove equivalence to prompt monad version *)
(*val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e*)
Definition internal_pickS {RV A E} (xs : list A) : monadS RV A E :=
(* Use sufficiently many nondeterministically chosen bits and convert into an
index into the list *)
choose_boolsS (List.length xs) >>$= fun bs =>
let idx := ((nat_of_bools bs) mod List.length xs)%nat in
match List.nth_error xs idx with
| Some x => returnS x
| None => failS "choose internal_pick"
end.
|
