diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/builtins/div_int.sail | 2 | ||||
| -rw-r--r-- | test/builtins/div_int2.sail | 2 | ||||
| -rw-r--r-- | test/builtins/divmod.sail | 43 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v1.expect | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v1.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v2.expect | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/Replicate/v2.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/guards.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/recursion.sail | 2 |
10 files changed, 66 insertions, 7 deletions
diff --git a/test/builtins/div_int.sail b/test/builtins/div_int.sail index fed6de6e..e8da4f4b 100644 --- a/test/builtins/div_int.sail +++ b/test/builtins/div_int.sail @@ -5,6 +5,8 @@ $include <flow.sail> $include <vector_dec.sail> $include <arith.sail> +overload div_int = {tdiv_int} + function main (() : unit) -> unit = { assert(div_int(48240160, 8) == 6030020); assert(div_int(48240168, 8) == 6030021); diff --git a/test/builtins/div_int2.sail b/test/builtins/div_int2.sail index d3df278d..8ce97cc0 100644 --- a/test/builtins/div_int2.sail +++ b/test/builtins/div_int2.sail @@ -5,6 +5,8 @@ $include <flow.sail> $include <vector_dec.sail> $include <arith.sail> +overload div_int = {tdiv_int} + function main (() : unit) -> unit = { assert(div_int(0, 8) == 0); assert(div_int(1000, 12) == 83); diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail new file mode 100644 index 00000000..f9d7e7c5 --- /dev/null +++ b/test/builtins/divmod.sail @@ -0,0 +1,43 @@ +default Order dec + +$include <exception_basic.sail> +$include <arith.sail> +$include <smt.sail> + +function main (() : unit) -> unit = { + assert(ediv_int( 7 , 5) == 1); + assert(ediv_int( 7 , -5) == -1); + assert(ediv_int(-7 , 5) == -2); + assert(ediv_int(-7 , -5) == 2); + assert(ediv_int( 12 , 3) == 4); + assert(ediv_int( 12 , -3) == -4); + assert(ediv_int(-12 , 3) == -4); + assert(ediv_int(-12 , -3) == 4); + + assert(emod_int( 7 , 5) == 2); + assert(emod_int( 7 , -5) == 2); + assert(emod_int(-7 , 5) == 3); + assert(emod_int(-7 , -5) == 3); + assert(emod_int( 12 , 3) == 0); + assert(emod_int( 12 , -3) == 0); + assert(emod_int(-12 , 3) == 0); + assert(emod_int(-12 , -3) == 0); + + assert(tdiv_int( 7 , 5) == 1); + assert(tdiv_int( 7 , -5) == -1); + assert(tdiv_int(-7 , 5) == -1); + assert(tdiv_int(-7 , -5) == 1); + assert(tdiv_int( 12 , 3) == 4); + assert(tdiv_int( 12 , -3) == -4); + assert(tdiv_int(-12 , 3) == -4); + assert(tdiv_int(-12 , -3) == 4); + + assert(tmod_int( 7 , 5) == 2); + assert(tmod_int( 7 , -5) == 2); + assert(tmod_int(-7 , 5) == -2); + assert(tmod_int(-7 , -5) == -2); + assert(tmod_int( 12 , 3) == 0); + assert(tmod_int( 12 , -3) == 0); + assert(tmod_int(-12 , 3) == 0); + assert(tmod_int(-12 , -3) == 0); +}
\ No newline at end of file diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail index 03954a9f..291b7e16 100644 --- a/test/typecheck/pass/Replicate.sail +++ b/test/typecheck/pass/Replicate.sail @@ -3,6 +3,9 @@ default Order dec $include <smt.sail> $include <prelude.sail> +overload operator / = {ediv_int} +overload operator % = {emod_int} + val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. (implicit('N), bits('M)) -> bits('N) effect {escape} diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect index 92c6d7cd..c40aa5ec 100644 --- a/test/typecheck/pass/Replicate/v1.expect +++ b/test/typecheck/pass/Replicate/v1.expect @@ -1,8 +1,8 @@ Type error: -[[96mReplicate/v1.sail[0m]:11:4-30 -11[96m |[0m replicate_bits(x, 'N / 'M) +[[96mReplicate/v1.sail[0m]:14:4-30 +14[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 Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_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/v1.sail b/test/typecheck/pass/Replicate/v1.sail index 69f2bb6f..55627db5 100644 --- a/test/typecheck/pass/Replicate/v1.sail +++ b/test/typecheck/pass/Replicate/v1.sail @@ -3,6 +3,9 @@ default Order dec $include <smt.sail> $include <prelude.sail> +overload operator / = {ediv_int} +overload operator % = {emod_int} + val Replicate : forall ('M : Int) ('N : Int), 'M >= 0. (implicit('N), bits('M)) -> bits('N) effect {escape} diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 6afdac30..c2c15c12 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -1,8 +1,8 @@ Type error: -[[96mReplicate/v2.sail[0m]:10:4-30 -10[96m |[0m replicate_bits(x, 'N / 'M) +[[96mReplicate/v2.sail[0m]:13:4-30 +13[96m |[0m replicate_bits(x, 'N / 'M) [91m |[0m [91m^------------------------^[0m - [91m |[0m Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) + [91m |[0m Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_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 index e54b0af4..436ef24b 100644 --- a/test/typecheck/pass/Replicate/v2.sail +++ b/test/typecheck/pass/Replicate/v2.sail @@ -2,6 +2,9 @@ default Order dec $include <prelude.sail> +overload operator / = {tdiv_int} +overload operator % = {tmod_int} + val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. (implicit('N), bits('M)) -> bits('N) effect {escape} diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail index 4aac2bed..594130a8 100644 --- a/test/typecheck/pass/guards.sail +++ b/test/typecheck/pass/guards.sail @@ -1,8 +1,9 @@ default Order dec $include <prelude.sail> +$include <smt.sail> -overload operator / = {quotient} +overload operator / = {ediv_int} union T = {C1 : int, C2 : int} diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail index 5ca85f53..cd3ca46c 100644 --- a/test/typecheck/pass/recursion.sail +++ b/test/typecheck/pass/recursion.sail @@ -2,6 +2,8 @@ default Order dec $include <prelude.sail> +overload operator / = {tdiv_int} + val log2 : int -> int function log2(n) = |