Merge remote-tracking branch 'origin/sail_new_tc' into experiments

5 files changed, 69 insertions, 0 deletions

diff --git a/test/typecheck/fail/overlap_field_wreg.sail b/test/typecheck/fail/overlap_field_wreg.sail
new file mode 100644
index 00000000..4c4d858d
--- /dev/null
+++ b/test/typecheck/fail/overlap_field_wreg.sail
@@ -0,0 +1,13 @@
+
+typedef A = const struct {bool field_A; int shared}
+typedef B = const struct {bool field_B; int shared}
+
+val (bool, int) -> A effect {undef, wreg} makeA
+
+function makeA (x, y) =
+{
+  (A) record := undefined;
+  record.field_A := x;
+  record.shared := y;
+  record
+}
diff --git a/test/typecheck/pass/add_real.sail b/test/typecheck/pass/add_real.sail
new file mode 100644
index 00000000..38a9cff3
--- /dev/null
+++ b/test/typecheck/pass/add_real.sail
@@ -0,0 +1,5 @@
+val (real, real) -> real effect pure add_real
+
+overload (deinfix +) [add_real]
+
+let (real) r = 2.2 + 0.2
diff --git a/test/typecheck/pass/add_vec_exts_no_annot.sail b/test/typecheck/pass/add_vec_exts_no_annot.sail
new file mode 100644
index 00000000..54aa2d40
--- /dev/null
+++ b/test/typecheck/pass/add_vec_exts_no_annot.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTS [exts]
+
+val forall Nat 'n, Nat 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+overload (deinfix +) [add_vec]
+
+val (bit[32], bit[32]) -> unit effect pure test
+
+function test (x, y) =
+{
+  let (bit[64]) z = add_vec(exts(x), exts(y)) in
+  ()
+}
diff --git a/test/typecheck/pass/add_vec_exts_no_annot_overload.sail b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail
new file mode 100644
index 00000000..01e3bf7c
--- /dev/null
+++ b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTS [exts]
+
+val forall Nat 'n, Nat 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+overload (deinfix +) [add_vec]
+
+val (bit[32], bit[32]) -> unit effect pure test
+
+function test (x, y) =
+{
+  let (bit[64]) z = EXTS(x) + EXTS(y) in
+  ()
+}
diff --git a/test/typecheck/pass/overlap_field.sail b/test/typecheck/pass/overlap_field.sail
new file mode 100644
index 00000000..82e685ee
--- /dev/null
+++ b/test/typecheck/pass/overlap_field.sail
@@ -0,0 +1,13 @@
+
+typedef A = const struct {bool field_A; int shared}
+typedef B = const struct {bool field_B; int shared}
+
+val (bool, int) -> A effect {undef} makeA
+
+function makeA (x, y) =
+{
+  (A) record := undefined;
+  record.field_A := x;
+  record.shared := y;
+  record
+}