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