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

3 files changed, 40 insertions, 0 deletions

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