diff options
| author | Alasdair Armstrong | 2019-03-01 16:38:03 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-03-01 16:39:13 +0000 |
| commit | 3e2cd8de57d4bc865f6b8299dd4e5689b5e8b875 (patch) | |
| tree | 58da240a2d4b79a262ee7d6b8b48c6cf672755e4 /test | |
| parent | d9db6da6d031effbf820de406f06c4ee973939a5 (diff) | |
Add a test case for previous commit
Also make unifying int against int('n) work as expected for
constructor applications.
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/existential_ast2.sail | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test/typecheck/pass/existential_ast2.sail b/test/typecheck/pass/existential_ast2.sail new file mode 100644 index 00000000..f15d1f57 --- /dev/null +++ b/test/typecheck/pass/existential_ast2.sail @@ -0,0 +1,28 @@ +default Order dec + +$include <prelude.sail> + +type datasize('n: Int) -> Bool = 'n in {32, 64} + +type regno = range(0, 31) + +union ast = { + Ctor1 : {'d, datasize('d). (nat, int('d), bits(4))}, + Ctor2 : {'d, datasize('d). (int, int('d), bits(4))}, +} + +val decode : bits(16) -> option(ast) + +function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = { + let x : {|32, 64|} = if b == 0b0 then 32 else 64; + let a = unsigned(a); + + Some(Ctor1(a, x, c)) +} + +function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = { + let x : {|32, 64|} = if b == 0b0 then 32 else 64; + let a = unsigned(a); + + Some(Ctor2(a, x, c)) +} |
