First bit of Power spec

Only chapter about branches (except system calls because of sail
typechecking issue).  Decoding seems to work. Execution typechecks
currently, but is pretty surely broken otherwise.

3 files changed, 10 insertions, 1 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 4873149e..4cda3316 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -2,12 +2,20 @@ open import Interp
 open import Interp_ast
 import Maybe_extra
 open import Num
+open import List
 
 let add (V_tuple [V_lit(L_num x); V_lit(L_num y)]) = V_lit(L_num (x+y)) ;;
 
+let rec vec_concat (V_tuple args) = match args with
+  | [V_vector 0 true l; V_vector 0 true l'] -> V_vector 0 true (l ++ l')
+  | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l; x])
+  | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l])
+  end;;
+
 let function_map = [
   ("add", add);
   ("add_infix", add);
+  (":", vec_concat);
 ] ;;
 
 let eval_external name v = (Maybe_extra.fromJust (List.lookup name function_map)) v ;;
diff --git a/src/test/power.sail b/src/test/power.sail
new file mode 120000
index 00000000..c6415fd5
--- /dev/null
+++ b/src/test/power.sail
@@ -0,0 +1 @@
+../../../../rsem/idl/power/generated/extract-full.sail
\ No newline at end of file
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index 30cd7071..ddad139a 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -4,7 +4,7 @@ let tests = [
   "test3", Test3.defs;
   "pattern", Pattern.defs;
   "vectors", Vectors.defs;
-  (*"power", Power.defs;*)
+  "power", Power.defs;
 ] ;;
 
 let run_all () = List.iter Run_interp.run tests ;;