Language/Symantic/Type/Test.hs

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