ProvableHQ/leo
1
1
Fork 0
mirror of https://github.com/ProvableHQ/leo.git synced 2024-12-23 02:01:54 +03:00
Code Issues Packages Projects Releases Wiki Activity

[ABNF] Fix use of integers in literals.

Browse Source 
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.
This commit is contained in:
Alessandro Coglio 2022-03-08 21:08:59 -08:00
parent 646c5eb697
commit 7e930d8670
2 changed files with 20 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
docs/grammar/README.md
View File

@ -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>

21
docs/grammar/abnf-grammar.txt
View File

@ -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"