Merge branch 'sail2' into rmem_interpreter

12 files changed, 75 insertions, 21 deletions

diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 369e72b2..3875105f 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -67,7 +67,7 @@ for test in $DIR/tests/*.elf; do
     fi
 done
 
-if make -C $SAILDIR/riscv riscv_c;
+if make -C $SAILDIR/riscv riscv_sim;
 then
     green "Building RISCV specification to C" "ok"
 else
@@ -75,8 +75,7 @@ else
 fi
 
 for test in $DIR/tests/*.elf; do
-    $SAILDIR/sail -elf $test -o ${test%.elf}.bin 2> /dev/null;
-    if timeout 5 $SAILDIR/riscv/riscv_c --binary=0x1000,reset_vec.bin --image=${test%.elf}.bin > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
+    if timeout 5 $SAILDIR/riscv/riscv_sim $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
     then
 	green "$(basename $test)_c" "ok"
     else
@@ -84,23 +83,23 @@ for test in $DIR/tests/*.elf; do
     fi
 done
 
-printf "Interpreting RISCV specification...\n"
-
-for test in $DIR/tests/*.elf; do
-    if {
-        timeout 30 $SAILDIR/sail -i $SAILDIR/riscv/riscv_all.sail $SAILDIR/riscv/main.sail > ${test%.elf}.iout 2>&1 <<EOF
-:bin 0x1000 $SAILDIR/riscv/reset_vec.bin
-:elf $test
-main()
-:run
-EOF
-    } && grep -q SUCCESS ${test%.elf}.iout
-    then
-        green "$(basename $test)_interpreter" "ok"
-    else
-        red "$(basename $test)_interpreter" "fail"
-    fi
-done
+# printf "Interpreting RISCV specification...\n"
+
+# for test in $DIR/tests/*.elf; do
+#     if {
+#         timeout 30 $SAILDIR/sail -i $SAILDIR/riscv/riscv_all.sail $SAILDIR/riscv/main.sail > ${test%.elf}.iout 2>&1 <<EOF
+# :bin 0x1000 $SAILDIR/riscv/reset_vec.bin
+# :elf $test
+# main()
+# :run
+# EOF
+#     } && grep -q SUCCESS ${test%.elf}.iout
+#     then
+#         green "$(basename $test)_interpreter" "ok"
+#     else
+#         red "$(basename $test)_interpreter" "fail"
+#     fi
+# done
 
 finish_suite "RISCV tests"
 
diff --git a/test/riscv/tests/.gitignore b/test/riscv/tests/.gitignore
index f47cb204..72a5e441 100644
--- a/test/riscv/tests/.gitignore
+++ b/test/riscv/tests/.gitignore
@@ -1 +1,2 @@
 *.out
+*.cout
diff --git a/test/typecheck/pass/constraint_sym.sail b/test/typecheck/pass/constraint_sym.sail
new file mode 100644
index 00000000..6d212e40
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v1.expect b/test/typecheck/pass/constraint_sym/v1.expect
new file mode 100644
index 00000000..71fd6f30
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v1.sail", line 3, character 23 to line 3, character 24
+
+constraint Size('n) = 'm in {32, 64}
+
+No type variable 'm
diff --git a/test/typecheck/pass/constraint_sym/v1.sail b/test/typecheck/pass/constraint_sym/v1.sail
new file mode 100644
index 00000000..4421ee77
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'm in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v2.expect b/test/typecheck/pass/constraint_sym/v2.expect
new file mode 100644
index 00000000..58a0f416
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v2.sail", line 7, character 22 to line 7, character 34
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
+
+Constraint synonym Siz is not defined
diff --git a/test/typecheck/pass/constraint_sym/v2.sail b/test/typecheck/pass/constraint_sym/v2.sail
new file mode 100644
index 00000000..1d98e3e4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v3.expect b/test/typecheck/pass/constraint_sym/v3.expect
new file mode 100644
index 00000000..ab4526dc
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v3.sail", line 7, character 42 to line 7, character 43
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
+
+Constraint is badly formed, 'n has kind Type but should have kind Int
diff --git a/test/typecheck/pass/constraint_sym/v3.sail b/test/typecheck/pass/constraint_sym/v3.sail
new file mode 100644
index 00000000..886acbe4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v4.expect b/test/typecheck/pass/constraint_sym/v4.expect
new file mode 100644
index 00000000..c8374baf
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v4.sail", line 2, character 12 to line 2, character 15
+
+constraint Size('n) = 'n in {32, 64}
+
+Use -Xconstraint_synonyms to enable constraint synonyms
diff --git a/test/typecheck/pass/constraint_sym/v4.sail b/test/typecheck/pass/constraint_sym/v4.sail
new file mode 100644
index 00000000..96bf5e82
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.sail
@@ -0,0 +1,6 @@
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 8014f88a..c7e06dc7 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-Kind identifier 'size is already bound
+type variable 'size is already bound