{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Compiling.Term.Test where

import Test.Tasty
import Test.Tasty.HUnit

import qualified Control.Arrow as Arrow
import qualified Control.Monad as Monad
import qualified Control.Monad.Classes as MC
import qualified Control.Monad.Classes.Run as MC
-- import Control.Monad.IO.Class (MonadIO(..))
import qualified Control.Monad.Trans.State.Strict as SS
import qualified Data.Foldable as Foldable
import Data.Functor.Identity (Identity(..))
import qualified Data.Map.Strict as Map
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude as Pre
import qualified Text.Megaparsec as P

import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Parsing
import qualified Language.Symantic.Grammar as Gram
import Language.Symantic.Typing

import Parsing.Test
import Typing.Test ()

type Meta = ()

---
-- P.ParsecT instances
---
type instance MC.CanDo (P.ParsecT e s m) eff = 'False
instance ParsecC e s => Gram_Term_Name (P.ParsecT e s m)
instance ParsecC e s => Gram.Gram_Meta Meta (P.ParsecT e s m) where
	metaG = (($ ()) Pre.<$>)
instance
 ( ParsecC e s
 , Gram.Gram_Meta meta (P.ParsecT e s m)
 ) => Gram_Term_Type meta (P.ParsecT e s m)
instance
 ( ParsecC e s
 ) => Gram_Error (P.ParsecT e s m) where
	term_unError (Gram.CF me) = Gram.CF $ do
		e <- me
		case e of
		 Left err -> Monad.fail $ Pre.show err
		 Right a -> Monad.return a
instance
 ( ParsecC e s
 , Gram.Gram_Meta meta (P.ParsecT e s m)
 , MC.MonadState (Tokenizers meta ts) m
 , Gram_Term_AtomsR meta ts ts (P.ParsecT e s m)
 ) => Gram_Term ts meta (P.ParsecT e s m) where
	term_tokenizers (Gram.CF ma) = Gram.CF $ do
		a <- ma
		toks :: Tokenizers meta ts <- MC.get
		Monad.return $ a toks
	term_abst_args_body (Gram.CF args) (Gram.CF body) = Gram.CF $ do
		as <- args
		bo <- do
			toks :: Tokenizers meta ts <- MC.get
			MC.put $
				Tokenizers
				 { tokenizers_prefix  = del (tokenizers_prefix  toks) as
				 , tokenizers_infix   = del (tokenizers_infix   toks) as
				 , tokenizers_postfix = del (tokenizers_postfix toks) as
				 }
			body Pre.<* MC.put toks
		Monad.return (as, bo)
		where del = Foldable.foldr (\(n, _) -> Map.adjust (Map.delete n) [])

test_tokenizer :: forall is.
 ( Inj_Tokens Meta is [Proxy (->), Proxy Integer]
 , Gram_Term is Meta (P.ParsecT P.Dec String (SS.StateT (Tokenizers Meta is) Identity))
 , Tokenize Meta is
 ) => String -> Either (P.ParseError Char P.Dec) (EToken Meta is)
test_tokenizer inp =
	runIdentity $
	MC.evalStateStrict (tokenizers::Tokenizers Meta is) $
	(`runParserT` inp) $
	Gram.unCF $ (termG Pre.<* Gram.eoi)

test_compile
 :: forall is h.
 ( Eq h
 , Eq_Token Meta is
 , Show h
 , Show_TyConst (TyConsts_of_Ifaces is)
 , Show_Token Meta is
 , Sym_of_Ifaces is HostI
 , Sym_of_Ifaces is TextI
 , Compile is
 , Inj_Tokens Meta is [Proxy (->), Proxy Integer]
 , Gram_Term is Meta (P.ParsecT P.Dec String (SS.StateT (Tokenizers Meta is) Identity))
 , Tokenize Meta is
 ) => String
 -> Either ( Type (TyConsts_of_Ifaces is) h
           , Either (P.ParseError Char P.Dec)
                    (Error_Term Meta is) )
           (Type (TyConsts_of_Ifaces is) h, h, Text)
 -> TestTree
test_compile inp expected =
	testCase (elide inp) $
	case test_tokenizer inp of
	 Left err -> Left (Left err) @?= Pre.snd `Arrow.left` expected
	 Right tok ->
		case compile tok of
		 Left err -> Left (Right err) @?= Pre.snd `Arrow.left` expected
		 Right (ETerm typ (Term te)) ->
			case expected of
			 Left (_, err) -> Right ("…"::Text) @?= Left err
			 Right (ty_expected::Type (TyConsts_of_Ifaces is) h, _::h, _::Text) ->
				(Monad.>>= (@?= (\(_::Type (TyConsts_of_Ifaces is) h, err) -> err) `Arrow.left` expected)) $
				case typ `eq_Type` ty_expected of
				 Nothing -> Monad.return $ Left $ Right $
					Error_Term_Con_Type $ Right $
					Con_TyEq
					 (Right $ At Nothing $ EType typ)
					 (At Nothing $ EType ty_expected)
				 Just Refl -> do
					let h = host_from_term te
					Monad.return $
						Right
						 ( typ
						 , h
						 , text_from_term te
						 -- , (text_from_term :: Repr_Text h -> Text) r
						 )

maybeRight :: Either l r -> Maybe r
maybeRight (Right r) = Just r
maybeRight Left{}    = Nothing