diff options
| author | Brian Campbell | 2018-06-07 18:00:59 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | 7cdbee76d454047271ef6cdaa82a2b7e2ed590ba (patch) | |
| tree | c0f6e3843758e009551c9de53afbe227ed3df31f /test/coq | |
| parent | dda8dd8689ea4756c41a5bb36a123b564dfb0b12 (diff) | |
Coq: add destructuring of atom existentials in patterns
Plus test case, broken builtin name
Diffstat (limited to 'test/coq')
| -rw-r--r-- | test/coq/pass/exatom.sail | 9 | ||||
| -rwxr-xr-x | test/coq/run_tests.sh | 37 |
2 files changed, 31 insertions, 15 deletions
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" |