some progress on lem backend: rewrite away mutable variable assignments, rewrite for-loops, if/case-expressions to return updated variables

1 files changed, 9 insertions, 1 deletions

diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index e7b20aeb..fe70c9c0 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,8 +1,14 @@
 open import Pervasives
 
-type bit = Zero | One | Undef
+type bit = B0 | B1 | BU
 type vector = Vector of list bit * nat
 
+
+let vector_access (Vector bs start) n =
+  let (Just b) = if is_inc then List.index bs (n - start)
+                 else List.index bs (start - n) in
+  b
+
 let read_vector_subrange is_inc (Vector bs start) n m =
   let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
   let (_,suffix) = List.splitAt offset bs in
@@ -14,3 +20,5 @@ let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) =
   let (prefix,_) = List.splitAt offset bs in
   let (_,suffix) = List.splitAt (offset + length) bs in
   Vector (prefix ++ (List.take length bs') ++ suffix) start
+
+let hd (x :: xs) = x