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

-- |
-- Module      : Data.Binding.Hobbits.Mb
-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : emw4@rice.edu
-- Stability   : experimental
-- Portability : GHC
--
-- This module defines multi-bindings as the type 'Mb', as well as a number of
-- operations on multi-bindings. See the paper E. Westbrook, N. Frisby,
-- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in
-- Functional Programming Languages\" for more information.

module Data.Binding.Hobbits.Mb (
  -- * Abstract types
  Name(),      -- hides Name implementation
  Binding(),   -- hides Binding implementation
  Mb(),        -- hides MultiBind implementation
  -- * Multi-binding constructors
  nu, nuMulti, nus, emptyMb, extMb, extMbMulti,
  -- * Queries on names
  cmpName, hcmpName, mbNameBoundP, mbCmpName,
  -- * Operations on multi-bindings
  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbPure, mbApply,
  mbMap2,
  -- * Eliminators for multi-bindings
  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1
) where

import Control.Applicative
import Control.Monad.Identity

import Data.Type.Equality ((:~:)(..))
import Data.Proxy (Proxy(..))

import Unsafe.Coerce (unsafeCoerce)

import Data.Type.RList

import Data.Binding.Hobbits.Internal.Name
import Data.Binding.Hobbits.Internal.Mb
--import qualified Data.Binding.Hobbits.Internal as I

-------------------------------------------------------------------------------
-- creating bindings
-------------------------------------------------------------------------------

-- | A @Binding@ is simply a multi-binding that binds one name
type Binding (a :: k) = Mb (RNil :> a)

-- note: we reverse l to show the inner-most bindings last
instance Show a => Show (Mb c a) where
  showsPrec :: Int -> Mb c a -> ShowS
showsPrec Int
p (Mb c a -> (RAssign Name c, a)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name c
names, a
b)) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Char -> ShowS
showChar Char
'#' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RAssign Name c -> ShowS
forall a. Show a => a -> ShowS
shows RAssign Name c
names ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'.' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Show a => a -> ShowS
shows a
b

{-|
  @nu f@ creates a binding which binds a fresh name @n@ and whose
  body is the result of @f n@.
-}
nu :: forall k1 (a :: k1) (b :: *) . (Name a -> b) -> Binding a b
nu :: (Name a -> b) -> Binding a b
nu Name a -> b
f = RAssign Proxy ('RNil ':> a)
-> (RAssign Name ('RNil ':> a) -> b) -> Binding a b
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun (RAssign Proxy 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign Proxy 'RNil -> Proxy a -> RAssign Proxy ('RNil ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Proxy a
forall k (t :: k). Proxy t
Proxy) (\(RAssign Name c
MNil :>: Name a
n) -> Name a -> b
f Name a
Name a
n)

{-|
  The expression @nuMulti p f@ creates a multi-binding of zero or more
  names, one for each element of the vector @p@. The bound names are
  passed the names to @f@, which returns the body of the
  multi-binding.  The argument @p@, of type @'RAssign' f ctx@, acts as a
  \"phantom\" argument, used to reify the list of types @ctx@ at the
  term level; thus it is unimportant what the type function @f@ is.
-}
nuMulti :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti RAssign f ctx
proxies RAssign Name ctx -> b
f = RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun ((forall (x :: k). f x -> Proxy x)
-> RAssign f 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 (Proxy x -> f x -> Proxy x
forall a b. a -> b -> a
const Proxy x
forall k (t :: k). Proxy t
Proxy) RAssign f ctx
proxies) RAssign Name ctx -> b
f

-- | @nus = nuMulti@
nus :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nus RAssign f ctx
x = RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
forall k (f :: k -> *) (ctx :: RList k) b.
RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti RAssign f ctx
x

-- | Extend the context of a name-binding by adding a single type
extMb :: Mb ctx a -> Mb (ctx :> tp) a
extMb :: Mb ctx a -> Mb (ctx ':> tp) a
extMb = Mb ctx (Mb ('RNil ':> tp) a) -> Mb (ctx ':> tp) a
forall k k (c1 :: RList k) (c2 :: RList k) (a :: k) b.
Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
mbCombine (Mb ctx (Mb ('RNil ':> tp) a) -> Mb (ctx ':> tp) a)
-> (Mb ctx a -> Mb ctx (Mb ('RNil ':> tp) a))
-> Mb ctx a
-> Mb (ctx ':> tp) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Mb ('RNil ':> tp) a)
-> Mb ctx a -> Mb ctx (Mb ('RNil ':> tp) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name tp -> a) -> Mb ('RNil ':> tp) a
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu ((Name tp -> a) -> Mb ('RNil ':> tp) a)
-> (a -> Name tp -> a) -> a -> Mb ('RNil ':> tp) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Name tp -> a
forall a b. a -> b -> a
const)

-- | Extend the context of a name-binding with multiple types
extMbMulti :: RAssign f ctx2 -> Mb ctx1 a -> Mb (ctx1 :++: ctx2) a
extMbMulti :: RAssign f ctx2 -> Mb ctx1 a -> Mb (ctx1 :++: ctx2) a
extMbMulti RAssign f ctx2
ns Mb ctx1 a
mb = Mb ctx1 (Mb ctx2 a) -> Mb (ctx1 :++: ctx2) a
forall k k (c1 :: RList k) (c2 :: RList k) (a :: k) b.
Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
mbCombine (Mb ctx1 (Mb ctx2 a) -> Mb (ctx1 :++: ctx2) a)
-> Mb ctx1 (Mb ctx2 a) -> Mb (ctx1 :++: ctx2) a
forall a b. (a -> b) -> a -> b
$ (a -> Mb ctx2 a) -> Mb ctx1 a -> Mb ctx1 (Mb ctx2 a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RAssign f ctx2 -> (RAssign Name ctx2 -> a) -> Mb ctx2 a
forall k (f :: k -> *) (ctx :: RList k) b.
RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti RAssign f ctx2
ns ((RAssign Name ctx2 -> a) -> Mb ctx2 a)
-> (a -> RAssign Name ctx2 -> a) -> a -> Mb ctx2 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> RAssign Name ctx2 -> a
forall a b. a -> b -> a
const) Mb ctx1 a
mb


-------------------------------------------------------------------------------
-- Queries on Names
-------------------------------------------------------------------------------

{-|
  Checks if a name is bound in a multi-binding, returning @Left mem@
  when the name is bound, where @mem@ is a proof that the type of the
  name is in the type list for the multi-binding, and returning
  @Right n@ when the name is not bound, where @n@ is the name.

  For example:

> nu $ \n -> mbNameBoundP (nu $ \m -> m)  ==  nu $ \n -> Left Member_Base
> nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n
-}
mbNameBoundP :: forall k1 k2 (a :: k1) (ctx :: RList k2).
                Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP (Mb ctx (Name a) -> (RAssign Name ctx, Name a)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name ctx
names, Name a
n)) = RAssign Name ctx -> Name a -> Either (Member ctx a) (Name a)
forall k1 k (c :: RList k1) (a :: k).
RAssign Name c -> Name a -> Either (Member c a) (Name a)
helper RAssign Name ctx
names Name a
n where
    helper :: RAssign Name c -> Name a -> Either (Member c a) (Name a)
    helper :: RAssign Name c -> Name a -> Either (Member c a) (Name a)
helper RAssign Name c
MNil Name a
n = Name a -> Either (Member c a) (Name a)
forall a b. b -> Either a b
Right Name a
n
    helper (RAssign Name c
names :>: (MkName Int
i)) (MkName Int
j)
      | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j =
        Either (Member (Any ':> Any) Any) Any
-> Either (Member c a) (Name a)
forall a b. a -> b
unsafeCoerce (Either (Member (Any ':> Any) Any) Any
 -> Either (Member c a) (Name a))
-> Either (Member (Any ':> Any) Any) Any
-> Either (Member c a) (Name a)
forall a b. (a -> b) -> a -> b
$ Member (Any ':> Any) Any -> Either (Member (Any ':> Any) Any) Any
forall a b. a -> Either a b
Left Member (Any ':> Any) Any
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
    helper (RAssign Name c
names :>: Name a
_) Name a
n =
      case RAssign Name c -> Name a -> Either (Member c a) (Name a)
forall k1 k (c :: RList k1) (a :: k).
RAssign Name c -> Name a -> Either (Member c a) (Name a)
helper RAssign Name c
names Name a
n of
        Left Member c a
memb -> Member (c ':> a) a -> Either (Member (c ':> a) a) (Name a)
forall a b. a -> Either a b
Left (Member c a -> Member (c ':> a) a
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step Member c a
memb)
        Right Name a
n -> Name a -> Either (Member c a) (Name a)
forall a b. b -> Either a b
Right Name a
n
-- old implementation with lists
{-
case elemIndex n names of
  Nothing -> Right (MkName n)
  Just i -> Left (I.unsafeLookupC i)
-}


{-|
  Compares two names inside bindings, taking alpha-equivalence into
  account; i.e., if both are the @i@th name, or both are the same name
  not bound in their respective multi-bindings, then they compare as
  equal. The return values are the same as for 'cmpName', so that
  @Some Refl@ is returned when the names are equal and @Nothing@ is
  returned when they are not.
-}
mbCmpName :: forall k1 k2 (a :: k1) (b :: k1) (c :: RList k2).
             Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
mbCmpName (Mb c (Name a) -> (RAssign Name c, Name a)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name c
names, Name a
n1)) (Mb c (Name b) -> (RAssign Proxy c, RAssign Name c -> Name b)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun -> (RAssign Proxy c
_, RAssign Name c -> Name b
f2)) =
  Name a -> Name b -> Maybe (a :~: b)
forall k (a :: k) (b :: k). Name a -> Name b -> Maybe (a :~: b)
cmpName Name a
n1 (RAssign Name c -> Name b
f2 RAssign Name c
names)


-------------------------------------------------------------------------------
-- Operations on multi-bindings
-------------------------------------------------------------------------------

-- | Creates an empty binding that binds 0 names.
emptyMb :: a -> Mb RNil a
emptyMb :: a -> Mb 'RNil a
emptyMb a
body = RAssign Proxy 'RNil -> (RAssign Name 'RNil -> a) -> Mb 'RNil a
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun RAssign Proxy 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil (\RAssign Name 'RNil
_ -> a
body)

{-|
  Eliminates an empty binding, returning its body. Note that
  @elimEmptyMb@ is the inverse of @emptyMb@.
-}
elimEmptyMb :: Mb RNil a -> a
elimEmptyMb :: Mb 'RNil a -> a
elimEmptyMb (Mb 'RNil a -> (RAssign Name 'RNil, a)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name 'RNil
_, a
body)) = a
body


-- Extract the proxy objects from an Mb inside of a fresh function
freshFunctionProxies :: RAssign Proxy ctx1 -> (RAssign Name ctx1 -> Mb ctx2 a) ->
                        RAssign Proxy ctx2
freshFunctionProxies :: RAssign Proxy ctx1
-> (RAssign Name ctx1 -> Mb ctx2 a) -> RAssign Proxy ctx2
freshFunctionProxies RAssign Proxy ctx1
proxies1 RAssign Name ctx1 -> Mb ctx2 a
f =
    case RAssign Name ctx1 -> Mb ctx2 a
f ((forall (x :: k). Proxy x -> Name x)
-> RAssign Proxy ctx1 -> RAssign Name ctx1
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 -> Name x
forall a b. a -> b -> a
const (Name x -> Proxy x -> Name x) -> Name x -> Proxy x -> Name x
forall a b. (a -> b) -> a -> b
$ Int -> Name x
forall k (a :: k). Int -> Name a
MkName Int
0) RAssign Proxy ctx1
proxies1) of
      MkMbFun RAssign Proxy ctx2
proxies2 RAssign Name ctx2 -> a
_ -> RAssign Proxy ctx2
proxies2
      MkMbPair MbTypeRepr a
_ RAssign Name ctx2
ns a
_ -> (forall (x :: k). Name x -> Proxy x)
-> RAssign Name ctx2 -> RAssign Proxy ctx2
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
mapRAssign (Proxy x -> Name x -> Proxy x
forall a b. a -> b -> a
const Proxy x
forall k (t :: k). Proxy t
Proxy) RAssign Name ctx2
ns


-- README: inner-most bindings come FIRST
-- | Combines a binding inside another binding into a single binding.
mbCombine :: forall k (c1 :: RList k) (c2 :: RList k) a b.
             Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
mbCombine (MkMbPair MbTypeRepr (Mb c2 b)
tRepr1 RAssign Name c1
l1 (MkMbPair MbTypeRepr b
tRepr2 RAssign Name c2
l2 b
b)) =
  MbTypeRepr b -> RAssign Name (c1 :++: c2) -> b -> Mb (c1 :++: c2) b
forall k (ctx :: RList k) b.
MbTypeRepr b -> RAssign Name ctx -> b -> Mb ctx b
MkMbPair MbTypeRepr b
tRepr2 (RAssign Name c1 -> RAssign Name c2 -> RAssign Name (c1 :++: c2)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
append RAssign Name c1
l1 RAssign Name c2
l2) b
b
mbCombine (Mb c1 (Mb c2 b) -> (RAssign Proxy c1, RAssign Name c1 -> Mb c2 b)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun -> (RAssign Proxy c1
proxies1, RAssign Name c1 -> Mb c2 b
f1)) =
    -- README: we pass in Names with integer value 0 here in order to
    -- get out the proxies for the inner-most bindings; this is "safe"
    -- because these proxies should never depend on the names
    -- themselves
    let proxies2 :: RAssign Proxy c2
proxies2 = RAssign Proxy c1
-> (RAssign Name c1 -> Mb c2 b) -> RAssign Proxy c2
forall k k (ctx1 :: RList k) (ctx2 :: RList k) a.
RAssign Proxy ctx1
-> (RAssign Name ctx1 -> Mb ctx2 a) -> RAssign Proxy ctx2
freshFunctionProxies RAssign Proxy c1
proxies1 RAssign Name c1 -> Mb c2 b
f1 in
    RAssign Proxy (c1 :++: c2)
-> (RAssign Name (c1 :++: c2) -> b) -> Mb (c1 :++: c2) b
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun
    (RAssign Proxy c1 -> RAssign Proxy c2 -> RAssign Proxy (c1 :++: c2)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
append RAssign Proxy c1
proxies1 RAssign Proxy c2
proxies2)
    (\RAssign Name (c1 :++: c2)
ns ->
         let (RAssign Name c1
ns1, RAssign Name c2
ns2) = Proxy c1
-> RAssign Proxy c2
-> RAssign Name (c1 :++: c2)
-> (RAssign Name c1, RAssign Name c2)
forall k (c :: RList k) (c1 :: RList k) (c2 :: RList k)
       (prx :: RList k -> *) (any :: k -> *) (f :: k -> *).
(c ~ (c1 :++: c2)) =>
prx c1
-> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
split Proxy c1
forall k (t :: k). Proxy t
Proxy RAssign Proxy c2
proxies2 RAssign Name (c1 :++: c2)
ns in
         let (RAssign Proxy c2
_, RAssign Name c2 -> b
f2) = Mb c2 b -> (RAssign Proxy c2, RAssign Name c2 -> b)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun (RAssign Name c1 -> Mb c2 b
f1 RAssign Name c1
ns1) in
         RAssign Name c2 -> b
f2 RAssign Name c2
ns2)


{-|
  Separates a binding into two nested bindings. The first argument, of
  type @'RAssign' any c2@, is a \"phantom\" argument to indicate how
  the context @c@ should be split.
-}
mbSeparate :: forall k (ctx1 :: RList k) (ctx2 :: RList k) (any :: k -> *) a.
              RAssign any ctx2 -> Mb (ctx1 :++: ctx2) a ->
              Mb ctx1 (Mb ctx2 a)
mbSeparate :: RAssign any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a)
mbSeparate RAssign any ctx2
c2 (MkMbPair MbTypeRepr a
tRepr RAssign Name (ctx1 :++: ctx2)
ns a
a) =
    MbTypeRepr (Mb ctx2 a)
-> RAssign Name ctx1 -> Mb ctx2 a -> Mb ctx1 (Mb ctx2 a)
forall k (ctx :: RList k) b.
MbTypeRepr b -> RAssign Name ctx -> b -> Mb ctx b
MkMbPair (MbTypeRepr a -> MbTypeRepr (Mb ctx2 a)
forall k a (ctx :: RList k). MbTypeRepr a -> MbTypeRepr (Mb ctx a)
MbTypeReprMb MbTypeRepr a
tRepr) RAssign Name ctx1
ns1 (MbTypeRepr a -> RAssign Name ctx2 -> a -> Mb ctx2 a
forall k (ctx :: RList k) b.
MbTypeRepr b -> RAssign Name ctx -> b -> Mb ctx b
MkMbPair MbTypeRepr a
tRepr RAssign Name ctx2
ns2 a
a) where
        (RAssign Name ctx1
ns1, RAssign Name ctx2
ns2) = Proxy ctx1
-> RAssign any ctx2
-> RAssign Name (ctx1 :++: ctx2)
-> (RAssign Name ctx1, RAssign Name ctx2)
forall k (c :: RList k) (c1 :: RList k) (c2 :: RList k)
       (prx :: RList k -> *) (any :: k -> *) (f :: k -> *).
(c ~ (c1 :++: c2)) =>
prx c1
-> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
split Proxy ctx1
forall k (t :: k). Proxy t
Proxy RAssign any ctx2
c2 RAssign Name (ctx1 :++: ctx2)
ns
mbSeparate RAssign any ctx2
c2 (MkMbFun RAssign Proxy (ctx1 :++: ctx2)
proxies RAssign Name (ctx1 :++: ctx2) -> a
f) =
    RAssign Proxy ctx1
-> (RAssign Name ctx1 -> Mb ctx2 a) -> Mb ctx1 (Mb ctx2 a)
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun RAssign Proxy ctx1
proxies1 (\RAssign Name ctx1
ns1 -> RAssign Proxy ctx2 -> (RAssign Name ctx2 -> a) -> Mb ctx2 a
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun RAssign Proxy ctx2
proxies2 (\RAssign Name ctx2
ns2 -> RAssign Name (ctx1 :++: ctx2) -> a
f (RAssign Name ctx1
-> RAssign Name ctx2 -> RAssign Name (ctx1 :++: ctx2)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
append RAssign Name ctx1
ns1 RAssign Name ctx2
ns2)))
        where
          (RAssign Proxy ctx1
proxies1, RAssign Proxy ctx2
proxies2) = Proxy ctx1
-> RAssign any ctx2
-> RAssign Proxy (ctx1 :++: ctx2)
-> (RAssign Proxy ctx1, RAssign Proxy ctx2)
forall k (c :: RList k) (c1 :: RList k) (c2 :: RList k)
       (prx :: RList k -> *) (any :: k -> *) (f :: k -> *).
(c ~ (c1 :++: c2)) =>
prx c1
-> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
split Proxy ctx1
forall k (t :: k). Proxy t
Proxy RAssign any ctx2
c2 RAssign Proxy (ctx1 :++: ctx2)
proxies


-- | Returns a proxy object that enumerates all the types in ctx.
mbToProxy :: forall k (ctx :: RList k) (a :: *) .
             Mb ctx a -> RAssign Proxy ctx
mbToProxy :: Mb ctx a -> RAssign Proxy ctx
mbToProxy (MkMbFun RAssign Proxy ctx
proxies RAssign Name ctx -> a
_) = RAssign Proxy ctx
proxies
mbToProxy (MkMbPair MbTypeRepr a
_ RAssign Name ctx
ns a
_) = (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


{-|
  Take a multi-binding inside another multi-binding and move the
  outer binding inside the ineer one.
-}
mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
mbSwap (Mb ctx1 (Mb ctx2 a)
-> (RAssign Proxy ctx1, RAssign Name ctx1 -> Mb ctx2 a)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun -> (RAssign Proxy ctx1
proxies1, RAssign Name ctx1 -> Mb ctx2 a
f1)) =
    let proxies2 :: RAssign Proxy ctx2
proxies2 = RAssign Proxy ctx1
-> (RAssign Name ctx1 -> Mb ctx2 a) -> RAssign Proxy ctx2
forall k k (ctx1 :: RList k) (ctx2 :: RList k) a.
RAssign Proxy ctx1
-> (RAssign Name ctx1 -> Mb ctx2 a) -> RAssign Proxy ctx2
freshFunctionProxies RAssign Proxy ctx1
proxies1 RAssign Name ctx1 -> Mb ctx2 a
f1 in
    RAssign Proxy ctx2
-> (RAssign Name ctx2 -> Mb ctx1 a) -> Mb ctx2 (Mb ctx1 a)
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun RAssign Proxy ctx2
proxies2
      (\RAssign Name ctx2
ns2 ->
         RAssign Proxy ctx1 -> (RAssign Name ctx1 -> a) -> Mb ctx1 a
forall k (ctx :: RList k) b.
RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
MkMbFun RAssign Proxy ctx1
proxies1
         (\RAssign Name ctx1
ns1 ->
            (RAssign Proxy ctx2, RAssign Name ctx2 -> a)
-> RAssign Name ctx2 -> a
forall a b. (a, b) -> b
snd (Mb ctx2 a -> (RAssign Proxy ctx2, RAssign Name ctx2 -> a)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun (RAssign Name ctx1 -> Mb ctx2 a
f1 RAssign Name ctx1
ns1)) RAssign Name ctx2
ns2))

-- | Put a value inside a multi-binding
mbPure :: RAssign f ctx -> a -> Mb ctx a
mbPure :: RAssign f ctx -> a -> Mb ctx a
mbPure RAssign f ctx
prxs = RAssign f ctx -> (RAssign Name ctx -> a) -> Mb ctx a
forall k (f :: k -> *) (ctx :: RList k) b.
RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti RAssign f ctx
prxs ((RAssign Name ctx -> a) -> Mb ctx a)
-> (a -> RAssign Name ctx -> a) -> a -> Mb ctx a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> RAssign Name ctx -> a
forall a b. a -> b -> a
const

{-|
  Applies a function in a multi-binding to an argument in a
  multi-binding that binds the same number and types of names.
-}
mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply (Mb ctx (a -> b) -> (RAssign Proxy ctx, RAssign Name ctx -> a -> b)
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 -> b
f_fun)) (Mb ctx 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
_, RAssign Name ctx -> a
f_arg)) =
  RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
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 -> RAssign Name ctx -> a -> b
f_fun RAssign Name ctx
ns (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ RAssign Name ctx -> a
f_arg RAssign Name ctx
ns)


-- | Lift a binary function function to `Mb`s
mbMap2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c
mbMap2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c
mbMap2 a -> b -> c
f Mb ctx a
mb1 Mb ctx b
mb2 = (a -> b -> c) -> Mb ctx a -> Mb ctx (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b -> c
f Mb ctx a
mb1 Mb ctx (b -> c) -> Mb ctx b -> Mb ctx c
forall k (ctx :: RList k) a b.
Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
`mbApply` Mb ctx b
mb2

-------------------------------------------------------------------------------
-- Functor and Applicative instances
-------------------------------------------------------------------------------

instance Functor (Mb ctx) where
    fmap :: (a -> b) -> Mb ctx a -> Mb ctx b
fmap a -> b
f Mb ctx a
mbArg =
        Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
forall k (ctx :: RList k) a b.
Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply (RAssign Proxy ctx
-> (RAssign Name ctx -> a -> b) -> Mb ctx (a -> b)
forall k (f :: k -> *) (ctx :: RList k) b.
RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti (Mb ctx a -> RAssign Proxy ctx
forall k (ctx :: RList k) a. Mb ctx a -> RAssign Proxy ctx
mbToProxy Mb ctx a
mbArg) (\RAssign Name ctx
_ -> a -> b
f)) Mb ctx a
mbArg

instance TypeCtx ctx => Applicative (Mb ctx) where
    pure :: a -> Mb ctx a
pure a
x = RAssign Proxy ctx -> (RAssign Name ctx -> a) -> Mb ctx a
forall k (f :: k -> *) (ctx :: RList k) b.
RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b
nuMulti RAssign Proxy ctx
forall k (ctx :: RList k). TypeCtx ctx => RAssign Proxy ctx
typeCtxProxies (a -> RAssign Name ctx -> a
forall a b. a -> b -> a
const a
x)
    <*> :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
(<*>) = Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
forall k (ctx :: RList k) a b.
Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply


-------------------------------------------------------------------------------
-- Eliminators for multi-bindings
-------------------------------------------------------------------------------

-- FIXME: add more examples!!
{-|

  asdfasdf

  The expression @nuWithElimMulti args f@ takes a sequence @args@ of one or more
  multi-bindings (it is a runtime error to pass an empty sequence of arguments),
  each of type @Mb ctx ai@ for the same type context @ctx@ of bound names, and a
  function @f@ and does the following:

  * Creates a multi-binding that binds names @n1,...,nn@, one name for
    each type in @ctx@;

  * Substitutes the names @n1,...,nn@ for the names bound by each
    argument in the @args@ sequence, yielding the bodies of the @args@
    (using the new name @n@); and then

  * Passes the sequence @n1,...,nn@ along with the result of
    substituting into @args@ to the function @f@, which then returns
    the value for the newly created binding.

  For example, here is an alternate way to implement 'mbApply':

> mbApply' :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
> mbApply' f a =
>     nuWithElimMulti ('MNil' :>: f :>: a)
>                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')
-}
nuMultiWithElim :: (RAssign Name ctx -> RAssign Identity args -> b) ->
                   RAssign (Mb ctx) args -> Mb ctx b
nuMultiWithElim :: (RAssign Name ctx -> RAssign Identity args -> b)
-> RAssign (Mb ctx) args -> Mb ctx b
nuMultiWithElim RAssign Name ctx -> RAssign Identity args -> b
f RAssign (Mb ctx) args
args =
  let proxies :: RAssign Proxy ctx
proxies =
        case RAssign (Mb ctx) args
args of
          RAssign (Mb ctx) args
MNil -> String -> RAssign Proxy ctx
forall a. HasCallStack => String -> a
error String
"nuMultiWithElim"
          (RAssign (Mb ctx) c
_ :>: Mb ctx a
arg1) -> Mb ctx a -> RAssign Proxy ctx
forall k (ctx :: RList k) a. Mb ctx a -> RAssign Proxy ctx
mbToProxy Mb ctx a
arg1 in
  RAssign Proxy ctx -> (RAssign Name ctx -> b) -> Mb ctx b
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 ->
            RAssign Name ctx -> RAssign Identity args -> b
f RAssign Name ctx
ns (RAssign Identity args -> b) -> RAssign Identity args -> b
forall a b. (a -> b) -> a -> b
$ (forall x. Mb ctx x -> Identity x)
-> RAssign (Mb ctx) args -> RAssign Identity args
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
mapRAssign (\Mb ctx x
arg ->
                                x -> Identity x
forall a. a -> Identity a
Identity (x -> Identity x) -> x -> Identity x
forall a b. (a -> b) -> a -> b
$ (RAssign Proxy ctx, RAssign Name ctx -> x) -> RAssign Name ctx -> x
forall a b. (a, b) -> b
snd (Mb ctx x -> (RAssign Proxy ctx, RAssign Name ctx -> x)
forall k (ctx :: RList k) a.
Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)
ensureFreshFun Mb ctx x
arg) RAssign Name ctx
ns) RAssign (Mb ctx) args
args)


{-|
  Similar to 'nuMultiWithElim' but binds only one name. Note that the argument
  list here is allowed to be empty.
-}
nuWithElim :: (Name a -> RAssign Identity args -> b) ->
              RAssign (Mb (RNil :> a)) args ->
              Binding a b
nuWithElim :: (Name a -> RAssign Identity args -> b)
-> RAssign (Mb ('RNil ':> a)) args -> Binding a b
nuWithElim Name a -> RAssign Identity args -> b
f RAssign (Mb ('RNil ':> a)) args
MNil = (Name a -> b) -> Binding a b
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu ((Name a -> b) -> Binding a b) -> (Name a -> b) -> Binding a b
forall a b. (a -> b) -> a -> b
$ \Name a
n -> Name a -> RAssign Identity args -> b
f Name a
n RAssign Identity args
forall k (f :: k -> *). RAssign f 'RNil
MNil
nuWithElim Name a -> RAssign Identity args -> b
f RAssign (Mb ('RNil ':> a)) args
args =
    (RAssign Name ('RNil ':> a) -> RAssign Identity args -> b)
-> RAssign (Mb ('RNil ':> a)) args -> Binding a b
forall k (ctx :: RList k) (args :: RList *) b.
(RAssign Name ctx -> RAssign Identity args -> b)
-> RAssign (Mb ctx) args -> Mb ctx b
nuMultiWithElim (\(RAssign Name c
MNil :>: Name a
n) -> Name a -> RAssign Identity args -> b
f Name a
Name a
n) RAssign (Mb ('RNil ':> a)) args
args


{-|
  Similar to 'nuMultiWithElim' but takes only one argument
-}
nuMultiWithElim1 :: (RAssign Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b
nuMultiWithElim1 :: (RAssign Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b
nuMultiWithElim1 RAssign Name ctx -> arg -> b
f Mb ctx arg
arg =
    (RAssign Name ctx -> RAssign Identity ('RNil ':> arg) -> b)
-> RAssign (Mb ctx) ('RNil ':> arg) -> Mb ctx b
forall k (ctx :: RList k) (args :: RList *) b.
(RAssign Name ctx -> RAssign Identity args -> b)
-> RAssign (Mb ctx) args -> Mb ctx b
nuMultiWithElim (\RAssign Name ctx
names (RAssign Identity c
MNil :>: Identity a
arg) -> RAssign Name ctx -> arg -> b
f RAssign Name ctx
names arg
a
arg)
    (RAssign (Mb ctx) 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign (Mb ctx) 'RNil
-> Mb ctx arg -> RAssign (Mb ctx) ('RNil ':> arg)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Mb ctx arg
arg)


{-|
  Similar to 'nuMultiWithElim' but takes only one argument that binds
  a single name.
-}
nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
nuWithElim1 Name a -> arg -> b
f Binding a arg
arg =
  (Name a -> RAssign Identity ('RNil ':> arg) -> b)
-> RAssign (Mb ('RNil ':> a)) ('RNil ':> arg) -> Binding a b
forall k (a :: k) (args :: RList *) b.
(Name a -> RAssign Identity args -> b)
-> RAssign (Mb ('RNil ':> a)) args -> Binding a b
nuWithElim (\Name a
n (RAssign Identity c
MNil :>: Identity a
arg) -> Name a -> arg -> b
f Name a
n arg
a
arg) (RAssign (Mb ('RNil ':> a)) 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign (Mb ('RNil ':> a)) 'RNil
-> Binding a arg -> RAssign (Mb ('RNil ':> a)) ('RNil ':> arg)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Binding a arg
arg)