Add signed and unsigned bitvector extensions

lib/Cryptol.cry

@@ -219,6 +219,19 @@ primitive scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
 sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
 sborrow x y = ( x <$ (x-y) ) ^ y@0
 
+/**
+ * Zero extension of a bitvector.
+ */
+zext : {n, m} (fin m, m >= n) => [n] -> [m]
+zext x = zero # x
+
+/**
+ * Sign extension of a bitvector.
+ */
+sext : {n, m} (fin m, m >= n, n >= 1) => [n] -> [m]
+sext x = newbits # x
+  where newbits = if x@0 then ~zero else zero
+
 /**
  * Short-cutting boolean conjuction function.
  * If the first argument is False, the second argument