]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Typing/Test.hs
Clarification : Megaparsec integration.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Typing / Test.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 module Typing.Test where
4
5 import Test.Tasty
6 import Test.Tasty.HUnit
7
8 import Control.Applicative (Applicative(..))
9 import Control.Arrow (left)
10 import Data.Map.Strict (Map)
11 import Data.Maybe (isJust)
12 import Data.NonNull (NonNull)
13 import Data.Proxy
14 import Data.Ratio (Ratio)
15 import Data.Text (Text)
16 import Data.List.NonEmpty (NonEmpty)
17 import GHC.Exts (Constraint)
18 import Prelude hiding (exp)
19 import qualified Data.Function as Fun
20 import qualified Data.Map.Strict as Map
21 import qualified Data.MonoTraversable as MT
22 import qualified Data.Sequences as Seqs
23 import qualified System.IO as IO
24 import qualified Text.Megaparsec as P
25
26 import Language.Symantic.Grammar
27 import Language.Symantic
28 import Language.Symantic.Lib hiding ((<$>), (<*), show)
29
30 import Grammar.Megaparsec ()
31
32 -- * Tests
33 type SS =
34 [ Proxy (->)
35 , Proxy Bool
36 , Proxy []
37 , Proxy ()
38 , Proxy (,)
39 , Proxy Char
40 , Proxy Either
41 , Proxy Int
42 , Proxy Integer
43 , Proxy IO
44 , Proxy IO.Handle
45 , Proxy IO.IOMode
46 , Proxy Ordering
47 , Proxy Map
48 , Proxy Maybe
49 , Proxy NonNull
50 , Proxy Ratio
51 , Proxy Text
52 , Proxy Applicative
53 , Proxy Bounded
54 , Proxy Enum
55 , Proxy Eq
56 , Proxy Foldable
57 , Proxy Functor
58 , Proxy Integral
59 , Proxy Monad
60 , Proxy Monoid
61 , Proxy MT.MonoFoldable
62 , Proxy MT.MonoFunctor
63 , Proxy Num
64 , Proxy Ord
65 , Proxy Real
66 , Proxy Seqs.IsSequence
67 , Proxy Seqs.SemiSequence
68 , Proxy Show
69 , Proxy Traversable
70 ]
71 type SRC = SrcTe (NonEmpty P.SourcePos) SS
72
73 cs :: Source src => Name2Type src
74 cs =
75 Map.insert "String"
76 (Len2Type $ \len -> TypeT $
77 tyConstLen @(K []) @[] len `tyApp`
78 tyConstLen @(K Char) @Char len) $
79 inj_Name2Type (Proxy @SS)
80
81 tests :: TestTree
82 tests = testGroup "Typing" $
83 [ testGroup "readType" $
84 let run inp (TypeT exp :: TypeT SRC '[]) =
85 testCase inp $ got @?= Right (Right $ TypeVT exp)
86 where
87 got :: Either (P.ParseError Char P.Dec)
88 (Either (Error_Type SRC) (TypeVT SRC))
89 got = readType cs <$> P.runParser (unCF g) "" inp
90 g :: Gram_Type SRC g => CF g (AST_Type SRC)
91 g = g_type <* eoi in
92 let (==>) = run; infixr 0 ==> in
93 [ "Bool" ==> TypeT $ tyBool
94 , "(->) Bool" ==> TypeT $ tyFun `tyApp` tyBool
95 , "[]" ==> TypeT $ tyConst @(K []) @[]
96 , "[Char]" ==> TypeT $ tyList tyChar
97 , "[Char -> [Char]]" ==> TypeT $ tyList (tyChar ~> tyList tyChar)
98 , "([])" ==> TypeT $ tyConst @(K []) @[]
99 , "[()]" ==> TypeT $ tyList tyUnit
100 , "()" ==> TypeT $ tyUnit
101 , "(())" ==> TypeT $ tyUnit
102 , "(,)" ==> TypeT $ tyConst @(K (,)) @(,)
103 , "((,))" ==> TypeT $ tyConst @(K (,)) @(,)
104 , "(,) Int" ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
105 , "(Bool)" ==> TypeT $ tyBool
106 , "((Bool))" ==> TypeT $ tyBool
107 , "(Bool, Int)" ==> TypeT $ tyBool `tyTuple2` tyInt
108 , "((Bool, Int))" ==> TypeT $ tyBool `tyTuple2` tyInt
109 , "((Bool, Int), Char)" ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
110 , "(Bool, Int) -> Char" ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
111 , "(Bool -> Int)" ==> TypeT $ tyBool ~> tyInt
112 , "String" ==> TypeT $ tyList tyChar
113 , "[Char] -> String" ==> TypeT $ tyList tyChar ~> tyList tyChar
114 , "String -> [Char]" ==> TypeT $ tyList tyChar ~> tyList tyChar
115 , "Maybe Bool" ==> TypeT $ tyMaybe tyBool
116 , "Either Bool Int" ==> TypeT $ tyEither tyBool tyInt
117 , "Bool -> Int" ==> TypeT $ tyBool ~> tyInt
118 , "(Bool -> Int) -> Char" ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
119 , "Bool -> (Int -> Char)" ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
120 , "Bool -> Int -> Char" ==> TypeT $ tyBool ~> tyInt ~> tyChar
121 , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
122 , "IO" ==> TypeT $ tyConst @(K IO) @IO
123 , "Traversable IO" ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
124 , "Monad IO" ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
125 , "(->) (IO Bool)" ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
126 , "Monad IO" ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
127 , "Eq" ==> TypeT $ tyConst @(K Eq) @Eq
128 , "Eq Bool" ==> TypeT $ tyEq tyBool
129 ]
130 , testGroup "Parsing errors" $
131 let run inp = testCase inp $ got @?= Left ()
132 where
133 got :: Either () (AST_Type SRC)
134 got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
135 g :: Gram_Type SRC g => CF g (AST_Type SRC)
136 g = g_type <* eoi in
137 run <$>
138 [ "Bool, Int"
139 , "(Bool -> Int) Char"
140 ]
141 , testGroup "Compiling errors" $
142 let run inp = testCase inp $ got @?= Right (Left ())
143 where
144 got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
145 got = left (Fun.const ()) . readType cs <$> P.runParser (unCF g) "" inp
146 g :: Gram_Type SRC g => CF g (AST_Type SRC)
147 g = g_type <* eoi in
148 run <$>
149 [ "NonExistingType"
150 , "Bool Int"
151 , "[IO]"
152 , "(->) IO"
153 , "(->) Bool Int Char"
154 , "Monad Eq"
155 ]
156 , testGroup "proveConstraint" $
157 let (==>) (typ::Type SRC '[] (t::Constraint)) expected =
158 testCase (show typ) $
159 isJust (proveConstraint typ) @?= expected in
160 [ tyEq tyBool ==> True
161 , tyOrd tyBool ==> True
162 , tyFunctor (tyConst @(K Maybe) @Maybe) ==> True
163 , tyFunctor (tyConst @(K IO) @IO) ==> True
164 , tyMonad (tyConst @(K IO) @IO) ==> True
165 , tyTraversable (tyConst @(K IO) @IO) ==> False
166 ]
167 ]