Language/Symantic/Compiling/Bool/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.Bool.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 hiding ((&&), not, (||))
  21
  22 import Language.Symantic.Typing
  23 import Language.Symantic.Compiling
  24 import Language.Symantic.Interpreting
  25 import Language.Symantic.Transforming
  26
  27 -- * Class 'Sym_Bool_Vars'
  28
  29 -- | A few boolean variables.
  30 class Sym_Bool_Vars repr where
  31         x :: repr Bool
  32         y :: repr Bool
  33         z :: repr Bool
  34 instance Sym_Bool_Vars TextI where
  35         x = TextI $ \_p _v -> "x"
  36         y = TextI $ \_p _v -> "y"
  37         z = TextI $ \_p _v -> "z"
  38 {-
  39 instance -- Trans_Boo_Const
  40  ( Sym_Bool repr
  41  , Sym_Bool_Vars repr
  42  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  43         x = trans_lift x
  44         y = trans_lift y
  45         z = trans_lift z
  46 -}
  47
  48 -- * Terms
  49 te1 = bool True && bool False
  50 te2 = (bool True && bool False) ||  (bool True && bool True)
  51 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  52 te4 = bool True && not (bool False)
  53 te5 = bool True && not x
  54 te6 = x `xor` y
  55 te7 = (x `xor` y) `xor` z
  56 te8 = x `xor` (y `xor` bool True)
  57
  58 -- * Tests
  59 type Ifaces =
  60  [ Proxy (->)
  61  , Proxy Bool
  62  ]
  63
  64 (==>) (ast::Syntax Text) expected =
  65         testCase (show ast) $
  66         case root_term_from ast of
  67          Left err -> Left err @?= Prelude.snd `Arrow.left` expected
  68          Right (ETerm ty (Term te)::ETerm Ifaces) ->
  69                 case expected of
  70                  Left (_, err) -> Right ("…"::Text) @?= Left err
  71                  Right (ty_expected::Type (Consts_of_Ifaces Ifaces) 'KiTerm h, _::UnProxy h, _::Text) ->
  72                         (Monad.>>= (@?= (\(_::Type (Consts_of_Ifaces Ifaces) 'KiTerm h, err) -> err) `Arrow.left` expected)) $
  73                         case ty `eq_type` ty_expected of
  74                          Nothing -> Monad.return $ Left $
  75                                 Error_Term_Type_mismatch
  76                                  (At Nothing $ EType ty)
  77                                  (At Nothing $ EType ty_expected)
  78                          Just Refl -> do
  79                                 let h = host_from_term te
  80                                 Monad.return $
  81                                         Right
  82                                          ( ty
  83                                          , h
  84                                          , text_from_term te
  85                                          -- , (text_from_expr :: Repr_Text h -> Text) r
  86                                          )
  87
  88 syTrue :: Syntax Text
  89 syTrue = Syntax "True" []
  90
  91 tests :: TestTree
  92 tests = testGroup "Bool" $
  93  [ syTrue ==> Right (tyBool, True, "True")
  94  , Syntax "xor" [syTrue, syTrue] ==> Right
  95          (tyBool, False, "True `xor` True")
  96  , Syntax " "
  97          [ Syntax "\\"
  98                  [ Syntax "x" []
  99                  , syBool
 100                  , Syntax "x" []
 101                  ]
 102          , syTrue
 103          ] ==> Right
 104          (tyBool, True, "(\\x0 -> x0) True")
 105  , Syntax " "
 106          [ Syntax "\\"
 107                  [ Syntax "x" []
 108                  , syBool
 109                  , Syntax "xor"
 110                          [ Syntax "x" []
 111                          , syTrue
 112                          ]
 113                  ]
 114          , syTrue
 115          ] ==> Right
 116          (tyBool, False, "(\\x0 -> x0 `xor` True) True" )
 117  , Syntax "let"
 118          [ Syntax "x" []
 119          , syTrue
 120          , Syntax "xor"
 121                  [ Syntax "x" []
 122                  , syTrue
 123                  ]
 124          ] ==> Right
 125          (tyBool, False, "let x0 = True in x0 `xor` True")
 126  , testGroup "Error_Term" $
 127          [ let sy = Syntax " "
 128                  [ syTrue
 129                  , syTrue
 130                  ] in sy ==> Left (tyBool,
 131                 Error_Term_not_applicable $ At (Just sy) $
 132                 EType tyBool)
 133          , Syntax " "
 134                  [ Syntax "\\"
 135                          [ Syntax "x" []
 136                          , syBool
 137                          , Syntax "xor"
 138                                  [ Syntax "x" []
 139                                  , syTrue
 140                                  ]
 141                          ]
 142                  , syBool
 143                  ] ==> Left (tyBool,
 144                 Error_Term_unknown $ At (Just syBool) $
 145                 "Bool")
 146          , let sy = Syntax " "
 147                  [ Syntax "\\"
 148                          [ Syntax "x" []
 149                          , syBool
 150                          , Syntax "x" []
 151                          ]
 152                  ] in sy ==> Left (tyBool,
 153                 Error_Term_Syntax $ Error_Syntax_more_arguments_needed $
 154                 At (Just sy) 1)
 155          , let sy = Syntax " "
 156                  [ Syntax "\\"
 157                          [ Syntax "x" []
 158                          , syBool
 159                          , Syntax "x" []
 160                          ]
 161                  , syTrue
 162                  , syTrue
 163                  ] in sy ==> Left (tyBool,
 164                 Error_Term_Syntax $ Error_Syntax_too_many_arguments $
 165                 At (Just sy) 1)
 166          , let sy =
 167                         Syntax "\\"
 168                          [ Syntax "x" []
 169                          , syBool .> syBool
 170                          , Syntax " " [Syntax "x" [], syTrue]
 171                          ] in
 172                 Syntax " "
 173                  [ sy
 174                  , syTrue
 175                  ] ==> Left (tyBool,
 176                 Error_Term_Type_mismatch
 177                  (At (Just sy) $ EType $ (tyBool ~> tyBool))
 178                  (At (Just $ syTrue) $ EType tyBool)
 179                  )
 180          ]
 181  ]