Language/Symantic/Compiling/Applicative/Test.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE NoMonomorphismRestriction #-}
   5 {-# LANGUAGE Rank2Types #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeOperators #-}
   8 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   9 module Compiling.Applicative.Test where
  10
  11 import Test.Tasty
  12 import Test.Tasty.HUnit
  13
  14 import qualified Control.Arrow as Arrow
  15 import qualified Control.Monad as Monad
  16 -- import Control.Monad.IO.Class (MonadIO(..))
  17 import Data.Proxy (Proxy(..))
  18 import Data.Text (Text)
  19 import Data.Type.Equality ((:~:)(Refl))
  20 import Prelude hiding ((&&), not, (||))
  21
  22 import Language.Symantic.Typing
  23 import Language.Symantic.Compiling
  24 import Language.Symantic.Interpreting
  25
  26 -- * Tests
  27 type Ifaces =
  28  [ Proxy (->)
  29  , Proxy Bool
  30  , Proxy Maybe
  31  , Proxy Applicative
  32  ]
  33 type Consts = Consts_of_Ifaces Ifaces
  34
  35 (==>) (ast::Syntax Text) expected =
  36         testCase (show ast) $
  37         case root_term_from ast of
  38          Left err -> Left err @?= Prelude.snd `Arrow.left` expected
  39          Right (ETerm ty (Term te)::ETerm Ifaces) ->
  40                 case expected of
  41                  Left (_, err) -> Right ("…"::Text) @?= Left err
  42                  Right (ty_expected::Type Consts h, _::h, _::Text) ->
  43                         (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $
  44                         case ty `eq_type` ty_expected of
  45                          Nothing -> Monad.return $ Left $
  46                                 Error_Term_Type_mismatch
  47                                  (At Nothing $ EType ty)
  48                                  (At Nothing $ EType ty_expected)
  49                          Just Refl -> do
  50                                 let h = host_from_term te
  51                                 Monad.return $
  52                                         Right
  53                                          ( ty
  54                                          , h
  55                                          , text_from_term te
  56                                          -- , (text_from_expr :: Repr_Text h -> Text) r
  57                                          )
  58
  59 tests :: TestTree
  60 tests = testGroup "Applicative"
  61  [ Syntax "<*>"
  62          [ syJust [Syntax "xor" [syTrue]]
  63          , syJust [syTrue]
  64          ] ==> Right (tyMaybe :$ tyBool, Just False, "(\\x0 -> Just ((\\x1 -> (\\x2 -> x1 `xor` x2)) True) <*> x0) (Just True)")
  65  , Syntax "*>"
  66          [ syJust [syFalse]
  67          , syJust [syTrue]
  68          ] ==> Right (tyMaybe :$ tyBool, Just True, "Just False *> Just True")
  69  , Syntax "<*"
  70          [ syJust [syFalse]
  71          , syJust [syTrue]
  72          ] ==> Right (tyMaybe :$ tyBool, Just False, "Just False <* Just True")
  73  ]