{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Base.SomeSing
-- Copyright   :  (C) 2013 Richard Eisenberg
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Provides the 'SomeSing' data type along with instances of 'Eq', 'Ord', etc.,
-- which are defined as orphans due to 'SomeSing' originally being defined in
-- a separate library (@singletons@).
--
----------------------------------------------------------------------------
module Data.Singletons.Base.SomeSing (SomeSing(..)) where

import Data.Eq.Singletons
import Data.Monoid.Singletons
import Data.Ord.Singletons
import Data.Semigroup.Singletons
import Data.Singletons
import Data.Singletons.Base.Enum
import Data.Singletons.Base.Instances
import Data.Singletons.ShowSing
import Data.String
import Data.String.Singletons
import qualified Data.Text as T (pack)
import GHC.Num.Singletons

instance SEq k => Eq (SomeSing k) where
  SomeSing Sing a
a == :: SomeSing k -> SomeSing k -> Bool
== SomeSing Sing a
b = Sing (a == a) -> Demote Bool
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (==@#@$) a) a)
forall a (t :: a) (t :: a).
SEq a =>
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== Sing a
b)
  SomeSing Sing a
a /= :: SomeSing k -> SomeSing k -> Bool
/= SomeSing Sing a
b = Sing (a /= a) -> Demote Bool
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (/=@#@$) a) a)
forall a (t :: a) (t :: a).
SEq a =>
Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)
%/= Sing a
b)

instance SOrd k => Ord (SomeSing k) where
  SomeSing Sing a
a compare :: SomeSing k -> SomeSing k -> Ordering
`compare` SomeSing Sing a
b = Sing (Compare a a) -> Demote Ordering
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply CompareSym0 a) a)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
`sCompare` Sing a
b)
  SomeSing Sing a
a < :: SomeSing k -> SomeSing k -> Bool
<         SomeSing Sing a
b = Sing (a < a) -> Demote Bool
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (<@#@$) a) a)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)
%<  Sing a
b)
  SomeSing Sing a
a <= :: SomeSing k -> SomeSing k -> Bool
<=        SomeSing Sing a
b = Sing (a <= a) -> Demote Bool
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (<=@#@$) a) a)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)
%<= Sing a
b)
  SomeSing Sing a
a > :: SomeSing k -> SomeSing k -> Bool
>         SomeSing Sing a
b = Sing (a > a) -> Demote Bool
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (>@#@$) a) a)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)
%>  Sing a
b)
  SomeSing Sing a
a >= :: SomeSing k -> SomeSing k -> Bool
>=        SomeSing Sing a
b = Sing (a >= a) -> Demote Bool
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (>=@#@$) a) a)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)
%>= Sing a
b)

instance SBounded k => Bounded (SomeSing k) where
  minBound :: SomeSing k
minBound = Sing MinBound -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing MinBound
forall a. SBounded a => Sing MinBoundSym0
sMinBound
  maxBound :: SomeSing k
maxBound = Sing MaxBound -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing MaxBound
forall a. SBounded a => Sing MaxBoundSym0
sMaxBound

instance SEnum k => Enum (SomeSing k) where
  succ :: SomeSing k -> SomeSing k
succ (SomeSing Sing a
a) = Sing (Succ a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing (Apply SuccSym0 a)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply SuccSym0 t)
sSucc Sing a
a)
  pred :: SomeSing k -> SomeSing k
pred (SomeSing Sing a
a) = Sing (Pred a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing (Apply PredSym0 a)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply PredSym0 t)
sPred Sing a
a)
  toEnum :: Int -> SomeSing k
toEnum Int
n = Demote Natural
-> (forall (a :: Natural). Sing a -> SomeSing k) -> SomeSing k
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (Int -> Demote Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) (Sing (ToEnum a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing (ToEnum a) -> SomeSing k)
-> (Sing a -> Sing (ToEnum a)) -> Sing a -> SomeSing k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Sing (ToEnum a)
forall a (t :: Natural).
SEnum a =>
Sing t -> Sing (Apply ToEnumSym0 t)
sToEnum)
  fromEnum :: SomeSing k -> Int
fromEnum (SomeSing Sing a
a) = Demote Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Sing (FromEnum a) -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing a -> Sing (Apply FromEnumSym0 a)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply FromEnumSym0 t)
sFromEnum Sing a
a))
  enumFromTo :: SomeSing k -> SomeSing k -> [SomeSing k]
enumFromTo (SomeSing Sing a
from) (SomeSing Sing a
to) =
    SList (EnumFromTo a a) -> [SomeSing k]
forall a (x :: [a]). SList x -> [SomeSing a]
listFromSingShallow (Sing a -> Sing a -> Sing (Apply (Apply EnumFromToSym0 a) a)
forall a (t :: a) (t :: a).
SEnum a =>
Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t)
sEnumFromTo Sing a
from Sing a
to)
  enumFromThenTo :: SomeSing k -> SomeSing k -> SomeSing k -> [SomeSing k]
enumFromThenTo (SomeSing Sing a
from) (SomeSing Sing a
then_) (SomeSing Sing a
to) =
    SList (EnumFromThenTo a a a) -> [SomeSing k]
forall a (x :: [a]). SList x -> [SomeSing a]
listFromSingShallow (Sing a
-> Sing a
-> Sing a
-> Sing (Apply (Apply (Apply EnumFromThenToSym0 a) a) a)
forall a (t :: a) (t :: a) (t :: a).
SEnum a =>
Sing t
-> Sing t
-> Sing t
-> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t)
sEnumFromThenTo Sing a
from Sing a
then_ Sing a
to)

-- Like the 'fromSing' implementation for lists, but bottoms out at
-- 'SomeSing' instead of recursively invoking 'fromSing'.
listFromSingShallow :: SList (x :: [a]) -> [SomeSing a]
listFromSingShallow :: forall a (x :: [a]). SList x -> [SomeSing a]
listFromSingShallow SList x
SNil         = []
listFromSingShallow (SCons Sing n
x Sing n
xs) = Sing n -> SomeSing a
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing n
x SomeSing a -> [SomeSing a] -> [SomeSing a]
forall a. a -> [a] -> [a]
: SList n -> [SomeSing a]
forall a (x :: [a]). SList x -> [SomeSing a]
listFromSingShallow Sing n
SList n
xs

instance SNum k => Num (SomeSing k) where
  SomeSing Sing a
a + :: SomeSing k -> SomeSing k -> SomeSing k
+ SomeSing Sing a
b = Sing (a + a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (+@#@$) a) a)
forall a (t :: a) (t :: a).
SNum a =>
Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t)
%+ Sing a
b)
  SomeSing Sing a
a - :: SomeSing k -> SomeSing k -> SomeSing k
- SomeSing Sing a
b = Sing (a - a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (-@#@$) a) a)
forall a (t :: a) (t :: a).
SNum a =>
Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t)
%- Sing a
b)
  SomeSing Sing a
a * :: SomeSing k -> SomeSing k -> SomeSing k
* SomeSing Sing a
b = Sing (a * a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (*@#@$) a) a)
forall a (t :: a) (t :: a).
SNum a =>
Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t)
%* Sing a
b)
  negate :: SomeSing k -> SomeSing k
negate (SomeSing Sing a
a) = Sing (Negate a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing (Apply NegateSym0 a)
forall a (t :: a). SNum a => Sing t -> Sing (Apply NegateSym0 t)
sNegate Sing a
a)
  abs :: SomeSing k -> SomeSing k
abs    (SomeSing Sing a
a) = Sing (Abs a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing (Apply AbsSym0 a)
forall a (t :: a). SNum a => Sing t -> Sing (Apply AbsSym0 t)
sAbs Sing a
a)
  signum :: SomeSing k -> SomeSing k
signum (SomeSing Sing a
a) = Sing (Signum a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> Sing (Apply SignumSym0 a)
forall a (t :: a). SNum a => Sing t -> Sing (Apply SignumSym0 t)
sSignum Sing a
a)
  fromInteger :: Integer -> SomeSing k
fromInteger Integer
n = Demote Natural
-> (forall (a :: Natural). Sing a -> SomeSing k) -> SomeSing k
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (Integer -> Demote Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) (Sing (FromInteger a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing (FromInteger a) -> SomeSing k)
-> (Sing a -> Sing (FromInteger a)) -> Sing a -> SomeSing k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Sing (FromInteger a)
forall a (t :: Natural).
SNum a =>
Sing t -> Sing (Apply FromIntegerSym0 t)
sFromInteger)

deriving instance ShowSing k => Show (SomeSing k)

instance SSemigroup k => Semigroup (SomeSing k) where
  SomeSing Sing a
a <> :: SomeSing k -> SomeSing k -> SomeSing k
<> SomeSing Sing a
b = Sing (a <> a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a
a Sing a -> Sing a -> Sing (Apply (Apply (<>@#@$) a) a)
forall a (t :: a) (t :: a).
SSemigroup a =>
Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t)
%<> Sing a
b)

instance SMonoid k => Monoid (SomeSing k) where
  mempty :: SomeSing k
mempty = Sing Mempty -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing Mempty
forall a. SMonoid a => Sing MemptySym0
sMempty

instance SIsString k => IsString (SomeSing k) where
  fromString :: String -> SomeSing k
fromString String
s = Demote Symbol
-> (forall (a :: Symbol). Sing a -> SomeSing k) -> SomeSing k
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (String -> Text
T.pack String
s) (Sing (FromString a) -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing (FromString a) -> SomeSing k)
-> (SSymbol a -> Sing (FromString a)) -> SSymbol a -> SomeSing k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SSymbol a -> Sing (FromString a)
forall a (t :: Symbol).
SIsString a =>
Sing t -> Sing (Apply FromStringSym0 t)
sFromString)