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