diff options
Diffstat (limited to 'test')
| -rwxr-xr-x | test/run_tests.sh | 5 | ||||
| -rw-r--r-- | test/typecheck/fail/pure_record_arity2.sail | 25 |
2 files changed, 28 insertions, 2 deletions
diff --git a/test/run_tests.sh b/test/run_tests.sh index 380ebb18..73f622c7 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -3,5 +3,6 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" -$DIR/typecheck/run_tests.sh -$DIR/ocaml/run_tests.sh +cd $DIR/.. +./test/typecheck/run_tests.sh +./test/ocaml/run_tests.sh diff --git a/test/typecheck/fail/pure_record_arity2.sail b/test/typecheck/fail/pure_record_arity2.sail new file mode 100644 index 00000000..a9566da8 --- /dev/null +++ b/test/typecheck/fail/pure_record_arity2.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<bit,inc> procState + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState1 := undefined; + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} |