module Unbound.Nominal.Name where
import Generics.RepLib
data Name a
= Nm (R a) (String, Integer)
deriving (Eq, Ord)
data AnyName = forall a. Rep a => AnyName (Name a)
$(derive_abstract [''AnyName])
instance Show AnyName where
show (AnyName n1) = show n1
instance Eq AnyName where
(AnyName n1) == (AnyName n2) =
case gcastR (getR n1) (getR n2) n1 of
Just n1' -> n1' == n2
Nothing -> False
instance Ord AnyName where
compare (AnyName n1) (AnyName n2) =
case compareR (getR n1) (getR n2) of
EQ -> case gcastR (getR n1) (getR n2) n1 of
Just n1' -> compare n1' n2
Nothing -> error "Panic: equal types are not equal in Ord AnyName instance!"
ord -> ord
name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11
:: Rep a => Name a
name1 = integer2Name 1
name2 = integer2Name 2
name3 = integer2Name 3
name4 = integer2Name 4
name5 = integer2Name 5
name6 = integer2Name 6
name7 = integer2Name 7
name8 = integer2Name 8
name9 = integer2Name 9
name10 = integer2Name 10
name11 = integer2Name 11
instance Show (Name a) where
show (Nm _ ("",n)) = "_" ++ (show n)
show (Nm _ (x,0)) = x
show (Nm _ (x,n)) = x ++ (show n)
name2Integer :: Name a -> Integer
name2Integer (Nm _ (_,x)) = x
name2String :: Name a -> String
name2String (Nm _ (s,_)) = s
anyName2Integer :: AnyName -> Integer
anyName2Integer (AnyName nm) = name2Integer nm
anyName2String :: AnyName -> String
anyName2String (AnyName nm) = name2String nm
toSortedName :: Rep a => AnyName -> Maybe (Name a)
toSortedName (AnyName n) = gcastR (getR n) rep n
integer2Name :: Rep a => Integer -> Name a
integer2Name n = makeName "" n
string2Name :: Rep a => String -> Name a
string2Name s = makeName s 0
s2n :: Rep a => String -> Name a
s2n = string2Name
makeName :: Rep a => String -> Integer -> Name a
makeName s i = Nm rep (s,i)
getR :: Name a -> R a
getR (Nm r _) = r
translate :: (Rep b) => Name a -> Name b
translate (Nm _ x) = Nm rep x