Add unicode operator support

src/Core/Name.idr

@@ -56,7 +56,7 @@ showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
 ||| Check whether a given character is a valid identifier character
 export
 identChar : Char -> Bool
-identChar x = isAlphaNum x || x == '_' || x == '\''
+identChar x = isAlphaNum x || x == '_' || x == '\'' ||  x > chr 127
 
 export Show Name where
   show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n

src/Idris/Desugar.idr

@@ -72,11 +72,10 @@ toTokList (POp fc opn l r)
          let op = nameRoot opn
          case lookup op (infixes syn) of
               Nothing =>
-                let ops = unpack opChars in
-                    if any (\x => x `elem` ops) (unpack op)
-                       then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
-                       else do rtoks <- toTokList r
-                               pure (Expr l :: Op fc opn backtickPrec :: rtoks)
+                  if any isOpChar (unpack op)
+                     then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
+                     else do rtoks <- toTokList r
+                             pure (Expr l :: Op fc opn backtickPrec :: rtoks)
               Just (Prefix, _) =>
                       throw (GenericMsg fc $ "'" ++ op ++ "' is a prefix operator")
               Just (fix, prec) =>

src/Idris/IDEMode/MakeClause.idr

@@ -9,7 +9,7 @@ import Parser.Unlit
 showRHSName : Name -> String
 showRHSName n
     = let fn = show (dropNS n) in
-          if any (flip elem (unpack opChars)) (unpack fn)
+          if any isOpChar (unpack fn)
              then "op"
              else fn
 

src/Idris/IDEMode/Parser.idr

@@ -21,13 +21,13 @@ ident = pred startIdent <+> many (pred validIdent)
   where
     startIdent : Char -> Bool
     startIdent '_' = True
-    startIdent x = isAlpha x
+    startIdent x = isAlpha x || x > chr 127
 
     validIdent : Char -> Bool
     validIdent '_' = True
     validIdent '-' = True
     validIdent '\'' = True
-    validIdent x = isAlphaNum x
+    validIdent x = isAlphaNum x || x > chr 127
 
 ideTokens : TokenMap Token
 ideTokens =

src/Idris/Parser.idr

@@ -39,6 +39,15 @@ export
 plhs : ParseOpts
 plhs = MkParseOpts False False
 
+leftArrow : Rule ()
+leftArrow = symbol "<-" <|> symbol "←"
+
+rightArrow : Rule ()
+rightArrow = symbol "->" <|> symbol "→"
+
+doubleRightArrow : Rule ()
+doubleRightArrow = symbol "=>" <|> symbol "⇒"
+
 atom : FileName -> Rule PTerm
 atom fname
     = do start <- location
@@ -418,12 +427,11 @@ mutual
 
   bindSymbol : Rule (PiInfo PTerm)
   bindSymbol
-      = do symbol "->"
+      = do rightArrow
            pure Explicit
-    <|> do symbol "=>"
+    <|> do doubleRightArrow
            pure AutoImplicit
 
-
   explicitPi : FileName -> IndentInfo -> Rule PTerm
   explicitPi fname indents
       = do start <- location
@@ -443,7 +451,7 @@ mutual
            commit
            binders <- pibindList fname start indents
            symbol "}"
-           symbol "->"
+           rightArrow
            scope <- typeExpr pdef fname indents
            end <- location
            pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
@@ -457,7 +465,7 @@ mutual
            t <- simpleExpr fname indents
            binders <- pibindList fname start indents
            symbol "}"
-           symbol "->"
+           rightArrow
            scope <- typeExpr pdef fname indents
            end <- location
            pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope)
@@ -483,7 +491,7 @@ mutual
            symbol "{"
            binders <- pibindList fname start indents
            symbol "}"
-           symbol "->"
+           rightArrow
            scope <- typeExpr pdef fname indents
            end <- location
            pure (pibindAll (MkFC fname start end) Implicit binders scope)
@@ -493,7 +501,7 @@ mutual
       = do start <- location
            symbol "\\"
            binders <- bindList fname start indents
-           symbol "=>"
+           doubleRightArrow
            mustContinue indents Nothing
            scope <- expr pdef fname indents
            end <- location
@@ -596,7 +604,7 @@ mutual
 
   caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PClause
   caseRHS fname start indents lhs
-      = do symbol "=>"
+      = do doubleRightArrow
            mustContinue indents Nothing
            rhs <- expr pdef fname indents
            atEnd indents
@@ -633,7 +641,7 @@ mutual
 
   field : FileName -> IndentInfo -> Rule PFieldUpdate
   field fname indents
-      = do path <- sepBy1 (symbol "->") unqualifiedName
+      = do path <- sepBy1 rightArrow unqualifiedName
            upd <- (do symbol "="; pure PSetField)
                       <|>
                   (do symbol "$="; pure PSetFieldApp)
@@ -675,7 +683,7 @@ mutual
            -- If the name doesn't begin with a lower case letter, we should
            -- treat this as a pattern, so fail
            validPatternVar n
-           symbol "<-"
+           leftArrow
            val <- expr pdef fname indents
            atEnd indents
            end <- location
@@ -701,7 +709,7 @@ mutual
            (do atEnd indents
                end <- location
                pure [DoExp (MkFC fname start end) e])
-             <|> (do symbol "<-"
+             <|> (do leftArrow
                      val <- expr pnowith fname indents
                      alts <- block (patAlt fname)
                      atEnd indents
@@ -1151,15 +1159,15 @@ getRight (Right v) = Just v
 constraints : FileName -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
 constraints fname indents
     = do tm <- appExpr pdef fname indents
-         symbol "=>"
+         doubleRightArrow
          more <- constraints fname indents
          pure ((Nothing, tm) :: more)
   <|> do symbol "("
          n <- name
          symbol ":"
          tm <- expr pdef fname indents
          symbol ")"
-         symbol "=>"
+         doubleRightArrow
          more <- constraints fname indents
          pure ((Just n, tm) :: more)
   <|> pure []
@@ -1173,7 +1181,7 @@ implBinds fname indents
          symbol ":"
          tm <- expr pdef fname indents
          symbol "}"
-         symbol "->"
+         rightArrow
          more <- implBinds fname indents
          pure ((n, rig, tm) :: more)
   <|> pure []

src/Parser/Lexer.idr

@@ -122,22 +122,39 @@ symbols
        "`(", "`"]
 
 export
-opChars : String
-opChars = ":!#$%&*+./<=>?@\\^|-~"
+isOpChar : Char -> Bool
+isOpChar c = inLatin || inArrows || inMathematicalOperators
+  where
+    inRange : (Int, Int) -> Lazy Bool
+    inRange (lowerBound, upperBound) = (c >= chr lowerBound && c <= chr upperBound)
+    inLatin = (c `elem` ['!', ':', '\\', '^', '|', '~']) ||
+      (or $ inRange <$>
+        [ (35, 38) -- #$%&
+        , (42, 43) -- *+
+        , (45, 47) -- -./
+        , (60, 64) -- <=>?@
+        ])
+    inArrows = or $ inRange <$>
+      [ ( 8592,  8703) -- Arrows
+      , (10224, 10239) -- Supplemental Arrows-A
+      , (10496, 10623) -- Supplemental Arrows-B
+      ]
+    inMathematicalOperators = or $ inRange <$>
+      [ ( 8704,  8959) -- Mathematical Operators
+      , (10752, 11007) -- Supplemental Mathematical Operators
+      ]
+
 
 validSymbol : Lexer
-validSymbol = some (oneOf opChars)
+validSymbol = some (pred isOpChar)
 
 -- Valid symbols which have a special meaning so can't be operators
 export
 reservedSymbols : List String
 reservedSymbols
     = symbols ++
-      ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
-       "&", "**", ".."]
-
-symbolChar : Char -> Bool
-symbolChar c = c `elem` unpack opChars
+      ["%", "\\", ":", "=", "|", "|||", "?", "!", "&", "**",
+       "..", "<-", "->", "=>", "←", "→", "⇒"]
 
 fromHexLit : String -> Integer
 fromHexLit str
@@ -161,9 +178,9 @@ rawTokens =
      (digits, \x => Literal (cast x)),
      (stringLit, \x => StrLit (stripQuotes x)),
      (charLit, \x => CharLit (stripQuotes x)),
-     (ident, \x => if x `elem` keywords then Keyword x else Ident x),
      (space, Comment),
      (validSymbol, Symbol),
+     (ident, \x => if x `elem` keywords then Keyword x else Ident x),
      (symbol, Unrecognised)]
   where
     stripQuotes : String -> String

tests/Main.idr

@@ -51,6 +51,8 @@ idrisTests
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",
        "literate009",
+       -- Unicode
+       "unicode001",
        -- Interfaces
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",

tests/idris2/unicode001/Unicode.idr

@@ -0,0 +1,9 @@
+module Unicode
+
+infix 6 ≡, ≢
+
+public export
+interface UnicodeEq a where
+    (≡) : a → a → Bool
+    (≢) : a → a → Bool
+

tests/idris2/unicode001/expected

@@ -0,0 +1 @@
+1/1: Building Unicode (Unicode.idr)

tests/idris2/unicode001/run

@@ -0,0 +1,3 @@
+$1 -c Unicode.idr
+
+rm -rf build/