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.

0 files changed, 0 insertions, 0 deletions