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