connections-0.2.0: test/Test/Data/Lattice.hs

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}
module Test.Data.Lattice where

import Data.Lattice
import Data.Connection.Property
import Data.Lattice.Property
import Test.Data.Connection

import Hedgehog
import qualified Hedgehog.Gen as G

prop_coheyting :: Property
prop_coheyting = withTests 1000 . property $ do
  b1 <- forAll G.bool
  b2 <- forAll G.bool
  b3 <- forAll G.bool
  o1 <- forAll ord
  o2 <- forAll ord
  o3 <- forAll ord
  w1 <- forAll $ G.integral (ri @Word)
  w2 <- forAll $ G.integral (ri @Word)
  w3 <- forAll $ G.integral (ri @Word)

  assert $ adjointL (algebra b3) b1 b2
  assert $ closedL (algebra b3) b1
  assert $ kernelL (algebra b3) b2
  assert $ monotonicL (algebra b3) b1 b2 b3 b2
  assert $ idempotentL (algebra b3) b1 b2

  assert $ adjointL booleanL b1 b2
  assert $ closedL booleanL b1
  assert $ kernelL booleanL b2
  assert $ monotonicL booleanL b1 b2 b3 b2
  assert $ idempotentL booleanL b1 b3
  
  assert $ coheyting1 b1 b2 b3
  assert $ coheyting2 b1 b2 b3
  assert $ coheyting3 b1 b2 b3
  assert $ coheyting4 b1 b2 b3
  assert $ coheyting5 b1 b2 b3
  assert $ coheyting6 b1 b2
  assert $ coheyting7 b1 b2
  assert $ coheyting8 b1
  assert $ coheyting9 b1 b2
  assert $ coheyting10 b1 b2
  assert $ coheyting11 b1 b2
  assert $ coheyting12 b1 b2
  assert $ coheyting13 b1 b2
  assert $ coheyting14 b1
  assert $ coheyting15 b1
  assert $ coheyting16 b1
  assert $ coheyting17 b1
  assert $ coheyting18 b1
  assert $ coheyting19 b1 b2
  assert $ coheyting20 b1 b2

  assert $ adjointL (algebra o3) o1 o2
  assert $ closedL (algebra o3) o1
  assert $ kernelL (algebra o3) o2
  assert $ monotonicL (algebra o3) o1 o2 o3 o2
  assert $ idempotentL (algebra o3) o1 o2

  assert $ adjointL booleanL o1 o2
  assert $ closedL booleanL o1
  assert $ kernelL booleanL o2
  assert $ monotonicL booleanL o1 o2 o3 o2
  assert $ idempotentL booleanL o1 o3

  assert $ coheyting1 o1 o2 o3
  assert $ coheyting2 o1 o2 o3
  assert $ coheyting3 o1 o2 o3
  assert $ coheyting4 o1 o2 o3
  assert $ coheyting5 o1 o2 o3
  assert $ coheyting6 o1 o2
  assert $ coheyting7 o1 o2
  assert $ coheyting8 o1
  assert $ coheyting9 o1 o2
  assert $ coheyting10 o1 o2
  assert $ coheyting11 o1 o2
  assert $ coheyting12 o1 o2
  assert $ coheyting13 o1 o2
  assert $ coheyting14 o1
  assert $ coheyting15 o1
  assert $ coheyting16 o1
  assert $ coheyting17 o1
  assert $ coheyting18 o1
  assert $ coheyting19 o1 o2
  assert $ coheyting20 o1 o2

  assert $ adjointL (algebra w3) w1 w2
  assert $ closedL (algebra w3) w1
  assert $ kernelL (algebra w3) w2
  assert $ monotonicL (algebra w3) w1 w2 w3 w2
  assert $ idempotentL (algebra w3) w1 w2

  assert $ adjointL booleanL w1 w2
  assert $ closedL booleanL w1
  assert $ kernelL booleanL w2
  assert $ monotonicL booleanL w1 w2 w3 w2
  assert $ idempotentL booleanL w1 w3

  assert $ coheyting1 w1 w2 w3
  assert $ coheyting2 w1 w2 w3
  assert $ coheyting3 w1 w2 w3
  assert $ coheyting4 w1 w2 w3
  assert $ coheyting5 w1 w2 w3
  assert $ coheyting6 w1 w2
  assert $ coheyting7 w1 w2
  assert $ coheyting8 w1
  assert $ coheyting9 w1 w2
  assert $ coheyting10 w1 w2
  assert $ coheyting11 w1 w2
  assert $ coheyting12 w1 w2
  assert $ coheyting13 w1 w2
  assert $ coheyting14 w1
  assert $ coheyting15 w1
  assert $ coheyting16 w1
  assert $ coheyting17 w1
  assert $ coheyting18 w1
  assert $ coheyting19 w1 w2
  assert $ coheyting20 w1 w2

prop_heyting :: Property
prop_heyting = withTests 1000 . property $ do
  b1 <- forAll G.bool
  b2 <- forAll G.bool
  b3 <- forAll G.bool
  o1 <- forAll ord
  o2 <- forAll ord
  o3 <- forAll ord
  w1 <- forAll $ G.integral (ri @Word)
  w2 <- forAll $ G.integral (ri @Word)
  w3 <- forAll $ G.integral (ri @Word)

  assert $ adjointR (algebra b3) b1 b2
  assert $ closedR (algebra b3) b1
  assert $ kernelR (algebra b3) b2
  assert $ monotonicR (algebra b3) b1 b2 b3 b2
  assert $ idempotentR (algebra b3) b1 b2
  
  assert $ adjointR booleanR b1 b2
  assert $ closedR booleanR b1
  assert $ kernelR booleanR b2
  assert $ monotonicR booleanR b1 b2 b3 b2
  assert $ idempotentR booleanR b1 b3

  assert $ heyting0 b1 b2 b3
  assert $ heyting1 b1 b2 b3
  assert $ heyting2 b1 b2 b3
  assert $ heyting3 b1 b2 b3
  assert $ heyting4 b1 b2 b3
  assert $ heyting5 b1 b2 b3
  assert $ heyting6 b1 b2
  assert $ heyting7 b1 b2
  assert $ heyting8 b1
  assert $ heyting9 b1 b2
  assert $ heyting10 b1 b2
  assert $ heyting11 b1 b2
  assert $ heyting12 b1 b2
  assert $ heyting13 b1 b2
  assert $ heyting14 b1
  assert $ heyting15 b1
  assert $ heyting16 b1
  assert $ heyting17 b1

  assert $ adjointR (algebra o3) o1 o2
  assert $ closedR (algebra o3) o1
  assert $ kernelR (algebra o3) o2
  assert $ monotonicR (algebra o3) o1 o2 o3 o2
  assert $ idempotentR (algebra o3) o1 o2

  assert $ adjointR booleanR o1 o2
  assert $ closedR booleanR o1
  assert $ kernelR booleanR o2
  assert $ monotonicR booleanR o1 o2 o3 o2
  assert $ idempotentR booleanR o1 o3

  assert $ heyting0 o1 o2 o3
  assert $ heyting1 o1 o2 o3
  assert $ heyting2 o1 o2 o3
  assert $ heyting3 o1 o2 o3
  assert $ heyting4 o1 o2 o3
  assert $ heyting5 o1 o2 o3
  assert $ heyting6 o1 o2
  assert $ heyting7 o1 o2
  assert $ heyting8 o1
  assert $ heyting9 o1 o2
  assert $ heyting10 o1 o2
  assert $ heyting11 o1 o2
  assert $ heyting12 o1 o2
  assert $ heyting13 o1 o2
  assert $ heyting14 o1
  assert $ heyting15 o1
  assert $ heyting16 o1
  assert $ heyting17 o1

  assert $ adjointR (algebra w3) w1 w2
  assert $ closedR (algebra w3) w1
  assert $ kernelR (algebra w3) w2
  assert $ monotonicR (algebra w3) w1 w2 w3 w2
  assert $ idempotentR (algebra w3) w1 w2
  
  assert $ adjointR booleanR w1 w2
  assert $ closedR booleanR w1
  assert $ kernelR booleanR w2
  assert $ monotonicR booleanR w1 w2 w3 w2
  assert $ idempotentR booleanR w1 w3

  assert $ heyting0 w1 w2 w3
  assert $ heyting1 w1 w2 w3
  assert $ heyting2 w1 w2 w3
  assert $ heyting3 w1 w2 w3
  assert $ heyting4 w1 w2 w3
  assert $ heyting5 w1 w2 w3
  assert $ heyting6 w1 w2
  assert $ heyting7 w1 w2
  assert $ heyting8 w1
  assert $ heyting9 w1 w2
  assert $ heyting10 w1 w2
  assert $ heyting11 w1 w2
  assert $ heyting12 w1 w2
  assert $ heyting13 w1 w2
  assert $ heyting14 w1
  assert $ heyting15 w1
  assert $ heyting16 w1
  assert $ heyting17 w1

prop_symmetric :: Property
prop_symmetric = withTests 1000 . property $ do
  b1 <- forAll G.bool
  b2 <- forAll G.bool
  b3 <- forAll G.bool
  o1 <- forAll ord
  o2 <- forAll ord
 
  assert $ symmetric1 b1
  assert $ symmetric2 b1
  assert $ symmetric3 b1
  assert $ symmetric4 b1
  assert $ symmetric5 b1
  assert $ symmetric6 b1
  assert $ symmetric7 b1 b2
  assert $ symmetric8 b1 b2
  assert $ symmetric9 b1 b2
  assert $ symmetric10 b1 b2
  assert $ symmetric11 b1 b2
  assert $ symmetric12 b1 b2
  assert $ symmetric13 b1 b2
 
  assert $ adjoint boolean b1 b2
  assert $ closed boolean b1
  assert $ kernel boolean b2
  assert $ monotonic boolean b1 b2 b3 b2
  assert $ idempotent boolean b1 b3

  assert $ boolean0 b1
  assert $ boolean1 b1
  assert $ boolean2 b1
  assert $ boolean3 b1
  assert $ boolean4 b1 b2
  assert $ boolean5 b1 b2
  assert $ boolean6 b1 b2
  
  assert $ symmetric1 o1
  assert $ symmetric2 o1
  assert $ symmetric3 o1
  assert $ symmetric4 o1
  assert $ symmetric5 o1
  assert $ symmetric6 o1
  assert $ symmetric7 o1 o2
  assert $ symmetric8 o1 o2
  assert $ symmetric9 o1 o2
  assert $ symmetric10 o1 o2
  assert $ symmetric11 o1 o2
  assert $ symmetric12 o1 o2
  assert $ symmetric13 o1 o2

tests :: IO Bool
tests = checkParallel $$(discover)