Merge pull request #3687 from mtzguido/ranges

Allowing tactics to bound error ranges

src/basic/FStarC.Errors.fst

@@ -44,6 +44,11 @@ let with_error_bound (r:range) (f : unit -> 'a) : 'a =
   error_range_bound := old;
   res
 
+let maybe_bound_range (r : Range.range) : Range.range =
+  match !error_range_bound with
+  | Some r' -> Range.bound_range r r'
+  | None -> r
+
 (** This exception is raised in FStar.Error
     when a warn_error string could not be processed;
     The exception is handled in FStarC.Options as part of
@@ -287,16 +292,11 @@ let compare_issues i1 i2 =
 let dummy_ide_rng : Range.rng =
   mk_rng "<input>" (mk_pos 1 0) (mk_pos 1 0)
 
-let maybe_bound_rng (r : Range.range) : Range.range =
-  match !error_range_bound with
-  | Some r' -> Range.bound_range r r'
-  | None -> r
-
 (* Attempts to set a decent range (no dummy, no dummy ide) relying
 on the fallback_range reference. *)
-let fixup_issue_range (i:issue) : issue =
+let fixup_issue_range (rng:option Range.range) : option Range.range =
   let rng =
-    match i.issue_range with
+    match rng with
     | None ->
       (* No range given, just rely on the fallback. NB: the
       fallback could also be set to None if it's too early. *)
@@ -316,7 +316,7 @@ let fixup_issue_range (i:issue) : issue =
       in
       Some (set_use_range range use_rng')
   in
-  { i with issue_range = map_opt rng maybe_bound_rng }
+  map_opt rng maybe_bound_range
 
 let mk_default_handler print =
     let issues : ref (list issue) = BU.mk_ref [] in
@@ -368,7 +368,6 @@ let get_err_count () = (!current_handler).eh_count_errors ()
 
 let wrapped_eh_add_one (h : error_handler) (issue : issue) : unit =
     (* Try to set a good use range if we got an empty/dummy one *)
-    let issue = fixup_issue_range issue in
     h.eh_add_one issue;
     if issue.issue_level <> EInfo then begin
       Options.abort_counter := !Options.abort_counter - 1;
@@ -533,27 +532,29 @@ let lookup err =
 
 let log_issue_ctx r (e, msg) ctx =
   let msg = maybe_add_backtrace msg in
+  let r = fixup_issue_range (Some r) in
   match lookup e with
   | (_, CAlwaysError, errno)
   | (_, CError, errno)  ->
-     add_one (mk_issue EError (Some r) msg (Some errno) ctx)
+     add_one (mk_issue EError r msg (Some errno) ctx)
   | (_, CWarning, errno) ->
-     add_one (mk_issue EWarning (Some r) msg (Some errno) ctx)
+     add_one (mk_issue EWarning r msg (Some errno) ctx)
   | (_, CSilent, _) -> ()
   // We allow using log_issue to report a Fatal error in interactive mode
   | (_, CFatal, errno) ->
-    let i = mk_issue EError (Some r) msg (Some errno) ctx in
+    let i = mk_issue EError r msg (Some errno) ctx in
     if Options.ide()
     then add_one i
     else failwith ("don't use log_issue to report fatal error, should use raise_error: " ^ format_issue i)
 
 let info r msg =
   let open FStarC.Class.HasRange in
   let rng = pos r in
+  let rng = fixup_issue_range (Some rng) in
   let msg = to_doc_list msg in
   let msg = maybe_add_backtrace msg in
   let ctx = get_ctx () in
-  add_one (mk_issue EInfo (Some rng) msg None ctx)
+  add_one (mk_issue EInfo rng msg None ctx)
 
 let diag r msg =
   if Debug.any() then
@@ -562,6 +563,7 @@ let diag r msg =
 let raise_error r e msg =
   let open FStarC.Class.HasRange in
   let rng = pos r in
+  let Some rng = fixup_issue_range (Some rng) in
   let msg = to_doc_list msg in
   raise (Error (e, maybe_add_backtrace msg, rng, error_context.get ()))
 
@@ -583,7 +585,8 @@ let issue_of_exn (e:exn) : option issue =
   match e with
   | Error(e, msg, r, ctx) ->
     let errno = error_number (lookup e) in
-    Some (mk_issue EError (Some r) msg (Some errno) ctx)
+    let r = fixup_issue_range (Some r) in
+    Some (mk_issue EError r msg (Some errno) ctx)
   | _ -> None
 
 let err_exn exn =

src/basic/FStarC.Errors.fsti

@@ -37,6 +37,9 @@ val error_range_bound : FStarC.Effect.ref (option Range.range)
 
 val with_error_bound (r:Range.range) (f : unit -> 'a) : 'a
 
+(* Intersect a range by the current bound (if any). *)
+val maybe_bound_range (rng:Range.range) : Range.range
+
 (* Get the error number for a particular code. Useful for creating error
 messages mentioning --warn_error. *)
 val errno : error_code -> int

src/ml/full/FStarC_Tactics_V2_Builtins.ml

@@ -61,6 +61,7 @@ let from_tac_5 s (t: 'a -> 'b -> 'c -> 'd -> 'e -> 'r TM.tac): 'a  -> 'b -> 'c -
 
 
 (* Pointing to the internal primitives *)
+let fixup_range             = from_tac_1 "B.fixup_range" B.fixup_range
 let compress                = from_tac_1 "B.compress" B.compress
 let set_goals               = from_tac_1 "TM.set_goals" TM.set_goals
 let set_smt_goals           = from_tac_1 "TM.set_smt_goals" TM.set_smt_goals

src/tactics/FStarC.Tactics.V2.Basic.fst

@@ -73,6 +73,9 @@ open FStarC.Class.Monad
 open FStarC.Class.PP
 open FStarC.Class.Setlike
 
+let fixup_range (r : FStarC.Range.range) : tac (FStarC.Range.range) =
+  return (Errors.maybe_bound_range r)
+
 let compress (t:term) : tac term =
   return ();!
   return (SS.compress t)

src/tactics/FStarC.Tactics.V2.Basic.fsti

@@ -47,6 +47,7 @@ val proofstate_of_all_implicits: Range.range -> env -> implicits -> proofstate &
 (* Metaprogramming primitives (not all of them).
  * Documented in `ulib/FStarC.Tactics.Builtins.fst` *)
 
+val fixup_range (r : Range.range) : tac (Range.range)
 val compress               : term -> tac term
 val top_env                : unit -> tac env
 val fresh                  : unit -> tac Z.t

src/tactics/FStarC.Tactics.V2.Primops.fst

@@ -100,6 +100,8 @@ let ops = [
 
   unseal_step;
 
+  mk_tac_step_1 0 "fixup_range" fixup_range fixup_range;
+
   mk_tac_step_1 0 "compress" compress compress;
   mk_tac_step_1 0 "set_goals" set_goals set_goals;
   mk_tac_step_1 0 "set_smt_goals" set_smt_goals set_smt_goals;

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

@@ -1,12 +1,12 @@
 >> Got issues: [
-{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n  FStar.Stubs.Tactics.Result.Success (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]}
+{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n  FStar.Stubs.Tactics.Result.Success (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":215,"col":48},"end_pos":{"line":215,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]}
 >>]
 >> Got issues: [
-{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
+{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":215,"col":48},"end_pos":{"line":215,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
 >>]
 >> Got issues: [
-{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n  FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
+{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n  FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":215,"col":48},"end_pos":{"line":215,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
 >>]
 >> Got issues: [
-{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]}
+{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":215,"col":48},"end_pos":{"line":215,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]}
 >>]

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

@@ -5,7 +5,7 @@
   - Reduction stopped at:
       FStar.Stubs.Tactics.Result.Success (Prims.admit ()) "(((proofstate)))"
   - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
-  - See also FStar.Tactics.Effect.fsti(212,48-212,58)
+  - See also FStar.Tactics.Effect.fsti(215,48-215,58)
 
 >>]
 >> Got issues: [
@@ -14,7 +14,7 @@
   - Tactic got stuck!
   - Reduction stopped at: Prims.admit ()
   - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
-  - See also FStar.Tactics.Effect.fsti(212,48-212,58)
+  - See also FStar.Tactics.Effect.fsti(215,48-215,58)
 
 >>]
 >> Got issues: [
@@ -24,14 +24,14 @@
   - Reduction stopped at:
       FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) "(((proofstate)))"
   - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
-  - See also FStar.Tactics.Effect.fsti(212,48-212,58)
+  - See also FStar.Tactics.Effect.fsti(215,48-215,58)
 
 >>]
 >> Got issues: [
 * Error 170 at Bug2899.fst(17,50-17,66):
   - Tactic failed
   - Tactic got stuck!
   - Reduction stopped at: reify (tac ()) "(((proofstate)))"
-  - See also FStar.Tactics.Effect.fsti(212,48-212,58)
+  - See also FStar.Tactics.Effect.fsti(215,48-215,58)
 
 >>]

tests/ide/emacs/FStarMode_GH73.ideout.expected

@@ -3,5 +3,5 @@
 {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}
-{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [121, 12], "end": [121, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"}
-{"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "- Tactic failed\n- 'exact' failed\n- Term 1 of type int does not exactly solve the goal bool\n- See also FStar.Tactics.V2.Derived.fst(121,12-121,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [121, 12], "end": [121, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
+{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [128, 12], "end": [128, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"}
+{"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "- Tactic failed\n- 'exact' failed\n- Term 1 of type int does not exactly solve the goal bool\n- See also FStar.Tactics.V2.Derived.fst(128,12-128,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [128, 12], "end": [128, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}

tests/ide/emacs/FailRange.ideout.expected

@@ -1,14 +1,14 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": [], "status": "success"}
-{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [6, 25], "end": [6, 33], "fname": "<input>"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "2"}
-{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Tactic failed\n- A\n- See also <input>(6,25-6,33)\n", "number": 228, "ranges": [{"beg": [5, 2], "end": [5, 18], "fname": "<input>"}, {"beg": [6, 25], "end": [6, 33], "fname": "<input>"}]}], "status": "failure"}
+{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "2"}
+{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Tactic failed\n- A\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [5, 2], "end": [5, 18], "fname": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
 {"kind": "response", "query-id": "3", "response": [], "status": "success"}
-{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [10, 25], "end": [10, 33], "fname": "<input>"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "4"}
-{"kind": "response", "query-id": "4", "response": [{"level": "error", "message": "- Tactic failed\n- B\n- See also <input>(10,25-10,33)\n", "number": 228, "ranges": [{"beg": [9, 2], "end": [9, 18], "fname": "<input>"}, {"beg": [10, 25], "end": [10, 33], "fname": "<input>"}]}], "status": "failure"}
+{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "4"}
+{"kind": "response", "query-id": "4", "response": [{"level": "error", "message": "- Tactic failed\n- B\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [9, 2], "end": [9, 18], "fname": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
 {"kind": "response", "query-id": "5", "response": [], "status": "success"}
-{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [13, 2], "end": [13, 18], "fname": "<input>"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "6"}
-{"kind": "response", "query-id": "6", "response": [{"level": "error", "message": "- Tactic failed\n- C\n", "number": 228, "ranges": [{"beg": [13, 2], "end": [13, 18], "fname": "<input>"}]}], "status": "failure"}
+{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "6"}
+{"kind": "response", "query-id": "6", "response": [{"level": "error", "message": "- Tactic failed\n- C\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [13, 2], "end": [13, 18], "fname": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
 {"kind": "response", "query-id": "7", "response": [], "status": "success"}
-{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [17, 2], "end": [17, 18], "fname": "<input>"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "8"}
-{"kind": "response", "query-id": "8", "response": [{"level": "error", "message": "- Tactic failed\n- D\n", "number": 228, "ranges": [{"beg": [17, 2], "end": [17, 18], "fname": "<input>"}]}], "status": "failure"}
+{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "8"}
+{"kind": "response", "query-id": "8", "response": [{"level": "error", "message": "- Tactic failed\n- D\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [17, 2], "end": [17, 18], "fname": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
 {"kind": "response", "query-id": "9", "response": [], "status": "success"}