diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index 954abb364..6e007fb55 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -171,11 +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 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 = ((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'] @@ -188,7 +187,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..ae87f009a --- /dev/null +++ b/test/format/default/operator.expect @@ -0,0 +1,96 @@ +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 ===*_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 =/ + +// comment +infix 4 ==/ +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..e8b527aa7 --- /dev/null +++ b/test/format/operator.sail @@ -0,0 +1,72 @@ +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 ===*_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 =/ // comment +infix 4 ==/ +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 +}