Merge pull request #3059 from mtzguido/misc

Improving some error formats.

src/basic/FStar.Errors.Msg.fst

@@ -40,4 +40,4 @@ let subdoc d =
   else blank 2 ^^ doc_of_string "-" ^^ blank 1 ^^ align d ^^ hardline
 
 let rendermsg (ds : list document) : string =
-  renderdoc (concat (List.map subdoc ds))
+  renderdoc (concat (List.map (fun d -> subdoc (group d)) ds))

src/basic/FStar.Errors.fst

@@ -183,7 +183,7 @@ let format_issue' (print_hdr:bool) (issue:issue) : string =
     | _ -> empty
   in
   let mainmsg : document =
-    concat (List.map subdoc issue.issue_msg)
+    concat (List.map (fun d -> subdoc (group d)) issue.issue_msg)
   in
   let doc : document =
     (* This ends in a hardline to get a 1-line spacing between errors *)

src/smtencoding/FStar.SMTEncoding.ErrorReporting.fst

@@ -114,7 +114,7 @@ let label_goals use_env_msg  //when present, provides an alternate error message
 
         | LblPos _ -> failwith "Impossible" //these get added after errorReporting instrumentation only
 
-        | Labeled(arg, "could not prove post-condition", label_range) ->
+        | Labeled(arg, "Could not prove post-condition", label_range) ->
           //printfn "GOT A LABELED WP IMPLICATION\n\t%s"
           //        (Term.print_smt_term q);
           let fallback debug_msg =
@@ -138,7 +138,7 @@ let label_goals use_env_msg  //when present, provides an alternate error message
                         | Quant(Forall, pats_ens, iopt_ens, sorts_ens, {tm=App(Imp, [ensures_conjuncts; post]); rng=rng_ens}) ->
                           if is_a_post_condition (Some post_name) post
                           then
-                            let labels, ensures_conjuncts = aux "could not prove post-condition" None (Some post_name) labels ensures_conjuncts in
+                            let labels, ensures_conjuncts = aux "Could not prove post-condition" None (Some post_name) labels ensures_conjuncts in
                             let pats_ens =
                               match pats_ens with
                               | []

src/smtencoding/FStar.SMTEncoding.Solver.fst

@@ -1262,11 +1262,13 @@ automatically retry increasing fuel as needed, and perform quake testing
 _log_ (not raise) an error if the VC could not be proven. *)
 let solve use_env_msg tcenv q : unit =
     if Options.no_smt () then
+        let open FStar.Errors.Msg in
+        let open FStar.Pprint in
         FStar.TypeChecker.Err.log_issue
           tcenv tcenv.range
             (Errors.Error_NoSMTButNeeded,
-             Errors.mkmsg <|
-             BU.format1 "Q = %s\nA query could not be solved internally, and --no_smt was given" (Print.term_to_string q))
+             [text "A query could not be solved internally, and --no_smt was given.";
+              text "Query = " ^/^ FStar.Syntax.Print.Pretty.term_to_doc q])
     else
     Profiling.profile
       (fun () -> do_solve_maybe_split use_env_msg tcenv q)

src/syntax/FStar.Syntax.Print.fst

@@ -935,3 +935,13 @@ let fv_qual_to_string fvq =
   | Record_ctor _ -> "Record_ctor _"
   | Unresolved_projector _ -> "Unresolved_projector _"
   | Unresolved_constructor _ -> "Unresolved_constructor _"
+
+let term_to_doc' dsenv t =
+  if Options.ugly ()
+  then Pprint.arbitrary_string (term_to_string t)
+  else Pretty.term_to_doc' dsenv t
+
+let term_to_doc t =
+  if Options.ugly ()
+  then Pprint.arbitrary_string (term_to_string t)
+  else Pretty.term_to_doc t

src/syntax/FStar.Syntax.Print.fsti

@@ -79,3 +79,6 @@ val ctx_uvar_to_string_no_reason    : ctx_uvar -> string
 val emb_typ_to_string: emb_typ -> string
 
 val fv_qual_to_string : fv_qual -> string
+
+val term_to_doc'          : DsEnv.env -> term -> Pprint.document
+val term_to_doc           : term -> Pprint.document

src/typechecker/FStar.TypeChecker.Env.fst

@@ -1153,14 +1153,17 @@ let def_check_vars_in_set rng msg vset t =
     if Options.defensive () then begin
         let s = Free.names t in
         if not (BU.set_is_empty <| BU.set_difference s vset)
-        then Errors.log_issue rng
-                    (Errors.Warning_Defensive,
-                     BU.format4 "Internal: term is not closed (%s).\nt = (%s)\nFVs = (%s)\nScope = (%s)\n"
-                                      msg
-                                      (Print.term_to_string t)
-                                      (BU.set_elements s |> Print.bvs_to_string ",\n\t")
-                                      (BU.set_elements vset |> Print.bvs_to_string ",")
-                                      )
+        then 
+          let open FStar.Pprint in
+          let doclist (ds : list Pprint.document) : Pprint.document =
+            surround_separate 2 0 (doc_of_string "[]") lbracket (semi ^^ break_ 1) rbracket ds
+          in
+          Errors.log_issue_doc rng (Errors.Warning_Defensive, [
+               text "Internal: term is not well-scoped " ^/^ parens (doc_of_string msg);
+               text "t = " ^/^ Print.term_to_doc t;
+               text "FVs = " ^/^ doclist (BU.set_elements s |> List.map (fun b -> arbitrary_string (Print.bv_to_string b)));
+               text "Scope = " ^/^ doclist (BU.set_elements vset |> List.map (fun b -> arbitrary_string (Print.bv_to_string b)));
+             ])
     end
 
 let def_check_closed_in rng msg l t =

src/typechecker/FStar.TypeChecker.Err.fst

@@ -205,15 +205,12 @@ let expected_expression_of_type env t1 e t2 =
   let d1 = N.term_to_doc env t1 in
   let d2 = N.term_to_doc env t2 in
   let ed = N.term_to_doc env e in
-  let open FStar.Pprint in
-  (Errors.Fatal_UnexpectedExpressionType,
-    [doc_of_string "Expected expression of type"
-    ^/^ blank 4 ^^ align d1
-    ^/^ doc_of_string "got expression"
-    ^/^ blank 4 ^^ align ed
-    ^/^ doc_of_string "of type"
-    ^/^ blank 4 ^^ align d2
-    ])
+  let open FStar.Errors.Msg in
+  (Errors.Fatal_UnexpectedExpressionType, [
+    prefix 4 1 (text "Expected expression of type") d1 ^/^
+    prefix 4 1 (text "got expression") ed ^/^
+    prefix 4 1 (text "of type") d2
+  ])
 
 let expected_pattern_of_type env t1 e t2 =
   let s1, s2 = err_msg_type_strings env t1 t2 in

src/typechecker/FStar.TypeChecker.Rel.fst

@@ -3690,6 +3690,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
                     | _ -> None
                 in
                 let is_reveal_or_hide t =
+                  // Returns Inl (u, ty, t) for reveal u#u #ty t
+                  // Returns Inr (u, ty, t) for hide u#u #ty t
                   let h, args = U.head_and_args t in
                   if U.is_fvar PC.reveal h
                   then match payload_of_hide_reveal h args with

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -317,7 +317,7 @@ let check_expected_effect env (use_eq:bool) (copt:option comp) (ec : term * comp
                  (Print.comp_to_string expected_c)
                  (string_of_bool use_eq);
        let e, _, g = TcUtil.check_comp env use_eq e c expected_c in
-       let g = TcUtil.label_guard (Env.get_range env) "could not prove post-condition" g in
+       let g = TcUtil.label_guard (Env.get_range env) "Could not prove post-condition" g in
        if debug env Options.Medium
        then BU.print2 "(%s) DONE check_expected_effect;\n\tguard is: %s\n"
                          (Range.string_of_range e.pos)

tests/error-messages/AnotType.fst.expected

@@ -6,12 +6,7 @@
 >>]
 >> Got issues: [
 * Error 189 at AnotType.fst(27,14-27,16):
-  - Expected expression of type
-        Type0
-    got expression
-        tb
-    of type
-        Type
+  - Expected expression of type Type0 got expression tb of type Type
 
 >>]
 Verified module: AnotType