Add support for actions that read just a slice or single bit of a register

3 files changed, 36 insertions, 18 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8ce1c354..f9a64da1 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1,8 +1,8 @@
 open import Pervasives
 import Map
-import Map_extra
-import List_extra
-open import String_extra
+import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
+import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
+open import String_extra (* for 'show' to convert nat to string) *)
 
 open import Interp_ast
 
@@ -100,7 +100,7 @@ instance (Eq value)
   let (<>) n1 n2 = not (value_eq n1 n2)
 end
 
-(*Constant unit value, for frequent uses in interpreter *)
+(*Constant unit value, for use in interpreter *)
 let unitv = V_lit (L_aux L_unit Unknown)
 
 (* Store for local memory of ref cells *)
@@ -448,7 +448,7 @@ let add_to_top_frame e_builder stack =
 
 let top_hole stack : bool =
   match stack with
-  | Hole_frame _ (E_aux (E_id (Id_aux (Id "1") _)) _) _ _ _ _ -> true
+  | Hole_frame _ (E_aux (E_id (Id_aux (Id "0") _)) _) _ _ _ Top -> true
   | _ -> false
 end
 
@@ -1108,7 +1108,6 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                               | Nothing -> Error l "Internal error, unrecognized read, no reg" end
                           | _ -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))) end)
     | E_vector_access vec i ->
-      (*Need to update to read one position of a register*)
       resolve_outcome (interp_main mode t_level l_env l_mem i)
                       (fun iv lm le -> 
                         match iv with
@@ -1120,13 +1119,19 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 					    | V_vector_sparse _ _ _ _ _ -> (Value (access_vector vvec n) Tag_empty,lm,le)
 					    | V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                             | _ -> (Error l "Vector access of non-vector",lm,le)end)
-                                          (fun a -> update_stack a 
-					    (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))))
+                                          (fun a ->
+                                            match a with
+                                            | Action (Read_reg reg Nothing) stack -> 
+                                              if (top_hole stack) 
+                                              then Action (Read_reg reg (Just(n,n))) stack 
+                                              else Action (Read_reg reg Nothing) (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot))) stack)
+                                            | _ -> 
+                                              update_stack a 
+					        (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))) end)
 			| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                         | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
                       (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) (l,annot))))
     | E_vector_subrange vec i1 i2 ->
-      (*Need to update to read a slice of a register*)
       resolve_outcome (interp_main mode t_level l_env l_mem i1)
                       (fun i1v lm le ->
                         match i1v with
@@ -1142,12 +1147,21 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 								| V_vector_sparse _ _ _ _ _ -> (Value (slice_vector vvec n1 n2) Tag_empty, lm,le)
 								| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                                                 | _ -> (Error l "Vector slice of non-vector",lm,le)end)
-                                                              (fun a -> update_stack a 
-                                                                (add_to_top_frame 
-								   (fun v -> (E_aux (E_vector_subrange v 
-										       (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
-										       (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
-										(l,annot)))))
+                                                              (fun a -> 
+                                                                match a with 
+                                                                | Action (Read_reg reg Nothing) stack ->
+                                                                  if (top_hole stack)
+                                                                  then Action (Read_reg reg (Just(n1,n2))) stack
+                                                                  else Action (Read_reg reg Nothing) (add_to_top_frame (fun v -> (E_aux (E_vector_subrange v
+                                                                                                                                           (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+                                                                                                                                           (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+                                                                                                                                        (l,annot))) stack)
+                                                                | _ -> update_stack a 
+                                                                  (add_to_top_frame 
+								     (fun v -> (E_aux (E_vector_subrange v 
+										         (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+										         (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+										  (l,annot)))) end)
 					    | V_unknown -> (Value V_unknown Tag_empty, lm,le)
                                             | _ -> (Error l "vector slice given non number for last index",lm,le) end)
                                           (fun a -> update_stack a 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 13aa728f..c4087edb 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -1,7 +1,7 @@
 open import Pervasives
 open import Interp
 open import Interp_ast
-import Assert_extra Maybe_extra
+import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
 open import Num
 open import List
 open import Word
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 18863ce2..1ca615c5 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -19,7 +19,7 @@ let ( bit [32] ) v2 = 0xABCDEF01
 val forall Type 'a. 'a -> 'a effect pure identity
 function forall Type 'a. 'a identity i = i
 
-function unit ignore(x) = ()
+(*function unit ignore(x) = ()*)
 
 (* scattered function definition and union definition *)
 scattered typedef ast = const union
@@ -41,5 +41,9 @@ function unit a (bit) b = if identity(b) then (identity()) else ()
 
 function bit sw s = switch s { case 0 -> bitzero }
 
-function bit main _ = {ignore(sw(0)); ignore((nat) v2); v1[0] }
+let colors rgb = red
+
+function bit enu (red) = 0
+
+function bit main _ = {ignore(sw(0)); ignore((nat) v2); ignore(enu(0)); v1[0] }