Various improvements to typechecker

Added vector concatenation patterns. Currently slightly more
restrictive than before as each subvector's length must be inferrable
from just that particular subvector - this may require additional type
annotations in certain vector patterns. How exactly weird vector
patterns, such as incrementing and decrementing vectors appearing in
the same pattern, as well as patterns with funny start indexes should
be dealt with correctly is unclear. It's probably best to be as
restrictive as possible to avoid unsoundness bugs.

Added a new option -ddump_tc_ast which dumps the (new) typechecked AST
to stdout. Also added a new option -dno_cast which disables implicit
casting in the typechecker. These options can be used in conjunction
to dump the typechecked ast (which has all implicit casts resolved),
and then re-typecheck it as a way to check that the typechecker is
indeed resolving all casts correctly, and is reconstructing a fully
type correct AST. The run_tests.sh script in test/typecheck has been
modified to do this.

Removed the dependency on Type_internal.ml from
pretty_print_sail.ml. This means that we can no longer pretty print
certain internal constructs produced by the old typechecker, but on
the plus side it means that the sail pretty printer is type system
agnostic and works with any annotation AST, irregardless of the type
of annotations. Also fixed a few bugs where certain constructs would
be pretty printed incorrectly.

4 files changed, 33 insertions, 16 deletions

diff --git a/test/typecheck/pass/mips_CP0Cause_access.sail b/test/typecheck/pass/mips_CP0Cause_access.sail
index 0ae1bb6f..c0e318c4 100644
--- a/test/typecheck/pass/mips_CP0Cause_access.sail
+++ b/test/typecheck/pass/mips_CP0Cause_access.sail
@@ -4,9 +4,9 @@
 *)
 
 val forall Num 'n, Num '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]
     
 default Order dec
 
diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail
index c7c1b502..4228a62e 100644
--- a/test/typecheck/pass/vector_access.sail
+++ b/test/typecheck/pass/vector_access.sail
@@ -4,6 +4,8 @@ val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l
 
 default Order inc
 
+overload vector_access [vector_access_inc; vector_access_dec]
+
 val bit[4] -> unit effect pure test
     
 function unit test v =
diff --git a/test/typecheck/pass/vector_access_dec.sail b/test/typecheck/pass/vector_access_dec.sail
index 7516ba91..c59100f0 100644
--- a/test/typecheck/pass/vector_access_dec.sail
+++ b/test/typecheck/pass/vector_access_dec.sail
@@ -2,6 +2,8 @@
 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]
+
 default Order dec
 
 val bit[4] -> unit effect pure test
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 49739b5a..7fca4770 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -8,24 +8,37 @@ GREEN='\033[0;32m'
 YELLOW='\033[0;33m'
 NC='\033[0m'
 
+mkdir -p $DIR/rtpass
+mkdir -p $DIR/rtfail
+
 for i in `ls $DIR/pass/`;
 do
-  printf "testing $i expecting pass: "
-  if $DIR/../../sail $1 $DIR/pass/$i 2> /dev/null;
-  then
-    printf "${GREEN}pass${NC}\n"
-  else
-    printf "${RED}fail${NC}\n"
-  fi
+    printf "testing $i expecting pass: "
+    if $DIR/../../sail -ddump_tc_ast -just_check $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
+    then
+	if $DIR/../../sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null;
+	then
+	    printf "${GREEN}pass${NC}\n"
+	else
+	    printf "${YELLOW}pass${NC}\n"
+	fi
+    else
+	printf "${RED}fail${NC}\n"
+    fi
 done
 
 for i in `ls $DIR/fail/`;
 do
-  printf "testing $i expecting fail: "
-  if $DIR/../../sail $1 $DIR/fail/$i 2> /dev/null;
-  then
-    printf "${RED}pass${NC}\n"
-  else
-    printf "${GREEN}fail${NC}\n"
-  fi
+    printf "testing $i expecting fail: "
+    if $DIR/../../sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i;
+    then
+	printf "${RED}pass${NC}\n"
+    else
+	if $DIR/../../sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null;
+	then
+	    printf "${YELLOW}fail${NC}\n"
+	else
+	    printf "${GREEN}fail${NC}\n"
+	fi
+    fi
 done