{-# 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.Eq qualified as Eq
import Data.Function qualified as Fun
import Data.Functor (Functor (..))
import Data.Kind (Type)
import Data.Tuple qualified as Tuple
import Text.Show (Show (..))
import Unsafe.Coerce (unsafeCoerce)

import Symantic.Syntaxes.Classes

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

{-# INLINE forall1 #-}
forall1 ::
  (forall sem. Syntaxes syns sem => sem a -> sem b) ->
  Forall syns a -> Forall syns b
forall1 f (Forall a) = Forall (f a)

{-# INLINE forall2 #-}
forall2 ::
  (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c) ->
  Forall syns a -> Forall syns b -> Forall syns c
forall2 f (Forall a) (Forall b) = Forall (f a b)

{-# INLINE forall3 #-}
forall3 ::
  (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d) ->
  Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d
forall3 f (Forall a) (Forall b) (Forall c) = Forall (f a b c)

{-# INLINE forall4 #-}
forall4 ::
  (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d -> sem e) ->
  Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d -> Forall syns e
forall4 f (Forall a) (Forall b) (Forall c) (Forall d) = Forall (f a b c d)

instance
  ( forall sem. Syntaxes syns sem => Functor sem
  ) => Functor (Forall syns) where
  fmap f = forall1 (fmap f)
  (<$) a = forall1 (a <$)
instance
  ( forall sem. Syntaxes syns sem => Applicative sem
  , Functor (Forall syns)
  ) => Applicative (Forall syns) where
  pure a = Forall (pure a)
  liftA2 f = forall2 (liftA2 f)
  (<*>) = forall2 (<*>)
  (<*)  = forall2 (<*)
  (*>)  = forall2 (*>)
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 => Varable sem
  ) => Varable (Forall syns) where
  var = forall1 var
instance
  (forall sem. Syntaxes syns sem => Instantiable sem) =>
  Instantiable (Forall syns)
  where
  (.@) = forall2 (.@)
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)
instance
  ( forall sem. Syntaxes syns sem => Unabstractable sem
  ) => Unabstractable (Forall syns) where
  ap = Forall ap
  const = Forall const
  id = Forall id
  (.) = Forall (.)
  flip = Forall flip
  ($) = Forall ($)
instance
  ( forall sem. Syntaxes syns sem => Constantable c sem
  ) => Constantable c (Forall syns) where
  constant c = Forall (constant c)
instance
  ( forall sem. Syntaxes syns sem => Eitherable sem
  ) => Eitherable (Forall syns) where
  either = Forall either
  left = Forall left
  right = Forall right
instance
  ( forall sem. Syntaxes syns sem => Equalable sem
  ) => Equalable (Forall syns) where
  equal = Forall equal
instance
  ( forall sem. Syntaxes syns sem => IfThenElseable sem
  ) => IfThenElseable (Forall syns) where
  ifThenElse = forall3 ifThenElse
instance
  ( forall sem. Syntaxes syns sem => Inferable c sem
  ) => Inferable c (Forall syns) where
  infer = Forall infer
instance
  ( forall sem. Syntaxes syns sem => Listable sem
  ) => Listable (Forall syns) where
  cons = Forall cons
  nil = Forall nil
instance
  ( forall sem. Syntaxes syns sem => Maybeable sem
  ) => Maybeable (Forall syns) where
  just = Forall just
  nothing = Forall nothing
instance
  ( forall sem. Syntaxes syns sem => IsoFunctor sem
  ) => IsoFunctor (Forall syns) where
  (<%>) iso = forall1 (iso <%>)
instance
  ( forall sem. Syntaxes syns sem => ProductFunctor sem
  , forall sem. Syntaxes syns sem => IsoFunctor sem
  , Syntaxes syns (Forall syns)
  ) => ProductFunctor (Forall syns) where
  (<.>) = forall2 (<.>)
  ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
  ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
instance
  ( forall sem. Syntaxes syns sem => SumFunctor sem
  ) => SumFunctor (Forall syns) where
  (<+>) = forall2 (<+>)
instance
  ( forall sem. Syntaxes syns sem => AlternativeFunctor sem
  ) => AlternativeFunctor (Forall syns) where
  (<|>) = forall2 (<|>)
instance
  ( forall sem. Syntaxes syns sem => Dicurryable sem
  ) => Dicurryable (Forall syns) where
  dicurry args constr destr = forall1 (dicurry args constr destr)
instance
  ( forall sem. Syntaxes syns sem => Emptyable sem
  ) => Emptyable (Forall syns) where
  empty = Forall empty
instance
  ( forall sem. Syntaxes syns sem => Semigroupable sem
  ) => Semigroupable (Forall syns) where
  concat = Forall concat
instance
  ( forall sem. Syntaxes syns sem => Optionable sem
  ) => Optionable (Forall syns) where
  optional = forall1 optional
instance
  ( forall sem. Syntaxes syns sem => Repeatable sem
  ) => Repeatable (Forall syns) where
  many0 = forall1 many0
  many1 = forall1 many1
instance
  ( forall sem. Syntaxes syns sem => Substractable sem
  ) => Substractable (Forall syns) where
  (<->) = forall2 (<->)
instance
  ( forall sem. Syntaxes syns sem => Voidable sem
  ) => Voidable (Forall syns) where
  void a = forall1 (void 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 Eq.== y
  PerSyntaxS x == PerSyntaxS y = x Eq.== 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 Fun.. perSyntax