1 files changed, 149 insertions, 37 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 426b0811..e9684414 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,10 +2,13 @@ open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
 
-val return : forall 'a. 'a -> outcome 'a
+type MR 'a 'r = outcome_r 'a 'r
+type M 'a = outcome 'a
+
+val return : forall 'a 'r. 'a -> MR 'a 'r
 let return a = Done a
 
-val bind : forall 'a 'b. outcome 'a -> ('a -> outcome 'b) -> outcome 'b
+val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r
 let rec bind m f = match m with
   | Done a ->              f a
   | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
@@ -19,25 +22,65 @@ let rec bind m f = match m with
   | Escape descr ->        Escape descr
   | Fail descr ->          Fail descr
   | Error descr ->         Error descr
+  | Return a ->            Return a
   | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
 end
 
-
-type M 'a = outcome 'a
-
 let inline (>>=) = bind
-val (>>) : forall 'b. M unit -> M 'b -> M 'b
+val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r
 let inline (>>) m n = m >>= fun _ -> n
 
 val exit : forall 'a 'b. 'b -> M 'a
 let exit s = Fail Nothing
 
-val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+val assert_exp : bool -> string -> M unit
+let assert_exp exp msg = if exp then Done () else Fail (Just msg)
+
+val early_return : forall 'r. 'r -> MR unit 'r
+let early_return r = Return r
+
+val liftR : forall 'a 'r. M 'a -> MR 'a 'r
+let rec liftR m = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (liftR o,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (liftR o,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (liftR o,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (liftR o,opt))
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (liftR o,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Return _ ->            Error "uncaught early return"
+end
+
+val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
+let rec catch_early_return m = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Return a ->            Done a
+end
+
+val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b
 let read_mem dir rk addr sz =
-  let addr = address_lifted_of_bitv addr in
+  let addr = address_lifted_of_bitv (bits_of addr) in
   let sz = natFromInteger sz in
   let k memory_value =
-    let bitv = internal_mem_value dir memory_value in
+    let bitv = of_bits (internal_mem_value dir memory_value) in
     (Done bitv,Nothing) in
   Read_mem (rk,addr,sz) k
 
@@ -46,22 +89,22 @@ let excl_result () =
   let k successful = (return successful,Nothing) in
   Excl_res k
 
-val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
+val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit
 let write_mem_ea wk addr sz =
-  let addr = address_lifted_of_bitv addr in
+  let addr = address_lifted_of_bitv (bits_of addr) in
   let sz = natFromInteger sz in
   Write_ea (wk,addr,sz) (Done (),Nothing)
 
-val write_mem_val : vector bitU -> M bool
+val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool
 let write_mem_val v =
-  let v = external_mem_value v in
+  let v = external_mem_value (bits_of v) in
   let k successful = (return successful,Nothing) in
   Write_memv v k
 
-val read_reg_aux : reg_name -> M (vector bitU)
+val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a
 let read_reg_aux reg = 
   let k reg_value =
-    let v = internal_reg_value reg_value in
+    let v = of_bits (internal_reg_value reg_value) in
     (Done v,Nothing) in
   Read_reg reg k
 
@@ -71,34 +114,40 @@ let read_reg_range reg i j =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
 let read_reg_bit reg i =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
-  return (extract_only_bit v)
+  return (extract_only_element v)
 let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield)
+  read_reg_aux (external_reg_field_whole reg regfield.field_name)
 let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
-  return (extract_only_bit v)
+  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
+  return (extract_only_element v)
 
-val write_reg_aux : reg_name -> vector bitU -> M unit
+let reg_deref = read_reg
+
+val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit
 let write_reg_aux reg_name v =
-  let regval = external_reg_value reg_name v in
+  let regval = external_reg_value reg_name (bits_of v) in
   Write_reg (reg_name,regval) (Done (), Nothing)
 
 let write_reg reg v =
   write_reg_aux (external_reg_whole reg) v
 let write_reg_range reg i j v =
   write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
-let write_reg_bit reg i bit =
+let write_reg_pos reg i v =
   let iN = natFromInteger i in
-  write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
+  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
+let write_reg_bit = write_reg_pos
 let write_reg_field reg regfield v =
-  write_reg_aux (external_reg_field_whole reg regfield) v
-let write_reg_bitfield reg regfield bit =
-  write_reg_aux (external_reg_field_whole reg regfield)
-                (Vector [bit] 0 (is_inc_of_reg reg))
+  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
+(*let write_reg_field_bit reg regfield bit =
+  write_reg_aux (external_reg_field_whole reg regfield.field_name)
+                (Vector [bit] 0 (is_inc_of_reg reg))*)
 let write_reg_field_range reg regfield i j v =
-  write_reg_aux (external_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
-
+  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
+let write_reg_field_pos reg regfield i v =
+  write_reg_field_range reg regfield i i [v]
+let write_reg_field_bit = write_reg_field_pos
 
+let write_reg_ref (reg, v) = write_reg reg v
 
 val barrier : barrier_kind -> M unit
 let barrier bk = Barrier bk (Done (), Nothing)
@@ -108,26 +157,89 @@ val footprint : M unit
 let footprint = Footprint (Done (),Nothing)
 
 
-val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
+let rec iter_aux i f xs = match xs with
+  | x :: xs -> f i x >> iter_aux (i + 1) f xs
+  | [] -> return ()
+  end
+
+val iteri : forall 'regs 'e 'a. (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
+let iteri f xs = iter_aux 0 f xs
+
+val iter : forall 'regs 'e 'a. ('a -> MR unit 'e) -> list 'a -> MR unit 'e
+let iter f xs = iteri (fun _ x -> f x) xs
+
+
+val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_inc (i,stop,by) vars body =
-  if i <= stop
+  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then
     body i vars >>= fun vars ->
     foreachM_inc (i + by,stop,by) vars body
   else return vars
 
 
-val foreachM_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_dec (i,stop,by) vars body =
-  if i >= stop
+  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then
     body i vars >>= fun vars ->
     foreachM_dec (i - by,stop,by) vars body
   else return vars
 
-let write_two_regs r1 r2 vec =
+val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec while_PP vars cond body =
+  if cond vars then while_PP (body vars) cond body else vars
+
+val while_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
+                ('vars -> MR 'vars 'r) -> MR 'vars 'r
+let rec while_PM vars cond body =
+  if cond vars then
+    body vars >>= fun vars -> while_PM vars cond body
+  else return vars
+
+val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
+                ('vars -> 'vars) -> MR 'vars 'r
+let rec while_MP vars cond body =
+  cond vars >>= fun cond_val ->
+  if cond_val then while_MP (body vars) cond body else return vars
+
+val while_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
+                ('vars -> MR 'vars 'r) -> MR 'vars 'r
+let rec while_MM vars cond body =
+  cond vars >>= fun cond_val ->
+  if cond_val then
+    body vars >>= fun vars -> while_MM vars cond body
+  else return vars
+
+val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec until_PP vars cond body =
+  let vars = body vars in
+  if (cond vars) then vars else until_PP (body vars) cond body
+
+val until_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
+                ('vars -> MR 'vars 'r) -> MR 'vars 'r
+let rec until_PM vars cond body =
+  body vars >>= fun vars ->
+  if (cond vars) then return vars else until_PM vars cond body
+
+val until_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
+                ('vars -> 'vars) -> MR 'vars 'r
+let rec until_MP vars cond body =
+  let vars = body vars in
+  cond vars >>= fun cond_val ->
+  if cond_val then return vars else until_MP vars cond body
+
+val until_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
+                ('vars -> MR 'vars 'r) -> MR 'vars 'r
+let rec until_MM vars cond body =
+  body vars >>= fun vars ->
+  cond vars >>= fun cond_val ->
+  if cond_val then return vars else until_MM vars cond body
+
+(*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
     let is_inc_r2 = is_inc_of_reg r2 in
@@ -146,4 +258,4 @@ let write_two_regs r1 r2 vec =
     if is_inc
     then slice vec (size_r1 - start_vec) (size_vec - start_vec)
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
-  write_reg r1 r1_v >> write_reg r2 r2_v
+  write_reg r1 r1_v >> write_reg r2 r2_v*)