{-# 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 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.Semigroup (Semigroup (..))
import Data.Void (Void)
import Text.Show (Show (..))
import Type.Reflection (eqTypeRep, typeRep, (:~~:) (..))
import Prelude (error)

import Symantic
import Symantic.Typer ()

parse ::
  forall syns meta finalSyns.
  finalSyns ~ (UnAbstractable ': syns) =>
  Show meta =>
  Monoid meta =>
  FinalSyntax finalSyns (Semantics finalSyns) =>
  -- (forall sem. FinalSyntax finalSyns sem => Constable sem) =>
  Parsers finalSyns finalSyns meta =>
  TermAST meta ->
  Either ErrMsg (TermVT finalSyns meta '[])
parse ast = unParser (fix parsersA ast) CtxTyZ
  where
    -- UnAbstractable is always needed
    parsersA final (BinTree2 fT aT) = Parser $ \ctx -> do
      let Parser fE = final fT
      TermVT fTy (f :: OTerm syn fVS a2b) <- fE ctx
      case fTy of
        -- FUN iTy bTy -> do
        TyApp
          { tyAppFun =
            TyApp
              { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
              , tyAppArg = iTy
              }
          , tyAppArg = bTy
          } -> do
            let Parser aE = final aT
            TermVT aTy (a :: OTerm syn aVS a) <- aE ctx
            let (iTy', aTy') = appendVars iTy aTy
            case eqTy iTy' aTy' of
              Nothing -> Left "TypeError: UnAbstractable: eqTy"
              Just HRefl -> Right $ TermVT bTy $ f `appOTerm` 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
  ( ParserFor syn finalSyns meta
  , Parsers syns finalSyns meta
  ) =>
  Parsers (syn ': syns) finalSyns meta
  where
  parsers final = parserFor @syn @finalSyns (parsers @syns @finalSyns final) final

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

-- ** Class 'ParserFor'
class ParserFor syn finalSyn meta where
  parserFor ::
    {-next-} (TokenTerm meta -> Parser finalSyn meta) ->
    OpenParser finalSyn meta
instance
  ( FinalSyntax finalSyn (Semantics finalSyn)
  ) =>
  ParserFor UnAbstractable finalSyn meta
  where
  parserFor next _final = next
instance
  ( FinalSyntax finalSyn (Semantics finalSyn)
  , forall sem. FinalSyntax finalSyn sem => Constable sem
  , forall sem. FinalSyntax finalSyn sem => UnAbstractable sem
  ) =>
  ParserFor (Abstractable meta) finalSyn meta
  where
  parserFor _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
  parserFor _next final (TokenTermAbst argName (TyT (aTy :: Ty meta '[] a)) bT) =
    Parser $ \ctx ->
      case eqTy typeTy (kindOf aTy) of
        Nothing -> Left "TypeError: Abstractable: TokenTermAbst"
        Just HRefl -> do
          let Parser bE = final bT
          TermVT bTy (b :: OTerm 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 `appOTerm` e
                N e -> e
    where
      typeTy = TyConst{tyConst = Const{constType = typeRep @Type, constMeta = mempty :: meta}, tyConstLen = LenZ}
  parserFor next _final e = next e
instance
  ( FinalSyntax finalSyn (Semantics finalSyn)
  , forall sem. FinalSyntax finalSyn sem => Addable sem
  ) =>
  ParserFor Addable finalSyn meta
  where
  parserFor next _final = \case
    TokenTermAtom s
      | Right (i :: Int) <- safeRead s ->
          Parser $ \ctx -> Right $ TermVT (tyOf @Int (mempty :: meta) (lenVar ctx)) $ E $ Semantics @_ @Int $ lit i
    TokenTermAtom "neg" -> Parser $ \_ctx ->
      Right $ TermVT (tyOf (mempty :: meta) LenZ) $ E neg
    TokenTermAtom "add" -> Parser $ \_ctx ->
      Right $ TermVT (tyOf (mempty :: meta) LenZ) $ E add
    ast -> next ast
instance
  () =>
  -- syn (Semantics syn)
  -- , forall sem. syn sem => Constable sem
  ParserFor Constable syns meta
  where
  parserFor next _final = next

--
-- Parsing
--

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

-- parseMulable ::
--  forall syn meta.
--  ( forall sem. syn sem => Mulable sem
--  , forall sem. syn sem => Addable sem
--  , syn (Semantics 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 (Semantics a :: Semantics 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 (Semantics b :: Semantics 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 (Semantics @_ @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 (tyOf @a mempty LenZ))
            (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
        )

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

-- 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)
tree0Print = print tree0

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

tree0ParsePrint :: TermAST ()
tree0ParsePrint = case parse @(Syntaxes ()) @() tree0Print of
  Left e -> error e
  Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem

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

tree2ParsePrint :: TermAST ()
tree2ParsePrint = case parse @(Syntaxes ()) @() tree2Print of
  Left e -> error e
  Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem

tree3ParsePrint :: TermAST ()
tree3ParsePrint = case parse @(Syntaxes ()) @() tree3Print of
  Left e -> error e
  Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem