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

-- |
-- 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.RList
import Data.Binding.Hobbits.Mb
import Data.Binding.Hobbits.Internal.Mb
import Data.Binding.Hobbits.QQ
import Data.Binding.Hobbits.Closed
import Data.Binding.Hobbits.NuMatching
import Data.Binding.Hobbits.NuMatchingInstances

import Data.Ratio
import Data.Proxy
import Numeric.Natural
import Data.Type.Equality


{-|
  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 NuMatching a => Liftable a where
    mbLift :: Mb ctx a -> a

-------------------------------------------------------------------------------
-- * Lifting instances that must be defined inside the library abstraction boundary
-------------------------------------------------------------------------------

instance Liftable Char where
    mbLift :: Mb ctx Char -> Char
mbLift (Mb ctx Char -> (RAssign Name ctx, Char)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name ctx
_, Char
c)) = Char
c

instance Liftable Int where
    mbLift :: Mb ctx Int -> Int
mbLift (Mb ctx Int -> (RAssign Name ctx, Int)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name ctx
_, Int
i)) = Int
i

instance Liftable Integer where
    mbLift :: Mb ctx Integer -> Integer
mbLift (Mb ctx Integer -> (RAssign Name ctx, Integer)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name ctx
_, Integer
i)) = Integer
i

instance Liftable (Closed a) where
    mbLift :: Mb ctx (Closed a) -> Closed a
mbLift (Mb ctx (Closed a) -> (RAssign Name ctx, Closed a)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name ctx
_, Closed a
c)) = Closed a
c

instance Liftable Natural where
    mbLift :: Mb ctx Natural -> Natural
mbLift (Mb ctx Natural -> (RAssign Name ctx, Natural)
forall k (ctx :: RList k) a. Mb ctx a -> (RAssign Name ctx, a)
ensureFreshPair -> (RAssign Name ctx
_, Natural
i)) = Natural
i


-------------------------------------------------------------------------------
-- * Lifting instances and related functions that could be defined outside the library
-------------------------------------------------------------------------------

-- 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 :: Mb ctx (Member c a) -> Member c a
mbLift Mb ctx (Member c a)
[nuP| Member_Base |] = Member c a
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
    mbLift Mb ctx (Member c a)
[nuP| Member_Step m |] = Member ctx a -> Member (ctx ':> b) a
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step (Mb ctx (Member ctx a) -> Member ctx a
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx (Member ctx a)
m)

-- | Lift a list (but not its elements) out of a multi-binding
mbList :: NuMatching a => Mb c [a] -> [Mb c a]
mbList :: Mb c [a] -> [Mb c a]
mbList Mb c [a]
[nuP| [] |] = []
mbList Mb c [a]
[nuP| x : xs |] = Mb c a
x Mb c a -> [Mb c a] -> [Mb c a]
forall a. a -> [a] -> [a]
: Mb c [a] -> [Mb c a]
forall k a (c :: RList k). NuMatching a => Mb c [a] -> [Mb c a]
mbList Mb c [a]
xs

instance (Integral a, NuMatching a) => NuMatching (Ratio a) where
  nuMatchingProof :: MbTypeRepr (Ratio a)
nuMatchingProof =
    (Ratio a -> (a, a)) -> ((a, a) -> Ratio a) -> MbTypeRepr (Ratio a)
forall b a. NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a
isoMbTypeRepr (\Ratio a
r -> (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
r, Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
r)) (\(a
n,a
d) -> a
na -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
%a
d)
instance (Integral a, Liftable a) => Liftable (Ratio a) where
  mbLift :: Mb ctx (Ratio a) -> Ratio a
mbLift Mb ctx (Ratio a)
mb_r =
    (\(a
n,a
d) -> a
na -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
%a
d) ((a, a) -> Ratio a) -> (a, a) -> Ratio a
forall a b. (a -> b) -> a -> b
$ Mb ctx (a, a) -> (a, a)
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift (Mb ctx (a, a) -> (a, a)) -> Mb ctx (a, a) -> (a, a)
forall a b. (a -> b) -> a -> b
$ (Ratio a -> (a, a)) -> Mb ctx (Ratio a) -> Mb ctx (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Ratio a
r -> (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
r, Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
r)) Mb ctx (Ratio a)
mb_r

instance Liftable a => Liftable [a] where
    mbLift :: Mb ctx [a] -> [a]
mbLift Mb ctx [a]
[nuP| [] |] = []
    mbLift Mb ctx [a]
[nuP| x : xs |] = (Mb ctx a -> a
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx a
x) a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (Mb ctx [a] -> [a]
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx [a]
xs)

instance Liftable () where
    mbLift :: Mb ctx () -> ()
mbLift Mb ctx ()
[nuP| () |] = ()

instance (Liftable a, Liftable b) => Liftable (a,b) where
    mbLift :: Mb ctx (a, b) -> (a, b)
mbLift Mb ctx (a, b)
[nuP| (x,y) |] = (Mb ctx a -> a
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx a
x, Mb ctx b -> b
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx b
y)

instance Liftable Bool where
  mbLift :: Mb ctx Bool -> Bool
mbLift Mb ctx Bool
[nuP| True |] = Bool
True
  mbLift Mb ctx Bool
[nuP| False |] = Bool
False

instance Liftable a => Liftable (Maybe a) where
  mbLift :: Mb ctx (Maybe a) -> Maybe a
mbLift Mb ctx (Maybe a)
[nuP| Nothing |] = Maybe a
forall a. Maybe a
Nothing
  mbLift Mb ctx (Maybe a)
[nuP| Just mb_a |] = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Mb ctx a -> a
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx a
mb_a

instance (Liftable a, Liftable b) => Liftable (Either a b) where
  mbLift :: Mb ctx (Either a b) -> Either a b
mbLift Mb ctx (Either a b)
[nuP| Left mb_a |] = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Mb ctx a -> a
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx a
mb_a
  mbLift Mb ctx (Either a b)
[nuP| Right mb_b |] = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Mb ctx b -> b
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb ctx b
mb_b

instance Liftable (a :~: b) where
  mbLift :: Mb ctx (a :~: b) -> a :~: b
mbLift Mb ctx (a :~: b)
[nuP| Refl |] = a :~: b
forall k (a :: k). a :~: a
Refl

instance Liftable (Proxy (a :: k)) where
  mbLift :: Mb ctx (Proxy a) -> Proxy a
mbLift Mb ctx (Proxy a)
[nuP| Proxy |] = Proxy a
forall k (t :: k). Proxy t
Proxy

-- Ideally this would be in the Mb module, but that ends up producing a circular
-- include due to needing `mbLift`
instance Eq a => Eq (Mb ctx a) where
  Mb ctx a
mb1 == :: Mb ctx a -> Mb ctx a -> Bool
== Mb ctx a
mb2 =
    Mb ctx Bool -> Bool
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift (Mb ctx Bool -> Bool) -> Mb ctx Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (RAssign Name ctx
 -> RAssign Identity (('RNil ':> a) ':> a) -> Bool)
-> RAssign (Mb ctx) (('RNil ':> a) ':> a) -> Mb ctx Bool
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
_ (RAssign Identity c
_ :>: Identity a
a1 :>: Identity a
a2) ->
                               Identity a
a1 Identity a -> Identity a -> Bool
forall a. Eq a => a -> a -> Bool
== Identity a
Identity a
a2) (RAssign (Mb ctx) 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign (Mb ctx) 'RNil
-> Mb ctx a -> RAssign (Mb ctx) ('RNil ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Mb ctx a
mb1 RAssign (Mb ctx) ('RNil ':> a)
-> Mb ctx a -> RAssign (Mb ctx) (('RNil ':> a) ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Mb ctx a
mb2)



-- README: these lead to overlapping instances...

{-

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

-}