diff options
| author | Alasdair Armstrong | 2017-07-11 16:34:33 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-11 16:34:33 +0100 |
| commit | bde6c320997b104b0dcdc24259875a1791416d51 (patch) | |
| tree | 0f6e1c1219df4437bdcae21f018247446997d2af /test | |
| parent | 6e323bc2be0c15eb70fc71d6791881cf00c42184 (diff) | |
Various typechecker improvements:
* Fixed a bug where non-polymorphic function return types could be incorrect
* Added support for LEXP_memory AST node
* Flow typing constraint generation for all inequality operators
* Better support for increasing vector indices in field access expressions
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/fail/funret1.sail | 16 | ||||
| -rw-r--r-- | test/typecheck/fail/funret2.sail | 16 | ||||
| -rw-r--r-- | test/typecheck/fail/funret3.sail | 16 | ||||
| -rw-r--r-- | test/typecheck/pass/lexp_memory.sail | 65 | ||||
| -rw-r--r-- | test/typecheck/pass/union_infer.sail | 16 |
5 files changed, 129 insertions, 0 deletions
diff --git a/test/typecheck/fail/funret1.sail b/test/typecheck/fail/funret1.sail new file mode 100644 index 00000000..09a4fd54 --- /dev/null +++ b/test/typecheck/fail/funret1.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + +let (option<int>) x = C + diff --git a/test/typecheck/fail/funret2.sail b/test/typecheck/fail/funret2.sail new file mode 100644 index 00000000..19536599 --- /dev/null +++ b/test/typecheck/fail/funret2.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<int> test2 () = C diff --git a/test/typecheck/fail/funret3.sail b/test/typecheck/fail/funret3.sail new file mode 100644 index 00000000..d178f2ad --- /dev/null +++ b/test/typecheck/fail/funret3.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<(option<int>)> test () = Some(C) diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail new file mode 100644 index 00000000..83313ac7 --- /dev/null +++ b/test/typecheck/pass/lexp_memory.sail @@ -0,0 +1,65 @@ +default Order dec + +register (bit[64]) GPR00 (* should never be read or written *) +register (bit[64]) GPR01 +register (bit[64]) GPR02 +register (bit[64]) GPR03 +register (bit[64]) GPR04 +register (bit[64]) GPR05 +register (bit[64]) GPR06 +register (bit[64]) GPR07 +register (bit[64]) GPR08 +register (bit[64]) GPR09 +register (bit[64]) GPR10 +register (bit[64]) GPR11 +register (bit[64]) GPR12 +register (bit[64]) GPR13 +register (bit[64]) GPR14 +register (bit[64]) GPR15 +register (bit[64]) GPR16 +register (bit[64]) GPR17 +register (bit[64]) GPR18 +register (bit[64]) GPR19 +register (bit[64]) GPR20 +register (bit[64]) GPR21 +register (bit[64]) GPR22 +register (bit[64]) GPR23 +register (bit[64]) GPR24 +register (bit[64]) GPR25 +register (bit[64]) GPR26 +register (bit[64]) GPR27 +register (bit[64]) GPR28 +register (bit[64]) GPR29 +register (bit[64]) GPR30 +register (bit[64]) GPR31 + +let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = + [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, + GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, + GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 + ] + +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec + +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 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 + +val (bit[5], bit[64]) -> unit effect {wreg} wGPR + +function unit wGPR (idx, v) = +{ + if idx == 0 then () else GPR[idx] := v +} + +function unit test () = +{ + wGPR(0b00001) := 0 +} diff --git a/test/typecheck/pass/union_infer.sail b/test/typecheck/pass/union_infer.sail new file mode 100644 index 00000000..397525e0 --- /dev/null +++ b/test/typecheck/pass/union_infer.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<Test> test () = Some(C) |
