symantic-lib/Language/Symantic/Compiling/Test.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE TypeInType #-}
   4 {-# LANGUAGE ViewPatterns #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Compiling.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11 import Debug.Trace (trace)
  12
  13 import Control.Arrow (left)
  14 import Data.Functor.Identity (Identity(..))
  15 import Data.Proxy (Proxy(..))
  16 import Data.Text (Text)
  17 import Data.Type.Equality
  18 import qualified Control.Monad.Classes as MC
  19 import qualified Control.Monad.Classes.Run as MC
  20 import qualified Control.Monad.Trans.State.Strict as SS
  21 import qualified Data.List as List
  22 import qualified Data.Text as Text
  23 import qualified Text.Megaparsec as P
  24
  25 import Language.Symantic
  26 import qualified Language.Symantic.Grammar as Gram
  27
  28 import Grammar.MegaParsec
  29 import Typing.Test ()
  30
  31 -- P.ParsecT instances
  32 type instance MC.CanDo (P.ParsecT e s m) eff = 'False
  33 instance ParsecC e s => Gram_Name (P.ParsecT e s m)
  34 instance ParsecC e s => Gram.Gram_Meta () (P.ParsecT e s m) where
  35         withMeta = (($ ()) <$>)
  36 instance
  37  ( ParsecC e s
  38  , Gram.Gram_Meta (Gram.Text_of_Source src) (P.ParsecT e s m)
  39  , Gram.Gram_Meta src (P.ParsecT e s m)
  40  , Inj_Source (Gram.Text_of_Source src) src
  41  ) => Gram_Term_Type src (P.ParsecT e s m)
  42 instance ParsecC e s => Gram.Gram_Error (Error_Term_Gram) (P.ParsecT e s m) where
  43         catch me = do
  44                 e <- me
  45                 case e of
  46                  Left err -> fail $ show err
  47                  Right a -> return a
  48 instance
  49  ( ParsecC e s
  50  , Source src, Show src
  51  ) => Gram.Gram_Error (Error_Term src) (P.ParsecT e s m) where
  52         catch me = do
  53                 e <- me
  54                 case e of
  55                  Left err -> fail $ show err
  56                  Right a -> return a
  57 instance
  58  ( ParsecC e s
  59  , Show src
  60  , Gram.Gram_Meta (Gram.Text_of_Source src) (P.ParsecT e s m)
  61  , Gram.Gram_Meta src (P.ParsecT e s m)
  62  , Gram_Term_Atoms src ss (P.ParsecT e s m)
  63  , Gram.Gram_Error Error_Term_Gram (P.ParsecT e s m)
  64  , MC.MonadState (Modules src ss) m
  65  , Inj_Source (Gram.Text_of_Source src) src
  66  ) => Gram_Term src ss (P.ParsecT e s m) where
  67         modules_get (Gram.CF g) = Gram.CF $ do
  68                 toks <- MC.get
  69                 f <- g
  70                 return $ f toks
  71         modules_put (Gram.CF g) = Gram.CF $ do
  72                 (toks, a) <- g
  73                 () <- MC.put toks
  74                 return a
  75
  76 test_modules ::
  77  forall ss src.
  78  Inj_Modules src ss =>
  79  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity)) =>
  80  Text ->
  81  Either (P.ParseError Char P.Dec) (AST_Term src ss)
  82 test_modules inp =
  83         runIdentity $
  84         MC.evalStateStrict (inj_modules::Modules src ss) $
  85         P.runParserT g "" inp
  86         where g = Gram.unCF $ g_term <* Gram.eoi
  87
  88 test_readTe ::
  89  forall src ss t.
  90  ( Eq t
  91  , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity))
  92  , Show t
  93  , Syms ss Eval
  94  , Syms ss View
  95  , Syms ss (BetaT View)
  96  , Inj_Modules src ss
  97  , Eq src
  98  , Show src
  99  , Inj_Source (TypeVT src) src
 100  , Inj_Source (TypeT src '[]) src
 101  , Inj_Source (KindK src) src
 102  , Inj_Source (AST_Type src) src
 103  , Inj_Name2Type ss
 104  ) =>
 105  Text ->
 106  Either ( Type src '[] t
 107         , Either (P.ParseError Char P.Dec)
 108                  (Error_Term src) )
 109         (Type src '[] t, t, Text) ->
 110  TestTree
 111 test_readTe inp expected =
 112         testCase (elide inp) $
 113         case reduceTeApp <$> test_modules @ss inp of
 114          Left err -> Left (Left err) @?= snd `left` expected
 115          Right ast ->
 116                 let tys = inj_Name2Type (Proxy @ss) in
 117                 case readTe tys ast CtxTyZ of
 118                  Left err -> Left (Right err) @?= snd `left` expected
 119                  Right term ->
 120                         case term of
 121                          TermVT (Term q t (TeSym te)) ->
 122                                 case expected of
 123                                  Left (_, err) -> Right ("…"::Text) @?= Left err
 124                                  Right (ty_expected::Type src '[] t, _::t, _::Text) ->
 125                                         (>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
 126                                         case lenVars t of
 127                                          LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
 128                                          LenZ ->
 129                                                 case proveConstraint q of
 130                                                  Nothing -> return $ Left $ Right $ Error_Term_qualified $ TypeVT t
 131                                                  Just Dict -> do
 132                                                         case t `eqTy` ty_expected of
 133                                                          Nothing -> return $ Left $ Right $
 134                                                                 Error_Term_Beta $ Error_Beta_Unify $
 135                                                                 Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
 136                                                          Just Refl -> do
 137                                                                 return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
 138
 139 maybeRight :: Either l r -> Maybe r
 140 maybeRight (Right r) = Just r
 141 maybeRight Left{}    = Nothing
 142
 143 elide :: Text -> String
 144 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
 145 elide s = Text.unpack s
 146
 147 dbg :: Show a => String -> a -> a
 148 dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x