From c741e731afe4a6d2c65d43ca299a1a48a1534ec0 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 14 Mar 2019 17:27:07 +0000
Subject: Add various useful methods to interactive mode

:def <definition> evaluates a top-level definition
:(b)ind <id> : <type> creates an identifier within the interactive type-checking environment
:let <id> = <expression> defines an identifier

Using :def the following now works and brings the correct vector
operations into scope.

:def default Order dec
:load lib/prelude.sail

Also fix a type-variable shadowing bug
---
 test/typecheck/pass/shadow_let.sail      | 14 ++++++++++++++
 test/typecheck/pass/shadow_let/v1.expect | 12 ++++++++++++
 test/typecheck/pass/shadow_let/v1.sail   | 14 ++++++++++++++
 3 files changed, 40 insertions(+)
 create mode 100644 test/typecheck/pass/shadow_let.sail
 create mode 100644 test/typecheck/pass/shadow_let/v1.expect
 create mode 100644 test/typecheck/pass/shadow_let/v1.sail

(limited to 'test')

diff --git a/test/typecheck/pass/shadow_let.sail b/test/typecheck/pass/shadow_let.sail
new file mode 100644
index 00000000..8a30744c
--- /dev/null
+++ b/test/typecheck/pass/shadow_let.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  foo(y);
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/shadow_let/v1.expect b/test/typecheck/pass/shadow_let/v1.expect
new file mode 100644
index 00000000..3cd21dc0
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.expect
@@ -0,0 +1,12 @@
+Type error:
+[shadow_let/v1.sail]:13:6-7
+13 |  bar(y);
+   |      ^
+   | Tried performing type coercion from int('_x#1) to int(2) on y
+   | Coercion failed because:
+   | int('_x#1) is not a subtype of int(2)
+   | [shadow_let/v1.sail]:9:6-8
+   | 9 |  let 'x : {'z, 'z == 1. int('z)} = 1;
+   |   |      ^^
+   |   | '_x#1 bound here
+   | 
diff --git a/test/typecheck/pass/shadow_let/v1.sail b/test/typecheck/pass/shadow_let/v1.sail
new file mode 100644
index 00000000..d7dc20a5
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  bar(y);
+}
\ No newline at end of file
-- 
cgit v1.2.3