Added tests for lem shallow embedding

Now the test suite generates lem for all the typechecker tests, and
tests if the generated lem typechecks. For a lot of the cases the
answer is currently no.

4 files changed, 39 insertions, 10 deletions

diff --git a/test/typecheck/pass/exit1.sail b/test/typecheck/pass/exit1.sail
index fa1de7e0..92515c5a 100644
--- a/test/typecheck/pass/exit1.sail
+++ b/test/typecheck/pass/exit1.sail
@@ -1,8 +1,8 @@
 
-val unit -> [:6:] effect pure test
+val unit -> [:6:] effect {escape} test
 
 function [:6:] test () =
 {
   exit ();
   6
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/exit2.sail b/test/typecheck/pass/exit2.sail
index 40bf7da3..574302cc 100644
--- a/test/typecheck/pass/exit2.sail
+++ b/test/typecheck/pass/exit2.sail
@@ -1,7 +1,7 @@
 
-val unit -> [:6:] effect pure test
+val unit -> [:6:] effect {escape} test
 
 function [:6:] test () =
 {
   exit ();
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/exit3.sail b/test/typecheck/pass/exit3.sail
index 9ac0aa78..e26ff95c 100644
--- a/test/typecheck/pass/exit3.sail
+++ b/test/typecheck/pass/exit3.sail
@@ -1,7 +1,7 @@
 
-val forall Type 'a. unit -> 'a effect pure test
+val forall Type 'a. unit -> 'a effect {escape} test
 
 function forall Type 'a. 'a test () =
 {
   exit ();
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index f33f21ac..a333901b 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -2,6 +2,7 @@
 set -e
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
 
 RED='\033[0;31m'
 GREEN='\033[0;32m'
@@ -9,6 +10,7 @@ YELLOW='\033[0;33m'
 NC='\033[0m'
 
 mkdir -p $DIR/rtpass
+mkdir -p $DIR/lem
 mkdir -p $DIR/rtfail
 
 pass=0
@@ -17,9 +19,9 @@ fail=0
 for i in `ls $DIR/pass/`;
 do
     printf "testing $i expecting pass: "
-    if $DIR/../../sail -ddump_tc_ast -just_check $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
+    if $SAILDIR/sail -ddump_tc_ast -just_check $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
     then
-	if $DIR/../../sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null;
+	if $SAILDIR/sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null;
 	then
 	    (( pass += 2))
 	    printf "${GREEN}pass${NC}\n"
@@ -37,12 +39,12 @@ done
 for i in `ls $DIR/fail/`;
 do
     printf "testing $i expecting fail: "
-    if $DIR/../../sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i;
+    if $SAILDIR/sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i;
     then
 	(( fail += 2 ))
 	printf "${RED}pass${NC}\n"
     else
-	if $DIR/../../sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null;
+	if $SAILDIR/sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null;
 	then
 	    (( fail += 1 ))
 	    (( pass += 1 ))
@@ -54,4 +56,31 @@ do
     fi
 done
 
+function test_lem {
+    for i in `ls $DIR/pass/`;
+    do
+	printf "generating lem for $1/$i: "
+	if $SAILDIR/sail -lem $DIR/$1/$i 2> /dev/null
+	then
+	    mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/
+	    mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/
+	    mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/
+	    if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed.lem 2> /dev/null
+	    then
+		(( pass += 1 ))
+		printf "${GREEN}pass${NC}\n"
+	    else
+		(( fail += 1 ))
+		printf "${RED}fail${NC}\n"
+	    fi
+	else
+	    (( fail += 1 ))
+	    printf "${RED}failed to generate lem!${NC}\n"
+	fi
+    done
+}
+
+test_lem pass
+test_lem rtpass
+
 printf "Passed ${pass} out of $(( pass + fail ))\n"