Language/LOL/Symantic/Expr/Int/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   7 module Expr.Int.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11
  12 -- import Data.Functor.Identity (Identity)
  13 -- import Control.Monad.IO.Class (MonadIO(..))
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (and, not, or)
  17
  18 import Language.LOL.Symantic.Repr
  19 import Language.LOL.Symantic.AST
  20 import Language.LOL.Symantic.Expr
  21 import Language.LOL.Symantic.Type
  22 -- import Language.LOL.Symantic.Trans
  23
  24 -- * Class 'Sym_Int_Vars'
  25
  26 -- | A few boolean variables.
  27 class Sym_Int_Vars repr where
  28         x :: repr Int
  29         y :: repr Int
  30         z :: repr Int
  31 instance Sym_Int_Vars (Repr_String fun) where
  32         x = Repr_String $ \_p _v -> "x"
  33         y = Repr_String $ \_p _v -> "y"
  34         z = Repr_String $ \_p _v -> "z"
  35
  36 -- * Expressions
  37 e1 = int 1 `add` int 0
  38 e2 = (int 1 `add` int 0) `add` neg (int 1 `add` int 1)
  39 e3 = (int 1 `add` neg (int 0)) `add` (int 1 `add` neg (int 1))
  40 e4 = int 0 `add` neg (int 1)
  41 e5 = int 1 `add` neg x
  42 e6 = x `add` y
  43 e7 = (x `add` y) `add` z
  44 e8 = x `add` (y `add` int 1)
  45
  46 -- * Tests
  47 (==>) :: forall h raw root.
  48       ( Eq h, Eq raw, Show h, Show raw
  49       , root ~ Expr_Lambda_Int IO
  50       , Expr_from raw (Expr_Lambda IO root)
  51       , Expr_from raw (Expr_Int      root)
  52       )
  53       => raw -> (Type_Fun_Int IO h, h, String) -> TestTree
  54 (==>) raw expected@(ty_expected::Type_Fun_Int IO h, _::h, _::String) =
  55         testCase (show raw) $
  56         (>>= (@?= Right expected)) $
  57         case expr_lambda_int_from (Proxy::Proxy IO) raw of
  58          Left err -> return $ Left err
  59          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  60                 case ty `type_eq` ty_expected of
  61                  Nothing -> return $ Left $
  62                         error_lambda_lift $ Error_Expr_Type
  63                          (error_type_lift $ Error_Type_Unsupported raw) raw
  64                  Just Refl -> do
  65                         h <- host_from_expr r
  66                         return $
  67                                 Right
  68                                  ( ty
  69                                  , h
  70                                  , string_from_expr r
  71                                  -- , (string_from_expr :: Repr_String IO h -> String) r
  72                                  )
  73         where
  74                 error_lambda_lift
  75                  :: (root ~ Expr_Lambda_Int IO)
  76                  => Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root))
  77                                       (Type_Root_of_Expr root)
  78                                       raw
  79                  -> Error_of_Expr raw root
  80                 error_lambda_lift = error_expr_lift
  81
  82 tests :: TestTree
  83 tests = testGroup "Int" $
  84  [ AST "int" [AST "1" []] ==>
  85          ( type_int
  86          , 1
  87          , "1" )
  88  , AST "add"
  89          [ AST "int" [AST "1" []]
  90          , AST "int" [AST "1" []]
  91          ] ==>
  92          ( type_int
  93          , 2
  94          , "1 + 1" )
  95  , AST "app"
  96          [ AST "val"
  97                  [ AST "x" []
  98                  , AST "Int" []
  99                  , AST "var" [AST "x" []]
 100                  ]
 101          , AST "int" [AST "1" []]
 102          ] ==>
 103          ( type_int
 104          , 1
 105          , "(\\x0 -> x0) 1" )
 106  , AST "app"
 107          [ AST "val"
 108                  [ AST "x" []
 109                  , AST "Int" []
 110                  , AST "add"
 111                          [ AST "var" [AST "x" []]
 112                          , AST "int" [AST "1" []]
 113                          ]
 114                  ]
 115          , AST "int" [AST "1" []]
 116          ] ==>
 117          ( type_int
 118          , 2
 119          , "(\\x0 -> x0 + 1) 1" )
 120  , AST "let_val"
 121          [ AST "x" []
 122          , AST "int" [AST "1" []]
 123          , AST "add"
 124                  [ AST "var" [AST "x" []]
 125                  , AST "int" [AST "1" []]
 126                  ]
 127          ] ==>
 128          ( type_int
 129          , 2
 130          , "let x0 = 1 in x0 + 1" )
 131  ]