From 09025929094d27ac2d401269d8bbd677e06e2dd2 Mon Sep 17 00:00:00 2001 From: Gabriel Hondet <7418676+gabrielhdt@users.noreply.github.com> Date: Wed, 24 Apr 2024 15:44:28 +0200 Subject: [PATCH] Parse integers and negative floats for notations (#1093) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 --- doc/Makefile.bnf | 1 + doc/commands.rst | 4 +--- doc/lambdapi.bnf | 9 +++++---- src/parsing/lpLexer.ml | 5 ++++- src/parsing/lpParser.mly | 10 ++++++---- tests/OK/iss706.lp | 5 +++++ tests/export_raw_dk.sh | 2 +- 7 files changed, 23 insertions(+), 13 deletions(-) create mode 100644 tests/OK/iss706.lp diff --git a/doc/Makefile.bnf b/doc/Makefile.bnf index d98702b79..e9e7d6a91 100644 --- 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/"-"/g' \ -e 's/NAT//g' \ -e 's/NOTATION/"notation"/g' \ -e 's/OPEN/"open"/g' \ diff --git a/doc/commands.rst b/doc/commands.rst index de0f288f8..38b7d95a5 100644 --- 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 index 6251318e9..75302a25a 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -176,12 +176,13 @@ QID ::= [UID "."]+ UID ::= "≡" - ::= "infix" [] - | "postfix" - | "prefix" + ::= "infix" [] + | "postfix" + | "prefix" | "quantifier" - ::= + ::= + | "-" | ::= ["generalize"] diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 045c8e045..cc349908d 100644 --- 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 index 9164f1dcf..c030535fc 100644 --- a/src/parsing/lpParser.mly +++ b/src/parsing/lpParser.mly @@ -85,6 +85,7 @@ %token DEBUG_FLAGS %token NAT +%token NEG_NAT %token FLOAT %token SIDE %token 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 new file mode 100644 index 000000000..73364e2a4 --- /dev/null +++ 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 index bf3541bd4..cbbf67d85 100755 --- 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