From 8efe97cd6d8140ebebf4d71e597f497dea385964 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 4 Mar 2019 15:48:09 +0000 Subject: Do not store type synonyms as functions in the environment --- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v3.expect | 7 +++++-- test/typecheck/pass/exist_synonym/v4.expect | 7 +++++-- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v2.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 ++-- test/typecheck/pass/if_infer/v2.expect | 4 ++-- 9 files changed, 25 insertions(+), 19 deletions(-) (limited to 'test') diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 6ca2fc40..62992f2c 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:10:4-30 10 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex41# : Int), true. vector(('M * 'ex41#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex80# : Int), true. vector(('M * 'ex80#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index c237ae2d..d63918b4 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,3 +1,6 @@ Type error: -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) - +[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) +  | diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index abb232cb..8157c64f 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,3 +1,6 @@ Type error: -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) - +[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) +  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 1b6239bb..af2cf65f 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('ex59#) +  | * datasize('ex157#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index a1975425..e904aa61 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | 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))  | Coercion failed because: -  | (int(33), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#)) +  | (int(33), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex57# bound here +  |  | 'ex114# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex58# bound here +  |  | 'ex115# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex62# bound here +  |  | 'ex119# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 1ac6c87c..fdd13607 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | 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))  | Coercion failed because: -  | (int(31), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#)) +  | (int(31), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex57# bound here +  |  | 'ex114# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex58# bound here +  |  | 'ex115# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex62# bound here +  |  | 'ex119# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 05dcd0a1..2432e632 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 <= 'ex78# & ('ex78# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex158# & ('ex158# + 1) <= 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index c3b453f2..a63f28f1 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 <= 'ex39# & ('ex39# + 1) <= 3) +  | * (0 <= 'ex76# & ('ex76# + 1) <= 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex42# & ('ex42# + 1) <= 3) +  | * (0 <= 'ex79# & ('ex79# + 1) <= 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index ba2ad410..f37d215f 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 <= 'ex39# & ('ex39# + 1) <= 4) +  | * (0 <= 'ex76# & ('ex76# + 1) <= 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex42# & ('ex42# + 1) <= 4) +  | * (0 <= 'ex79# & ('ex79# + 1) <= 4)  | -- cgit v1.2.3