Some error nits

bare-tests/Check.fst.output.expected

@@ -1,9 +1,9 @@
-* Info at Check.fst(5,0-5,8):
+* Info at Check.fst:5.1-5.9:
   - Term 1 has type Prims.int
 
-* Info at Check.fst(6,0-6,10):
+* Info at Check.fst:6.1-6.11:
   - Term 1 + 1 has type Prims.int
 
-* Info at Check.fst(11,0-11,10):
+* Info at Check.fst:11.1-11.11:
   - Term Check.foo has type Prims.Tot (#_: Type -> x: _ -> Prims.Tot _)
 

src/basic/FStarC.Range.Ops.fst

@@ -48,11 +48,11 @@ let rng_included r1 r2 =
     r2.end_pos >=? r1.end_pos
 
 let string_of_pos pos =
-    Format.fmt2 "%s,%s" (show pos.line) (show pos.col)
+    Format.fmt2 "%s.%s" (show pos.line) (show pos.col)
 let file_of_range r = r.def_range.file_name
 let set_file_of_range r (f:string) = {r with def_range = {r.def_range with file_name = Filepath.basename f}}
 let string_of_rng r =
-    Format.fmt3 "%s(%s-%s)" r.file_name (string_of_pos r.start_pos) (string_of_pos r.end_pos)
+    Format.fmt3 "%s:%s-%s" r.file_name (string_of_pos r.start_pos) (string_of_pos r.end_pos)
 let string_of_def_range r = string_of_rng r.def_range
 let string_of_use_range r = string_of_rng r.use_range
 let string_of_range r     = string_of_def_range r
@@ -90,7 +90,11 @@ let extend_to_end_of_line r = mk_range (file_of_range r)
                                        (end_of_line (end_of_range r))
 
 let json_of_pos pos =
-  JsonList [JsonInt (line_of_pos pos); JsonInt (col_of_pos pos)]
+  (* This -1 below is here since the IDE expects 0-based column numbers,
+     while we internally keep 1-based column numbers. In fact, the VS Code
+     extension does a +1 to adjust the number into 1-based numbering, so
+     that +1 and this -1 should both be removed. *)
+  JsonList [JsonInt (line_of_pos pos); JsonInt (col_of_pos pos - 1)]
 
 let json_of_range_fields file b e =
   JsonAssoc [("fname", JsonStr file);

src/interactive/FStarC.Interactive.Ide.fst

@@ -533,7 +533,7 @@ let run_segment (st: repl_state) (code: string) =
   // Unfortunately, frag_fname is a special case in the interactive mode,
   // while in LSP, it is the only mode. To cope with this difference,
   // pass a frag_fname that is expected by the Interactive mode.
-  let frag = { frag_fname = st.repl_fname; frag_text = code; frag_line = 1; frag_col = 0 } in
+  let frag = { frag_fname = st.repl_fname; frag_text = code; frag_line = 1; frag_col = 1 } in
 
   let collect_decls () =
     match Parser.Driver.parse_fragment None frag with

src/ml/FStarC_Format.ml

@@ -15,11 +15,11 @@ let colorize (o, c) s =
   | _ -> s
 
 let colorize_bold    = colorize ("\x1b[39;1m", "\x1b[0m")
-let colorize_red     = colorize ("\x1b[31;1m", "\x1b[0m")
-let colorize_yellow  = colorize ("\x1b[33;1m", "\x1b[0m")
-let colorize_cyan    = colorize ("\x1b[36;1m", "\x1b[0m")
-let colorize_green   = colorize ("\x1b[32;1m", "\x1b[0m")
-let colorize_magenta = colorize ("\x1b[35;1m", "\x1b[0m")
+let colorize_red     = colorize ("\x1b[31m", "\x1b[0m")
+let colorize_yellow  = colorize ("\x1b[33m", "\x1b[0m")
+let colorize_cyan    = colorize ("\x1b[36m", "\x1b[0m")
+let colorize_green   = colorize ("\x1b[32m", "\x1b[0m")
+let colorize_magenta = colorize ("\x1b[35m", "\x1b[0m")
 
 type printer = {
   printer_prinfo: string -> unit;

src/ml/FStarC_Parser_ParseIt.ml

@@ -187,18 +187,19 @@ let parse_incremental_decls
   in
   parse []
 
-let contents_at contents =
+let contents_at (contents : string) : Range.t -> code_fragment =
     let lines = U.splitlines contents in
     let split_line_at_col line col =
-        if col > 0
+        (* NB: columns are 1-based *)
+        if col > 1
         then (
             (* Don't index directly into the string, since this is a UTF-8 string.
                 Convert first to a list of characters, index into that, and then convert
                 back to a string *)
             let chars = FStar_String.list_of_string line in
-            if col <= List.length chars
+            if col <= List.length chars + 1
             then (
-              let prefix, suffix = FStarC_Util.first_N (Z.of_int col) chars in
+              let prefix, suffix = FStarC_Util.first_N (Z.of_int (col - 1)) chars in
               Some (FStar_String.string_of_list prefix, 
                     FStar_String.string_of_list suffix)
             )

src/ml/FStarC_Parser_Util.ml

@@ -12,7 +12,7 @@ type bytes = byte array
 let parseState = ()
 
 let pos_of_lexpos (p:position) =
-  mk_pos (Z.of_int p.pos_lnum) (Z.of_int (p.pos_cnum - p.pos_bol))
+  mk_pos (Z.of_int p.pos_lnum) (Z.of_int (1 + p.pos_cnum - p.pos_bol))
 
 let mksyn_range (p1:position) p2 =
   mk_range p1.pos_fname (pos_of_lexpos p1) (pos_of_lexpos p2)

src/tests/FStarC.Tests.Pars.fst

@@ -224,11 +224,11 @@ let parse_incremental_decls () =
   let input0 = Incremental { frag_fname = "Demo.fst";
                              frag_text = source0;
                              frag_line = 1;
-                             frag_col = 0 } in
+                             frag_col = 1 } in
   let input1 = Incremental { frag_fname = "Demo.fst";
                              frag_text = source1;
                              frag_line = 1;
-                             frag_col = 0 } in
+                             frag_col = 1 } in
   let open FStarC.Range in
   match parse None input0, parse None input1 with
   | IncrementalFragment (decls0, _, parse_err0),
@@ -250,8 +250,8 @@ let parse_incremental_decls () =
         | _, None ->
           failwith "Incremental parsing failed: Expected syntax error at (9, 6), got no error"
         | Some (_, _, rng0), Some (_, _, rng1)  ->
-          check_range rng0 11 6;
-          check_range rng1 12 6
+          check_range rng0 11 7;
+          check_range rng1 12 7
       in
       match decls0, decls1 with
       | [d0;d1;d2;d3;d4;d5],

tests/bug-reports/closed/Bug3757.fst.output.expected

@@ -1,18 +1,18 @@
-* Info at Bug3757.fst(8,4-8,13):
+* Info at Bug3757.fst:8.5-8.14:
   - Expected failure:
   - Expected a pattern of type Prims.int & Prims.int
   - Type FStar.Pervasives.Native.tuple2 is not a record type.
 
-* Info at Bug3757.fst(12,28-12,31):
+* Info at Bug3757.fst:12.29-12.32:
   - Expected failure:
   - Expected an expression of type Prims.int & Prims.bool
   - Type FStar.Pervasives.Native.tuple2 is not a record type.
 
-* Info at Bug3757.fst(15,15-15,17):
+* Info at Bug3757.fst:15.16-15.18:
   - Expected failure:
   - Field name _1 could not be resolved.
 
-* Info at Bug3757.fst(21,9-21,11):
+* Info at Bug3757.fst:21.10-21.12:
   - Expected failure:
   - Field name f1 could not be resolved.
 

tests/bug-reports/closed/Bug3980.fst.output.expected

@@ -1,26 +1,26 @@
-* Info at Bug3980.fst(16,0-16,24):
+* Info at Bug3980.fst:16.1-16.25:
   - Term Bug3980.p 1 ** Bug3980.p 2 ** Bug3980.p 3 has type Bug3980.slprop
 
-* Info at Bug3980.fst(17,0-17,26):
+* Info at Bug3980.fst:17.1-17.27:
   - Term (Bug3980.p 1 ** Bug3980.p 2) ** Bug3980.p 3 has type Bug3980.slprop
 
-* Info at Bug3980.fst(18,0-18,26):
+* Info at Bug3980.fst:18.1-18.27:
   - Term Bug3980.p 1 ** Bug3980.p 2 ** Bug3980.p 3 has type Bug3980.slprop
 
-* Info at Bug3980.fst(23,8-23,14):
+* Info at Bug3980.fst:23.9-23.15:
   - Expected failure:
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Bug3980.fst(23,15-23,23)
+  - See also Bug3980.fst:23.16-23.24
 
-* Info at Bug3980.fst(25,8-25,14):
+* Info at Bug3980.fst:25.9-25.15:
   - Expected failure:
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Bug3980.fst(25,15-25,23)
+  - See also Bug3980.fst:25.16-25.24
 
-* Info at Bug3980.fst(33,0-33,29):
+* Info at Bug3980.fst:33.1-33.30:
   - Term "a" |-> 1 ** "b" |-> 2 has type Bug3980.slprop
 

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

@@ -1,3 +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"]}
-{"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":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]}
+{"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":5},"end_pos":{"line":3,"col":6}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":5},"end_pos":{"line":3,"col":6}}},"number":240,"ctx":["While desugaring module AQualMismatch"]}
+{"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":8},"end_pos":{"line":6,"col":9}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":8},"end_pos":{"line":6,"col":9}}},"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":"AQualMismatch.fst","start_pos":{"line":6,"col":1},"end_pos":{"line":6,"col":13}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":1},"end_pos":{"line":6,"col":13}}},"number":240,"ctx":[]}

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

@@ -1,13 +1,13 @@
-* Warning 240 at AQualMismatch.fst(3,4-3,5):
+* Warning 240 at AQualMismatch.fst:3.5-3.6:
   - AQualMismatch.f is declared but no definition was found
   - Add an 'assume' if this is intentional
 
-* Info at AQualMismatch.fst(6,7-6,8):
+* Info at AQualMismatch.fst:6.8-6.9:
   - Expected failure:
   - Inconsistent implicit argument annotation on argument x
   - Got: '#'
   - Expected: ''
 
-* Warning 240 at AQualMismatch.fst(6,0-6,12):
+* Warning 240 at AQualMismatch.fst:6.1-6.13:
   - Missing definitions in module AQualMismatch: f
 

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

@@ -1,2 +1,2 @@
-{"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`"]}
+{"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":6},"end_pos":{"line":19,"col":8}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":6},"end_pos":{"line":19,"col":8}}},"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":15},"end_pos":{"line":27,"col":17}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":15},"end_pos":{"line":27,"col":17}}},"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,9 +1,9 @@
-* Info at AnotType.fst(19,5-19,7):
+* Info at AnotType.fst:19.6-19.8:
   - Expected failure:
   - Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype,
     or it is eqtype but contains noeq/unopteq qualifiers
 
-* Info at AnotType.fst(27,14-27,16):
+* Info at AnotType.fst:27.15-27.17:
   - Expected failure:
   - Expected expression of type Type0 got expression tb of type Type
 

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

@@ -1,3 +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"]}
-{"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":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]}
+{"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":5},"end_pos":{"line":23,"col":10}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":5},"end_pos":{"line":23,"col":10}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]}
+{"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":17},"end_pos":{"line":25,"col":19}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":17},"end_pos":{"line":25,"col":19}}},"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":"ArgsAndQuals.fst","start_pos":{"line":25,"col":1},"end_pos":{"line":25,"col":30}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":1},"end_pos":{"line":25,"col":30}}},"number":240,"ctx":[]}

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

@@ -1,13 +1,13 @@
-* Warning 240 at ArgsAndQuals.fst(23,4-23,9):
+* Warning 240 at ArgsAndQuals.fst:23.5-23.10:
   - ArgsAndQuals.test1 is declared but no definition was found
   - Add an 'assume' if this is intentional
 
-* Info at ArgsAndQuals.fst(25,16-25,18):
+* Info at ArgsAndQuals.fst:25.17-25.19:
   - Expected failure:
   - Inconsistent implicit argument annotation on argument uu___
   - Got: '#'
   - Expected: '$'
 
-* Warning 240 at ArgsAndQuals.fst(25,0-25,29):
+* Warning 240 at ArgsAndQuals.fst:25.1-25.30:
   - Missing definitions in module ArgsAndQuals: test1