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

-- | This module provides the 'Forall' semantic
-- which preserves the polymorphism of the semantic.
-- Useful when parsing the syntax from a text
-- (ie. when the domain-specific language
-- is not embedded into a Haskell file).
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 Unsafe.Coerce (unsafeCoerce)

import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), 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 => Instantiable sem) =>
  Instantiable (Forall syns)
  where
  Forall a2b .@ Forall a = Forall (a2b .@ a)
instance
  ( forall sem. Syntaxes syns sem => Abstractable sem
  , forall sem. Syntaxes syns sem => Instantiable sem
  ) => Abstractable (Forall syns) where
  lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
    where
      -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
      forallSem :: sem a -> Forall syns a
      forallSem a = Forall (unsafeCoerce 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