{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Compiling.Functor.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 hiding ((&&), not, (||)) import Language.Symantic.Typing import Language.Symantic.Compiling import Language.Symantic.Interpreting -- * Tests type Ifaces = [ Proxy (->) , Proxy Bool , Proxy Maybe , Proxy Functor -- , Proxy Foldable -- , Proxy Traversable ] type Consts = Consts_of_Ifaces Ifaces (==>) (ast::Syntax Text) expected = testCase (show ast) $ case root_term_from ast of Left err -> Left err @?= Prelude.snd `Arrow.left` expected Right (ETerm ty (Term te)::ETerm Ifaces) -> case expected of Left (_, err) -> Right ("…"::Text) @?= Left err Right (ty_expected::Type Consts h, _::h, _::Text) -> (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $ case ty `eq_type` ty_expected of Nothing -> Monad.return $ Left $ Error_Term_Type_mismatch (At Nothing $ EType ty) (At Nothing $ EType ty_expected) Just Refl -> do let h = host_from_term te Monad.return $ Right ( ty , h , text_from_term te -- , (text_from_expr :: Repr_Text h -> Text) r ) tests :: TestTree tests = testGroup "Functor" [ Syntax "fmap" [ syLam (Syntax "x" []) syBool (Syntax "not" [Syntax "x" []]) , syJust [syTrue] ] ==> Right (tyMaybe :$ tyBool, Just False, "fmap (\\x0 -> (\\x1 -> not x1) x0) (Just True)") , Syntax "<$" [ syFalse , syJust [syTrue] ] ==> Right (tyMaybe :$ tyBool, Just False, "False <$ Just True") ]