sanitization test

Author: flupe

agda2lambox.cabal

@@ -49,7 +49,8 @@ executable agda2lambox
                        directory,
                        filepath,
                        text,
-                       mtl
+                       mtl,
+		       unicode-data
   default-language:    Haskell2010
   default-extensions:
     LambdaCase RecordWildCards PatternSynonyms TupleSections

HACKING.md notes/HACKING.mdHACKING.md renamed to notes/HACKING.md

@@ -116,8 +116,7 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
 
         -- otherwise, compiling it as an axiom
         _ -> do
-          reportSDoc "agda2lambox.compile" 5 $
-            "Compiling it to an axiom."
+          reportSDoc "agda2lambox.compile" 5 $ "Compiling it to an axiom."
           typ <- whenTyped target $ compileTopLevelType defType
           pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 

NOTES.md notes/NOTES.mdNOTES.md renamed to notes/NOTES.md

@@ -27,7 +27,7 @@ import Agda.Syntax.Common (Arg)
 import Agda.Syntax.Internal
 import Agda.Utils.Monad ( unlessM )
 
-import Agda.Utils ( isDataOrRecDef, isArity )
+import Agda.Utils
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
@@ -54,7 +54,7 @@ compileInductive t defn@Defn{defName} = do
   let items = fromMaybe (NEL.singleton defName) $ NEL.nonEmpty mutuals
 
   -- ensure that all mutuals get compiled, eventually
-  mapM requireDef items
+  mapM_ requireDef items
 
   {- also note that we assume the list of mutuals will be the same
      for every record/datatype in the list (especially the order),
@@ -123,9 +123,9 @@ actuallyConvertInductive t defn = do
       let domType = unDom pdom
       isParamLogical <- liftTCM $ isLogical pdom
       isParamArity   <- liftTCM $ isArity domType
-      let isParamSort = isJust  $ isSort $ unEl $ domType
+      let isParamSort = isJust  $ isSort $ unEl domType
       pure LBox.TypeVarInfo
-        { tvarName      = maybe LBox.Anon (LBox.Named . sanitize . prettyShow) $ domName pdom
+        { tvarName      = domToName pdom
         , tvarIsLogical = isParamLogical
         , tvarIsArity   = isParamArity
         , tvarIsSort    = isParamSort
@@ -138,18 +138,18 @@ actuallyConvertInductive t defn = do
           RecordCon _ _ arity _ -> arity
 
         conTypeInfo <- whenTyped t do
-          conType <- liftTCM $ (`piApplyM` pvars) =<< defType <$> getConstInfo cname
+          conType <- liftTCM $ (`piApplyM` pvars) . defType =<< getConstInfo cname
           conTel  <- toList . theTel <$> telView conType
           compileArgs indPars conTel
 
         pure LBox.Constructor
-          { cstrName  = sanitize $ prettyShow $ qnameName cname
+          { cstrName  = qnameToIdent cname
           , cstrArgs  = arity
           , cstrTypes = conTypeInfo
           }
 
     pure LBox.OneInductive
-      { indName          = sanitize $ prettyShow $ qnameName indName
+      { indName          = qnameToIdent indName
       , indPropositional = False        -- TODO(flupe)
       , indKElim         = LBox.IntoAny -- TODO(flupe)
       , indCtors         = ctors

src/Agda2Lambox/Compile.hs

@@ -18,11 +18,10 @@ import Data.Function ( applyWhen )
 import Agda.Syntax.Common ( unArg, Arg (Arg) )
 import Agda.Syntax.Internal
 import Agda.TypeChecking.Monad.Base ( TCM, MonadTCM (liftTCM), Definition(..))
-import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Utils.Monad (ifM)
 
 import qualified LambdaBox as LBox
-import Agda2Lambox.Compile.Utils ( qnameToKName, isLogical, toInductive )
+import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import Agda.Compiler.Backend (HasConstInfo(getConstInfo), Definition(Defn), AddContext (addContext))
 import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy)
@@ -91,7 +90,7 @@ compileArgs tvars = runC tvars . compileArgsC
   compileArgsC :: [Dom Type] -> C [(LBox.Name, LBox.Type)]
   compileArgsC [] = pure []
   compileArgsC (dom:args) = do
-    let name = maybe LBox.Anon (LBox.Named . prettyShow) $ domName dom
+    let name = domToName dom
     typ <- ifM (liftTCM $ isLogical dom) (pure LBox.TBox) (compileTypeC $ unDom dom)
     ((name, typ):) <$> underBinder dom (compileArgsC args)
 
@@ -172,7 +171,7 @@ compileTypeTerm = \case
 
     else do
       (vars, codomType') <- underTypeVar dom $ compileTopLevelTypeC codomType
-      let name = maybe LBox.Anon (LBox.Named . prettyShow) $ domName dom
+      let name = domToName dom
       pure (name : vars, LBox.TArr LBox.TBox codomType')
 
   _ -> pure ([], LBox.TAny)

src/Agda2Lambox/Compile/Inductive.hs

@@ -4,6 +4,8 @@ module Agda2Lambox.Compile.Utils
   ( modNameToModPath
   , qnameToKName
   , qnameToName
+  , qnameToIdent
+  , domToName
   , dataOrRecDefMutuals
   , dataOrRecMutuals
   , toInductive
@@ -18,6 +20,7 @@ import Data.Char
 import Data.List ( elemIndex, foldl' )
 import Data.Maybe ( fromMaybe, listToMaybe, isJust )
 
+import Unicode.Char.Identifiers
 import Agda.Compiler.Backend 
 import Agda.Syntax.Internal
 import Agda.Syntax.Abstract.Name
@@ -34,22 +37,26 @@ import Agda.Utils.Monad (orM)
 import Agda2Lambox.Compile.Monad
 import LambdaBox qualified as LBox
 
-
 -- | Convert and Agda module name to its "equivalent" λ□ module path.
 modNameToModPath :: ModuleName -> LBox.ModPath
 modNameToModPath =
   LBox.MPFile . map (sanitize . prettyShow) . mnameToList
 
-
 -- | Convert and Agda definition name to a λ□ kernel name.
 qnameToKName :: QName -> LBox.KerName
 qnameToKName qn =
   LBox.KerName
     (modNameToModPath $ qnameModule qn)
-    (sanitize $ prettyShow $ qnameName qn)
+    (qnameToIdent qn)
+
+domToName :: Dom' a b -> LBox.Name
+domToName = maybe LBox.Anon (LBox.Named . sanitize . prettyShow) . domName
+
+qnameToIdent :: QName -> LBox.Ident
+qnameToIdent = sanitize . prettyShow . qnameName
 
 qnameToName :: QName -> LBox.Name
-qnameToName q = LBox.Named (sanitize $ prettyShow $ qnameName q)
+qnameToName = LBox.Named . qnameToIdent
 
 dataOrRecDefMutuals :: Definition -> TCM [QName]
 dataOrRecDefMutuals d = do
@@ -135,7 +142,21 @@ instance MayBeLogical a => MayBeLogical (Arg a) where
 -- Must be injective.
 -- We may require a smarter transformation later on for other targets.
 sanitize :: String -> String
-sanitize s = concatMap encode s
+sanitize xs | xs `elem` ["true", "false"] = "r#" ++ xs
+sanitize [] = []
+sanitize (x:xs) = toXIDStart x <> concatMap toXIDContinue xs
+  where
+    toXIDStart, toXIDContinue :: Char -> String
+    toXIDStart c
+      | isXIDStart c || c == '_' = [c]
+      | isXIDContinue c          = "_" <> [c]
+      | otherwise                = toXIDContinue c
+
+    toXIDContinue c
+      | isXIDContinue c = [c]
+      | otherwise       = "y" <> show (ord c) <> "y"
+{-
+sanitize q = "agda" ++ concatMap encode q
   where
   encode '$' = "$$"
   encode c
@@ -144,5 +165,21 @@ sanitize s = concatMap encode s
     || isUpper c
     || c == '_'
     || generalCategory c == DecimalNumber = [c]
-    | otherwise = "$" ++ show (fromEnum c)
+    | otherwise = "$" ++ show (fromEnum c) ++ "$"
 
+-- | Sanitize an agda name to something Rust-compliant.
+-- Must be injective.
+sanitize :: String -> String
+sanitize [] = []
+sanitize (c:cs) = toXIDStart c <> concatMap toXIDContinue cs
+  where
+    toXIDStart, toXIDContinue :: Char -> String
+    toXIDStart c
+      | isXIDStart c || c == '_' = [c]
+      | isXIDContinue c          = "_" <> [c]
+      | otherwise                = toXIDContinue c
+
+    toXIDContinue c
+      | isXIDContinue c = [c]
+      | otherwise        = "Ֆ" <> show (ord c) <> "Ֆ"
+      -}

src/Agda2Lambox/Compile/Type.hs

@@ -40,7 +40,7 @@ data Name = Anon | Named Ident
 instance Pretty ModPath where
   pretty = \case
     MPFile  dp      -> cat $ punctuate "." (map pretty dp)
-    MPBound dp id i -> "MPBound??" -- don't know what this corresponds to
+    MPBound dp id i -> "MPBound??" -- NOTE: don't know what this corresponds to
     MPDot mp i      -> pretty mp <> "." <> pretty i
 
 instance Pretty KerName where