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