{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Generics.Product.Internal.Positions
-- Copyright   :  (C) 2020 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Derive positional product type getters and setters generically.
--
-----------------------------------------------------------------------------

module Data.Generics.Product.Internal.Positions
  ( type (<?)
  , Size
  , CRep

  , Context
  , Context_
  , Context'
  , Context0
  , derived0
  , derived'
  ) where

import Data.Generics.Internal.Families.Has (Pos)
import Data.Kind      (Type, Constraint)
import Data.Type.Bool (If, Not, type (&&))
import GHC.Generics
import GHC.TypeLits   (type (<=?), type (+), Nat, TypeError, ErrorMessage(..))
import Data.Coerce

import Data.Generics.Internal.Families
import Data.Generics.Product.Internal.GLens
import Data.Generics.Internal.Errors
import Data.Generics.Internal.Profunctor.Lens
import Data.Generics.Internal.Profunctor.Iso

type Context' (i :: Nat) s a
  = ( Generic s
    , ErrorUnless i s (0 <? i && i <=? Size (Rep s))
    , Coercible (Rep s) (CRep s)
    , GLens' (HasTotalPositionPSym i) (CRep s) a
    , Defined (Rep s)
      (NoGeneric s '[ 'Text "arising from a generic lens focusing on the field at"
                    , 'Text "position " ':<>: QuoteType i ':<>: 'Text " of type " ':<>: QuoteType a
                      ':<>: 'Text " in " ':<>: QuoteType s
                    ])
      (() :: Constraint)
    )

class Context (i :: Nat) s t a b | s i -> a, t i -> b, s i b -> t, t i a -> s
instance
  ( ErrorUnless i s (0 <? i && i <=? Size (Rep s))
  , HasTotalPositionP i (CRep s) ~ 'Just a
  , HasTotalPositionP i (CRep t) ~ 'Just b
  , HasTotalPositionP i (CRep (Indexed s)) ~ 'Just a'
  , HasTotalPositionP i (CRep (Indexed t)) ~ 'Just b'
  , t ~ Infer s a' b
  , s ~ Infer t b' a
  ) => Context i s t a b

type Context_ i s t a b =
  ( ErrorUnless i s (0 <? i && i <=? Size (Rep s))
  , UnifyHead s t
  , UnifyHead t s
  )

type Context0 i s t a b
  = ( Generic s
    , Generic t
    , GLens (HasTotalPositionPSym i) (CRep s) (CRep t) a b
    , Coercible (CRep s) (Rep s)
    , Coercible (CRep t) (Rep t)
    , Defined (Rep s)
      (NoGeneric s '[ 'Text "arising from a generic lens focusing on the field at"
                    , 'Text "position " ':<>: QuoteType i ':<>: 'Text " of type " ':<>: QuoteType a
                      ':<>: 'Text " in " ':<>: QuoteType s
                    ])
      (() :: Constraint)
    )

derived0 :: forall i s t a b. Context0 i s t a b => Lens s t a b
derived0 = (repIso . coerced @(CRep s) @(CRep t) . glens @(HasTotalPositionPSym i))
{-# INLINE derived0 #-}

derived' :: forall i s a. Context' i s a => Lens s s a a
derived' = (repIso . coerced @(CRep s) @(CRep s) . glens @(HasTotalPositionPSym i))
{-# INLINE derived' #-}

type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
  ErrorUnless i s 'False
    = TypeError
        (     'Text "The type "
        ':<>: 'ShowType s
        ':<>: 'Text " does not contain a field at position "
        ':<>: 'ShowType i
        )

  ErrorUnless _ _ 'True
    = ()

data HasTotalPositionPSym  :: Nat -> (TyFun (Type -> Type) (Maybe Type))
type instance Eval (HasTotalPositionPSym t) tt = HasTotalPositionP t tt


-- We wouldn't need the universal 'x' here if we could express above that
-- forall x. Coercible (cs x) (Rep s x), but this requires quantified
-- constraints
coerced :: forall s t s' t' x. (Coercible t t', Coercible s s')
        => Iso (s' x) (t' x) (s x) (t x)
coerced = iso coerce coerce
{-# INLINE coerced #-}

--------------------------------------------------------------------------------  

-- | Alias for the kind of the generic rep
type G = Type -> Type

--------------------------------------------------------------------------------

-- | In-order labeling of the generic tree with the field positions
--
-- We replace the (K1 R a) nodes with (K1 (Pos n) a), where 'n' is the position
-- of the field in question in the data type. This is convenient, because we
-- can reuse all the existing functions as long as they are polymorphic in the
-- first parameter of 'K1'.
type family CRep (a :: Type) :: G where
  CRep rep = Fst (Traverse (Rep rep) 1)

-- | The actual traversal.
--
-- Might be cleaner if the sum and product parts were separated (as there's
-- and invariant that 'n' should be zero when we're at a sum node, which holds
-- for derived Generic instances (where the sums are strictly above the products))
type family Traverse (a :: G) (n :: Nat) :: (G, Nat) where
  Traverse (M1 mt m s) n
    = Traverse1 (M1 mt m) (Traverse s n)
  Traverse (l :+: r) n
    = '(Fst (Traverse l n) :+: Fst (Traverse r n), n)
  Traverse (l :*: r) n
    = TraverseProd (:*:) (Traverse l n) r
  Traverse (K1 _ p) n
    = '(K1 (Pos n) p, n + 1)
  Traverse U1 n
    = '(U1, n)

type family Traverse1 (w :: G -> G) (z :: (G, Nat)) :: (G, Nat) where
  Traverse1 w '(i, n) = '(w i, n)

-- | For products, we first traverse the left-hand side, followed by the second
-- using the counter returned by the left traversal.
type family TraverseProd (c :: G -> G -> G) (a :: (G, Nat)) (r :: G) :: (G, Nat) where
  TraverseProd w '(i, n) r = Traverse1 (w i) (Traverse r n)

--------------------------------------------------------------------------------
-- Utilities

type family Fst (p :: (a, b)) :: a where
  Fst '(a, b) = a

type family Size f :: Nat where
  Size (l :*: r)
    = Size l + Size r
  Size (l :+: r)
    = Min (Size l) (Size r)
  Size (D1 meta f)
    = Size f
  Size (C1 meta f)
    = Size f
  Size f
    = 1

type x <? y = Not (y <=? x)
infixl 4 <?

type Min a b = If (a <? b) a b