module Compiling.Term.Test where

import Test.Tasty
import Test.Tasty.HUnit

import qualified Control.Arrow as Arrow
import qualified Control.Monad as Monad
-- import Control.Monad.IO.Class (MonadIO(..))
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude as P

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting

import Parsing.Test

test_term_from
 :: forall ast is h.
 ( Eq h
 , Eq ast
 , Eq_Token ast is
 , Show ast
 , Show h
 , Show_Const (Consts_of_Ifaces is)
 , Show_Token ast is
 , Sym_of_Ifaces is HostI
 , Sym_of_Ifaces is TextI
 , Term_from is
 , Tokenize ast ast is
 ) => Proxy is
 -> ast
 -> Either (Type (Consts_of_Ifaces is) h, Either (Error_Syntax ast) (Error_Term ast is))
           (Type (Consts_of_Ifaces is) h, h, Text)
 -> TestTree
test_term_from _is syn expected =
	testCase (elide $ show syn) $
	case tokenize syn of
	 Left err -> Left (Left err) @?= P.snd `Arrow.left` expected
	 Right (tok::EToken ast is) ->
		case closed_term_from tok of
		 Left err -> Left (Right err) @?= P.snd `Arrow.left` expected
		 Right (ETerm typ (Term te)) ->
			case expected of
			 Left (_, err) -> Right ("…"::Text) @?= Left err
			 Right (ty_expected::Type (Consts_of_Ifaces is) h, _::h, _::Text) ->
				(Monad.>>= (@?= (\(_::Type (Consts_of_Ifaces is) h, err) -> err) `Arrow.left` expected)) $
				case typ `eq_type` ty_expected of
				 Nothing -> Monad.return $ Left $ Right $
					Error_Term_Constraint_Type $ Right $
					Constraint_Type_Eq
					 (Right $ At Nothing $ EType typ)
					 (At Nothing $ EType ty_expected)
				 Just Refl -> do
					let h = host_from_term te
					Monad.return $
						Right
						 ( typ
						 , h
						 , text_from_term te
						 -- , (text_from_term :: Repr_Text h -> Text) r
						 )
	where
		elide s | P.length s P.> 42 = P.take 42 s P.++ ['…']
		elide s = s