Make partiality more explicit in library functions of Lem shallow embedding

Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits.  Undefined
cases can be handled in different ways:

- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
  default so far),
- return an option type,
- raise a failure  in the monad, or
- use a bitstream oracle to resolve undefined bits.

This patch adds different versions of partial functions corresponding to those
options.  The desired behaviour can be selected by choosing a binding in the
Sail prelude.  The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.

1 files changed, 20 insertions, 5 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 1d8623df..8cef266e 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -30,20 +30,35 @@ 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
+val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let bool_of_bitU_fail = function
+  | B0 -> return false
+  | B1 -> return true
+  | BU -> Fail "bool_of_bitU"
+end
+
+val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let bool_of_bitU_oracle = 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 =
+val bools_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
+let bools_of_bits_oracle bits =
   foreachM bits []
     (fun b bools ->
-      bool_of_bitU_undef b >>= (fun b ->
+      bool_of_bitU_oracle b >>= (fun b ->
       return (bools ++ [b])))
 
+val of_bits_oracle : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
+let of_bits_oracle bits =
+  bools_of_bits_oracle bits >>= (fun bs ->
+  return (of_bools bs))
+
+val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
+let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits)
+
 val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec whileM vars cond body =