Language/LOL/Symantic/Type/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 module Type.Test where
   3
   4 import Test.Tasty
   5 import Test.Tasty.HUnit
   6 import Data.Proxy
   7
   8 import Language.LOL.Symantic.Raw
   9 import Language.LOL.Symantic.Type
  10
  11 tests :: TestTree
  12 tests = testGroup "Type" $
  13         let (==>) raw expected p =
  14                 testCase (show raw) $
  15                 type_from p raw (Right . Exists_Type) @?=
  16                 (Exists_Type <$> expected) in
  17          [ testGroup "Fun_Bool" $
  18                  [ Raw "Bool" []
  19                    ==> Right (type_bool :: Type_Fun_Bool lam Bool) $
  20                    (Proxy :: Proxy (Type_Fun_Bool lam))
  21                  , Raw "->" [Raw "Bool" []]
  22                    ==> Left (Just $ error_type_lift $ Error_Type_Fun_Wrong_number_of_arguments 2 (Raw "->" [Raw "Bool" []])) $
  23                    (Proxy :: Proxy (Type_Fun_Bool lam))
  24                  , Raw "->" [Raw "Bool" [], Raw "Bool" []]
  25                    ==> Right (type_bool `type_fun` type_bool
  26                    :: Type_Fun_Bool lam (lam Bool -> lam Bool)) $
  27                    (Proxy :: Proxy (Type_Fun_Bool lam))
  28                  , Raw "->" [ Raw "->" [Raw "Bool" [], Raw "Bool" []]
  29                             , Raw "Bool" [] ]
  30                    ==> Right ((type_bool `type_fun` type_bool) `type_fun` type_bool
  31                    :: Type_Fun_Bool lam (lam (lam Bool -> lam Bool) -> lam Bool)) $
  32                    (Proxy :: Proxy (Type_Fun_Bool lam))
  33                  , Raw "->" [ Raw "Bool" []
  34                             , Raw "->" [Raw "Bool" [], Raw "Bool" []] ]
  35                    ==> Right (type_bool `type_fun` (type_bool `type_fun` type_bool)
  36                    :: Type_Fun_Bool lam (lam Bool -> lam (lam Bool -> lam Bool))) $
  37                    (Proxy :: Proxy (Type_Fun_Bool lam))
  38                  , Raw "Int" []
  39                    ==> Left Nothing $
  40                    (Proxy :: Proxy (Type_Fun_Bool lam))
  41                  , Raw "->" [Raw "Bool" [], Raw "Int" []]
  42                    ==> Left Nothing $
  43                    (Proxy :: Proxy (Type_Fun_Bool lam))
  44                  , Raw "->" [ Raw "->" [Raw "Int" [], Raw "Bool" []]
  45                             , Raw "Int" [] ]
  46                    ==> Left Nothing $
  47                    (Proxy :: Proxy (Type_Fun_Bool lam))
  48                  ]
  49          , testGroup "Fun_Bool_Int" $
  50                  [ Raw "Int"  []
  51                    ==> Right (type_int :: Type_Fun_Bool_Int lam Int) $
  52                    (Proxy :: Proxy (Type_Fun_Bool_Int lam))
  53                  , Raw "->" [Raw "Bool" [], Raw "Int" []]
  54                    ==> Right (type_bool `type_fun` type_int :: Type_Fun_Bool_Int lam (lam Bool -> lam Int)) $
  55                    (Proxy :: Proxy (Type_Fun_Bool_Int lam))
  56                  , Raw "->" [ Raw "->" [Raw "Int" [], Raw "Bool" []]
  57                             , Raw "Int" [] ]
  58                    ==> Right ((type_int `type_fun` type_bool) `type_fun` type_int
  59                    :: Type_Fun_Bool_Int lam (lam (lam Int -> lam Bool) -> lam Int)) $
  60                    (Proxy :: Proxy (Type_Fun_Bool_Int lam))
  61                  ]
  62          ]