{-# LANGUAGE ConstraintKinds #-}
module BooleanModelLaws (booleanModelLaws) where

import Test.Tasty
import Test.Tasty.QuickCheck as QC

import FreeBoolean

import Data.Algebra.Boolean.NormalForm

modelProperty :: (CoBoolean a, NormalForm nf, NFConstraint nf a) => nf a -> FreeBoolean a-> Property
modelProperty t b = collect (freeBooleanHeight b) $
  toBoolWith toBool b == toBoolWith toBool (fromFreeBoolean b `asTypeOf` t)

booleanModelLaws :: (Arbitrary a, Show a, CoBoolean a, NormalForm nf, NFConstraint nf a) => nf a -> TestTree
booleanModelLaws t = QC.testProperty "Boolean model" $ modelProperty t