{-# LANGUAGE GADTs, DeriveDataTypeable, ViewPatterns #-}
{-# 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 @'Mb' ctx a@. In order to ensure
-- adequacy of the Hobbits name-binding approach, this representation
-- is hidden, and so this file should never be imported directly by
-- the user.
--

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


{-|
  An @Mb ctx b@ is a multi-binding that binds one name for each type
  in @ctx@, where @ctx@ has the form @'RNil' ':>' t1 ':>' ... ':>' tn@.
  Internally, multi-bindings are represented either as "fresh
  functions", which are functions that quantify over all fresh names
  that have not been used before and map them to the body of the
  binding, or as "fresh pairs", which are pairs of a list of names
  that are guaranteed to be fresh along with a body. Note that fresh
  pairs must come with an 'MbTypeRepr' for the body type, to ensure
  that the names given in the pair can be relaced by fresher names.
-}
data Mb (ctx :: RList k) b
    = MkMbFun (RAssign Proxy ctx) (RAssign Name ctx -> b)
    | MkMbPair (MbTypeRepr b) (RAssign Name ctx) b
    deriving Typeable


{-|
   This type states that it is possible to replace free names with
   fresh names in an object of type @a@. This type essentially just
   captures a representation of the type a as either a Name type, a
   multi-binding, a function type, or a (G)ADT. In order to be sure
   that only the "right" proofs are used for (G)ADTs, however, this
   type is hidden from the user, and can only be constructed with
   'mkNuMatching'.
-}

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)

{-|
  The call @mapNamesPf data ns ns' a@ replaces each occurrence of a
  free name in @a@ which is listed in @ns@ by the corresponding name
  listed in @ns'@. This is similar to the name-swapping of Nominal
  Logic, except that the swapping does not go both ways.
-}
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)) =
    -- README: the fresh function created below is *guaranteed* to not
    -- be passed elements of either names1 or names2, since it should
    -- only ever be passed fresh names
    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


-- | Ensures a multi-binding is in "fresh function" form
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)

-- | Ensures a multi-binding is in "fresh pair" form
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)