{-# LANGUAGE GADTs, DeriveDataTypeable, ViewPatterns #-}
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds #-}
module Data.Binding.Hobbits.Internal.Mb where
import Data.Typeable
import Data.Proxy
import Data.Type.Equality
import Data.Type.RList hiding (map)
import Data.Binding.Hobbits.Internal.Name
data Mb (ctx :: RList k) b
= MkMbFun (RAssign Proxy ctx) (RAssign Name ctx -> b)
| MkMbPair (MbTypeRepr b) (RAssign Name ctx) b
deriving Typeable
data MbTypeRepr a where
MbTypeReprName :: MbTypeRepr (Name a)
MbTypeReprMb :: MbTypeRepr a -> MbTypeRepr (Mb ctx a)
MbTypeReprFun :: MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)
MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a
data MbTypeReprData a =
MkMbTypeReprData (forall ctx. NameRefresher -> a -> a)
mapNamesPf :: MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf :: MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf MbTypeRepr a
MbTypeReprName NameRefresher
refresher a
n = NameRefresher -> Name a -> Name a
forall k (a :: k). NameRefresher -> Name a -> Name a
refreshName NameRefresher
refresher a
Name a
n
mapNamesPf (MbTypeReprMb MbTypeRepr a
tRepr) NameRefresher
refresher (a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun -> (RAssign Proxy ctx
proxies, RAssign Name ctx -> a
f)) =
RAssign Proxy ctx -> (RAssign Name ctx -> a) -> Mb ctx a
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun RAssign Proxy ctx
proxies (\RAssign Name ctx
ns -> MbTypeRepr a -> NameRefresher -> a -> a
forall a. MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf MbTypeRepr a
tRepr NameRefresher
refresher (RAssign Name ctx -> a
f RAssign Name ctx
ns))
mapNamesPf (MbTypeReprFun MbTypeRepr a
tReprIn MbTypeRepr b
tReprOut) NameRefresher
refresher a
f =
(MbTypeRepr b -> NameRefresher -> b -> b
forall a. MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf MbTypeRepr b
tReprOut NameRefresher
refresher) (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a
a -> b
f (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MbTypeRepr a -> NameRefresher -> a -> a
forall a. MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf MbTypeRepr a
tReprIn NameRefresher
refresher)
mapNamesPf (MbTypeReprData (MkMbTypeReprData forall (ctx :: k). NameRefresher -> a -> a
mapFun)) NameRefresher
refresher a
x =
NameRefresher -> a -> a
forall (ctx :: k). NameRefresher -> a -> a
mapFun NameRefresher
refresher a
x
ensureFreshFun :: Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun :: Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun (MkMbFun RAssign Proxy ctx
proxies RAssign Name ctx -> a
f) = (RAssign Proxy ctx
proxies, RAssign Name ctx -> a
f)
ensureFreshFun (MkMbPair MbTypeRepr a
tRepr RAssign Name ctx
ns a
body) =
((forall (x :: k). Name x -> Proxy x)
-> RAssign Name ctx -> RAssign Proxy ctx
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
mapRAssign (\Name x
_ -> Proxy x
forall k (t :: k). Proxy t
Proxy) RAssign Name ctx
ns, \RAssign Name ctx
ns' ->
MbTypeRepr a -> NameRefresher -> a -> a
forall a. MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf MbTypeRepr a
tRepr (RAssign Name ctx -> RAssign Name ctx -> NameRefresher
forall k (ctx :: RList k).
RAssign Name ctx -> RAssign Name ctx -> NameRefresher
mkRefresher RAssign Name ctx
ns RAssign Name ctx
ns') a
body)
ensureFreshPair :: Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair :: Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair (MkMbPair MbTypeRepr a
_ RAssign Name ctx
ns a
body) = (RAssign Name ctx
ns, a
body)
ensureFreshPair (MkMbFun RAssign Proxy ctx
proxies RAssign Name ctx -> a
f) =
let ns :: RAssign Name ctx
ns = (forall (x :: k). Proxy x -> Name x)
-> RAssign Proxy ctx -> RAssign Name ctx
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
mapRAssign (Int -> Name x
forall k (a :: k). Int -> Name a
MkName (Int -> Name x) -> (Proxy x -> Int) -> Proxy x -> Name x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy x -> Int
forall a. a -> Int
fresh_name) RAssign Proxy ctx
proxies in
(RAssign Name ctx
ns, RAssign Name ctx -> a
f RAssign Name ctx
ns)