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