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

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Prelude.Semigroup.Internal
-- Copyright   :  (C) 2018 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines the promoted version of 'Semigroup', 'PSemigroup'; the
-- singleton version, 'SSemigroup'; and some @newtype@ wrappers, all
-- of which are reexported from the "Data.Semigroup" module or
-- imported directly by some other modules.
--
-- This module exists to avoid import cycles with
-- "Data.Singletons.Prelude.Monoid".
--
----------------------------------------------------------------------------

module Data.Singletons.Prelude.Semigroup.Internal where

import Data.List.NonEmpty (NonEmpty(..))
import Data.Ord (Down(..))
import Data.Proxy
import Data.Semigroup (Dual(..), All(..), Any(..), Sum(..), Product(..), Option(..))
import Data.Singletons.Internal
import Data.Singletons.Prelude.Base
import Data.Singletons.Prelude.Bool
import Data.Singletons.Prelude.Enum
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Instances
import Data.Singletons.Prelude.Monad.Internal
import Data.Singletons.Prelude.Num
import Data.Singletons.Prelude.Ord hiding (MinSym0, MinSym1, MaxSym0, MaxSym1)
import Data.Singletons.Promote
import Data.Singletons.Single
import Data.Singletons.TypeLits.Internal
import Data.Singletons.Util
import qualified Data.Text as T
import Data.Void (Void)

import GHC.TypeLits (AppendSymbol, SomeSymbol(..), someSymbolVal)

import Unsafe.Coerce

$(singletonsOnly [d|
  -- -| The class of semigroups (types with an associative binary operation).
  --
  -- Instances should satisfy the associativity law:
  --
  --  * @x '<>' (y '<>' z) = (x '<>' y) '<>' z@
  class Semigroup a where
        -- -| An associative operation.
        (<>) :: a -> a -> a
        infixr 6 <>

        -- -| Reduce a non-empty list with @\<\>@
        --
        -- The default definition should be sufficient, but this can be
        -- overridden for efficiency.
        --
        sconcat :: NonEmpty a -> a
        sconcat (a :| as) = go a as where
          go :: a -> [a] -> a
          go b (c:cs) = b <> go c cs
          go b []     = b

        {-
        Can't single 'stimes', since there's no singled 'Integral' class.

        -- -| Repeat a value @n@ times.
        --
        -- Given that this works on a 'Semigroup' it is allowed to fail if
        -- you request 0 or fewer repetitions, and the default definition
        -- will do so.
        --
        -- By making this a member of the class, idempotent semigroups
        -- and monoids can upgrade this to execute in /O(1)/ by
        -- picking @stimes = 'stimesIdempotent'@ or @stimes =
        -- 'stimesIdempotentMonoid'@ respectively.
        stimes :: Integral b => b -> a -> a
        stimes = stimesDefault
        -}


  instance Semigroup [a] where
        (<>) = (++)

  instance Semigroup (NonEmpty a) where
        (a :| as) <> (b :| bs) = a :| (as ++ b : bs)

  instance Semigroup b => Semigroup (a -> b) where
        f <> g = \x -> f x <> g x

  instance Semigroup () where
        _ <> _      = ()
        sconcat _   = ()

  instance (Semigroup a, Semigroup b) => Semigroup (a, b) where
        (a,b) <> (a',b') = (a<>a',b<>b')

  instance (Semigroup a, Semigroup b, Semigroup c) => Semigroup (a, b, c) where
        (a,b,c) <> (a',b',c') = (a<>a',b<>b',c<>c')

  instance (Semigroup a, Semigroup b, Semigroup c, Semigroup d)
         => Semigroup (a, b, c, d) where
        (a,b,c,d) <> (a',b',c',d') = (a<>a',b<>b',c<>c',d<>d')

  instance (Semigroup a, Semigroup b, Semigroup c, Semigroup d, Semigroup e)
         => Semigroup (a, b, c, d, e) where
        (a,b,c,d,e) <> (a',b',c',d',e') = (a<>a',b<>b',c<>c',d<>d',e<>e')

  instance Semigroup Ordering where
    LT <> _ = LT
    EQ <> y = y
    GT <> _ = GT

  instance Semigroup a => Semigroup (Maybe a) where
    Nothing <> b       = b
    a       <> Nothing = a
    Just a  <> Just b  = Just (a <> b)

  instance Semigroup (Either a b) where
    Left _    <> b = b
    -- a      <> _ = a
    a@Right{} <> _ = a

  instance Semigroup Void where
    a <> _ = a

  -- deriving newtype instance Semigroup a => Semigroup (Down a)
  instance Semigroup a => Semigroup (Down a) where
    Down a <> Down b = Down (a <> b)
  |])

-- Workaround for #326
infixr 6 <>

$(genSingletons       $ ''Option : semigroupBasicTypes)
$(singBoundedInstances             semigroupBasicTypes)
$(singEqInstances     $ ''Option : semigroupBasicTypes)
$(singDecideInstances $ ''Option : semigroupBasicTypes)
$(singOrdInstances    $ ''Option : semigroupBasicTypes)

$(singletonsOnly [d|
  instance Applicative Dual where
    pure = Dual
    Dual f <*> Dual x = Dual (f x)

  deriving instance Functor Dual

  instance Monad Dual where
    Dual a >>= k = k a

  instance Semigroup a => Semigroup (Dual a) where
          Dual a <> Dual b = Dual (b <> a)

  instance Semigroup All where
          All a <> All b = All (a && b)

  instance Semigroup Any where
          Any a <> Any b = Any (a || b)

  instance Applicative Sum where
    pure = Sum
    Sum f <*> Sum x = Sum (f x)

  deriving instance Functor Sum

  instance Monad Sum where
    Sum a >>= k = k a

  instance Num a => Semigroup (Sum a) where
          Sum a <> Sum b = Sum (a + b)

  -- deriving newtype instance Num a => Num (Sum a)
  instance Num a => Num (Sum a) where
      Sum a + Sum b = Sum (a + b)
      Sum a - Sum b = Sum (a - b)
      Sum a * Sum b = Sum (a * b)
      negate (Sum a) = Sum (negate a)
      abs    (Sum a) = Sum (abs a)
      signum (Sum a) = Sum (signum a)
      fromInteger n  = Sum (fromInteger n)

  instance Applicative Product where
    pure = Product
    Product f <*> Product x = Product (f x)

  deriving instance Functor Product

  instance Monad Product where
    Product a >>= k = k a

  instance Num a => Semigroup (Product a) where
          Product a <> Product b = Product (a * b)

  -- deriving newtype instance Num a => Num (Product a)
  instance Num a => Num (Product a) where
      Product a + Product b = Product (a + b)
      Product a - Product b = Product (a - b)
      Product a * Product b = Product (a * b)
      negate (Product a) = Product (negate a)
      abs    (Product a) = Product (abs a)
      signum (Product a) = Product (signum a)
      fromInteger n      = Product (fromInteger n)
  |])

instance PSemigroup Symbol where
  type a <> b = AppendSymbol a b

instance SSemigroup Symbol where
  sa :: Sing t
sa %<> :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t)
%<> sb :: Sing t
sb =
    let a :: Demote Symbol
a  = Sing t -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
sa
        b :: Demote Symbol
b  = Sing t -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
sb
        ex :: SomeSymbol
ex = String -> SomeSymbol
someSymbolVal (String -> SomeSymbol) -> String -> SomeSymbol
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text
Demote Symbol
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
Demote Symbol
b
    in case SomeSymbol
ex of
         SomeSymbol (Proxy n
_ :: Proxy ab) -> SSymbol n -> SSymbol (AppendSymbol t t)
forall a b. a -> b
unsafeCoerce (Sing n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSym :: Sing ab)

-- We need these in Data.Singletons.Prelude.Semigroup, as we need to promote
-- code that simultaneously uses the Min/Max constructors and the min/max
-- functions, which have clashing defunctionalization symbol names. Our
-- workaround is to simply define synonyms for min/max and use those instead.
min_, max_ :: Ord a => a -> a -> a
min_ :: a -> a -> a
min_ = a -> a -> a
forall a. Ord a => a -> a -> a
min
max_ :: a -> a -> a
max_ = a -> a -> a
forall a. Ord a => a -> a -> a
max

type Min_ x y = Min x y
type Max_ x y = Max x y
$(genDefunSymbols [''Min_, ''Max_])

sMin_ :: forall a (x :: a) (y :: a). SOrd a => Sing x -> Sing y -> Sing (x `Min_` y)
sMin_ :: Sing x -> Sing y -> Sing (Min_ x y)
sMin_ = Sing x -> Sing y -> Sing (Min_ x y)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)
sMin

sMax_ :: forall a (x :: a) (y :: a). SOrd a => Sing x -> Sing y -> Sing (x `Max_` y)
sMax_ :: Sing x -> Sing y -> Sing (Max_ x y)
sMax_ = Sing x -> Sing y -> Sing (Max_ x y)
forall a (t :: a) (t :: a).
SOrd a =>
Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)
sMax

-- We need these in Data.Singletons.Prelude.Foldable.
all_ :: Bool -> All
all_ :: Bool -> All
all_ = Bool -> All
All

any_ :: Bool -> Any
any_ :: Bool -> Any
any_ = Bool -> Any
Any

sum_ :: a -> Sum a
sum_ :: a -> Sum a
sum_ = a -> Sum a
forall a. a -> Sum a
Sum

product_ :: a -> Product a
product_ :: a -> Product a
product_ = a -> Product a
forall a. a -> Product a
Product

type All_     a = 'All a
type Any_     a = 'Any a
type Sum_     a = 'Sum a
type Product_ a = 'Product a
$(genDefunSymbols [''All_, ''Any_, ''Sum_, ''Product_])

sAll_ :: forall (x :: Bool). Sing x -> Sing (All_ x)
sAll_ :: Sing x -> Sing (All_ x)
sAll_ = Sing x -> Sing (All_ x)
forall (n :: Bool). Sing n -> SAll ('All n)
SAll

sAny_ :: forall (x :: Bool). Sing x -> Sing (Any_ x)
sAny_ :: Sing x -> Sing (Any_ x)
sAny_ = Sing x -> Sing (Any_ x)
forall (n :: Bool). Sing n -> SAny ('Any n)
SAny

sSum_ :: forall a (x :: a). Sing x -> Sing (Sum_ x)
sSum_ :: Sing x -> Sing (Sum_ x)
sSum_ = Sing x -> Sing (Sum_ x)
forall a (n :: a). Sing n -> SSum ('Sum n)
SSum

sProduct_ :: forall a (x :: a). Sing x -> Sing (Product_ x)
sProduct_ :: Sing x -> Sing (Product_ x)
sProduct_ = Sing x -> Sing (Product_ x)
forall a (n :: a). Sing n -> SProduct ('Product n)
SProduct