diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 10 | ||||
| -rw-r--r-- | src/ast_util.mli | 3 | ||||
| -rw-r--r-- | src/isail.ml | 2 | ||||
| -rw-r--r-- | src/latex.ml | 2 | ||||
| -rw-r--r-- | src/reporting.ml | 14 | ||||
| -rw-r--r-- | src/reporting.mli | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 8 |
7 files changed, 27 insertions, 18 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index ad8302ce..95954d0f 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1908,20 +1908,12 @@ let subst_kids_nc, subst_kids_typ, subst_kids_typ_arg = | A_bool nc -> A_aux (A_bool (subst_kids_nc substs nc), l) in subst_kids_nc, s_styp, s_starg - -let rec simp_loc = function - | Parse_ast.Unknown -> None - | Parse_ast.Unique (_, l) -> simp_loc l - | Parse_ast.Generated l -> simp_loc l - | Parse_ast.Range (p1, p2) -> Some (p1, p2) - | Parse_ast.Documented (_, l) -> simp_loc l - let before p1 p2 = let open Lexing in p1.pos_fname = p2.pos_fname && p1.pos_cnum <= p2.pos_cnum let subloc sl l = - match sl, simp_loc l with + match sl, Reporting.simp_loc l with | _, None -> false | None, _ -> false | Some (p1a, p1b), Some (p2a, p2b) -> diff --git a/src/ast_util.mli b/src/ast_util.mli index f7391e28..1f459870 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -483,9 +483,6 @@ val locate_typ : (l -> l) -> typ -> typ a generated number. *) val unique : l -> l -(** Reduce a location to a pair of positions if possible *) -val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option - (** Try to find the annotation closest to the provided (simplified) location. Note that this function makes no guarantees about finding the closest annotation or even finding an annotation at all. This diff --git a/src/isail.ml b/src/isail.ml index 51501e25..cce56fb0 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -603,7 +603,7 @@ let handle_input' input = begin match find_annot_ast sl !Interactive.ast with | Some annot -> let msg = String.escaped (string_of_typ (Type_check.typ_of_annot annot)) in - begin match simp_loc (fst annot) with + begin match Reporting.simp_loc (fst annot) with | Some (p1, p2) -> print_endline ("(sail-highlight-region " ^ string_of_int (p1.pos_cnum + 1) ^ " " ^ string_of_int (p2.pos_cnum + 1) diff --git a/src/latex.ml b/src/latex.ml index 1806da47..aa786b83 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -300,7 +300,7 @@ let rec read_lines in_chan = function l :: ls let latex_loc no_loc l = - match simp_loc l with + match Reporting.simp_loc l with | Some (p1, p2) -> begin let open Lexing in diff --git a/src/reporting.ml b/src/reporting.ml index 0bc73ed6..20e44c57 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -111,6 +111,20 @@ let loc_to_string ?code:(code=true) l = format_message (Location (l, Line "")) (buffer_formatter b); Buffer.contents b +let rec simp_loc = function + | Parse_ast.Unknown -> None + | Parse_ast.Unique (_, l) -> simp_loc l + | Parse_ast.Generated l -> simp_loc l + | Parse_ast.Range (p1, p2) -> Some (p1, p2) + | Parse_ast.Documented (_, l) -> simp_loc l + +let short_loc_to_string l = + match simp_loc l with + | None -> "unknown location" + | Some (p1, p2) -> + Printf.sprintf "%s %d:%d - %d:%d" + p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol) + let print_err l m1 m2 = print_err_internal (Loc l) m1 m2 diff --git a/src/reporting.mli b/src/reporting.mli index 2d886111..86399e84 100644 --- a/src/reporting.mli +++ b/src/reporting.mli @@ -65,6 +65,12 @@ (** [loc_to_string] includes code from file if code optional argument is true (default) *) val loc_to_string : ?code:bool -> Parse_ast.l -> string +(** Reduce a location to a pair of positions if possible *) +val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option + +(** [short_loc_to_string] prints the location as a single line in a simple format *) +val short_loc_to_string : Parse_ast.l -> string + (** [print_err fatal print_loc_source l head mes] prints an error / warning message to std-err. It starts with printing location information stored in [l] It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards. diff --git a/src/type_check.ml b/src/type_check.ml index 69e1e2c9..4396728b 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2643,10 +2643,10 @@ let irule r env exp = (* This function adds useful assertion messages to asserts missing them *) -let assert_msg test = function +let assert_msg = function | E_aux (E_lit (L_aux (L_string "", _)), (l, _)) -> let open Reporting in - locate (fun _ -> l) (mk_lit_exp (L_string (loc_to_string ~code:false l ^ ": " ^ string_of_exp test))) + locate (fun _ -> l) (mk_lit_exp (L_string (short_loc_to_string l))) | msg -> msg let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp @@ -2894,7 +2894,7 @@ and check_block l env exps ret_typ = let texp, env = bind_assignment env lexp bind in texp :: check_block l env exps ret_typ | ((E_aux (E_assert (constr_exp, msg), _) as exp) :: exps) -> - let msg = assert_msg constr_exp msg in + let msg = assert_msg msg in let constr_exp = crule check_exp env constr_exp bool_typ in let checked_msg = crule check_exp env msg string_typ in let env = match assert_constraint env true constr_exp with @@ -3761,7 +3761,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let vec_typ = dvector_typ env (nint (List.length vec)) (typ_of inferred_item) in annot_exp (E_vector (inferred_item :: checked_items)) vec_typ | E_assert (test, msg) -> - let msg = assert_msg test msg in + let msg = assert_msg msg in let checked_test = crule check_exp env test bool_typ in let checked_msg = crule check_exp env msg string_typ in annot_exp_effect (E_assert (checked_test, checked_msg)) unit_typ (mk_effect [BE_escape]) |