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_compile :: 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 , Compile 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_compile _is syn expected = testCase (elide $ P.show syn) $ case tokenize syn of Left err -> Left (Left err) @?= P.snd `Arrow.left` expected Right (tok::EToken ast is) -> case compile 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