{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

module Symantic.Semantics.Forall where

import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Data.Bool (Bool (..))
import Data.Eq (Eq (..))
import Data.Function ((.))
import Data.Functor (Functor (..))
import Data.Kind (Type)
import Text.Show (Show (..))

import Symantic.Syntaxes.Classes (Syntax, Syntaxes, Unabstractable (..))

-- * Type 'Forall'
newtype Forall (syns :: [Syntax]) (a :: Type)
  = Forall (forall sem. Syntaxes syns sem => sem a)

instance
  ( forall sem. Syntaxes syns sem => Functor sem
  ) =>
  Functor (Forall syns)
  where
  fmap f (Forall sem) = Forall (fmap f sem)
  a <$ (Forall sem) = Forall (a <$ sem)
instance
  ( forall sem. Syntaxes syns sem => Applicative sem
  , Functor (Forall syns)
  ) =>
  Applicative (Forall syns)
  where
  pure a = Forall (pure a)
  liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
  (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
  (<*) (Forall f) (Forall a) = Forall ((<*) f a)
  (*>) (Forall f) (Forall a) = Forall ((*>) f a)
instance
  ( forall sem. Syntaxes syns sem => Monad sem
  , Applicative (Forall syns)
  ) =>
  Monad (Forall syns)
  where
  (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
  return = pure
  (>>) = (*>)
instance
  (forall sem. Syntaxes syns sem => Unabstractable sem) =>
  Unabstractable (Forall syns)
  where
  Forall a2b .@ Forall a = Forall (a2b .@ a)

-- * Type 'PerSyntax'
data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
  PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
  PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a

instance Eq (PerSyntax '[] a) where
  (==) = \case {}
instance
  ( Eq (a syn)
  , Eq (PerSyntax syns a)
  ) =>
  Eq (PerSyntax (syn ': syns) a)
  where
  PerSyntaxZ x == PerSyntaxZ y = x == y
  PerSyntaxS x == PerSyntaxS y = x == y
  _ == _ = False

instance Show (PerSyntax '[] a) where
  showsPrec _p = \case {}
instance
  ( Show (a syn)
  , Show (PerSyntax syns a)
  ) =>
  Show (PerSyntax (syn ': syns) a)
  where
  showsPrec p = \case
    PerSyntaxZ a -> showsPrec p a
    PerSyntaxS s -> showsPrec p s

-- ** Class 'PerSyntaxable'
class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
  perSyntax :: a syn -> PerSyntax syns a
instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
  perSyntax = PerSyntaxZ
instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
  perSyntax = PerSyntaxS . perSyntax