Merge pull request #3293 from mtzguido/3292

Partial fix for 3292

src/parser/FStar.Parser.AST.fst

@@ -328,15 +328,15 @@ let string_to_op s =
     match s with
     | "Amp" ->  Some ("&", None)
     | "At" -> Some ("@", None)
-    | "Plus" -> Some ("+", None)
+    | "Plus" -> Some ("+", Some 2)
     | "Minus" -> Some ("-", None)
     | "Subtraction" -> Some ("-", Some 2)
     | "Tilde" -> Some ("~", None)
-    | "Slash" -> Some ("/", None)
+    | "Slash" -> Some ("/", Some 2)
     | "Backslash" -> Some ("\\", None)
-    | "Less" -> Some ("<", None)
+    | "Less" -> Some ("<", Some 2)
     | "Equals" -> Some ("=", None)
-    | "Greater" -> Some (">", None)
+    | "Greater" -> Some (">", Some 2)
     | "Underscore" -> Some ("_", None)
     | "Bar" -> Some ("|", None)
     | "Bang" -> Some ("!", None)

src/parser/FStar.Parser.AST.fsti

@@ -303,7 +303,7 @@ val strip_prefix : string -> string -> option string
 
 val compile_op : int -> string -> range -> string
 val compile_op' : string -> range -> string
-val string_to_op : string -> option (string & option int)
+val string_to_op : string -> option (string & option int) // returns operator symbol and optional arity
 
 val string_of_fsdoc : string & list (string & string) -> string
 val string_of_let_qualifier : let_qualifier -> string

tests/error-messages/Bug3292.fst

@@ -0,0 +1,19 @@
+module Bug3292
+
+#set-options "--print_implicits"
+
+let op_Plus #a (x y : a) = (x,y)
+let op_Minus #a (x y : a) = (x,y)
+let op_Slash #a (x y : a) = (x,y)
+let op_Greater #a (x y : a) = (x,y)
+let op_Less #a (x y : a) = (x,y)
+let op_GreaterEquals #a (x y : a) = (x,y)
+let op_LessEquals #a (x y : a) = (x,y)
+
+let _ = 1 + 1
+let _ = 1 - 1
+let _ = 1 / 1
+let _ = 1 > 1
+let _ = 1 < 1
+let _ = 1 >= 1
+let _ = 1 <= 1

tests/error-messages/Bug3292.fst.expected

@@ -0,0 +1,155 @@
+Module after desugaring:
+module Bug3292
+Declarations: [
+#set-options "--print_implicits"
+let op_Plus #a x y = x, y
+let op_Minus #a x y = x, y
+let op_Slash #a x y = x, y
+let op_Greater #a x y = x, y
+let op_Less #a x y = x, y
+let op_GreaterEquals #a x y = x, y
+let op_LessEquals #a x y = x, y
+private
+let _ = 1 + 1
+private
+let _ = 1 - 1
+private
+let _ = 1 / 1
+private
+let _ = 1 > 1
+private
+let _ = 1 < 1
+private
+let _ = 1 >= 1
+private
+let _ = 1 <= 1
+]
+Exports: [
+#set-options "--print_implicits"
+let op_Plus #a x y = x, y
+let op_Minus #a x y = x, y
+let op_Slash #a x y = x, y
+let op_Greater #a x y = x, y
+let op_Less #a x y = x, y
+let op_GreaterEquals #a x y = x, y
+let op_LessEquals #a x y = x, y
+private
+let _ = 1 + 1
+private
+let _ = 1 - 1
+private
+let _ = 1 / 1
+private
+let _ = 1 > 1
+private
+let _ = 1 < 1
+private
+let _ = 1 >= 1
+private
+let _ = 1 <= 1
+]
+
+Module before type checking:
+module Bug3292
+Declarations: [
+#set-options "--print_implicits"
+let op_Plus x y = x, y
+let op_Minus x y = x, y
+let op_Slash x y = x, y
+let op_Greater x y = x, y
+let op_Less x y = x, y
+let op_GreaterEquals x y = x, y
+let op_LessEquals x y = x, y
+private
+let _ = 1 + 1
+private
+let _ = 1 - 1
+private
+let _ = 1 / 1
+private
+let _ = 1 > 1
+private
+let _ = 1 < 1
+private
+let _ = 1 >= 1
+private
+let _ = 1 <= 1
+]
+Exports: [
+#set-options "--print_implicits"
+let op_Plus x y = x, y
+let op_Minus x y = x, y
+let op_Slash x y = x, y
+let op_Greater x y = x, y
+let op_Less x y = x, y
+let op_GreaterEquals x y = x, y
+let op_LessEquals x y = x, y
+private
+let _ = 1 + 1
+private
+let _ = 1 - 1
+private
+let _ = 1 / 1
+private
+let _ = 1 > 1
+private
+let _ = 1 < 1
+private
+let _ = 1 >= 1
+private
+let _ = 1 <= 1
+]
+
+Module after type checking:
+module Bug3292
+Declarations: [
+#set-options "--print_implicits"
+let op_Plus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Minus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Slash #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Greater #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Less #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_GreaterEquals #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_LessEquals #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+private
+let _ = Bug3292.op_Plus #Prims.int 1 1
+private
+let _ = 1 - 1
+private
+let _ = Bug3292.op_Slash #Prims.int 1 1
+private
+let _ = Bug3292.op_Greater #Prims.int 1 1
+private
+let _ = Bug3292.op_Less #Prims.int 1 1
+private
+let _ = 1 >= 1
+private
+let _ = 1 <= 1
+]
+Exports: [
+#set-options "--print_implicits"
+let op_Plus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Minus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Slash #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Greater #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_Less #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_GreaterEquals #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+let op_LessEquals #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
+private
+let _ = Bug3292.op_Plus #Prims.int 1 1
+private
+let _ = 1 - 1
+private
+let _ = Bug3292.op_Slash #Prims.int 1 1
+private
+let _ = Bug3292.op_Greater #Prims.int 1 1
+private
+let _ = Bug3292.op_Less #Prims.int 1 1
+private
+let _ = 1 >= 1
+private
+let _ = 1 <= 1
+]
+
+Verified module: Bug3292
+All verification conditions discharged successfully

tests/error-messages/Makefile

@@ -26,6 +26,7 @@ all: check-all
 Bug1997.fst.output: OTHERFLAGS+=--dump_module Bug1997
 Bug2820.fst.output: OTHERFLAGS+=--dump_module Bug2820
 Bug3227.fst.output: OTHERFLAGS+=--dump_module Bug3227
+Bug3292.fst.output: OTHERFLAGS+=--dump_module Bug3292
 CalcImpl.fst.output: OTHERFLAGS+=--dump_module CalcImpl
 
 include $(FSTAR_HOME)/examples/Makefile.common