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  ModulesInj src ss =>
  31  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports NameTe, 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 modulesInj in
  36         let imps = [] `importModules` 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 NameTe, Modules src ss) Identity))
  46  , Show t
  47  , Syms ss Eval
  48  , Syms ss View
  49  , Syms ss (BetaT View)
  50  , ModulesInj src ss
  51  , Eq src
  52  , Show src
  53  , SourceInj (TypeVT src) src
  54  , SourceInj (TypeT src '[]) src
  55  , SourceInj (KindK src) src
  56  , SourceInj (AST_Type src) src
  57  , ModulesTyInj ss
  58  , ImportTypes 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 modsTy = modulesTyInj @ss in
  72                 let imps = importTypes @ss [] in
  73                 case readTerm imps modsTy 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 ->
  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 ->
  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