diff options
Diffstat (limited to 'test')
20 files changed, 221 insertions, 12 deletions
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect index 5173ef0b..ab25cbc4 100644 --- a/test/typecheck/pass/constrained_struct/v1.expect +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -2,4 +2,4 @@ Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 1 type MyStruct64 = [41mMyStruct[0m(65) -Could not prove (65 = 32 | 65 = 64) for type constructor MyStruct +Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct diff --git a/test/typecheck/pass/constraint_ctor.sail b/test/typecheck/pass/constraint_ctor.sail new file mode 100644 index 00000000..2b4a5746 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <flow.sail> + +union Foo = { + Foo : {'n, 'n >= 3. int('n)} +} + +function foo(Foo(x as int('x)): Foo) -> unit = { + _prove(constraint('x >= 3)); +} + +union Bar('m), 'm <= 100 = { + Bar : {'n, 'n >= 'm. int('n)} +} + +function bar(Bar(x as int('x)) : Bar(23)) -> unit = { + _prove(constraint('x >= 23)); + () +} diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect new file mode 100644 index 00000000..c3886af8 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v1.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_ctor/v1.sail", line 10, character 3 to line 10, character 29 + + [41m_prove(constraint('x >= 4))[0m; + +Cannot prove 'x >= 4 diff --git a/test/typecheck/pass/constraint_ctor/v1.sail b/test/typecheck/pass/constraint_ctor/v1.sail new file mode 100644 index 00000000..20df5480 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v1.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <flow.sail> + +union Foo = { + Foo : {'n, 'n >= 3. int('n)} +} + +function foo(Foo(x as int('x)): Foo) -> unit = { + _prove(constraint('x >= 4)); +} + +union Bar('m), 'm <= 100 = { + Bar : {'n, 'n >= 'm. int('n)} +} + +function bar(Bar(x as int('x)) : Bar(23)) -> unit = { + _prove(constraint('x >= 23)); + () +} diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect new file mode 100644 index 00000000..a315b3b7 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v2.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_ctor/v2.sail", line 18, character 3 to line 18, character 30 + + [41m_prove(constraint('x >= 24))[0m; + +Cannot prove 'x >= 24 diff --git a/test/typecheck/pass/constraint_ctor/v2.sail b/test/typecheck/pass/constraint_ctor/v2.sail new file mode 100644 index 00000000..76d9793d --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v2.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <flow.sail> + +union Foo = { + Foo : {'n, 'n >= 3. int('n)} +} + +function foo(Foo(x as int('x)): Foo) -> unit = { + _prove(constraint('x >= 3)); +} + +union Bar('m), 'm <= 100 = { + Bar : {'n, 'n >= 'm. int('n)} +} + +function bar(Bar(x as int('x)) : Bar(23)) -> unit = { + _prove(constraint('x >= 24)); + () +} diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect new file mode 100644 index 00000000..e0edd01a --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v3.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_ctor/v3.sail", line 18, character 3 to line 18, character 30 + + [41m_prove(constraint('x >= 23))[0m; + +Cannot prove 'x >= 23 diff --git a/test/typecheck/pass/constraint_ctor/v3.sail b/test/typecheck/pass/constraint_ctor/v3.sail new file mode 100644 index 00000000..a8f5bd13 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v3.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <flow.sail> + +union Foo = { + Foo : {'n, 'n >= 3. int('n)} +} + +function foo(Foo(x as int('x)): Foo) -> unit = { + _prove(constraint('x >= 3)); +} + +union Bar('m), 'm <= 100 = { + Bar : {'n, 'n >= 'm. int('n)} +} + +function bar(Bar(x as int('x)) : Bar(22)) -> unit = { + _prove(constraint('x >= 23)); + () +} diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect new file mode 100644 index 00000000..06eb9d22 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v4.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_ctor/v4.sail", line 17, character 34 to line 17, character 36 + +function bar(Bar(x as int('x)) : [41mBar[0m(23)) -> unit = { + +Could not prove 23 <= 22 for type constructor Bar diff --git a/test/typecheck/pass/constraint_ctor/v4.sail b/test/typecheck/pass/constraint_ctor/v4.sail new file mode 100644 index 00000000..d8dab178 --- /dev/null +++ b/test/typecheck/pass/constraint_ctor/v4.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <flow.sail> + +union Foo = { + Foo : {'n, 'n >= 3. int('n)} +} + +function foo(Foo(x as int('x)): Foo) -> unit = { + _prove(constraint('x >= 3)); +} + +union Bar('m), 'm <= 22 = { + Bar : {'n, 'n >= 'm. int('n)} +} + +function bar(Bar(x as int('x)) : Bar(23)) -> unit = { + _prove(constraint('x >= 23)); + () +} diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail index 102a1084..e518609d 100644 --- a/test/typecheck/pass/exist2.sail +++ b/test/typecheck/pass/exist2.sail @@ -39,6 +39,6 @@ overload existential = {existential_int, existential_range} let v11 : {'n, 0 == 0. atom('n)} = existential(v10) -let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3)) +let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = 2 let v13 : MyInt = existential(v10) diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index 7e3b517c..e81c467e 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/test/typecheck/pass/global_type_var/v1.expect @@ -6,15 +6,15 @@ Tried performing type coercion from int(32) to int('size) on 32 Coercion failed because: int(32) is not a subtype of int('size) in context - * 'size = 'ex8# - * ('ex8# = 32 | 'ex8# = 64) - * ('ex7# = 32 | 'ex7# = 64) + * 'size == 'ex14# + * ('ex14# == 32 | 'ex14# == 64) + * ('ex13# == 32 | 'ex13# == 64) where - * 'ex7# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32 + * 'ex13# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32 let [41m(size as 'size) : {|32, 64|}[0m = 32 - * 'ex8# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18 + * 'ex14# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18 let ([41msize as 'size[0m) : {|32, 64|} = 32 diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index dc1281d2..21c4b348 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/test/typecheck/pass/global_type_var/v2.expect @@ -6,15 +6,15 @@ Tried performing type coercion from int(64) to int('size) on 64 Coercion failed because: int(64) is not a subtype of int('size) in context - * 'size = 'ex8# - * ('ex8# = 32 | 'ex8# = 64) - * ('ex7# = 32 | 'ex7# = 64) + * 'size == 'ex14# + * ('ex14# == 32 | 'ex14# == 64) + * ('ex13# == 32 | 'ex13# == 64) where - * 'ex7# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32 + * 'ex13# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32 let [41m(size as 'size) : {|32, 64|}[0m = 32 - * 'ex8# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18 + * 'ex14# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18 let ([41msize as 'size[0m) : {|32, 64|} = 32 diff --git a/test/typecheck/pass/if_infer.sail b/test/typecheck/pass/if_infer.sail new file mode 100644 index 00000000..f3fec1c4 --- /dev/null +++ b/test/typecheck/pass/if_infer.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +register R : bool + +val f : unit -> {'n, 1 <= 'n <= 3. int('n)} + +function main((): unit) -> unit = { + let _ = 0b1001[if R then 0 else f()]; + () +} diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect new file mode 100644 index 00000000..06df7dc5 --- /dev/null +++ b/test/typecheck/pass/if_infer/v1.expect @@ -0,0 +1,17 @@ +Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, character 37 + + let _ = [41m0b100[if R then 0 else f()][0m; + +No overloadings for vector_access, tried: + bitvector_access: + Could not resolve quantifiers for bitvector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 3) + + Try adding named type variables for + + + plain_vector_access: + Could not resolve quantifiers for plain_vector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 3) + + Try adding named type variables for + + diff --git a/test/typecheck/pass/if_infer/v1.sail b/test/typecheck/pass/if_infer/v1.sail new file mode 100644 index 00000000..0938aaed --- /dev/null +++ b/test/typecheck/pass/if_infer/v1.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +register R : bool + +val f : unit -> {'n, 1 <= 'n <= 3. int('n)} + +function main((): unit) -> unit = { + let _ = 0b100[if R then 0 else f()]; + () +} diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect new file mode 100644 index 00000000..050e90e4 --- /dev/null +++ b/test/typecheck/pass/if_infer/v2.expect @@ -0,0 +1,17 @@ +Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, character 38 + + let _ = [41m0b1001[if R then 0 else f()][0m; + +No overloadings for vector_access, tried: + bitvector_access: + Could not resolve quantifiers for bitvector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 4) + + Try adding named type variables for + + + plain_vector_access: + Could not resolve quantifiers for plain_vector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 4) + + Try adding named type variables for + + diff --git a/test/typecheck/pass/if_infer/v2.sail b/test/typecheck/pass/if_infer/v2.sail new file mode 100644 index 00000000..a49e1ed7 --- /dev/null +++ b/test/typecheck/pass/if_infer/v2.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +register R : bool + +val f : unit -> {'n, 1 <= 'n <= 4. int('n)} + +function main((): unit) -> unit = { + let _ = 0b1001[if R then 0 else f()]; + () +} diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect new file mode 100644 index 00000000..8b149bc8 --- /dev/null +++ b/test/typecheck/pass/if_infer/v3.expect @@ -0,0 +1,7 @@ +Type error at file "if_infer/v3.sail", line 10, character 11 to line 10, character 38 + + let _ = [41m0b1001[if R then 0 else f()][0m; + +No overloadings for vector_access, tried: + bitvector_access: Numeric type is non-simple + plain_vector_access: Numeric type is non-simple diff --git a/test/typecheck/pass/if_infer/v3.sail b/test/typecheck/pass/if_infer/v3.sail new file mode 100644 index 00000000..0c3dec21 --- /dev/null +++ b/test/typecheck/pass/if_infer/v3.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +register R : bool + +val f : unit -> {'n 'm, 'm == 3 & 1 <= 'n <= 'm. int('n)} + +function main((): unit) -> unit = { + let _ = 0b1001[if R then 0 else f()]; + () +} |