{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
-- | promoted enum functions
module Predicate.Data.Enum (

  -- ** constructors
    type (...)
  , EnumFromTo
  , EnumFromThenTo
  , FromEnum
  , FromEnum'
  , Universe
  , Universe'

  -- ** bounded enums
  , SuccB
  , SuccB'
  , PredB
  , PredB'
  , ToEnumBDef
  , ToEnumBDef'
  , ToEnumBFail

  -- ** unsafe enums
  , Succ
  , SuccN
  , Pred
  , ToEnum
  , ToEnum'

 ) where
import Predicate.Core
import Predicate.Util
import Safe (succMay, predMay, toEnumMay)
import Data.Proxy (Proxy(..))
import Data.Kind (Type)
import Data.Tree (Tree)
-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> :set -XTypeOperators
-- >>> :set -XOverloadedStrings
-- >>> import qualified Data.Text as T
-- >>> import Predicate.Prelude
-- >>> import qualified Data.Semigroup as SG
-- >>> import Data.Time

-- | bounded 'succ' function
--
-- >>> pz @(SuccB 'LT Id) GT
-- Val LT
--
-- >>> pz @(SuccB 'LT 'GT) ()
-- Val LT
--
-- >>> pz @(SuccB 'GT 'LT) ()
-- Val EQ
--
-- >>> pl @(SuccB 'LT Id) GT
-- Present LT (SuccB out of range)
-- Val LT
--
data SuccB p q deriving Show

instance ( PP q x ~ a
         , P q x
         , P p (Proxy a)
         , PP p (Proxy a) ~ a
         , Show a
         , Eq a
         , Bounded a
         , Enum a
         ) => P (SuccB p q) x where
  type PP (SuccB p q) x = PP q x
  eval _ opts x = do
    let msg0 = "SuccB"
    qq <- eval (Proxy @q) opts x
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right q ->
        case succMay q of
          Nothing -> _enumDefault @p @a opts msg0 (hh qq)
          Just n -> pure $ mkNode opts (Val n) (show3 opts msg0 n q) [hh qq]

_enumDefault :: forall p a m
  . ( MonadEval m
    , P p (Proxy a)
    , PP p (Proxy a) ~ a
    )
  => POpts
  -> String
  -> Tree PE
  -> m (TT a)
_enumDefault opts msg0 hhqq = do
   let msg1 = msg0 <> " out of range"
   pp <- eval (Proxy @p) opts (Proxy @a)
   pure $ case getValueLR NoInline opts msg1 pp [hhqq] of
     Left e -> e
     Right _ -> mkNodeCopy opts pp msg1 [hhqq, hh pp]

-- | bounded 'succ' function
--
-- >>> pz @(SuccB' Id) GT
-- Fail "Succ bounded"
--
-- >>> pz @(SuccB' Id) (13 :: Int)
-- Val 14
--
-- >>> pz @(SuccB' Id) LT
-- Val EQ
--
data SuccB' q deriving Show
type SuccBT' q = SuccB (FailP "Succ bounded") q

instance P (SuccBT' q) x => P (SuccB' q) x where
  type PP (SuccB' q) x = PP (SuccBT' q) x
  eval _ = eval (Proxy @(SuccBT' q))

-- | bounded 'pred' function
--
-- >>> pz @(PredB' Id) (13 :: Int)
-- Val 12
--
-- >>> pz @(PredB' Id) LT
-- Fail "Pred bounded"
--
-- >>> pl @(PredB' Id) GT
-- Present EQ (PredB EQ | GT)
-- Val EQ
--
-- >>> pl @(PredB' Id) LT
-- Error Pred bounded (PredB out of range)
-- Fail "Pred bounded"
--

data PredB' q deriving Show
type PredBT' q = PredB (FailP "Pred bounded") q

instance ( PP q x ~ a
         , P q x
         , P p (Proxy a)
         , PP p (Proxy a) ~ a
         , Show a
         , Eq a
         , Bounded a
         , Enum a
         ) => P (PredB p q) x where
  type PP (PredB p q) x = PP q x
  eval _ opts x = do
    let msg0 = "PredB"
    qq <- eval (Proxy @q) opts x
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right q ->
        case predMay q of
          Nothing -> _enumDefault @p @a opts msg0 (hh qq)
          Just n -> pure $ mkNode opts (Val n) (show3 opts msg0 n q) [hh qq]


-- | unbounded 'succ' function
--
-- >>> pz @Succ 13
-- Val 14
--
-- >>> pz @Succ LT
-- Val EQ
--
-- >>> pz @Succ GT
-- Fail "Succ IO e=Prelude.Enum.Ordering.succ: bad argument"
--
-- >>> pl @Succ 10
-- Present 11 (Succ 11 | 10)
-- Val 11
--
-- >>> pl @Succ True -- captures the exception
-- Error Succ IO e=Prelude.Enum.Bool.succ: bad argument (True)
-- Fail "Succ IO e=Prelude.Enum.Bool.succ: bad argument"
--
-- >>> pz @Succ (Proxy @44)
-- Fail "Succ IO e=Proxy.succ"
--
data Succ deriving Show
{-
>print $! (succ Proxy)
*** Exception: Proxy.succ
-}
instance ( Show x
         , Enum x
         ) => P Succ x where
  type PP Succ x = x
  eval _ opts x = do
    let msg0 = "Succ"
    lr <- catchit (succ x)
    pure $ case lr of
      Left e -> mkNode opts (Fail (msg0 <> " " <> e)) (showL opts x) []
      Right n -> mkNode opts (Val n) (show3 opts msg0 n x) []

-- | SuccN n p (unsafe) increments an enum p by the given integral n
--
-- >>> pz @(ReadP Day Id >> Id ... SuccN 5 Id) "2020-07-27"
-- Val [2020-07-27,2020-07-28,2020-07-29,2020-07-30,2020-07-31,2020-08-01]
--
-- >>> pz @(ReadP Day Id >> SuccN (Negate 5) Id) "2020-07-27"
-- Val 2020-07-22
--
-- >>> pl @(SuccN 3 'LT) ()
-- Error SuccN IO e=Prelude.Enum.Ordering.toEnum: bad argument (SuccN 3 LT)
-- Fail "SuccN IO e=Prelude.Enum.Ordering.toEnum: bad argument"
--
-- >>> pz @(SuccN 2 'LT) ()
-- Val GT
--
data SuccN n p deriving Show

instance ( Show a
         , Enum a
         , Integral (PP n x)
         , P n x
         , PP p x ~ a
         , P p x
         ) => P (SuccN n p) x where
  type PP (SuccN n p) x = PP p x
  eval _ opts x = do
    let msg0 = "SuccN"
    lr <- runPQ NoInline msg0 (Proxy @n) (Proxy @p) opts x []
    case lr of
      Left e -> pure e
      Right (fromIntegral -> n :: Int,p,nn,pp) -> do
        lr1 <- catchit (toEnum (fromEnum p + n))
        pure $ case lr1 of
          Left e -> mkNode opts (Fail (msg0 <> " " <> e)) (litL opts (msg0 <> " " <> show n <> " " <> show p)) [hh nn, hh pp]
          Right r -> mkNode opts (Val r) (litL opts (msg0 <> " " <> show n <> " " <> show p)) [hh nn, hh pp]


-- | unbounded 'pred' function
--
-- >>> pz @Pred 13
-- Val 12
--
-- >>> pz @Pred LT
-- Fail "Pred IO e=Prelude.Enum.Ordering.pred: bad argument"
--
data Pred deriving Show

instance ( Show x
         , Enum x
         ) => P Pred x where
  type PP Pred x = x
  eval _ opts x = do
    let msg0 = "Pred"
    lr <- catchit (pred x)
    pure $ case lr of
      Left e -> mkNode opts (Fail (msg0 <> " " <> e)) (showL opts x) []
      Right n -> mkNode opts (Val n) (show3 opts msg0 n x) []

-- | bounded 'pred' function
--
-- >>> pl @(PredB 'GT Id) LT
-- Present GT (PredB out of range)
-- Val GT
--
-- >>> pl @(PredB 'LT Id) GT
-- Present EQ (PredB EQ | GT)
-- Val EQ
--
data PredB p q deriving Show

instance P (PredBT' q) x => P (PredB' q) x where
  type PP (PredB' q) x = PP (PredBT' q) x
  eval _ = eval (Proxy @(PredBT' q))


-- | 'fromEnum' function
--
-- >>> pz @(FromEnum' Id) 'x'
-- Val 120
--
-- >>> pl @(FromEnum' ("aa" ==! Id) >> Same 1) "aaaa"
-- False ((>>) False | {0 == 1})
-- Val False
--
-- >>> pl @(FromEnum' ("aa" ==! Id) >> ToEnum OrderingP) "aaaa"
-- Present CGt ((>>) CGt | {ToEnum CGt | 0})
-- Val CGt
--
-- >>> pl @(Map (FromEnum' Id) >> Map (ToEnum Char)) "abcd"
-- Present "abcd" ((>>) "abcd" | {Map "abcd" | [97,98,99,100]})
-- Val "abcd"
--
data FromEnum' p deriving Show

instance ( Show a
         , Enum a
         , PP p x ~ a
         , P p x
         ) => P (FromEnum' p) x where
  type PP (FromEnum' p) x = Int
  eval _ opts x = do
    let msg0 = "FromEnum"
    pp <- eval (Proxy @p) opts x
    pure $ case getValueLR NoInline opts msg0 pp [] of
      Left e -> e
      Right p ->
        let n = fromEnum p
        in mkNode opts (Val n) (show3 opts msg0 n p) [hh pp]

-- | 'fromEnum' function
--
-- >>> pz @FromEnum 'x'
-- Val 120
--
data FromEnum deriving Show

instance ( Show x
         , Enum x
         ) => P FromEnum x where
  type PP FromEnum x = Int
  eval _ opts x =
    let msg0 = "FromEnum"
        n = fromEnum x
    in pure $ mkNode opts (Val n) (show3 opts msg0 n x) []


-- | unsafe 'toEnum' function that allows you to specify the target @p@ and a pointer to a type @t@
--
data ToEnum' t p deriving Show

instance ( PP p x ~ a
         , P p x
         , Show a
         , Enum (PP t x)
         , Show (PP t x)
         , Integral a
         ) => P (ToEnum' t p) x where
  type PP (ToEnum' t p) x = PP t x
  eval _ opts x = do
    let msg0 = "ToEnum"
    pp <- eval (Proxy @p) opts x
    case getValueLR NoInline opts msg0 pp [] of
      Left e -> pure e
      Right p -> do
        lr <- catchit (toEnum $! fromIntegral p)
        pure $ case lr of
          Left e -> mkNode opts (Fail (msg0 <> " " <> e)) (showL opts p) [hh pp]
          Right n -> mkNode opts (Val n) (show3 opts msg0 n p) [hh pp]

-- | unsafe 'toEnum' function
--
-- >>> pz @(ToEnum Char) 120
-- Val 'x'
--
-- >>> pl @(Map FromEnum >> Map (Id - 97 >> ToEnum Ordering)) "abcde"
-- Error ToEnum IO e=Prelude.Enum.Ordering.toEnum: bad argument(2) (Map(i=3, a=100) excnt=2)
-- Fail "ToEnum IO e=Prelude.Enum.Ordering.toEnum: bad argument(2)"
--
-- >>> pl @((ToEnum Day *** ToEnum Day) >> EnumFromTo Fst Snd) (0,5)
-- Present [1858-11-17,1858-11-18,1858-11-19,1858-11-20,1858-11-21,1858-11-22] ((>>) [1858-11-17,1858-11-18,1858-11-19,1858-11-20,1858-11-21,1858-11-22] | {1858-11-17 ... 1858-11-22})
-- Val [1858-11-17,1858-11-18,1858-11-19,1858-11-20,1858-11-21,1858-11-22]
--
-- >>> pz @(ToEnum (Proxy ())) 0
-- Val Proxy
--
-- >>> pz @(ToEnum (Proxy ())) 1
-- Fail "ToEnum IO e=Proxy.toEnum: 0 expected"
--
-- >>> pz @(ToEnum (Proxy "sss") >> Pop0 Id ()) 0
-- Val "sss"
--
data ToEnum (t :: Type) deriving Show
type ToEnumT (t :: Type) = ToEnum' (Hole t) Id

instance P (ToEnumT t) x => P (ToEnum t) x where
  type PP (ToEnum t) x = PP (ToEnumT t) x
  eval _ = eval (Proxy @(ToEnumT t))

data ToEnumBDef' t def deriving Show

instance ( P def (Proxy (PP t a))
         , PP def (Proxy (PP t a)) ~ PP t a
         , Show a
         , Show (PP t a)
         , Bounded (PP t a)
         , Enum (PP t a)
         , Integral a
         ) => P (ToEnumBDef' t def) a where
  type PP (ToEnumBDef' t def) a = PP t a
  eval _ opts a = do
    let msg0 = "ToEnumBDef"
    case toEnumMay $ fromIntegral a of
      Nothing -> do
         let msg1 = msg0 <> " out of range"
         pp <- eval (Proxy @def) opts (Proxy @(PP t a))
         pure $ case getValueLR NoInline opts msg1 pp [] of
           Left e -> e
           Right _ -> mkNodeCopy opts pp msg1 [hh pp]
      Just n -> pure $ mkNode opts (Val n) (show3 opts msg0 n a) []

-- | bounded 'toEnum' function
--
-- >>> pz @(ToEnumBDef Ordering LT) 2
-- Val GT
--
-- >>> pz @(ToEnumBDef Ordering LT) 6
-- Val LT
--
-- >>> pl @(ToEnumBDef Ordering 'LT) 123
-- Present LT (ToEnumBDef out of range)
-- Val LT
--
-- >>> pl @(ToEnumBDef Ordering 'GT) 1
-- Present EQ (ToEnumBDef EQ | 1)
-- Val EQ
--
data ToEnumBDef (t :: Type) def deriving Show
type ToEnumBDefT (t :: Type) def = ToEnumBDef' (Hole t) def

instance P (ToEnumBDefT t def) x => P (ToEnumBDef t def) x where
  type PP (ToEnumBDef t def) x = PP (ToEnumBDefT t def) x
  eval _ = eval (Proxy @(ToEnumBDefT t def))

-- | bounded 'toEnum' function
--
-- >>> pz @(ToEnumBFail Ordering) 6
-- Fail "ToEnum bounded"
--
-- >>> pl @(ToEnumBFail Ordering) 1
-- Present EQ (ToEnumBDef EQ | 1)
-- Val EQ
--
-- >>> pl @(ToEnumBFail Ordering) 44
-- Error ToEnum bounded (ToEnumBDef out of range)
-- Fail "ToEnum bounded"
--
data ToEnumBFail (t :: Type) deriving Show
type ToEnumBFailT (t :: Type) = ToEnumBDef' (Hole t) (FailP "ToEnum bounded")

instance P (ToEnumBFailT t) x => P (ToEnumBFail t) x where
  type PP (ToEnumBFail t) x = PP (ToEnumBFailT t) x
  eval _ = eval (Proxy @(ToEnumBFailT t))

-- | similar to 'enumFromTo'
--
-- >>> pz @(EnumFromTo 'GT 'LT) ()
-- Val []
--
-- >>> pz @(EnumFromTo Pred Succ) (SG.Max 10)
-- Val [Max {getMax = 9},Max {getMax = 10},Max {getMax = 11}]
--
-- >>> pz @(EnumFromTo 1 20 >> Map '(Id, (If (Id `Mod` 3 == 0) "Fizz" "" <> If (Id `Mod` 5 == 0) "Buzz" ""))) 123
-- Val [(1,""),(2,""),(3,"Fizz"),(4,""),(5,"Buzz"),(6,"Fizz"),(7,""),(8,""),(9,"Fizz"),(10,"Buzz"),(11,""),(12,"Fizz"),(13,""),(14,""),(15,"FizzBuzz"),(16,""),(17,""),(18,"Fizz"),(19,""),(20,"Buzz")]
--
-- >>> pl @(EnumFromTo (Pure SG.Min 9) (Pure _ 13)) ()
-- Present [Min {getMin = 9},Min {getMin = 10},Min {getMin = 11},Min {getMin = 12},Min {getMin = 13}] (Min {getMin = 9} ... Min {getMin = 13})
-- Val [Min {getMin = 9},Min {getMin = 10},Min {getMin = 11},Min {getMin = 12},Min {getMin = 13}]
--
-- >>> pl @(EnumFromTo (Wrap (SG.Min _) 9) (Wrap _ 13)) ()
-- Present [Min {getMin = 9},Min {getMin = 10},Min {getMin = 11},Min {getMin = 12},Min {getMin = 13}] (Min {getMin = 9} ... Min {getMin = 13})
-- Val [Min {getMin = 9},Min {getMin = 10},Min {getMin = 11},Min {getMin = 12},Min {getMin = 13}]
--
data EnumFromTo p q deriving Show

-- | similar to 'enumFromTo'
--
-- >>> pz @(2 ... 5) ()
-- Val [2,3,4,5]
--
-- >>> pz @('LT ... 'GT) ()
-- Val [LT,EQ,GT]
--
-- >>> pz @('Just (MkDay '(2020, 1, 2)) ... 'Just (MkDay '(2020, 1, 7))) ()
-- Val [2020-01-02,2020-01-03,2020-01-04,2020-01-05,2020-01-06,2020-01-07]
--
data p ... q deriving Show
infix 7 ...

type EnumFromToT p q = EnumFromTo p q

instance P (EnumFromToT p q) x => P (p ... q) x where
  type PP (p ... q) x = PP (EnumFromToT p q) x
  eval _ = eval (Proxy @(EnumFromToT p q))

instance ( P p x
         , P q x
         , PP p x ~ a
         , Show a
         , PP q x ~ a
         , Enum a
         ) => P (EnumFromTo p q) x where
  type PP (EnumFromTo p q) x = [PP p x]
  eval _ opts z = do
    let msg0 = "..."
    lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts z []
    pure $ case lr of
      Left e -> e
      Right (p,q,pp,qq) -> mkNode opts (Val (enumFromTo p q)) (showL opts p <> " " <> msg0 <> " " <> showL opts q) [hh pp, hh qq]

-- | similar to 'enumFromThenTo'
--
-- >>> pz @(EnumFromThenTo (10 >> ToEnum Day) (20 >> ToEnum Day) (70 >> ToEnum Day)) ()
-- Val [1858-11-27,1858-12-07,1858-12-17,1858-12-27,1859-01-06,1859-01-16,1859-01-26]
--
-- >>> pz @(EnumFromThenTo (ReadP Day "2020-01-12") (ReadP Day "2020-02-12") (ReadP Day "2020-08-12")) ()
-- Val [2020-01-12,2020-02-12,2020-03-14,2020-04-14,2020-05-15,2020-06-15,2020-07-16]
--
data EnumFromThenTo p q r deriving Show

instance ( P p x
         , P q x
         , P r x
         , PP p x ~ a
         , Show a
         , PP q x ~ a
         , PP r x ~ a
         , Enum a
         ) => P (EnumFromThenTo p q r) x where
  type PP (EnumFromThenTo p q r) x = [PP p x]
  eval _ opts z = do
    let msg0 = "EnumFromThenTo"
    lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts z []
    case lr of
      Left e -> pure e
      Right (p,q,pp,qq) -> do
        rr <- eval (Proxy @r) opts z
        pure $ case getValueLR NoInline opts (msg0 ++ " r failed") rr [hh pp, hh qq] of
          Left e -> e
          Right r ->
            mkNode opts (Val (enumFromThenTo p q r)) (msg0 <> " [" <> showL opts p <> ", " <> showL opts q <> " .. " <> showL opts r <> "]") [hh pp, hh qq, hh rr]

-- | universe of enum using the type pointed to by @p@
--
-- >>> pl @(Universe' Id) LT
-- Present [LT,EQ,GT] (Universe [LT .. GT])
-- Val [LT,EQ,GT]
--
data Universe' p deriving Show

instance ( PP p x ~ a
         , Show a
         , Enum a
         , Bounded a
         ) => P (Universe' p) x where
  type PP (Universe' p) x = [PP p x]
  eval _ opts _ =
    let msg0 = "Universe"
        u = [mn .. mx]
        mn = minBound @a
        mx = maxBound @a
    in pure $ mkNode opts (Val u) (msg0 <> " [" <> showL opts mn <> " .. " <> showL opts mx <> "]") []

-- | get universe of an enum of type @t@
--
-- >>> pz @(Universe Ordering) ()
-- Val [LT,EQ,GT]
--
data Universe (t :: Type) deriving Show
type UniverseT (t :: Type) = Universe' (Hole t)

instance P (UniverseT t) x => P (Universe t) x where
  type PP (Universe t) x = PP (UniverseT t) x
  eval _ = eval (Proxy @(UniverseT t))