diff options
Diffstat (limited to 'test')
43 files changed, 404 insertions, 252 deletions
diff --git a/test/c/bool_bits_mapping.expect b/test/c/bool_bits_mapping.expect new file mode 100644 index 00000000..79ebd086 --- /dev/null +++ b/test/c/bool_bits_mapping.expect @@ -0,0 +1,2 @@ +ok +ok diff --git a/test/c/bool_bits_mapping.sail b/test/c/bool_bits_mapping.sail new file mode 100644 index 00000000..1a104186 --- /dev/null +++ b/test/c/bool_bits_mapping.sail @@ -0,0 +1,23 @@ +default Order dec + +$include <prelude.sail> + +mapping bool_bits : bool <-> bits(1) = { + true <-> 0b1, + false <-> 0b0 +} + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + if bool_bits(0b1) then { + print_endline("ok") + } else { + print_endline("fail") + }; + if bool_bits(true) == 0b1 then { + print_endline("ok") + } else { + print_endline("fail") + } +}
\ No newline at end of file diff --git a/test/c/nonexistent_pragma.expect b/test/c/nonexistent_pragma.expect new file mode 100644 index 00000000..9daeafb9 --- /dev/null +++ b/test/c/nonexistent_pragma.expect @@ -0,0 +1 @@ +test diff --git a/test/c/nonexistent_pragma.sail b/test/c/nonexistent_pragma.sail new file mode 100644 index 00000000..da4b99f7 --- /dev/null +++ b/test/c/nonexistent_pragma.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +$not_a_valid_pragma test + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + print_endline("test") +} + diff --git a/test/c/unroll.expect b/test/c/unroll.expect new file mode 100644 index 00000000..355943c1 --- /dev/null +++ b/test/c/unroll.expect @@ -0,0 +1,6 @@ +fac(4) = 24 +fac(5) = 120 +fac(6) = 720 +fac2(4) = 24 +fac2(5) = 120 +fac2(6) = 720 diff --git a/test/c/unroll.sail b/test/c/unroll.sail new file mode 100644 index 00000000..c68bb49d --- /dev/null +++ b/test/c/unroll.sail @@ -0,0 +1,37 @@ +default Order dec + +$include <prelude.sail> + +/* It's hard to test that this optimization does the right thing, but +we can at least test that it doesn't do the wrong thing. */ + +$optimize unroll 20 +val fac : forall 'n, 'n >= 0. int('n) -> int +function fac(n) = { + if n == 0 then { + 1 + } else { + n * fac(n - 1) + } +} + +$optimize unroll 2 +val fac2 : forall 'n, 'n >= 0. int('n) -> int +function fac2(n) = { + if n == 0 then { + 1 + } else { + n * fac2(n - 1) + } +} + +val "print_int" : (string, int) -> unit + +function main((): unit) -> unit = { + print_int("fac(4) = ", fac(4)); + print_int("fac(5) = ", fac(5)); + print_int("fac(6) = ", fac(6)); + print_int("fac2(4) = ", fac2(4)); + print_int("fac2(5) = ", fac2(5)); + print_int("fac2(6) = ", fac2(6)) +}
\ No newline at end of file diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile index 43028fed..1f488db1 100644 --- a/test/isabelle/Makefile +++ b/test/isabelle/Makefile @@ -1,7 +1,13 @@ -CHERI_DIR = ../../cheri -AARCH64_DIR = ../../aarch64 +LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) +$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif + +SAIL_ISA_LIB = ../../lib/isabelle +CHERI_DIR ?= ../../../sail-cheri-mips/cheri +AARCH64_DIR ?= ../../aarch64 TGTS = run_cheri.native run_aarch64.native -SESSION_DIRS = -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . +SESSION_DIRS = -d $(LEM_ISA_LIB) -d $(SAIL_ISA_LIB) -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . .PHONY: all clean diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail index 99447d42..770259be 100644 --- a/test/mono/builtins.sail +++ b/test/mono/builtins.sail @@ -43,7 +43,7 @@ function test(b) = { assert(x != y, "!= by propagation"); assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice"); assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice"); - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt propagation vs literal"); assert(shl_int(5,2) == shl_int(launder_int(5),2), "shl_int"); } diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail index 9de412ac..b2c9e7ee 100644 --- a/test/mono/varpatterns.sail +++ b/test/mono/varpatterns.sail @@ -35,7 +35,7 @@ val test : bool -> unit effect {escape} function test(b) = { let 'n : {|8,16|} = if b then 8 else 16; let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 }; - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt"); } val test2 : bool -> unit effect {escape} @@ -43,7 +43,7 @@ val test2 : bool -> unit effect {escape} function test2(b) = { let 'n = (if b then 8 else 16) : {|8,16|}; let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 }; - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt"); } val test_mult : {|4,8|} -> unit effect {escape} @@ -51,7 +51,7 @@ val test_mult : {|4,8|} -> unit effect {escape} function test_mult('m) = { let 'n = 2 * 'm; let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 }; - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt"); } val run : unit -> unit effect {escape} diff --git a/test/typecheck/pass/bool_bits_mapping.sail b/test/typecheck/pass/bool_bits_mapping.sail new file mode 100644 index 00000000..7fd2bae3 --- /dev/null +++ b/test/typecheck/pass/bool_bits_mapping.sail @@ -0,0 +1,8 @@ +default Order dec + +$include <prelude.sail> + +mapping bool_bits : bool <-> bits(1) = { + true <-> 0b1, + false <-> 0b0 +} diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect index 3e2c7bde..b1597759 100644 --- a/test/typecheck/pass/bool_constraint/v1.expect +++ b/test/typecheck/pass/bool_constraint/v1.expect @@ -1,27 +1,20 @@ -Type error at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20 - - if b then n else [41m4[0m - -Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm == 3). int('m)} on 4 -Coercion failed because: - int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} - in context - * 4 == 'ex41#m - * not('b) - where - * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1 - -[41mfunction foo(b, n) = {[0m -[41m if b then n else 4[0m -[41m}[0m - - * 'ex41#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20 - - if b then n else [41m4[0m - - * 'n bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1 - -[41mfunction foo(b, n) = {[0m -[41m if b then n else 4[0m -[41m}[0m - +Type error: +[[96mbool_constraint/v1.sail[0m]:12:19-20 +12[96m |[0m if b then n else 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} on 4 + [91m |[0m Coercion failed because: + [91m |[0m int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} + [91m |[0m [[96mbool_constraint/v1.sail[0m]:11:0-13:1 + [91m |[0m 11[96m |[0mfunction foo(b, n) = { + [91m |[0m [93m |[0m[93m^---------------------[0m + [91m |[0m 13[96m |[0m} + [91m |[0m [93m |[0m[93m^[0m + [91m |[0m [93m |[0m 'b bound here + [91m |[0m [[96mbool_constraint/v1.sail[0m]:11:0-13:1 + [91m |[0m 11[96m |[0mfunction foo(b, n) = { + [91m |[0m [93m |[0m[93m^---------------------[0m + [91m |[0m 13[96m |[0m} + [91m |[0m [93m |[0m[93m^[0m + [91m |[0m [93m |[0m 'n bound here + [91m |[0m diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect index 847ef329..c7a355e1 100644 --- a/test/typecheck/pass/bool_constraint/v2.expect +++ b/test/typecheck/pass/bool_constraint/v2.expect @@ -1,5 +1,6 @@ -Type error at file "bool_constraint/v2.sail", line 38, character 5 to line 38, character 32 - - [41m_prove(constraint('n <= 14))[0m - -Cannot prove 'n <= 14 +Type error: +[[96mbool_constraint/v2.sail[0m]:38:4-32 +38[96m |[0m _prove(constraint('n <= 14)) + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'n <= 14 + [91m |[0m diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect index ca87fac1..63791a70 100644 --- a/test/typecheck/pass/bool_constraint/v3.expect +++ b/test/typecheck/pass/bool_constraint/v3.expect @@ -1,5 +1,6 @@ -Type error at file "bool_constraint/v3.sail", line 46, character 5 to line 46, character 32 - - [41m_prove(constraint('n <= 14))[0m - -Cannot prove 'n <= 14 +Type error: +[[96mbool_constraint/v3.sail[0m]:46:4-32 +46[96m |[0m _prove(constraint('n <= 14)) + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'n <= 14 + [91m |[0m diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect index 07363175..420909bf 100644 --- a/test/typecheck/pass/bool_constraint/v4.expect +++ b/test/typecheck/pass/bool_constraint/v4.expect @@ -1,5 +1,6 @@ -Type error at file "bool_constraint/v4.sail", line 46, character 5 to line 46, character 32 - - [41m_prove(constraint('n <= 13))[0m - -Cannot prove 'n <= 13 +Type error: +[[96mbool_constraint/v4.sail[0m]:46:4-32 +46[96m |[0m _prove(constraint('n <= 13)) + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'n <= 13 + [91m |[0m diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect index ab25cbc4..8c95193d 100644 --- a/test/typecheck/pass/constrained_struct/v1.expect +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -1,5 +1,6 @@ -Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 10, character 26 - -type MyStruct64 = [41mMyStruct[0m(65) - -Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct +Type error: +[[96mconstrained_struct/v1.sail[0m]:10:18-26 +10[96m |[0mtype MyStruct64 = MyStruct(65) + [91m |[0m [91m^------^[0m + [91m |[0m Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect index c3886af8..cf3b9399 100644 --- a/test/typecheck/pass/constraint_ctor/v1.expect +++ b/test/typecheck/pass/constraint_ctor/v1.expect @@ -1,5 +1,6 @@ -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 +Type error: +[[96mconstraint_ctor/v1.sail[0m]:10:2-29 +10[96m |[0m _prove(constraint('x >= 4)); + [91m |[0m [91m^-------------------------^[0m + [91m |[0m Cannot prove 'x >= 4 + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect index a315b3b7..0e56f0a4 100644 --- a/test/typecheck/pass/constraint_ctor/v2.expect +++ b/test/typecheck/pass/constraint_ctor/v2.expect @@ -1,5 +1,6 @@ -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 +Type error: +[[96mconstraint_ctor/v2.sail[0m]:18:2-30 +18[96m |[0m _prove(constraint('x >= 24)); + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'x >= 24 + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect index e0edd01a..37d1dff2 100644 --- a/test/typecheck/pass/constraint_ctor/v3.expect +++ b/test/typecheck/pass/constraint_ctor/v3.expect @@ -1,5 +1,6 @@ -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 +Type error: +[[96mconstraint_ctor/v3.sail[0m]:18:2-30 +18[96m |[0m _prove(constraint('x >= 23)); + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'x >= 23 + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect index 06eb9d22..64893e4d 100644 --- a/test/typecheck/pass/constraint_ctor/v4.expect +++ b/test/typecheck/pass/constraint_ctor/v4.expect @@ -1,5 +1,6 @@ -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 +Type error: +[[96mconstraint_ctor/v4.sail[0m]:17:33-36 +17[96m |[0mfunction bar(Bar(x as int('x)) : Bar(23)) -> unit = { + [91m |[0m [91m^-^[0m + [91m |[0m Could not prove 23 <= 22 for type constructor Bar + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect index b6df0222..fc2ef615 100644 --- a/test/typecheck/pass/constraint_ctor/v5.expect +++ b/test/typecheck/pass/constraint_ctor/v5.expect @@ -1,5 +1,6 @@ -Type error at file "constraint_ctor/v5.sail", line 27, character 3 to line 27, character 29 - - [41m_prove(constraint('x >= 4))[0m; - -Cannot prove 'x >= 4 +Type error: +[[96mconstraint_ctor/v5.sail[0m]:27:2-29 +27[96m |[0m _prove(constraint('x >= 4)); + [91m |[0m [91m^-------------------------^[0m + [91m |[0m Cannot prove 'x >= 4 + [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index fb1b2619..cc8b874f 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -1,6 +1,8 @@ -Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, character 42 - -let x : {'n, 0 <= 'n <= 33. regno('n)} = [41m4[0m - -Tried performing type coercion from int(4) to {'n, (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) +Type error: +[[96mexist_synonym/v1.sail[0m]:6:41-42 +6[96m |[0mlet x : {'n, 0 <= 'n <= 33. regno('n)} = 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4 + [91m |[0m Coercion failed because: + [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) + [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index 5bde04ba..c01d8359 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -1,6 +1,8 @@ -Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, character 41 - -let x : {'n, 0 <= 'n <= 8. regno('n)} = [41m4[0m - -Tried performing type coercion from int(4) to {'n, (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) +Type error: +[[96mexist_synonym/v2.sail[0m]:6:40-41 +6[96m |[0mlet x : {'n, 0 <= 'n <= 8. regno('n)} = 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4 + [91m |[0m Coercion failed because: + [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) + [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index a647ef00..c237ae2d 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,3 +1,3 @@ -Type error at no location information available +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) -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8) diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index d8bad777..abb232cb 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,3 +1,3 @@ -Type error at no location information available +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) -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8) diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect index 6e40adc0..2bb734aa 100644 --- a/test/typecheck/pass/function_namespace/v1.expect +++ b/test/typecheck/pass/function_namespace/v1.expect @@ -1,5 +1,6 @@ -Type error at file "function_namespace/v1.sail", line 9, character 7 to line 9, character 10 - - let [41mtest[0m = true; - -Local variable test is already bound as a function name +Type error: +[[96mfunction_namespace/v1.sail[0m]:9:6-10 +9[96m |[0m let test = true; + [91m |[0m [91m^--^[0m + [91m |[0m Local variable test is already bound as a function name + [91m |[0m diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index e81c467e..ac4428c6 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/test/typecheck/pass/global_type_var/v1.expect @@ -1,24 +1,12 @@ -Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15 - -let _ = test([41m32[0m) - -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 == 'ex14# - * ('ex14# == 32 | 'ex14# == 64) - * ('ex13# == 32 | 'ex13# == 64) - where - * '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 - - * '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 - - * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18 - -let (size as [41m'size[0m) : {|32, 64|} = 32 - +Type error: +[[96mglobal_type_var/v1.sail[0m]:23:13-15 +23[96m |[0mlet _ = test(32) + [91m |[0m [91m^^[0m + [91m |[0m Tried performing type coercion from int(32) to int('size) on 32 + [91m |[0m Coercion failed because: + [91m |[0m int(32) is not a subtype of int('size) + [91m |[0m [[96mglobal_type_var/v1.sail[0m]:5:13-18 + [91m |[0m 5[96m |[0mlet (size as 'size) : {|32, 64|} = 32 + [91m |[0m [93m |[0m [93m^---^[0m + [91m |[0m [93m |[0m 'size bound here + [91m |[0m diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index 21c4b348..93eb628b 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/test/typecheck/pass/global_type_var/v2.expect @@ -1,24 +1,12 @@ -Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15 - -let _ = test([41m64[0m) - -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 == 'ex14# - * ('ex14# == 32 | 'ex14# == 64) - * ('ex13# == 32 | 'ex13# == 64) - where - * '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 - - * '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 - - * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18 - -let (size as [41m'size[0m) : {|32, 64|} = 32 - +Type error: +[[96mglobal_type_var/v2.sail[0m]:23:13-15 +23[96m |[0mlet _ = test(64) + [91m |[0m [91m^^[0m + [91m |[0m Tried performing type coercion from int(64) to int('size) on 64 + [91m |[0m Coercion failed because: + [91m |[0m int(64) is not a subtype of int('size) + [91m |[0m [[96mglobal_type_var/v2.sail[0m]:5:13-18 + [91m |[0m 5[96m |[0mlet (size as 'size) : {|32, 64|} = 32 + [91m |[0m [93m |[0m [93m^---^[0m + [91m |[0m [93m |[0m 'size bound here + [91m |[0m diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect index 43096686..6def5172 100644 --- a/test/typecheck/pass/global_type_var/v3.expect +++ b/test/typecheck/pass/global_type_var/v3.expect @@ -1,5 +1,12 @@ -Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23 - -val test : forall [41m'size[0m. atom('size) -> unit - -type variable ('size : Int) is already bound +Type error: +[[96mglobal_type_var/v3.sail[0m]:15:23-27 +15[96m |[0m let y : atom(64) = size in + [91m |[0m [91m^--^[0m + [91m |[0m Tried performing type coercion from int('_size) to int(64) on size + [91m |[0m Coercion failed because: + [91m |[0m int('_size) is not a subtype of int(64) + [91m |[0m [[96mglobal_type_var/v3.sail[0m]:5:5-18 + [91m |[0m 5[96m |[0mlet (size as 'size) : {|32, 64|} = 32 + [91m |[0m [93m |[0m [93m^-----------^[0m + [91m |[0m [93m |[0m '_size bound here + [91m |[0m diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 95073799..c8217478 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -1,17 +1,12 @@ -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 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 3) - - Try adding named type variables for - - - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 3) - - Try adding named type variables for - - +Type error: +[[96mif_infer/v1.sail[0m]:10:10-37 +10[96m |[0m let _ = 0b100[if R then 0 else f()]; + [91m |[0m [91m^-------------------------^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 'ex40# & ('ex40# + 1) <= 3) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 'ex43# & ('ex43# + 1) <= 3) + [91m |[0m diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index afa04343..f0c2fab3 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -1,17 +1,12 @@ -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 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 4) - - Try adding named type variables for - - - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 4) - - Try adding named type variables for - - +Type error: +[[96mif_infer/v2.sail[0m]:10:10-38 +10[96m |[0m let _ = 0b1001[if R then 0 else f()]; + [91m |[0m [91m^--------------------------^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 'ex40# & ('ex40# + 1) <= 4) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 'ex43# & ('ex43# + 1) <= 4) + [91m |[0m diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect index 8b149bc8..7e0e74bb 100644 --- a/test/typecheck/pass/if_infer/v3.expect +++ b/test/typecheck/pass/if_infer/v3.expect @@ -1,7 +1,10 @@ -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 +Type error: +[[96mif_infer/v3.sail[0m]:10:10-38 +10[96m |[0m let _ = 0b1001[if R then 0 else f()]; + [91m |[0m [91m^--------------------------^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Numeric type is non-simple + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Numeric type is non-simple + [91m |[0m diff --git a/test/typecheck/pass/mutrec.sail b/test/typecheck/pass/mutrec.sail new file mode 100644 index 00000000..26dbf729 --- /dev/null +++ b/test/typecheck/pass/mutrec.sail @@ -0,0 +1,12 @@ +$include <prelude.sail> + +val f : list(int) -> int +val g : list(int) -> int + +function f([| |]) = 0 +and f(h::t) = h + g(t) +function g([||]) = 0 +and g(h::t) = f(t) - h + +val test : unit -> int +function test() = f([|1,2,3|]) diff --git a/test/typecheck/pass/nonexistent_pragma.sail b/test/typecheck/pass/nonexistent_pragma.sail new file mode 100644 index 00000000..da4b99f7 --- /dev/null +++ b/test/typecheck/pass/nonexistent_pragma.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> + +$not_a_valid_pragma test + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + print_endline("test") +} + diff --git a/test/typecheck/pass/not_pattern/v1.expect b/test/typecheck/pass/not_pattern/v1.expect index 9de82d1f..aeefb901 100644 --- a/test/typecheck/pass/not_pattern/v1.expect +++ b/test/typecheck/pass/not_pattern/v1.expect @@ -1,5 +1,6 @@ -Type error at file "not_pattern/v1.sail", line 12, character 7 to line 12, character 7 - - ~([41my[0m) => (), - -Bindings are not allowed in this context +Type error: +[[96mnot_pattern/v1.sail[0m]:12:6-7 +12[96m |[0m ~(y) => (), + [91m |[0m [91m^[0m + [91m |[0m Bindings are not allowed in this context + [91m |[0m diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail index 86294543..4433a2c3 100644 --- a/test/typecheck/pass/patternrefinement.sail +++ b/test/typecheck/pass/patternrefinement.sail @@ -12,7 +12,7 @@ val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order). (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int). - (int('n), int('m)) -> bool + (int('n), int('m)) -> bool('n == 'm) val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool diff --git a/test/typecheck/pass/true_false.sail b/test/typecheck/pass/true_false.sail new file mode 100644 index 00000000..42b175d8 --- /dev/null +++ b/test/typecheck/pass/true_false.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +function main((): unit) -> unit = { + let x: bool(false) = false; + let y: bool(true) = true; + _check(x : bool); + _check(x : bool(false)); + _not_check(x : bool(true)) +} diff --git a/test/typecheck/pass/tyvar_shadow.sail b/test/typecheck/pass/tyvar_shadow.sail new file mode 100644 index 00000000..973aa916 --- /dev/null +++ b/test/typecheck/pass/tyvar_shadow.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +function main((): unit) -> unit = { + let x as int('x) = 3; + let x as int('x) = 4; + _prove(constraint('x + 'x == 8)); + _not_prove(constraint('x + 'x == 6 | 'x + 'x == 7)); + + let y : {'n, 'n == 3. int('n)} = 3; + _prove(constraint('_y == 3)) +} + diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index 68a4ca70..ce61cf2a 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15 - - let y = [41mx[10][0m; - -No overloadings for vector_access, tried: - bitvector_access: - Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v1.sail[0m]:6:10-15 +6[96m |[0m let y = x[10]; + [91m |[0m [91m^---^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index 7ce8fd99..3d40cdb0 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15 - - let y = [41mx[10][0m; - -No overloadings for vector_access, tried: - bitvector_access: - Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v1_inc.sail[0m]:6:10-15 +6[96m |[0m let y = x[10]; + [91m |[0m [91m^---^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index d123cabd..c77ecaa7 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25 - - let z = [41m[x with 10 = y][0m; - -No overloadings for vector_update, tried: - bitvector_update: - Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_update: - Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v2.sail[0m]:7:10-25 +7[96m |[0m let z = [x with 10 = y]; + [91m |[0m [91m^-------------^[0m + [91m |[0m No overloading for vector_update, tried: + [91m |[0m [94m*[0m bitvector_update + [91m |[0m Could not resolve quantifiers for bitvector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_update + [91m |[0m Could not resolve quantifiers for plain_vector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index e7d2b52f..cff65f62 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25 - - let z = [41m[x with 10 = y][0m; - -No overloadings for vector_update, tried: - bitvector_update: - Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_update: - Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v2_inc.sail[0m]:7:10-25 +7[96m |[0m let z = [x with 10 = y]; + [91m |[0m [91m^-------------^[0m + [91m |[0m No overloading for vector_update, tried: + [91m |[0m [94m*[0m bitvector_update + [91m |[0m Could not resolve quantifiers for bitvector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_update + [91m |[0m Could not resolve quantifiers for plain_vector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect new file mode 100644 index 00000000..e3afecee --- /dev/null +++ b/test/typecheck/pass/vec_length/v3.expect @@ -0,0 +1,14 @@ +Type error: +[[96mvec_length/v3.sail[0m]:6:10-12:3 +6 [96m |[0m let y = x[ + [91m |[0m [91m^-[0m +12[96m |[0m ]; + [91m |[0m[91m--^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v3.sail b/test/typecheck/pass/vec_length/v3.sail new file mode 100644 index 00000000..8736278e --- /dev/null +++ b/test/typecheck/pass/vec_length/v3.sail @@ -0,0 +1,14 @@ +default Order dec +$include <vector_dec.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[ + + + + + 10 + ]; + () +} |