{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-} -- For ReprKind
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Data where

import Data.Bool (Bool)
import Data.Either (Either)
import Data.Kind (Constraint)
import Data.Maybe (Maybe)
import Data.Semigroup (Semigroup)
import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
import qualified Data.Eq as Eq
import qualified Data.Function as Fun
import qualified Data.Maybe as Maybe

import Symantic.Classes
import Symantic.Derive

-- * Type 'SomeData'
data SomeData sem a =
  forall able.
  ( Derivable (Data able sem)
  , Typeable able
  ) => SomeData (Data able sem a)

type instance Derived (SomeData sem) = sem
instance Derivable (SomeData sem) where
  derive (SomeData x) = derive x

-- ** Type 'Data'
-- 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
data family Data
  (able :: ReprKind -> Constraint)
  :: ReprKind -> ReprKind
type instance Derived (Data able sem) = sem

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

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

-- Abstractable
data instance Data Abstractable sem a where
  (:@) :: SomeData sem (a->b) -> SomeData sem a -> Data Abstractable sem b
  Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a->b)
  Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a->b)
  Var :: sem a -> Data Abstractable sem a
  -- FIXME: add constructors
instance
  ( Abstractable sem
  ) => Derivable (Data Abstractable sem) where
  derive = \case
    f :@ x -> derive f .@ derive x
    Lam f -> lam (\x -> derive (f (SomeData (Var x))))
    Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
    Var x -> var x
instance
  ( Abstractable sem
  ) => Abstractable (SomeData sem) where
  f .@ x = SomeData (f :@ x)
  lam f = SomeData (Lam f)
  lam1 f = SomeData (Lam1 f)
  var = Fun.id

-- Functionable
instance
  ( Abstractable sem
  ) => Functionable (SomeData sem) where
  ($) = 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)

-- Anythingable
data instance Data Anythingable sem a where
  Anything :: sem a -> Data Anythingable sem a
instance
  ( Anythingable sem
  ) => Derivable (Data Anythingable sem) where
  derive = \case
    Anything x -> anything x
instance Anythingable (SomeData sem)
instance Anythingable (Data Anythingable sem)

-- Bottomable
data instance Data Bottomable sem a where
  Bottom :: Data Bottomable sem a
instance Bottomable sem => Derivable (Data Bottomable sem) where
  derive Bottom{} = bottom

-- Constantable
data instance Data (Constantable c) sem a where
  Constant :: {-Typeable c =>-} c -> Data (Constantable c) sem c
instance Constantable c sem => Derivable (Data (Constantable c) sem) where
  derive = \case
    Constant x -> constant x
instance
  ( Constantable c sem
  , Typeable c
  ) => Constantable c (SomeData sem) where
  constant c = SomeData (Constant c)
instance {-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
  constant = Constant

-- Eitherable
data instance Data Eitherable sem a where
  Left :: Data Eitherable sem (l -> Either l r)
  Right :: Data Eitherable sem (r -> Either l r)
instance Eitherable sem => Derivable (Data Eitherable sem) where
  derive = \case
    Left -> left
    Right -> right
instance
  ( Eitherable sem
  ) => Eitherable (SomeData sem) where
  left = SomeData Left
  right = SomeData Right
instance Eitherable (Data Eitherable sem) where
  left = Left
  right = Right

-- Equalable
data instance Data Equalable sem a where
  Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
instance Equalable sem => Derivable (Data Equalable sem) where
  derive = \case
    Equal -> equal
instance
  ( Equalable sem
  ) => Equalable (SomeData sem) where
  equal = SomeData Equal
instance Equalable (Data Equalable sem) where
  equal = Equal

-- Emptyable
data instance Data Emptyable sem a where
  Empty :: Data Emptyable sem a
instance Emptyable sem => Derivable (Data Emptyable sem) where
  derive = \case
    Empty -> empty
instance
  ( Emptyable sem
  ) => Emptyable (SomeData sem) where
  empty = SomeData Empty
instance Emptyable (Data Emptyable sem) where
  empty = Empty

-- Semigroupable
data instance Data Semigroupable sem a where
  Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
infixr 4 `Concat`
instance Semigroupable sem => Derivable (Data Semigroupable sem) where
  derive = \case
    Concat -> concat
instance
  ( Semigroupable sem
  ) => Semigroupable (SomeData sem) where
  concat = SomeData Concat
instance Semigroupable (Data Semigroupable sem) where
  concat = Concat

-- IfThenElseable
data instance Data IfThenElseable sem a where
  IfThenElse ::
    SomeData sem Bool ->
    SomeData sem a ->
    SomeData sem a ->
    Data IfThenElseable sem a
instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
  derive = \case
    IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
instance
  ( IfThenElseable sem
  ) => IfThenElseable (SomeData sem) where
  ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
  ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)

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

-- Maybeable
data instance Data Maybeable sem a where
  Nothing :: Data Maybeable sem (Maybe a)
  Just :: Data Maybeable sem (a -> Maybe a)
instance Maybeable sem => Derivable (Data Maybeable sem) where
  derive = \case
    Nothing -> nothing
    Just -> just
instance
  ( Maybeable sem
  ) => Maybeable (SomeData sem) where
  nothing = SomeData Nothing
  just = SomeData Just
instance Maybeable (Data Maybeable sem) where
  nothing = Nothing
  just = Just