{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-fields #-}

module Symantic.Compiler.Term where

import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Data.Function ((.))
import Data.Function qualified as Fun
import Data.Functor (Functor (..))
import GHC.Types (Constraint, Type)
import Symantic.Syntaxes.Classes (Unabstractable (..))
import Text.Show (Show (..))
import Unsafe.Coerce (unsafeCoerce)

import Symantic.Typer.Type (Ty)

type Semantic = Type -> Type
type Syntax = Semantic -> Constraint

-- * 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 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 (not_syn ': syns) syn where
  perSyntax = PerSyntaxS . perSyntax

-- | Merge syntax 'Constraint's into a single 'Constraint'.
type family Syntaxes (syns :: [(Type -> Type) -> Constraint]) (sem :: Type -> Type) :: Constraint where
  Syntaxes '[] sem = (() :: Constraint)
  Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint)

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

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

-- * Class 'Abstractable'
class Abstractable meta sem where
  -- type AbstractableLam sem (a::Type) :: Constraint
  -- type AbstractableLam sem a = (()::Constraint)

  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)

-- * Class 'Constable'
class Constable sem where
  constI :: sem (a -> a)
  constK :: sem (a -> b -> a)
  constS :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
  constB :: sem ((b -> c) -> (a -> b) -> a -> c)
  constC :: sem ((a -> b -> c) -> b -> a -> c)

instance (forall sem. Syntaxes syns sem => Constable sem) => Constable (AnySemantic syns) where
  constI = AnySemantic constI
  constK = AnySemantic constK
  constS = AnySemantic constS
  constB = AnySemantic constB
  constC = AnySemantic constC
instance
  ( forall sem. Syntaxes syns sem => Abstractable meta sem
  -- , forall sem a. syn sem => AbstractableLam sem a
  -- , forall sem. syn sem => AbstractableLam sem a
  -- , forall sem. syn sem => Typeable sem -- user instance not accepted
  -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
  ) =>
  Abstractable meta (AnySemantic syns)
  where
  lam aTy f = AnySemantic (lam aTy (\a -> let AnySemantic b = f (forallSem a) in b))
    where
      -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
      forallSem :: sem a -> AnySemantic syns a
      forallSem a = AnySemantic (unsafeCoerce a)

-- * Type 'OpenTerm'
data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
  -- E contains embedded closed (i.e. already abstracted) terms.
  E :: AnySemantic syns a -> OpenTerm syns vs a
  -- V represents a reference to the innermost/top environment
  -- variable, i.e. Z
  V :: OpenTerm syns (a ': vs) a
  -- N represents internalizing the innermost bound variable as a
  -- function argument. In other words, we can represent an open
  -- term referring to a certain variable as a function which
  -- takes that variable as an argument.
  N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
  -- For efficiency, there is also a special variant of N for the
  -- case where the term does not refer to the topmost variable at all.
  W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
instance
  ( forall sem. Syntaxes syns sem => Abstractable meta sem
  , Syntaxes syns (AnySemantic syns)
  ) =>
  Abstractable meta (OpenTerm syns '[])
  where
  lam aTy f = E (lam aTy (runOpenTerm . f . E))
instance
  ( forall sem. Syntaxes syns sem => Constable sem
  , Syntaxes syns (AnySemantic syns)
  ) =>
  Constable (OpenTerm syns vs)
  where
  constI = E constI
  constK = E constK
  constS = E constS
  constB = E constB
  constC = E constC

-- * Type 'R'
newtype R a = R {unR :: a}
instance Abstractable meta R where
  lam _aTy f = R (unR . f . R)
instance Unabstractable R where
  R f .@ R x = R (f x)
instance Constable R where
  constI = R Fun.id
  constK = R Fun.const
  constS = R (<*>)
  constB = R (.)
  constC = R Fun.flip

runOpenTerm :: OpenTerm syns '[] a -> AnySemantic syns a
runOpenTerm t = case t of E t' -> t'

eval :: Syntaxes syns R => OpenTerm syns '[] a -> a
eval t
  | AnySemantic sem <- runOpenTerm t =
      unR sem

instance
  ( forall sem. Syntaxes syns sem => Constable sem
  , forall sem. Syntaxes syns sem => Unabstractable sem
  , Syntaxes syns (AnySemantic syns)
  -- , forall a as. syns (OpenTerm syns (as)) => syns (OpenTerm syns (a ': as))
  ) =>
  Unabstractable (OpenTerm syns vs)
  where
  (.@) = appOpenTerm

appOpenTerm ::
  forall syns as a b.
  ( forall sem. Syntaxes syns sem => Constable sem
  , forall sem. Syntaxes syns sem => Unabstractable sem
  , Syntaxes syns (AnySemantic syns)
  ) =>
  OpenTerm syns as (a -> b) ->
  OpenTerm syns as a ->
  OpenTerm syns as b
W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)
W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
W e `appOpenTerm` V = N e
V `appOpenTerm` W e = N (E (constC .@ constI) `appOpenTerm` e)
W e1 `appOpenTerm` N e2 = N (E constB `appOpenTerm` e1 `appOpenTerm` e2)
N e1 `appOpenTerm` W e2 = N (E constC `appOpenTerm` e1 `appOpenTerm` e2)
N e1 `appOpenTerm` N e2 = N (E constS `appOpenTerm` e1 `appOpenTerm` e2)
N e `appOpenTerm` V = N (E constS `appOpenTerm` e `appOpenTerm` E constI)
V `appOpenTerm` N e = N (E (constS .@ constI) `appOpenTerm` e)
E d `appOpenTerm` N e = N (E (constB .@ d) `appOpenTerm` e)
E d `appOpenTerm` V = N (E d)
V `appOpenTerm` E d = N (E (constC .@ constI .@ d))
N e `appOpenTerm` E d = N (E (constC .@ constC .@ d) `appOpenTerm` e)
E d1 `appOpenTerm` E d2 = E (d1 .@ d2)