Rename Undefined outcome to Choose

It is used for nondeterministic choice, so Undefined might be
misleading.

11 files changed, 89 insertions, 37 deletions

diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index 76750117..98b7d077 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -164,7 +164,7 @@ qed
 lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
   unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def)
 
-lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q"
+lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> set xs. Q (Value x) s) (chooseS xs) Q"
   by (auto simp: PrePost_def chooseS_def)
 
 lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q"
@@ -381,7 +381,7 @@ lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (e
   unfolding exitS_def PrePostE_def PrePost_def failS_def by auto
 
 lemma PrePostE_chooseS[intro, PrePostE_atomI]:
-  "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E"
+  "PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (chooseS xs) Q E"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
 lemma PrePostE_throwS[PrePostE_atomI]: "PrePostE (E (Throw e)) (throwS e) Q E"
@@ -488,11 +488,11 @@ lemma PrePostE_liftState_untilM_pure_cond:
   shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E"
   using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp)
 
-lemma PrePostE_undefined_boolS[PrePostE_atomI]:
+lemma PrePostE_choose_boolS_any[PrePostE_atomI]:
   "PrePostE (\<lambda>s. \<forall>b. Q b s)
-            (undefined_boolS unit) Q E"
-  unfolding undefined_boolS_def seqS_def
-  by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS)
+            (choose_boolS unit) Q E"
+  unfolding choose_boolS_def seqS_def
+  by (auto intro: PrePostE_strengthen_pre)
 
 lemma PrePostE_bool_of_bitU_nondetS_any:
   "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E"
@@ -507,11 +507,19 @@ lemma PrePostE_bools_of_bits_nondetS_any:
             PrePostE_bool_of_bitU_nondetS_any)+)
      auto
 
+lemma PrePostE_choose_boolsS_any:
+  "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (choose_boolsS n) Q E"
+  unfolding choose_boolsS_def genlistS_def Let_def
+  by (rule PrePostE_weaken_post[where B = "\<lambda>_ s. \<forall>bs. Q bs s"], rule PrePostE_strengthen_pre,
+      (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS
+            PrePostE_choose_boolS_any)+)
+     auto
+
 lemma PrePostE_internal_pick:
   "xs \<noteq> [] \<Longrightarrow> PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (internal_pickS xs) Q E"
   unfolding internal_pickS_def Let_def
   by (rule PrePostE_strengthen_pre,
-      (rule PrePostE_compositeI PrePostE_atomI PrePostE_bools_of_bits_nondetS_any)+)
+      (rule PrePostE_compositeI PrePostE_atomI PrePostE_choose_boolsS_any)+)
      (auto split: option.splits)
 
 end
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index 545e47c4..fb73a673 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -2,7 +2,7 @@ session "Sail" = "LEM" +
   options [browser_info, document = pdf, document_output = "output"]
   sessions
     "HOL-Eisbach"
-  theories [document = false]
+  theories
     Sail2_values_lemmas
     Sail2_prompt
     Sail2_state_lemmas
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
index fd54c93a..3e8dcb2f 100644
--- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy
+++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
@@ -55,7 +55,7 @@ lemma bool_of_bitU_monadic_simps[simp]:
   "bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
   "bool_of_bitU_nondet B0 = return False"
   "bool_of_bitU_nondet B1 = return True"
-  "bool_of_bitU_nondet BU = undefined_bool ()"
+  "bool_of_bitU_nondet BU = choose_bool ''bool_of_bitU''"
   unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def
   by auto
 
@@ -68,7 +68,7 @@ lemma update_vec_dec_simps[simp]:
   "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
   "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)"
   "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)"
-  "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
+  "update_vec_dec_nondet w i BU = choose_bool ''bool_of_bitU'' \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
   "update_vec_dec w i B0 = set_bit w (nat i) False"
   "update_vec_dec w i B1 = set_bit w (nat i) True"
   unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_nondet_def update_vec_dec_def
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index c59fc62f..54f58fad 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -40,7 +40,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T"
 | Read_reg: "((Read_reg r k), E_read_reg r v, k v) \<in> T"
 | Write_reg: "((Write_reg r v k), E_write_reg r v, k) \<in> T"
-| Undefined: "((Undefined k), E_undefined v, k v) \<in> T"
+| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T"
 | Print: "((Print msg k), E_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
@@ -70,7 +70,7 @@ lemma Traces_cases:
   | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = E_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
   | (Footprint) k t' where "m = Footprint k" and "t = E_footprint # t'" and "(k, t', m') \<in> Traces"
   | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = E_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
-  | (Undefined) xs v k t' where "m = Undefined k" and "t = E_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Choose) descr v k t' where "m = Choose descr k" and "t = E_choose descr v # t'" and "(k v, t', m') \<in> Traces"
   | (Print) msg k t' where "m = Print msg k" and "t = E_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
@@ -185,8 +185,10 @@ lemma bind_cong[fundef_cong]:
 
 lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits)
 lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def)
+lemma try_catch_choose_bool[simp]: "try_catch (choose_bool descr) h = choose_bool descr" by (auto simp: choose_bool_def)
+lemma liftR_choose_bool[simp]: "liftR (choose_bool descr) = choose_bool descr" by (auto simp: choose_bool_def liftR_def)
 lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def)
-lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def liftR_def)
+lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def)
 lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def)
 
 end
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 77f4ac5a..d99dfc85 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -45,6 +45,9 @@ lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()"
   by (auto simp: barrier_def)
 lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()"
   by (auto simp: footprint_def)
+lemma liftState_choose_bool[liftState_simp]: "liftState r (choose_bool descr) = choose_boolS ()"
+  by (auto simp: choose_bool_def liftState_simp)
+declare undefined_boolS_def[simp]
 lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()"
   by (auto simp: undefined_bool_def liftState_simp)
 lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
@@ -149,6 +152,14 @@ lemma liftState_foreachM[liftState_simp]:
   by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
      (auto simp: liftState_simp cong: bindS_cong)
 
+lemma liftState_genlistM[liftState_simp]:
+  "liftState r (genlistM f n) = genlistS (liftState r \<circ> f) n"
+  by (auto simp: genlistM_def genlistS_def liftState_simp cong: bindS_cong)
+
+lemma liftState_choose_bools[liftState_simp]:
+  "liftState r (choose_bools descr n) = choose_boolsS n"
+  by (auto simp: choose_bools_def choose_boolsS_def liftState_simp comp_def)
+
 lemma liftState_bools_of_bits_nondet[liftState_simp]:
   "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs"
   unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def
@@ -157,6 +168,7 @@ lemma liftState_bools_of_bits_nondet[liftState_simp]:
 lemma liftState_internal_pick[liftState_simp]:
   "liftState r (internal_pick xs) = internal_pickS xs"
   by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def
+                 chooseM_def
                  option.case_distrib[where h = "liftState r"]
            simp del: repeat.simps
            cong: option.case_cong)
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 12452ca4..ca7e5751 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -38,10 +38,9 @@ lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
 lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()"
   by (auto simp: assert_expS_def)
 
-lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (f ` xs)"
+lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (map f xs)"
   by (intro ext) (auto simp: bindS_def chooseS_def returnS_def)
 
-
 lemma result_cases:
   fixes r :: "('a, 'e) result"
   obtains (Value) a where "r = Value a"
@@ -198,9 +197,10 @@ lemma no_throw_basic_builtins[simp]:
   "\<And>f. ignore_throw (readS f) = readS f"
   "\<And>f. ignore_throw (updateS f) = updateS f"
   "ignore_throw (chooseS xs) = chooseS xs"
+  "ignore_throw (choose_boolS ()) = choose_boolS ()"
   "ignore_throw (failS msg) = failS msg"
   "ignore_throw (maybe_failS msg x) = maybe_failS msg x"
-  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def
+  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def choose_boolS_def
   by (intro ext; auto split: option.splits)+
 
 lemmas ignore_throw_option_case_distrib =
diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem
index e01cc051..3cde7ade 100644
--- a/src/gen_lib/sail2_prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -38,6 +38,11 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
+let genlistM f n =
+  let indices = genlist (fun n -> n) n in
+  foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
+
 val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
 let and_boolM l r = l >>= (fun l -> if l then r else return false)
 
@@ -55,7 +60,7 @@ val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_nondet = function
   | B0 -> return false
   | B1 -> return true
-  | BU -> undefined_bool ()
+  | BU -> choose_bool "bool_of_bitU"
 end
 
 val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
@@ -93,16 +98,25 @@ let rec untilM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then return vars else untilM vars cond body
 
-val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
-let internal_pick xs =
-  (* Use sufficiently many undefined bits and convert into an index into the list *)
-  bools_of_bits_nondet (repeat [BU] (length_list xs)) >>= fun bs ->
+val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
+let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
+
+val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
+let choose descr xs =
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_bools descr (List.length xs) >>= fun bs ->
   let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
   match index xs idx with
     | Just x -> return x
-    | Nothing -> Fail "internal_pick"
+    | Nothing -> Fail ("choose " ^ descr)
   end
 
+declare {isabelle} rename function choose = chooseM
+
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs = choose "internal_pick" xs
+
 (*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 079375a3..c6249d7a 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -29,8 +29,10 @@ type monad 'regval 'a 'e =
   | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
   (* Request to write register *)
   | Write_reg of register_name * 'regval * monad 'regval 'a 'e
-  (* Request to choose a Boolean, e.g. to resolve an undefined bit *)
-  | Undefined of (bool -> monad 'regval 'a 'e)
+  (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string
+     argument may be used to provide information to the system about what the
+     Boolean is going to be used for. *)
+  | Choose of string * (bool -> monad 'regval 'a 'e)
   (* Print debugging or tracing information *)
   | Print of string * monad 'regval 'a 'e
   (*Result of a failed assert with possible error message to report*)
@@ -48,7 +50,7 @@ type event 'regval =
   | E_footprint
   | E_read_reg of register_name * 'regval
   | E_write_reg of register_name * 'regval
-  | E_undefined of bool
+  | E_choose of string * bool
   | E_print of string
 
 type trace 'regval = list (event 'regval)
@@ -64,7 +66,7 @@ let rec bind m f = match m with
   | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> bind (k v) f)
   | Read_reg descr k ->          Read_reg descr          (fun v -> bind (k v) f)
   | Excl_res k ->                Excl_res                (fun v -> bind (k v) f)
-  | Undefined k ->               Undefined               (fun v -> bind (k v) f)
+  | Choose descr k ->            Choose descr            (fun v -> bind (k v) f)
   | Write_ea wk a sz k ->        Write_ea wk a sz        (bind k f)
   | Footprint k ->               Footprint               (bind k f)
   | Barrier bk k ->              Barrier bk              (bind k f)
@@ -77,8 +79,11 @@ end
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
 let exit () = Fail "exit"
 
+val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e
+let choose_bool descr = Choose descr return
+
 val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
-let undefined_bool () = Undefined return
+let undefined_bool () = choose_bool "undefined_bool"
 
 val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
 let assert_exp exp msg = if exp then Done () else Fail msg
@@ -94,7 +99,7 @@ let rec try_catch m h = match m with
   | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> try_catch (k v) h)
   | Read_reg descr k ->          Read_reg descr          (fun v -> try_catch (k v) h)
   | Excl_res k ->                Excl_res                (fun v -> try_catch (k v) h)
-  | Undefined k ->               Undefined               (fun v -> try_catch (k v) h)
+  | Choose descr k ->            Choose descr            (fun v -> try_catch (k v) h)
   | Write_ea wk a sz k ->        Write_ea wk a sz        (try_catch k h)
   | Footprint k ->               Footprint               (try_catch k h)
   | Barrier bk k ->              Barrier bk              (try_catch k h)
@@ -267,7 +272,7 @@ let emitEvent m e = match (e, m) with
   | (E_print m, Print m' k) ->
      if m' = m then Just k else Nothing
   | (E_excl_res v, Excl_res k) -> Just (k v)
-  | (E_undefined v, Undefined k) -> Just (k v)
+  | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing
   | (E_footprint, Footprint k) -> Just k
   | _ -> Nothing
 end
diff --git a/src/gen_lib/sail2_state.lem b/src/gen_lib/sail2_state.lem
index f703dead..ec787764 100644
--- a/src/gen_lib/sail2_state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -28,6 +28,11 @@ end
 
 declare {isabelle} termination_argument foreachS = automatic
 
+val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e
+let genlistS f n =
+  let indices = genlist (fun n -> n) 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
 let and_boolS l r = l >>$= (fun l -> if l then r else returnS false)
 
@@ -84,12 +89,17 @@ let rec untilS vars cond body 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
+let choose_boolsS n = genlistS (fun _ -> choose_boolS ()) 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
 let internal_pickS xs =
-  (* Use sufficiently many undefined bits and convert into an index into the list *)
-  bools_of_bits_nondetS (repeat [BU] (length_list xs)) >>$= fun bs ->
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_boolsS (List.length xs) >>$= fun bs ->
   let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
   match index xs idx with
     | Just x -> returnS x
-    | Nothing -> failS "internal_pick"
+    | Nothing -> failS "choose internal_pick"
   end
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 07a6215b..c227e89b 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -14,7 +14,7 @@ let rec liftState ra m = match m with
   | (Write_mem wk a sz v t k)   -> bindS (write_mem_bytesS wk a sz v t)   (fun v -> liftState ra (k v))
   | (Read_reg r k)              -> bindS (read_regvalS ra r)              (fun v -> liftState ra (k v))
   | (Excl_res k)                -> bindS (excl_resultS ())                (fun v -> liftState ra (k v))
-  | (Undefined k)               -> bindS (undefined_boolS ())             (fun v -> liftState ra (k v))
+  | (Choose _ k)                -> bindS (choose_boolS ())                (fun v -> liftState ra (k v))
   | (Write_reg r v k)           -> seqS (write_regvalS ra r v)            (liftState ra k)
   | (Write_ea _ _ _ k)          -> liftState ra k
   | (Footprint k)               -> liftState ra k
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 8626052f..b2a7bb31 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -47,8 +47,8 @@ let seqS m n = bindS m (fun (_ : unit) -> n)
 let inline (>>$=) = bindS
 let inline (>>$) = seqS
 
-val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.map (fun x -> (Value x, s)) xs
+val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = Set.fromList (List.map (fun x -> (Value x, s)) xs)
 
 val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
 let readS f = (fun s -> returnS (f s) s)
@@ -59,8 +59,9 @@ let updateS f = (fun s -> returnS () (f s))
 val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = {(Ex (Failure msg), s)}
 
-val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () = chooseS {false; true}
+val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
+let choose_boolS () = chooseS [false; true]
+let undefined_boolS = choose_boolS
 
 val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
 let exitS () = failS "exit"