summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b4e6f7ad..b2dc6295 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -3,6 +3,7 @@ import Map
import Map_extra
import Maybe
import List_extra
+import String
open import Interp_ast
@@ -159,6 +160,14 @@ let update_mem (Mem c m) loc value =
let m' = Map.insert loc value m' in
Mem c m'
+val litV_to_vec : lit -> value
+let litV_to_vec l =
+ match l with
+ | L_bin s ->
+ let bits = String.toCharList s in
+ V_vector 0 true []
+ end
+
val access_vector : value -> nat -> value
let access_vector v n =
match v with