Bad range on bogus operator

[mtzguido]

let (+) = 1
let test = 1 + 2

(Error) Expected a function; got an expression of type "int"

The error points to 1 and not to +

[mtzguido]

Ha, this was fun. Inline rules in the parser were to blame:

commit 93c97b29f1241bb51ceb5356e01935733064b808
Author: Guido Martínez <mtzguido@gmail.com>
Date:   Sun Mar 22 00:25:54 2020 -0300

    parser: fix issue #1955

    Fixes #1955

diff --git a/src/parser/parse.mly b/src/parser/parse.mly
index f7b1906a1a..1279db3503 100644
--- a/src/parser/parse.mly
+++ b/src/parser/parse.mly
@@ -1164,7 +1164,11 @@ range:
   | op=OPINFIX0d
   | op=OPINFIX1
   | op=OPINFIX2
-     { mk_ident (op, rhs parseState 1) }
+     { mk_ident (op, rhs parseState 2) }
+/* ATTENTION! We're getting the range from the second component of the
+ * parse rule since this is *INLINED* below in the tmEqWith(X) rule, and
+ * there this production appears in the second position. Were this not
+ * %inline, it should be 1. See issue #1955. */

 %inline dotOperator:
   | DOT_LPAREN e=term RPAREN { mk_ident (".()", rhs parseState 1), e, rhs2 parseState 1 3 }

[mtzguido]

This seems like a limitation of ocamlyacc though, since menhir's docs state that

Finally, we remark that Menhir’s %inline keyword (§5.3) does not affect the computation of positions. The same positions are computed, regardless of where %inline keywords are placed.

So not sure if I should merge this fix or not, since we plan to move to menhir eventually, right?

[nikswamy]

I'm confused ...we are using menhir

[mtzguido]

Maybe I'm confused myself but it seems we use menhir only to preprocess the grammar and then we call ocamlyacc:

parse.mly: ../parser/parse.mly
ifeq ($(HAS_VALID_MENHIR), 1)
    @# TODO : call menhir directly when positions are fixed instead of
    @# letting OCamlbuild go through ocamlyacc
    $(MENHIR) --only-preprocess-for-ocamlyacc $< > $@
else
    $(error Correct version of menhir not found (needs a version newer than $(MENHIR_MIN_VERSION)))
endif

FStar_Parser_Parse.ml: parse.mly
    @# We are opening the same module twice but we need these modules
    @# open for the definition of tokens
    echo "open Prims" > $@
    echo "open FStar_Errors" >> $@
    echo "open FStar_List" >> $@
    echo "open FStar_Util" >> $@
    echo "open FStar_Range" >> $@
    echo "open FStar_Options" >> $@
    echo "open FStar_Syntax_Syntax" >> $@
    echo "open FStar_Parser_Const" >> $@
    echo "open FStar_Syntax_Util" >> $@
    echo "open FStar_Parser_AST" >> $@
    echo "open FStar_Parser_Util" >> $@
    echo "open FStar_Const" >> $@
    echo "open FStar_Ident" >> $@
    echo "open FStar_String" >> $@
    @# TODO: create a proper OCamlbuild rule for this production so that
    @# OCamlbuild knows how to generate parse.mly first (possibly using
    @# menhir) and removes the production as needed.
    ocamlyacc parse.mly 2> yac-log ### <--- HERE
    cat yac-log
    @if [ "0$$(grep "shift/reduce" yac-log | sed 's/^\([0-9]\+\).*/\1/')" -gt 6 ]; then \
      echo "shift-reduce conflicts have increased; please fix" && exit 255; \
    fi
    @if grep -q "reduce/reduce" yac-log ; then \
      echo "A reduce-reduce conflict was introduced; please fix" && exit 255; \
    fi
    cat parse.ml >> $@
    rm parse.ml parse.mli