{-# 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.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.Grammar
import Language.Symantic
import Language.Symantic.Lib ()

import Grammar.Megaparsec ()

test_parseTerm ::
 forall ss src.
 Inj_Modules src ss =>
 Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity)) =>
 Text ->
 Either (P.ParseError Char P.Dec) (AST_Term src ss)
test_parseTerm inp =
	let mods :: Modules src ss = either (error . show) id inj_Modules in
	let imps = importModulesAs [] mods in
	runIdentity $
	MC.evalStateStrict (imps, mods) $
	P.runParserT g "" inp
	where g = unCF $ g_term <* eoi

test_readTerm ::
 forall src ss t.
 ( Eq t
 , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, 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_readTerm inp expected =
	testCase (elide inp) $
	case reduceTeApp <$> test_parseTerm @ss inp of
	 Left err -> Left (Left err) @?= snd `left` expected
	 Right ast ->
		let tys = inj_Name2Type (Proxy @ss) in
		case readTerm 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_proofless $ TypeVT t
						 Just Dict -> do
							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 -> 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