Progress on toFromInterp backend

Now builds for riscv duopod

1 files changed, 46 insertions, 0 deletions

diff --git a/src/toFromInterp_lib.ml b/src/toFromInterp_lib.ml
new file mode 100644
index 00000000..b045e4e8
--- /dev/null
+++ b/src/toFromInterp_lib.ml
@@ -0,0 +1,46 @@
+(************************************************************)
+(* Support for toFromInterp                                 *)
+(************************************************************)
+
+open Sail_lib;;
+open Value;;
+
+type vector_order =
+ | Order_inc
+ | Order_dec
+
+
+let zunitFromInterpValue v = match v with
+  | V_unit -> ()
+  | _ -> failwith "invalid interpreter value for unit"
+
+let zunitToInterpValue () = V_unit
+
+
+let zatomFromInterpValue typq_'n v = match v with
+  | V_int i ->
+     assert (typq_'n = i);
+     i
+  | _ -> failwith "invalid interpreter value for atom"
+
+let zatomToInterpValue typq_'n v =
+  assert (typq_'n = v);
+  V_int v
+
+
+let zvectorFromInterpValue typq_'n typq_'ord typq_'a v = match v with
+  | V_vector vs ->
+     assert (Big_int.of_int (List.length vs) = typq_'n);
+     List.map typq_'a vs
+  | _ -> failwith "invalid interpreter value for vector"
+
+let zvectorToInterpValue typq_'n typq_'ord typq_'a v =
+  assert (Big_int.of_int (List.length v) = typq_'n);
+  V_vector (List.map typq_'a v)
+
+
+let zbitFromInterpValue v = match v with
+  | V_bit b -> b
+  | _ -> failwith "invalid interpreter value for bit"
+
+let zbitToInterpValue v = V_bit v