Language/Symantic/Compiling/Functor/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.Functor.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 Functor
  32  -- , Proxy Foldable
  33  -- , Proxy Traversable
  34  ]
  35 type Consts = Consts_of_Ifaces Ifaces
  36
  37 (==>) (ast::Syntax Text) expected =
  38         testCase (show ast) $
  39         case root_term_from ast of
  40          Left err -> Left err @?= Prelude.snd `Arrow.left` expected
  41          Right (ETerm ty (Term te)::ETerm Ifaces) ->
  42                 case expected of
  43                  Left (_, err) -> Right ("…"::Text) @?= Left err
  44                  Right (ty_expected::Type Consts h, _::h, _::Text) ->
  45                         (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $
  46                         case ty `eq_type` ty_expected of
  47                          Nothing -> Monad.return $ Left $
  48                                 Error_Term_Type_mismatch
  49                                  (At Nothing $ EType ty)
  50                                  (At Nothing $ EType ty_expected)
  51                          Just Refl -> do
  52                                 let h = host_from_term te
  53                                 Monad.return $
  54                                         Right
  55                                          ( ty
  56                                          , h
  57                                          , text_from_term te
  58                                          -- , (text_from_expr :: Repr_Text h -> Text) r
  59                                          )
  60
  61 tests :: TestTree
  62 tests = testGroup "Functor"
  63  [ Syntax "fmap"
  64          [ syLam (Syntax "x" []) syBool
  65                  (Syntax "not" [Syntax "x" []])
  66          , syJust [syTrue]
  67          ] ==> Right (tyMaybe :$ tyBool, Just False, "fmap (\\x0 -> (\\x1 -> not x1) x0) (Just True)")
  68  , Syntax "<$"
  69          [ syFalse
  70          , syJust [syTrue]
  71          ] ==> Right (tyMaybe :$ tyBool, Just False, "False <$ Just True")
  72  ]