diff options
Diffstat (limited to 'test')
33 files changed, 428 insertions, 0 deletions
diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail new file mode 100644 index 00000000..1ad9f8bf --- /dev/null +++ b/test/typecheck/fail/assignment_simple1.sail @@ -0,0 +1,16 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + z := 9; + z +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple2.sail b/test/typecheck/fail/assignment_simple2.sail new file mode 100644 index 00000000..db45bbcf --- /dev/null +++ b/test/typecheck/fail/assignment_simple2.sail @@ -0,0 +1,15 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + f(z, z := 10) +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple3.sail b/test/typecheck/fail/assignment_simple3.sail new file mode 100644 index 00000000..2a596c29 --- /dev/null +++ b/test/typecheck/fail/assignment_simple3.sail @@ -0,0 +1,15 @@ + +val (unit, [:10:]) -> [:10:] effect pure f + +function [:10:] f (x, y) = y + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + f(z := 10, z) +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/case_simple1.sail b/test/typecheck/fail/case_simple1.sail new file mode 100644 index 00000000..471c3565 --- /dev/null +++ b/test/typecheck/fail/case_simple1.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> x + } +} diff --git a/test/typecheck/fail/cast_lexp1.sail b/test/typecheck/fail/cast_lexp1.sail new file mode 100644 index 00000000..dad4c84c --- /dev/null +++ b/test/typecheck/fail/cast_lexp1.sail @@ -0,0 +1,7 @@ + +val unit -> nat effect pure test + +function nat test () = { + (int) y := 10; + y +} diff --git a/test/typecheck/fail/cast_simple.sail b/test/typecheck/fail/cast_simple.sail new file mode 100644 index 00000000..19768fbe --- /dev/null +++ b/test/typecheck/fail/cast_simple.sail @@ -0,0 +1,7 @@ + +val unit -> nat effect pure test + +function nat test () = { + (int) y := ([|0:10|]) 10; + (nat) y +} diff --git a/test/typecheck/fail/fun_simple_constraints1.sail b/test/typecheck/fail/fun_simple_constraints1.sail new file mode 100644 index 00000000..979e0cdf --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:64|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints2.sail b/test/typecheck/fail/fun_simple_constraints2.sail new file mode 100644 index 00000000..43a0b6d7 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(9) diff --git a/test/typecheck/fail/fun_simple_constraints3.sail b/test/typecheck/fail/fun_simple_constraints3.sail new file mode 100644 index 00000000..098054e4 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints3.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(plus(sizeof 'N, 1)) diff --git a/test/typecheck/fail/fun_simple_constraints4.sail b/test/typecheck/fail/fun_simple_constraints4.sail new file mode 100644 index 00000000..07b8c596 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints4.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-54)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints5.sail b/test/typecheck/fail/fun_simple_constraints5.sail new file mode 100644 index 00000000..7e28db85 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints5.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-9)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints6.sail b/test/typecheck/fail/fun_simple_constraints6.sail new file mode 100644 index 00000000..6dc5e0e6 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints6.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'k, Nat 'm. ([:'n + 'k:], [:'m:]) -> [:'n + 'k + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints7.sail b/test/typecheck/fail/fun_simple_constraints7.sail new file mode 100644 index 00000000..00d2a172 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints7.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|11:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints8.sail b/test/typecheck/fail/fun_simple_constraints8.sail new file mode 100644 index 00000000..e4c02da0 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints8.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|11:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/return_simple1.sail b/test/typecheck/fail/return_simple1.sail new file mode 100644 index 00000000..1bbc0e73 --- /dev/null +++ b/test/typecheck/fail/return_simple1.sail @@ -0,0 +1,7 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x +} diff --git a/test/typecheck/fail/return_simple2.sail b/test/typecheck/fail/return_simple2.sail new file mode 100644 index 00000000..f212a945 --- /dev/null +++ b/test/typecheck/fail/return_simple2.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + x; + return x; + x +} diff --git a/test/typecheck/fail/return_simple3.sail b/test/typecheck/fail/return_simple3.sail new file mode 100644 index 00000000..df75c5bd --- /dev/null +++ b/test/typecheck/fail/return_simple3.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return 9; + x +} diff --git a/test/typecheck/fail/return_simple4.sail b/test/typecheck/fail/return_simple4.sail new file mode 100644 index 00000000..aa7c3010 --- /dev/null +++ b/test/typecheck/fail/return_simple4.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + 9 +} diff --git a/test/typecheck/fail/return_simple5.sail b/test/typecheck/fail/return_simple5.sail new file mode 100644 index 00000000..d6947d91 --- /dev/null +++ b/test/typecheck/fail/return_simple5.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N - 1|] -> [|10:'N - 1|] effect pure return_test + +function forall Nat 'N. [|10:'N - 1|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/fail/return_simple6.sail b/test/typecheck/fail/return_simple6.sail new file mode 100644 index 00000000..0e118632 --- /dev/null +++ b/test/typecheck/fail/return_simple6.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/pass/assignment_simple.sail b/test/typecheck/pass/assignment_simple.sail new file mode 100644 index 00000000..dc0c78d8 --- /dev/null +++ b/test/typecheck/pass/assignment_simple.sail @@ -0,0 +1,16 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + z := 10; + z +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10
\ No newline at end of file diff --git a/test/typecheck/pass/case_simple1.sail b/test/typecheck/pass/case_simple1.sail new file mode 100644 index 00000000..e4a81a36 --- /dev/null +++ b/test/typecheck/pass/case_simple1.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> y + } +} diff --git a/test/typecheck/pass/case_simple2.sail b/test/typecheck/pass/case_simple2.sail new file mode 100644 index 00000000..0ffba780 --- /dev/null +++ b/test/typecheck/pass/case_simple2.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N, 'N >= 10. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> x + } +} diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail new file mode 100644 index 00000000..f1b87235 --- /dev/null +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + switch x { + case ([|10:30|]) y -> y + case ([:31:]) _ -> sizeof 'N + case ([|31:40|]) _ -> plus(60,3) + } +} +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/pass/cast_lexp1.sail b/test/typecheck/pass/cast_lexp1.sail new file mode 100644 index 00000000..b8b29b87 --- /dev/null +++ b/test/typecheck/pass/cast_lexp1.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (int) y := 10; + y +} diff --git a/test/typecheck/pass/cast_lexp2].sail b/test/typecheck/pass/cast_lexp2].sail new file mode 100644 index 00000000..a6f6d299 --- /dev/null +++ b/test/typecheck/pass/cast_lexp2].sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := 10; + y +} diff --git a/test/typecheck/pass/cast_simple.sail b/test/typecheck/pass/cast_simple.sail new file mode 100644 index 00000000..c1507f26 --- /dev/null +++ b/test/typecheck/pass/cast_simple.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := ([|0:10|]) 10; + (int) y +} diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail new file mode 100644 index 00000000..7fd502b0 --- /dev/null +++ b/test/typecheck/pass/fun_simple_constraints1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N)
\ No newline at end of file diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail new file mode 100644 index 00000000..338ef8e8 --- /dev/null +++ b/test/typecheck/pass/fun_simple_constraints2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [|'n:'n|] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/pass/return_simple1.sail b/test/typecheck/pass/return_simple1.sail new file mode 100644 index 00000000..26e6fc1d --- /dev/null +++ b/test/typecheck/pass/return_simple1.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + x +} diff --git a/test/typecheck/pass/return_simple2.sail b/test/typecheck/pass/return_simple2.sail new file mode 100644 index 00000000..06ce9757 --- /dev/null +++ b/test/typecheck/pass/return_simple2.sail @@ -0,0 +1,11 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + return x; + return x; + return x; + x +} diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail new file mode 100644 index 00000000..7e81b5b2 --- /dev/null +++ b/test/typecheck/pass/return_simple3.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N, 'N >= 10. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N, 'N >= 10. [|10:'N|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh new file mode 100755 index 00000000..49739b5a --- /dev/null +++ b/test/typecheck/run_tests.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +for i in `ls $DIR/pass/`; +do + printf "testing $i expecting pass: " + if $DIR/../../sail $1 $DIR/pass/$i 2> /dev/null; + then + printf "${GREEN}pass${NC}\n" + else + printf "${RED}fail${NC}\n" + fi +done + +for i in `ls $DIR/fail/`; +do + printf "testing $i expecting fail: " + if $DIR/../../sail $1 $DIR/fail/$i 2> /dev/null; + then + printf "${RED}pass${NC}\n" + else + printf "${GREEN}fail${NC}\n" + fi +done |