From 7cdbee76d454047271ef6cdaa82a2b7e2ed590ba Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 7 Jun 2018 18:00:59 +0100
Subject: Coq: add destructuring of atom existentials in patterns Plus test
 case, broken builtin name

---
 test/coq/pass/exatom.sail |  9 +++++++++
 test/coq/run_tests.sh     | 37 ++++++++++++++++++++++---------------
 2 files changed, 31 insertions(+), 15 deletions(-)
 create mode 100644 test/coq/pass/exatom.sail

(limited to 'test')

diff --git a/test/coq/pass/exatom.sail b/test/coq/pass/exatom.sail
new file mode 100644
index 00000000..db162536
--- /dev/null
+++ b/test/coq/pass/exatom.sail
@@ -0,0 +1,9 @@
+$include <prelude.sail>
+
+val f : forall 'n, 'n in {8,16}. atom('n) -> atom('n)
+
+val make : unit -> {'n, 'n in {8,16}. atom('n)}
+
+val test : {'n, 'n in {8,16}. atom('n)} -> int
+
+function test(v) = f(v)
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index f782ed80..2be5e535 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -3,7 +3,8 @@ set -e
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 SAILDIR="$DIR/../.."
-TESTSDIR="$DIR/../typecheck/pass"
+TYPECHECKTESTSDIR="$DIR/../typecheck/pass"
+EXTRATESTSDIR="$DIR/pass"
 BBVDIR="$DIR/../../../bbv"
 
 RED='\033[0;31m'
@@ -49,20 +50,26 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 
 cd $DIR
 
-for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`;
-do
-    if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null;
-    then
-	if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null;
-	then
-	    green "tested $i expecting pass" "pass"
-	else
-	    yellow "tested $i expecting pass" "failed to typecheck generated Coq"
-	fi
-    else
-	red "tested $i expecting pass" "failed to generate Coq"
-    fi
-done
+function check_tests_dir {
+    TESTSDIR="$1"
+    for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`;
+    do
+        if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null;
+        then
+    	if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null;
+    	then
+    	    green "tested $i expecting pass" "pass"
+    	else
+    	    yellow "tested $i expecting pass" "failed to typecheck generated Coq"
+    	fi
+        else
+    	red "tested $i expecting pass" "failed to generate Coq"
+        fi
+    done
+}
+
+check_tests_dir "$TYPECHECKTESTSDIR"
+check_tests_dir "$EXTRATESTSDIR"
 
 finish_suite "Coq tests"
 
-- 
cgit v1.2.3