Merge branch 'cheri-mono' into sail2

5 files changed, 89 insertions, 40 deletions

diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index 9eb59319..87c9af39 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -212,3 +212,10 @@ let barrier bk = Barrier bk (Done ())
 
 val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
 let footprint _ = Footprint (Done ())
+
+(* Define a type synonym that also takes the register state as a type parameter,
+   in order to make switching to the state monad without changing generated
+   definitions easier, see also lib/hol/prompt_monad.lem. *)
+
+type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e
+type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 5c6dc593..a709a8c1 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -85,7 +85,7 @@ let rec replace bs (n : integer) b' = match bs with
      if n = 0 then b' :: bs
               else b :: replace bs (n - 1) b'
   end
-declare {isabelle} termination_argument replace = automatic
+declare {isabelle; hol} termination_argument replace = automatic
 
 let upper n = n
 
@@ -128,7 +128,7 @@ let rec just_list l = match l with
       | (_, _) -> Nothing
     end
   end
-declare {isabelle} termination_argument just_list = automatic
+declare {isabelle; hol} termination_argument just_list = automatic
 
 lemma just_list_spec:
   ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) &&
@@ -267,7 +267,7 @@ let rec nat_of_bools_aux acc bs = match bs with
   | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs
   | false :: bs -> nat_of_bools_aux (2 * acc) bs
 end
-declare {isabelle} termination_argument nat_of_bools_aux = automatic
+declare {isabelle; hol} termination_argument nat_of_bools_aux = automatic
 let nat_of_bools bs = nat_of_bools_aux 0 bs
 
 val unsigned_of_bools : list bool -> integer
@@ -306,7 +306,7 @@ let rec add_one_bool_ignore_overflow_aux bits = match bits with
   | false :: bits -> true :: bits
   | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits
 end
-declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic
+declare {isabelle; hol} termination_argument add_one_bool_ignore_overflow_aux = automatic
 
 let add_one_bool_ignore_overflow bits =
   List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits))
@@ -369,7 +369,7 @@ let rec add_one_bit_ignore_overflow_aux bits = match bits with
   | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
   | BU :: bits -> BU :: List.map (fun _ -> BU) bits
 end
-declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic
+declare {isabelle; hol} termination_argument add_one_bit_ignore_overflow_aux = automatic
 
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
@@ -417,7 +417,7 @@ let rec hexstring_of_bits bs = match bs with
   | [] -> Just []
   | _ -> Nothing
   end
-declare {isabelle} termination_argument hexstring_of_bits = automatic
+declare {isabelle; hol} termination_argument hexstring_of_bits = automatic
 
 let show_bitlist bs =
   match hexstring_of_bits bs with
@@ -630,7 +630,7 @@ let rec byte_chunks bs = match bs with
      Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest))
   | _ -> Nothing
 end
-declare {isabelle} termination_argument byte_chunks = automatic
+declare {isabelle; hol} termination_argument byte_chunks = automatic
 
 val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte)
 let bytes_of_bits bs = byte_chunks (bits_of bs)
@@ -854,7 +854,7 @@ let rec foreach l vars body =
     | (x :: xs) -> foreach xs (body x vars) body
   end
 
-declare {isabelle} termination_argument foreach = automatic
+declare {isabelle; hol} termination_argument foreach = automatic
 
 val index_list : integer -> integer -> integer -> list integer
 let rec index_list from to step =
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 61477258..f69f59c1 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,33 +1,8 @@
 open import Pervasives_extra
-(*open import Sail_impl_base*)
 open import Sail_values
-open import Prompt_monad
-open import Prompt
 open import State_monad
 open import {isabelle} `State_monad_lemmas`
 
-(* State monad wrapper around prompt monad *)
-
-val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
-  | (Done a)             -> returnS a
-  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
-  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
-  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
-  | (Write_tag a t k)    -> bindS (write_tagS a 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))
-  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
-  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
-  | (Footprint k)        -> liftState ra k
-  | (Barrier _ k)        -> liftState ra k
-  | (Print _ k)          -> liftState ra k (* TODO *)
-  | (Fail descr)         -> failS descr
-  | (Exception e)        -> throwS e
-end
-
-
 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
@@ -53,6 +28,46 @@ end
 
 declare {isabelle} termination_argument foreachS = automatic
 
+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)
+
+val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
+let or_boolS l r = l >>$= (fun l -> if l then returnS true else r)
+
+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
diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/state_lifting.lem
new file mode 100644
index 00000000..7e569a7e
--- /dev/null
+++ b/src/gen_lib/state_lifting.lem
@@ -0,0 +1,27 @@
+open import Pervasives_extra
+open import Sail_values
+open import Prompt_monad
+open import Prompt
+open import State_monad
+open import {isabelle} `State_monad_lemmas`
+
+(* State monad wrapper around prompt monad *)
+
+val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
+let rec liftState ra s = match s with
+  | (Done a)             -> returnS a
+  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
+  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
+  | (Write_tag a t k)    -> bindS (write_tagS a 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))
+  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
+  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
+  | (Footprint k)        -> liftState ra k
+  | (Barrier _ k)        -> liftState ra k
+  | (Print _ k)          -> liftState ra k (* TODO *)
+  | (Fail descr)         -> failS descr
+  | (Exception e)        -> throwS e
+end
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index a2919762..89021890 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg
 (* For early return, we abuse exceptions by throwing and catching
    the return value. The exception type is "either 'r 'e", where "Right e"
    represents a proper exception and "Left r" an early return of value "r". *)
-type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
 
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
+val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
 let early_returnS r = throwS (Left r)
 
-val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
+val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
 let catch_early_returnS m =
   try_catchS m
     (function
@@ -108,12 +108,12 @@ let catch_early_returnS m =
      end)
 
 (* Lift to monad with early return by wrapping exceptions *)
-val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
-let liftSR m = try_catchS m (fun e -> throwS (Right e))
+val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
+let liftRS m = try_catchS m (fun e -> throwS (Right e))
 
 (* Catch exceptions in the presence of early returns *)
-val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) ->  monadSR 'regs 'a 'r 'e2
-let try_catchSR m h =
+val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) ->  monadRS 'regs 'a 'r 'e2
+let try_catchRS m h =
   try_catchS m
     (function
       | Left r -> throwS (Left r)