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

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

import Control.Arrow (left)
import Data.Functor.Identity (Identity(..))
import Data.Text (Text)
import Data.Type.Equality
import Data.Void (Void)
import qualified Control.Monad.Classes.Run as MC
import qualified Control.Monad.Trans.State.Strict as S
import qualified Data.List as List
import qualified Data.Text as Text
import qualified Text.Megaparsec as P

import Language.Symantic.Grammar
import Language.Symantic
import Language.Symantic.Lib ()

import Testing.Megaparsec ()

type G src ss =
 P.ParsecT Void Text
           (S.StateT (Imports NameTe, Modules src ss)
                     ((S.StateT (Imports NameTy, ModulesTy src))
                                Identity))

parseTe ::
 forall ss src.
 ImportTypes ss =>
 ModulesTyInj ss =>
 ModulesInj src ss =>
 Gram_Term src ss (G src ss) =>
 Text -> Either (P.ParseError Char Void) (AST_Term src ss)
parseTe inp =
	let modsTe :: Modules src ss = either (error . show) id modulesInj in
	let impsTe = [] `importModules` modsTe in
	let modsTy = modulesTyInj @ss @src in
	let impsTy = importTypes @ss [] in
	runIdentity $
	MC.evalStateStrict (impsTy, modsTy) $
	MC.evalStateStrict (impsTe, modsTe) $
	P.runParserT g "" inp
	where g = unCF $ g_term <* eoi

readTe ::
 forall src ss t.
 ( Eq t
 , Eq src
 , Gram_Term src ss (G src ss)
 , ImportTypes ss
 , ModulesInj src ss
 , ModulesTyInj ss
 , Show src
 , Show t
 , SourceInj (AST_Type src) src
 , SourceInj (KindK src) src
 , SourceInj (TypeT src '[]) src
 , SourceInj (TypeVT src) src
 , Syms ss (BetaT View)
 , Syms ss Eval
 , Syms ss View
 ) =>
 Text ->
 Either ( Type src '[] t
        , Either (P.ParseError Char Void)
                 (Error_Term src) )
        (Type src '[] t, t, Text) ->
 TestTree
readTe inp expected =
	testCase (elide inp) $
	case reduceTeApp <$> parseTe @ss inp of
	 Left err -> Left (Left err) @?= snd `left` expected
	 Right ast ->
		case readTerm 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_proofless $ TypeVT t
						 Just Dict ->
							case t `eqType` ty_expected of
							 Nothing -> return $ Left $ Right $
								Error_Term_Beta $ Error_Beta_Unify $
								Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
							 Just Refl ->
								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