{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Compiling.Applicative.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 Applicative ] 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 "Applicative" [ Syntax "<*>" [ syJust [Syntax "xor" [syTrue]] , syJust [syTrue] ] ==> Right (tyMaybe :$ tyBool, Just False, "Just (\\x0 -> True `xor` x0) <*> Just True") , Syntax "*>" [ syJust [syFalse] , syJust [syTrue] ] ==> Right (tyMaybe :$ tyBool, Just True, "Just False *> Just True") , Syntax "<*" [ syJust [syFalse] , syJust [syTrue] ] ==> Right (tyMaybe :$ tyBool, Just False, "Just False <* Just True") ]