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 import qualified Language.Symantic.Lib as Sym
  27
  28 import Parsing.Test
  29 import Typing.Test ()
  30
  31 type Meta = ()
  32
  33 ---
  34 -- P.ParsecT instances
  35 ---
  36 type instance MC.CanDo (P.ParsecT e s m) eff = 'False
  37 instance ParsecC e s => Gram_Name (P.ParsecT e s m)
  38 instance ParsecC e s => Gram.Gram_Meta Meta (P.ParsecT e s m) where
  39         metaG = (($ ()) <$>)
  40 instance
  41  ( ParsecC e s
  42  , Gram.Gram_Meta meta (P.ParsecT e s m)
  43  ) => Gram_Term_Type meta (P.ParsecT e s m)
  44 instance
  45  ( ParsecC e s
  46  ) => Gram_Error (P.ParsecT e s m) where
  47         term_unError (Gram.CF me) = Gram.CF $ do
  48                 e <- me
  49                 case e of
  50                  Left err -> fail $ show err
  51                  Right a -> return a
  52 instance
  53  ( ParsecC e s
  54  , Gram.Gram_Meta   meta       (P.ParsecT e s m)
  55  , Gram_Term_AtomsR meta ts ts (P.ParsecT e s m)
  56  , MC.MonadState (Tokenizers meta ts) m
  57  ) => Gram_Term ts meta (P.ParsecT e s m) where
  58         term_tokenizers (Gram.CF ma) = Gram.CF $ do
  59                 a <- ma
  60                 toks :: Tokenizers meta ts <- MC.get
  61                 return $ a toks
  62         g_term_abst_args_body (Gram.CF args) (Gram.CF body) = Gram.CF $ do
  63                 as <- args
  64                 bo <- do
  65                         toks :: Tokenizers meta ts <- MC.get
  66                         MC.put $
  67                                 Tokenizers
  68                                  { tokenizers_prefix  = del (tokenizers_prefix  toks) as
  69                                  , tokenizers_infix   = del (tokenizers_infix   toks) as
  70                                  , tokenizers_postfix = del (tokenizers_postfix toks) as
  71                                  }
  72                         body <* MC.put toks
  73                 return (as, bo)
  74                 where del = foldr $ \(n, _) -> Map.adjust (Map.delete n) []
  75
  76 test_tokenizer :: forall is.
  77  ( Inj_Tokens Meta is [Proxy (->), Proxy Integer]
  78  , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
  79  , Tokenize Meta is
  80  ) => Text -> Either (P.ParseError Char P.Dec) (EToken Meta is)
  81 test_tokenizer inp =
  82         runIdentity $
  83         MC.evalStateStrict (tokenizers::Tokenizers Meta is) $
  84         P.runParserT g "" inp
  85         where g = Gram.unCF $ g_term <* Gram.eoi
  86
  87 test_compile
  88  :: forall is cs h.
  89  ( Compile cs is
  90  , Eq h
  91  , Eq_Token Meta is
  92  , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
  93  , Inj_Tokens Meta is [Proxy (->), Proxy Integer]
  94  , Show h
  95  , Show_Token Meta is
  96  , Show_TyConst cs
  97  , Sym_of_Ifaces is HostI
  98  , Sym_of_Ifaces is TextI
  99  , Tokenize Meta is
 100  , cs ~ TyConsts_of_Ifaces is
 101  ) => Text
 102  -> Either ( Type cs h
 103            , Either (P.ParseError Char P.Dec)
 104                     (Error_Term Meta cs is) )
 105            (Type cs 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) @?= snd `left` expected
 111          Right tok ->
 112                 case compileWithoutCtx tok of
 113                  Left err -> Left (Right err) @?= snd `left` expected
 114                  Right (ETermClosed typ (TermClosed te)) ->
 115                         case expected of
 116                          Left (_, err) -> Right ("…"::Text) @?= Left err
 117                          Right (ty_expected::Type cs h, _::h, _::Text) ->
 118                                 (>>= (@?= (\(_::Type cs h, err) -> err) `left` expected)) $
 119                                 case typ `eq_Type` ty_expected of
 120                                  Nothing -> 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                                         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
 138
 139 elide :: Text -> String
 140 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
 141 elide s = Text.unpack s