From 7e930d86701c9dfc31740211525101e2a5d4e942 Mon Sep 17 00:00:00 2001
From: Alessandro Coglio <coglio@kestrel.edu>
Date: Tue, 8 Mar 2022 21:08:59 -0800
Subject: [PATCH] [ABNF] Fix use of integers in literals.

This removes the rule for `integer` and uses `natural` for all numeric literals.

Otherwise, lexing would be context-dependent for no good reason.

This is consistent with the lexer and parser of the Leo compiler.

Note that, for instance, `-1field` is not a literal, but rather a unary
expression where `-` is applied to the literal `1field`. This is consistent with
other languages too.
---
 docs/grammar/README.md        | 35 ++++++++++++-----------------------
 docs/grammar/abnf-grammar.txt | 21 ++++++++-------------
 2 files changed, 20 insertions(+), 36 deletions(-)

diff --git a/docs/grammar/README.md b/docs/grammar/README.md
index 04616cec3a..9dd11c0471 100644
--- a/docs/grammar/README.md
+++ b/docs/grammar/README.md
@@ -643,17 +643,6 @@ We allow leading zeros, e.g. `007`.
 natural = 1*decimal-digit
 ```
 
-An integer (number) is either a natural or its negation.
-We allow leading zeros also in negative numbers, e.g. `-007`.
-
-<a name="integer"></a>
-```abnf
-integer = [ "-" ] natural
-```
-
-Go to: _[natural](#user-content-natural)_;
-
-
 Unsigned literals are naturals followed by unsigned types.
 
 <a name="unsigned-literal"></a>
@@ -664,38 +653,38 @@ unsigned-literal = natural ( %s"u8" / %s"u16" / %s"u32" / %s"u64" / %s"u128" )
 Go to: _[natural](#user-content-natural)_;
 
 
-Signed literals are integers followed by signed types.
+Signed literals are naturals followed by signed types.
 
 <a name="signed-literal"></a>
 ```abnf
-signed-literal = integer ( %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128" )
+signed-literal = natural ( %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128" )
 ```
 
-Go to: _[integer](#user-content-integer)_;
+Go to: _[natural](#user-content-natural)_;
 
 
-Field literals are integers followed by the type of field elements.
+Field literals are naturals followed by the type of field elements.
 
 <a name="field-literal"></a>
 ```abnf
-field-literal = integer %s"field"
+field-literal = natural %s"field"
 ```
 
-Go to: _[integer](#user-content-integer)_;
+Go to: _[natural](#user-content-natural)_;
 
 
 There are two kinds of group literals.
-One is a single integer followed by the type of group elements,
-which denotes the scalar product of the generator point by the integer.
+One is a single natural followed by the type of group elements,
+which denotes the scalar product of the generator point by the natural.
 The other kind is not a token because it allows some whitespace inside;
 therefore, it is defined in the syntactic grammar.
 
 <a name="product-group-literal"></a>
 ```abnf
-product-group-literal = integer %s"group"
+product-group-literal = natural %s"group"
 ```
 
-Go to: _[integer](#user-content-integer)_;
+Go to: _[natural](#user-content-natural)_;
 
 
 Boolean literals are the usual two.
@@ -1080,10 +1069,10 @@ because it consists of affine point coordinates.
 
 <a name="group-coordinate"></a>
 ```abnf
-group-coordinate = integer / "+" / "-" / "_"
+group-coordinate = [ "-" ] natural / "+" / "-" / "_"
 ```
 
-Go to: _[integer](#user-content-integer)_;
+Go to: _[natural](#user-content-natural)_;
 
 
 <a name="affine-group-literal"></a>
diff --git a/docs/grammar/abnf-grammar.txt b/docs/grammar/abnf-grammar.txt
index fc903b6c85..3fc364bf3b 100644
--- a/docs/grammar/abnf-grammar.txt
+++ b/docs/grammar/abnf-grammar.txt
@@ -456,30 +456,25 @@ annotation-name = "@" identifier
 
 natural = 1*decimal-digit
 
-; An integer (number) is either a natural or its negation.
-; We allow leading zeros also in negative numbers, e.g. `-007`.
-
-integer = [ "-" ] natural
-
 ; Unsigned literals are naturals followed by unsigned types.
 
 unsigned-literal = natural ( %s"u8" / %s"u16" / %s"u32" / %s"u64" / %s"u128" )
 
-; Signed literals are integers followed by signed types.
+; Signed literals are naturals followed by signed types.
 
-signed-literal = integer ( %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128" )
+signed-literal = natural ( %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128" )
 
-; Field literals are integers followed by the type of field elements.
+; Field literals are naturals followed by the type of field elements.
 
-field-literal = integer %s"field"
+field-literal = natural %s"field"
 
 ; There are two kinds of group literals.
-; One is a single integer followed by the type of group elements,
-; which denotes the scalar product of the generator point by the integer.
+; One is a single natural followed by the type of group elements,
+; which denotes the scalar product of the generator point by the natural.
 ; The other kind is not a token because it allows some whitespace inside;
 ; therefore, it is defined in the syntactic grammar.
 
-product-group-literal = integer %s"group"
+product-group-literal = natural %s"group"
 
 ; Boolean literals are the usual two.
 
@@ -688,7 +683,7 @@ named-type = identifier / self-type / scalar-type
 ; This is an affine group literal,
 ; because it consists of affine point coordinates.
 
-group-coordinate = integer / "+" / "-" / "_"
+group-coordinate = [ "-" ] natural / "+" / "-" / "_"
 
 affine-group-literal = "(" group-coordinate "," group-coordinate %s")group"