{-# LANGUAGE ConstraintKinds #-}
-- For Semantic
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}

-- | This module provides the intermediate semantic 'SomeData'
-- which interprets combinators as data constructors.
-- This enables to pattern-match on combinators
-- while keeping their extensibility.
module Symantic.Syntaxes.Data where

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

import Symantic.Syntaxes.Classes
import Symantic.Syntaxes.Derive

-- * Type 'SomeData'
data SomeData sem a
  = forall syn.
    ( Derivable (Data syn sem)
    , Typeable syn
    ) =>
    SomeData (Data syn 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 (syn :: Syntax) :: Semantic -> Semantic
type instance Derived (Data syn sem) = sem

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

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

-- Abstractable
data instance Data Abstractable sem a where
  Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
instance (Abstractable sem, Varable sem) => Derivable (Data Abstractable sem) where
  derive = \case
    Lam f -> lam (\x -> derive (f (SomeData (Var x))))
instance (Abstractable sem, Varable sem) => Abstractable (SomeData sem) where
  lam f = SomeData (Lam f)

-- Abstractable1
data instance Data Abstractable1 sem a where
  Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable1 sem (a -> b)
instance (Abstractable1 sem, Varable sem) => Derivable (Data Abstractable1 sem) where
  derive = \case
    Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
instance (Abstractable1 sem, Varable sem) => Abstractable1 (SomeData sem) where
  lam1 f = SomeData (Lam1 f)

-- Varable
data instance Data Varable sem a where
  Var :: sem a -> Data Varable sem a
instance Varable sem => Derivable (Data Varable sem) where
  derive = \case
    Var x -> var x
instance Varable sem => Varable (SomeData sem) where
  var = Fun.id

-- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
-- but to avoid duplication of work, only those manually marked
-- as using their variable at most once.
--
-- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
-- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
normalOrderReduction ::
  forall sem a.
  Abstractable sem =>
  Abstractable1 sem =>
  Unabstractable sem =>
  Varable sem =>
  IfThenElseable sem =>
  SomeData sem a ->
  SomeData sem a
normalOrderReduction = nor
  where
    nor :: SomeData sem b -> SomeData sem b
    nor = \case
      Data (Lam f) -> lam (nor Fun.. f)
      Data (Lam1 f) -> lam1 (nor Fun.. f)
      Data (x :@ y) -> case whnf x of
        Data (Lam1 f) -> nor (f y)
        x' -> nor x' .@ nor y
      Data (IfThenElse test ok ko) ->
        case nor test of
          Data (Constant b :: Data (Constantable Bool) sem Bool) ->
            if b then nor ok else nor ko
          t -> ifThenElse (nor t) (nor ok) (nor ko)
      x -> x

    whnf :: SomeData sem b -> SomeData sem b
    whnf = \case
      Data (x :@ y) -> case whnf x of
        Data (Lam1 f) -> whnf (f y)
        x' -> x' .@ y
      x -> x

-- Unabstractable
data instance Data Unabstractable sem a where
  (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
instance Unabstractable sem => Derivable (Data Unabstractable sem) where
  derive = \case
    f :@ x -> derive f .@ derive x
instance Unabstractable sem => Unabstractable (SomeData sem) where
  f .@ x = SomeData (f :@ x)

-- Functionable
instance
  ( Abstractable sem
  , Unabstractable sem
  , Varable sem
  ) =>
  Functionable (SomeData sem)
  where
  ($) = lam (\f -> lam (\x -> f .@ x))
  (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
  const = lam (\x -> lam (\_y -> x))
  flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
  id = lam (\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
  Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
  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
    Either -> either
    Left -> left
    Right -> right
instance Eitherable sem => Eitherable (SomeData sem) where
  either = SomeData Either
  left = SomeData Left
  right = SomeData Right
instance Eitherable (Data Eitherable sem) where
  either = Either
  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