From aa1f89abb2f42d085bd123147144c9c5c7ceb22f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 13 Sep 2017 16:27:34 +0100 Subject: 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 --- src/ast_util.mli | 2 ++ src/initial_check.ml | 6 ++-- src/lexer2.mll | 2 -- src/parser2.mly | 57 +++++++++++------------------------ src/reporting_basic.ml | 59 +++++++++++++++++++++++++++---------- src/type_check.ml | 80 ++++++++++++++++++++++++++++++++++++-------------- src/type_check.mli | 4 ++- 7 files changed, 127 insertions(+), 83 deletions(-) (limited to 'src') 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 Id TyVar Decl TyDecl +%token Id TyVar %token Num %token String Bin Hex Real @@ -153,9 +153,8 @@ let rec desugar_rchain chain s e = %token Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r %start file -%start typschm -%type typschm -%type defs +%start typschm_eof +%type typschm_eof %type 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 -- cgit v1.2.3