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

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