]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Test.hs
init
[haskell/symantic.git] / 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 ]