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.

7 files changed, 90 insertions, 26 deletions

diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 9a002454..67475616 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -44,9 +44,9 @@ open Ast
 open Type_internal
 
 (* Prints the defs following source syntax *)
-val pp_defs : out_channel -> tannot defs -> unit
+val pp_defs : out_channel -> 'a defs -> unit 
 val pp_exp : Buffer.t -> exp -> unit
-val pat_to_string : tannot pat -> string
+val pat_to_string : 'a pat -> string
 
 (* Prints on formatter the defs as Lem Ast nodes *)
 val pp_lem_defs : Format.formatter -> tannot defs -> unit
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 22cb707b..9c33c841 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -40,7 +40,7 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
-open Type_internal
+(* open Type_internal *)
 open Ast
 open PPrint
 open Pretty_print_common
@@ -238,6 +238,7 @@ let doc_exp, doc_let =
   | E_id id -> doc_id id
   | E_lit lit -> doc_lit lit
   | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e))
+                            (*
   | E_internal_cast((_,NoTyp),e) -> atomic_exp e
   | E_internal_cast((_,Base((_,t),_,_,_,_,bindings)), (E_aux(_,(_,eannot)) as e)) ->
       (match t.t,eannot with
@@ -247,6 +248,7 @@ let doc_exp, doc_let =
       | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_,_,_)
           when nexp_eq n1 n2 -> atomic_exp e
       | _ -> prefix 2 1 (parens (doc_typ (t_to_typ t))) (group (atomic_exp e)))
+                             *)
   | E_tuple exps ->
       parens (separate_map comma exp exps)
   | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -325,6 +327,7 @@ let doc_exp, doc_let =
   (* doc_op (doc_id op) (exp l) (exp r) *)
   | E_comment s -> comment (string s)
   | E_comment_struc e -> comment (exp e)
+                                 (*
   | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*)
     (match t.t with
       | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
@@ -342,7 +345,7 @@ let doc_exp, doc_let =
       | _ ->  raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t)))
   | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away"))
   | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
-
+                                  *)
   and let_exp (LB_aux(lb,_)) = match lb with
     | LB_val_explicit(ts,pat,e) ->
       (match ts with
@@ -391,16 +394,18 @@ let doc_exp, doc_let =
 let doc_default (DT_aux(df,_)) = match df with
   | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v]
   | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id]
-  | DT_order(ord) -> separate space [string "default"; string "order"; doc_ord ord]
+  | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
 
 let doc_spec (VS_aux(v,_)) = match v with
   | VS_val_spec(ts,id) ->
-      separate space [string "val"; doc_typscm ts; doc_id id]
+     separate space [string "val"; doc_typscm ts; doc_id id]
+  | VS_cast_spec (ts, id) ->
+     separate space [string "val"; string "cast"; doc_typscm ts; doc_id id]
   | VS_extern_no_rename(ts,id) ->
-      separate space [string "val"; string "extern"; doc_typscm ts; doc_id id]
+     separate space [string "val"; string "extern"; doc_typscm ts; doc_id id]
   | VS_extern_spec(ts,id,s) ->
-      separate space [string "val"; string "extern"; doc_typscm ts;
-      doc_op equals (doc_id id) (dquotes (string s))]
+     separate space [string "val"; string "extern"; doc_typscm ts;
+                     doc_op equals (doc_id id) (dquotes (string s))]
 
 let doc_namescm (Name_sect_aux(ns,_)) = match ns with
   | Name_sect_none -> empty
@@ -549,6 +554,9 @@ let rec doc_def def = group (match def with
   | DEF_val lbind -> doc_let lbind
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> doc_scattered sdef
+  | DEF_overload (id, ids) ->
+      let ids_doc = group (separate_map (semi ^^ break 1) doc_id ids) in
+      string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc
   | DEF_comm (DC_comm s) -> comment (string s)
   | DEF_comm (DC_comm_struct d) -> comment (doc_def d)
   ) ^^ hardline
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
diff --git a/src/process_file.mli b/src/process_file.mli
index 4c703dd2..aa8d3265 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -50,7 +50,9 @@ val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot As
 
 val opt_new_typecheck : bool ref
 val opt_just_check : bool ref
-                                                                              
+val opt_ddump_tc_ast : bool ref
+val opt_dno_cast : bool ref
+
 type out_type =
   | Lem_ast_out
   | Lem_out of string option (* If present, the string is a file to open in the lem backend*)
diff --git a/src/sail.ml b/src/sail.ml
index 0bdcf4ab..452e6e72 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -88,10 +88,16 @@ let options = Arg.align ([
     " (debug) skip constraint resolution in type-checking");
   ( "-new_typecheck",
     Arg.Set opt_new_typecheck,
-    " use new typechecker with Z3 constraint solving (experimental)");
+    " (experimental) use new typechecker with Z3 constraint solving");
   ( "-just_check",
     Arg.Tuple [Arg.Set opt_new_typecheck; Arg.Set opt_just_check],
-    " terminate immediately after typechecking, implies -new_typecheck");
+    " (experimental) terminate immediately after typechecking, implies -new_typecheck");
+  ( "-ddump_tc_ast",
+    Arg.Set opt_ddump_tc_ast,
+    " (debug) dump the typechecked ast to stdout");
+  ( "-dno_cast",
+    Arg.Set opt_dno_cast,
+    " (debug) typecheck without any implicit casting");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index cc232eb8..5f997409 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -98,6 +98,8 @@ and map_pat_annot_aux f = function
   | P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats)
   | P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
   | P_list pats -> P_list (List.map (map_pat_annot f) pats)
+  | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats)
+  | P_vector pats -> P_vector (List.map (map_pat_annot f) pats)
   | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot map annot in pat"
 and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
 and map_letbind_annot_aux f = function
@@ -262,6 +264,7 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]"
   | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]"
   | E_vector_subrange (v, n1, n2) -> string_of_exp v ^ "[" ^ string_of_exp n1 ^ " .. " ^ string_of_exp n2 ^ "]"
+  | E_vector_append (v1, v2) -> string_of_exp v1 ^ " : " ^ string_of_exp v2
   | E_if (cond, then_branch, else_branch) ->
      "if " ^ string_of_exp cond ^ " then " ^ string_of_exp then_branch ^ " else " ^ string_of_exp else_branch
   | E_field (exp, id) -> string_of_exp exp ^ "." ^ string_of_id id
@@ -1084,6 +1087,9 @@ let subtyp l env typ1 typ2 =
                     ^ " is not a subtype of " ^ string_of_typ typ2
                     ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
 
+let typ_equality l env typ1 typ2 =
+  subtyp l env typ1 typ2; subtyp l env typ2 typ1
+                 
 let rec nexp_frees (Nexp_aux (nexp, l)) =
   match nexp with
   | Nexp_id _ -> typ_error l "Unimplemented Nexp_id in nexp_frees"
@@ -1254,6 +1260,13 @@ let vector_typ n m ord typ =
 
 let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ
 
+let lvector_typ env l typ =
+  match Env.get_default_order env with
+  | Ord_aux (Ord_inc, _) as ord ->
+     vector_typ (nconstant 0) l ord typ
+  | Ord_aux (Ord_dec, _) as ord ->
+     vector_typ (nminus l (nconstant 1)) l ord typ
+                                         
 let infer_lit env (L_aux (lit_aux, l) as lit) =
   match lit_aux with
   | L_unit -> mk_typ (Typ_id (mk_id "unit"))
@@ -1343,6 +1356,10 @@ let typ_of (E_aux (_, (_, tannot))) = match tannot with
   | Some (_, typ) -> typ
   | None -> assert false
 
+let pat_typ_of (P_aux (_, (_, tannot))) = match tannot with
+  | Some (_, typ) -> typ
+  | None -> assert false
+                   
 let crule r env exp typ =
   incr depth;
   typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ);
@@ -1494,6 +1511,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
   let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in
+  let switch_typ (P_aux (pat_aux, (l, Some (env, _)))) typ = P_aux (pat_aux, (l, Some (env, typ))) in
   match pat_aux with
   | P_id v ->
      begin
@@ -1504,12 +1522,6 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env
      end
   | P_wild -> annot_pat P_wild typ, env
-  | P_typ (typ_annot, pat) ->
-     begin
-       subtyp l env typ_annot typ;
-       let (typed_pat, env) = bind_pat env pat typ_annot in
-       annot_pat (P_typ (typ_annot, typed_pat)) typ, env
-     end
   | P_tup pats ->
      begin
        match typ_aux with
@@ -1521,16 +1533,46 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
             try List.fold_left2 bind_tuple_pat ([], env) pats typs with
             | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length"
           in
-          annot_pat (P_tup tpats) typ, env
+          annot_pat (P_tup (List.rev tpats)) typ, env
        | _ -> typ_error l "Cannot bind tuple pattern against non tuple type"
      end
-  | P_lit lit ->
+  | _ ->
+     let (inferred_pat, env) = infer_pat env pat in
+     subtyp l env (pat_typ_of inferred_pat) typ;
+     switch_typ inferred_pat typ, env
+
+and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
+  let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in
+  match pat_aux with
+  | P_id v ->
      begin
-       let lit_typ = infer_lit env lit in
-       subtyp l env lit_typ typ; (* CHECK: is the the correct way round? *)
-       annot_pat (P_lit lit) typ, env
+       match Env.lookup_id v env with
+       | Local (Immutable, _) | Unbound ->
+          typ_error l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation")
+       | Local (Mutable, _) | Register _ ->
+          typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
+       | Enum enum -> annot_pat (P_id v) enum, env
      end
-  | _ -> typ_error l ("Unhandled pat " ^ string_of_pat pat)
+  | P_typ (typ_annot, pat) ->
+     let (typed_pat, env) = bind_pat env pat typ_annot in
+     annot_pat (P_typ (typ_annot, typed_pat)) typ_annot, env
+  | P_lit lit ->
+     annot_pat (P_lit lit) (infer_lit env lit), env
+  | P_vector_concat (pat :: pats) ->
+     let fold_pats (pats, env) pat =
+       let inferred_pat, env = infer_pat env pat in
+       pats @ [inferred_pat], env
+     in
+     let (inferred_pat :: inferred_pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in
+     let (_, len, _, vtyp) = destructure_vec_typ l (pat_typ_of inferred_pat) in
+     let fold_len len pat =
+       let (_, len', _, vtyp') = destructure_vec_typ l (pat_typ_of pat) in
+       typ_equality l env vtyp vtyp';
+       nsum len len'
+     in
+     let len = nexp_simp (List.fold_left fold_len len inferred_pats) in
+     annot_pat (P_vector_concat (inferred_pat :: inferred_pats)) (lvector_typ env len vtyp), env
+  | _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat)
 
 and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) =
   let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit"))))) in
@@ -1557,7 +1599,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
             | _, _ -> typ_error l "Not implemented this register field type yet..."
           in
           let checked_exp = crule check_exp env exp vec_typ in
-          annot_assign (annot_lexp (LEXP_id v) vec_typ) checked_exp, env
+          annot_assign (annot_lexp (LEXP_field (annot_lexp (LEXP_id v) regtyp, field)) vec_typ) checked_exp, env
        | _ ->  typ_error l "Field l-expression has invalid type"
      end
   | _ ->
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index cf0500a5..e8685bb2 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -67,6 +67,7 @@ module Env : sig
   val lookup_id : id -> t -> lvar
   val fresh_kid : t -> kid
   val expand_synonyms : t -> typ -> typ
+  val no_casts : t -> t
   val empty : t                                   
 end