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