Work on improving Sail error messages

- Modified how sail type error messages are displayed. The
  typechecker, rather than immediately outputing a string has a
  datatype for error types, which are the pretty-printed using a
  PPrint pretty-printer. Needs more work for all the error messages.

- Error messages now attempt to highlight the part of the file where
  the error occurred, by printing the line the error is on and
  highlighting where the error message is in red. Again, this needs to
  be made more robust, especially when the error messages span
  multiple lines.

Other things

- Improved new parser and lexer. Made the lexer & parser handling of
  colons simpler and more intuitive.

- Added some more typechecking test cases

7 files changed, 127 insertions, 83 deletions

diff --git a/src/ast_util.mli b/src/ast_util.mli
index e6823ee9..6164fc17 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,6 +44,8 @@
 
 open Ast
 
+val no_annot : unit annot
+
 val mk_id : string -> id
 val mk_kid : string -> kid
 val mk_ord : order_aux -> order
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4c0a0db4..1f7840d0 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1010,7 +1010,7 @@ let initial_kind_env =
   ]
 
 let typschm_of_string order str =
-  let typschm = Parser2.typschm Lexer2.token (Lexing.from_string str) in
+  let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
@@ -1057,14 +1057,14 @@ let generate_undefineds vs_ids (Defs defs) =
     if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
   in
   let undefined_builtins = List.concat
-    [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}";
+    [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
      gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
      gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
      gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
      gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
      gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
      (* FIXME: How to handle inc/dec order correctly? *)
-     gen_vs (mk_id "undefined_vector") "forall 'n 'm 'a:Type. (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
+     gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
      gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
   in
   let undefined_td = function
diff --git a/src/lexer2.mll b/src/lexer2.mll
index f5350ea8..a1717d62 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -235,8 +235,6 @@ rule token = parse
       with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
   | "(*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
   | "*)"        { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
-  | (tyvar_start startident ident* as i) ":" { TyDecl(r i) }
-  | (startident ident* as i) ":"        { Decl(r i) }
   | tyvar_start startident ident* as i  { TyVar(r i) }
   | startident ident* as i              { if M.mem i kw_table then
                                             (M.find i kw_table) ()
diff --git a/src/parser2.mly b/src/parser2.mly
index 42e13721..02a8f09c 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -139,7 +139,7 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with content*/
 
-%token <string> Id TyVar Decl TyDecl
+%token <string> Id TyVar
 %token <int> Num
 %token <string> String Bin Hex Real
 
@@ -153,9 +153,8 @@ let rec desugar_rchain chain s e =
 %token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
 %start file
-%start typschm
-%type <Parse_ast.typschm> typschm
-%type <Parse_ast.defs> defs
+%start typschm_eof
+%type <Parse_ast.typschm> typschm_eof
 %type <Parse_ast.defs> file
 
 %%
@@ -233,10 +232,6 @@ op7r: Op7r { mk_id (Id $1) $startpos $endpos }
 op8r: Op8r { mk_id (Id $1) $startpos $endpos }
 op9r: Op9r { mk_id (Id $1) $startpos $endpos }
 
-decl:
-  | Decl
-    { mk_id (Id $1) $startpos $endpos }
-
 id_list:
   | id
     { [$1] }
@@ -247,10 +242,6 @@ kid:
   | TyVar
     { mk_kid $1 $startpos $endpos }
 
-tydecl:
-  | TyDecl
-    { mk_kid $1 $startpos $endpos }
-
 kid_list:
   | kid
     { [$1] }
@@ -515,8 +506,6 @@ kind:
     { K_aux (K_kind [$1], loc $startpos $endpos) }
 
 kopt:
-  | tydecl kind
-    { KOpt_aux (KOpt_kind ($2, $1), loc $startpos $endpos) }
   | Lparen kid Colon kind Rparen
     { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) }
   | kid
@@ -589,6 +578,10 @@ typschm:
   | Forall typquant Dot typ MinusGt typ Effect effect_set
     { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos }
 
+typschm_eof:
+  | typschm Eof
+    { $1 }
+
 pat:
   | atomic_pat
     { $1 }
@@ -612,14 +605,10 @@ atomic_pat:
     { mk_pat (P_id $1) $startpos $endpos }
   | kid
     { mk_pat (P_var $1) $startpos $endpos }
-  | tydecl typ
-    { mk_pat (P_typ ($2, mk_pat (P_var $1) $startpos $endpos($1))) $startpos $endpos }
   | id Lparen pat_list Rparen
     { mk_pat (P_app ($1, $3)) $startpos $endpos }
   | pat Colon typ
     { mk_pat (P_typ ($3, $1)) $startpos $endpos }
-  | decl typ
-    { mk_pat (P_typ ($2, mk_pat (P_id $1) $startpos $endpos($1))) $startpos $endpos }
   | Lparen pat Rparen
     { $2 }
 
@@ -646,27 +635,21 @@ lit:
     { mk_lit (L_string $1) $startpos $endpos }
 
 exp:
-  | cast_exp Colon typ
-    { mk_exp (E_cast ($3, $1)) $startpos $endpos }
-  | cast_exp
-    { $1 }
-
-cast_exp:
   | exp0
     { $1 }
-  | atomic_exp Eq cast_exp
+  | atomic_exp Eq exp
     { mk_exp (E_assign ($1, $3)) $startpos $endpos }
-  | Let_ letbind In cast_exp
+  | Let_ letbind In exp
     { mk_exp (E_let ($2, $4)) $startpos $endpos }
   | Lcurly block Rcurly
     { mk_exp (E_block $2) $startpos $endpos }
-  | Return cast_exp
+  | Return exp
     { mk_exp (E_return $2) $startpos $endpos }
-  | Throw cast_exp
+  | Throw exp
     { mk_exp (E_throw $2) $startpos $endpos }
-  | If_ exp Then cast_exp Else cast_exp
+  | If_ exp Then exp Else exp
     { mk_exp (E_if ($2, $4, $6)) $startpos $endpos }
-  | If_ exp Then cast_exp
+  | If_ exp Then exp
     { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos }
   | Match exp Lcurly case_list Rcurly
     { mk_exp (E_case ($2, $4)) $startpos $endpos }
@@ -856,12 +839,14 @@ block:
     { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
 
 atomic_exp:
+  | atomic_exp Colon atomic_typ
+    { mk_exp (E_cast ($3, $1)) $startpos $endpos }
   | lit
     { mk_exp (E_lit $1) $startpos $endpos }
-  | decl atomic_typ
-    { mk_exp (E_cast ($2, mk_exp (E_id $1) $startpos $endpos($1))) $startpos $endpos }
   | id
     { mk_exp (E_id $1) $startpos $endpos }
+  | kid
+    { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
   | id Unit
     { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
   | id Lparen exp_list Rparen
@@ -922,8 +907,6 @@ enum:
     { $1 :: $3 }
 
 struct_field:
-  | decl typ
-    { ($2, $1) }
   | id Colon typ
     { ($3, $1) }
 
@@ -936,8 +919,6 @@ struct_fields:
     { $1 :: $3 }
 
 type_union:
-  | decl typ
-    { Tu_aux (Tu_ty_id ($2, $1), loc $startpos $endpos) }
   | id Colon typ
     { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) }
   | id
@@ -960,14 +941,10 @@ let_def:
     { $2 }
 
 val_spec_def:
-  | Val decl typschm
-    { mk_vs (VS_val_spec ($3, $2)) $startpos $endpos }
   | Val id Colon typschm
     { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
 
 register_def:
-  | Register decl typ
-    { mk_reg_dec (DEC_reg ($3, $2)) $startpos $endpos }
   | Register id Colon typ
     { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
 
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 69c5c084..2bd5d5bc 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -87,19 +87,48 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-let format_pos ff p = (
-  Format.fprintf ff "File \"%s\", line %d, character %d:\n"
-    p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol);
-  Format.pp_print_flush ff ())
-
-
-let format_pos2 ff p1 p2 = (
-  Format.fprintf ff "File \"%s\", line %d, character %d to line %d, character %d"
-    p1.Lexing.pos_fname 
-    p1.Lexing.pos_lnum (p1.Lexing.pos_cnum - p1.Lexing.pos_bol + 1)
-    p2.Lexing.pos_lnum (p2.Lexing.pos_cnum - p2.Lexing.pos_bol);
-  Format.pp_print_flush ff ()
-)
+let format_pos ff p =
+  let open Lexing in
+  begin
+    Format.fprintf ff "file \"%s\", line %d, character %d:\n"
+                   p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
+    Format.pp_print_flush ff ()
+  end
+
+let rec skip_lines in_chan = function
+  | n when n <= 0 -> ()
+  | n -> input_line in_chan; skip_lines in_chan (n - 1)
+
+let termcode n = "\x1B[" ^ string_of_int n ^ "m"
+
+let print_code ff fname lnum1 cnum1 cnum2 =
+  try
+    let in_chan = open_in fname in
+    begin
+      try
+        skip_lines in_chan (lnum1 - 1);
+        let line = input_line in_chan in
+        Format.fprintf ff "%s%s%s%s%s"
+                       (Str.string_before line cnum1)
+                       (termcode 41)
+                       (Str.string_before (Str.string_after line cnum1) (cnum2 - cnum1))
+                       (termcode 49)
+                       (Str.string_after line cnum2);
+        close_in in_chan
+      with e -> (close_in_noerr in_chan; print_endline (Printexc.to_string e))
+    end
+  with _ -> ()
+
+let format_pos2 ff p1 p2 =
+  let open Lexing in
+  begin
+    Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d\n\n"
+                   p1.pos_fname
+                   p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
+                   p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
+    print_code ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol);
+    Format.pp_print_flush ff ()
+  end
 
 (* reads the part between p1 and p2 from the file *)
 
@@ -171,12 +200,12 @@ let loc_to_string l =
 type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position
 
 let print_err_internal fatal verb_loc p_l m1 m2 =
+  Format.eprintf "%s at " m1;
   let _ = (match p_l with Pos p -> print_err_pos p
                         | Loc l -> print_err_loc l
                         | LocD (l1,l2) ->
                           print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in
-  let m12 = if String.length m2 = 0 then "" else ": " in
-  Format.eprintf "  %s%s%s\n" m1 m12 m2;
+  Format.eprintf "%s\n" m2;
   if verb_loc then (match p_l with Loc l ->
       format_loc_source Format.err_formatter l;
       Format.pp_print_newline Format.err_formatter (); | _ -> ());
diff --git a/src/type_check.ml b/src/type_check.ml
index 636d4049..f952d0d6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -65,9 +65,47 @@ let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ m) el
 
 let typ_warning m = prerr_endline ("Warning: " ^ m)
 
-exception Type_error of l * string;;
+type type_error =
+  (* First parameter is the error that caused us to start doing type
+     coercions, the second is the errors encountered by all possible
+     coerctions *)
+  | Err_no_casts of type_error * type_error list
+  | Err_subtype of typ * typ * n_constraint list
+  | Err_other of string
+
+let pp_type_error err =
+  let open PPrint in
+  let rec pp_err = function
+    | Err_no_casts (trigger, []) ->
+       (string "Tried performing type coercion because" ^//^ pp_err trigger)
+       ^/^ string "No possible coercions"
+    | Err_no_casts (trigger, errs) ->
+       (string "Tried performing type coerction because" ^//^ pp_err trigger)
+    | Err_subtype (typ1, typ2, []) ->
+       separate space [ string (string_of_typ typ1);
+                        string "is not a subtype of";
+                        string (string_of_typ typ2) ]
+    | Err_subtype (typ1, typ2, constrs) ->
+       separate space [ string (string_of_typ typ1);
+                        string "is not a subtype of";
+                        string (string_of_typ typ2) ]
+       ^/^ string "in context"
+       ^//^ string (string_of_list ", " string_of_n_constraint constrs)
+    | Err_other str -> string str
+  in
+  pp_err err
+
+let rec string_of_type_error err =
+  let open PPrint in
+  let b = Buffer.create 20 in
+  ToBuffer.pretty 1. 120 b (pp_type_error err);
+  "\n" ^ Buffer.contents b
+
+exception Type_error of l * type_error;;
+
+let typ_error l m = raise (Type_error (l, Err_other m))
 
-let typ_error l m = raise (Type_error (l, m))
+let typ_raise l err = raise (Type_error (l, err))
 
 let deinfix = function
   | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
@@ -1447,9 +1485,7 @@ let rec subtyp l env typ1 typ2 =
   | _, None ->
      if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2)
      then ()
-     else typ_error l (string_of_typ typ1
-                       ^ " is not a subtype of " ^ string_of_typ typ2
-                       ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
+     else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env))
 
 let typ_equality l env typ1 typ2 =
   subtyp l env typ1 typ2; subtyp l env typ2 typ1
@@ -1782,7 +1818,7 @@ let crule r env exp typ =
     let checked_exp = r env exp typ in
     decr depth; checked_exp
   with
-  | Type_error (l, m) -> decr depth; typ_error l m
+  | Type_error (l, err) -> decr depth; typ_raise l err
 
 let irule r env exp =
   incr depth;
@@ -1792,7 +1828,7 @@ let irule r env exp =
     decr depth;
     inferred_exp
   with
-  | Type_error (l, m) -> decr depth; typ_error l m
+  | Type_error (l, err) -> decr depth; typ_raise l err
 
 let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
 let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
@@ -1928,7 +1964,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        | (f :: fs) -> begin
            typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")");
            try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with
-           | Type_error (_, m) -> typ_print ("Error : " ^ m); try_overload fs
+           | Type_error (_, err) -> typ_print ("Error : " ^ string_of_type_error err); try_overload fs
          end
      in
      try_overload (Env.get_overloads f env)
@@ -1991,15 +2027,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
 and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
-  let rec try_casts m = function
-    | [] -> typ_error l ("No valid casts:\n" ^ m)
+  let rec try_casts trigger errs = function
+    | [] -> typ_raise l (Err_no_casts (trigger, errs))
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ);
         try
           let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in
           annot_exp (E_cast (typ, checked_cast)) typ
         with
-        | Type_error (_, m) -> try_casts m casts
+        | Type_error (_, err) -> try_casts trigger (err :: errs) casts
       end
   in
   begin
@@ -2007,10 +2043,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
       typ_debug ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ);
       subtyp l env (typ_of annotated_exp) typ; annotated_exp
     with
-    | Type_error (_, m) when Env.allow_casts env ->
+    | Type_error (_, trigger) when Env.allow_casts env ->
        let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
-       try_casts "" casts
-    | Type_error (l, m) -> typ_error l ("Subtype error " ^ m)
+       try_casts trigger [] casts
+    | Type_error (l, err) -> typ_error l "Subtype error"
   end
 
 (* type_coercion_unify env exp typ attempts to coerce exp to a type
@@ -2021,8 +2057,8 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
 and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
-  let rec try_casts m = function
-    | [] -> unify_error l ("No valid casts resulted in unification:\n" ^ m)
+  let rec try_casts = function
+    | [] -> unify_error l "No valid casts resulted in unification"
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " for unification");
         try
@@ -2030,8 +2066,8 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
           let ityp = typ_of inferred_cast in
           annot_exp (E_cast (ityp, inferred_cast)) ityp, unify l env typ ityp
         with
-        | Type_error (_, m) -> try_casts m casts
-        | Unification_error (_, m) -> try_casts m casts
+        | Type_error (_, err) -> try_casts casts
+        | Unification_error (_, err) -> try_casts casts
       end
   in
   begin
@@ -2041,7 +2077,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
     with
     | Unification_error (_, m) when Env.allow_casts env ->
        let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
-       try_casts "" casts
+       try_casts casts
   end
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
@@ -2497,7 +2533,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | (f :: fs) -> begin
            typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")");
            try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with
-           | Type_error (_, m) -> typ_print ("Error: " ^ m); try_overload fs
+           | Type_error (_, err) -> typ_print ("Overload error"); try_overload fs
          end
      in
      try_overload (Env.get_overloads f env)
@@ -3125,7 +3161,7 @@ let mk_synonym typq typ =
        typ_subst_typ (kopt_kid kopt) (unaux_typ arg) typ, ncs
     | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt ->
        let typ, ncs = subst_args kopts args in
-       typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs     
+       typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs
     | [], [] -> typ, ncs
     | _, Typ_arg_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments"
     | _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments"
@@ -3193,4 +3229,4 @@ let rec check' env (Defs defs) =
 
 let check env defs =
   try check' env defs with
-  | Type_error (l, m) -> raise (Reporting_basic.err_typ l m)
+  | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
diff --git a/src/type_check.mli b/src/type_check.mli
index fa75b156..ca2fb90c 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -47,7 +47,9 @@ open Ast_util
 val opt_tc_debug : int ref
 val opt_no_effects : bool ref
 
-exception Type_error of l * string;;
+type type_error
+
+exception Type_error of l * type_error;;
 
 type mut = Immutable | Mutable