Language/Symantic/Compiling/Term/Test.hs

   1 module Compiling.Term.Test where
   2
   3 import Test.Tasty
   4 import Test.Tasty.HUnit
   5
   6 import qualified Control.Arrow as Arrow
   7 import qualified Control.Monad as Monad
   8 -- import Control.Monad.IO.Class (MonadIO(..))
   9 import Data.Proxy (Proxy(..))
  10 import Data.Text (Text)
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude as P
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18
  19 import Parsing.Test
  20
  21 test_term_from
  22  :: forall ast is h.
  23  ( Eq h
  24  , Eq ast
  25  , Eq_Token ast is
  26  , Show ast
  27  , Show h
  28  , Show_Const (Consts_of_Ifaces is)
  29  , Show_Token ast is
  30  , Sym_of_Ifaces is HostI
  31  , Sym_of_Ifaces is TextI
  32  , Term_from is
  33  , Tokenize ast ast is
  34  ) => Proxy is
  35  -> ast
  36  -> Either (Type (Consts_of_Ifaces is) h, Either (Error_Syntax ast) (Error_Term ast is))
  37            (Type (Consts_of_Ifaces is) h, h, Text)
  38  -> TestTree
  39 test_term_from _is syn expected =
  40         testCase (elide $ show syn) $
  41         case tokenize syn of
  42          Left err -> Left (Left err) @?= P.snd `Arrow.left` expected
  43          Right (tok::EToken ast is) ->
  44                 case closed_term_from tok of
  45                  Left err -> Left (Right err) @?= P.snd `Arrow.left` expected
  46                  Right (ETerm typ (Term te)) ->
  47                         case expected of
  48                          Left (_, err) -> Right ("…"::Text) @?= Left err
  49                          Right (ty_expected::Type (Consts_of_Ifaces is) h, _::h, _::Text) ->
  50                                 (Monad.>>= (@?= (\(_::Type (Consts_of_Ifaces is) h, err) -> err) `Arrow.left` expected)) $
  51                                 case typ `eq_type` ty_expected of
  52                                  Nothing -> Monad.return $ Left $ Right $
  53                                         Error_Term_Constraint_Type $ Right $
  54                                         Constraint_Type_Eq
  55                                          (Right $ At Nothing $ EType typ)
  56                                          (At Nothing $ EType ty_expected)
  57                                  Just Refl -> do
  58                                         let h = host_from_term te
  59                                         Monad.return $
  60                                                 Right
  61                                                  ( typ
  62                                                  , h
  63                                                  , text_from_term te
  64                                                  -- , (text_from_term :: Repr_Text h -> Text) r
  65                                                  )
  66         where
  67                 elide s | P.length s P.> 42 = P.take 42 s P.++ ['…']
  68                 elide s = s