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_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         g_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 $ g_term <* Gram.eoi
  85
  86 test_compile
  87  :: forall is cs h.
  88  ( Compile cs 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 cs
  96  , Sym_of_Ifaces is HostI
  97  , Sym_of_Ifaces is TextI
  98  , Tokenize Meta is
  99  , cs ~ TyConsts_of_Ifaces is
 100  ) => Text
 101  -> Either ( Type cs h
 102            , Either (P.ParseError Char P.Dec)
 103                     (Error_Term Meta cs is) )
 104            (Type cs h, h, Text)
 105  -> TestTree
 106 test_compile inp expected =
 107         testCase (elide inp) $
 108         case test_tokenizer inp of
 109          Left err -> Left (Left err) @?= snd `left` expected
 110          Right tok ->
 111                 case compile tok of
 112                  Left err -> Left (Right err) @?= snd `left` expected
 113                  Right (ETerm typ (Term te)) ->
 114                         case expected of
 115                          Left (_, err) -> Right ("…"::Text) @?= Left err
 116                          Right (ty_expected::Type cs h, _::h, _::Text) ->
 117                                 (>>= (@?= (\(_::Type cs h, err) -> err) `left` expected)) $
 118                                 case typ `eq_Type` ty_expected of
 119                                  Nothing -> return $ Left $ Right $
 120                                         Error_Term_Con_Type $ Right $
 121                                         Con_TyEq
 122                                          (Right $ At Nothing $ EType typ)
 123                                          (At Nothing $ EType ty_expected)
 124                                  Just Refl -> do
 125                                         let h = host_from_term te
 126                                         return $
 127                                                 Right
 128                                                  ( typ
 129                                                  , h
 130                                                  , text_from_term te
 131                                                  -- , (text_from_term :: Repr_Text h -> Text) r
 132                                                  )
 133
 134 maybeRight :: Either l r -> Maybe r
 135 maybeRight (Right r) = Just r
 136 maybeRight Left{}    = Nothing
 137
 138 elide :: Text -> String
 139 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
 140 elide s = Text.unpack s