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_expr (Proxy::Proxy root) $ 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
  74 tests :: TestTree
  75 tests = testGroup "Int" $
  76  [ AST "int" [AST "1" []] ==>
  77          ( type_int
  78          , 1
  79          , "1" )
  80  , AST "add"
  81          [ AST "int" [AST "1" []]
  82          , AST "int" [AST "1" []]
  83          ] ==>
  84          ( type_int
  85          , 2
  86          , "1 + 1" )
  87  , AST "app"
  88          [ AST "val"
  89                  [ AST "x" []
  90                  , AST "Int" []
  91                  , AST "var" [AST "x" []]
  92                  ]
  93          , AST "int" [AST "1" []]
  94          ] ==>
  95          ( type_int
  96          , 1
  97          , "(\\x0 -> x0) 1" )
  98  , AST "app"
  99          [ AST "val"
 100                  [ AST "x" []
 101                  , AST "Int" []
 102                  , AST "add"
 103                          [ AST "var" [AST "x" []]
 104                          , AST "int" [AST "1" []]
 105                          ]
 106                  ]
 107          , AST "int" [AST "1" []]
 108          ] ==>
 109          ( type_int
 110          , 2
 111          , "(\\x0 -> x0 + 1) 1" )
 112  , AST "let_val"
 113          [ AST "x" []
 114          , AST "int" [AST "1" []]
 115          , AST "add"
 116                  [ AST "var" [AST "x" []]
 117                  , AST "int" [AST "1" []]
 118                  ]
 119          ] ==>
 120          ( type_int
 121          , 2
 122          , "let x0 = 1 in x0 + 1" )
 123  ]