6 files changed, 89 insertions, 9 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
new file mode 100755
index 00000000..efca8275
--- /dev/null
+++ b/test/coq/run_tests.sh
@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+TESTSDIR="$DIR/../typecheck/pass"
+
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[0;33m'
+NC='\033[0m'
+
+rm -f $DIR/tests.xml
+
+pass=0
+fail=0
+
+XML=""
+
+function green {
+    (( pass += 1 ))
+    printf "$1: ${GREEN}$2${NC}\n"
+    XML+="    <testcase name=\"$1\"/>\n"
+}
+
+function yellow {
+    (( fail += 1 ))
+    printf "$1: ${YELLOW}$2${NC}\n"
+    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
+}
+
+function red {
+    (( fail += 1 ))
+    printf "$1: ${RED}$2${NC}\n"
+    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
+}
+
+function finish_suite {
+    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
+    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
+    printf "$XML" >> $DIR/tests.xml
+    XML=""
+    pass=0
+    fail=0
+}
+
+printf "<testsuites>\n" >> $DIR/tests.xml
+
+cd $DIR
+
+for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`;
+do
+    if $SAILDIR/sail -coq -o out $TESTSDIR/$i &>/dev/null;
+    then
+	if coqc -R ~/bbv bbv -R ../../../sail-private/coq-duopods/precise/lib 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
+
+finish_suite "Coq tests"
+
+printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/coq/skip b/test/coq/skip
new file mode 100644
index 00000000..922cbbe1
--- /dev/null
+++ b/test/coq/skip
@@ -0,0 +1,12 @@
+XXXXX tests with undefined functions
+bind_typ_var.sail
+bitwise_not.*
+bv_simple_index_bit.sail
+ex_cast.sail
+exint.sail
+exist1.sail
+exist2.sail
+exist_subrange.sail
+exist_tlb.sail
+XXXXX tests with full generic equality
+decode_patterns.sail
+\ No newline at end of file
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index d93143f0..2021bf67 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,12 +1,12 @@
 default Order dec
 
-val vector_access = {ocaml: "access", lem: "access_vec_dec"}: forall ('n : Int).
+val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int).
   (vector('n, dec, bit), int) -> bit
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
   (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
 
-val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit)
 
 register _FPEXC32_EL2 : vector(32, dec, bit)
diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail
index 4e030a60..d2549e01 100644
--- a/test/typecheck/pass/atomcase.sail
+++ b/test/typecheck/pass/atomcase.sail
@@ -2,7 +2,7 @@ default Order dec
 
 infix 4 ==
 
-val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
+val eq_atom = {ocaml: "eq_atom", lem: "eq", coq: "Z.eqb"}: forall ('n : Int) ('m : Int).
   (atom('n), atom('m)) -> bool
 
 overload operator == = {eq_atom}
diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
index 991cd828..261e3b44 100644
--- a/test/typecheck/pass/deinfix_plus.sail
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val bv_add = {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int).
   (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
 
 overload operator + = {bv_add}
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 47343e02..96b1ecf1 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -8,14 +8,14 @@ register x : nat
 
 register y : nat
 
-val eq_int = {lem: "eq"} : (int, int) -> bool
-val eq_vec = {lem: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+val eq_int = {lem: "eq", coq: "Z.eqb"} : (int, int) -> bool
+val eq_vec = {lem: "eq_vec", coq: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool
 
 overload operator == = {eq_int, eq_vec}
 
-val "and_bool" : (bool, bool) -> bool
+val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc", coq: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
   (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit)
 
 type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)}