Language/Symantic/Compiling/Term/Test.hs

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