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_Source src (P.ParsecT e s m)
  39  ) => Gram_Term_Type src (P.ParsecT e s m)
  40 instance ParsecC e s => Gram.Gram_Error (Error_Term_Gram) (P.ParsecT e s m) where
  41         g_catch me = do
  42                 e <- me
  43                 case e of
  44                  Left err -> fail $ show err
  45                  Right a -> return a
  46 instance
  47  ( ParsecC e s
  48  , Source src, Show src
  49  ) => Gram.Gram_Error (Error_Term src) (P.ParsecT e s m) where
  50         g_catch me = do
  51                 e <- me
  52                 case e of
  53                  Left err -> fail $ show err
  54                  Right a -> return a
  55 instance
  56  ( ParsecC e s
  57  , Gram.Gram_Source src            (P.ParsecT e s m)
  58  , Gram.Gram_Error Error_Term_Gram (P.ParsecT e s m)
  59  , Gram_Term_Atoms src ss          (P.ParsecT e s m)
  60  , Gram_State (Modules src ss)     (P.ParsecT e s m)
  61  ) => Gram_Term src ss (P.ParsecT e s m)
  62
  63 test_modules ::
  64  forall ss src.
  65  Inj_Modules src ss =>
  66  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity)) =>
  67  Text ->
  68  Either (P.ParseError Char P.Dec) (AST_Term src ss)
  69 test_modules inp =
  70         runIdentity $
  71         MC.evalStateStrict (inj_Modules::Modules src ss) $
  72         P.runParserT g "" inp
  73         where g = Gram.unCF $ g_term <* Gram.eoi
  74
  75 test_readTe ::
  76  forall src ss t.
  77  ( Eq t
  78  , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity))
  79  , Show t
  80  , Syms ss Eval
  81  , Syms ss View
  82  , Syms ss (BetaT View)
  83  , Inj_Modules src ss
  84  , Eq src
  85  , Show src
  86  , Inj_Source (TypeVT src) src
  87  , Inj_Source (TypeT src '[]) src
  88  , Inj_Source (KindK src) src
  89  , Inj_Source (AST_Type src) src
  90  , Inj_Name2Type ss
  91  ) =>
  92  Text ->
  93  Either ( Type src '[] t
  94         , Either (P.ParseError Char P.Dec)
  95                  (Error_Term src) )
  96         (Type src '[] t, t, Text) ->
  97  TestTree
  98 test_readTe inp expected =
  99         testCase (elide inp) $
 100         case reduceTeApp <$> test_modules @ss inp of
 101          Left err -> Left (Left err) @?= snd `left` expected
 102          Right ast ->
 103                 let tys = inj_Name2Type (Proxy @ss) in
 104                 case readTe tys CtxTyZ ast of
 105                  Left err -> Left (Right err) @?= snd `left` expected
 106                  Right term ->
 107                         case term of
 108                          TermVT (Term q t (TeSym te)) ->
 109                                 case expected of
 110                                  Left (_, err) -> Right ("…"::Text) @?= Left err
 111                                  Right (ty_expected::Type src '[] t, _::t, _::Text) ->
 112                                         (>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
 113                                         case lenVars t of
 114                                          LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
 115                                          LenZ ->
 116                                                 case proveConstraint q of
 117                                                  Nothing -> return $ Left $ Right $ Error_Term_qualified $ TypeVT t
 118                                                  Just Dict -> do
 119                                                         case t `eqTy` ty_expected of
 120                                                          Nothing -> return $ Left $ Right $
 121                                                                 Error_Term_Beta $ Error_Beta_Unify $
 122                                                                 Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
 123                                                          Just Refl -> do
 124                                                                 return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
 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
 133
 134 dbg :: Show a => String -> a -> a
 135 dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x