{-# 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 prov finalSyns.
  finalSyns ~ (Unabstractable ': Constable ': syns) =>
  (forall k. ProvenanceKindOf (Ty @k) prov) =>
  (forall k. ProvenanceKindOf (Var @k) prov) =>
  Show prov =>
  Monoid prov =>
  Syntaxes finalSyns (Forall finalSyns) =>
  Parsers finalSyns finalSyns prov =>
  TermAST prov ->
  Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov '[])
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 = 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 @prov final e
data instance ErrorParser prov Unabstractable
  = ErrorParserUnabstractableArgumentMismatch (TyVT prov) (TyVT prov)
  | ErrorParserUnabstractableNotAFunction (TyVT prov)
  | ErrorParserUnabstractableUnify (ErrorUnify prov)
  deriving (Show)

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

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

-- ** Class 'TokenParser'
class TokenParser syn finalSyns prov where
  tokenParser ::
    {-next-} (TokenTerm prov -> Parser finalSyns prov) ->
    OpenParser finalSyns prov
instance
  ( Syntaxes finalSyns (Forall finalSyns)
  ) =>
  TokenParser Unabstractable finalSyns prov
  where
  tokenParser next _final = next
data instance ErrorParser prov (AbstractableTy (Ty prov '[]))
  = ErrorParserAbstractableUnknown Name
  | ErrorParserAbstractableNotAType (TyVT prov)
  deriving (Show)
instance
  ( Syntaxes finalSyns (Forall finalSyns)
  , forall sem. Syntaxes finalSyns sem => Constable sem
  , forall sem. Syntaxes finalSyns sem => Unabstractable sem
  , PerSyntaxable finalSyns (AbstractableTy (Ty prov '[]))
  , forall k. ProvenanceKindOf (Ty @k) prov
  ) =>
  TokenParser (AbstractableTy (Ty prov '[])) finalSyns prov
  where
  tokenParser _next _final (TokenTermVar vN) = Parser go
    where
      go :: forall vs. CtxTy prov vs Void -> Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov 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 prov '[] a)) bT) =
    Parser $ \ctx ->
      case eqTy (monoTy @Type @prov) (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 prov
  where
  tokenParser next _final = \case
    TokenTermAtom s
      | Right (i :: Int) <- safeRead s ->
          Parser $ \ctx ->
            Right
              $ TermVT
                (tyOfTypeRep (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 prov
  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 prov 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 prov.
--  ( forall sem. syn sem => Mulable sem
--  , forall sem. syn sem => Addable sem
--  , syn (Forall syn)
--  ) =>
--  Monoid prov =>
--  Show prov =>
--  (TermAST prov -> Parser syn prov) ->
--  TermAST prov -> Parser syn prov
-- 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::prov}, 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::prov}, 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 prov) where
  constI = printConst "id"
  constK = printConst "const"
  constS = printConst "(<*>)"
  constB = printConst "(.)"
  constC = printConst "flip"
instance Addable (Printer prov) where
  lit n = Printer $ BinTree0 (TokenTermAtom (show n))
  neg = printConst "neg"
  add = printConst "add"
instance Mulable (Printer prov) where
  mul = print2 "mul"
instance Unabstractable (Printer prov) where
  Printer f .@ Printer a = Printer $ BinTree2 f a
instance (Monoid prov) => AbstractableTy (Ty prov '[]) (Printer prov) where
  lamTy xTy (f :: Printer prov a -> Printer prov b) =
    Printer $
      BinTree0
        ( TokenTermAbst
            "x"
            (TyT xTy)
            (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
        )

-- * Type 'FinalSyntaxes'
type FinalSyntaxes prov = '[AbstractableTy (Ty prov '[]), 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 (unE -> Forall sem)) -> print sem

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

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

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

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

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