{-# 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.Semantics.Forall (Forall (..), PerSyntax, PerSyntaxable (..))
import Symantic.Syntaxes.Classes (Syntaxes, 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 (Forall 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 xT) = Parser $ \ctx -> do
      TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- unParser (final fT) ctx
      TermVT xTy (a :: OpenTerm finalSyns aVS a) <- unParser (final xT) ctx
      case fTy of
        TyApp
          { tyAppFun =
            TyApp
              { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
              , tyAppArg = fxTy
              }
          , tyAppArg = rTy
          } -> do
            let (fxTy', xTy') = appendVars fxTy xTy
            mgu <- (perSyntax . ErrorParserUnabstractableUnify) `left` unifyType mempty fxTy' xTy'
            let fxTy'' = subst @Ty mgu fxTy'
            let xTy'' = subst @Ty mgu xTy'
            case eqTy fxTy'' xTy'' of
              Nothing -> Left $ perSyntax $ ErrorParserUnabstractableArgumentMismatch (TyVT fxTy'') (TyVT xTy'')
              Just HRefl -> Right $ TermVT rTy $ 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 (Forall finalSyns)
  ) =>
  TokenParser Unabstractable finalSyns meta
  where
  tokenParser next _final = next
data instance ErrorParser meta (AbstractableTy meta)
  = ErrorParserAbstractableUnknown Name
  | ErrorParserAbstractableNotAType (TyVT meta)
  deriving (Show)
instance
  ( Syntaxes finalSyns (Forall finalSyns)
  , forall sem. Syntaxes finalSyns sem => Constable sem
  , forall sem. Syntaxes finalSyns sem => Unabstractable sem
  , PerSyntaxable finalSyns (AbstractableTy meta)
  ) =>
  TokenParser (AbstractableTy 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 (argTy :: Ty meta '[] a)) bT) =
    Parser $ \ctx ->
      case eqTy (monoTy @Type @meta) (kindOf argTy) of
        Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT argTy)
        Just HRefl -> do
          TermVT resTy (b :: OpenTerm syn bVS b) <- (unParser (final bT)) (CtxTyS argName argTy ctx)
          let argTy' = allocVarsR (lenVar resTy) argTy
          Right $
            TermVT (argTy' ~> resTy) $
              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 (Forall 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
              $ Forall @_ @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 (Forall syns)
  , forall sem. Syntaxes syns sem => Constable sem
  ) =>
  TokenParser Constable syns meta
  where
  tokenParser next _final = \case
    TokenTermAtom "id" -> Parser $ \_ctx ->
      Right $ TermVT (aTy ~> aTy @'[]) $ E constI
    TokenTermAtom "(<*>)" -> Parser $ \_ctx ->
      Right $
        TermVT ((aTy ~> bTy ~> cTy) ~> (aTy ~> bTy) ~> aTy ~> cTy @'[]) $
          E constS
    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 (Forall syn) where
  lit n = Forall (lit n)
  neg = Forall neg
  add = Forall add
instance (forall sem. Syntaxes syn sem => Mulable sem) => Mulable (Forall syn) where
  mul (Forall a) (Forall b) = Forall (mul a b)

--
-- Parsing
--

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

-- parseMulable ::
--  forall syn meta.
--  ( forall sem. syn sem => Mulable sem
--  , forall sem. syn sem => Addable sem
--  , syn (Forall 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 (Forall a :: Forall 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 (Forall b :: Forall 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 (Forall @_ @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) => AbstractableTy meta (Printer meta) where
  lamTy xTy (f :: Printer meta a -> Printer meta b) =
    Printer $
      BinTree0
        ( TokenTermAbst
            "x"
            (TyT xTy)
            (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
        )

-- * Type 'FinalSyntaxes'
type FinalSyntaxes meta = '[AbstractableTy 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 = 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 -> Forall sem)) -> print sem

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

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

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

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

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