{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Prelude.Const
-- Copyright   :  (C) 2018 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Exports the promoted and singled versions of the 'Const' data type.
--
-----------------------------------------------------------------------------

module Data.Singletons.Prelude.Const (
  -- * The 'Const' singleton
  Sing, SConst(..), GetConst, sGetConst,

  -- * Defunctionalization symbols
  ConstSym0, ConstSym1,
  GetConstSym0, GetConstSym1
  ) where

import Control.Applicative
import Data.Kind (Type)
import Data.Singletons.Internal
import Data.Singletons.Prelude.Base
  hiding ( Const, ConstSym0, ConstSym1
         , Foldr, FoldrSym0, sFoldr )
import Data.Singletons.Prelude.Enum
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Foldable
import Data.Singletons.Prelude.Instances hiding (FoldlSym0, sFoldl)
import Data.Singletons.Prelude.Monad.Internal
import Data.Singletons.Prelude.Monoid
import Data.Singletons.Prelude.Num
import Data.Singletons.Prelude.Ord
import Data.Singletons.Prelude.Semigroup.Internal
import Data.Singletons.Prelude.Show
import Data.Singletons.Promote
import Data.Singletons.Single

{-
Const's argument `b` is poly-kinded, and as a result, we have a choice as to
what singleton type to give it. We could use either

1. type SConst :: forall {k :: Type} (a :: Type) (b :: k).    Const a b -> Type
2. type SConst :: forall             (a :: Type) (b :: Type). Const a b -> Type

Option (1) is the more permissive one, so we opt for that. However, singletons'
TH machinery does not jive with this option, since the SingKind instance it
tries to generate:

  instance (SingKind a, SingKind b) => SingKind (Const a b) where
    type Demote (Const a b) = Const (Demote a) (Demote b)

Assumes that `b` is of kind Type. Until we get a more reliable story for
poly-kinded Sing instances (see #150), we simply write the singleton type by
hand.
-}
type SConst :: Const a b -> Type
data SConst c where
  SConst :: Sing a -> SConst ('Const a)
type instance Sing = SConst
instance SingKind a => SingKind (Const a b) where
  type Demote (Const a b) = Const (Demote a) b
  fromSing :: Sing a -> Demote (Const a b)
fromSing (SConst sa) = Demote a -> Const (Demote a) b
forall k a (b :: k). a -> Const a b
Const (Sing a -> Demote a
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sa)
  toSing :: Demote (Const a b) -> SomeSing (Const a b)
toSing (Const a) = Demote a
-> (forall (a :: a). Sing a -> SomeSing (Const a b))
-> SomeSing (Const a b)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote a
a ((forall (a :: a). Sing a -> SomeSing (Const a b))
 -> SomeSing (Const a b))
-> (forall (a :: a). Sing a -> SomeSing (Const a b))
-> SomeSing (Const a b)
forall a b. (a -> b) -> a -> b
$ SConst ('Const a) -> SomeSing (Const a b)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SConst ('Const a) -> SomeSing (Const a b))
-> (Sing a -> SConst ('Const a)) -> Sing a -> SomeSing (Const a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> SConst ('Const a)
forall a k (b :: k) (a :: a). Sing a -> SConst ('Const a)
SConst
instance SingI a => SingI ('Const a) where
  sing :: Sing ('Const a)
sing = Sing a -> SConst ('Const a)
forall a k (b :: k) (a :: a). Sing a -> SConst ('Const a)
SConst Sing a
forall k (a :: k). SingI a => Sing a
sing

$(genDefunSymbols [''Const])
instance SingI ConstSym0 where
  sing :: Sing ConstSym0
sing = SingFunction1 ConstSym0 -> Sing ConstSym0
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 ConstSym0
forall a k (b :: k) (a :: a). Sing a -> SConst ('Const a)
SConst

$(singletonsOnly [d|
  getConst :: Const a b -> a
  getConst (Const x) = x

  deriving instance Bounded a => Bounded (Const a b)
  deriving instance Eq      a => Eq      (Const a b)
  deriving instance Ord     a => Ord     (Const a b)

  -- deriving instance Enum a => Enum (Const a b)
  instance Enum a => Enum (Const a b) where
    succ (Const x)     = Const (succ x)
    pred (Const x)     = Const (pred x)
    toEnum i           = Const (toEnum i)
    fromEnum (Const x) = fromEnum x
    enumFromTo (Const x) (Const y) = map Const (enumFromTo x y)
    enumFromThenTo (Const x) (Const y) (Const z) =
        map Const (enumFromThenTo x y z)

  -- deriving instance Monoid a => Monoid (Const a b)
  instance Monoid a => Monoid (Const a b) where
    mempty = Const mempty

  -- deriving instance Num a => Num (Const a b)
  instance Num a => Num (Const a b) where
    Const x + Const y = Const (x + y)
    Const x - Const y = Const (x - y)
    Const x * Const y = Const (x * y)
    negate (Const x)  = Const (negate x)
    abs    (Const x)  = Const (abs    x)
    signum (Const x)  = Const (signum x)
    fromInteger n     = Const (fromInteger n)

  -- deriving instance Semigroup a => Semigroup (Const a b)
  instance Semigroup a => Semigroup (Const a b) where
    Const x <> Const y = Const (x <> y)

  -- -| This instance would be equivalent to the derived instances of the
  -- 'Const' newtype if the 'runConst' field were removed
  instance Show a => Show (Const a b) where
      showsPrec d (Const x) = showParen (d > 10) $
                              showString "Const " . showsPrec 11 x

  deriving instance Functor (Const m)
  deriving instance Foldable (Const m)

  instance Monoid m => Applicative (Const m) where
      pure _ = Const mempty
      liftA2 _ (Const x) (Const y) = Const (x `mappend` y)
      Const x <*> Const y = Const (x `mappend` y)
  |])