{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Compiling.Test where

import Test.Tasty
import Test.Tasty.HUnit
import Debug.Trace (trace)

import Control.Arrow (left)
import Data.Functor.Identity (Identity(..))
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality
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 qualified Data.List as List
import qualified Data.Text as Text
import qualified Text.Megaparsec as P

import Language.Symantic
import qualified Language.Symantic.Grammar as Gram

import Grammar.Megaparsec
import Typing.Test ()

-- 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 () (P.ParsecT e s m) where
--	withMeta = (($ ()) <$>)
instance
 ( ParsecC e s
 , Gram.Gram_Source src (P.ParsecT e s m)
 ) => Gram_Term_Type src (P.ParsecT e s m)
instance ParsecC e s => Gram.Gram_Error (Error_Term_Gram) (P.ParsecT e s m) where
	g_catch me = do
		e <- me
		case e of
		 Left err -> fail $ show err
		 Right a -> return a
instance
 ( ParsecC e s
 , Source src, Show src
 ) => Gram.Gram_Error (Error_Term src) (P.ParsecT e s m) where
	g_catch me = do
		e <- me
		case e of
		 Left err -> fail $ show err
		 Right a -> return a
instance
 ( ParsecC e s
 , Gram.Gram_Source src            (P.ParsecT e s m)
 , Gram.Gram_Error Error_Term_Gram (P.ParsecT e s m)
 , Gram_Term_Atoms src ss          (P.ParsecT e s m)
 , Gram_State (Modules src ss)     (P.ParsecT e s m)
 ) => Gram_Term src ss (P.ParsecT e s m)

test_modules ::
 forall ss src.
 Inj_Modules src ss =>
 Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity)) =>
 Text ->
 Either (P.ParseError Char P.Dec) (AST_Term src ss)
test_modules inp =
	runIdentity $
	MC.evalStateStrict (inj_Modules::Modules src ss) $
	P.runParserT g "" inp
	where g = Gram.unCF $ g_term <* Gram.eoi

test_readTe ::
 forall src ss t.
 ( Eq t
 , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity))
 , Show t
 , Syms ss Eval
 , Syms ss View
 , Syms ss (BetaT View)
 , Inj_Modules src ss
 , Eq src
 , Show src
 , Inj_Source (TypeVT src) src
 , Inj_Source (TypeT src '[]) src
 , Inj_Source (KindK src) src
 , Inj_Source (AST_Type src) src
 , Inj_Name2Type ss
 ) =>
 Text ->
 Either ( Type src '[] t
        , Either (P.ParseError Char P.Dec)
                 (Error_Term src) )
        (Type src '[] t, t, Text) ->
 TestTree
test_readTe inp expected =
	testCase (elide inp) $
	case reduceTeApp <$> test_modules @ss inp of
	 Left err -> Left (Left err) @?= snd `left` expected
	 Right ast ->
		let tys = inj_Name2Type (Proxy @ss) in
		case readTe tys CtxTyZ ast of
		 Left err -> Left (Right err) @?= snd `left` expected
		 Right term ->
			case term of
			 TermVT (Term q t (TeSym te)) ->
				case expected of
				 Left (_, err) -> Right ("…"::Text) @?= Left err
				 Right (ty_expected::Type src '[] t, _::t, _::Text) ->
					(>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
					case lenVars t of
					 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
					 LenZ ->
						case proveConstraint q of
						 Nothing -> return $ Left $ Right $ Error_Term_qualified $ TypeVT t
						 Just Dict -> do
							case t `eqTy` ty_expected of
							 Nothing -> return $ Left $ Right $
								Error_Term_Beta $ Error_Beta_Unify $
								Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
							 Just Refl -> do
								return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)

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

dbg :: Show a => String -> a -> a
dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x