From 790da51af29e5a17f4bf0c8d95c9bbccb9747b41 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 18 Jun 2019 20:41:21 +0100 Subject: Update test cases --- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v1.expect | 2 +- test/typecheck/pass/exist_synonym/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v3.expect | 2 +- test/typecheck/pass/exist_synonym/v4.expect | 2 +- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 10 +++++----- test/typecheck/pass/existential_ast3/v2.expect | 10 +++++----- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 ++-- test/typecheck/pass/if_infer/v2.expect | 4 ++-- test/typecheck/pass/vec_length/v1.expect | 4 ++-- test/typecheck/pass/vec_length/v1_inc.expect | 4 ++-- test/typecheck/pass/vec_length/v2.expect | 4 ++-- test/typecheck/pass/vec_length/v2_inc.expect | 4 ++-- test/typecheck/pass/vec_length/v3.expect | 4 ++-- 16 files changed, 31 insertions(+), 31 deletions(-) diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 89ab2910..151eb1da 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:13:4-30 13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex172# : Int), true. vector(('M * 'ex172#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex174# : Int), true. vector(('M * 'ex174#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index cc8b874f..940ba4d5 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -4,5 +4,5 @@ Type error:  | ^  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4  | Coercion failed because: -  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) +  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)  | diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index c01d8359..b52572e5 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -4,5 +4,5 @@ Type error:  | ^  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4  | Coercion failed because: -  | Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) +  | Could not prove constraints (0 <= 'n & 'n < 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)  | diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index d63918b4..11563de1 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -2,5 +2,5 @@ Type error: [exist_synonym/v3.sail]:9:38-47 9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit  | ^-------^ -  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) +  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)  | diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index 8157c64f..30e51117 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -2,5 +2,5 @@ Type error: [exist_synonym/v4.sail]:9:35-44 9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit  | ^-------^ -  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) +  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 56b89364..b6d21c9d 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex248#) +  | * datasize('ex250#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 346b7b75..f926c07e 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -2,19 +2,19 @@ Type error: [existential_ast3/v1.sail]:17:48-65 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  | ^---------------^ -  | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a)) +  | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (33, unsigned(a))  | Coercion failed because: -  | (int(33), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#)) +  | (int(33), int('ex212#)) is not a subtype of (int('ex207#), int('ex208#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex205# bound here +  |  | 'ex207# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex206# bound here +  |  | 'ex208# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex210# bound here +  |  | 'ex212# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 7f18c94e..f348260d 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -2,19 +2,19 @@ Type error: [existential_ast3/v2.sail]:17:48-65 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  | ^---------------^ -  | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a)) +  | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (31, unsigned(a))  | Coercion failed because: -  | (int(31), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#)) +  | (int(31), int('ex212#)) is not a subtype of (int('ex207#), int('ex208#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex205# bound here +  |  | 'ex207# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex206# bound here +  |  | 'ex208# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex210# bound here +  |  | 'ex212# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 585cf2c6..9f1f6286 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex249# & ('ex249# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex251# & 'ex251# < 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 50bd530d..3df876b5 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex166# & ('ex166# + 1) <= 3) +  | * (0 <= 'ex168# & 'ex168# < 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex169# & ('ex169# + 1) <= 3) +  | * (0 <= 'ex171# & 'ex171# < 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 27b05208..630a9f2d 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex166# & ('ex166# + 1) <= 4) +  | * (0 <= 'ex168# & 'ex168# < 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex169# & ('ex169# + 1) <= 4) +  | * (0 <= 'ex171# & 'ex171# < 4)  | diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index ce61cf2a..f4cf71c1 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index 3d40cdb0..55f072f2 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index c77ecaa7..349000fb 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_update, tried:  | * bitvector_update  | Could not resolve quantifiers for bitvector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_update  | Could not resolve quantifiers for plain_vector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index cff65f62..1f900286 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_update, tried:  | * bitvector_update  | Could not resolve quantifiers for bitvector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_update  | Could not resolve quantifiers for plain_vector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect index e3afecee..91bb4c99 100644 --- a/test/typecheck/pass/vec_length/v3.expect +++ b/test/typecheck/pass/vec_length/v3.expect @@ -7,8 +7,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | * (0 <= 10 & 10 < 8)  | -- cgit v1.2.3