From 2db5c590f7390e344c699dffe60b104186bff76d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Tue, 30 Apr 2024 14:45:16 +0200
Subject: [PATCH] fix #1103 (#1104)

---
 doc/lambdapi.bnf         | 29 ++++++++++++++++-------------
 src/parsing/lpLexer.ml   |  5 +++--
 src/parsing/lpParser.mly | 26 +++++++++++++++-----------
 tests/OK/1103.lp         |  3 +++
 tests/OK/1103b.lp        |  3 +++
 5 files changed, 40 insertions(+), 26 deletions(-)
 create mode 100644 tests/OK/1103.lp
 create mode 100644 tests/OK/1103b.lp

diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index 75302a25a..3f794d123 100644
--- a/doc/lambdapi.bnf
+++ b/doc/lambdapi.bnf
@@ -18,22 +18,22 @@ QID ::= [UID "."]+ UID
 
 <search_query_alone> ::= <search_query> EOF
 
-<command> ::= "opaque" <qid_or_nat> ";"
+<command> ::= "opaque" <qid_or_int> ";"
             | "require" "open" <path>* ";"
             | "require" <path>* ";"
             | "require" <path> "as" <uid> ";"
             | "open" <path>* ";"
-            | <modifier>* "symbol" <uid_or_nat> <param_list>* ":" <term>
+            | <modifier>* "symbol" <uid_or_int> <param_list>* ":" <term>
               [<proof>] ";"
-            | <modifier>* "symbol" <uid_or_nat> <param_list>* [":" <term>]
+            | <modifier>* "symbol" <uid_or_int> <param_list>* [":" <term>]
               "≔" <term_proof> ";"
             | [<exposition>] <param_list>* "inductive" <inductive> ("with"
               <inductive>)* ";"
             | "rule" <rule> ("with" <rule>)* ";"
-            | "builtin" <stringlit> "≔" <qid_or_nat> ";"
+            | "builtin" <stringlit> "≔" <qid_or_int> ";"
             | "coerce_rule" <rule> ";"
             | "unif_rule" <unif_rule> ";"
-            | "notation" <qid_or_nat> <notation> ";"
+            | "notation" <qid_or_int> <notation> ";"
             | <query> ";"
             
 
@@ -70,11 +70,11 @@ QID ::= [UID "."]+ UID
 
 <uid> ::= UID
 
-<uid_or_nat> ::= <uid>
-               | <nat>
+<uid_or_int> ::= <uid>
+               | <int>
 
-<qid_or_nat> ::= <qid>
-               | <nat>
+<qid_or_int> ::= <qid>
+               | <int>
 
 <param_list> ::= <param>
                | "(" <param>+ ":" <term> ")"
@@ -104,6 +104,7 @@ QID ::= [UID "."]+ UID
           | "(" <term> ")"
           | "[" <term> "]"
           | <nat>
+          | "-"<nat>
 
 <env> ::= "." "[" [<term> (";" <term>)*] "]"
 
@@ -150,7 +151,7 @@ QID ::= [UID "."]+ UID
            | "reflexivity"
            | "remove" <uid>+
            | "rewrite" [<side>] [<rw_patt_spec>] <term>
-           | "simplify" [<qid_or_nat>]
+           | "simplify" [<qid_or_int>]
            | "solve"
            | "symmetry"
            | "try" <tactic>
@@ -167,7 +168,7 @@ QID ::= [UID "."]+ UID
 <inductive> ::= <uid> <param_list>* ":" <term> "≔" ["|"] [<constructor>
                 ("|" <constructor>)*]
 
-<constructor> ::= <uid_or_nat> <param_list>* ":" <term>
+<constructor> ::= <uid_or_int> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
 
@@ -182,8 +183,10 @@ QID ::= [UID "."]+ UID
              | "quantifier"
 
 <float_or_int> ::= <float>
-                 | "-"<nat>
-                 | <nat>
+                 | <int>
+
+<int> ::= "-"<nat>
+        | <nat>
 
 <maybe_generalize> ::= ["generalize"]
 
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index cc349908d..f2e767427 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -131,8 +131,9 @@ type token =
 (** Some regexp definitions. *)
 let space = [%sedlex.regexp? Chars " \t\n\r"]
 let digit = [%sedlex.regexp? '0' .. '9']
-let nat = [%sedlex.regexp? '0' | ('1' .. '9', Star digit)]
-let neg_nat = [%sedlex.regexp? '-', nat]
+let pos = [%sedlex.regexp? ('1' .. '9', Star digit)]
+let nat = [%sedlex.regexp? '0' | pos]
+let neg_nat = [%sedlex.regexp? '-', pos]
 let float = [%sedlex.regexp? (nat | neg_nat), '.', Plus digit]
 let oneline_comment = [%sedlex.regexp? "//", Star (Compl ('\n' | '\r'))]
 let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
index c030535fc..c25a151fc 100644
--- a/src/parsing/lpParser.mly
+++ b/src/parsing/lpParser.mly
@@ -149,7 +149,7 @@ search_query_alone:
     { q }
 
 command:
-  | OPAQUE i=qid_or_nat SEMICOLON { make_pos $sloc (P_opaque i) }
+  | OPAQUE i=qid_or_int SEMICOLON { make_pos $sloc (P_opaque i) }
   | REQUIRE OPEN l=list(path) SEMICOLON
     { make_pos $sloc (P_require(true,l)) }
   | REQUIRE l=list(path) SEMICOLON
@@ -158,13 +158,13 @@ command:
     { make_pos $sloc (P_require_as(p,i)) }
   | OPEN l=list(path) SEMICOLON
     { make_pos $sloc (P_open l) }
-  | ms=modifier* SYMBOL s=uid_or_nat al=param_list* COLON a=term
+  | ms=modifier* SYMBOL s=uid_or_int al=param_list* COLON a=term
     po=proof? SEMICOLON
     { let sym =
         {p_sym_mod=ms; p_sym_nam=s; p_sym_arg=al; p_sym_typ=Some(a);
          p_sym_trm=None; p_sym_def=false; p_sym_prf=po}
       in make_pos $sloc (P_symbol(sym)) }
-  | ms=modifier* SYMBOL s=uid_or_nat al=param_list* ao=preceded(COLON, term)?
+  | ms=modifier* SYMBOL s=uid_or_int al=param_list* ao=preceded(COLON, term)?
     ASSIGN tp=term_proof SEMICOLON
     { let sym =
         {p_sym_mod=ms; p_sym_nam=s; p_sym_arg=al; p_sym_typ=ao;
@@ -175,11 +175,11 @@ command:
       { make_pos $sloc (P_inductive(Option.to_list exp,xs,is)) }
   | RULE rs=separated_nonempty_list(WITH, rule) SEMICOLON
       { make_pos $sloc (P_rules(rs)) }
-  | BUILTIN s=STRINGLIT ASSIGN i=qid_or_nat SEMICOLON
+  | BUILTIN s=STRINGLIT ASSIGN i=qid_or_int SEMICOLON
     { make_pos $loc (P_builtin(s,i)) }
   | COERCE_RULE r=rule SEMICOLON { make_pos $loc (P_coercion r) }
   | UNIF_RULE r=unif_rule SEMICOLON { make_pos $loc (P_unif_rule(r)) }
-  | NOTATION i=qid_or_nat n=notation SEMICOLON
+  | NOTATION i=qid_or_int n=notation SEMICOLON
     { make_pos $loc (P_notation(i,n)) }
   | q=query SEMICOLON { make_pos $sloc (P_query(q)) }
   | EOF { raise End_of_file }
@@ -237,13 +237,13 @@ exposition:
 
 uid: s=UID { make_pos $sloc s}
 
-uid_or_nat:
+uid_or_int:
   | i=uid { i }
-  | n=NAT { make_pos $sloc n }
+  | n=int { make_pos $sloc n }
 
-qid_or_nat:
+qid_or_int:
   | i=qid { i }
-  | n=NAT { make_pos $sloc ([],n) }
+  | n=int { make_pos $sloc ([],n) }
 
 param_list:
   | x=param { ([x], None, false) }
@@ -289,6 +289,7 @@ aterm:
   | L_PAREN t=term R_PAREN { make_pos $sloc (P_Wrap(t)) }
   | L_SQ_BRACKET t=term R_SQ_BRACKET { make_pos $sloc (P_Expl(t)) }
   | n=NAT { make_pos $sloc (P_NLit n) }
+  | n=NEG_NAT { make_pos $sloc (P_Iden(make_pos $sloc ([],n), false)) }
 
 env: DOT L_SQ_BRACKET ts=separated_list(SEMICOLON, term) R_SQ_BRACKET { ts }
 
@@ -346,7 +347,7 @@ tactic:
   | REWRITE d=SIDE? p=rw_patt_spec? t=term
     { let b = match d with Some Pratter.Left -> false | _ -> true in
       make_pos $sloc (P_tac_rewrite(b,p,t)) }
-  | SIMPLIFY i=qid_or_nat? { make_pos $sloc (P_tac_simpl i) }
+  | SIMPLIFY i=qid_or_int? { make_pos $sloc (P_tac_simpl i) }
   | SOLVE { make_pos $sloc P_tac_solve }
   | SYMMETRY { make_pos $sloc P_tac_sym }
   | TRY t=tactic { make_pos $sloc (P_tac_try t) }
@@ -375,7 +376,7 @@ inductive: i=uid ps=param_list* COLON t=term ASSIGN
     { let t = make_prod $startpos(ps) ps t $endpos(t) in
       make_pos $sloc (i,t,l) }
 
-constructor: i=uid_or_nat ps=param_list* COLON t=term
+constructor: i=uid_or_int ps=param_list* COLON t=term
     { (i, make_prod $startpos(ps) ps t $endpos(t)) }
 
 rule: l=term HOOK_ARROW r=term { make_pos $sloc (l, r) }
@@ -404,6 +405,9 @@ notation:
 
 float_or_int:
   | s=FLOAT { s }
+  | s=int { s }
+
+int:
   | s=NEG_NAT { s }
   | s=NAT { s }
 
diff --git a/tests/OK/1103.lp b/tests/OK/1103.lp
new file mode 100644
index 000000000..67be2cd69
--- /dev/null
+++ b/tests/OK/1103.lp
@@ -0,0 +1,3 @@
+symbol A:TYPE;
+symbol 2:A;
+symbol -2:A;
diff --git a/tests/OK/1103b.lp b/tests/OK/1103b.lp
new file mode 100644
index 000000000..e5c2d7f3b
--- /dev/null
+++ b/tests/OK/1103b.lp
@@ -0,0 +1,3 @@
+require tests.OK.1103;
+symbol a ≔ tests.OK.1103.2;
+symbol b ≔ tests.OK.1103.-2;