{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, OverlappingInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}

-- |
-- Module      : Data.Binding.Hobbits.Mb
-- Copyright   : (c) 2014 Edwin Westbrook
--
-- License     : BSD3
--
-- Maintainer  : emw4@rice.edu
-- Stability   : experimental
-- Portability : GHC
--
-- This module defines the type-class Liftable for lifting
-- non-binding-related data out of name-bindings. Note that this code
-- is not "trusted", i.e., it is not part of the name-binding
-- abstraction: instead, it is all written using the primitives
-- exported by the Mb

module Data.Binding.Hobbits.Liftable where

import Data.Type.List.Proof.Member
import Data.Binding.Hobbits.Mb
import Data.Binding.Hobbits.QQ


{-|
  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 = mbLiftInt

instance Liftable Integer where
    mbLift = mbLiftInteger

instance Liftable Char where
    mbLift = mbLiftChar

-- README: this requires overlapping instances, because it clashes
-- with Liftable2, but this instance is better because it does not
-- require c nor a to be liftable
instance Liftable (Member c a) where
    mbLift [nuP| Member_Base |] = Member_Base
    mbLift [nuP| Member_Step m |] = Member_Step (mbLift m)

{-|
  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

instance Liftable1 [] where
    mbLift1 [nuP| [] |] = []
    mbLift1 [nuP| x : xs |] = (mbLift x) : (mbLift1 xs)

{-|
  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 (,) where
    mbLift2 [nuP| (x,y) |] = (mbLift x, mbLift y)

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 [nuP| [] |] = []
mbList [nuP| x : xs |] = x : mbList xs