{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- {-# OPTIONS_GHC -Wno-monomorphism-restriction #-}

module Symantic.Syntaxes where

import Control.Arrow (left)
import Data.Either (Either (..))
import Data.Eq (Eq (..))
import Data.Function (fix, ($), (.))
import Data.Int (Int)
import Data.Kind (Type)
import Data.Maybe (Maybe (..))
import Data.Monoid (Monoid (..))
import Data.Void (Void)
import Symantic.Syntaxes.Classes (Unabstractable (..))
import Text.Show (Show (..))
import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
import Prelude (error)

import Symantic
import Symantic.Typer ()

parse ::
  forall syns meta finalSyns.
  finalSyns ~ (Unabstractable ': Constable ': syns) =>
  Show meta =>
  Monoid meta =>
  Syntaxes finalSyns (ForallSemantic finalSyns) =>
  Parsers finalSyns finalSyns meta =>
  TermAST meta ->
  Either (PerSyntax finalSyns (ErrorParser meta)) (TermVT finalSyns meta '[])
parse ast = unParser (fix openParser ast) CtxTyZ
  where
    -- Unabstractable and Constable are always required.
    openParser final (BinTree2 fT aT) = Parser $ \ctx -> do
      let Parser fE = final fT
      let Parser aE = final aT
      TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- fE ctx
      TermVT aTy (a :: OpenTerm finalSyns aVS a) <- aE ctx
      case fTy of
        -- FUN faTy bTy -> do
        TyApp
          { tyAppFun =
            TyApp
              { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
              , tyAppArg = faTy
              }
          , tyAppArg = bTy
          } -> do
            let (faTy', aTy') = appendVars faTy aTy
            mgu <- (perSyntax . ErrorParserUnabstractableUnify) `left` unifyType mempty faTy' aTy'
            let faTy'' = subst @Ty mgu faTy'
            let aTy'' = subst @Ty mgu aTy'
            case eqTy faTy'' aTy'' of
              Nothing -> Left $ perSyntax $ ErrorParserUnabstractableArgumentMismatch (TyVT faTy'') (TyVT aTy'')
              Just HRefl -> Right $ TermVT bTy $ f .@ a
        _ -> Left $ perSyntax $ ErrorParserUnabstractableNotAFunction (TyVT fTy)
    openParser final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e
data instance ErrorParser meta Unabstractable
  = ErrorParserUnabstractableArgumentMismatch (TyVT meta) (TyVT meta)
  | ErrorParserUnabstractableNotAFunction (TyVT meta)
  | ErrorParserUnabstractableUnify (ErrorUnify meta)
  deriving (Show)

data instance ErrorParser meta Constable
  = ErrorParserConstableInvalid (TokenTerm meta)
  deriving (Show)

-- * Class 'Parsers'
class Parsers syns finalSyns meta where
  parsers :: OpenParser finalSyns meta
instance PerSyntaxable finalSyns Constable => Parsers '[] finalSyns meta where
  parsers _final tok = Parser $ \_ctx ->
    Left $ perSyntax $ ErrorParserConstableInvalid tok
instance
  ( TokenParser syn finalSyns meta
  , Parsers syns finalSyns meta
  ) =>
  Parsers (syn ': syns) finalSyns meta
  where
  parsers final = tokenParser @syn @finalSyns (parsers @syns @finalSyns final) final

-- ** Type 'OpenParser'
type OpenParser syns meta =
  Show meta =>
  Monoid meta =>
  {-final-} (TermAST meta -> Parser syns meta) ->
  TokenTerm meta ->
  Parser syns meta

-- ** Class 'TokenParser'
class TokenParser syn finalSyns meta where
  tokenParser ::
    {-next-} (TokenTerm meta -> Parser finalSyns meta) ->
    OpenParser finalSyns meta
instance
  ( Syntaxes finalSyns (ForallSemantic finalSyns)
  ) =>
  TokenParser Unabstractable finalSyns meta
  where
  tokenParser next _final = next
data instance ErrorParser meta (Abstractable meta)
  = ErrorParserAbstractableUnknown Name
  | ErrorParserAbstractableNotAType (TyVT meta)
  deriving (Show)
instance
  ( Syntaxes finalSyns (ForallSemantic finalSyns)
  , forall sem. Syntaxes finalSyns sem => Constable sem
  , forall sem. Syntaxes finalSyns sem => Unabstractable sem
  , PerSyntaxable finalSyns (Abstractable meta)
  ) =>
  TokenParser (Abstractable meta) finalSyns meta
  where
  tokenParser _next _final (TokenTermVar vN) = Parser go
    where
      go :: forall vs. CtxTy meta vs Void -> Either (PerSyntax finalSyns (ErrorParser meta)) (TermVT finalSyns meta vs)
      go CtxTyZ = Left $ perSyntax $ ErrorParserAbstractableUnknown vN
      go (CtxTyS n ty _) | n == vN = Right $ TermVT ty $ V
      go (CtxTyS _n _typ tys) = do
        TermVT ty ot <- go tys
        Right $ TermVT ty $ W ot
  tokenParser _next final (TokenTermAbst argName (TyT (aTy :: Ty meta '[] a)) bT) =
    Parser $ \ctx ->
      case eqTy (monoTy @Type @meta) (kindOf aTy) of
        Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT aTy)
        Just HRefl -> do
          let Parser bE = final bT
          TermVT bTy (b :: OpenTerm syn bVS b) <- bE (CtxTyS argName aTy ctx)
          let aTy' = allocVarsR (lenVar bTy) aTy
          Right $
            TermVT (aTy' ~> bTy) $
              case b of
                E d -> E (constK .@ d)
                V -> E constI
                W e -> E constK `appOpenTerm` e
                N e -> e
  tokenParser next _final e = next e
instance
  ( Syntaxes finalSyns (ForallSemantic finalSyns)
  , forall sem. Syntaxes finalSyns sem => Addable sem
  ) =>
  TokenParser Addable finalSyns meta
  where
  tokenParser next _final = \case
    TokenTermAtom s
      | Right (i :: Int) <- safeRead s ->
          Parser $ \ctx ->
            Right
              $ TermVT
                (tyOfTypeRep mempty (lenVar ctx) (typeRep @Int))
              $ E
              $ ForallSemantic @_ @Int
              $ lit i
    TokenTermAtom "neg" -> Parser $ \_ctx ->
      Right $ TermVT (monoTy @Int ~> monoTy @Int) $ E neg
    TokenTermAtom "add" -> Parser $ \_ctx ->
      Right $ TermVT (monoTy @Int ~> monoTy @Int ~> monoTy @Int) $ E add
    ast -> next ast
instance
  ( Syntaxes syns (ForallSemantic syns)
  , forall sem. Syntaxes syns sem => Constable sem
  ) =>
  TokenParser Constable syns meta
  where
  tokenParser next _final = \case
    TokenTermAtom "id" -> Parser $ \_ctx ->
      Right
        $ TermVT
          (a ~> a)
        $ E constI
      where
        a = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
    TokenTermAtom "(<*>)" -> Parser $ \_ctx ->
      Right
        $ TermVT
          ((a ~> b ~> c) ~> (a ~> b) ~> a ~> c)
        $ E constS
      where
        a = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = LenS $ LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
        b = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "b"}
        c = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "c"}
    tok -> next tok

-- * Class 'Addable'
class Addable sem where
  lit :: Int -> sem Int
  neg :: sem (Int -> Int)
  add :: sem (Int -> Int -> Int)
data instance ErrorParser meta Addable
  deriving (Show)

-- * Class 'Mulable'
class Mulable sem where
  mul :: sem Int -> sem Int -> sem Int
instance (forall sem. Syntaxes syn sem => Addable sem) => Addable (ForallSemantic syn) where
  lit n = ForallSemantic (lit n)
  neg = ForallSemantic neg
  add = ForallSemantic add
instance (forall sem. Syntaxes syn sem => Mulable sem) => Mulable (ForallSemantic syn) where
  mul (ForallSemantic a) (ForallSemantic b) = ForallSemantic (mul a b)

--
-- Parsing
--

-- tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSemantic syn)) => Either ErrMsg (ForallSemantic syn Int)
-- tree0Parser = unParser $ parse tree0Print

-- parseMulable ::
--  forall syn meta.
--  ( forall sem. syn sem => Mulable sem
--  , forall sem. syn sem => Addable sem
--  , syn (ForallSemantic syn)
--  ) =>
--  Monoid meta =>
--  Show meta =>
--  (TermAST meta -> Parser syn meta) ->
--  TermAST meta -> Parser syn meta
-- parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "mul")) aT) bT) =
--  Parser $ \ctx -> do
--    case (final aT, final bT) of
--      (Parser aE, Parser bE) -> do
--        TermVT aTy (ForallSemantic a :: ForallSemantic syn a) <- aE ctx
--        case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar aTy} of
--          Nothing -> Left "TypeError: Mulable 1"
--          Just HRefl -> do
--            TermVT bTy (ForallSemantic b :: ForallSemantic syn b) <- bE ctx
--            case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar bTy} of
--              Nothing -> Left "TypeError: Mulable 2"
--              Just HRefl -> do
--                Right $ TermVT aTy (ForallSemantic @_ @a $ mul a b)
-- parseMulable final t = parseAddable final t

--
-- Printing
--

printConst n = Printer (BinTree0 (TokenTermAtom n))

instance Constable (Printer meta) where
  constI = printConst "id"
  constK = printConst "const"
  constS = printConst "(<*>)"
  constB = printConst "(.)"
  constC = printConst "flip"
instance Addable (Printer meta) where
  lit n = Printer $ BinTree0 (TokenTermAtom (show n))
  neg = printConst "neg"
  add = printConst "add"
instance Mulable (Printer meta) where
  mul = print2 "mul"
instance Unabstractable (Printer meta) where
  Printer f .@ Printer a = Printer $ BinTree2 f a
instance (Monoid meta) => Abstractable meta (Printer meta) where
  lam aTy (f :: Printer meta a -> Printer meta b) =
    Printer $
      BinTree0
        ( TokenTermAbst
            "x"
            (TyT aTy) -- (TyT (inferTy @a mempty LenZ))
            (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
        )

-- * Type 'FinalSyntaxes'
type FinalSyntaxes meta = '[Abstractable meta, Addable]

-- tree0 = lit 0
tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))

fun ::
  Abstractable () sem =>
  Typeable a =>
  (sem a -> sem b) ->
  sem (a -> b)
fun = lam (monoTy @_ @())

-- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
tree2 = fun (\x -> add .@ x .@ lit 0)
tree3 = fun (\x -> add .@ x .@ x)
tree4 = constS .@ add .@ constI
tree0Print = print tree0

-- tree1Print = print tree1
tree2Print = print tree2
tree3Print = print tree3
tree4Print = print tree4

tree0ParsePrint :: TermAST ()
tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
  Left e -> error $ show e
  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem

-- tree1ParsePrint :: TermAST ()
-- tree1ParsePrint = case parse @(FinalSyntaxes ()) @() tree1Print of
--  Left e -> error e
--  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem

tree2ParsePrint :: TermAST ()
tree2ParsePrint = case parse @(FinalSyntaxes ()) @() tree2Print of
  Left e -> error $ show e
  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem

tree3ParsePrint :: TermAST ()
tree3ParsePrint = case parse @(FinalSyntaxes ()) @() tree3Print of
  Left e -> error $ show e
  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem

tree3ParsePrint' :: TermAST ()
tree3ParsePrint' = case parse @(FinalSyntaxes ()) @() tree3ParsePrint of
  Left e -> error $ show e
  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem

tree4ParsePrint :: TermAST ()
tree4ParsePrint = case parse @(FinalSyntaxes ()) @() tree4Print of
  Left e -> error $ show e
  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem