add basic name sanitization

Author: flupe

src/Agda2Lambox/Compile/Function.hs

@@ -87,7 +87,7 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
       projTel <- telViewUpTo recPars defType
       projType <- theCore <$> telViewUpTo recPars defType
       let names  = map domName $ toList $ theTel projTel
-          pnames = map (maybe LBox.Anon (LBox.Named . prettyShow)) names
+          pnames = map (maybe LBox.Anon (LBox.Named . sanitize . prettyShow)) names
       (pnames,) <$> compileType recPars projType
 
     -- TODO(flupe): ^ take care of projection-like functions
@@ -108,7 +108,7 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
       forM mdefs \def@Defn{defName} -> do
         body <- compileFunctionBody mnames def
         return LBox.Def
-          { dName = LBox.Named $ prettyShow defName
+          { dName = qnameToName defName
           , dBody = body
           , dArgs = 0
           }

src/Agda2Lambox/Compile/Inductive.hs

@@ -125,7 +125,7 @@ actuallyConvertInductive t defn = do
       isParamArity   <- liftTCM $ isArity domType
       let isParamSort = isJust  $ isSort $ unEl $ domType
       pure LBox.TypeVarInfo
-        { tvarName      = maybe LBox.Anon (LBox.Named . prettyShow) $ domName pdom
+        { tvarName      = maybe LBox.Anon (LBox.Named . sanitize . prettyShow) $ domName pdom
         , tvarIsLogical = isParamLogical
         , tvarIsArity   = isParamArity
         , tvarIsSort    = isParamSort
@@ -143,13 +143,13 @@ actuallyConvertInductive t defn = do
           compileArgs indPars conTel
 
         pure LBox.Constructor
-          { cstrName  = prettyShow $ qnameName cname
+          { cstrName  = sanitize $ prettyShow $ qnameName cname
           , cstrArgs  = arity
           , cstrTypes = conTypeInfo
           }
 
     pure LBox.OneInductive
-      { indName          = prettyShow $ qnameName indName
+      { indName          = sanitize $ prettyShow $ qnameName indName
       , indPropositional = False        -- TODO(flupe)
       , indKElim         = LBox.IntoAny -- TODO(flupe)
       , indCtors         = ctors

src/Agda2Lambox/Compile/Utils.hs

@@ -2,10 +2,12 @@
 module Agda2Lambox.Compile.Utils
   ( modNameToModPath
   , qnameToKName
+  , qnameToName
   , dataOrRecDefMutuals
   , dataOrRecMutuals
   , toInductive
   , toConApp
+  , sanitize
   , MayBeLogical(isLogical)
   ) where
 
@@ -27,6 +29,7 @@ import LambdaBox qualified as LBox
 import Agda.TypeChecking.Substitute (TelV(TelV))
 import Agda.TypeChecking.Telescope (telView)
 import Agda.Utils.Monad (orM)
+import Data.Char (isLower, isUpper, GeneralCategory (DecimalNumber), generalCategory)
 
 
 -- | Convert and Agda module name to its "equivalent" λ□ module path.
@@ -39,7 +42,10 @@ qnameToKName :: QName -> LBox.KerName
 qnameToKName qn =
   LBox.KerName
     (modNameToModPath $ qnameModule qn)
-    (prettyShow $ qnameName qn)
+    (sanitize $ prettyShow $ qnameName qn)
+
+qnameToName :: QName -> LBox.Name
+qnameToName q = LBox.Named (sanitize $ prettyShow $ qnameName q)
 
 dataOrRecDefMutuals :: Definition -> TCM [QName]
 dataOrRecDefMutuals d = do
@@ -106,6 +112,21 @@ instance MayBeLogical Type where
         LevelUniv{} -> True -- LevelUniv
         _           -> False
 
+
+-- | Sanitize an agda name to something without unicode.
+-- Must be injective.
+-- We may require a smarter transformation later on for other targets.
+sanitize :: String -> String
+sanitize s = concatMap encode s
+  where
+  encode '$' = "$$"
+  encode c
+    | isLower c || isUpper c || c == '_' ||
+      generalCategory c == DecimalNumber =
+      [c]
+    | otherwise = "$" ++ show (fromEnum c)
+
+
 -- | Additionally, we consider erased domains logical.
 instance MayBeLogical a => MayBeLogical (Dom a) where
   isLogical dom | not (usableModality dom) = pure True