{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, OverlappingInstances #-} -- | -- 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, emptyMb, nuMulti, -- * Operations on multi-bindings elimEmptyMb, combineMb, separateMb, mbToProxy, -- * Queries on names cmpName, mbCmpName, mbNameBoundP, -- * type classes for lifting data out of bindings Liftable(..), Liftable1(..), Liftable2(..), -- * Optimized, safe multi-binding eliminators mbList ) where import Data.Type.List import qualified Data.Type.List.Proof.Member as Mem import qualified Data.Type.List.Proof.Append as App import Data.Binding.Hobbits.Internal import qualified Data.Binding.Hobbits.Internal as I import Data.List (elemIndex) import Unsafe.Coerce (unsafeCoerce) ------------------------------------------------------------------------------- -- bindings ------------------------------------------------------------------------------- -- | A @Binding@ is simply a multi-binding that binds one name type Binding a = Mb (Nil :> a) instance Show (Name a) where showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#' -- note: we reverse l to show the inner-most bindings last instance Show a => Show (Mb c a) where showsPrec p (MkMb l b) = showParen (p > 10) $ showChar '#' . shows (reverse l) . showChar '.' . shows b -- README: we pass f to fresh_name to avoid let-floating the results -- of fresh_name (which would always give the same name for each nu) -- README: is *is* ok to do CSE on multiple copies of nu, because -- the programmer cannot tell if two distinct (non-nested) nus get the -- same fresh integer, and two nus that look the same to the CSE engine -- cannot be nested -- README: it *is* ok to inline nu because we don't care in -- what order fresh names are created {-| @nu f@ creates a binding which binds a fresh name @n@ and whose body is the result of @f n@. -} nu :: (Name a -> b) -> Binding a b nu f = let n = fresh_name f in n `seq` MkMb [n] (f (MkName n)) -- README: inner-most bindings come FIRST -- | Combines a binding inside another binding into a single binding. combineMb :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b combineMb (MkMb l1 (MkMb l2 b)) = MkMb (l2 ++ l1) b {-| Separates a binding into two nested bindings. The first argument, of type @'Append' c1 c2 c@, is a \"phantom\" argument to indicate how the context @c@ should be split. -} separateMb :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a) separateMb app (MkMb l a) = MkMb d (MkMb t a) where (d, t) = splitAt (App.length app) l -- | Returns a proxy object that enumerates all the types in ctx. mbToProxy :: Mb ctx a -> MapC Proxy ctx mbToProxy (MkMb l _) = unsafeProxyFromLen (length l) -- | Creates an empty binding that binds 0 names. emptyMb :: a -> Mb Nil a emptyMb t = MkMb [] t {-| 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 @'Mb' 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 :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b nuMulti Nil f = emptyMb $ f Nil nuMulti (proxies :> proxy) f = combineMb $ nuMulti proxies $ \names -> nu $ \n -> f (names :> n) {-| Eliminates an empty binding, returning its body. Note that @elimEmptyMb@ is the inverse of @emptyMb@. -} elimEmptyMb :: Mb Nil a -> a elimEmptyMb (MkMb [] t) = t elimEmptyMb _ = error "Should not happen! (elimEmptyMb)" {-| @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 (MkName n1) (MkName n2) | n1 == n2 = Just $ unsafeCoerce Refl | otherwise = Nothing {-| 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 :: Mb ctx (Name a) -> Either (Member ctx a) (Name a) mbNameBoundP (MkMb names (MkName n)) = 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 :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :=: b) mbCmpName b1 b2 = case (mbNameBoundP b1, mbNameBoundP b2) of (Left mem1, Left mem2) -> Mem.same mem1 mem2 (Right n1, Right n2) -> cmpName n1 n2 _ -> Nothing {-| The class @Liftable a@ gives a \"lifting function\" for a, which can take any data of type @a@ out of a multi-binding of type @'Mb' ctx a@. -} class Liftable a where mbLift :: Mb ctx a -> a instance Liftable Int where mbLift (MkMb _ i) = i instance Liftable Char where mbLift (MkMb _ c) = c {- instance Liftable a => Liftable [a] where mbLift (MkMb _ []) = [] mbLift (MkMb names (x : xs)) = (mbLift (MkMb names x)) : (mbLift (MkMb names xs)) -} instance Liftable (Member c a) where mbLift (MkMb _ mem) = mem {-| The class @Liftable1 f@ gives a lifting function for each type @f a@ when @a@ itself is @Liftable@. -} class Liftable1 f where mbLift1 :: Liftable a => Mb ctx (f a) -> f a instance (Liftable1 f, Liftable a) => Liftable (f a) where mbLift = mbLift1 {-| The class @Liftable2 f@ gives a lifting function for each type @f a b@ when @a@ and @b@ are @Liftable@. -} class Liftable2 f where mbLift2 :: (Liftable a, Liftable b) => Mb ctx (f a b) -> f a b instance (Liftable2 f, Liftable a) => Liftable1 (f a) where mbLift1 = mbLift2 -- | Lift a list (but not its elements) out of a multi-binding mbList :: Mb c [a] -> [Mb c a] mbList (MkMb names []) = [] mbList (MkMb names (x : xs)) = (MkMb names x) : (mbList (MkMb names xs))