Syntax bug (nat literals, reported by Yacine).

rlepigre · Oct 17, 2018 · 1862846 · 1862846
1 parent 20a16bd
commit 1862846
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 6 deletions.
diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim
@@ -18,7 +18,7 @@ syntax include @markdown syntax/markdown.vim
 syntax region Comment start="///" end="$" contains=@markdown
 
 " Natural number.
-syntax match NaturalNumber "\<\([0]\|\([1-9][0-9]*\)\)\>"
+syntax match NaturalNumber "\<[0-9]\+\>"
 highlight link NaturalNumber PreProc
 
 " String literal.

diff --git a/src/parser.ml b/src/parser.ml
@@ -56,14 +56,13 @@ let _proofterm_  = KW.create "proofterm"
 
 (** Natural number literal. *)
 let nat_lit =
-  let head_cs = Charset.from_string "1-9" in
-  let body_cs = Charset.from_string "0-9" in
+  let nat_cs = Charset.from_string "0-9" in
   let fn buf pos =
     let nb = ref 1 in
-    while Charset.mem body_cs (Input.get buf (pos + !nb)) do incr nb done;
+    while Charset.mem nat_cs (Input.get buf (pos + !nb)) do incr nb done;
     (int_of_string (String.sub (Input.line buf) pos !nb), buf, pos + !nb)
   in
-  Earley.black_box fn head_cs false "<nat>"
+  Earley.black_box fn nat_cs false "<nat>"
 
 (** String literal. *)
 let string_lit =

diff --git a/syntax.bnf b/syntax.bnf
@@ -39,7 +39,7 @@ reserved "_"
 
 // Natural number literal
 <nat_lit> ::=
-  | RE("[1-9][0-9]*")
+  | RE("[0-9]+")
 
 // String literal
 <string_lit> ::=