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