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

import Test.Tasty
import Test.Tasty.HUnit

import Control.Arrow
import qualified Control.Monad.Classes as MC
import qualified Control.Monad.Classes.Run as MC
import qualified Control.Monad.Trans.State.Strict as SS
import Data.Functor.Identity (Identity(..))
import qualified Data.Map.Strict as Map
import qualified Data.List as List
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(Refl))
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 = (($ ()) <$>)
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 -> fail $ show err
		 Right a -> 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
		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 <* MC.put toks
		return (as, bo)
		where del = 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 Text (SS.StateT (Tokenizers Meta is) Identity))
 , Tokenize Meta is
 ) => Text -> Either (P.ParseError Char P.Dec) (EToken Meta is)
test_tokenizer inp =
	runIdentity $
	MC.evalStateStrict (tokenizers::Tokenizers Meta is) $
	P.runParserT g "" inp
	where g = Gram.unCF $ termG <* 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 Text (SS.StateT (Tokenizers Meta is) Identity))
 , Tokenize Meta is
 ) => Text
 -> 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) @?= snd `left` expected
	 Right tok ->
		case compile tok of
		 Left err -> Left (Right err) @?= snd `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) ->
				(>>= (@?= (\(_::Type (TyConsts_of_Ifaces is) h, err) -> err) `left` expected)) $
				case typ `eq_Type` ty_expected of
				 Nothing -> 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
					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

elide :: Text -> String
elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
elide s = Text.unpack s