Remove work-around from interpreter, move it to power.sail

Two bugs are worked-around here:
- missing cast to nat when a vector is wrapped in exts
  (exts is a no-op currently anyway, so we are discarding it)
- missing cast (due to limited type-inference) in one if branch:
  type given explicitly.

3 files changed, 5 insertions, 38 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index b5e94a42..9b3ba3b0 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -44,33 +44,7 @@ let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
   V_vector 0 false (map bool_to_bit l) ;;
 
 let rec add (V_tuple args) = match args with
-  (* vector case *)
-  | [(V_vector _ d l as v); (V_vector _ d' l' as v')] ->
-      let (V_lit (L_aux (L_num x) lx)) = (if d then to_num_inc else to_num_dec) v in
-      let (V_lit (L_aux (L_num y) ly)) = (if d' then to_num_inc else to_num_dec) v' in
-      (* XXX how shall I decide this? max? max+1? *)
-      let len = max (List.length l) (List.length l') in
-      (* XXX assume d = d' *)
-      V_lit (L_aux (L_num (x+y)) lx)
-  (* integer case *)
   | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
-  | [(V_lit(L_aux (L_num _) _) as n); (V_vector _ d l as v)] ->
-      let len = List.length l in
-      add (V_tuple [(if d then to_vec_inc else to_vec_dec) len n; v])
-  | [(V_vector _ d l as v); (V_lit(L_aux (L_num _) _) as n)] ->
-      let len = List.length l in
-      add (V_tuple [v; (if d then to_vec_inc else to_vec_dec) len n])
-  (* assume other literals are L_bin or L_hex, ie. vectors *)
-  | [(V_lit (L_aux L_zero _) as l); x] ->
-      add (V_tuple [V_vector 0 true [l]; x])
-  | [(V_lit (L_aux L_one _) as l); x] ->
-      add (V_tuple [V_vector 0 true [l]; x])
-  | [x; (V_lit (L_aux L_zero _) as l)] ->
-      add (V_tuple [x; V_vector 0 true [l]])
-  | [x; (V_lit (L_aux L_one _) as l)] ->
-      add (V_tuple [x; V_vector 0 true [l]])
-  | [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
-  | [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
   end ;;
 
 let rec vec_concat (V_tuple args) = match args with
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 8e495df4..8ae6d1ee 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -196,11 +196,6 @@ let rec perform_action ((reg, mem) as env) = function
      perform_action env (Write_reg (r, slice, V_vector(zero_big_int, true, [value])))
  | Write_mem (id, (V_lit(L_aux(L_num _,_)) as n), (Some (start, stop) as slice), value) when eq_big_int start stop ->
      perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
- (* XXX work-around missing cast *)
- | Write_mem (id, V_tuple (((V_vector (m, true, vs)) as v) :: l), sub, value) ->
-    perform_action env (Write_mem (id, V_tuple ((to_num_inc v) :: l), sub, value))
- | Read_mem (id, V_tuple (((V_vector (m, true, vs)) as v) :: l), sub) ->
-    perform_action env (Read_mem (id, V_tuple ((to_num_inc v) :: l), sub))
  (* extern functions *)
  | Call_extern (name, arg) -> eval_external name arg, env
  | _ -> assert false
diff --git a/src/test/power.sail b/src/test/power.sail
index 07b74c60..dc774f1d 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -1,7 +1,4 @@
 
-(* XXX sign extension *)
-function forall Type 'a . 'a exts ( x ) = x
-
 register (vector <0, 63, inc, bit>) GPR0
 register (vector <0, 63, inc, bit>) GPR1
 register (vector <0, 63, inc, bit>) GPR2
@@ -50,7 +47,7 @@ scattered function ast decode
 
  function clause execute (  AddImmediate  (  RA, RT, SI  )  ) =
   {
-    if  (  RA  ==  0  )  then  GPR[  RT  ]  :=  (  exts  (  SI  ))  else  GPR[  RT  ]  :=  (  (GPR[  RA  ])  +  (  exts  (  SI  ))  )  ;
+    if  (  RA  ==  0  )  then  GPR[  RT  ]  :=  (  (  SI  ))  else  GPR[  RT  ]  :=  (  (GPR[  RA  ])  +  (  (  SI  ))  )  ;
   } 
 
  union ast member  bit [ 1 ] (* BH *) * bit [ 4 ] (* BI *) * bit [ 4 ] (* BO *) * bit (* LK *)  BranchConditionaltoLinkRegister 
@@ -77,7 +74,7 @@ scattered function ast decode
  function clause execute (  LoadWordandZero  (  D, RA, RT  )  ) =
   {
     if  (  RA  ==  0  )  then  b  :=  0  else  b  :=  (GPR[  RA  ])  ;
-    EA  :=  (  b  +  (  exts  (  D  ))  )  ;
+    EA  :=  (  b  +  (  (  D  ))  )  ;
     GPR[  RT  ]  :=  (  0b00000000000000000000000000000000  :  MEM(  EA  ,   4  )  )  ;
   } 
 
@@ -96,8 +93,9 @@ scattered function ast decode
 
  function clause execute (  StoreWord  (  D, RA, RS  )  ) =
   {
+    (bit[64]) b := 0;
     if  (  RA  ==  0  )  then  b  :=  0  else  b  :=  (GPR[  RA  ])  ;
-    EA  :=  (  b  +  (  exts  (  D  ))  )  ;
+    EA  :=  (  b  +  (  (  D  ))  )  ;
     MEM(  EA  ,   4  )  :=  ((  (GPR[  RS  ])  )[  32  ..  63  ])  ;
   } 
 
@@ -108,7 +106,7 @@ scattered function ast decode
 
  function clause execute (  StoreWordwithUpdate  (  D, RA, RS  )  ) =
   {
-    EA  :=  (  (GPR[  RA  ])  +  (  exts  (  D  ))  )  ;
+    EA  :=  (  (GPR[  RA  ])  +  (  (  D  ))  )  ;
     MEM(  EA  ,   4  )  :=  ((  (GPR[  RS  ])  )[  32  ..  63  ])  ;
     GPR[  RA  ]  :=  EA  ;
   }