{-# LANGUAGE GADTs, DeriveDataTypeable, FlexibleInstances, TypeOperators #-}
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds #-}

-- |
-- Module      : Data.Binding.Hobbits.Internal.Name
-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : westbrook@kestrel.edu
-- Stability   : experimental
-- Portability : GHC
--
-- This module defines the type @'Name' a@ as a wrapper around a fresh
-- integer. Note that, in order to ensure adequacy of the Hobbits
-- name-binding approach, this representation is hidden from the user,
-- and so this file should never be imported directly by the user.
--

module Data.Binding.Hobbits.Internal.Name where

import Data.List
import Data.Functor.Constant
import Data.Typeable
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.Type.Equality
import Unsafe.Coerce (unsafeCoerce)
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
import System.IO.Unsafe (unsafePerformIO)

import Data.Type.RList


-- | A @Name a@ is a bound name that is associated with type @a@.
newtype Name (a :: k) = MkName Int deriving (Typeable, Name a -> Name a -> Bool
(Name a -> Name a -> Bool)
-> (Name a -> Name a -> Bool) -> Eq (Name a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). Name a -> Name a -> Bool
/= :: Name a -> Name a -> Bool
$c/= :: forall k (a :: k). Name a -> Name a -> Bool
== :: Name a -> Name a -> Bool
$c== :: forall k (a :: k). 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 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 k (a :: k). Eq (Name a)
forall k (a :: k). Name a -> Name a -> Bool
forall k (a :: k). Name a -> Name a -> Ordering
forall k (a :: k). Name a -> Name a -> Name a
min :: Name a -> Name a -> Name a
$cmin :: forall k (a :: k). Name a -> Name a -> Name a
max :: Name a -> Name a -> Name a
$cmax :: forall k (a :: k). Name a -> Name a -> Name a
>= :: Name a -> Name a -> Bool
$c>= :: forall k (a :: k). Name a -> Name a -> Bool
> :: Name a -> Name a -> Bool
$c> :: forall k (a :: k). Name a -> Name a -> Bool
<= :: Name a -> Name a -> Bool
$c<= :: forall k (a :: k). Name a -> Name a -> Bool
< :: Name a -> Name a -> Bool
$c< :: forall k (a :: k). Name a -> Name a -> Bool
compare :: Name a -> Name a -> Ordering
$ccompare :: forall k (a :: k). Name a -> Name a -> Ordering
$cp1Ord :: forall k (a :: k). Eq (Name a)
Ord)

instance Show (Name a) where
  showsPrec :: Int -> Name a -> ShowS
showsPrec Int
_ (MkName Int
n) = Char -> ShowS
showChar Char
'#' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
n ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'#'

instance Show (RAssign Name c) where
    show :: RAssign Name c -> String
show RAssign Name c
names = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"," ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Name a -> String) -> RAssign Name c -> [String]
forall k (f :: k -> *) b (ctx :: RList k).
(forall (a :: k). f a -> b) -> RAssign f ctx -> [b]
mapToList forall (a :: k). Name a -> String
forall a. Show a => a -> String
show RAssign Name c
names) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"


-------------------------------------------------------------------------------
-- Externally visible operators
-------------------------------------------------------------------------------

{-|
  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,
  respectively. When they are equal, @Some e@ is returned for @e@ a proof
  of type @a :~: b@ that their types are equal. Otherwise, @None@ is returned.

  For example:

> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl
> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None
-}
cmpName :: Name a -> Name b -> Maybe (a :~: b)
cmpName :: Name a -> Name b -> Maybe (a :~: b)
cmpName (MkName Int
n1) (MkName Int
n2)
  | Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n2 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((a :~: b) -> Maybe (a :~: b)) -> (a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl
  | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance TestEquality Name where
  testEquality :: Name a -> Name b -> Maybe (a :~: b)
testEquality = Name a -> Name b -> Maybe (a :~: b)
forall k (a :: k) (b :: k). Name a -> Name b -> Maybe (a :~: b)
cmpName

-- | Heterogeneous comparison of names, that could be at different kinds
hcmpName :: forall k1 k2 (a :: k1) (b :: k2). Name a -> Name b -> Maybe (a :~~: b)
hcmpName :: Name a -> Name b -> Maybe (a :~~: b)
hcmpName (MkName Int
n1) (MkName Int
n2)
  | Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n2 = (a :~~: b) -> Maybe (a :~~: b)
forall a. a -> Maybe a
Just ((a :~~: b) -> Maybe (a :~~: b)) -> (a :~~: b) -> Maybe (a :~~: b)
forall a b. (a -> b) -> a -> b
$ (Any :~~: Any) -> a :~~: b
forall a b. a -> b
unsafeCoerce Any :~~: Any
forall k1 (a :: k1). a :~~: a
HRefl
  | Bool
otherwise = Maybe (a :~~: b)
forall a. Maybe a
Nothing

-- | A name refresher gives new fresh indices to names
newtype NameRefresher = NameRefresher { NameRefresher -> IntMap Int
unNameRefresher :: IntMap Int }

-- | Apply a 'NameRefresher' to a 'Name'
refreshName :: NameRefresher -> Name a -> Name a
refreshName :: NameRefresher -> Name a -> Name a
refreshName (NameRefresher IntMap Int
nmap) (MkName Int
i) =
  Int -> Name a
forall k (a :: k). Int -> Name a
MkName (Int -> Name a) -> Int -> Name a
forall a b. (a -> b) -> a -> b
$ Int -> Int -> IntMap Int -> Int
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault Int
i Int
i IntMap Int
nmap

-- | Build a 'NameRefresher' that maps one sequence of names to another
mkRefresher :: forall k (ctx :: RList k) .
               RAssign Name ctx -> RAssign Name ctx -> NameRefresher
mkRefresher :: RAssign Name ctx -> RAssign Name ctx -> NameRefresher
mkRefresher RAssign Name ctx
ns1 RAssign Name ctx
ns2 =
  IntMap Int -> NameRefresher
NameRefresher (IntMap Int -> NameRefresher) -> IntMap Int -> NameRefresher
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ RAssign (Constant (Int, Int)) ctx -> [(Int, Int)]
forall k a (c :: RList k). RAssign (Constant a) c -> [a]
toList (RAssign (Constant (Int, Int)) ctx -> [(Int, Int)])
-> RAssign (Constant (Int, Int)) ctx -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$
  (forall (x :: k). Name x -> Name x -> Constant (Int, Int) x)
-> RAssign Name ctx
-> RAssign Name ctx
-> RAssign (Constant (Int, Int)) ctx
forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x -> h x)
-> RAssign f c -> RAssign g c -> RAssign h c
map2 (\(MkName i) (MkName j) -> (Int, Int) -> Constant (Int, Int) x
forall k a (b :: k). a -> Constant a b
Constant (Int
i,Int
j)) RAssign Name ctx
ns1 RAssign Name ctx
ns2

-- | Extend a 'NameRefresher' with one more name mapping
extRefresher :: forall k (a :: k). NameRefresher -> Name a -> Name a ->
                NameRefresher
extRefresher :: NameRefresher -> Name a -> Name a -> NameRefresher
extRefresher (NameRefresher IntMap Int
nmap) (MkName Int
n1) (MkName Int
n2) =
  IntMap Int -> NameRefresher
NameRefresher (IntMap Int -> NameRefresher) -> IntMap Int -> NameRefresher
forall a b. (a -> b) -> a -> b
$
  (Int -> Int -> Int) -> Int -> Int -> IntMap Int -> IntMap Int
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith (\Int
_ Int
_ -> String -> Int
forall a. HasCallStack => String -> a
error String
"Hobbit name already in NameRefresher!")
  Int
n1 Int
n2 IntMap Int
nmap


-------------------------------------------------------------------------------
-- Hidden, unsafe operators
-------------------------------------------------------------------------------


-- building an arbitrary InCtx proof with a given length
-- (this is used internally in HobbitLib)

data ExMember where ExMember :: Member c a -> ExMember

-- creating some Member proof of length i
memberFromLen :: Int -> ExMember
memberFromLen :: Int -> ExMember
memberFromLen Int
0 = Member (Any ':> Any) Any -> ExMember
forall k1 k2 (c :: RList k1) (a :: k2). Member c a -> ExMember
ExMember Member (Any ':> Any) Any
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
memberFromLen Int
n = case Int -> ExMember
memberFromLen (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) of
  ExMember Member c a
mem -> Member (c ':> Any) a -> ExMember
forall k1 k2 (c :: RList k1) (a :: k2). Member c a -> ExMember
ExMember (Member c a -> Member (c ':> Any) a
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step Member c a
mem)

-- unsafely creating a *specific* member proof from length i;
-- this is for when we know the ith element of c must be type a
unsafeLookupC :: Int -> Member c a
unsafeLookupC :: Int -> Member c a
unsafeLookupC Int
n = case Int -> ExMember
memberFromLen Int
n of
  ExMember Member c a
mem -> Member c a -> Member c a
forall a b. a -> b
unsafeCoerce Member c a
mem


-- building a proxy for each type in some unknown context
data ExProxy where ExProxy :: RAssign Proxy ctx -> ExProxy
proxyFromLen :: Int -> ExProxy
proxyFromLen :: Int -> ExProxy
proxyFromLen Int
0 = RAssign Proxy 'RNil -> ExProxy
forall k (ctx :: RList k). RAssign Proxy ctx -> ExProxy
ExProxy RAssign Proxy 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil
proxyFromLen Int
n = case Int -> ExProxy
proxyFromLen (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) of
                   ExProxy RAssign Proxy ctx
proxy -> RAssign Proxy (ctx ':> Any) -> ExProxy
forall k (ctx :: RList k). RAssign Proxy ctx -> ExProxy
ExProxy (RAssign Proxy ctx
proxy RAssign Proxy ctx -> Proxy Any -> RAssign Proxy (ctx ':> Any)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Proxy Any
forall k (t :: k). Proxy t
Proxy)

-- -- unsafely building a proxy for each type in ctx from the length n
-- -- of ctx; this is only safe when we know the length of ctx = n
-- unsafeProxyFromLen :: Int -> MapC Proxy ctx
-- unsafeProxyFromLen n = case proxyFromLen n of
--                          ExProxy proxy -> unsafeCoerce proxy

-- -- unsafely convert a list of Ints, used to represent names, to
-- -- names of certain, given types; note that the first name in the
-- -- list becomes the last name in the output, with the same reversal
-- -- used in the Mb representation (see, e.g., mbCombine)
-- unsafeNamesFromInts :: [Int] -> MapC Name ctx
-- unsafeNamesFromInts [] = unsafeCoerce Nil
-- unsafeNamesFromInts (x:xs) =
--     unsafeCoerce $ unsafeNamesFromInts xs :> MkName x

-------------------------------------------------------------------------------
-- encapsulated impurity
-------------------------------------------------------------------------------

-- README: we *cannot* inline counter, because we want all uses
-- of counter to be the same IORef
counter :: IORef Int
{-# NOINLINE counter #-}
counter :: IORef Int
counter = IO (IORef Int) -> IORef Int
forall a. IO a -> a
unsafePerformIO (Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0)

-- README: fresh_name takes a dummy argument that is used in a dummy
-- way to avoid let-floating its body (and thus getting a fresh name
-- exactly once)
-- README: it *is* ok to inline fresh_name because we don't care in
-- what order fresh names are created
fresh_name :: a -> Int
fresh_name :: a -> Int
fresh_name a
a = IO Int -> Int
forall a. IO a -> a
unsafePerformIO (IO Int -> Int) -> IO Int -> Int
forall a b. (a -> b) -> a -> b
$ do 
    IORef a
dummyRef <- a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef a
a
    Int
x <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
counter
    IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
counter (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
    Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
x

-- -- make one fresh name for each name in a given input list
-- fresh_names :: MapC Name ctx -> MapC Name ctx
-- fresh_names Nil = Nil
-- fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)