{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
-- {-# OPTIONS_GHC -Wno-monomorphism-restriction #-}
{-# OPTIONS_GHC -freduction-depth=400 #-}

module Symantic.Syntaxes where

import Data.Either (Either (..))
import Data.Eq (Eq (..))
import Data.Function (($))
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 Debug.Trace
import Text.Show (Show (..))
import Type.Reflection (eqTypeRep, typeRep, (:~~:) (..))
import Prelude (error)

import Symantic
import Symantic.Typer ()

--
-- Parsing
--

parseAbstractable ::
  forall syn meta.
  ( forall sem. syn sem => Constable sem
  , forall sem. syn sem => Abstractable meta sem
  , forall sem. syn sem => UnAbstractable sem
  , -- , forall sem a. syn sem => AbstractableLam sem a
    -- , forall sem. syn sem => Mulable sem
    forall sem. syn sem => Addable sem
  , syn (ForallSem syn)
  -- , forall vs. syn (OTerm syn vs)
  ) =>
  Show meta =>
  Monoid meta =>
  (TermAST meta -> Parser syn meta) ->
  TermAST meta ->
  Parser syn meta
-- FIXME: parse variables
parseAbstractable _final (BinTree0 (TokenTermVar vN)) = Parser go
  where
    go :: forall vs. CtxTy meta vs Void -> Either ErrMsg (TermVT syn 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
parseAbstractable final (BinTree2 fT aT) = Parser $ \ctx ->
  case (final fT, final aT) of
    (Parser fE, Parser aE) -> do
      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
            TermVT aTy (a :: OTerm syn aVS a) <- aE ctx
            let (iTy', aTy') = appendVars iTy aTy
            case eqTy iTy' aTy' of
              Nothing -> Left "TypeError: Abstractable: BinTree2: eqTy"
              Just HRefl -> Right $ TermVT bTy $ f `appOTerm` a
        _ -> Left "TypeError: Abstractable: BinTree2"
parseAbstractable final (BinTree0 (TokenTermAbst argName (TyT (aTy :: Ty meta '[] a)) bT)) =
  Parser $ \ctx ->
    let typeTy = TyConst{tyConst = Const{constType = typeRep @Type, constMeta = mempty :: meta}, tyConstLen = LenZ}
     in case eqTy typeTy (kindOf aTy) of
          Nothing -> Left "TypeError: Abstractable: BinTree0: TokenTermAbst"
          Just HRefl ->
            case final bT of
              Parser bE -> do
                TermVT bTy (b :: OTerm syn bVS b) <- bE (CtxTyS argName aTy ctx)
                -- let (aTy', bTy') = appendVars aTy bTy
                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
parseAbstractable final t = parseConstable final t

parseAddable ::
  forall syn meta.
  ( forall sem. syn sem => Addable sem
  , syn (ForallSem syn)
  -- , forall vs. syn (OTerm syn vs)
  ) =>
  Monoid meta =>
  Show meta =>
  (TermAST meta -> Parser syn meta) ->
  TermAST meta ->
  Parser syn meta
parseAddable _final (BinTree0 (TokenTermAtom s))
  | Right (i :: Int) <- safeRead s =
      Parser $ \ctx -> Right $ TermVT (tyOf @Int (mempty :: meta) (lenVar ctx)) $ E $ ForallSem @_ @Int $ lit i
parseAddable _final (BinTree0 (TokenTermAtom "neg")) = Parser $ \_ctx ->
  Right $ TermVT (tyOf (mempty :: meta) LenZ) $ E neg
parseAddable _final (BinTree0 (TokenTermAtom "add")) = Parser $ \_ctx ->
  Right $ TermVT (tyOf (mempty :: meta) LenZ) $ E add
parseAddable _final e = Parser $ \_ctx -> Left $ "Invalid tree: " <> show e

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

-- parseMulable ::
--  forall syn meta.
--  ( forall sem. syn sem => Mulable sem
--  , forall sem. syn sem => Addable sem
--  , syn (ForallSem 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 (ForallSem a :: ForallSem 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 (ForallSem b :: ForallSem 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 (ForallSem @_ @a $ mul a b)
-- parseMulable final t = parseAddable final t

parseConstable ::
  ( forall sem. syn sem => Constable sem
  , -- , forall sem. syn sem => Mulable sem
    forall sem. syn sem => Addable sem
  , syn (ForallSem syn)
  ) =>
  Show meta =>
  Monoid meta =>
  (TermAST meta -> Parser syn meta) ->
  TermAST meta ->
  Parser syn meta
parseConstable = parseAddable

-- parseConstable final t = parseAddable final t
-- parseConstable _final e = Parser $ \_ctx -> Left $ "Invalid tree: " <> show e

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

class (Addable sem {- Mulable sem,-}, Abstractable meta sem, UnAbstractable sem, Constable sem) => FinalSyntaxes meta sem
instance (Addable sem {- Mulable sem,-}, Abstractable meta sem, UnAbstractable sem, Constable sem) => FinalSyntaxes meta sem

fix :: (a -> a) -> a
fix f = f (fix f)

parse ::
  forall syn meta.
  ( -- , forall sem. syn sem => Mulable sem
    forall sem. syn sem => Constable sem
  , forall sem. syn sem => Abstractable meta sem
  , forall sem. syn sem => UnAbstractable sem
  , forall sem. syn sem => Addable sem
  , syn (ForallSem syn)
  -- , syn (OTerm syn '[])
  ) =>
  Monoid meta =>
  Show meta =>
  TermAST meta ->
  -- Parser syn meta
  Either ErrMsg (TermVT syn meta '[])
parse ast = unParser (fix parseAbstractable ast) CtxTyZ

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

-- tree1Print = print tree1
tree2Print = print tree2

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

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