content: -- |
  -- Module     : Unbound.Generics.LocallyNameless.Name
  -- Copyright  : (c) 2014, Aleksey Kliger
  -- License    : BSD3 (See LICENSE)
  -- Maintainer : Aleksey Kliger
  -- Stability  : experimental
  --
  -- Names stand for values.  They may be bound or free.
  {-# LANGUAGE DeriveDataTypeable
               , DeriveGeneric
               , ExistentialQuantification
               , FlexibleContexts
               , GADTs #-}
  module Unbound.Generics.LocallyNameless.Name
         (
           -- * Names over terms
           Name(..)
         , isFreeName
           -- * Name construction
         , string2Name
         , s2n
         , makeName
           -- * Name inspection
         , name2String
         , name2Integer
           -- * Heterogeneous names
         , AnyName(..)
         ) where
  
  import Control.DeepSeq (NFData(..))
  import Data.Typeable (Typeable, gcast, typeOf)
  import GHC.Generics (Generic)
  
  -- | An abstract datatype of names @Name a@ that stand for terms of
  -- type @a@.  The type @a@ is used as a tag to distinguish these names
  -- from names that may stand for other sorts of terms.
  --
  -- Two names in a term are considered
  -- 'Unbound.Generics.LocallyNameless.Operations.aeq' equal when they
  -- are the same name (in the sense of '(==)').  In patterns, however,
  -- any two names are equal if they occur in the same place within the
  -- pattern.  This induces alpha equivalence on terms in general.
  --
  -- Names may either be free or bound (see 'isFreeName').  Free names
  -- may be extracted from patterns using
  -- 'Unbound.Generics.LocallyNameless.Alpha.isPat'.  Bound names
  -- cannot be.
  -- 
  data Name a = Fn String !Integer    -- free names
              | Bn !Integer !Integer  -- bound names / binding level + pattern index
              deriving (Eq, Ord, Typeable, Generic)
  
  instance NFData (Name a) where
    rnf (Fn s n) = rnf s `seq` rnf n `seq` ()
    rnf (Bn i j) = rnf i `seq` rnf j `seq` ()
  
  -- | Returns 'True' iff the given @Name a@ is free.
  isFreeName :: Name a -> Bool
  isFreeName (Fn _ _) = True
  isFreeName _ = False
  
  -- | Make a free 'Name a' from a 'String'
  string2Name :: String -> Name a
  string2Name s = makeName s 0
  
  -- | Synonym for 'string2Name'.
  s2n :: String -> Name a
  s2n = string2Name
  
  -- | Make a name from a 'String' and an 'Integer' index
  makeName :: String -> Integer -> Name a
  makeName = Fn
  
  -- | Get the integer part of a 'Name'.
  name2Integer :: Name a -> Integer
  name2Integer (Fn _ i) = i
  name2Integer (Bn _ _) = error "Internal Error: cannot call name2Integer for bound names"
  
  -- | Get the string part of a 'Name'.
  name2String :: Name a -> String
  name2String (Fn s _) = s
  name2String (Bn _ _) = error "Internal Error: cannot call name2String for bound names"
  
  instance Show (Name a) where
    show (Fn "" n) = "_" ++ (show n)
    show (Fn x 0) = x
    show (Fn x n) = x ++ (show n)
    show (Bn x y) = show x ++ "@" ++ show y
  
  -- | An @AnyName@ is a name that stands for a term of some (existentially hidden) type.
  data AnyName where
    AnyName :: Typeable a => Name a -> AnyName
  
  instance Show AnyName where
    show (AnyName nm) = show nm
  
  instance Eq AnyName where
    (AnyName n1) == (AnyName n2) = case gcast n2 of
      Just n2' -> n1 == n2'
      Nothing -> False
  
  instance Ord AnyName where
    compare (AnyName n1) (AnyName n2) = case compare (typeOf n1) (typeOf n2) of
      EQ -> case gcast n2 of
        Just n2' -> compare n1 n2'
        Nothing -> error "Equal type representations, but gcast failed in comparing two AnyName values"
      ord -> ord
  