1 {-# LANGUAGE FlexibleContexts #-}
5 import Test.Tasty.HUnit
8 import Language.LOL.Symantic.AST
9 import Language.LOL.Symantic.Type
12 tests = testGroup "Type" $
13 let (==>) ast expected p =
15 (@?= Exists_Type <$> expected) $
16 type_from p ast (Right . Exists_Type) in
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" []]
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))
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" []]
47 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
48 (Proxy :: Proxy (Type_Fun_Bool lam))
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" []]
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))
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" []]
80 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
81 (Proxy :: Proxy (Type_Fun_Int lam))
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" []]
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))