Merge pull request #833 from CakeML/parse-err

Improve compiler error messages

Author: myreen

basis/basis_ffi.c

@@ -158,16 +158,17 @@ int hasT = 0;
 void cml_exit(int arg) {
 
   #ifdef STDERR_MEM_EXHAUST
-  if(arg == 1) {
-    fprintf(stderr,"CakeML heap space exhausted.\n");
-  }
-  else if(arg == 2) {
-    fprintf(stderr,"CakeML stack space exhausted.\n");
-  }
+  fprintf(stderr,"Program exited with nonzero exit code.\n");
   #endif
 
   #ifdef DEBUG_FFI
   {
+    if(arg == 1) {
+      fprintf(stderr,"CakeML heap space exhausted.\n");
+    }
+    else if(arg == 2) {
+      fprintf(stderr,"CakeML stack space exhausted.\n");
+    }
     fprintf(stderr,"GCNum: %d, GCTime(us): %ld\n",numGC,microsecs);
   }
   #endif

compiler/bootstrap/translation/compiler32ProgScript.sml

@@ -131,7 +131,22 @@ val res = translate (spec32 word_to_string_def);
 
 (* compilerTheory *)
 
-val _ = translate compilerTheory.locn_to_string_def;
+val res = translate compilerTheory.find_next_newline_def;
+
+Theorem find_next_newline_side = prove(
+  “∀n s. compiler_find_next_newline_side n s”,
+  ho_match_mp_tac compilerTheory.find_next_newline_ind \\ rw []
+  \\ once_rewrite_tac [fetch "-" "compiler_find_next_newline_side_def"]
+  \\ fs []) |> update_precondition;
+
+val res = translate compilerTheory.safe_substring_def;
+
+Theorem safe_substring_side = prove(
+  “compiler_safe_substring_side s n l”,
+  fs [fetch "-" "compiler_safe_substring_side_def"])
+  |> update_precondition;
+
+val _ = translate compilerTheory.get_nth_line_def;
 val _ = translate compilerTheory.locs_to_string_def;
 val _ = translate compilerTheory.parse_cml_input_def;
 val _ = translate (compilerTheory.parse_sexp_input_def
@@ -236,7 +251,9 @@ val res = translate compilerTheory.help_string_def;
 val nonzero_exit_code_for_error_msg_def = Define `
   nonzero_exit_code_for_error_msg e =
     if compiler$is_error_msg e then
-      ml_translator$force_out_of_memory_error () else ()`;
+      (let a = empty_ffi (strlit "nonzero_exit") in
+         ml_translator$force_out_of_memory_error ())
+    else ()`;
 
 val res = translate compilerTheory.is_error_msg_def;
 val res = translate nonzero_exit_code_for_error_msg_def;

compiler/bootstrap/translation/compiler64ProgScript.sml

@@ -132,7 +132,22 @@ val res = translate (spec64 word_to_string_def);
 
 (* compilerTheory *)
 
-val _ = translate compilerTheory.locn_to_string_def;
+val res = translate compilerTheory.find_next_newline_def;
+
+Theorem find_next_newline_side = prove(
+  “∀n s. compiler_find_next_newline_side n s”,
+  ho_match_mp_tac compilerTheory.find_next_newline_ind \\ rw []
+  \\ once_rewrite_tac [fetch "-" "compiler_find_next_newline_side_def"]
+  \\ fs []) |> update_precondition;
+
+val res = translate compilerTheory.safe_substring_def;
+
+Theorem safe_substring_side = prove(
+  “compiler_safe_substring_side s n l”,
+  fs [fetch "-" "compiler_safe_substring_side_def"])
+  |> update_precondition;
+
+val _ = translate compilerTheory.get_nth_line_def;
 val _ = translate compilerTheory.locs_to_string_def;
 val _ = translate compilerTheory.parse_cml_input_def;
 val _ = translate (compilerTheory.parse_sexp_input_def
@@ -255,7 +270,9 @@ val res = translate compilerTheory.help_string_def;
 val nonzero_exit_code_for_error_msg_def = Define `
   nonzero_exit_code_for_error_msg e =
     if compiler$is_error_msg e then
-      ml_translator$force_out_of_memory_error () else ()`;
+      (let a = empty_ffi (strlit "nonzero_exit") in
+         ml_translator$force_out_of_memory_error ())
+    else ()`;
 
 val res = translate compilerTheory.is_error_msg_def;
 val res = translate nonzero_exit_code_for_error_msg_def;

compiler/compilerScript.sml

@@ -172,24 +172,49 @@ Datatype:
                 | ConfigError mlstring
 End
 
-Definition locn_to_string_def:
-  locn_to_string UNKNOWNpt = implode "unknown point" ∧
-  locn_to_string EOFpt = implode "end-of-file" ∧
-  locn_to_string (POSN r c) =
-    concat [strlit "row " ; toString r ; strlit ", column " ; toString c]
+Definition find_next_newline_def:
+  find_next_newline n s =
+    if strlen s ≤ n then n else
+      if strsub s n = #"\n" then n else
+        find_next_newline (n+1) s
+Termination
+  WF_REL_TAC ‘measure (λ(n,s). strlen s - n)’
 End
 
-val locs_to_string_def = Define `
-  (locs_to_string NONE = implode "unknown location") ∧
-  (locs_to_string (SOME (Locs startl endl)) =
-    if Locs startl endl = unknown_loc then
-      implode "unknown location"
+Definition safe_substring_def:
+  safe_substring s n l =
+    let k = strlen s in
+      if k ≤ n then strlit "" else
+        if n + l ≤ k then
+          substring s n l
+        else substring s n (k - n)
+End
+
+Definition get_nth_line_def:
+  get_nth_line k s n =
+    if k = 0 then
+      let n1 = find_next_newline n s in
+        safe_substring s n (n1 - n)
     else
-      concat
-        [implode "location starting at ";
-         locn_to_string startl ;
-         implode ", ending at ";
-         locn_to_string endl])`;
+      get_nth_line (k-1:num) s (find_next_newline n s + 1)
+End
+
+Definition locs_to_string_def:
+  (locs_to_string input NONE = implode "unknown location") ∧
+  (locs_to_string input (SOME (Locs startl endl)) =
+    case startl of
+    | POSN r c =>
+       (let line = get_nth_line r input 0 in
+        let len = strlen line in
+        let stop =
+          (case endl of POSN r1 c1 => (if r1 = r then c1 else len) | _ => len) in
+        let underline =
+          concat (REPLICATE c (strlit " ") ++ REPLICATE ((stop - c) + 1) (strlit [CHR 94])) in
+          concat [strlit "line "; toString (r+1); strlit "\n\n";
+                  line; strlit "\n";
+                  underline;  strlit "\n"])
+    | _ => implode "unknown location")
+End
 
 (* this is a rather annoying feature of peg_exec requiring locs... *)
 Overload add_locs = ``MAP (λc. (c,unknown_loc))``
@@ -207,7 +232,7 @@ End
 Definition parse_cml_input_def:
   parse_cml_input input =
     case parse_prog (lexer_fun input) of
-    | Failure l _ => INL (strlit "Parsing failed at " ^ locs_to_string (SOME l))
+    | Failure l _ => INL (strlit "Parsing failed at " ^ locs_to_string (implode input) (SOME l))
     | Success _ x _ => INR x
 End
 
@@ -230,7 +255,7 @@ val compile_def = Define`
        of
        | Failure (locs, msg) =>
            (Failure (TypeError (concat [msg; implode " at ";
-               locs_to_string locs])), [])
+               locs_to_string (implode input) locs])), [])
        | Success ic =>
           let _ = empty_ffi (strlit "finished: type inference") in
           if c.only_print_types then