{-# 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.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_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)
 , Gram_Term_AtomsR meta ts ts (P.ParsecT e s m)
 , Inj_Token meta ts (->)
 , MC.MonadState (Tokenizers meta ts) m
 , Show_Token meta ts, Show meta
 ) => Gram_Term ts meta (P.ParsecT e s m) where
	tokenizers_get (Gram.CF g) = Gram.CF $ do
		toks <- MC.get
		f <- g
		return $ f toks
	tokenizers_put (Gram.CF g) = Gram.CF $ do
		(toks, a) <- g
		() <- MC.put toks
		return a

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 $ g_term <* Gram.eoi

test_compile
 :: forall is cs h.
 ( Compile cs is
 , Eq h
 , Eq_Token Meta is
 , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
 , Inj_Tokens Meta is [Proxy (->), Proxy Integer]
 , Show h
 , Show_Token Meta is
 , Show_TyConst cs
 , Sym_of_Ifaces is HostI
 , Sym_of_Ifaces is TextI
 , Tokenize Meta is
 , cs ~ TyConsts_of_Ifaces is
 ) => Text
 -> Either ( Type cs h
           , Either (P.ParseError Char P.Dec)
                    (Error_Term Meta cs is) )
           (Type cs 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 compileWithoutCtx tok of
		 Left err -> Left (Right err) @?= snd `left` expected
		 Right (ETermClosed typ (TermClosed te)) ->
			case expected of
			 Left (_, err) -> Right ("…"::Text) @?= Left err
			 Right (ty_expected::Type cs h, _::h, _::Text) ->
				(>>= (@?= (\(_::Type cs 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