Merge branch 'sail2' into mappings

(involved some manual tinkering with gitignore, type_check, riscv)

3 files changed, 58 insertions, 58 deletions

diff --git a/test/builtins/run_tests.sh b/test/builtins/run_tests.sh
index 1fe2d182..eeb57a79 100755
--- a/test/builtins/run_tests.sh
+++ b/test/builtins/run_tests.sh
@@ -50,7 +50,7 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 shopt -s nullglob;
 for file in $DIR/*.sail;
 do
-    if $SAILDIR/sail -no_warn -c $file 1> ${file%.sail}.c 2> /dev/null;
+    if $SAILDIR/sail -no_warn -c -O $file 1> ${file%.sail}.c 2> /dev/null;
     then
 	green "compiling $(basename $file) (C)" "ok";
 	if gcc -I $SAILDIR/lib/ ${file%.sail}.c -lgmp;
@@ -69,61 +69,61 @@ do
 	red "compiling $file" "fail"
     fi;
 
-    if $SAILDIR/sail -no_warn -o out -ocaml $file 1> /dev/null 2> /dev/null;
-    then
-	green "compiling $(basename $file) (OCaml)" "ok"
-	if $DIR/out;
-	then
-	    green "tested $(basename ${file%.sail}) (OCaml)" "ok"
-	else
-	    red "tested $(basename ${file%.sail}) (OCaml)" "fail"
-	fi
-    else
-	red "compiling $(basename $file) (OCaml)" "fail"
-    fi;
-
-    mkdir -p "$LEMBUILDDIR"
-
-    if "$SAILDIR/sail" -no_warn -lem -lem_mwords -lem_lib Test_extras -undefined_gen -o out "$file" 1> /dev/null 2> /dev/null;
-    then
-        mv out.lem out_types.lem "$LEMBUILDDIR"
-        if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
-               -outdir "$LEMBUILDDIR" \
-               "$SAILDIR/src/gen_lib/sail_values.lem" \
-               "$SAILDIR/src/gen_lib/sail_operators.lem" \
-               "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \
-               "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \
-               "$SAILDIR/src/gen_lib/prompt.lem" \
-               "$SAILDIR/src/gen_lib/state_monad.lem" \
-               "$SAILDIR/src/gen_lib/state.lem" \
-               "$SAILDIR/src/gen_lib/prompt_monad.lem" \
-               "test_extras.lem" "$LEMBUILDDIR/out_types.lem" "$LEMBUILDDIR/out.lem" 1> /dev/null 2> /dev/null;
-        then
-            cd "$LEMBUILDDIR"
-            if ocamlfind ocamlc -linkpkg -package zarith -package lem \
-                         sail_values.ml sail_operators.ml \
-                         sail_instr_kinds.ml prompt_monad.ml prompt.ml \
-                         sail_operators_mwords.ml state_monad.ml state.ml \
-                         test_extras.ml out_types.ml out.ml ../test.ml \
-                         -o test 1> /dev/null 2> /dev/null
-            then
-                green "compiling $(basename $file) (Lem)" "ok"
-                if ./test 1> /dev/null 2> /dev/null
-                then
-	            green "tested $(basename ${file%.sail}) (Lem)" "ok"
-                else
-	            red "tested $(basename ${file%.sail}) (Lem)" "fail"
-                fi
-            else
-                red "compiling $(basename $file) (Sail->Lem->Ocaml->Bytecode)" "fail"
-            fi
-            cd "$DIR"
-        else
-            red "compiling $(basename $file) (Sail->Lem->Ocaml)" "fail"
-        fi
-    else
-        red "compiling $(basename $file) (Sail->Lem)" "fail"
-    fi;
+    # if $SAILDIR/sail -no_warn -o out -ocaml $file 1> /dev/null 2> /dev/null;
+    # then
+    # 	green "compiling $(basename $file) (OCaml)" "ok"
+    # 	if $DIR/out;
+    # 	then
+    # 	    green "tested $(basename ${file%.sail}) (OCaml)" "ok"
+    # 	else
+    # 	    red "tested $(basename ${file%.sail}) (OCaml)" "fail"
+    # 	fi
+    # else
+    # 	red "compiling $(basename $file) (OCaml)" "fail"
+    # fi;
+
+    # mkdir -p "$LEMBUILDDIR"
+
+    # if "$SAILDIR/sail" -no_warn -lem -lem_mwords -lem_lib Test_extras -undefined_gen -o out "$file" 1> /dev/null 2> /dev/null;
+    # then
+    #     mv out.lem out_types.lem "$LEMBUILDDIR"
+    #     if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
+    #            -outdir "$LEMBUILDDIR" \
+    #            "$SAILDIR/src/gen_lib/sail_values.lem" \
+    #            "$SAILDIR/src/gen_lib/sail_operators.lem" \
+    #            "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \
+    #            "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \
+    #            "$SAILDIR/src/gen_lib/prompt.lem" \
+    #            "$SAILDIR/src/gen_lib/state_monad.lem" \
+    #            "$SAILDIR/src/gen_lib/state.lem" \
+    #            "$SAILDIR/src/gen_lib/prompt_monad.lem" \
+    #            "test_extras.lem" "$LEMBUILDDIR/out_types.lem" "$LEMBUILDDIR/out.lem" 1> /dev/null 2> /dev/null;
+    #     then
+    #         cd "$LEMBUILDDIR"
+    #         if ocamlfind ocamlc -linkpkg -package zarith -package lem \
+    #                      sail_values.ml sail_operators.ml \
+    #                      sail_instr_kinds.ml prompt_monad.ml prompt.ml \
+    #                      sail_operators_mwords.ml state_monad.ml state.ml \
+    #                      test_extras.ml out_types.ml out.ml ../test.ml \
+    #                      -o test 1> /dev/null 2> /dev/null
+    #         then
+    #             green "compiling $(basename $file) (Lem)" "ok"
+    #             if ./test 1> /dev/null 2> /dev/null
+    #             then
+    # 	            green "tested $(basename ${file%.sail}) (Lem)" "ok"
+    #             else
+    # 	            red "tested $(basename ${file%.sail}) (Lem)" "fail"
+    #             fi
+    #         else
+    #             red "compiling $(basename $file) (Sail->Lem->Ocaml->Bytecode)" "fail"
+    #         fi
+    #         cd "$DIR"
+    #     else
+    #         red "compiling $(basename $file) (Sail->Lem->Ocaml)" "fail"
+    #     fi
+    # else
+    #     red "compiling $(basename $file) (Sail->Lem)" "fail"
+    # fi;
 
     rm -rf $DIR/_sbuild/;
     rm -rf "$LEMBUILDDIR";
diff --git a/test/builtins/unsigned1.sail b/test/builtins/unsigned1.sail
index 1a65a06c..ea103099 100644
--- a/test/builtins/unsigned1.sail
+++ b/test/builtins/unsigned1.sail
@@ -3,7 +3,7 @@ default Order dec
 $include <exception_basic.sail>
 $include <vector_dec.sail>
 
-val flip_mask : forall 'len 'v, 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
+val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
 
 function flip_mask(v, len) = len ^ v
 
diff --git a/test/builtins/unsigned3.sail b/test/builtins/unsigned3.sail
index 5b1bc6c2..7d122b2e 100644
--- a/test/builtins/unsigned3.sail
+++ b/test/builtins/unsigned3.sail
@@ -3,7 +3,7 @@ default Order dec
 $include <exception_basic.sail>
 $include <vector_dec.sail>
 
-val flip_mask : forall 'len 'v, 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
+val flip_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (vector('v, dec, bit), atom('len)) -> vector('len, dec, bit)
 
 function flip_mask(v, len) = len ^ v