Language/Symantic/Compiling/Bool/Test.hs

   1 {-# LANGUAGE NoMonomorphismRestriction #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   4 {-# OPTIONS_GHC -fno-warn-orphans #-}
   5 module Compiling.Bool.Test where
   6
   7 import Test.Tasty
   8
   9 import Data.Proxy (Proxy(..))
  10 import Data.Text (Text)
  11 import qualified Data.Text as Text
  12 import Prelude hiding ((&&), not, (||))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Compiling.Term.Test
  19
  20 import Parsing.Test
  21
  22 -- * Class 'Sym_Bool_Vars'
  23
  24 -- | A few boolean variables.
  25 class Sym_Bool_Vars repr where
  26         x :: repr Bool
  27         y :: repr Bool
  28         z :: repr Bool
  29 instance Sym_Bool_Vars TextI where
  30         x = TextI $ \_p _v -> "x"
  31         y = TextI $ \_p _v -> "y"
  32         z = TextI $ \_p _v -> "z"
  33 {-
  34 instance -- Trans_Boo_Const
  35  ( Sym_Bool repr
  36  , Sym_Bool_Vars repr
  37  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  38         x = trans_lift x
  39         y = trans_lift y
  40         z = trans_lift z
  41 -}
  42
  43 -- * Terms
  44 te1 = bool True && bool False
  45 te2 = (bool True && bool False) ||  (bool True && bool True)
  46 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  47 te4 = bool True && not (bool False)
  48 te5 = bool True && not x
  49 te6 = x `xor` y
  50 te7 = (x `xor` y) `xor` z
  51 te8 = x `xor` (y `xor` bool True)
  52
  53 instance
  54  ( Inj_Token (Syntax Text) ts Bool
  55  {-, Tokenize (Syntax Text) (Syntax Text) ts-} ) =>
  56  TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Bool) where
  57         tokenizeT _t (Syntax "bool" (ast_b : as)) = Just $ do
  58                 b <- read_syntax ast_b
  59                 Right $ (as,) $ EToken $ inj_token (Syntax "bool" [ast_b]) $
  60                         Token_Term_Bool b
  61         tokenizeT _t (Syntax "xor" as) = Just $
  62                 Right $ (as,) $ EToken $ inj_token (Syntax "xor" []) $
  63                         Token_Term_Bool_xor
  64         tokenizeT _t (Syntax "not" as) = Just $
  65                 Right $ (as,) $ EToken $ inj_token (Syntax "not" []) $
  66                         Token_Term_Bool_not
  67         tokenizeT _t _sy = Nothing
  68
  69 -- * Tests
  70 type Ifaces =
  71  [ Proxy Bool
  72  , Proxy (->)
  73  ]
  74 (==>) = test_term_from (Proxy::Proxy Ifaces)
  75
  76 syBool b = Syntax "bool" [Syntax (Text.pack $ show b) []]
  77
  78 tests :: TestTree
  79 tests = testGroup "Bool" $
  80  [ syBool True ==> Right (ty @Bool, True, "True")
  81  , Syntax "xor" [syBool True, syBool True] ==> Right
  82          (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
  83  , syApp (syLam "x" (sy @Bool) (syVar "x")) (syBool True) ==> Right
  84          (ty @Bool, True, "(\\x0 -> x0) True")
  85  , syApp
  86          (syLam "x" (sy @Bool)
  87                  (Syntax "xor" [ syVar "x", syBool True ]))
  88          (syBool True) ==> Right
  89          (ty @Bool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
  90  , syLet "x" (syBool True)
  91          (Syntax "xor" [ syVar "x", syBool True ]) ==> Right
  92          (ty @Bool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
  93  , testGroup "Error_Term" $
  94          [ (syBool True `syApp` syBool True) ==> Left (ty @Bool,
  95                 Right $ Error_Term_Constraint_Type $
  96                 Right $ Constraint_Type_App $
  97                 At (maybeRight $ tokenize $ syBool True) $
  98                 EType $ ty @Bool)
  99          , syApp
 100                  (syLam "x" (sy @Bool)
 101                          (Syntax "xor" [ syVar "x", syBool True ]))
 102                  (sy @Bool) ==> Left (ty @Bool,
 103                 Left $ Error_Syntax_unsupported $
 104                 sy @Bool)
 105          , let syn = Syntax " "
 106                  [ syLam "x" (sy @Bool) (syVar "x")
 107                  ] in syn ==> Left (ty @Bool,
 108                 Left $ Error_Syntax_unsupported syn)
 109          , Syntax " "
 110                  [ syLam "x" (sy @Bool) (syVar "x")
 111                  , syBool True
 112                  , syBool True
 113                  ] ==> Left (ty @Bool,
 114                 Right $ Error_Term_Constraint_Type $
 115                 Right $ Constraint_Type_App $
 116                 At (maybeRight $ tokenize $
 117                         Syntax " "
 118                          [ syLam "x" (sy @Bool) (syVar "x")
 119                          , syBool True
 120                          ]) $
 121                 EType $ ty @Bool)
 122          , let syn =
 123                         syLam "x" (sy @Bool .> sy @Bool)
 124                          (Syntax " " [syVar "x", syBool True]) in
 125                 syApp syn (syBool True) ==> Left (ty @Bool,
 126                 Right $ Error_Term_Constraint_Type $ Right $
 127                 Constraint_Type_Eq
 128                  (Right $ At (maybeRight $ tokenize syn) $ EType $ (ty @Bool ~> ty @Bool))
 129                  (At (maybeRight $ tokenize $ syBool $ True) $ EType $ ty @Bool)
 130                  )
 131          ]
 132  ]