From 567c6f28463a0bdeac58ff8cc732f33685e7c664 Mon Sep 17 00:00:00 2001 From: trdthg Date: Tue, 23 Jul 2024 06:36:45 +0000 Subject: [PATCH] remote rules --- 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..82365d5da 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 +}