{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- | A combinator to flip the order of the last two type parameters of a 'Hyper.Type.HyperType'.
module Hyper.Combinator.Flip
    ( HFlip (..)
    , _HFlip
    , hflipped
    , htraverseFlipped
    ) where

import Control.Lens (from, iso)
import Hyper.Class.Nodes (HWitness)
import Hyper.Class.Traversable (HTraversable, htraverse)
import Hyper.Type (GetHyperType, type (#))

import Hyper.Internal.Prelude

-- | Flip the order of the last two type parameters of a 'Hyper.Type.HyperType'.
--
-- Useful to use instances of classes such as 'Hyper.Class.Traversable.HTraversable' which
-- are available on the flipped 'Hyper.Type.HyperType'.
-- For example 'Hyper.Unify.Generalize.GTerm' has instances when flipped.
newtype HFlip f x h
    = MkHFlip (f (GetHyperType h) # x)
    deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: HyperType -> HyperType) (x :: HyperType)
       (h :: AHyperType) x.
Rep (HFlip f x h) x -> HFlip f x h
forall (f :: HyperType -> HyperType) (x :: HyperType)
       (h :: AHyperType) x.
HFlip f x h -> Rep (HFlip f x h) x
$cto :: forall (f :: HyperType -> HyperType) (x :: HyperType)
       (h :: AHyperType) x.
Rep (HFlip f x h) x -> HFlip f x h
$cfrom :: forall (f :: HyperType -> HyperType) (x :: HyperType)
       (h :: AHyperType) x.
HFlip f x h -> Rep (HFlip f x h) x
Generic)

makeCommonInstances [''HFlip]

-- | An 'Iso' from 'Flip' to its content.
--
-- Using `_Flip` rather than the 'MkFlip' data constructor is recommended,
-- because it helps the type inference know that @ANode c@ is parameterized with a 'Hyper.Type.HyperType'.
_HFlip ::
    Iso
        (HFlip f0 x0 # k0)
        (HFlip f1 x1 # k1)
        (f0 k0 # x0)
        (f1 k1 # x1)
_HFlip :: forall (f0 :: HyperType -> HyperType) (x0 :: HyperType)
       (k0 :: HyperType) (f1 :: HyperType -> HyperType) (x1 :: HyperType)
       (k1 :: HyperType).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip = forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (\(MkHFlip f0 (GetHyperType ('AHyperType k0)) # x0
x) -> f0 (GetHyperType ('AHyperType k0)) # x0
x) forall (f :: HyperType -> HyperType) (x :: HyperType)
       (h :: AHyperType).
(f (GetHyperType h) # x) -> HFlip f x h
MkHFlip

hflipped ::
    Iso
        (f0 k0 # x0)
        (f1 k1 # x1)
        (HFlip f0 x0 # k0)
        (HFlip f1 x1 # k1)
hflipped :: forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
       (x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
       (x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped = forall s t a b. AnIso s t a b -> Iso b a t s
from forall (f0 :: HyperType -> HyperType) (x0 :: HyperType)
       (k0 :: HyperType) (f1 :: HyperType -> HyperType) (x1 :: HyperType)
       (k1 :: HyperType).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip

-- | Convinience function for traversal over second last 'HyperType' argument.
htraverseFlipped ::
    (Applicative f, HTraversable (HFlip h a)) =>
    (forall n. HWitness (HFlip h a) n -> p # n -> f (q # n)) ->
    h p # a ->
    f (h q # a)
htraverseFlipped :: forall (f :: * -> *) (h :: HyperType -> HyperType) (a :: HyperType)
       (p :: HyperType) (q :: HyperType).
(Applicative f, HTraversable (HFlip h a)) =>
(forall (n :: HyperType).
 HWitness (HFlip h a) n -> (p # n) -> f (q # n))
-> (h p # a) -> f (h q # a)
htraverseFlipped forall (n :: HyperType).
HWitness (HFlip h a) n -> (p # n) -> f (q # n)
f = forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
       (x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
       (x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped (forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse forall (n :: HyperType).
HWitness (HFlip h a) n -> (p # n) -> f (q # n)
f)