{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

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 Data.Int (Int)
import GHC.Types (Constraint, Type)
import Unsafe.Coerce (unsafeCoerce)

import Symantic.Typer.Type (Ty)

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

-- | Like 'FinalSyntax' but partially applicable.
--class FinalSyntax syns sem => ForallSyntaxes syns (sem::Type -> Type) where
--instance ForallSyntaxes '[] sem
--instance ((syn sem, ForallSyntaxes syns sem)::Constraint) => ForallSyntaxes (syn ': syns) sem

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

data Semantics (syns :: [Syntax]) (a :: Type) = Semantics {unForallSem :: forall sem. FinalSyntax syns sem => sem a}

-- * Type 'CtxTe'

-- | GADT for an /interpreting context/:
-- accumulating at each /lambda abstraction/
-- the term of the introduced variable.
data CtxTe (sem :: Type -> Type) (as :: [Type]) where
  CtxTeZ :: CtxTe sem '[]
  CtxTeS :: sem a -> CtxTe sem as -> CtxTe sem (a ': as)

infixr 5 `CtxTeS`

class Addable sem where
  lit :: Int -> sem Int
  neg :: sem (Int -> Int)
  add :: sem (Int -> Int -> Int)

class Mulable sem where
  mul :: sem Int -> sem Int -> sem Int

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 UnAbstractable sem where
  -- | Application, aka. unabstract.
  (.@) :: sem (a -> b) -> sem a -> sem b

instance (forall sem. FinalSyntax syn sem => Constable sem) => Constable (Semantics syn) where
  constI = Semantics constI
  constK = Semantics constK
  constS = Semantics constS
  constB = Semantics constB
  constC = Semantics constC
instance (forall sem. FinalSyntax syn sem => Addable sem) => Addable (Semantics syn) where
  lit n = Semantics (lit n)
  neg = Semantics neg
  add = Semantics add
instance (forall sem. FinalSyntax syn sem => Mulable sem) => Mulable (Semantics syn) where
  mul (Semantics a) (Semantics b) = Semantics (mul a b)
instance
  ( forall sem. FinalSyntax syn 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 (Semantics syn)
  where
  lam aTy f = Semantics (lam aTy (\a -> let Semantics b = f (forallSem a) in b))
    where
      -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
      forallSem :: sem a -> Semantics syn a
      forallSem a = Semantics (unsafeCoerce a)
instance
  (forall sem. FinalSyntax syn sem => UnAbstractable sem) =>
  UnAbstractable (Semantics syn)
  where
  Semantics a2b .@ Semantics a = Semantics (a2b .@ a)

data TTerm (syn :: [Syntax]) (vs :: [Type]) (a :: Type) where
  -- TVar :: Var vs a -> TTerm syn vs a
  TConst :: Semantics syn a -> TTerm syn vs a
  TLam :: TTerm syn (a ': vs) b -> TTerm syn vs (a -> b)
  TApp :: TTerm syn vs (a -> b) -> TTerm syn vs a -> TTerm syn vs b

data OTerm (syn :: [Syntax]) (vs :: [Type]) (a :: Type) where
  -- E contains embedded closed (i.e. already abstracted) terms.
  E :: Semantics syn a -> OTerm syn vs a
  -- V represents a reference to the innermost/top environment
  -- variable, i.e. Z
  V :: OTerm syn (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 :: OTerm syn vs (a -> b) -> OTerm syn (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 :: OTerm syn vs b -> OTerm syn (a ': vs) b
instance
  ( forall sem. FinalSyntax syn sem => Abstractable meta sem
  , FinalSyntax syn (Semantics syn)
  ) =>
  Abstractable meta (OTerm syn '[])
  where
  lam aTy f = E (lam aTy (runOTerm . f . E))
instance
  ( forall sem. FinalSyntax syn sem => Constable sem
  , FinalSyntax syn (Semantics syn)
  ) =>
  Constable (OTerm syn vs)
  where
  constI = E constI
  constK = E constK
  constS = E constS
  constB = E constB
  constC = E constC

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

runOTerm :: OTerm syn '[] a -> Semantics syn a
runOTerm t = case t of E t' -> t'

eval :: FinalSyntax syn R => OTerm syn '[] a -> a
eval t
  | Semantics sem <- runOTerm t =
      unR sem

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. FinalSyntax syn sem => Constable sem
  , forall sem. FinalSyntax syn sem => UnAbstractable sem
  , FinalSyntax syn (Semantics syn)
  -- , forall a as. syn (OTerm syn (as)) => syn (OTerm syn (a ': as))
  ) =>
  UnAbstractable (OTerm syn vs)
  where
  (.@) = appOTerm

appOTerm ::
  forall syn as a b.
  ( forall sem. FinalSyntax syn sem => Constable sem
  , forall sem. FinalSyntax syn sem => UnAbstractable sem
  , FinalSyntax syn (Semantics syn)
  ) =>
  OTerm syn as (a -> b) ->
  OTerm syn as a ->
  OTerm syn as b
W e1 `appOTerm` W e2 = W (e1 `appOTerm` e2)
W e `appOTerm` E d = W (e `appOTerm` E d)
E d `appOTerm` W e = W (E d `appOTerm` e)
W e `appOTerm` V = N e
V `appOTerm` W e = N (E (constC .@ constI) `appOTerm` e)
W e1 `appOTerm` N e2 = N (E constB `appOTerm` e1 `appOTerm` e2)
N e1 `appOTerm` W e2 = N (E constC `appOTerm` e1 `appOTerm` e2)
N e1 `appOTerm` N e2 = N (E constS `appOTerm` e1 `appOTerm` e2)
N e `appOTerm` V = N (E constS `appOTerm` e `appOTerm` E constI)
V `appOTerm` N e = N (E (constS .@ constI) `appOTerm` e)
E d `appOTerm` N e = N (E (constB .@ d) `appOTerm` e)
E d `appOTerm` V = N (E d)
V `appOTerm` E d = N (E (constC .@ constI .@ d))
N e `appOTerm` E d = N (E (constC .@ constC .@ d) `appOTerm` e)
E d1 `appOTerm` E d2 = E (d1 .@ d2)

data CONST syn a where
  -- CInt :: Int -> Const Int
  -- CIf :: Const (Bool -> a -> a -> a)
  -- CAdd :: Const (Int -> Int -> Int)
  -- CGt :: Ord a => Const (a -> a -> Bool)
  F :: Semantics syn a -> CONST syn a
  I :: CONST syn (a -> a)
  K :: CONST syn (a -> b -> a)
  S :: CONST syn ((a -> b -> c) -> (a -> b) -> a -> c)
  B :: CONST syn ((b -> c) -> (a -> b) -> a -> c)
  C :: CONST syn ((a -> b -> c) -> b -> a -> c)

-- conv :: Term vs α -> OTerm vs α
-- conv = \case
--  TVar VZ -> V
--  TVar (VS x) -> W (conv (TVar x))
--  TLam t -> case conv t of
--    V -> E (embed I)
--    E d -> E (K .$$ d)
--    N e -> e
--    W e -> K .$$ e
--  TApp t1 t2 -> conv t1 $$ conv t2
--  TConst c -> embed c

instance
  ( forall sem. FinalSyntax syn sem => Functor sem
  ) =>
  Functor (Semantics syn)
  where
  fmap f (Semantics sem) = Semantics (fmap f sem)
  a <$ (Semantics sem) = Semantics (a <$ sem)
instance
  ( forall sem. FinalSyntax syn sem => Applicative sem
  , Functor (Semantics syn)
  ) =>
  Applicative (Semantics syn)
  where
  pure a = Semantics (pure a)
  liftA2 f (Semantics a) (Semantics b) = Semantics (liftA2 f a b)
  (<*>) (Semantics f) (Semantics a) = Semantics ((<*>) f a)
  (<*) (Semantics f) (Semantics a) = Semantics ((<*) f a)
  (*>) (Semantics f) (Semantics a) = Semantics ((*>) f a)
instance
  ( forall sem. FinalSyntax syn sem => Monad sem
  , Applicative (Semantics syn)
  ) =>
  Monad (Semantics syn)
  where
  (>>=) (Semantics sa) f = Semantics (sa >>= \a -> case f a of Semantics sb -> sb)
  return = pure
  (>>) = (*>)