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)
-- dfStr (Name (NameId i) c) = "d" ++ (show i)

conQStr :: QName -> String
conQStr qn = "C" ++ (show $ numOfQName qn)

dfQStr :: QName -> String
dfQStr qn = "d" ++ (show $ numOfQName qn)

-- For now a hack that allows hierarhical modules, but not local modules(?)
moduleStr :: ModuleName -> String
-- moduleStr m = show m
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))

-- dataQName :: QName -> HsQName
-- dataQName 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 (QName m (Name (NameId i) nc) ) = i
numOfQName = numOfName . qnameName


rtpQName :: String -> HsQName
rtpQName s = Qual (Module "RTP")(HsIdent $ ('_':s))
rtpCon s = Qual (Module "RTP")(HsIdent s)