{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
-- {-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoOverloadedStrings #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Compiling.Test where

import Test.Tasty
-- import Test.Tasty.HUnit

import qualified Compiling.Bool.Test as Bool

-- import Data.Maybe (isJust)
-- import Data.Proxy
-- import GHC.Prim (Constraint)
import Prelude hiding ((&&), not, (||), (==), id)

import Language.Symantic.Compiling

tests :: TestTree
tests = testGroup "Compiling" $
	 [ Bool.tests
	 ]


-- * Terms
te1 = lam $ \x -> lam $ \y -> (x || y) && not (x && y)
te2 = lam $ \x -> lam $ \y -> (x && not y) || (not x && y)
te3 = let_ (bool True) $ \x -> x && x
te4 = let_ (lam $ \x -> x && x) $ \f -> f .$ bool True
te5 = lam $ \x0 -> lam $ \x1 -> x0 && x1
te6 = let_ (bool True) id && bool False
te7 = lam $ \f -> (f .$ bool True) && bool True
te8 = lam $ \f -> f .$ (bool True && bool True)