module Agda.Compiler.Alonzo.Names where
import Data.List
import Language.Haskell.Syntax
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
conStr :: Name -> String
conStr n = "C" ++ (show $ numOfName n)
dfStr :: Name -> String
dfStr n = "d" ++ (show $ numOfName n)
conQStr :: QName -> String
conQStr qn = "C" ++ (show $ numOfQName qn)
dfQStr :: QName -> String
dfQStr qn = "d" ++ (show $ numOfQName qn)
moduleStr :: ModuleName -> String
moduleStr (MName []) = error "Empty module list!"
moduleStr (MName ns) = intercalate "." (map show ns)
conName :: Name -> HsName
conName = HsIdent . conStr
dataName :: Name -> HsName
dataName n = HsIdent $ "T" ++ (show (numOfName n))
dfName :: Name -> HsName
dfName = HsIdent . dfStr
dfNameSub :: Name -> Int -> HsName
dfNameSub name i = HsIdent id where
id = (dfStr name) ++ "_" ++ (show i)
dfQName :: QName -> HsQName
dfQName (QName m n)
| (moduleStr m) == "RTP" = Qual (Module $ moduleStr m)(HsIdent $ "_"++(show n))
| otherwise = Qual (Module $ moduleStr m) (dfName n)
conQName :: QName -> HsQName
conQName (QName m n)
|(moduleStr m)=="RTP" = Qual (Module $ moduleStr m) (HsIdent $ show n)
| otherwise = Qual (Module $ moduleStr m) (conName n)
numOfName :: Name -> Nat
numOfName n = i where
id = nameId n
(NameId i mi) = id
numOfQName :: QName -> Nat
numOfQName = numOfName . qnameName
rtpQName :: String -> HsQName
rtpQName s = Qual (Module "RTP")(HsIdent $ ('_':s))
rtpCon s = Qual (Module "RTP")(HsIdent s)