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.
  48       ( Eq h, Eq raw, Show h, Show raw
  49       , Expr_from raw (Expr_Lambda IO (Expr_Lambda_Int IO))
  50       , Expr_from raw (Expr_Int       (Expr_Lambda_Int IO)))
  51       => raw -> (Type_Fun_Int IO h, h, String) -> TestTree
  52 (==>) raw expected@(ty_expected::Type_Fun_Int IO h, _::h, _::String) =
  53         testCase (show raw) $
  54         (>>= (@?= Right expected)) $
  55         case expr_lambda_int_from (Proxy::Proxy IO) raw of
  56          Left err -> return $ Left err
  57          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  58                 case ty `type_eq` ty_expected of
  59                  Nothing -> return $ Left $ Nothing -- Just $ "Type mismatch"
  60                  Just Refl -> do
  61                         h <- host_from_expr r
  62                         return $
  63                                 Right
  64                                  ( ty
  65                                  , h
  66                                  , string_from_expr r
  67                                  -- , (string_from_expr :: Repr_String IO h -> String) r
  68                                  )
  69
  70 tests :: TestTree
  71 tests = testGroup "Int" $
  72  [ AST "int" [AST "1" []] ==>
  73          ( type_int
  74          , 1
  75          , "1" )
  76  , AST "add"
  77          [ AST "int" [AST "1" []]
  78          , AST "int" [AST "1" []]
  79          ] ==>
  80          ( type_int
  81          , 2
  82          , "1 + 1" )
  83  , AST "app"
  84          [ AST "val"
  85                  [ AST "x" []
  86                  , AST "Int" []
  87                  , AST "var" [AST "x" []]
  88                  ]
  89          , AST "int" [AST "1" []]
  90          ] ==>
  91          ( type_int
  92          , 1
  93          , "(\\x0 -> x0) 1" )
  94  , AST "app"
  95          [ AST "val"
  96                  [ AST "x" []
  97                  , AST "Int" []
  98                  , AST "add"
  99                          [ AST "var" [AST "x" []]
 100                          , AST "int" [AST "1" []]
 101                          ]
 102                  ]
 103          , AST "int" [AST "1" []]
 104          ] ==>
 105          ( type_int
 106          , 2
 107          , "(\\x0 -> x0 + 1) 1" )
 108  ]