summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGabriel Kerneis2013-10-10 17:21:17 +0100
committerGabriel Kerneis2013-10-10 17:21:17 +0100
commit40b4aefdd9d225acf7c6a22237e89ecb4148f2e6 (patch)
tree3d535a99b4f26c3b649158cf5d07d0d9dc387283
parentee74df73e643a905e70bb234a150a05e94a9e9ff (diff)
Run interpreter
Forgotten because of a wrong .gitignore.
-rw-r--r--.gitignore2
-rw-r--r--src/lem_interp/run_interp.ml29
2 files changed, 29 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore
index ea9ace17..8c7767f2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,6 @@
*.native
*.byte
src/_build/
-src/lem_interp/_build/
-src/lem_interp/*.ml
language/*.pdf
language/*.uo
language/*.ui
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
new file mode 100644
index 00000000..2d5ff230
--- /dev/null
+++ b/src/lem_interp/run_interp.ml
@@ -0,0 +1,29 @@
+open Printf ;;
+open Interp_ast ;;
+open Interp ;;
+
+let val_to_string = function
+ (*
+ | V_boxref of nat
+ | V_lit of lit
+ | V_tuple of list value
+ | V_list of list value
+ | V_vector of nat * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
+ | V_record of list (id * value)
+ | V_ctor of id * value
+ *)
+ | _ -> "*** value pretty-printing not implemented ***"
+;;
+
+let act_to_string = function
+ | Read_reg _ -> "read_reg"
+ | Write_reg _ -> "write_reg"
+ | Read_mem _ -> "read_mem"
+ | Write_mem _ -> "write_mem"
+;;
+
+let run (name, test) = match interp test (E_block []) with
+ | Value v -> eprintf "%s: returned %s\n" name (val_to_string v)
+ | Action (a, s) -> eprintf "%s: suspended on action %s\n" name (act_to_string a)
+ | Error e -> eprintf "%s: error: %s\n" name e
+;;