Language/Symantic/Compiling/Bool/Test.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE NoMonomorphismRestriction #-}
   3 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   4 module Compiling.Bool.Test where
   5
   6 import Test.Tasty
   7
   8 import Data.Proxy (Proxy(..))
   9 import Prelude hiding ((&&), not, (||))
  10
  11 import Language.Symantic.Typing
  12 import Language.Symantic.Compiling
  13 import Language.Symantic.Interpreting
  14 import Compiling.Term.Test
  15
  16 -- * Class 'Sym_Bool_Vars'
  17
  18 -- | A few boolean variables.
  19 class Sym_Bool_Vars repr where
  20         x :: repr Bool
  21         y :: repr Bool
  22         z :: repr Bool
  23 instance Sym_Bool_Vars TextI where
  24         x = TextI $ \_p _v -> "x"
  25         y = TextI $ \_p _v -> "y"
  26         z = TextI $ \_p _v -> "z"
  27 {-
  28 instance -- Trans_Boo_Const
  29  ( Sym_Bool repr
  30  , Sym_Bool_Vars repr
  31  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  32         x = trans_lift x
  33         y = trans_lift y
  34         z = trans_lift z
  35 -}
  36
  37 -- * Terms
  38 te1 = bool True && bool False
  39 te2 = (bool True && bool False) ||  (bool True && bool True)
  40 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  41 te4 = bool True && not (bool False)
  42 te5 = bool True && not x
  43 te6 = x `xor` y
  44 te7 = (x `xor` y) `xor` z
  45 te8 = x `xor` (y `xor` bool True)
  46
  47 -- * Tests
  48 type Ifaces =
  49  [ Proxy (->)
  50  , Proxy Bool
  51  ]
  52 (==>) = test_term_from (Proxy::Proxy Ifaces)
  53
  54 tests :: TestTree
  55 tests = testGroup "Bool" $
  56  [ syTrue ==> Right (tyBool, True, "True")
  57  , Syntax "xor" [syTrue, syTrue] ==> Right
  58          (tyBool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
  59  , syApp
  60          (syLam (Syntax "x" []) syBool
  61                  (Syntax "x" []))
  62          syTrue ==> Right
  63          (tyBool, True, "(\\x0 -> x0) True")
  64  , syApp
  65          (syLam (Syntax "x" []) syBool
  66                  (Syntax "xor"
  67                          [ Syntax "x" []
  68                          , syTrue
  69                          ]))
  70          syTrue ==> Right
  71          (tyBool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
  72  , syLet (Syntax "x" []) syTrue
  73          (Syntax "xor"
  74                  [ Syntax "x" []
  75                  , syTrue
  76                  ]) ==> Right
  77          (tyBool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
  78  , testGroup "Error_Term" $
  79          [ syApp syTrue syTrue ==> Left (tyBool,
  80                 Error_Term_Type_is_not_an_application $ At (Just syTrue) $
  81                 EType tyBool)
  82          , syApp
  83                  (syLam
  84                          (Syntax "x" []) syBool
  85                          (Syntax "xor"
  86                                  [ Syntax "x" []
  87                                  , syTrue
  88                                  ])
  89                          )
  90                  syBool ==> Left (tyBool,
  91                 Error_Term_unknown $ At (Just syBool) $
  92                 "Bool")
  93          , let sy = Syntax " "
  94                  [ syLam (Syntax "x" []) syBool
  95                          (Syntax "x" [])
  96                  ] in sy ==> Left (tyBool,
  97                 Error_Term_Syntax $ Error_Syntax_more_arguments_needed $
  98                 At (Just sy) 2)
  99          , let sy = Syntax " "
 100                  [ syLam (Syntax "x" []) syBool
 101                          (Syntax "x" [])
 102                  , syTrue
 103                  , syTrue
 104                  ] in sy ==> Left (tyBool,
 105                 Error_Term_Type_is_not_an_application $
 106                 At (Just sy) $ EType tyBool)
 107          , let sy =
 108                         syLam (Syntax "x" []) (syBool .> syBool)
 109                          (Syntax " " [Syntax "x" [], syTrue]) in
 110                 syApp sy syTrue ==> Left (tyBool,
 111                 Error_Term_Type_mismatch
 112                  (At (Just sy) $ EType $ (tyBool ~> tyBool))
 113                  (At (Just $ syTrue) $ EType tyBool)
 114                  )
 115          ]
 116  ]