summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-07-11 16:34:33 +0100
committerAlasdair Armstrong2017-07-11 16:34:33 +0100
commitbde6c320997b104b0dcdc24259875a1791416d51 (patch)
tree0f6e1c1219df4437bdcae21f018247446997d2af /test
parent6e323bc2be0c15eb70fc71d6791881cf00c42184 (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.sail16
-rw-r--r--test/typecheck/fail/funret2.sail16
-rw-r--r--test/typecheck/fail/funret3.sail16
-rw-r--r--test/typecheck/pass/lexp_memory.sail65
-rw-r--r--test/typecheck/pass/union_infer.sail16
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)