{-# 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 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.Lang
import Symantic.Derive

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

type instance Derived (SomeData repr) = repr
instance Derivable (SomeData repr) 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 repr) = repr

-- | 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)

-- | @(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
  ) => Derivable (Data Abstractable repr) 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 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)

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

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

-- Constantable
data instance Data (Constantable c) repr a where
  Constant :: {-Typeable c =>-} c -> Data (Constantable c) repr c
instance Constantable c repr => Derivable (Data (Constantable c) repr) where
  derive = \case
    Constant x -> constant x
instance
  ( Constantable c repr
  , Typeable c
  ) => Constantable c (SomeData repr) where
  constant c = SomeData (Constant c)
instance {-Typeable c =>-} 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 => Derivable (Data Eitherable repr) where
  derive = \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 => Derivable (Data Equalable repr) where
  derive = \case
    Equal -> equal
instance
  ( Equalable repr
  ) => Equalable (SomeData repr) where
  equal = SomeData Equal
instance Equalable (Data Equalable repr) where
  equal = Equal

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

-- 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 => Derivable (Data Listable repr) where
  derive = \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 => Derivable (Data Maybeable repr) where
  derive = \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