[ refactor ] Add parser primitive for basic username

Author: spcfox

src/Idris/Parser.idr

@@ -76,7 +76,7 @@ decoratedDataConstructorName : OriginDesc -> Rule Name
 decoratedDataConstructorName fname = decorate fname Data dataConstructorName
 
 decoratedSimpleBinderUName : OriginDesc -> Rule Name
-decoratedSimpleBinderUName fname = decorate fname Bound (UN . Basic <$> unqualifiedName)
+decoratedSimpleBinderUName fname = decorate fname Bound userName
 
 decoratedSimpleNamedArg : OriginDesc -> Rule String
 decoratedSimpleNamedArg fname
@@ -1627,10 +1627,7 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
            commit
            decoratedSymbol fname "("
            us <- sepBy (decoratedSymbol fname ",")
-                       (do n <- optional $ do
-                                      x <- unqualifiedName
-                                      decoratedSymbol fname ":"
-                                      pure (UN $ Basic x)
+                       (do n <- optional $ userName <* decoratedSymbol fname ":"
                            ty <- typeExpr pdef fname indents
                            pure (n, ty))
            decoratedSymbol fname ")"

src/Parser/Rule/Source.idr

@@ -347,6 +347,10 @@ export
 unqualifiedName : Rule String
 unqualifiedName = identPart
 
+export
+userName : Rule Name
+userName = UN . Basic <$> unqualifiedName
+
 export
 holeName : Rule String
 holeName

src/TTImp/Parser.idr

@@ -59,7 +59,7 @@ atom fname
          pure (IVar (MkFC fname start end) x)
   <|> do start <- location
          symbol "$"
-         x <- UN . Basic <$> unqualifiedName
+         x <- userName
          end <- location
          pure (IBindVar (MkFC fname start end) x)
   <|> do start <- location
@@ -185,7 +185,7 @@ mutual
   implicitArg fname indents
       = do start <- location
            symbol "{"
-           x <- UN . Basic <$> unqualifiedName
+           x <- userName
            (do symbol "="
                commit
                tm <- expr fname indents
@@ -203,7 +203,7 @@ mutual
   as : OriginDesc -> IndentInfo -> Rule RawImp
   as fname indents
       = do start <- location
-           x <- UN . Basic <$> unqualifiedName
+           x <- userName
            nameEnd <- location
            symbol "@"
            pat <- simpleExpr fname indents
@@ -245,26 +245,26 @@ mutual
   bindList fname start indents
       = forget <$> sepBy1 (symbol ",")
                           (do rigc <- multiplicity
-                              n <- unqualifiedName
+                              n <- userName
                               end <- location
                               ty <- option
                                        (Implicit (MkFC fname start end) False)
                                        (do symbol ":"
                                            appExpr fname indents)
                               rig <- getMult rigc
-                              pure (rig, UN (Basic n), ty))
+                              pure (rig, n, ty))
 
 
   pibindListName : OriginDesc -> FilePos -> IndentInfo ->
                    Rule (List (RigCount, Name, RawImp))
   pibindListName fname start indents
        = do rigc <- multiplicity
-            ns <- sepBy1 (symbol ",") unqualifiedName
+            ns <- sepBy1 (symbol ",") userName
             symbol ":"
             ty <- expr fname indents
             atEnd indents
             rig <- getMult rigc
-            pure (map (\n => (rig, UN (Basic n), ty)) (forget ns))
+            pure (map (\n => (rig, n, ty)) (forget ns))
      <|> forget <$> sepBy1 (symbol ",")
                            (do rigc <- multiplicity
                                n <- name
@@ -299,11 +299,11 @@ mutual
            keyword "forall"
            commit
            nstart <- location
-           ns <- sepBy1 (symbol ",") unqualifiedName
+           ns <- sepBy1 (symbol ",") userName
            nend <- location
            let nfc = MkFC fname nstart nend
            let binders = map (\n => ( erased {a=RigCount}
-                                    , Just (UN $ Basic n)
+                                    , Just n
                                     , Implicit nfc False))
                              (forget ns)
            symbol "."
@@ -640,12 +640,12 @@ fieldDecl fname indents
     fieldBody : PiInfo RawImp -> Rule (List IField)
     fieldBody p
         = do start <- location
-             ns <- sepBy1 (symbol ",") unqualifiedName
+             ns <- sepBy1 (symbol ",") userName
              symbol ":"
              ty <- expr fname indents
              end <- location
              pure (map (\n => MkIField (MkFC fname start end)
-                                       linear p (UN $ Basic n) ty) (forget ns))
+                                       linear p n ty) (forget ns))
 
 recordDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
 recordDecl fname indents