Refactor ident to reuse in IDEMode, fixes out of sync bug.

Related: 1a4f424 on 2019-September-28

Author: fabianhjr

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

@@ -1,3 +1,6 @@
+||| Slightly different lexer than the source language because we are more free
+||| as to what can be identifiers, and fewer tokens are supported. But otherwise,
+||| we can reuse the standard stuff
 module Idris.IDEMode.Parser
 
 import Idris.IDEMode.Commands
@@ -7,34 +10,17 @@ import Parser.Lexer
 import Parser.Support
 import Text.Lexer
 
--- Slightly different lexer than the source language because we are more free
--- as to what can be identifiers, and fewer tokens are supported. But otherwise,
--- we can reuse the standard stuff
-
 %hide Lexer.symbols
 
 symbols : List String
 symbols = ["(", ":", ")"]
 
-ident : Lexer
-ident = pred startIdent <+> many (pred validIdent)
-  where
-    startIdent : Char -> Bool
-    startIdent '_' = True
-    startIdent x = isAlpha x
-
-    validIdent : Char -> Bool
-    validIdent '_' = True
-    validIdent '-' = True
-    validIdent '\'' = True
-    validIdent x = isAlphaNum x
-
 ideTokens : TokenMap Token
 ideTokens =
     map (\x => (exact x, Symbol)) symbols ++
     [(digits, \x => Literal (cast x)),
      (stringLit, \x => StrLit (stripQuotes x)),
-     (ident, Ident),
+     (identRelaxed, Ident),
      (space, Comment)]
   where
     stripQuotes : String -> String

src/Idris/IDEMode/TokenLine.idr

@@ -1,7 +1,7 @@
+||| Tokenise a source line for easier processing
 module Idris.IDEMode.TokenLine
 
--- Tokenise a source line for easier processing
-
+import Parser.Lexer
 import Text.Lexer
 
 public export
@@ -14,24 +14,12 @@ data SourcePart
   | Equal
   | Other String
 
-ident : Lexer
-ident = pred startIdent <+> many (pred validIdent)
-  where
-    startIdent : Char -> Bool
-    startIdent '_' = True
-    startIdent x = isAlpha x
-
-    validIdent : Char -> Bool
-    validIdent '_' = True
-    validIdent '\'' = True
-    validIdent x = isAlphaNum x
-
 holeIdent : Lexer
-holeIdent = is '?' <+> ident
+holeIdent = is '?' <+> identRelaxed
 
 srcTokens : TokenMap SourcePart
 srcTokens =
-    [(ident, Name),
+    [(identRelaxed, Name),
      (holeIdent, \x => HoleName (assert_total (strTail x))),
      (space, Whitespace),
      (is '{', const LBrace),
@@ -47,4 +35,3 @@ tokens str
            -- number to read when storing spans in the file
            (srctoks, (l, c, rest)) =>
               map tok srctoks ++ (if rest == "" then [] else [Other rest])
-

src/Parser/Lexer.idr

@@ -61,20 +61,39 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1
 docComment : Lexer
 docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')
 
-ident : Lexer
-ident = pred startIdent <+> many (pred validIdent)
-  where
-    startIdent : Char -> Bool
-    startIdent '_' = True
-    startIdent x = isAlpha x || x > chr 127
+-- Identifier Lexer
+--
+-- There are two variants, a strict ident and a relaxed ident.
+-- Prime definitions recieve a boolean determining if it is relaxed.
+
+startIdent : Char -> Bool
+startIdent '_' = True
+startIdent  x  = isAlpha x || x > chr 127
+
+%inline
+validIdent' : Bool -> Char -> Bool
+validIdent' _ '_'  = True
+validIdent' r '-'  = r
+validIdent' _ '\'' = True
+validIdent' _  x   = isAlphaNum x || x > chr 127
+
+%inline
+ident' : Bool -> Lexer
+ident' relaxed =
+  (pred $ startIdent) <+>
+    (many . pred $ validIdent' relaxed)
+
+-- This are the two identifier lexer specializations
 
-    validIdent : Char -> Bool
-    validIdent '_' = True
-    validIdent '\'' = True
-    validIdent x = isAlphaNum x || x > chr 127
+identStrict : Lexer
+identStrict = ident' False
+
+export
+identRelaxed : Lexer
+identRelaxed = ident' True
 
 holeIdent : Lexer
-holeIdent = is '?' <+> ident
+holeIdent = is '?' <+> identStrict
 
 doubleLit : Lexer
 doubleLit
@@ -121,12 +140,13 @@ symbols
        "(", ")", "{", "}", "[", "]", ",", ";", "_",
        "`(", "`"]
 
+
 export
-opChars : String
-opChars = ":!#$%&*+./<=>?@\\^|-~"
+isOpChar : Char -> Bool
+isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
 
 validSymbol : Lexer
-validSymbol = some (oneOf opChars)
+validSymbol = some (pred isOpChar)
 
 -- Valid symbols which have a special meaning so can't be operators
 export
@@ -136,9 +156,6 @@ reservedSymbols
       ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
        "&", "**", ".."]
 
-symbolChar : Char -> Bool
-symbolChar c = c `elem` unpack opChars
-
 fromHexLit : String -> Integer
 fromHexLit str
   = if length str <= 2
@@ -161,7 +178,7 @@ 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),
+     (identStrict, \x => if x `elem` keywords then Keyword x else Ident x),
      (space, Comment),
      (validSymbol, Symbol),
      (symbol, Unrecognised)]