{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Expr.Int.Test where import Test.Tasty import Test.Tasty.HUnit -- import Data.Functor.Identity (Identity) -- import Control.Monad.IO.Class (MonadIO(..)) import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (and, not, or) import Language.LOL.Symantic.Repr import Language.LOL.Symantic.AST import Language.LOL.Symantic.Expr import Language.LOL.Symantic.Type -- import Language.LOL.Symantic.Trans -- * Class 'Sym_Int_Vars' -- | A few boolean variables. class Sym_Int_Vars repr where x :: repr Int y :: repr Int z :: repr Int instance Sym_Int_Vars (Repr_String fun) where x = Repr_String $ \_p _v -> "x" y = Repr_String $ \_p _v -> "y" z = Repr_String $ \_p _v -> "z" -- * Expressions e1 = int 1 `add` int 0 e2 = (int 1 `add` int 0) `add` neg (int 1 `add` int 1) e3 = (int 1 `add` neg (int 0)) `add` (int 1 `add` neg (int 1)) e4 = int 0 `add` neg (int 1) e5 = int 1 `add` neg x e6 = x `add` y e7 = (x `add` y) `add` z e8 = x `add` (y `add` int 1) -- * Tests (==>) :: forall h raw root. ( Eq h, Eq raw, Show h, Show raw , root ~ Expr_Lambda_Int IO , Expr_from raw (Expr_Lambda IO root) , Expr_from raw (Expr_Int root) ) => raw -> (Type_Fun_Int IO h, h, String) -> TestTree (==>) raw expected@(ty_expected::Type_Fun_Int IO h, _::h, _::String) = testCase (show raw) $ (>>= (@?= Right expected)) $ case expr_lambda_int_from (Proxy::Proxy IO) raw of Left err -> return $ Left err Right (Exists_Type_and_Repr ty (Forall_Repr r)) -> case ty `type_eq` ty_expected of Nothing -> return $ Left $ error_lambda_lift $ Error_Expr_Type (error_type_lift $ Error_Type_Unsupported raw) raw Just Refl -> do h <- host_from_expr r return $ Right ( ty , h , string_from_expr r -- , (string_from_expr :: Repr_String IO h -> String) r ) where error_lambda_lift :: (root ~ Expr_Lambda_Int IO) => Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root)) (Type_Root_of_Expr root) raw -> Error_of_Expr raw root error_lambda_lift = error_expr_lift tests :: TestTree tests = testGroup "Int" $ [ AST "int" [AST "1" []] ==> ( type_int , 1 , "1" ) , AST "add" [ AST "int" [AST "1" []] , AST "int" [AST "1" []] ] ==> ( type_int , 2 , "1 + 1" ) , AST "app" [ AST "val" [ AST "x" [] , AST "Int" [] , AST "var" [AST "x" []] ] , AST "int" [AST "1" []] ] ==> ( type_int , 1 , "(\\x0 -> x0) 1" ) , AST "app" [ AST "val" [ AST "x" [] , AST "Int" [] , AST "add" [ AST "var" [AST "x" []] , AST "int" [AST "1" []] ] ] , AST "int" [AST "1" []] ] ==> ( type_int , 2 , "(\\x0 -> x0 + 1) 1" ) , AST "let_val" [ AST "x" [] , AST "int" [AST "1" []] , AST "add" [ AST "var" [AST "x" []] , AST "int" [AST "1" []] ] ] ==> ( type_int , 2 , "let x0 = 1 in x0 + 1" ) ]