{-# 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_Meta (Gram.Text_of_Source src) (P.ParsecT e s m) , Gram.Gram_Meta src (P.ParsecT e s m) , Inj_Source (Gram.Text_of_Source src) src ) => 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 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 catch me = do e <- me case e of Left err -> fail $ show err Right a -> return a instance ( ParsecC e s , Show src , Gram.Gram_Meta (Gram.Text_of_Source src) (P.ParsecT e s m) , Gram.Gram_Meta src (P.ParsecT e s m) , Gram_Term_Atoms src ss (P.ParsecT e s m) , Gram.Gram_Error Error_Term_Gram (P.ParsecT e s m) , MC.MonadState (Modules src ss) m , Inj_Source (Gram.Text_of_Source src) src ) => Gram_Term src ss (P.ParsecT e s m) where modules_get (Gram.CF g) = Gram.CF $ do toks <- MC.get f <- g return $ f toks modules_put (Gram.CF g) = Gram.CF $ do (toks, a) <- g () <- MC.put toks return a 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 ast CtxTyZ 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