Merge pull request #3972 from mtzguido/errs

Errors: print expected failures as diags

Author: mtzguido

src/basic/FStarC.Errors.fst

@@ -742,3 +742,11 @@ let _ = Options.check_include_dir := (fun s ->
                 (Pprint.doc_of_string s)
             ]
 )
+
+let print_expected_failures (issues : list issue) : unit =
+  (* Add them as diagnostics so we see them in the IDE. *)
+  let issues = issues |> List.map (fun i -> { i with
+    issue_level = EInfo;
+    issue_msg   = (text "Expected failure:") :: i.issue_msg;
+  }) in
+  add_issues issues

src/basic/FStarC.Errors.fsti

@@ -203,3 +203,6 @@ val raise_error_doc  : Range.t -> error_code -> error_message -> 'a
 val log_issue_doc    : Range.t -> error_code -> error_message -> unit
 val raise_error_text : Range.t -> error_code -> string -> 'a
 val log_issue_text   : Range.t -> error_code -> string -> unit
+
+(* Print expected failures as diagnostics, without failing. *)
+val print_expected_failures (issues : list issue) : unit

src/tosyntax/FStarC.ToSyntax.ToSyntax.fst

@@ -3408,12 +3408,8 @@ and desugar_decl_maybe_fail_attr env (d: decl) (attrs : list S.term) : (env_t &
 
       | errs, ropt -> (* failed! check that it failed as expected *)
         let errnos = List.concatMap (fun i -> FStarC.Common.list_of_option i.issue_number) errs in
-        if Options.print_expected_failures () then (
-          (* Print errors if asked for *)
-          Format.print_string ">> Got issues: [\n";
-          List.iter Errors.print_issue errs;
-          Format.print_string ">>]\n"
-        );
+        if Options.print_expected_failures () then
+          Errors.print_expected_failures errs;
         if expected_errs = [] then
           env0, []
         else begin

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -625,13 +625,8 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
                     Options.with_saved_options (fun () ->
                       Some?.v (!tc_decls_knot) env' ses)) in
 
-    if Options.print_expected_failures ()
-       || Debug.low () then
-    begin
-        Format.print_string ">> Got issues: [\n";
-        List.iter Errors.print_issue errs;
-        Format.print_string ">>]\n"
-    end;
+    if Options.print_expected_failures () || Debug.low () then
+      Errors.print_expected_failures errs;
 
     (* Pop environment, reset SMT context *)
     let _ = Env.pop env' "expect_failure" in

tests/error-messages/AQualMismatch.fst.json_output.expected

@@ -1,5 +1,3 @@
 {"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]}
->> Got issues: [
-{"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
->>]
+{"msg":["Expected failure:","Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Info","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
 {"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]}

tests/error-messages/AQualMismatch.fst.output.expected

@@ -2,13 +2,12 @@
   - AQualMismatch.f is declared but no definition was found
   - Add an 'assume' if this is intentional
 
->> Got issues: [
-* Error 91 at AQualMismatch.fst(6,7-6,8):
+* Info at AQualMismatch.fst(6,7-6,8):
+  - Expected failure:
   - Inconsistent implicit argument annotation on argument x
   - Got: '#'
   - Expected: ''
 
->>]
 * Warning 240 at AQualMismatch.fst(6,0-6,12):
   - Missing definitions in module AQualMismatch: f
 

tests/error-messages/AnotType.fst.json_output.expected

@@ -1,6 +1,2 @@
->> Got issues: [
-{"msg":["Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]}
->>]
->> Got issues: [
-{"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
->>]
+{"msg":["Expected failure:","Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Info","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]}
+{"msg":["Expected failure:","Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Info","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}

tests/error-messages/AnotType.fst.output.expected

@@ -1,11 +1,9 @@
->> Got issues: [
-* Error 309 at AnotType.fst(19,5-19,7):
+* Info at AnotType.fst(19,5-19,7):
+  - Expected failure:
   - Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype,
     or it is eqtype but contains noeq/unopteq qualifiers
 
->>]
->> Got issues: [
-* Error 189 at AnotType.fst(27,14-27,16):
+* Info at AnotType.fst(27,14-27,16):
+  - Expected failure:
   - Expected expression of type Type0 got expression tb of type Type
 
->>]

tests/error-messages/ArgsAndQuals.fst.json_output.expected

@@ -1,5 +1,3 @@
 {"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]}
->> Got issues: [
-{"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
->>]
+{"msg":["Expected failure:","Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Info","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
 {"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]}

tests/error-messages/ArgsAndQuals.fst.output.expected

@@ -2,13 +2,12 @@
   - ArgsAndQuals.test1 is declared but no definition was found
   - Add an 'assume' if this is intentional
 
->> Got issues: [
-* Error 91 at ArgsAndQuals.fst(25,16-25,18):
+* Info at ArgsAndQuals.fst(25,16-25,18):
+  - Expected failure:
   - Inconsistent implicit argument annotation on argument uu___
   - Got: '#'
   - Expected: '$'
 
->>]
 * Warning 240 at ArgsAndQuals.fst(25,0-25,29):
   - Missing definitions in module ArgsAndQuals: test1