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
  26 -- * Class 'Sym_Bool_Vars'
  27
  28 -- | A few boolean variables.
  29 class Sym_Bool_Vars repr where
  30         x :: repr Bool
  31         y :: repr Bool
  32         z :: repr Bool
  33 instance Sym_Bool_Vars TextI where
  34         x = TextI $ \_p _v -> "x"
  35         y = TextI $ \_p _v -> "y"
  36         z = TextI $ \_p _v -> "z"
  37 {-
  38 instance -- Trans_Boo_Const
  39  ( Sym_Bool repr
  40  , Sym_Bool_Vars repr
  41  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  42         x = trans_lift x
  43         y = trans_lift y
  44         z = trans_lift z
  45 -}
  46
  47 -- * Terms
  48 te1 = bool True && bool False
  49 te2 = (bool True && bool False) ||  (bool True && bool True)
  50 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  51 te4 = bool True && not (bool False)
  52 te5 = bool True && not x
  53 te6 = x `xor` y
  54 te7 = (x `xor` y) `xor` z
  55 te8 = x `xor` (y `xor` bool True)
  56
  57 -- * Tests
  58 type Ifaces =
  59  [ Proxy (->)
  60  , Proxy Bool
  61  ]
  62 type Consts = Consts_of_Ifaces Ifaces
  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 h, _::h, _::Text) ->
  72                         (Monad.>>= (@?= (\(_::Type Consts 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 tests :: TestTree
  89 tests = testGroup "Bool" $
  90  [ syTrue ==> Right (tyBool, True, "True")
  91  , Syntax "xor" [syTrue, syTrue] ==> Right
  92          (tyBool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
  93  , syApp
  94          (syLam (Syntax "x" []) syBool
  95                  (Syntax "x" []))
  96          syTrue ==> Right
  97          (tyBool, True, "(\\x0 -> x0) True")
  98  , syApp
  99          (syLam (Syntax "x" []) syBool
 100                  (Syntax "xor"
 101                          [ Syntax "x" []
 102                          , syTrue
 103                          ]))
 104          syTrue ==> Right
 105          (tyBool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
 106  , syLet (Syntax "x" []) syTrue
 107          (Syntax "xor"
 108                  [ Syntax "x" []
 109                  , syTrue
 110                  ]) ==> Right
 111          (tyBool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
 112  , testGroup "Error_Term" $
 113          [ syApp syTrue syTrue ==> Left (tyBool,
 114                 Error_Term_Type_is_not_an_application $ At (Just syTrue) $
 115                 EType tyBool)
 116          , syApp
 117                  (syLam
 118                          (Syntax "x" []) syBool
 119                          (Syntax "xor"
 120                                  [ Syntax "x" []
 121                                  , syTrue
 122                                  ])
 123                          )
 124                  syBool ==> Left (tyBool,
 125                 Error_Term_unknown $ At (Just syBool) $
 126                 "Bool")
 127          , let sy = Syntax " "
 128                  [ syLam (Syntax "x" []) syBool
 129                          (Syntax "x" [])
 130                  ] in sy ==> Left (tyBool,
 131                 Error_Term_Syntax $ Error_Syntax_more_arguments_needed $
 132                 At (Just sy) 2)
 133          , let sy = Syntax " "
 134                  [ syLam (Syntax "x" []) syBool
 135                          (Syntax "x" [])
 136                  , syTrue
 137                  , syTrue
 138                  ] in sy ==> Left (tyBool,
 139                 Error_Term_Type_is_not_an_application $
 140                 At (Just sy) $ EType tyBool)
 141          , let sy =
 142                         syLam (Syntax "x" []) (syBool .> syBool)
 143                          (Syntax " " [Syntax "x" [], syTrue]) in
 144                 syApp sy syTrue ==> Left (tyBool,
 145                 Error_Term_Type_mismatch
 146                  (At (Just sy) $ EType $ (tyBool ~> tyBool))
 147                  (At (Just $ syTrue) $ EType tyBool)
 148                  )
 149          ]
 150  ]