-- |
-- 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 (Name a -> Name a -> Bool
(Name a -> Name a -> Bool)
-> (Name a -> Name a -> Bool) -> Eq (Name a)
forall a. Name a -> Name a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Name a -> Name a -> Bool
== :: Name a -> Name a -> Bool
$c/= :: forall a. Name a -> Name a -> Bool
/= :: Name a -> Name a -> Bool
Eq, Eq (Name a)
Eq (Name a)
-> (Name a -> Name a -> Ordering)
-> (Name a -> Name a -> Bool)
-> (Name a -> Name a -> Bool)
-> (Name a -> Name a -> Bool)
-> (Name a -> Name a -> Bool)
-> (Name a -> Name a -> Name a)
-> (Name a -> Name a -> Name a)
-> Ord (Name a)
Name a -> Name a -> Bool
Name a -> Name a -> Ordering
Name a -> Name a -> Name a
forall a. Eq (Name a)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Name a -> Name a -> Bool
forall a. Name a -> Name a -> Ordering
forall a. Name a -> Name a -> Name a
$ccompare :: forall a. Name a -> Name a -> Ordering
compare :: Name a -> Name a -> Ordering
$c< :: forall a. Name a -> Name a -> Bool
< :: Name a -> Name a -> Bool
$c<= :: forall a. Name a -> Name a -> Bool
<= :: Name a -> Name a -> Bool
$c> :: forall a. Name a -> Name a -> Bool
> :: Name a -> Name a -> Bool
$c>= :: forall a. Name a -> Name a -> Bool
>= :: Name a -> Name a -> Bool
$cmax :: forall a. Name a -> Name a -> Name a
max :: Name a -> Name a -> Name a
$cmin :: forall a. Name a -> Name a -> Name a
min :: Name a -> Name a -> Name a
Ord, Typeable, (forall x. Name a -> Rep (Name a) x)
-> (forall x. Rep (Name a) x -> Name a) -> Generic (Name a)
forall x. Rep (Name a) x -> Name a
forall x. Name a -> Rep (Name a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Name a) x -> Name a
forall a x. Name a -> Rep (Name a) x
$cfrom :: forall a x. Name a -> Rep (Name a) x
from :: forall x. Name a -> Rep (Name a) x
$cto :: forall a x. Rep (Name a) x -> Name a
to :: forall x. Rep (Name a) x -> Name a
Generic)

instance NFData (Name a) where
  rnf :: Name a -> ()
rnf (Fn String
s Integer
n) = String -> ()
forall a. NFData a => a -> ()
rnf String
s () -> () -> ()
forall a b. a -> b -> b
`seq` Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
n () -> () -> ()
forall a b. a -> b -> b
`seq` ()
  rnf (Bn Integer
i Integer
j) = Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
i () -> () -> ()
forall a b. a -> b -> b
`seq` Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
j () -> () -> ()
forall a b. a -> b -> b
`seq` ()

-- | Returns 'True' iff the given @Name a@ is free.
isFreeName :: Name a -> Bool
isFreeName :: forall a. Name a -> Bool
isFreeName (Fn String
_ Integer
_) = Bool
True
isFreeName Name a
_ = Bool
False

-- | Make a free 'Name a' from a 'String'
string2Name :: String -> Name a
string2Name :: forall a. String -> Name a
string2Name String
s = String -> Integer -> Name a
forall a. String -> Integer -> Name a
makeName String
s Integer
0

-- | Synonym for 'string2Name'.
s2n :: String -> Name a
s2n :: forall a. String -> Name a
s2n = String -> Name a
forall a. String -> Name a
string2Name

-- | Make a name from a 'String' and an 'Integer' index
makeName :: String -> Integer -> Name a
makeName :: forall a. String -> Integer -> Name a
makeName = String -> Integer -> Name a
forall a. String -> Integer -> Name a
Fn

-- | Get the integer part of a 'Name'.
name2Integer :: Name a -> Integer
name2Integer :: forall a. Name a -> Integer
name2Integer (Fn String
_ Integer
i) = Integer
i
name2Integer (Bn Integer
_ Integer
_) = String -> Integer
forall a. HasCallStack => String -> a
error String
"Internal Error: cannot call name2Integer for bound names"

-- | Get the string part of a 'Name'.
name2String :: Name a -> String
name2String :: forall a. Name a -> String
name2String (Fn String
s Integer
_) = String
s
name2String (Bn Integer
_ Integer
_) = String -> String
forall a. HasCallStack => String -> a
error String
"Internal Error: cannot call name2String for bound names"

instance Show (Name a) where
  show :: Name a -> String
show (Fn String
"" Integer
n) = String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer -> String
forall a. Show a => a -> String
show Integer
n)
  show (Fn String
x Integer
0) = String
x
  show (Fn String
x Integer
n) = String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer -> String
forall a. Show a => a -> String
show Integer
n)
  show (Bn Integer
x Integer
y) = Integer -> String
forall a. Show a => a -> String
show Integer
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
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 -> String
show (AnyName Name a
nm) = Name a -> String
forall a. Show a => a -> String
show Name a
nm

instance Eq AnyName where
  (AnyName Name a
n1) == :: AnyName -> AnyName -> Bool
== (AnyName Name a
n2) = case Name a -> Maybe (Name a)
forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast Name a
n2 of
    Just Name a
n2' -> Name a
n1 Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
== Name a
n2'
    Maybe (Name a)
Nothing -> Bool
False

instance Ord AnyName where
  compare :: AnyName -> AnyName -> Ordering
compare (AnyName Name a
n1) (AnyName Name a
n2) = case TypeRep -> TypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Name a
n1) (Name a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Name a
n2) of
    Ordering
EQ -> case Name a -> Maybe (Name a)
forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast Name a
n2 of
      Just Name a
n2' -> Name a -> Name a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Name a
n1 Name a
n2'
      Maybe (Name a)
Nothing -> String -> Ordering
forall a. HasCallStack => String -> a
error String
"Equal type representations, but gcast failed in comparing two AnyName values"
    Ordering
ord -> Ordering
ord