From d03da2e9d2a61ae47c9785d7c804e9863cd29321 Mon Sep 17 00:00:00 2001 From: trdthg Date: Wed, 10 Jul 2024 06:21:21 +0000 Subject: [PATCH] Fix lexer rule to handle operator of format like `operator + comment` --- src/lib/lexer.mll | 23 +++++++++++++----- test/format/default/operator.expect | 36 +++++++++++++++++++++++++++++ test/format/operator.sail | 28 ++++++++++++++++++++++ 3 files changed, 81 insertions(+), 6 deletions(-) create mode 100644 test/format/default/operator.expect create mode 100644 test/format/operator.sail diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index 954abb364..d889d9a91 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -172,10 +172,12 @@ let tyvar_start = '\'' let oper_char = ['!''%''&''*''+''-''.''/'':''<''=''>''@''^''|'] let oper_char_no_slash = ['!''%''&''*''+''-''.'':''<''=''>''@''^''|'] let oper_char_no_slash_star = ['!''%''&''+''-''.'':''<''=''>''@''^''|'] -let operator1 = oper_char -let operator2 = oper_char oper_char_no_slash_star | oper_char_no_slash oper_char -let operatorn = oper_char oper_char_no_slash_star (oper_char* ('_' ident)?) | oper_char_no_slash oper_char (oper_char* ('_' ident)?) | oper_char ('_' ident)? -let operator = operator1 | operator2 | operatorn +let oper_char_no_star = ['!''%''&''+''-''.''/'':''<''=''>''@''^''|'] +let operator_any_start = oper_char (oper_char_no_slash_star oper_char)* + | (oper_char oper_char_no_slash_star)* +let operator_no_slash_start = oper_char_no_slash (oper_char oper_char_no_slash_star)* + | (oper_char_no_slash_star oper_char)* +let operator = (operator_any_start | operator_no_slash_start) ('_' ident)? let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit) let lchar = [^'\n'] @@ -188,7 +190,7 @@ rule token comments = parse token comments lexbuf } | "@" { At } | "2" ws "^" { TwoCaret } - | "^" { Caret } + | "^" { Caret } | "::" { ColonColon } | ":" { Colon ":" } | "," { Comma } @@ -235,7 +237,16 @@ rule token comments = parse { Fixity (InfixL, Big_int.of_string (Char.escaped p), op) } | "infixr" ws (digit as p) ws (operator as op) { Fixity (InfixR, Big_int.of_string (Char.escaped p), op) } - | operator as op { OpId op } + | operator as op { + OpId op } + | (operator as op) ['/'] ['*'] { + block_comment comments (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 lexbuf; + if op = "=" then Eq "=" else OpId op + } + | (operator as op) ['/'] ['/'] { + line_comment comments (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf; + if op = "=" then Eq "=" else OpId op + } | tyvar_start startident ident* as i { TyVar i } | "~" { Id "~" } | startident ident* as i { if M.mem i kw_table then diff --git a/test/format/default/operator.expect b/test/format/default/operator.expect new file mode 100644 index 000000000..37d688bbc --- /dev/null +++ b/test/format/default/operator.expect @@ -0,0 +1,36 @@ +default Order dec +$include + +infix 4 ===_u +infix 4 =/ +infix 4 ===/_u +infix 4 /=/=/=_u +infix 4 ===*_u + +val operator ===/_u : forall 'n. (int('n), int('n)) -> bool +function operator ===/_u(x, y) = x == y + +val operator =/ : forall 'n. (int('n), int('n)) -> bool +function operator =/(x, y) = x == y + +function f () = { + if eq2_comment == /**/ /**/ 1 then { + 1 + }; + + if eq_slash =/ 1 then { + 1 + }; + + let eq_comment = + /**/ 1; + let eq_comment = + // + 1; + + if eq3_slash ===/_u 1 then { + 1 + }; + + 0 +} diff --git a/test/format/operator.sail b/test/format/operator.sail new file mode 100644 index 000000000..054646911 --- /dev/null +++ b/test/format/operator.sail @@ -0,0 +1,28 @@ +default Order dec +$include + +infix 4 ===_u +infix 4 =/ +infix 4 ===/_u +infix 4 /=/=/=_u +infix 4 ===*_u + +val operator ===/_u : forall 'n. (int('n), int('n)) -> bool +function operator ===/_u(x, y) = x == y + +val operator =/ : forall 'n. (int('n), int('n)) -> bool +function operator =/(x, y) = x == y + +function f () = { + if eq2_comment /**/==/**/ 1 then { 1 }; + + if eq_slash =/ 1 then { 1 }; + + let eq_comment =/**/ 1; + let eq_comment =// + 1; + + if eq3_slash ===/_u 1 then { 1 }; + + 0 +}