Add functions "rotateL" and "rotateR" to SAWCore prelude; set up eval…

…uator
GaloisInc · May 27, 2014 · b53cc78 · b53cc78
1 parent 4ff7460
commit b53cc78
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
@@ -605,6 +605,12 @@ append m n a x y =
     (\(i :: Fin (addNat m n)) ->
       either (Fin m) (Fin n) a (get m a x) (get n a y) (finSplitSum m n i));
 
+-- Rotate array to the left.
+rotateL :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> Vec n a;
+
+-- Rotate array to the right.
+rotateR :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> Vec n a;
+
 --------------------------------------------------------------------------------
 -- Bitvectors