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.AST
   9 import Language.LOL.Symantic.Type
  10
  11 tests :: TestTree
  12 tests = testGroup "Type" $
  13         let (==>) ast expected p =
  14                 testCase (show ast) $
  15                 (@?= Exists_Type <$> expected) $
  16                 type_from p ast (Right . Exists_Type) in
  17          [ testGroup "Bool"
  18                  [ AST "Bool" []
  19                          ==> Right (type_bool :: Type_Fun_Bool lam Bool) $
  20                          (Proxy :: Proxy (Type_Fun_Bool lam))
  21                  , AST "->" [AST "Bool" []]
  22                          ==> Left (error_type_lift $
  23                          Error_Type_Wrong_number_of_arguments (AST "->" [AST "Bool" []]) 2) $
  24                          (Proxy :: Proxy (Type_Fun_Bool lam))
  25                  , AST "->" [AST "Bool" [], AST "Bool" []]
  26                          ==> Right (type_bool `type_fun` type_bool
  27                          :: Type_Fun_Bool lam (lam Bool -> lam Bool)) $
  28                          (Proxy :: Proxy (Type_Fun_Bool lam))
  29                  , AST "->" [ AST "->" [AST "Bool" [], AST "Bool" []]
  30                                                                 , AST "Bool" [] ]
  31                          ==> Right ((type_bool `type_fun` type_bool) `type_fun` type_bool
  32                          :: Type_Fun_Bool lam (lam (lam Bool -> lam Bool) -> lam Bool)) $
  33                          (Proxy :: Proxy (Type_Fun_Bool lam))
  34                  , AST "->" [ AST "Bool" []
  35                                                                 , AST "->" [AST "Bool" [], AST "Bool" []] ]
  36                          ==> Right (type_bool `type_fun` (type_bool `type_fun` type_bool)
  37                          :: Type_Fun_Bool lam (lam Bool -> lam (lam Bool -> lam Bool))) $
  38                          (Proxy :: Proxy (Type_Fun_Bool lam))
  39                  , AST "Int" []
  40                          ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
  41                          (Proxy :: Proxy (Type_Fun_Bool lam))
  42                  , AST "->" [AST "Bool" [], AST "Int" []]
  43                          ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
  44                          (Proxy :: Proxy (Type_Fun_Bool lam))
  45                  , AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
  46                                                                 , AST "Int" [] ]
  47                          ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
  48                          (Proxy :: Proxy (Type_Fun_Bool lam))
  49                  ]
  50          , testGroup "Int"
  51                  [ AST "Int" []
  52                          ==> Right (type_int :: Type_Fun_Int lam Int) $
  53                          (Proxy :: Proxy (Type_Fun_Int lam))
  54                  , AST "->" [AST "Int" []]
  55                          ==> Left (error_type_lift $
  56                          Error_Type_Wrong_number_of_arguments (AST "->" [AST "Int" []]) 2) $
  57                          (Proxy :: Proxy (Type_Fun_Int lam))
  58                  , AST "->" [AST "Int" [], AST "Int" []]
  59                          ==> Right (type_int `type_fun` type_int
  60                          :: Type_Fun_Int lam (lam Int -> lam Int)) $
  61                          (Proxy :: Proxy (Type_Fun_Int lam))
  62                  , AST "->" [ AST "->" [AST "Int" [], AST "Int" []]
  63                                                                 , AST "Int" [] ]
  64                          ==> Right ((type_int `type_fun` type_int) `type_fun` type_int
  65                          :: Type_Fun_Int lam (lam (lam Int -> lam Int) -> lam Int)) $
  66                          (Proxy :: Proxy (Type_Fun_Int lam))
  67                  , AST "->" [ AST "Int" []
  68                                                                 , AST "->" [AST "Int" [], AST "Int" []] ]
  69                          ==> Right (type_int `type_fun` (type_int `type_fun` type_int)
  70                          :: Type_Fun_Int lam (lam Int -> lam (lam Int -> lam Int))) $
  71                          (Proxy :: Proxy (Type_Fun_Int lam))
  72                  , AST "Bool" []
  73                          ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
  74                          (Proxy :: Proxy (Type_Fun_Int lam))
  75                  , AST "->" [AST "Int" [], AST "Bool" []]
  76                          ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
  77                          (Proxy :: Proxy (Type_Fun_Int lam))
  78                  , AST "->" [ AST "->" [AST "Bool" [], AST "Int" []]
  79                                                                 , AST "Bool" [] ]
  80                          ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
  81                          (Proxy :: Proxy (Type_Fun_Int lam))
  82                  ]
  83          , testGroup "Fun" $
  84                  [ AST "Int"  []
  85                    ==> Right (type_int :: Type_Fun_Bool_Int lam Int) $
  86                    (Proxy :: Proxy (Type_Fun_Bool_Int lam))
  87                  , AST "->" [AST "Bool" [], AST "Int" []]
  88                    ==> Right (type_bool `type_fun` type_int
  89                    :: Type_Fun_Bool_Int lam (lam Bool -> lam Int)) $
  90                    (Proxy :: Proxy (Type_Fun_Bool_Int lam))
  91                  , AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
  92                             , AST "Int" [] ]
  93                    ==> Right ((type_int `type_fun` type_bool) `type_fun` type_int
  94                    :: Type_Fun_Bool_Int lam (lam (lam Int -> lam Bool) -> lam Int)) $
  95                    (Proxy :: Proxy (Type_Fun_Bool_Int lam))
  96                  ]
  97          ]