{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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 tuple functions
module Predicate.Data.Tuple (

 -- ** arrows
    Dup
  , First
  , Second
  , type (&&&)
  , type (***)
  , Both
  , On

 -- ** flat tuples
  , Tuple
  , Tuple'
  , Pairs

 -- ** boolean
  , AndA
  , type (&*)
  , OrA
  , type (|+)

 -- ** inductive tuples
  , EachITuple
  , ToITuple
  , ReverseITuple
  , ToITupleList

 ) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Proxy (Proxy(Proxy))
import GHC.TypeNats (Nat, KnownNat)
import qualified GHC.TypeLits as GL
import Control.Lens
import Data.Kind (Type)

-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> :set -XTypeOperators
-- >>> :set -XOverloadedStrings
-- >>> :set -XNoOverloadedLists
-- >>> import Predicate.Prelude
-- >>> import qualified Data.Semigroup as SG
-- >>> :m + Data.Ratio

-- | duplicate a value into a tuple
--
-- >>> pl @Dup 4
-- Present (4,4) ('(4,4))
-- Val (4,4)
--
-- >>> pl @(Dup >> Id) 4
-- Present (4,4) ((>>) (4,4) | {Id (4,4)})
-- Val (4,4)
--
-- >>> pl @(Dup << Fst * Snd) (4,5)
-- Present (20,20) ((>>) (20,20) | {'(20,20)})
-- Val (20,20)
--
-- >>> pl @(Fst * Snd >> Dup) (4,5)
-- Present (20,20) ((>>) (20,20) | {'(20,20)})
-- Val (20,20)
--
data Dup deriving Show
type DupT = W '(Id, Id)

instance Show x => P Dup x where
  type PP Dup x = PP DupT x
  eval _ = eval (Proxy @DupT)

-- | creates a list of overlapping pairs of elements. requires two or more elements
--
-- >>> pz @Pairs [1,2,3,4]
-- Val [(1,2),(2,3),(3,4)]
--
-- >>> pz @Pairs []
-- Val []
--
-- >>> pz @Pairs [1]
-- Val []
--
-- >>> pl @Pairs [1,2]
-- Present [(1,2)] (Pairs [(1,2)] | [1,2])
-- Val [(1,2)]
--
-- >>> pl @Pairs [1,2,3]
-- Present [(1,2),(2,3)] (Pairs [(1,2),(2,3)] | [1,2,3])
-- Val [(1,2),(2,3)]
--
-- >>> pl @Pairs [1,2,3,4]
-- Present [(1,2),(2,3),(3,4)] (Pairs [(1,2),(2,3),(3,4)] | [1,2,3,4])
-- Val [(1,2),(2,3),(3,4)]
--
-- >>> pan @(Pairs >> Len >> 'True >> 'False >> FailT _ "xyzzy") "abcde"
-- [Error xyzzy] False
-- |
-- +- P Pairs [('a','b'),('b','c'),('c','d'),('d','e')]
-- |
-- +- P Len 4
-- |
-- +- True 'True
-- |
-- +- False 'False
-- |
-- `- [Error xyzzy]
-- Fail "xyzzy"
--
data Pairs deriving Show
instance ([a] ~ x, Show a) => P Pairs x where
  type PP Pairs x = [(ExtractAFromTA x,ExtractAFromTA x)]
  eval _ opts as =
    let zs = case as of
               [] -> []
               _:bs -> zip as bs
    in pure $ mkNode opts (Val zs) (show3 opts "Pairs" zs as) []

-- | similar to 'Control.Arrow.&&&'
--
-- >>> pl @(Min &&& Max >> Id >> Fst < Snd) [10,4,2,12,14]
-- True ((>>) True | {2 < 14})
-- Val True
--
-- >>> pl @((123 &&& Id) >> Fst + Snd) 4
-- Present 127 ((>>) 127 | {123 + 4 = 127})
-- Val 127
--
-- >>> pl @(4 &&& "sadf" &&& 'LT) ()
-- Present (4,("sadf",LT)) ('(4,("sadf",LT)))
-- Val (4,("sadf",LT))
--
-- >>> pl @(Id &&& '() &&& ()) (Just 10)
-- Present (Just 10,((),())) ('(Just 10,((),())))
-- Val (Just 10,((),()))
--
-- >>> pl @(Fst &&& Snd &&& Thd &&& ()) (1,'x',True)
-- Present (1,('x',(True,()))) ('(1,('x',(True,()))))
-- Val (1,('x',(True,())))
--
-- >>> pl @(Fst &&& Snd &&& Thd &&& ()) (1,'x',True)
-- Present (1,('x',(True,()))) ('(1,('x',(True,()))))
-- Val (1,('x',(True,())))
--
-- >>> pl @(Fst &&& Snd &&& Thd &&& ()) (1,1.4,"aaa")
-- Present (1,(1.4,("aaa",()))) ('(1,(1.4,("aaa",()))))
-- Val (1,(1.4,("aaa",())))
--
data p &&& q deriving Show
infixr 3 &&&
type WAmpT p q = W '(p, q)

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

-- | similar to 'Control.Arrow.***'
--
-- >>> pz @(Pred *** ShowP Id) (13, True)
-- Val (12,"True")
--
-- >>> pl @(FlipT (***) Len (Id * 12)) (99,"cdef")
-- Present (1188,4) ((***) (1188,4) | (99,"cdef"))
-- Val (1188,4)
--
-- >>> pl @(4 *** "sadf" *** 'LT) ('x',("abv",[1]))
-- Present (4,("sadf",LT)) ((***) (4,("sadf",LT)) | ('x',("abv",[1])))
-- Val (4,("sadf",LT))
--
data p *** q deriving Show
infixr 3 ***

instance ( Show (PP p a)
         , Show (PP q b)
         , P p a
         , P q b
         , Show a
         , Show b
         ) => P (p *** q) (a,b) where
  type PP (p *** q) (a,b) = (PP p a, PP q b)
  eval _ opts (a,b) = do
    let msg0 = "(***)"
    pp <- eval (Proxy @p) opts a
    case getValueLR NoInline opts msg0 pp [] of
      Left e -> pure e
      Right a1 -> do
        qq <- eval (Proxy @q) opts b
        pure $ case getValueLR NoInline opts msg0 qq [hh pp] of
          Left e -> e
          Right b1 -> mkNode opts (Val (a1,b1)) (msg0 <> " " <> showL opts (a1,b1) <> showVerbose opts " | " (a,b)) [hh pp, hh qq]

-- | applies a function against the first part of a tuple: similar to 'Control.Arrow.first'
--
-- >>> pz @(First Succ) (12,True)
-- Val (13,True)
--
data First p deriving Show
type FirstT p = p *** Id

instance P (FirstT p) x => P (First p) x where
  type PP (First p) x = PP (FirstT p) x
  eval _ = eval (Proxy @(FirstT p))

-- | applies a function against the second part of a tuple: similar to 'Control.Arrow.second'
--
-- >>> pz @(Second Succ) (12,False)
-- Val (12,True)
--
data Second q deriving Show
type SecondT q = Id *** q

instance P (SecondT q) x => P (Second q) x where
  type PP (Second q) x = PP (SecondT q) x
  eval _ = eval (Proxy @(SecondT q))

-- | applies @p@ to lhs of the tuple and @q@ to the rhs and then @ands@ them together: see '&*'
--
-- >>> pl @(AndA (Gt 3) (Lt 10) Id) (1,2)
-- False (False (&*) True | (1 > 3))
-- Val False
--
data AndA p q r deriving Show
instance ( PP r x ~ (a,b)
         , PP p a ~ Bool
         , PP q b ~ Bool
         , P p a
         , P q b
         , P r x
         ) => P (AndA p q r) x where
  type PP (AndA p q r) x = Bool
  eval _ opts x = do
    let msg0 = "(&*)"
    rr <- eval (Proxy @r) opts x
    case getValueLR NoInline opts msg0 rr [] of
      Left e -> pure e
      Right (r1,r2) -> do
        pp <- evalBool (Proxy @p) opts r1
        case getValueLR NoInline opts msg0 pp [hh rr] of
          Left e -> pure e
          Right p -> do
            qq <- evalBool (Proxy @q) opts r2
            pure $ case getValueLR NoInline opts msg0 qq [hh rr, hh pp] of
              Left e -> e
              Right q ->
                let zz = case (p,q) of
                          (True, True) -> ""
                          (False, True) -> topMessage pp
                          (True, False) -> topMessage qq
                          (False, False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
                in mkNodeB opts (p&&q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> nullIf " | " zz) [hh rr, hh pp, hh qq]

-- | applies @p@ to lhs of the tuple and @q@ to the rhs and then @Ands@ them together
--
-- >>> pl @(SplitAt 4 "abcdefg" >> Len > 4 &* Len < 5) ()
-- False ((>>) False | {False (&*) True | (4 > 4)})
-- Val False
--
data p &* q deriving Show
type AndAT p q = AndA p q Id
infixr 3 &*

instance P (AndAT p q) x => P (p &* q) x where
  type PP (p &* q) x = PP (AndAT p q) x
  eval _ = evalBool (Proxy @(AndAT p q))

-- | applies @p@ to lhs of the tuple and @q@ to the rhs and then @ors@ them together: see '|+'
--
-- >>> pl @(OrA (Gt 3) (Lt 10) Id) (1,2)
-- True (False (|+) True)
-- Val True
--
data OrA p q r deriving Show
instance ( PP r x ~ (a,b)
         , PP p a ~ Bool
         , PP q b ~ Bool
         , P p a
         , P q b
         , P r x
         ) => P (OrA p q r) x where
  type PP (OrA p q r) x = Bool
  eval _ opts x = do
    let msg0 = "(|+)"
    rr <- eval (Proxy @r) opts x
    case getValueLR NoInline opts msg0 rr [] of
      Left e -> pure e
      Right (r1,r2) -> do
        pp <- evalBool (Proxy @p) opts r1
        case getValueLR NoInline opts msg0 pp [hh rr] of
          Left e -> pure e
          Right p -> do
            qq <- evalBool (Proxy @q) opts r2
            pure $ case getValueLR NoInline opts msg0 qq [hh rr, hh pp] of
              Left e -> e
              Right q ->
                let zz = case (p,q) of
                          (False,False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
                          _ -> ""
                in mkNodeB opts (p||q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> nullIf " | " zz) [hh rr, hh pp, hh qq]

-- | applies @p@ to lhs of the tuple and @q@ to the rhs and then @Ors@ them together
--
-- >>> pl @(Sum > 44 |+ Id < 2) ([5,6,7,8,14,44],9)
-- True (True (|+) False)
-- Val True
--
-- >>> pl @(Sum > 44 |+ Id < 2) ([5,6,7,14],9)
-- False (False (|+) False | (32 > 44) (|+) (9 < 2))
-- Val False
--
-- >>> pl @(Sum > 44 |+ Id < 2) ([5,6,7,14],1)
-- True (False (|+) True)
-- Val True
--
data p |+ q deriving Show
type OrAT p q = OrA p q Id
infixr 3 |+

instance P (OrAT p q) x => P (p |+ q) x where
  type PP (p |+ q) x = PP (OrAT p q) x
  eval _ = evalBool (Proxy @(OrAT p q))

-- | applies @p@ to the first and second slot of an n-tuple (similar to '***')
--
-- >>> pl @(Fst >> Both Len) (("abc",[10..17]),True)
-- Present (3,8) ((>>) (3,8) | {Both})
-- Val (3,8)
--
-- >>> pl @(Lift (Both Pred) Fst) ((12,'z'),True)
-- Present (11,'y') ((>>) (11,'y') | {Both})
-- Val (11,'y')
--
-- >>> pl @(Both Succ) (4,'a')
-- Present (5,'b') (Both)
-- Val (5,'b')
--
-- >>> import Data.Time
-- >>> pl @(Both (ReadP Day Id)) ("1999-01-01","2001-02-12")
-- Present (1999-01-01,2001-02-12) (Both)
-- Val (1999-01-01,2001-02-12)
--
-- >>> pz @(Both (Id * Id) >> ((Fst + Snd) ** (DivI Double 1 2))) (3,4)
-- Val 5.0
--
data Both p deriving Show
instance ( P p a
         , P p a'
   ) => P (Both p) (a,a') where
  type PP (Both p) (a,a') = (PP p a, PP p a')
  eval _ opts (a,a') = do
    let msg0 = "Both"
    pp <- eval (Proxy @p) opts a
    case getValueLR NoInline opts msg0 pp [] of
      Left e -> pure e
      Right b -> do
        pp' <- eval (Proxy @p) opts a'
        pure $ case getValueLR NoInline opts msg0 pp' [hh pp] of
          Left e -> e
          Right b' ->
            mkNode opts (Val (b,b')) msg0 [hh pp, hh pp']

-- | similar to 'Data.Function.on': may require kind signatures: Both is a better choice
--
-- >>> pz @('(4,2) >> On (**) (FromIntegral _)) ()
-- Val 16.0
--
-- >>> pz @('(4,2) >> Both (FromIntegral _) >> Fst ** Snd) () -- equivalent to the above but easier on ghc
-- Val 16.0
--
-- >>> pz @(On (+) (Id * Id) >> Id ** (1 % 2 >> FromRational _)) (3,4)
-- Val 5.0
--
-- >>> pz @(Both (Id * Id) >> ((Fst + Snd) ** (1 % 2 >> FromRational _))) (3,4) -- equivalent to the above but easier on ghc
-- Val 5.0
--

data On (p :: Type -> Type -> k2) q deriving Show

instance ( P q a
         , P q a'
         , P (p Fst Snd) (PP q a, PP q a')
   ) => P (On p q) (a,a') where
  type PP (On p q) (a,a') = PP (p Fst Snd) (PP q a, PP q a')
  eval _ opts (a,a') = do
    let msg0 = "On"
    qq <- eval (Proxy @q) opts a
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right b -> do
        qq' <- eval (Proxy @q) opts a'
        case getValueLR NoInline opts msg0 qq' [hh qq] of
          Left e -> pure e
          Right b' -> do
            pp <- eval (Proxy @(p Fst Snd)) opts (b,b')
            pure $ case getValueLR NoInline opts msg0 pp [hh qq, hh qq'] of
              Left e -> e
              Right p -> mkNode opts (Val p) msg0 [hh qq, hh qq', hh pp]

-- | create a @n@ tuple from a list or fail
--
-- >>> pz @(Tuple 4) "abcdefg"
-- Val ('a','b','c','d')
--
-- >>> pz @(Tuple 4) "abc"
-- Fail "Tuple(4) not enough elements(3)"
--
-- >>> pz @(Fst >> Tuple 3) ([1..5],True)
-- Val (1,2,3)
--
-- >>> pz @(Lift (Tuple 3) Fst) ([1..5],True)
-- Val (1,2,3)
--
data Tuple (n :: Nat) deriving Show

instance ( KnownNat n
         , FailWhenT (n GL.<=? 1)
                  ('GL.Text "Tuple:n cannot be less than two but found n="
                   'GL.:<>: 'GL.ShowType n)
         , TupleC n a
         , x ~ [a]
         , Show a
         ) => P (Tuple n) x where
  type PP (Tuple n) x = TupleT n (ExtractAFromList x)
  eval _ opts as =
    let msg0 = "Tuple(" ++ show n ++ ")"
        n = nat @n @Int
    in pure $ case getTupleC @n as of
         Left es -> mkNode opts (Fail (msg0 <> " not enough elements(" <> show (length as) <> ")")) (showVerbose opts " | " es) []
         Right r -> mkNode opts (Val r) msg0 []

-- | create a @n@ tuple from a list and return as an Either
--
-- >>> pz @(Tuple' 4) "abcdefg"
-- Val (Right ('a','b','c','d'))
--
-- >>> pz @(Tuple' 4) "abc"
-- Val (Left "abc")
--
-- >>> pz @(Tuple' 4) []
-- Val (Left [])
--
-- >>> pl @(Tuple' 4) "abc"
-- Present Left "abc" (Tuple'(4) not enough elements(3))
-- Val (Left "abc")
--
-- >>> :set -XPolyKinds
-- >>> type F n i = ChunksOf' n i Id >> Map (Tuple' n) >> PartitionEithers
-- >>> pz @(F 3 1) [1..7]
-- Val ([[6,7],[7]],[(1,2,3),(2,3,4),(3,4,5),(4,5,6),(5,6,7)])
--
data Tuple' (n :: Nat) deriving Show

instance ( KnownNat n
         , FailWhenT (n GL.<=? 1)
                  ('GL.Text "Tuple':n cannot be less than two but found n="
                   'GL.:<>: 'GL.ShowType n)
         , TupleC n a
         , x ~ [a]
         ) => P (Tuple' n) x where
  type PP (Tuple' n) x = Either x (TupleT n (ExtractAFromList x))
  eval _ opts as =
    let msg0 = "Tuple'(" ++ show n ++ ")"
        n = nat @n @Int
        lr = getTupleC @n as
    in pure $ case lr of
         Left e -> mkNode opts (Val (Left e)) (msg0 <> " not enough elements(" <> show (length as) <> ")") []
         Right ret -> mkNode opts (Val (Right ret)) msg0 []

-- | run @p@ with inductive tuples
--
-- >>> pz @(EachITuple Succ) (False,(2,(LT,('c',()))))
-- Val (True,(3,(EQ,('d',()))))
--
-- >>> pz @(EachITuple (Id + (4 >> FromIntegral _))) (1,(1/4,(5%6,())))
-- Val (5 % 1,(17 % 4,(29 % 6,())))
--
-- >>> pz @(ToITuple >> EachITuple (Id + (4 >> FromIntegral _))) (1000,1/4,5%6)
-- Val (1004 % 1,(17 % 4,(29 % 6,())))
--
-- >>> pz @(ToITuple >> EachITuple ((Id >> FromIntegral _) + (4 >> FromIntegral _))) (1000::Integer,17::Int)
-- Val (1004,(21,()))
--
-- >>> pz @(ToITuple >> EachITuple (Dup >> Fst<>Snd)) (SG.Min 1,SG.First 'x',"abcd")
-- Val (Min {getMin = 1},(First {getFirst = 'x'},("abcdabcd",())))
--
data EachITuple p deriving Show

instance ( P p b
         , P (EachITuple p) bs
         ) => P (EachITuple p) (b,bs) where
  type PP (EachITuple p) (b,bs) = (PP p b, PP (EachITuple p) bs)
  eval _ opts (b,bs) = do
    let msg0 = "EachITuple"
    pp <- eval (Proxy @p) opts b
    case getValueLR NoInline opts msg0 pp [] of
      Left e -> pure e
      Right p -> do
        qq <- eval (Proxy @(EachITuple p)) opts bs
        pure $ case getValueLR NoInline opts msg0 qq [] of
          Left e -> e
          Right q ->
            qq & ttVal .~ Val (p,q)
               & ttForest %~ (hh pp:)

instance P (EachITuple p) () where
  type PP (EachITuple p) () = ()
  eval _ opts () = do
    let msg0 = "EachITuple"
    pure $ mkNode opts (Val ()) msg0 []

-- | create inductive tuples from flat tuples
--
-- >>> pz @(ToITuple >> EachITuple Succ) (1,2,False,'x')
-- Val (2,(3,(True,('y',()))))
--
data ToITuple deriving Show

instance ToITupleC x => P ToITuple x where
  type PP ToITuple x = ToITupleP x
  eval _ opts x = do
    let msg0 = "ToITuple"
    pure $ mkNode opts (Val (toITupleC x)) msg0 []

-- | reverse an inductive tuple
--
-- >>> pz @ReverseITuple (1.4,(1,(2,(False,('x',())))))
-- Val ('x',(False,(2,(1,(1.4,())))))
--
data ReverseITuple deriving Show

instance P ReverseITuple () where
  type PP ReverseITuple () = ()
  eval _ opts () = do
    let msg0 = "ReverseITuple"
    pure $ mkNode opts (Val ()) msg0 []

instance ReverseITupleC x xs () => P ReverseITuple (x,xs) where
  type PP ReverseITuple (x,xs) = ReverseITupleT x xs ()
  eval _ opts (x,xs) = do
    let msg0 = "ReverseITuple"
    pure $ mkNode opts (Val (reverseITupleC x xs ())) msg0 []

-- | create inductive tuples from a list of the exact size @n@
--
-- >>> pz @(ToITupleList 4 >> EachITuple Succ) ['a','c','y','B']
-- Val ('b',('d',('z',('C',()))))
--
-- >>> pz @(ToITupleList 4) ['a','c','y','B']
-- Val ('a',('c',('y',('B',()))))
--
-- >>> pz @(Take 10 Id >> ToITupleList 10) ['a'..'z']
-- Val ('a',('b',('c',('d',('e',('f',('g',('h',('i',('j',()))))))))))
--
data ToITupleList (n :: Nat) deriving Show

instance ( KnownNat n
         , FailWhenT (n GL.<=? 0)
                  ('GL.Text "ToITupleList:n cannot be 0")
         , ToITupleListC n a
         , xs ~ [a]
         ) => P (ToITupleList n) xs where
  type PP (ToITupleList n) xs = ToITupleListP n (ExtractAFromTA xs)
  eval _ opts xs =
    let msg0 = "ToITupleList(" <> show n <> ")"
        n = nat @n @Int
    in pure $ case toITupleListC @n @a xs of
         Left e -> mkNode opts (Fail e) (msg0 <> " instead found " <> show (length xs)) []
         Right d -> mkNode opts (Val d) msg0 []