symantic-lib/test/Testing/Compiling.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE TypeInType #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Testing.Compiling 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 Data.Void (Void)
  17 import qualified Control.Monad.Classes.Run as MC
  18 import qualified Control.Monad.Trans.State.Strict as S
  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 Testing.Megaparsec ()
  28
  29 type G src ss =
  30  P.ParsecT Void Text
  31            (S.StateT (Imports NameTe, Modules src ss)
  32                      ((S.StateT (Imports NameTy, ModulesTy src))
  33                                 Identity))
  34
  35 parseTe ::
  36  forall ss src.
  37  ImportTypes ss =>
  38  ModulesTyInj ss =>
  39  ModulesInj src ss =>
  40  Gram_Term src ss (G src ss) =>
  41  Text -> Either (P.ParseError Char Void) (AST_Term src ss)
  42 parseTe inp =
  43         let modsTe :: Modules src ss = either (error . show) id modulesInj in
  44         let impsTe = [] `importModules` modsTe in
  45         let modsTy = modulesTyInj @ss @src in
  46         let impsTy = importTypes @ss [] in
  47         runIdentity $
  48         MC.evalStateStrict (impsTy, modsTy) $
  49         MC.evalStateStrict (impsTe, modsTe) $
  50         P.runParserT g "" inp
  51         where g = unCF $ g_term <* eoi
  52
  53 readTe ::
  54  forall src ss t.
  55  ( Eq t
  56  , Eq src
  57  , Gram_Term src ss (G src ss)
  58  , ImportTypes ss
  59  , ModulesInj src ss
  60  , ModulesTyInj ss
  61  , Show src
  62  , Show t
  63  , SourceInj (AST_Type src) src
  64  , SourceInj (KindK src) src
  65  , SourceInj (TypeT src '[]) src
  66  , SourceInj (TypeVT src) src
  67  , Syms ss (BetaT View)
  68  , Syms ss Eval
  69  , Syms ss View
  70  ) =>
  71  Text ->
  72  Either ( Type src '[] t
  73         , Either (P.ParseError Char Void)
  74                  (Error_Term src) )
  75         (Type src '[] t, t, Text) ->
  76  TestTree
  77 readTe inp expected =
  78         testCase (elide inp) $
  79         case reduceTeApp <$> parseTe @ss inp of
  80          Left err -> Left (Left err) @?= snd `left` expected
  81          Right ast ->
  82                 case readTerm CtxTyZ ast of
  83                  Left err -> Left (Right err) @?= snd `left` expected
  84                  Right term ->
  85                         case term of
  86                          TermVT (Term q t (TeSym te)) ->
  87                                 case expected of
  88                                  Left (_, err) -> Right ("…"::Text) @?= Left err
  89                                  Right (ty_expected::Type src '[] t, _::t, _::Text) ->
  90                                         (>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
  91                                         case lenVars t of
  92                                          LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
  93                                          LenZ ->
  94                                                 case proveConstraint q of
  95                                                  Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t
  96                                                  Just Dict ->
  97                                                         case t `eqType` ty_expected of
  98                                                          Nothing -> return $ Left $ Right $
  99                                                                 Error_Term_Beta $ Error_Beta_Unify $
 100                                                                 Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
 101                                                          Just Refl ->
 102                                                                 return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
 103
 104 maybeRight :: Either l r -> Maybe r
 105 maybeRight (Right r) = Just r
 106 maybeRight Left{}    = Nothing
 107
 108 elide :: Text -> String
 109 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
 110 elide s = Text.unpack s
 111
 112 dbg :: Show a => String -> a -> a
 113 dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x