]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Typing/Test.hs
Add Parsing.Token.
[haskell/symantic.git] / Language / Symantic / Typing / Test.hs
1 {-# LANGUAGE TypeInType #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 module Typing.Test where
4
5 import Test.Tasty
6 import Test.Tasty.HUnit
7
8 import Data.Maybe (isJust)
9 import Data.Proxy
10 import Data.Text (Text)
11 import GHC.Exts (Constraint)
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16
17 import Parsing.Test
18
19 -- * Tests
20 tests :: TestTree
21 tests = testGroup "Typing" $
22 [ testGroup "type_from" $
23 let (==>) (syn::Syntax Text) expected =
24 let Right (tok::EToken (Syntax Text) '[Proxy Token_Type]) = tokenize_type syn in
25 testCase (show syn) $
26 (@?= EType Prelude.<$> expected) $
27 (type_from tok (Right . EType)
28 :: Either (Error_Type (Syntax Text) '[Proxy Token_Type])
29 (EType Constants))
30 in
31 [ sy @Bool ==> Right (ty @Bool)
32 , sy @IO [] ==> Right (ty @IO)
33 , sy @Eq [] ==> Right (ty @Eq)
34 , sy @(->) [sy @Bool] ==> Right (ty @(->) :$ ty @Bool)
35 , sy @Eq [sy @Bool] ==> Right (ty @Eq :$ ty @Bool)
36 , sy @Monad [sy @IO []] ==> Right (ty @Monad :$ ty @IO)
37 , sy @(->) [sy @IO [sy @Bool]] ==> Right (ty @(->) :$ (ty @IO :$ ty @Bool))
38 , (sy @Bool .> sy @Bool) ==> Right
39 (ty @Bool ~> ty @Bool)
40 , ((sy @Bool .> sy @Bool) .> sy @Bool) ==> Right
41 ((ty @Bool ~> ty @Bool) ~> ty @Bool)
42 , ((sy @Bool .> sy @Int) .> sy @Bool) ==> Right
43 ((ty @Bool ~> ty @Int) ~> ty @Bool)
44 , (sy @Bool .> sy @Int .> sy @Bool) ==> Right
45 (ty @Bool ~> ty @Int ~> ty @Bool)
46 , ((sy @Bool .> (sy @Bool .> sy @Int)) .> sy @Bool) ==> Right
47 ((ty @Bool ~> (ty @Bool ~> ty @Int)) ~> ty @Bool)
48 , testGroup "Error_Type"
49 [ sy @(->) [sy @IO []] ==> Left
50 (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
51 (At (maybeRight $ tokenize_type $ sy @(->) [sy @IO []]) $ EKind SKiType)
52 (At (maybeRight $ tokenize_type $ sy @IO []) $ EKind $ SKiType `SKiArrow` SKiType))
53 , sy @IO [sy @Eq [sy @Bool]] ==> Left
54 (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
55 (At (maybeRight $ tokenize_type $ sy @IO [sy @Eq [sy @Bool]]) $ EKind SKiType)
56 (At (maybeRight $ tokenize_type $ sy @Eq [sy @Bool]) $ EKind $ SKiConstraint))
57 , Syntax "Bool" [sy @Bool] ==> Left
58 (Error_Type_Constraint_Kind $ Constraint_Kind_Arrow
59 (At (maybeRight $ tokenize_type $ Syntax "Bool" [sy @Bool]) $ EKind SKiType))
60 , Syntax ("Unknown"::Text) [] ==> Left
61 (Error_Type_Constant_unknown $
62 At (maybeRight $ tokenize_type $ Syntax ("Unknown"::Text) []) "Unknown")
63 ]
64 ]
65 , testGroup "proj_con" $
66 let (==>) (typ::Type Constants (h::Constraint)) expected =
67 testCase (show_type typ) $
68 isJust (proj_con typ) @?= expected
69 in
70 [ (ty @Eq :$ ty @Bool) ==> True
71 , (ty @Ord :$ ty @Bool) ==> True
72 , (ty @Functor :$ ty @Maybe) ==> True
73 , (ty @Functor :$ ty @IO) ==> True
74 , (ty @Monad :$ ty @IO) ==> True
75 , (ty @Traversable :$ ty @IO) ==> False
76 ]
77 ]