Test.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# 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.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.
 ModulesInj src ss =>
 Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports NameTe, 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 modulesInj in
	let imps = [] `importModules` 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 NameTe, Modules src ss) Identity))
 , Show t
 , Syms ss Eval
 , Syms ss View
 , Syms ss (BetaT View)
 , ModulesInj src ss
 , Eq src
 , Show src
 , SourceInj (TypeVT src) src
 , SourceInj (TypeT src '[]) src
 , SourceInj (KindK src) src
 , SourceInj (AST_Type src) src
 , ModulesTyInj ss
 , ImportTypes 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 modsTy = modulesTyInj @ss in
		let imps = importTypes @ss [] in
		case readTerm imps modsTy 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