From 3e94824ce6c95ff4adbc617128ea1c658ae2a51d Mon Sep 17 00:00:00 2001 From: trdthg Date: Tue, 23 Jul 2024 06:59:11 +0000 Subject: [PATCH 1/2] Fix lexer rule to handle operator of format like operator + comment --- src/lib/lexer.mll | 12 ++-- test/format/default/operator.expect | 97 +++++++++++++++++++++++++++++ test/format/operator.sail | 73 ++++++++++++++++++++++ 3 files changed, 177 insertions(+), 5 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..816109ae2 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 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 } diff --git a/test/format/default/operator.expect b/test/format/default/operator.expect new file mode 100644 index 000000000..43ae2e990 --- /dev/null +++ b/test/format/default/operator.expect @@ -0,0 +1,97 @@ +default Order dec +$include + +// comment +//comment +/// line_comment with more than two slash +///line_comment with more than two slash +//// line_comment with more than two slash +////line_comment with more than two slash +// /*/*/ +/*/ block_comment with slash near and +*/ +//* line_block_comment */ +infix 4 ===_u +infix 4 ===/_u +infix 4 /=/=/= + +infix 4 ===*_u +val operator ===/_u : forall 'n. (int('n), int('n)) -> bool +function operator ===/_u(x, y) = x == y + +infix 4 =/ +val operator =/ : forall 'n. (int('n), int('n)) -> bool +function operator =/(x, y) = x == y + +infix 4 = + +// comment +infix 4 =/ + +// comment +infix 4 ==/ +infix 4 -/- + +//comment +infix 4 -/-/ + +//comment +infix 4 /-* + +//comment +infixl 4 = + +// comment +infixl 4 =/ + +// comment +infixl 4 ==/ +infixl 4 -/- + +//comment +infixl 4 -/-/ + +//comment +infixl 4 /-* + +//comment +infixr 4 = + +// comment +infixr 4 =/ + +// comment +infixr 4 ==/ +infixr 4 -/- + +//comment +infixr 4 -/-/ + +//comment +infixr 4 /-* + +//comment +function f () = { + if op_eq2_with_block_comment == /**/ /**/ 1 then { 1 }; + + if op_eq_slash =/ 1 then { 1 }; + if op_eq_slash_with_block_comment =/ 1 then /**/ { 1 }; + + let op_eq_with_line_comment = + // + 1; + + let op_eq_with_line_comment = + /// + 1; + + if op_eq_with_line_comment = + // comment + if eq_slash = /**/ 1 then { 1 } else { 2 } then { 1 }; + + if eq_with_blcok_comment = /**/ 1 then { 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..5b286841a --- /dev/null +++ b/test/format/operator.sail @@ -0,0 +1,73 @@ +default Order dec +$include + +// comment +//comment +/// line_comment with more than two slash +///line_comment with more than two slash +//// line_comment with more than two slash +////line_comment with more than two slash + +// /*/*/ + +/*/ block_comment with slash near /* and */ +*/ + + +//* line_block_comment */ + +infix 4 ===_u +infix 4 ===/_u +infix 4 /=/=/= + +infix 4 ===*_u +val operator ===/_u : forall 'n. (int('n), int('n)) -> bool +function operator ===/_u(x, y) = x == y + +infix 4 =/ +val operator =/ : forall 'n. (int('n), int('n)) -> bool +function operator =/(x, y) = x == y + +infix 4 = // comment +infix 4 =/ // comment +infix 4 ==/ +infix 4 -/- //comment +infix 4 -/-/ //comment +infix 4 /-*//comment + +infixl 4 = // comment +infixl 4 =/ // comment +infixl 4 ==/ +infixl 4 -/- //comment +infixl 4 -/-/ //comment +infixl 4 /-*//comment + +infixr 4 = // comment +infixr 4 =/ // comment +infixr 4 ==/ +infixr 4 -/- //comment +infixr 4 -/-/ //comment +infixr 4 /-*//comment + +function f () = { + if op_eq2_with_block_comment /**/== /**/ 1 then { 1 }; + + if op_eq_slash =/1 then { 1 }; + if op_eq_slash_with_block_comment =/1/**/ then { 1 }; + + let op_eq_with_line_comment = // + 1; + + let op_eq_with_line_comment = /// + 1; + + if op_eq_with_line_comment = // comment + (if eq_slash = /**/1 then { 1 } else {2}) then {1}; + + if eq_with_blcok_comment = /**/1 then { 1 }; + + + if eq3_slash ===/_u 1 then { 1 }; + + 0 +} From be519cfa98db5f8831e329f96275e94774bca238 Mon Sep 17 00:00:00 2001 From: trdthg Date: Wed, 24 Jul 2024 09:37:47 +0000 Subject: [PATCH 2/2] test --- src/lib/lexer.mll | 7 ++----- test/format/default/operator.expect | 17 ++++++++--------- test/format/operator.sail | 13 ++++++------- 3 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index 816109ae2..6e007fb55 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -171,13 +171,10 @@ let tyvar_start = '\'' (* Ensure an operator cannot start with comment openings *) let oper_char = ['!''%''&''*''+''-''.''/'':''<''=''>''@''^''|'] let oper_char_no_slash = ['!''%''&''*''+''-''.'':''<''=''>''@''^''|'] +let oper_char_no_star = ['!''%''&''+''-''.''/'':''<''=''>''@''^''|'] let oper_char_no_slash_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 operator = ((oper_char_no_slash_star* ['/']? oper_char_no_slash_star*) | oper_char_no_slash*) ('_' ident)? let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit) let lchar = [^'\n'] diff --git a/test/format/default/operator.expect b/test/format/default/operator.expect index 43ae2e990..ae87f009a 100644 --- a/test/format/default/operator.expect +++ b/test/format/default/operator.expect @@ -13,7 +13,6 @@ $include //* line_block_comment */ infix 4 ===_u infix 4 ===/_u -infix 4 /=/=/= infix 4 ===*_u val operator ===/_u : forall 'n. (int('n), int('n)) -> bool @@ -25,6 +24,9 @@ function operator =/(x, y) = x == y infix 4 = +// comment +infix 4 + // comment infix 4 =/ @@ -33,10 +35,7 @@ infix 4 ==/ infix 4 -/- //comment -infix 4 -/-/ - -//comment -infix 4 /-* +infix 4 /-- //comment infixl 4 = @@ -49,10 +48,10 @@ infixl 4 ==/ infixl 4 -/- //comment -infixl 4 -/-/ +infixl 4 -/- //comment -infixl 4 /-* +infixl 4 /-- //comment infixr 4 = @@ -65,10 +64,10 @@ infixr 4 ==/ infixr 4 -/- //comment -infixr 4 -/-/ +infixr 4 -/- //comment -infixr 4 /-* +infixr 4 /-- //comment function f () = { diff --git a/test/format/operator.sail b/test/format/operator.sail index 5b286841a..e8b527aa7 100644 --- a/test/format/operator.sail +++ b/test/format/operator.sail @@ -18,7 +18,6 @@ $include infix 4 ===_u infix 4 ===/_u -infix 4 /=/=/= infix 4 ===*_u val operator ===/_u : forall 'n. (int('n), int('n)) -> bool @@ -29,25 +28,25 @@ val operator =/ : forall 'n. (int('n), int('n)) -> bool function operator =/(x, y) = x == y infix 4 = // comment +infix 4 // comment infix 4 =/ // comment infix 4 ==/ infix 4 -/- //comment -infix 4 -/-/ //comment -infix 4 /-*//comment +infix 4 /-- //comment infixl 4 = // comment infixl 4 =/ // comment infixl 4 ==/ infixl 4 -/- //comment -infixl 4 -/-/ //comment -infixl 4 /-*//comment +infixl 4 -/- //comment +infixl 4 /-- //comment infixr 4 = // comment infixr 4 =/ // comment infixr 4 ==/ infixr 4 -/- //comment -infixr 4 -/-/ //comment -infixr 4 /-*//comment +infixr 4 -/- //comment +infixr 4 /-- //comment function f () = { if op_eq2_with_block_comment /**/== /**/ 1 then { 1 };