rewriting fixes, syntactically correct lem syntax, number type errors remaining

3 files changed, 118 insertions, 43 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index a51a0091..00b3e3ab 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -9,22 +9,22 @@ let to_bool = function
 (*  | BU -> assert false *)
   end
 
-let get_elements (Vector elements _) = elements
 let get_start (Vector _ s) = s
 let length (Vector bs _) = length bs
 
-(*
-let write_two_registers r1 r2 vec =
-  let size = length_register r1 in
+let write_two_regs r1 r2 vec =
+  let size = length_reg r1 in
   let start = get_start vec in
   let vsize = length vec in
-  let r1_v = read_vector_subrange is_inc vec start ((if is_inc then size - start else start - size) - 1) in
+  let r1_v =
+    (slice vec)
+      start
+      ((if is_inc then size - start else start - size) - 1) in
   let r2_v =
-    read_vector_subrange is_inc
-      vec (if is_inc then size - start else start - size)
+    (slice vec)
+      (if is_inc then size - start else start - size)
       (if is_inc then vsize - start else start - vsize) in
-  write_register r1 r1_v >> write_register r2 r2_v
- *)
+  write_reg r1 r1_v >> write_reg r2 r2_v
 
 let rec replace bs ((n : nat),b') = match (n,bs) with
   | (_, []) -> []
@@ -269,15 +269,15 @@ let shift_op_vec op (((Vector bs start) as l),r) =
     match op with
      | LL (*"<<"*) ->
        let right_vec = Vector (List.replicate n B0) 0 in
-       let left_vec = read_vector_subrange is_inc l n (if is_inc then len + start else start - len) in
+       let left_vec = slice l n (if is_inc then len + start else start - len) in
        vector_concat left_vec right_vec
      | RR (*">>"*) ->
-       let right_vec = read_vector_subrange is_inc l start n in
+       let right_vec = slice l start n in
        let left_vec = Vector (List.replicate n B0) 0 in
        vector_concat left_vec right_vec 
      | LLL (*"<<<"*) ->
-       let left_vec = read_vector_subrange is_inc l n (if is_inc then len + start else start - len) in
-       let right_vec = read_vector_subrange is_inc l start n in
+       let left_vec = slice l n (if is_inc then len + start else start - len) in
+       let right_vec = slice l start n in
        vector_concat left_vec right_vec
      end
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index f9404416..268077da 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,4 +1,6 @@
 open import Pervasives
+open import Vector
+open import Arch
 
 type M 's 'a = 's -> ('a * 's)
 
@@ -11,18 +13,111 @@ let bind m f s = let (a,s') = m s in f a s'
 let (>>=) = bind
 let (>>) m n = m >>= fun _ -> n
 
+val foreach_inc : forall 's 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_inc (i,stop,by) vars body = 
+  if i <= stop
+  then
+    let (_,vars) = body i vars in
+    foreach_inc (i + by,stop,by) vars body
+  else ((),vars)
+
+
+val foreach_dec : forall 's 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_dec (i,stop,by) vars body = 
+  if i >= stop
+  then
+    let (_,vars) = body i vars in
+    foreach_dec (i - by,stop,by) vars body
+  else ((),vars)
+
 
-val foreach_inc : forall 's 'vars. (nat * nat * nat) -> (nat -> 'vars -> M 's 'vars) ->
-                  'vars -> M 's 'vars
-let rec foreach_inc (i,stop,by) body vars = 
+val foreachM_inc : forall 's 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M 's (unit * 'vars)) -> M 's (unit * 'vars)
+let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
-  then (body i vars >>= fun vars -> foreach_inc (i + by,stop,by) body vars)
-  else return vars
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_inc (i + by,stop,by) vars body
+  else return ((),vars)
 
 
-val foreach_dec : forall 's 'vars. (nat * nat * nat) -> (nat -> 'vars -> M 's 'vars) ->
-                  'vars -> M 's 'vars
-let rec foreach_dec (i,stop,by) body vars = 
+val foreachM_dec : forall 's 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M 's (unit * 'vars)) -> M 's (unit * 'vars)
+let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
-  then (body i vars >>= fun vars -> foreach_dec (i - by,stop,by) body vars)
-  else return vars
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_dec (i - by,stop,by) vars body
+  else return ((),vars)
+
+
+
+let slice (Vector bs start) n m =
+  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+  let (_,suffix) = List.splitAt offset bs in
+  let (subvector,_) = List.splitAt length suffix in
+  Vector subvector n
+
+let update (Vector bs start) n m (Vector bs' _) =
+  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+  let (prefix,_) = List.splitAt offset bs in
+  let (_,suffix) = List.splitAt (offset + length) bs in
+  Vector (prefix ++ (List.take length bs') ++ suffix) start
+
+let hd (x :: _) = x
+
+val access : forall 'a. vector 'a -> nat -> 'a
+let access (Vector bs start) n =
+  if is_inc then nth bs (n - start) else nth bs (start - n)
+
+val update_pos : forall 'a. vector 'a -> nat -> 'a -> vector 'a
+let update_pos v n b =
+  update v n n (Vector [b] 0)
+
+val read_reg_range : register -> (nat * nat) -> M state (vector bit)
+let read_reg_range reg (i,j) s =
+  let v = slice (read_regstate s reg) i j in
+  (v,s)
+
+val read_reg_bit : register -> nat -> M state bit
+let read_reg_bit reg i s =
+  let v = access (read_regstate s reg) i in
+  (v,s)
+
+val write_reg_range : register -> (nat * nat) -> vector bit -> M state unit
+let write_reg_range (reg : register) (i,j) (v : vector bit) s =
+  let v' = update (read_regstate s reg) i j v in
+  let s' = write_regstate s reg v' in
+  ((),s')
+
+val write_reg_bit : register -> nat -> bit -> M state unit
+let write_reg_bit reg i bit s =
+  let v = read_regstate s reg in
+  let v' = update_pos v i bit in
+  let s' = write_regstate s reg v' in
+  ((),s')
+  
+
+val read_reg : register -> M state (vector bit)
+let read_reg reg s =
+  let v = read_regstate s reg in
+  (v,s)
+
+val write_reg : register -> vector bit -> M state unit
+let write_reg reg v s =
+  let s' = write_regstate s reg v in
+  ((),s')
+
+val read_reg_field : register -> register_field -> M state (vector bit)
+let read_reg_field reg rfield = read_reg_range reg (field_indices rfield)
+
+val write_reg_field : register -> register_field -> vector bit -> M state unit
+let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+
+val read_reg_field_bit : register -> register_field_bit -> M state bit
+let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)
+
+val write_reg_field_bit : register -> register_field_bit -> bit -> M state unit
+let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit)
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index d5f47492..5f239e37 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -7,23 +7,3 @@ let rec nth xs (n : nat) = match (n,xs) with
   | (0,x :: xs) -> x
   | (n + 1,x :: xs) -> nth xs n
 end
-
-let vector_access is_inc (Vector bs start) n =
-  if is_inc then nth bs (n - start) else nth bs (start - n)
-
-let read_vector_subrange is_inc (Vector bs start) n m =
-  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-  let (_,suffix) = List.splitAt offset bs in
-  let (subvector,_) = List.splitAt length suffix in
-  Vector subvector n
-
-let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) =
-  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-  let (prefix,_) = List.splitAt offset bs in
-  let (_,suffix) = List.splitAt (offset + length) bs in
-  Vector (prefix ++ (List.take length bs') ++ suffix) start
-
-let write_vector_bit is_inc v n (Vector [b] 0) =
-  write_vector_subrange is_inc v n n b
-
-let hd (x :: xs) = x