diff options
Diffstat (limited to 'test')
| -rwxr-xr-x | test/mono/run_tests.sh | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate.sail | 12 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v1.expect | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v1.sail | 12 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v2.expect | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v2.sail | 11 |
6 files changed, 54 insertions, 3 deletions
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh index 6a9dedd6..08926aaa 100755 --- a/test/mono/run_tests.sh +++ b/test/mono/run_tests.sh @@ -6,9 +6,9 @@ SAILDIR="$DIR/../.." TESTSDIR="$DIR" OUTPUTDIR="$DIR/test-output" -RED='\033[0;31m' -GREEN='\033[0;32m' -YELLOW='\033[0;33m' +RED='\033[0;91m' +GREEN='\033[0;92m' +YELLOW='\033[0;93m' NC='\033[0m' rm -f $DIR/tests.xml diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail new file mode 100644 index 00000000..03954a9f --- /dev/null +++ b/test/typecheck/pass/Replicate.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <smt.sail> +$include <prelude.sail> + +val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. + (implicit('N), bits('M)) -> bits('N) effect {escape} + +function Replicate (N, x) = { + assert('N % 'M == 0); + replicate_bits(x, 'N / 'M) +}
\ No newline at end of file diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect new file mode 100644 index 00000000..92c6d7cd --- /dev/null +++ b/test/typecheck/pass/Replicate/v1.expect @@ -0,0 +1,8 @@ +Type error: +[[96mReplicate/v1.sail[0m]:11:4-30 +11[96m |[0m replicate_bits(x, 'N / 'M) + [91m |[0m [91m^------------------------^[0m + [91m |[0m Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x))) + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail new file mode 100644 index 00000000..69f2bb6f --- /dev/null +++ b/test/typecheck/pass/Replicate/v1.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <smt.sail> +$include <prelude.sail> + +val Replicate : forall ('M : Int) ('N : Int), 'M >= 0. + (implicit('N), bits('M)) -> bits('N) effect {escape} + +function Replicate (N, x) = { + assert('N % 'M == 0); + replicate_bits(x, 'N / 'M) +}
\ No newline at end of file diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect new file mode 100644 index 00000000..0dec309f --- /dev/null +++ b/test/typecheck/pass/Replicate/v2.expect @@ -0,0 +1,8 @@ +Type error: +[[96mReplicate/v2.sail[0m]:10:4-30 +10[96m |[0m replicate_bits(x, 'N / 'M) + [91m |[0m [91m^------------------------^[0m + [91m |[0m Tried performing type coercion from {('ex42# : Int), true. vector(('M * 'ex42#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail new file mode 100644 index 00000000..e54b0af4 --- /dev/null +++ b/test/typecheck/pass/Replicate/v2.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. + (implicit('N), bits('M)) -> bits('N) effect {escape} + +function Replicate (N, x) = { + assert('N % 'M == 0); + replicate_bits(x, 'N / 'M) +}
\ No newline at end of file |