[ refactor ] introduce UserName for (UN/RF) (#1926)

Instead of having UN & RF (& Hole in the near future & maybe even
more later e.g. operator names) we have a single UN constructor
that takes a UserName instead of a String.

UserName is (for now)

```idris
data UserName : Type where
  Basic : String -> UserName -- default name constructor       e.g. map
  Field : String -> UserName -- field accessor                 e.g. .fst
  Underscore : UserName      -- no name                        e.g. _
```

This is extracted from the draft PR #1852 which is too big to easily
debug. Once this is working, I can go back to it.

Author: gallais

idris2api.ipkg

@@ -147,6 +147,7 @@ modules =
     Libraries.Data.String.Iterator,
     Libraries.Data.StringMap,
     Libraries.Data.StringTrie,
+    Libraries.Data.UserNameMap,
     Libraries.Data.Version,
 
     Libraries.System.Directory.Tree,

libs/base/Language/Reflection/TT.idr

@@ -97,22 +97,32 @@ data Constant
     | WorldType
 
 public export
-data Name = UN String -- user defined name
+data UserName
+  = Basic String -- default name constructor       e.g. map
+  | Field String -- field accessor                 e.g. .fst
+  | Underscore   -- no name                        e.g. _
+
+public export
+data Name = NS Namespace Name -- name in a namespace
+          | UN UserName -- user defined name
           | MN String Int -- machine generated name
-          | NS Namespace Name -- name in a namespace
           | DN String Name -- a name and how to display it
-          | RF String -- record field name
           | Nested (Int, Int) Name -- nested function name
           | CaseBlock String Int -- case block nested in (resolved) name
           | WithBlock String Int -- with block nested in (resolved) name
 
+export
+Show UserName where
+  show (Basic n) = n
+  show (Field n) = "." ++ n
+  show Underscore = "_"
+
 export
 Show Name where
   show (NS ns n) = show ns ++ "." ++ show n
-  show (UN x) = x
+  show (UN x) = show x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (DN str y) = str
-  show (RF n) = "." ++ n
   show (Nested (outer, idx) inner)
       = show outer ++ ":" ++ show idx ++ ":" ++ show inner
   show (CaseBlock outer i) = "case block in " ++ show outer

src/Compiler/Common.idr

@@ -199,10 +199,10 @@ replaceEntry (i, Just (ns, b))
 
 natHackNames : List Name
 natHackNames
-    = [UN "prim__add_Integer",
-       UN "prim__sub_Integer",
-       UN "prim__mul_Integer",
-       NS typesNS (UN "prim__integerToNat")]
+    = [UN (Basic "prim__add_Integer"),
+       UN (Basic "prim__sub_Integer"),
+       UN (Basic "prim__mul_Integer"),
+       NS typesNS (UN $ Basic "prim__integerToNat")]
 
 -- Hmm, these dump functions are all very similar aren't they...
 dumpCases : String -> List (Name,FC,NamedDef) -> Core ()

src/Compiler/CompileExpr.idr

@@ -181,33 +181,33 @@ magic ms e = go ms e where
 %inline
 magic__integerToNat : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
 magic__integerToNat fc fc' [k]
-  = CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k]
+  = CApp fc (CRef fc' (NS typesNS (UN $ Basic "prim__integerToNat"))) [k]
 
 magic__natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
 magic__natMinus fc fc' [m,n]
   = magic__integerToNat fc fc'
-    [CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]]
+    [CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, n]]
 
 -- We don't reuse natMinus here because we assume that unsuc will only be called
 -- on S-headed numbers so we do not need the truncating integerToNat call!
 magic__natUnsuc : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
 magic__natUnsuc fc fc' [m]
-  = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, CPrimVal fc (BI 1)]
+  = CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, CPrimVal fc (BI 1)]
 
 -- TODO: next release remove this and use %builtin pragma
 natHack : List Magic
 natHack =
-    [ MagicCRef (NS typesNS (UN "natToInteger")) 1 (\ _, _, [k] => k)
-    , MagicCRef (NS typesNS (UN "integerToNat")) 1 magic__integerToNat
-    , MagicCRef (NS typesNS (UN "plus")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
-    , MagicCRef (NS typesNS (UN "mult")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
-    , MagicCRef (NS typesNS (UN "minus")) 2 magic__natMinus
-    , MagicCRef (NS typesNS (UN "equalNat")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__eq_Integer")) [m, n])
-    , MagicCRef (NS typesNS (UN "compareNat")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN "compareInteger"))) [m, n])
+    [ MagicCRef (NS typesNS (UN $ Basic "natToInteger")) 1 (\ _, _, [k] => k)
+    , MagicCRef (NS typesNS (UN $ Basic "integerToNat")) 1 magic__integerToNat
+    , MagicCRef (NS typesNS (UN $ Basic "plus")) 2
+         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__add_Integer")) [m, n])
+    , MagicCRef (NS typesNS (UN $ Basic "mult")) 2
+         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__mul_Integer")) [m, n])
+    , MagicCRef (NS typesNS (UN $ Basic "minus")) 2 magic__natMinus
+    , MagicCRef (NS typesNS (UN $ Basic "equalNat")) 2
+         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__eq_Integer")) [m, n])
+    , MagicCRef (NS typesNS (UN $ Basic "compareNat")) 2
+         (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN $ Basic "compareInteger"))) [m, n])
     ]
 
 -- get all transformation from %builtin pragmas
@@ -321,8 +321,9 @@ mutual
                           (CLet fc x True !(toCExp m n val) sc')
                           rig
   toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
-      = pure $ CCon fc (UN "->") TYCON Nothing [!(toCExp m n ty),
-                                    CLam fc x !(toCExp m n sc)]
+      = pure $ CCon fc (UN (Basic "->")) TYCON Nothing
+                       [ !(toCExp m n ty)
+                       , CLam fc x !(toCExp m n sc)]
   toCExpTm m n (Bind fc x b tm) = pure $ CErased fc
   -- We'd expect this to have been dealt with in toCExp, but for completeness...
   toCExpTm m n (App fc tm arg)
@@ -339,9 +340,9 @@ mutual
       = let t = constTag c in
             if t == 0
                then pure $ CPrimVal fc c
-               else pure $ CCon fc (UN (show c)) TYCON Nothing []
+               else pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing []
   toCExpTm m n (Erased fc _) = pure $ CErased fc
-  toCExpTm m n (TType fc) = pure $ CCon fc (UN "Type") TYCON Nothing []
+  toCExpTm m n (TType fc) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing []
 
   toCExp : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
@@ -576,15 +577,15 @@ getFieldArgs defs cl
 
 getNArgs : {auto c : Ref Ctxt Defs} ->
            Defs -> Name -> List (Closure []) -> Core NArgs
-getNArgs defs (NS _ (UN "IORes")) [arg] = pure $ NIORes arg
-getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr
-getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr
-getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr
-getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr
-getNArgs defs (NS _ (UN "Buffer")) [] = pure NBuffer
-getNArgs defs (NS _ (UN "ForeignObj")) [] = pure NForeignObj
-getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit
-getNArgs defs (NS _ (UN "Struct")) [n, args]
+getNArgs defs (NS _ (UN $ Basic "IORes")) [arg] = pure $ NIORes arg
+getNArgs defs (NS _ (UN $ Basic "Ptr")) [arg] = pure NPtr
+getNArgs defs (NS _ (UN $ Basic "AnyPtr")) [] = pure NPtr
+getNArgs defs (NS _ (UN $ Basic "GCPtr")) [arg] = pure NGCPtr
+getNArgs defs (NS _ (UN $ Basic "GCAnyPtr")) [] = pure NGCPtr
+getNArgs defs (NS _ (UN $ Basic "Buffer")) [] = pure NBuffer
+getNArgs defs (NS _ (UN $ Basic "ForeignObj")) [] = pure NForeignObj
+getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit
+getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]
     = do NPrimVal _ (Str n') <- evalClosure defs n
              | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct")
          pure (Struct n' !(getFieldArgs defs args))
@@ -641,9 +642,9 @@ nfToCFType _ s (NTCon fc n_in _ _ args)
                    carg <- nfToCFType fc s narg
                    pure (CFIORes carg)
 nfToCFType _ s (NType _)
-    = pure (CFUser (UN "Type") [])
+    = pure (CFUser (UN (Basic "Type")) [])
 nfToCFType _ s (NErased _ _)
-    = pure (CFUser (UN "__") [])
+    = pure (CFUser (UN (Basic "__")) [])
 nfToCFType fc s t
     = do defs <- get Ctxt
          ty <- quote defs [] t
@@ -766,7 +767,7 @@ compileExp : {auto c : Ref Ctxt Defs} ->
 compileExp tm
     = do m <- builtinMagic
          s <- newRef NextSucc 0
-         exp <- toCExp m (UN "main") tm
+         exp <- toCExp m (UN $ Basic "main") tm
          pure exp
 
 ||| Given a name, look up an expression, and compile it to a CExp in the environment

src/Compiler/ES/Codegen.idr

@@ -83,13 +83,17 @@ keywordSafe s = s
 --          JS Name
 --------------------------------------------------------------------------------
 
+jsUserName : UserName -> String
+jsUserName (Basic n) = keywordSafe $ jsIdent n
+jsUserName (Field n) = "rf__" ++ jsIdent n
+jsUserName Underscore = keywordSafe $ jsIdent "_"
+
 jsName : Name -> String
 jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n
-jsName (UN n) = keywordSafe $ jsIdent n
+jsName (UN n) = jsUserName n
 jsName (MN n i) = jsIdent n ++ "_" ++ show i
 jsName (PV n d) = "pat__" ++ jsName n
 jsName (DN _ n) = jsName n
-jsName (RF n) = "rf__" ++ jsIdent n
 jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
 jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
 jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
@@ -515,32 +519,33 @@ foreignDecl n ccs = do
 
 -- implementations for external primitive functions.
 jsPrim : {auto c : Ref ESs ESSt} -> Name -> List Doc -> Core Doc
-jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ hcat ["({value:", v, "})"]
-jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ hcat ["(", r, ".value)"]
-jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ hcat ["(", r, ".value=", v, ")"]
-jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ hcat ["(Array(", s, ").fill(", v, "))"]
-jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ hcat ["(", x, "[", p, "])"]
-jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ hcat ["(", x, "[", p, "]=", v, ")"]
-jsPrim (NS _ (UN "void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
-jsPrim (NS _ (UN "prim__void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
-jsPrim (NS _ (UN "prim__codegen")) [] = do
+jsPrim nm docs = case (dropAllNS nm, docs) of
+  (UN (Basic "prim__newIORef"), [_,v,_]) => pure $ hcat ["({value:", v, "})"]
+  (UN (Basic "prim__readIORef"), [_,r,_]) => pure $ hcat ["(", r, ".value)"]
+  (UN (Basic "prim__writeIORef"), [_,r,v,_]) => pure $ hcat ["(", r, ".value=", v, ")"]
+  (UN (Basic "prim__newArray"), [_,s,v,_]) => pure $ hcat ["(Array(", s, ").fill(", v, "))"]
+  (UN (Basic "prim__arrayGet"), [_,x,p,_]) => pure $ hcat ["(", x, "[", p, "])"]
+  (UN (Basic "prim__arraySet"), [_,x,p,v,_]) => pure $ hcat ["(", x, "[", p, "]=", v, ")"]
+  (UN (Basic "void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
+  (UN (Basic "prim__void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
+  (UN (Basic "prim__codegen"), []) => do
     (cg :: _) <- ccTypes <$> get ESs
         | _ => pure "\"javascript\""
     pure . Text $ jsString cg
 
 -- fix #1839: Only support `prim__os` in Node backend but not in browsers
-jsPrim (NS _ (UN "prim__os")) [] = do
-  tys <- ccTypes <$> get ESs
-  case searchForeign tys ["node"] of
-    Right _ => do
-      addToPreamble "prim__os" $
-        "const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++
-        "(require('os').platform()));"
-      pure $ Text $ esName "sysos"
-    Left  _ =>
-      throw $ InternalError $ "prim not implemented: prim__os"
-
-jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x)
+  (UN (Basic "prim__os"), []) => do
+    tys <- ccTypes <$> get ESs
+    case searchForeign tys ["node"] of
+      Right _ => do
+        addToPreamble "prim__os" $
+          "const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++
+          "(require('os').platform()));"
+        pure $ Text $ esName "sysos"
+      Left  _ =>
+        throw $ InternalError $ "prim not implemented: prim__os"
+
+  _ => throw $ InternalError $ "prim not implemented: " ++ show nm
 
 --------------------------------------------------------------------------------
 --          Codegen
@@ -696,7 +701,7 @@ foreign _                            = pure []
 -- name of the toplevel tail call loop from the
 -- preamble.
 tailRec : Name
-tailRec = UN "__tailRec"
+tailRec = UN $ Basic "__tailRec"
 
 ||| Compiles the given `ClosedTerm` for the list of supported
 ||| backends to JS code.

src/Compiler/Inline.idr

@@ -151,7 +151,7 @@ mutual
   -- whether they're safe to inline, but until then this gives such a huge
   -- boost by removing unnecessary lambdas that we'll keep the special case.
   eval rec env stk (CRef fc n)
-      = case (n == NS primIONS (UN "io_bind"), stk) of
+      = case (n == NS primIONS (UN $ Basic "io_bind"), stk) of
           (True, act :: cont :: world :: stk) =>
                  do xn <- genName "act"
                     sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])

src/Compiler/Interpreter/VMCode.idr

@@ -120,7 +120,7 @@ callPrim stk fn args = case the (Either Object (Vect ar Constant)) $ traverse ge
     getConst o = Left o
 
 NS_UN : Namespace -> String -> Name
-NS_UN ns un = NS ns (UN un)
+NS_UN ns un = NS ns (UN $ Basic un)
 
 argError : Ref State InterpState => Stack -> Vect h Object -> Core a
 argError stk obj = interpError stk $ "Unexpected arguments: " ++ foldMap ((" " ++) . showType) obj

src/Compiler/LambdaLift.idr

@@ -148,7 +148,7 @@ genName
   where
     mkName : Name -> Int -> Name
     mkName (NS ns b) i = NS ns (mkName b i)
-    mkName (UN n) i = MN n i
+    mkName (UN n) i = MN (displayUserName n) i
     mkName (DN _ n) i = mkName n i
     mkName (CaseBlock outer inner) i = MN ("case block in " ++ outer ++ " (" ++ show inner ++ ")") i
     mkName (WithBlock outer inner) i = MN ("with block in " ++ outer ++ " (" ++ show inner ++ ")") i

src/Compiler/RefC/RefC.idr

@@ -63,14 +63,19 @@ showcCleanString (c ::cs) = (showcCleanStringChar c) . showcCleanString cs
 cCleanString : String -> String
 cCleanString cs = showcCleanString (unpack cs) ""
 
+export
+cUserName : UserName -> String
+cUserName (Basic n) = cCleanString n
+cUserName (Field n) = "rec__" ++ cCleanString n
+cUserName Underscore = cCleanString "_"
+
 export
 cName : Name -> String
 cName (NS ns n) = cCleanString (showNSWithSep "_" ns) ++ "_" ++ cName n
-cName (UN n) = cCleanString n
+cName (UN n) = cUserName n
 cName (MN n i) = cCleanString n ++ "_" ++ cCleanString (show i)
 cName (PV n d) = "pat__" ++ cName n
 cName (DN _ n) = cName n
-cName (RF n) = "rec__" ++ cCleanString n
 cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
 cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
 cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
@@ -228,20 +233,20 @@ Show ExtPrim where
 ||| Match on a user given name to get the scheme primitive
 toPrim : Name -> ExtPrim
 toPrim pn@(NS _ n)
-    = cond [(n == UN "prim__newIORef", NewIORef),
-            (n == UN "prim__readIORef", ReadIORef),
-            (n == UN "prim__writeIORef", WriteIORef),
-            (n == UN "prim__newArray", NewArray),
-            (n == UN "prim__arrayGet", ArrayGet),
-            (n == UN "prim__arraySet", ArraySet),
-            (n == UN "prim__getField", GetField),
-            (n == UN "prim__setField", SetField),
-            (n == UN "void", VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
-            (n == UN "prim__void", VoidElim),
-            (n == UN "prim__os", SysOS),
-            (n == UN "prim__codegen", SysCodegen),
-            (n == UN "prim__onCollect", OnCollect),
-            (n == UN "prim__onCollectAny", OnCollectAny)
+    = cond [(n == UN (Basic "prim__newIORef"), NewIORef),
+            (n == UN (Basic "prim__readIORef"), ReadIORef),
+            (n == UN (Basic "prim__writeIORef"), WriteIORef),
+            (n == UN (Basic "prim__newArray"), NewArray),
+            (n == UN (Basic "prim__arrayGet"), ArrayGet),
+            (n == UN (Basic "prim__arraySet"), ArraySet),
+            (n == UN (Basic "prim__getField"), GetField),
+            (n == UN (Basic "prim__setField"), SetField),
+            (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
+            (n == UN (Basic "prim__void"), VoidElim),
+            (n == UN (Basic "prim__os"), SysOS),
+            (n == UN (Basic "prim__codegen"), SysCodegen),
+            (n == UN (Basic "prim__onCollect"), OnCollect),
+            (n == UN (Basic "prim__onCollectAny"), OnCollectAny)
             ]
            (Unknown pn)
 toPrim pn = assert_total $ idris_crash ("INTERNAL ERROR: Unknown primitive: " ++ cName pn)
@@ -909,8 +914,8 @@ createCFunctions n (MkAForeign ccs fargs ret) = do
                          else CLangC
           let isStandardFFI = Prelude.elem lang ["RefC", "C"]
           let fctName = if isStandardFFI
-                           then UN fctForeignName
-                           else UN $ lang ++ "_" ++ fctForeignName
+                           then UN $ Basic $ fctForeignName
+                           else UN $ Basic $ lang ++ "_" ++ fctForeignName
           if isStandardFFI
              then case extLibOpts of
                       [lib, header] => addHeader header

src/Compiler/Scheme/Chez.idr

@@ -128,7 +128,7 @@ chezString cs = strCons '"' (showChezString (unpack cs) "\"")
 
 mutual
   handleRet : String -> String -> String
-  handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN "") (Just 0) [])
+  handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN $ Basic "") (Just 0) [])
   handleRet _ op = mkWorld op
 
   getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))