{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, EmptyCase, LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-} -- experiment
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeInType #-}

-- -- Experiment
-- {-# LANGUAGE MagicHash #-}

{-# OPTIONS_GHC -Wall #-}

-- {-# OPTIONS_GHC -fno-warn-unused-imports #-} -- TEMP
-- {-# OPTIONS_GHC -fno-warn-unused-binds   #-} -- TEMP

----------------------------------------------------------------------
-- |
-- Module      :  ConCat.Rep
-- Copyright   :  (c) 2016 Conal Elliott
-- 
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
-- 
-- Convert to and from standard representations.
-- TODO: Can I replace HasRep with Generic or Newtype?
----------------------------------------------------------------------

module ConCat.Rep (HasRep(..), inAbst,inAbst2, inAbstF1, inRepr,inRepr2) where

import Data.Monoid
-- import Data.Newtypes.PrettyDouble
import Control.Applicative (WrappedMonad(..))
import qualified GHC.Generics as G
import Data.Complex (Complex(..))
-- import GHC.TypeLits (KnownNat)
import Data.Proxy

import Data.Functor.Identity (Identity(..))
import Control.Monad.Trans.Reader (ReaderT(..))
import Control.Monad.Trans.Writer (WriterT(..))
import Control.Monad.Trans.State (StateT(..))
-- import Data.Finite (Finite,finite,getFinite)
-- import Data.Finite.Internal (Finite(..))

-- import Data.Void (Void)
-- TODO: more

-- import ConCat.Complex

-- import GHC.Types (TYPE)
-- import GHC.Exts (Int(..),Int#)

-- TODO: Eliminate most of the following when I drop these types.
import ConCat.Misc ((:*),(:+),Parity(..),(<~),bottom)

-- import TypeUnary.TyNat (Z,S)
-- import TypeUnary.Nat (Nat(..),IsNat(..))
-- import TypeUnary.Vec (Vec(..))

-- | Convert to and from standard representations. Used for transforming case
-- expression scrutinees and constructor applications. The 'repr' method should
-- convert to a standard representation (unit, products, sums), or closer to
-- such a representation, via another type with a 'HasRep' instance. The 'abst'
-- method should reveal a constructor so that we can perform the
-- case-of-known-constructor transformation.
-- It is very important to give @INLINE@ pragmas for 'repr' and 'abst' definitions.

class HasRep a where
  type Rep a
  repr :: a -> Rep a
  abst :: Rep a -> a

-- -- Identity as @'abst' . 'repr'@.
-- abstRepr :: HasRep a => a -> a
-- abstRepr = abst . repr

#define INLINES {-# INLINE repr #-};{-# INLINE abst #-}

instance HasRep (Proxy a) where
  type Rep (Proxy a) = ()
  repr :: Proxy a -> Rep (Proxy a)
repr Proxy a
Proxy = ()
  abst :: Rep (Proxy a) -> Proxy a
abst () = Proxy a
forall {k} (t :: k). Proxy t
Proxy
  INLINES

instance HasRep (a,b,c) where
  type Rep (a,b,c) = ((a,b),c)
  repr :: (a, b, c) -> Rep (a, b, c)
repr (a
a,b
b,c
c) = ((a
a,b
b),c
c)
  abst :: Rep (a, b, c) -> (a, b, c)
abst ((a
a,b
b),c
c) = (a
a,b
b,c
c)
  INLINES

instance HasRep (a,b,c,d) where
  type Rep (a,b,c,d) = ((a,b),(c,d))
  repr :: (a, b, c, d) -> Rep (a, b, c, d)
repr (a
a,b
b,c
c,d
d) = ((a
a,b
b),(c
c,d
d))
  abst :: Rep (a, b, c, d) -> (a, b, c, d)
abst ((a
a,b
b),(c
c,d
d)) = (a
a,b
b,c
c,d
d)
  INLINES

instance HasRep (a,b,c,d,e) where
  type Rep (a,b,c,d,e) = ((a,b,c,d),e)
  repr :: (a, b, c, d, e) -> Rep (a, b, c, d, e)
repr (a
a,b
b,c
c,d
d,e
e) = ((a
a,b
b,c
c,d
d),e
e)
  abst :: Rep (a, b, c, d, e) -> (a, b, c, d, e)
abst ((a
a,b
b,c
c,d
d),e
e) = (a
a,b
b,c
c,d
d,e
e)
  INLINES

instance HasRep (a,b,c,d,e,f) where
  type Rep (a,b,c,d,e,f) = ((a,b,c,d),(e,f))
  repr :: (a, b, c, d, e, f) -> Rep (a, b, c, d, e, f)
repr (a
a,b
b,c
c,d
d,e
e,f
f) = ((a
a,b
b,c
c,d
d),(e
e,f
f))
  abst :: Rep (a, b, c, d, e, f) -> (a, b, c, d, e, f)
abst ((a
a,b
b,c
c,d
d),(e
e,f
f)) = (a
a,b
b,c
c,d
d,e
e,f
f)
  INLINES

instance HasRep (a,b,c,d,e,f,g) where
  type Rep (a,b,c,d,e,f,g) = ((a,b,c,d),(e,f,g))
  repr :: (a, b, c, d, e, f, g) -> Rep (a, b, c, d, e, f, g)
repr (a
a,b
b,c
c,d
d,e
e,f
f,g
g) = ((a
a,b
b,c
c,d
d),(e
e,f
f,g
g))
  abst :: Rep (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)
abst ((a
a,b
b,c
c,d
d),(e
e,f
f,g
g)) = (a
a,b
b,c
c,d
d,e
e,f
f,g
g)
  INLINES

instance HasRep (a,b,c,d,e,f,g,h) where
  type Rep (a,b,c,d,e,f,g,h) = ((a,b,c,d),(e,f,g,h))
  repr :: (a, b, c, d, e, f, g, h) -> Rep (a, b, c, d, e, f, g, h)
repr (a
a,b
b,c
c,d
d,e
e,f
f,g
g,h
h) = ((a
a,b
b,c
c,d
d),(e
e,f
f,g
g,h
h))
  abst :: Rep (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)
abst ((a
a,b
b,c
c,d
d),(e
e,f
f,g
g,h
h)) = (a
a,b
b,c
c,d
d,e
e,f
f,g
g,h
h)
  INLINES

#if 1

-- I'm now synthesizing HasRep instances for newtypes.
-- Oh! I still need support for explicit uses.

#define WrapRep(abstT,reprT,con) \
instance HasRep (abstT) where { type Rep (abstT) = reprT; repr (con a) = a ; abst a = con a }

WrapRep(Sum a,a,Sum)
-- WrapRep(PrettyDouble,Double,PrettyDouble)
WrapRep(Product a,a,Product)
WrapRep(All,Bool,All)
WrapRep(Any,Bool,Any)
WrapRep(Dual a,a,Dual)
WrapRep(Endo a,a->a,Endo)
WrapRep(WrappedMonad m a,m a,WrapMonad)
WrapRep(Identity a,a,Identity)
WrapRep(ReaderT e m a, e -> m a, ReaderT)
WrapRep(WriterT w m a, m (a,w), WriterT)
WrapRep(StateT s m a, s -> m (a,s), StateT)

WrapRep(Parity,Bool,Parity)

-- instance KnownNat n => HasRep (Finite n) where
--   type Rep (Finite n) = Integer
--   -- abst = finite
--   -- repr = getFinite
--   abst n = Finite n
--   repr (Finite n) = n

-- instance KnownNat n => HasRep (Finite n) where
--   type Rep (Finite n) = Int
--   abst n = Finite (fromIntegral n)
--   repr (Finite n) = fromInteger n

-- Since Finite is a newtype, the HasRep instance doesn't come into play.

#endif

-- TODO: Generate these dictionaries on the fly during compilation, so we won't
-- have to list them here.

-- Experimental treatment of Maybe
instance HasRep (Maybe a) where
  type Rep (Maybe a) = Bool :* a
  repr :: Maybe a -> Rep (Maybe a)
repr (Just a
a) = (Bool
True,a
a)
  repr Maybe a
Nothing  = (Bool
False, a
forall a. a
bottom)
  abst :: Rep (Maybe a) -> Maybe a
abst (Bool
True,a
a ) = a -> Maybe a
forall a. a -> Maybe a
Just a
a
  abst (Bool
False,a
_) = Maybe a
forall a. Maybe a
Nothing 
  INLINES

-- TODO: LambdaCCC.Prim has an BottomP primitive. If the error ever occurs,
-- replace with ErrorP (taking a string argument) and tweak the reification.

-- Generalize Maybe to sums:

-- I use this version for circuits. Restore it later, after I'm handing :+ in reify-rules.

-- instance HasRep (a :+ b) where
--   type Rep (a :+ b) = Bool :* (a :* b)
--   repr (Left  a) = (False,(a,undefined)) -- error "repr on Maybe: undefined value"
--   repr (Right b) = (True,(undefined,b))
--   abst (False,(a,_)) = Left  a
--   abst (True ,(_,b)) = Right b

-- -- TODO: Redefine `Maybe` representation as sum:
-- 
-- type instance Rep (Maybe a) = Unit :+ a
-- ...

instance HasRep (Complex a) where
  type Rep (Complex a) = a :* a
  repr :: Complex a -> Rep (Complex a)
repr (a
a :+ a
a') = (a
a,a
a')
  abst :: Rep (Complex a) -> Complex a
abst (a
a,a
a') = (a
a a -> a -> Complex a
forall a. a -> a -> Complex a
:+ a
a')
  INLINES

-- instance HasRep (G.V1 p) where
--   type Rep (G.V1 p) = Void
--   repr = \ case
--   abst = \ case
--   INLINES

instance HasRep (G.U1 p) where
  type Rep (G.U1 p) = ()
  repr :: U1 p -> Rep (U1 p)
repr U1 p
G.U1 = ()
  abst :: Rep (U1 p) -> U1 p
abst () = U1 p
forall k (p :: k). U1 p
G.U1
  INLINES

instance HasRep (G.Par1 p) where
  type Rep (G.Par1 p) = p
  repr :: Par1 p -> Rep (Par1 p)
repr = Par1 p -> p
Par1 p -> Rep (Par1 p)
forall p. Par1 p -> p
G.unPar1
  abst :: Rep (Par1 p) -> Par1 p
abst = p -> Par1 p
Rep (Par1 p) -> Par1 p
forall p. p -> Par1 p
G.Par1
  INLINES

instance HasRep (G.K1 i c p) where
  type Rep (G.K1 i c p) = c
  repr :: K1 i c p -> Rep (K1 i c p)
repr = K1 i c p -> c
K1 i c p -> Rep (K1 i c p)
forall k i c (p :: k). K1 i c p -> c
G.unK1
  abst :: Rep (K1 i c p) -> K1 i c p
abst = c -> K1 i c p
Rep (K1 i c p) -> K1 i c p
forall k i c (p :: k). c -> K1 i c p
G.K1
  INLINES

instance HasRep (G.M1 i c f p) where
  type Rep (G.M1 i c f p) = f p
  repr :: M1 i c f p -> Rep (M1 i c f p)
repr = M1 i c f p -> f p
M1 i c f p -> Rep (M1 i c f p)
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  abst :: Rep (M1 i c f p) -> M1 i c f p
abst = f p -> M1 i c f p
Rep (M1 i c f p) -> M1 i c f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1
  INLINES

instance HasRep ((f G.:+: g) p) where
  type Rep ((f G.:+: g) p) = f p :+ g p
  repr :: (:+:) f g p -> Rep ((:+:) f g p)
repr (G.L1  f p
x) = f p -> Either (f p) (g p)
forall a b. a -> Either a b
Left  f p
x
  repr (G.R1  g p
x) = g p -> Either (f p) (g p)
forall a b. b -> Either a b
Right g p
x
  abst :: Rep ((:+:) f g p) -> (:+:) f g p
abst (Left  f p
x) = f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
G.L1  f p
x
  abst (Right g p
x) = g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
G.R1  g p
x
  INLINES

instance HasRep ((f G.:*: g) p) where
  type Rep ((f G.:*: g) p) = f p :* g p
  repr :: (:*:) f g p -> Rep ((:*:) f g p)
repr (f p
x G.:*: g p
y) = (f p
x,g p
y)
  abst :: Rep ((:*:) f g p) -> (:*:) f g p
abst (f p
x,g p
y) = (f p
x f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: g p
y)
  INLINES

instance HasRep ((g G.:.: f) p) where
  type Rep ((g G.:.: f) p) = g (f p)
  repr :: (:.:) g f p -> Rep ((:.:) g f p)
repr = (:.:) g f p -> g (f p)
(:.:) g f p -> Rep ((:.:) g f p)
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
G.unComp1
  abst :: Rep ((:.:) g f p) -> (:.:) g f p
abst = g (f p) -> (:.:) g f p
Rep ((:.:) g f p) -> (:.:) g f p
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
G.Comp1
  INLINES

-- TODO: Can I *replace* HasRep with Generic?

{--------------------------------------------------------------------
    Utilities
--------------------------------------------------------------------}

inAbst :: (HasRep p, HasRep q) =>
          (Rep p -> Rep q) -> (p -> q)
inAbst :: forall p q. (HasRep p, HasRep q) => (Rep p -> Rep q) -> p -> q
inAbst = Rep q -> q
forall a. HasRep a => Rep a -> a
abst (Rep q -> q) -> (p -> Rep p) -> (Rep p -> Rep q) -> p -> q
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ p -> Rep p
forall a. HasRep a => a -> Rep a
repr
{-# INLINE inAbst #-}

inAbst2 :: (HasRep p, HasRep q, HasRep r) =>
           (Rep p -> Rep q -> Rep r) -> (p -> q -> r)
inAbst2 :: forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 = (Rep q -> Rep r) -> q -> r
forall p q. (HasRep p, HasRep q) => (Rep p -> Rep q) -> p -> q
inAbst ((Rep q -> Rep r) -> q -> r)
-> (p -> Rep p) -> (Rep p -> Rep q -> Rep r) -> p -> q -> r
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ p -> Rep p
forall a. HasRep a => a -> Rep a
repr
{-# INLINE inAbst2 #-}

inAbstF1 :: (HasRep p, HasRep q, Functor f) => (f (Rep p) -> Rep q) -> (f p -> q)
inAbstF1 :: forall p q (f :: * -> *).
(HasRep p, HasRep q, Functor f) =>
(f (Rep p) -> Rep q) -> f p -> q
inAbstF1 = Rep q -> q
forall a. HasRep a => Rep a -> a
abst (Rep q -> q)
-> (f p -> f (Rep p)) -> (f (Rep p) -> Rep q) -> f p -> q
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ (p -> Rep p) -> f p -> f (Rep p)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p -> Rep p
forall a. HasRep a => a -> Rep a
repr
{-# INLINE inAbstF1 #-}

inRepr :: (HasRep p, HasRep q) =>
          (p -> q) -> (Rep p -> Rep q)
inRepr :: forall p q. (HasRep p, HasRep q) => (p -> q) -> Rep p -> Rep q
inRepr = q -> Rep q
forall a. HasRep a => a -> Rep a
repr (q -> Rep q) -> (Rep p -> p) -> (p -> q) -> Rep p -> Rep q
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ Rep p -> p
forall a. HasRep a => Rep a -> a
abst
{-# INLINE inRepr #-}

inRepr2 :: (HasRep p, HasRep q, HasRep r) =>
          (p -> q -> r) -> (Rep p -> Rep q -> Rep r)
inRepr2 :: forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(p -> q -> r) -> Rep p -> Rep q -> Rep r
inRepr2 = (q -> r) -> Rep q -> Rep r
forall p q. (HasRep p, HasRep q) => (p -> q) -> Rep p -> Rep q
inRepr ((q -> r) -> Rep q -> Rep r)
-> (Rep p -> p) -> (p -> q -> r) -> Rep p -> Rep q -> Rep r
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ Rep p -> p
forall a. HasRep a => Rep a -> a
abst
{-# INLINE inRepr2 #-}

{--------------------------------------------------------------------
    Unlifted types
--------------------------------------------------------------------}

#if 0
-- Represent unboxed types as boxed counterparts.

instance HasRep Int# where
  type Rep Int# = Int
  abst (I# n) = n
  repr n = I# n
  INLINES
#elif 0
-- Represent boxed types as unboxed counterparts.

instance HasRep Int where
  type Rep Int = Int#
  abst n = I# n
  repr (I# n) = n
  INLINES

#endif


-- data Int = I# Int# 	-- Defined in ‘GHC.Types’

-- class HasRep (a :: TYPE r) where
--   type Rep a :: TYPE s
--   repr :: a -> Rep a
--   abst :: Rep a -> a