]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Compiling/Term/Test.hs
Fix Inj_ConstP -> Inj_TyConstP.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Compiling / Term / Test.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 module Compiling.Term.Test where
4
5 import Test.Tasty
6 import Test.Tasty.HUnit
7
8 import Control.Arrow
9 import qualified Control.Monad.Classes as MC
10 import qualified Control.Monad.Classes.Run as MC
11 import qualified Control.Monad.Trans.State.Strict as SS
12 import Data.Functor.Identity (Identity(..))
13 import qualified Data.Map.Strict as Map
14 import qualified Data.List as List
15 import Data.Proxy (Proxy(..))
16 import Data.Text (Text)
17 import qualified Data.Text as Text
18 import Data.Type.Equality ((:~:)(Refl))
19 import qualified Text.Megaparsec as P
20
21 import Language.Symantic.Compiling
22 import Language.Symantic.Interpreting
23 import Language.Symantic.Parsing
24 import qualified Language.Symantic.Grammar as Gram
25 import Language.Symantic.Typing
26
27 import Parsing.Test
28 import Typing.Test ()
29
30 type Meta = ()
31
32 ---
33 -- P.ParsecT instances
34 ---
35 type instance MC.CanDo (P.ParsecT e s m) eff = 'False
36 instance ParsecC e s => Gram_Term_Name (P.ParsecT e s m)
37 instance ParsecC e s => Gram.Gram_Meta Meta (P.ParsecT e s m) where
38 metaG = (($ ()) <$>)
39 instance
40 ( ParsecC e s
41 , Gram.Gram_Meta meta (P.ParsecT e s m)
42 ) => Gram_Term_Type meta (P.ParsecT e s m)
43 instance
44 ( ParsecC e s
45 ) => Gram_Error (P.ParsecT e s m) where
46 term_unError (Gram.CF me) = Gram.CF $ do
47 e <- me
48 case e of
49 Left err -> fail $ show err
50 Right a -> return a
51 instance
52 ( ParsecC e s
53 , Gram.Gram_Meta meta (P.ParsecT e s m)
54 , Gram_Term_AtomsR meta ts ts (P.ParsecT e s m)
55 , MC.MonadState (Tokenizers meta ts) m
56 ) => Gram_Term ts meta (P.ParsecT e s m) where
57 term_tokenizers (Gram.CF ma) = Gram.CF $ do
58 a <- ma
59 toks :: Tokenizers meta ts <- MC.get
60 return $ a toks
61 term_abst_args_body (Gram.CF args) (Gram.CF body) = Gram.CF $ do
62 as <- args
63 bo <- do
64 toks :: Tokenizers meta ts <- MC.get
65 MC.put $
66 Tokenizers
67 { tokenizers_prefix = del (tokenizers_prefix toks) as
68 , tokenizers_infix = del (tokenizers_infix toks) as
69 , tokenizers_postfix = del (tokenizers_postfix toks) as
70 }
71 body <* MC.put toks
72 return (as, bo)
73 where del = foldr $ \(n, _) -> Map.adjust (Map.delete n) []
74
75 test_tokenizer :: forall is.
76 ( Inj_Tokens Meta is [Proxy (->), Proxy Integer]
77 , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
78 , Tokenize Meta is
79 ) => Text -> Either (P.ParseError Char P.Dec) (EToken Meta is)
80 test_tokenizer inp =
81 runIdentity $
82 MC.evalStateStrict (tokenizers::Tokenizers Meta is) $
83 P.runParserT g "" inp
84 where g = Gram.unCF $ termG <* Gram.eoi
85
86 test_compile
87 :: forall is h.
88 ( Compile is
89 , Eq h
90 , Eq_Token Meta is
91 , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
92 , Inj_Tokens Meta is [Proxy (->), Proxy Integer]
93 , Show h
94 , Show_Token Meta is
95 , Show_TyConst (TyConsts_of_Ifaces is)
96 , Sym_of_Ifaces is HostI
97 , Sym_of_Ifaces is TextI
98 , Tokenize Meta is
99 ) => Text
100 -> Either ( Type (TyConsts_of_Ifaces is) h
101 , Either (P.ParseError Char P.Dec)
102 (Error_Term Meta is) )
103 (Type (TyConsts_of_Ifaces is) h, h, Text)
104 -> TestTree
105 test_compile inp expected =
106 testCase (elide inp) $
107 case test_tokenizer inp of
108 Left err -> Left (Left err) @?= snd `left` expected
109 Right tok ->
110 case compile tok of
111 Left err -> Left (Right err) @?= snd `left` expected
112 Right (ETerm typ (Term te)) ->
113 case expected of
114 Left (_, err) -> Right ("…"::Text) @?= Left err
115 Right (ty_expected::Type (TyConsts_of_Ifaces is) h, _::h, _::Text) ->
116 (>>= (@?= (\(_::Type (TyConsts_of_Ifaces is) h, err) -> err) `left` expected)) $
117 case typ `eq_Type` ty_expected of
118 Nothing -> return $ Left $ Right $
119 Error_Term_Con_Type $ Right $
120 Con_TyEq
121 (Right $ At Nothing $ EType typ)
122 (At Nothing $ EType ty_expected)
123 Just Refl -> do
124 let h = host_from_term te
125 return $
126 Right
127 ( typ
128 , h
129 , text_from_term te
130 -- , (text_from_term :: Repr_Text h -> Text) r
131 )
132
133 maybeRight :: Either l r -> Maybe r
134 maybeRight (Right r) = Just r
135 maybeRight Left{} = Nothing
136
137 elide :: Text -> String
138 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
139 elide s = Text.unpack s