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.List as List
  14 import Data.Proxy (Proxy(..))
  15 import Data.Text (Text)
  16 import qualified Data.Text as Text
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import qualified Text.Megaparsec as P
  19
  20 import Language.Symantic.Compiling
  21 import Language.Symantic.Interpreting
  22 import Language.Symantic.Parsing
  23 import qualified Language.Symantic.Grammar as Gram
  24 import Language.Symantic.Typing
  25
  26 import Parsing.Test
  27 import Typing.Test ()
  28
  29 type Meta = ()
  30
  31 ---
  32 -- P.ParsecT instances
  33 ---
  34 type instance MC.CanDo (P.ParsecT e s m) eff = 'False
  35 instance ParsecC e s => Gram_Name (P.ParsecT e s m)
  36 instance ParsecC e s => Gram.Gram_Meta Meta (P.ParsecT e s m) where
  37         metaG = (($ ()) <$>)
  38 instance
  39  ( ParsecC e s
  40  , Gram.Gram_Meta meta (P.ParsecT e s m)
  41  ) => Gram_Term_Type meta (P.ParsecT e s m)
  42 instance
  43  ( ParsecC e s
  44  ) => Gram_Error (P.ParsecT e s m) where
  45         term_unError (Gram.CF me) = Gram.CF $ do
  46                 e <- me
  47                 case e of
  48                  Left err -> fail $ show err
  49                  Right a -> return a
  50 instance
  51  ( ParsecC e s
  52  , Gram.Gram_Meta   meta       (P.ParsecT e s m)
  53  , Gram_Term_AtomsR meta ts ts (P.ParsecT e s m)
  54  , Inj_Token meta ts (->)
  55  , MC.MonadState (Tokenizers meta ts) m
  56  , Show_Token meta ts, Show meta
  57  ) => Gram_Term ts meta (P.ParsecT e s m) where
  58         tokenizers_get (Gram.CF g) = Gram.CF $ do
  59                 toks <- MC.get
  60                 f <- g
  61                 return $ f toks
  62         tokenizers_put (Gram.CF g) = Gram.CF $ do
  63                 (toks, a) <- g
  64                 () <- MC.put toks
  65                 return a
  66
  67 test_tokenizer :: forall is.
  68  ( Inj_Tokens Meta is [Proxy (->), Proxy Integer]
  69  , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
  70  , Tokenize Meta is
  71  ) => Text -> Either (P.ParseError Char P.Dec) (EToken Meta is)
  72 test_tokenizer inp =
  73         runIdentity $
  74         MC.evalStateStrict (tokenizers::Tokenizers Meta is) $
  75         P.runParserT g "" inp
  76         where g = Gram.unCF $ g_term <* Gram.eoi
  77
  78 test_compile
  79  :: forall is cs h.
  80  ( Compile cs is
  81  , Eq h
  82  , Eq_Token Meta is
  83  , Gram_Term is Meta (P.ParsecT P.Dec Text (SS.StateT (Tokenizers Meta is) Identity))
  84  , Inj_Tokens Meta is [Proxy (->), Proxy Integer]
  85  , Show h
  86  , Show_Token Meta is
  87  , Show_TyConst cs
  88  , Sym_of_Ifaces is HostI
  89  , Sym_of_Ifaces is TextI
  90  , Tokenize Meta is
  91  , cs ~ TyConsts_of_Ifaces is
  92  ) => Text
  93  -> Either ( Type cs h
  94            , Either (P.ParseError Char P.Dec)
  95                     (Error_Term Meta cs is) )
  96            (Type cs h, h, Text)
  97  -> TestTree
  98 test_compile inp expected =
  99         testCase (elide inp) $
 100         case test_tokenizer inp of
 101          Left err -> Left (Left err) @?= snd `left` expected
 102          Right tok ->
 103                 case compileWithoutCtx tok of
 104                  Left err -> Left (Right err) @?= snd `left` expected
 105                  Right (ETermClosed typ (TermClosed te)) ->
 106                         case expected of
 107                          Left (_, err) -> Right ("…"::Text) @?= Left err
 108                          Right (ty_expected::Type cs h, _::h, _::Text) ->
 109                                 (>>= (@?= (\(_::Type cs h, err) -> err) `left` expected)) $
 110                                 case typ `eq_Type` ty_expected of
 111                                  Nothing -> return $ Left $ Right $
 112                                         Error_Term_Con_Type $ Right $
 113                                         Con_TyEq
 114                                          (Right $ At Nothing $ EType typ)
 115                                          (At Nothing $ EType ty_expected)
 116                                  Just Refl -> do
 117                                         let h = host_from_term te
 118                                         return $
 119                                                 Right
 120                                                  ( typ
 121                                                  , h
 122                                                  , text_from_term te
 123                                                  -- , (text_from_term :: Repr_Text h -> Text) r
 124                                                  )
 125
 126 maybeRight :: Either l r -> Maybe r
 127 maybeRight (Right r) = Just r
 128 maybeRight Left{}    = Nothing
 129
 130 elide :: Text -> String
 131 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
 132 elide s = Text.unpack s