{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# 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.Maybe (Maybe (..))
import Data.Monoid (Monoid (..))
import Data.Semigroup (Semigroup (..))
import Data.Void (Void)
import Symantic.Syntaxes.Classes (Unabstractable (..))
import Text.Show (Show (..))
import Type.Reflection (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 ErrMsg (TermVT finalSyns meta '[])
parse ast = unParser (fix parsersA ast) CtxTyZ
  where
    -- Unabstractable and Constable are always required.
    parsersA final (BinTree2 fT aT) = Parser $ \ctx -> do
      let Parser fE = final fT
      TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- fE ctx
      let Parser aE = final aT
      TermVT aTy (a :: OpenTerm finalSyns aVS a) <- aE ctx
      let (fTy', aTy') = appendVars fTy aTy
      case fTy' of
        -- FUN faTy bTy -> do
        TyApp
          { tyAppFun =
            TyApp
              { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
              , tyAppArg = faTy
              }
          , tyAppArg = bTy
          } -> do
            mgu <- show `left` unifyType mempty faTy aTy'
            let faTy' = subst @Ty mgu faTy
            let aTy'' = subst @Ty mgu aTy'
            case eqTy faTy' aTy'' of
              Nothing ->
                Left $
                  "TypeError: Unabstractable: eqTy: "
                    <> "\n faTy'="
                    <> show faTy
                    <> "\n aTy'="
                    <> show aTy''
              Just HRefl -> Right $ TermVT bTy $ f .@ a
        _ -> Left "TypeError: Unabstractable: fTy is not a function"
    parsersA final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e

-- * Class 'Parsers'
class Parsers syns finalSyns meta where
  parsers :: OpenParser finalSyns meta
instance Parsers '[] finalSyns meta where
  parsers _final ast = Parser $ \_ctx -> Left $ "Invalid tree: " <> show ast
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 finalSyn meta where
  tokenParser ::
    {-next-} (TokenTerm meta -> Parser finalSyn meta) ->
    OpenParser finalSyn meta
instance
  ( Syntaxes finalSyn (ForallSemantic finalSyn)
  ) =>
  TokenParser Unabstractable finalSyn meta
  where
  tokenParser next _final = next
instance
  ( Syntaxes finalSyn (ForallSemantic finalSyn)
  , forall sem. Syntaxes finalSyn sem => Constable sem
  , forall sem. Syntaxes finalSyn sem => Unabstractable sem
  ) =>
  TokenParser (Abstractable meta) finalSyn meta
  where
  tokenParser _next _final (TokenTermVar vN) = Parser go
    where
      go :: forall vs. CtxTy meta vs Void -> Either ErrMsg (TermVT finalSyn meta vs)
      go CtxTyZ = Left $ "Error_Term_unknown: " <> 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 (typeTy @meta) (kindOf aTy) of
        Nothing -> Left "TypeError: Abstractable: TokenTermAbst"
        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 finalSyn (ForallSemantic finalSyn)
  , forall sem. Syntaxes finalSyn sem => Addable sem
  ) =>
  TokenParser Addable finalSyn meta
  where
  tokenParser next _final = \case
    TokenTermAtom s
      | Right (i :: Int) <- safeRead s ->
          Parser $ \ctx -> Right $ TermVT (inferTy @_ @Int (mempty :: meta) (lenVar ctx)) $ E $ ForallSemantic @_ @Int $ lit i
    TokenTermAtom "neg" -> Parser $ \_ctx ->
      Right $ TermVT (intTy ~> intTy) $ E neg
    TokenTermAtom "add" -> Parser $ \_ctx ->
      Right $ TermVT (intTy ~> intTy ~> intTy) $ 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 = typeTy, 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 = typeTy, varZNext = LenS $ LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
        b = TyVar{tyVar = VarS $ VarZ{varZKind = typeTy, varZNext = LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "b"}
        c = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = typeTy, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "c"}
    tok -> next tok

intTy :: Monoid meta => Ty meta '[] Int
intTy = TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty}, tyConstLen = LenZ}

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
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))

-- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
tree2 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ lit 0)
tree3 = lam (typeOf @()) (\(x :: sem Int) -> 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 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 e
  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem

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

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

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