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

module Symantic.Compiler.Term where

import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Data.Functor (Functor (..))
import GHC.Types (Constraint, Type)

import Symantic.Typer.Type (Ty)

type Semantic = GHC.Types.Type -> GHC.Types.Type
type Syntax = Semantic -> GHC.Types.Constraint

data ForallSem (syn :: Syntax) (a :: GHC.Types.Type) = ForallSem {unForallSem :: forall sem. syn sem => sem a}

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

-- * Interpreter 'Parser'
data TermVT syn = forall vs a.
  TermVT
  { typeTermVT :: Ty () vs a
  , unTermVT :: ForallSem syn a
  }