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.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 63e42219..42d1402b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -90,6 +90,8 @@ let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tann
 
 let opt_new_typecheck = ref false
 let opt_just_check = ref false
+let opt_ddump_tc_ast = ref false
+let opt_dno_cast = ref false
                                         
 let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs =
   let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
@@ -101,7 +103,10 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
 		                                     | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec
 						     | _ -> Type_internal.Oinc)};} in
   if !opt_new_typecheck
-  then let _ = Type_check_new.check Type_check_new.initial_env defs in ()
+  then
+    let ienv = if !opt_dno_cast then Type_check_new.Env.no_casts Type_check_new.initial_env else Type_check_new.initial_env in
+    let ast, _ = Type_check_new.check ienv defs in
+    if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else ()
   else ();
   if !opt_just_check
   then exit 0