summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGabriel Kerneis2014-02-27 10:23:53 +0000
committerGabriel Kerneis2014-02-27 14:16:14 +0000
commit3875102240b66c9ee0180cf0733c578d8c0d7447 (patch)
tree4080abe5fd557c5eae59c0213a3a4db62697fadc
parentbfe28e3e443fd28e7182cfeff1cf8b5fa5bc4e5a (diff)
More flexible test execution
-rw-r--r--src/lem_interp/run_interp.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 19c27b56..66880ade 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -180,7 +180,11 @@ let perform_action ((reg, mem) as env) = function
;;
-let run (name, test) =
+let run
+ ?(entry=E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)))
+ ?(reg=Reg.empty)
+ ?(mem=Mem.empty)
+ (name, test) =
let rec loop env = function
| Value v -> eprintf "%s: returned %s\n" name (val_to_string v); true
| Action (a, s) ->
@@ -190,11 +194,10 @@ let run (name, test) =
eprintf "%s: action returned %s\n" name (val_to_string return);
loop env' (resume test s return)
| Error(l, e) -> eprintf "%s: %s: error: %s\n" name (loc_to_string l) e; false in
- let entry = E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)) in
eprintf "%s: starting\n" name;
try
Printexc.record_backtrace true;
- loop (Reg.empty, Mem.empty) (interp test entry)
+ loop (reg, mem) (interp test entry)
with e ->
let trace = Printexc.get_backtrace () in
eprintf "%s: interpretor error %s\n%s\n" name (Printexc.to_string e) trace;