summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGabriel Kerneis2013-10-14 13:37:07 +0100
committerGabriel Kerneis2013-10-14 13:37:07 +0100
commit14d544935fc87df2b258cd4c9ed5acede44fe1f3 (patch)
tree4d4ddf7927acf2fd276068ea21d6395cfba99bc5 /src
parent5c9abc9e9b56640270aa3b50560ccc87d5b765e3 (diff)
Run main() to execute tests
Tests do not pass because of weird pattern-matching errors in the interpreter.
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/run_interp.ml2
-rw-r--r--src/test/test1.sail2
-rw-r--r--src/test/test2.sail7
3 files changed, 7 insertions, 4 deletions
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index d28cb0d6..ba3557bf 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -47,7 +47,7 @@ let act_to_string = function
| Write_mem _ -> "write_mem"
;;
-let run (name, test) = match interp test (E_block []) with
+let run (name, test) = match interp test (E_app(E_id(Id "main"), [E_lit L_unit])) 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
diff --git a/src/test/test1.sail b/src/test/test1.sail
index e3a98e3f..98dd92c2 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -10,3 +10,5 @@ typedef maybe = const union forall a. { unit None; a Some; }
typedef colors = enumerate { red; green; blue }
typedef creg = register bits [5:i] { 5 : h ; 6..7 : j}
let bool e = true
+
+function unit main _ = ()
diff --git a/src/test/test2.sail b/src/test/test2.sail
index 778e69cb..baffd9b3 100644
--- a/src/test/test2.sail
+++ b/src/test/test2.sail
@@ -1,4 +1,5 @@
-function unit main ( < bit > x ) = {
- 42
+function nat id ( n ) = n
+
+function nat main _ = {
+ id ( 42 );
}
-let unit run = main ( 42 )