Add support for undefined bit oracle to Lem shallow embedding

Add an Undefined outcome to the prompt monad that asks the environment for a
Boolean value.  For the state monad, add fields for a random generator and a
seed (currently of type nat) to the state.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 9642c714..1d8623df 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -30,6 +30,19 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val bool_of_bitU_undef : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let bool_of_bitU_undef = function
+  | B0 -> return false
+  | B1 -> return true
+  | BU -> undefined_bool ()
+end
+
+val bools_of_bitUs : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
+let bools_of_bitUs bits =
+  foreachM bits []
+    (fun b bools ->
+      bool_of_bitU_undef b >>= (fun b ->
+      return (bools ++ [b])))
 
 val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e