{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
--{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-} -- For Abstractable (SomeData repr)
{-# LANGUAGE ViewPatterns #-}
module Symantic.Univariant.Data where

import Data.Kind
import Type.Reflection
import Data.Char (Char)
import Data.Bool (Bool)
import Data.Either (Either)
import Data.Maybe (Maybe)
import Data.Functor.Identity (Identity(..))
import Data.String (String)
import Prelude (undefined)
import Text.Show (Show(..))
import qualified Data.Eq as Eq
import qualified Data.Maybe as Maybe
import qualified Data.Function as Fun
import Data.Coerce

import Symantic.Univariant.Lang
import Symantic.Univariant.Trans

data SomeData repr a =
  forall able.
  ( Trans (Data able repr) repr
  , Typeable able
  ) => SomeData (Data able repr a)

instance Trans (SomeData repr) repr where
  trans (SomeData x) = trans x

type UnivariantRepr = Type -> Type

-- TODO: neither data families nor data instances
-- can have phantom roles with GHC-9's RoleAnnotations,
-- hence 'Data.Coerce.coerce' cannot be used on them for now.
-- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
-- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
-- Would be useful for @Trans (Data able repr) (Data able repr')@ instances.
data family Data
  (able :: UnivariantRepr -> Constraint)
  :: UnivariantRepr -> UnivariantRepr
--instance Trans (Data able repr) (Data able repr) where
--  trans = Fun.id

-- | Convenient utility to pattern-match a 'SomeData'.
pattern Data :: Typeable able => Data able repr a -> SomeData repr a
pattern Data x <- (unSomeData -> Maybe.Just x)

{-
class TransUnit able where
  -- | The 'Bottomable' constraint is needed when a @(repr)@ value
  -- has to be constructed.
  reprFromUnit :: Bottomable repr => Data able Unit a -> SomeData repr a
  -- | The 'Bottomable' constraint is also needed here
  -- to call 'reprFromUnit' in the 'Lam' case.
  unitFromRepr :: Bottomable repr => Data able repr a -> SomeData Unit a

coerceRepr ::
  Bottomable repr => Bottomable repr' =>
  SomeData repr a -> SomeData repr' a
coerceRepr (SomeData r) =
  case unitFromRepr r of
    SomeData d -> reprFromUnit d
-}

-- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
-- extract the data-constructor from the given 'SomeData'
-- iif. it belongs to the @('Data' able repr a)@ data-instance.
unSomeData ::
  forall able repr a.
  Typeable able =>
  SomeData repr a -> Maybe (Data able repr a)
unSomeData (SomeData (c::Data c repr a)) =
  case typeRep @able `eqTypeRep` typeRep @c of
    Maybe.Just HRefl -> Maybe.Just c
    Maybe.Nothing -> Maybe.Nothing

-- Abstractable
data instance Data Abstractable repr a where
  (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
  Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
  Var :: repr a -> Data Abstractable repr a
  -- FIXME: add constructors
instance
  ( Abstractable repr
  --, Trans (SomeData repr) repr
  --, Trans repr (SomeData repr)
  ) => Trans (Data Abstractable repr) repr where
  trans = \case
    f :@ x -> trans f .@ trans x
    Lam f -> lam (\x -> trans (f (SomeData (Var x))))
    Lam1 f -> lam1 (\x -> trans (f (SomeData (Var x))))
    Var x -> var x
instance
  ( Abstractable repr
  --, Trans (SomeData repr) repr
  --, Trans repr (SomeData repr)
  ) => Abstractable (SomeData repr) where
  f .@ x = SomeData (f :@ x)
  lam f = SomeData (Lam f)
  lam1 f = SomeData (Lam1 f)
  var = Fun.id
  ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  const = lam1 (\x -> lam1 (\_y -> x))
  flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  id = lam1 (\x -> x)

{-
instance
  ( Abstractable repr
  ) =>
  Abstractable (Data Abstractable repr) where
  var = Var Fun.. SomeData
  f .@ x = SomeData f :@ SomeData x
  lam f = Lam (SomeData Fun.. f Fun.. Var)
  lam1 f = Lam1 (SomeData Fun.. f Fun.. Var)
  ($) = lam1 (\f -> lam1 (\x -> f .@ x))
  (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
  const = lam1 (\x -> lam1 (\_y -> x))
  flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
  id = lam1 (\x -> x)
-}
{-
instance Bottomable repr => Morph (SomeData repr) (SomeData Unit) where
  morph (SomeData x) = morph x
instance Bottomable repr => Morph (SomeData Unit) (SomeData repr) where
  morph (SomeData x) = morph x
instance Abstractable Unit where
  (.@) _f _x = Unit
  lam _f = Unit
  lam1 _f = Unit
  ($) = Unit
  (.) = Unit
  const = Unit
  flip = Unit
  id = Unit
instance Abstractable (Data Abstractable Unit) where
  f .@ x = SomeData f :@ SomeData x
  lam f = Lam (\(SomeData x) -> SomeData (f (trans x)))
  lam1 f = Lam1 (\(SomeData x) -> SomeData (f (trans x)))
  ($) = ($)
  (.) = (.)
  const = const
  flip = flip
  id = id
-}

-- Anythingable
data instance Data Anythingable repr a where
  Anything :: repr a -> Data Anythingable repr a
instance
  ( Anythingable repr
  ) =>
  Trans (Data Anythingable repr) repr where
  trans = \case
    Anything x -> anything x
instance Anythingable (SomeData repr)
instance Anythingable (Data Anythingable repr)

-- Bottomable
class Bottomable repr where
  bottom :: repr a
data instance Data Bottomable repr a where
  Bottom :: Data Bottomable repr a
instance Bottomable repr => Trans (Data Bottomable repr) repr where
  trans Bottom{} = bottom

-- Constantable
data instance Data (Constantable c) repr a where
  Constant :: c -> Data (Constantable c) repr c
instance Constantable c repr => Trans (Data (Constantable c) repr) repr where
  trans = \case
    Constant x -> constant x
instance
  ( Constantable c repr
  , Typeable c
  ) => Constantable c (SomeData repr) where
  constant c = SomeData (Constant c)
instance Constantable c (Data (Constantable c) repr) where
  constant = Constant

-- Eitherable
data instance Data Eitherable repr a where
  Left :: Data Eitherable repr (l -> Either l r)
  Right :: Data Eitherable repr (r -> Either l r)
instance Eitherable repr => Trans (Data Eitherable repr) repr where
  trans = \case
    Left -> left
    Right -> right
instance
  ( Eitherable repr
  ) => Eitherable (SomeData repr) where
  left = SomeData Left
  right = SomeData Right
instance Eitherable (Data Eitherable repr) where
  left = Left
  right = Right

-- Equalable
data instance Data Equalable repr a where
  Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
instance Equalable repr => Trans (Data Equalable repr) repr where
  trans = \case
    Equal -> equal
instance
  ( Equalable repr
  ) => Equalable (SomeData repr) where
  equal = SomeData Equal
instance Equalable (Data Equalable repr) where
  equal = Equal

-- Listable
data instance Data Listable repr a where
  Cons :: Data Listable repr (a -> [a] -> [a])
  Nil :: Data Listable repr [a]
infixr 4 `Cons`
instance Listable repr => Trans (Data Listable repr) repr where
  trans = \case
    Cons -> cons
    Nil -> nil
instance
  ( Listable repr
  ) => Listable (SomeData repr) where
  cons = SomeData Cons
  nil = SomeData Nil
instance Listable (Data Listable repr) where
  cons = Cons
  nil = Nil

-- Maybeable
data instance Data Maybeable repr a where
  Nothing :: Data Maybeable repr (Maybe a)
  Just :: Data Maybeable repr (a -> Maybe a)
instance Maybeable repr => Trans (Data Maybeable repr) repr where
  trans = \case
    Nothing -> nothing
    Just -> just
instance
  ( Maybeable repr
  ) => Maybeable (SomeData repr) where
  nothing = SomeData Nothing
  just = SomeData Just
instance Maybeable (Data Maybeable repr) where
  nothing = Nothing
  just = Just