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

module Symantic.Compiler.Term where

import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Control.Monad.Trans.Except qualified as MT
import Control.Monad.Trans.Reader qualified as MT
import Control.Monad.Trans.State qualified as MT
import Data.Bool (otherwise)
import Data.Either (Either (..))
import Data.Eq (Eq (..))
import Data.Function (id, ($), (.))
import Data.Functor (Functor (..), (<$>))
import Data.Functor.Constant (Constant (..))
import Data.Int (Int)
import Data.Kind (Constraint, Type)
import Data.Maybe (Maybe (..), isJust)
import Data.Proxy (Proxy (..))
import Data.Semigroup (Semigroup (..))
import Data.String (String)
import GHC.Types
import Text.Read (Read (..), reads)
import Text.Show (Show (..))
import Unsafe.Coerce (unsafeCoerce)
import Prelude (error)
import Prelude qualified

import Symantic.Typer

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

data ForallSem (syn :: Syntax) (a :: 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
  }