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.Run as MC
  19 import qualified Control.Monad.Trans.State.Strict as SS
  20 import qualified Data.List as List
  21 import qualified Data.Text as Text
  22 import qualified Text.Megaparsec as P
  23
  24 import Language.Symantic.Grammar
  25 import Language.Symantic
  26 import Language.Symantic.Lib ()
  27
  28 import Grammar.Megaparsec ()
  29
  30 test_parseTerm ::
  31  forall ss src.
  32  Inj_Modules src ss =>
  33  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity)) =>
  34  Text ->
  35  Either (P.ParseError Char P.Dec) (AST_Term src ss)
  36 test_parseTerm inp =
  37         let mods :: Modules src ss = either (error . show) id inj_Modules in
  38         let imps = importModulesAs [] mods in
  39         runIdentity $
  40         MC.evalStateStrict (imps, mods) $
  41         P.runParserT g "" inp
  42         where g = unCF $ g_term <* eoi
  43
  44 test_readTerm ::
  45  forall src ss t.
  46  ( Eq t
  47  , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity))
  48  , Show t
  49  , Syms ss Eval
  50  , Syms ss View
  51  , Syms ss (BetaT View)
  52  , Inj_Modules src ss
  53  , Eq src
  54  , Show src
  55  , Inj_Source (TypeVT src) src
  56  , Inj_Source (TypeT src '[]) src
  57  , Inj_Source (KindK src) src
  58  , Inj_Source (AST_Type src) src
  59  , Inj_Name2Type ss
  60  ) =>
  61  Text ->
  62  Either ( Type src '[] t
  63         , Either (P.ParseError Char P.Dec)
  64                  (Error_Term src) )
  65         (Type src '[] t, t, Text) ->
  66  TestTree
  67 test_readTerm inp expected =
  68         testCase (elide inp) $
  69         case reduceTeApp <$> test_parseTerm @ss inp of
  70          Left err -> Left (Left err) @?= snd `left` expected
  71          Right ast ->
  72                 let tys = inj_Name2Type (Proxy @ss) in
  73                 case readTerm tys CtxTyZ ast of
  74                  Left err -> Left (Right err) @?= snd `left` expected
  75                  Right term ->
  76                         case term of
  77                          TermVT (Term q t (TeSym te)) ->
  78                                 case expected of
  79                                  Left (_, err) -> Right ("…"::Text) @?= Left err
  80                                  Right (ty_expected::Type src '[] t, _::t, _::Text) ->
  81                                         (>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
  82                                         case lenVars t of
  83                                          LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
  84                                          LenZ ->
  85                                                 case proveConstraint q of
  86                                                  Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t
  87                                                  Just Dict -> do
  88                                                         case t `eqType` ty_expected of
  89                                                          Nothing -> return $ Left $ Right $
  90                                                                 Error_Term_Beta $ Error_Beta_Unify $
  91                                                                 Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
  92                                                          Just Refl -> do
  93                                                                 return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
  94
  95 maybeRight :: Either l r -> Maybe r
  96 maybeRight (Right r) = Just r
  97 maybeRight Left{}    = Nothing
  98
  99 elide :: Text -> String
 100 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
 101 elide s = Text.unpack s
 102
 103 dbg :: Show a => String -> a -> a
 104 dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x