diff options
| author | Alasdair Armstrong | 2017-08-01 17:29:43 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-08-01 17:29:43 +0100 |
| commit | 886ac51d3d53c4fd6de060dd99ca7decd358cd06 (patch) | |
| tree | d8378e9fa9b141e84d6ca808339b1fbab4eb284b /test | |
| parent | 364a2755dec816da0e660d050d9ef78c466e53d7 (diff) | |
Added additional test for existentials
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/exist_pattern.sail | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail new file mode 100644 index 00000000..46913de4 --- /dev/null +++ b/test/typecheck/pass/exist_pattern.sail @@ -0,0 +1,38 @@ +default Order inc + +register nat n +register nat x +register nat y + +typedef wordsize = exist 'n, 'n IN {8,16,32}. [|'n|] +let (wordsize) word = ([|8|]) 8 + +function nat main () = { + + (* works - x and y are set to 42 *) + n := 1; + y := + (switch n { + case 0 -> { x := 21; x } + case 1 -> { x := 42; x } + case z -> { x := 99; x } + }); + + switch word { + case ([|8|]) 8 -> { x:= 32; } + case ([|16|]) 16 -> { x:= 64; } + case ([|32|]) 32 -> { x:= 128; } + }; + + switch 0b010101 { + case (0b01:(bit[1]) _:0b101) -> n:= 42 + case _ -> n:=0 + }; + + n := 3; + switch n { + case 0 -> { 21 } + case 1 -> { 42 } + case u -> { 99 } + }; +} |
