From 678d260f5b236404d39906696caf34c8ad74c4e0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Sep 2017 15:11:56 +0100 Subject: More test cases for ocaml backend --- test/ocaml/lsl/expect | 4 +++ test/ocaml/lsl/lsl.sail | 31 +++++++++++++++++++ test/ocaml/pattern1/expect | 1 + test/ocaml/pattern1/pattern.sail | 11 +++++++ test/ocaml/prelude.sail | 4 +++ test/ocaml/run_tests.sh | 5 ++- test/run_tests.sh | 7 +++++ test/typecheck/run_tests.sh | 66 ++++++++++++++++++++-------------------- 8 files changed, 95 insertions(+), 34 deletions(-) create mode 100644 test/ocaml/lsl/expect create mode 100644 test/ocaml/lsl/lsl.sail create mode 100644 test/ocaml/pattern1/expect create mode 100644 test/ocaml/pattern1/pattern.sail create mode 100755 test/run_tests.sh (limited to 'test') diff --git a/test/ocaml/lsl/expect b/test/ocaml/lsl/expect new file mode 100644 index 00000000..c72d1eb8 --- /dev/null +++ b/test/ocaml/lsl/expect @@ -0,0 +1,4 @@ +pass +pass +pass +pass diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail new file mode 100644 index 00000000..fdb9dc43 --- /dev/null +++ b/test/ocaml/lsl/lsl.sail @@ -0,0 +1,31 @@ + +val forall Num 'n, 'n >= 0. [:'n:] -> bit['n] effect pure zeros + +function zeros n = replicate_bits(0b0, sizeof 'n) + +val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> (bit['n], bit) effect pure lslc + +function lslc (vec, shift) = { + assert(constraint('shift >= 1), "shift must be positive"); + (bit['shift + 'n]) extended := vec : zeros(shift); + (bit['n]) result := extended[sizeof 'n - 1 .. 0]; + (bit) c := extended[sizeof 'n]; + return (result, c) +} + +val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> bit['n] effect pure lsl + +function lsl (vec, shift) = + if shift == 0 + then vec + else let (result, _) = lslc(vec, shift) in result + +val unit -> unit effect pure main + +function main () = { + print(if lsl(0b0110,1) == 0b1100 then "pass" else "fail"); + print(if lsl(0b1111,2) == 0b1100 then "pass" else "fail"); + print(if lsl(0x0F,4) == 0xF0 then "pass" else "fail"); + let (result, c) = lslc(0xF000,2) in + print(if result == 0xC000 & c == bitone then "pass" else "fail") +} diff --git a/test/ocaml/pattern1/expect b/test/ocaml/pattern1/expect new file mode 100644 index 00000000..2ae28399 --- /dev/null +++ b/test/ocaml/pattern1/expect @@ -0,0 +1 @@ +pass diff --git a/test/ocaml/pattern1/pattern.sail b/test/ocaml/pattern1/pattern.sail new file mode 100644 index 00000000..a2314adc --- /dev/null +++ b/test/ocaml/pattern1/pattern.sail @@ -0,0 +1,11 @@ + +val unit -> unit effect pure main + +function main () = { + vec := 0x4F; + switch vec { + case (0b01 : (bit[2]) x : 0xF) -> + if (x == 0b00) then print("pass") else print("x is incorrect") + case _ -> print("pattern fail") + } +} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 2526d109..cbe1927d 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -15,6 +15,10 @@ val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "subrange" +(* FIXME: rewriter shouldn't assume this exists *) +val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure bitvector_subrange_dec = "subrange" + val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int) -> 'a effect pure vector_access = "access" val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int, 'a) -> vector<'n - 1, 'n, dec, 'a> effect pure vector_update = "update" diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index d01535b6..4454aa48 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -2,6 +2,7 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +cd $DIR SAILDIR="$DIR/../.." RED='\033[0;31m' @@ -49,7 +50,7 @@ printf "\n" >> $DIR/tests.xml for i in `ls -d */`; do cd $DIR/$i; - if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail`; + if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null; then ./out > result; if diff expect result; @@ -66,4 +67,6 @@ do fi done +finish_suite "Ocaml testing" + printf "\n" >> $DIR/tests.xml diff --git a/test/run_tests.sh b/test/run_tests.sh new file mode 100755 index 00000000..380ebb18 --- /dev/null +++ b/test/run_tests.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +$DIR/typecheck/run_tests.sh +$DIR/ocaml/run_tests.sh diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index e83cc20b..41a19cb4 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -97,43 +97,43 @@ done finish_suite "Expecting fail" -function test_lem { - for i in `ls $DIR/pass/`; - do - # MIPS requires an additional library, Mips_extras_embed. - # It might be useful to allow adding options for specific test cases. - # For now, include the library for all test cases, which doesn't seem to hurt. - if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null - then - green "generated lem for $1/$i" "pass" - - cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ - # Test sequential embedding for now - # TODO: Add tests for the free monad - if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null - then - green "typechecking lem for $1/$i" "pass" - else - red "typechecking lem for $1/$i" "fail" - fi - else - red "generated lem for $1/$i" "fail" - red "typechecking lem for $1/$i" "fail" - fi - done -} +# function test_lem { +# for i in `ls $DIR/pass/`; +# do +# # MIPS requires an additional library, Mips_extras_embed. +# # It might be useful to allow adding options for specific test cases. +# # For now, include the library for all test cases, which doesn't seem to hurt. +# if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null +# then +# green "generated lem for $1/$i" "pass" + +# cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ +# # Test sequential embedding for now +# # TODO: Add tests for the free monad +# if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null +# then +# green "typechecking lem for $1/$i" "pass" +# else +# red "typechecking lem for $1/$i" "fail" +# fi +# else +# red "generated lem for $1/$i" "fail" +# red "typechecking lem for $1/$i" "fail" +# fi +# done +# } -test_lem pass +# test_lem pass -finish_suite "Lem generation 1" +# finish_suite "Lem generation 1" -test_lem rtpass +# test_lem rtpass -finish_suite "Lem generation 2" +# finish_suite "Lem generation 2" # function test_ocaml { # for i in `ls $DIR/pass/`; -- cgit v1.2.3 From 8124c487b576661dfa7a0833415d07d0978bc43e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Sep 2017 15:33:24 +0100 Subject: Testing typedef generation for ocaml --- test/ocaml/types/expect | 5 +++++ test/ocaml/types/types.sail | 37 +++++++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+) create mode 100644 test/ocaml/types/expect create mode 100644 test/ocaml/types/types.sail (limited to 'test') diff --git a/test/ocaml/types/expect b/test/ocaml/types/expect new file mode 100644 index 00000000..747ef4c9 --- /dev/null +++ b/test/ocaml/types/expect @@ -0,0 +1,5 @@ +pass +pass +pass +pass +pass diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail new file mode 100644 index 00000000..be3606d6 --- /dev/null +++ b/test/ocaml/types/types.sail @@ -0,0 +1,37 @@ + +typedef signal = enumerate {Low; High} + +typedef enum_single = enumerate {SingleConstructor} + +typedef byte = bit[8] +typedef b32 = bit[32] +typedef b64 = bit[64] + +register b64 R64 +register b32 R32 +register byte R8 + +register signal SIGNALREG + +typedef TestStruct = const struct { + bit[2] field1; + byte field2; + bool field3 +} + +register TestStruct SREG + +val unit -> unit effect {rreg, wreg} main + +function main () = { + R8 := 0xFF; + SIGNALREG := Low; + print(if SIGNALREG == Low then "pass" else "fail"); + SIGNALREG := High; + print(if SIGNALREG == High then "pass" else "fail"); + SREG.field1 := 0b00; + print(if SREG.field1 == 0b00 then "pass" else "faiL"); + SREG.field1 := 0b11; + print(if SREG.field1 == 0b11 then "pass" else "faiL"); + print("pass") +} -- cgit v1.2.3 From 842165c1171fde332bd42e7520338c59a797f76b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 7 Sep 2017 16:54:20 +0100 Subject: Add ocaml run-time and updates to sail for ocaml backend --- test/ocaml/types/types.sail | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test') diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail index be3606d6..8f50e057 100644 --- a/test/ocaml/types/types.sail +++ b/test/ocaml/types/types.sail @@ -21,6 +21,13 @@ typedef TestStruct = const struct { register TestStruct SREG +typedef option = const union forall Type 'a. { + None; + 'a Some +} + +register (option) OREG + val unit -> unit effect {rreg, wreg} main function main () = { -- cgit v1.2.3 From aa1f89abb2f42d085bd123147144c9c5c7ceb22f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 13 Sep 2017 16:27:34 +0100 Subject: Work on improving Sail error messages - Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases --- test/typecheck/fail/mismatch_return.sail | 7 +++++++ test/typecheck/fail/pure_record_arity.sail | 25 +++++++++++++++++++++++++ test/typecheck/fail/vector_append_old.sail | 14 ++++++++++++++ test/typecheck/pass/exist_subrange.sail | 12 ++++++++++++ test/typecheck/pass/exist_true.sail | 7 +++++++ test/typecheck/pass/pure_record2.sail | 22 ++++++++++++++++++++++ test/typecheck/pass/pure_record3.sail | 25 +++++++++++++++++++++++++ test/typecheck/pass/vec_pat1.sail | 2 +- test/typecheck/pass/vector_append.sail | 6 +++--- 9 files changed, 116 insertions(+), 4 deletions(-) create mode 100644 test/typecheck/fail/mismatch_return.sail create mode 100644 test/typecheck/fail/pure_record_arity.sail create mode 100644 test/typecheck/fail/vector_append_old.sail create mode 100644 test/typecheck/pass/exist_subrange.sail create mode 100644 test/typecheck/pass/exist_true.sail create mode 100644 test/typecheck/pass/pure_record2.sail create mode 100644 test/typecheck/pass/pure_record3.sail (limited to 'test') diff --git a/test/typecheck/fail/mismatch_return.sail b/test/typecheck/fail/mismatch_return.sail new file mode 100644 index 00000000..85b8b636 --- /dev/null +++ b/test/typecheck/fail/mismatch_return.sail @@ -0,0 +1,7 @@ + +val unit -> unit effect pure test + +function int test () = +{ + () +} diff --git a/test/typecheck/fail/pure_record_arity.sail b/test/typecheck/fail/pure_record_arity.sail new file mode 100644 index 00000000..846df2c3 --- /dev/null +++ b/test/typecheck/fail/pure_record_arity.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State procState + +let (State) myStateM = { + (State) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State) myState1 := undefined; + (State) myState2 := { N = undefined; Z = 0b1 }; + (State) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/fail/vector_append_old.sail b/test/typecheck/fail/vector_append_old.sail new file mode 100644 index 00000000..fb6018b9 --- /dev/null +++ b/test/typecheck/fail/vector_append_old.sail @@ -0,0 +1,14 @@ + +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" + +default Order inc + +val (bit[4], bit[4]) -> bit[8] effect pure test + +function bit[8] test (v1, v2) = +{ + zv := vector_append(v1, v2); + zv := v1 : v2; + zv +} diff --git a/test/typecheck/pass/exist_subrange.sail b/test/typecheck/pass/exist_subrange.sail new file mode 100644 index 00000000..de867b75 --- /dev/null +++ b/test/typecheck/pass/exist_subrange.sail @@ -0,0 +1,12 @@ +default Order dec + +val forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange + +function unit test ((bit[6]) xs) = +{ + (int) len := 4; + (exist 'n. [:'n:]) len := 5; + ys := xs[len .. 0]; + () +} diff --git a/test/typecheck/pass/exist_true.sail b/test/typecheck/pass/exist_true.sail new file mode 100644 index 00000000..a30fb87b --- /dev/null +++ b/test/typecheck/pass/exist_true.sail @@ -0,0 +1,7 @@ + +function unit test () = +{ + (exist 'n. [:'n:]) x := 4; + (exist 'n, true. [:'n:]) y := 5; + () +} diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail new file mode 100644 index 00000000..a0a85313 --- /dev/null +++ b/test/typecheck/pass/pure_record2.sail @@ -0,0 +1,22 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +let (State) myStateM = { + (State) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State) myState2 := { N = undefined; Z = 0b1 }; + (State) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail new file mode 100644 index 00000000..61d74ebf --- /dev/null +++ b/test/typecheck/pass/pure_record3.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State procState + +let (State) myStateM = { + (State) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State) myState1 := undefined; + (State) myState2 := { N = undefined; Z = 0b1 }; + (State) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index fe9b4a0a..b22f0029 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -10,7 +10,7 @@ val forall Num 'n, Num 'm, Num 'o, Num 'p. effect pure bitvector_concat overload (deinfix +) [bv_add] -overload vector_append [bitvector_concat] +overload append [bitvector_concat] val (bit[3], bit[3]) -> bit[3] effect pure test diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index 17db3fbd..df610fb1 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,14 +1,14 @@ val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure append = "bitvector_concat" default Order inc val (bit[4], bit[4]) -> bit[8] effect pure test - + function bit[8] test (v1, v2) = { - zv := vector_append(v1, v2); + zv := append(v1, v2); zv := v1 : v2; zv } -- cgit v1.2.3 From cb90735550541fa6752aaad82ff809d84e6c5f88 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 13 Sep 2017 19:03:31 +0100 Subject: Fix some more test cases --- test/typecheck/pass/lexp_memory.sail | 5 ++++- test/typecheck/pass/mips_CP0Cause_BD_assign1.sail | 9 +++++++-- test/typecheck/pass/mips_CP0Cause_BD_assign2.sail | 9 +++++++-- test/typecheck/pass/set_mark.sail | 7 ++++++- test/typecheck/pass/set_mark2.sail | 8 +++++++- test/typecheck/pass/varity.sail | 4 ++++ test/typecheck/pass/vector_synonym_cast.sail | 2 +- 7 files changed, 36 insertions(+), 8 deletions(-) (limited to 'test') diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail index 83313ac7..cc84130f 100644 --- a/test/typecheck/pass/lexp_memory.sail +++ b/test/typecheck/pass/lexp_memory.sail @@ -48,7 +48,10 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or overload (deinfix ==) [eq_vec] -val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i) val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index 7808b2c0..0160dd8a 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,5 +1,10 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec + +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) default Order dec diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail index 26f161e2..847bca60 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -1,6 +1,11 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) + default Order dec typedef CauseReg = register bits [ 31 : 0 ] { diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail index 7bc7370b..af0b5ba2 100644 --- a/test/typecheck/pass/set_mark.sail +++ b/test/typecheck/pass/set_mark.sail @@ -1,5 +1,10 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail index cabfb1af..591c17ad 100644 --- a/test/typecheck/pass/set_mark2.sail +++ b/test/typecheck/pass/set_mark2.sail @@ -1,4 +1,10 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail index d196f777..750d70eb 100644 --- a/test/typecheck/pass/varity.sail +++ b/test/typecheck/pass/varity.sail @@ -3,6 +3,10 @@ val int -> unit effect pure f1 val (int, int) -> unit effect pure f2 val (int, int, int) -> unit effect pure f3 +function f1 (i1) = () +function f2 (i1, i2) = () +function f3 (i1, i2, i3) = () + overload f [f1; f2; f3] val unit -> unit effect pure test diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail index f1de42e9..bd0acaa6 100644 --- a/test/typecheck/pass/vector_synonym_cast.sail +++ b/test/typecheck/pass/vector_synonym_cast.sail @@ -1,7 +1,7 @@ typedef vecsyn = vector<0,1,dec,bit> -val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec +val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec val vector<1,1,dec,bit> -> vecsyn effect pure test -- cgit v1.2.3