Parse integers and negative floats for notations (Deducteam#1093)

* Parse integers and negative floats for notations * Update manual * Fix lexing Use non overlapping syntactical classes * Don't test raw_dk on iss706.lp (notation) * Update Makefile.bnf to include neg_nat --------- Co-authored-by: Frédéric Blanqui <[email protected]>
fblanqui · Apr 24, 2024 · 0902592 · 0902592
1 parent bc7e377
commit 0902592
Show file tree

Hide file tree

Showing 7 changed files with 23 additions and 13 deletions.
diff --git a/doc/Makefile.bnf b/doc/Makefile.bnf
@@ -39,6 +39,7 @@ lambdapi.bnf: Makefile.bnf ../src/parsing/lpParser.mly
 	-e 's/INFIX/"infix"/g' \
 	-e 's/INJECTIVE/"injective"/g' \
 	-e 's/LET/"let"/g' \
+        -e 's/NEG_NAT/"-"<nat>/g' \
 	-e 's/NAT/<nat>/g' \
 	-e 's/NOTATION/"notation"/g' \
 	-e 's/OPEN/"open"/g' \

diff --git a/doc/commands.rst b/doc/commands.rst
@@ -224,7 +224,7 @@ priority levels ``6`` and ``7`` respectively.
 The modifier ``infix``, ``infix right`` and ``infix left`` can be used
 to specify whether the defined symbol is non-associative, associative to
 the right, or associative to the left.
-Priority levels are non-negative floating point numbers, hence a
+Priority levels are floating point numbers, hence a
 priority can (almost) always be inserted between two different levels.
 
 As explained above, at this point, ``+`` is not a valid term anymore, as it was
@@ -251,8 +251,6 @@ negation with some priority level.
 * The functional arrow has a lower binding power than any operator, therefore
   for any prefix operator ``-``, ``- A → A`` is always parsed ``(- A) → A``
 
-* Parsing of operators is performed with the `pratter`_ library.
-
 
 **quantifier** Allows to write ```f x, t`` instead of ``f (λ x, t)``:
 

diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
@@ -176,12 +176,13 @@ QID ::= [UID "."]+ UID
 
 <equation> ::= <term> "≡" <term>
 
-<notation> ::= "infix" [<side>] <float_or_nat>
-             | "postfix" <float_or_nat>
-             | "prefix" <float_or_nat>
+<notation> ::= "infix" [<side>] <float_or_int>
+             | "postfix" <float_or_int>
+             | "prefix" <float_or_int>
              | "quantifier"
 
-<float_or_nat> ::= <float>
+<float_or_int> ::= <float>
+                 | "-"<nat>
                  | <nat>
 
 <maybe_generalize> ::= ["generalize"]

diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
@@ -92,6 +92,7 @@ type token =
   | DEBUG_FLAGS of (bool * string)
       (* Tuple constructor (with parens) required by Menhir. *)
   | NAT of string
+  | NEG_NAT of string
   | FLOAT of string
   | SIDE of Pratter.associativity
   | STRINGLIT of string
@@ -131,7 +132,8 @@ type token =
 let space = [%sedlex.regexp? Chars " \t\n\r"]
 let digit = [%sedlex.regexp? '0' .. '9']
 let nat = [%sedlex.regexp? '0' | ('1' .. '9', Star digit)]
-let float = [%sedlex.regexp? nat, '.', Plus digit]
+let neg_nat = [%sedlex.regexp? '-', nat]
+let float = [%sedlex.regexp? (nat | neg_nat), '.', Plus digit]
 let oneline_comment = [%sedlex.regexp? "//", Star (Compl ('\n' | '\r'))]
 let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
 
@@ -261,6 +263,7 @@ let rec token lb =
   (* other tokens *)
   | '+', Plus lowercase -> DEBUG_FLAGS(true, remove_first lb)
   | '-', Plus lowercase -> DEBUG_FLAGS(false, remove_first lb)
+  | neg_nat -> NEG_NAT(Utf8.lexeme lb)
   | nat -> NAT(Utf8.lexeme lb)
   | float -> FLOAT(Utf8.lexeme lb)
   | string -> STRINGLIT(Utf8.sub_lexeme lb 1 (lexeme_length lb - 2))

diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
@@ -85,6 +85,7 @@
 
 %token <bool * string> DEBUG_FLAGS
 %token <string> NAT
+%token <string> NEG_NAT
 %token <string> FLOAT
 %token <Pratter.associativity> SIDE
 %token <string> STRINGLIT
@@ -395,14 +396,15 @@ unif_rule: e=equation HOOK_ARROW
 equation: l=term EQUIV r=term { (l, r) }
 
 notation:
-  | INFIX a=SIDE? p=float_or_nat
+  | INFIX a=SIDE? p=float_or_int
     { Sign.Infix(Option.get Pratter.Neither a, p) }
-  | POSTFIX p=float_or_nat { Sign.Postfix(p) }
-  | PREFIX p=float_or_nat { Sign.Prefix(p) }
+  | POSTFIX p=float_or_int { Sign.Postfix(p) }
+  | PREFIX p=float_or_int { Sign.Prefix(p) }
   | QUANTIFIER { Sign.Quant }
 
-float_or_nat:
+float_or_int:
   | s=FLOAT { s }
+  | s=NEG_NAT { s }
   | s=NAT { s }
 
 maybe_generalize:

diff --git a/tests/OK/iss706.lp b/tests/OK/iss706.lp
@@ -0,0 +1,5 @@
+// Support for negative priorities.
+
+symbol E : TYPE;
+symbol o (_ _: E): E;
+notation o infix -3;
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
@@ -52,7 +52,7 @@ do
         # "as"
         729);;
         # "notation"
-        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|iss861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|builtin_zero_succ|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026);;
+        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|iss861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|builtin_zero_succ|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|iss706);;
         # "quantifier"
         683|650|573|565|430);;
         # nested module name