lattices 1.7.1.1 → 2

raw patch · 30 files changed

+2510/−811 lines, 30 filesdep +integer-logarithmsdep −universe-instances-basedep ~QuickCheckdep ~basedep ~base-compatbinary-addedPVP ok

version bump matches the API change (PVP)

Dependencies added: integer-logarithms

Dependencies removed: universe-instances-base

Dependency ranges changed: QuickCheck, base, base-compat, containers, hashable, quickcheck-instances, semigroupoids, semigroups, tagged, tasty, tasty-quickcheck, transformers, universe-base, universe-reverse-instances, unordered-containers, void

API changes (from Hackage documentation)

Files

• CHANGELOG.md +12/−0
• README.md +0/−9
• lattices.cabal +91/−58
• m2.png binary
• m3.png binary
• n5.png binary
• src/Algebra/Enumerable.hs +0/−50
• src/Algebra/Heyting.hs +151/−0
• src/Algebra/Heyting/Free.hs +183/−0
• src/Algebra/Heyting/Free/Expr.hs +280/−0
• src/Algebra/Lattice.hs +161/−219
• src/Algebra/Lattice/Divisibility.hs +41/−25
• src/Algebra/Lattice/Dropped.hs +63/−32
• src/Algebra/Lattice/Free.hs +115/−119
• src/Algebra/Lattice/Free/Final.hs +106/−0
• src/Algebra/Lattice/Levitated.hs +70/−27
• src/Algebra/Lattice/Lexicographic.hs +35/−24
• src/Algebra/Lattice/Lifted.hs +55/−25
• src/Algebra/Lattice/M2.hs +124/−0
• src/Algebra/Lattice/M3.hs +89/−0
• src/Algebra/Lattice/N5.hs +94/−0
• src/Algebra/Lattice/Op.hs +29/−21
• src/Algebra/Lattice/Ordered.hs +45/−28
• src/Algebra/Lattice/Unicode.hs +29/−0
• src/Algebra/Lattice/Wide.hs +138/−0
• src/Algebra/Lattice/ZeroHalfOne.hs +80/−0
• src/Algebra/PartialOrd.hs +21/−8
• src/Algebra/PartialOrd/Instances.hs +6/−0
• test/Tests.hs +492/−166
• wide.png binary

@@ -1,3 +1,15 @@+# 2 (2019-04-17)++- Reduce to three classes (from six): `Lattice`, `BoundedMeetSemiLattice`+  `BoundeJoinSemiLattice`.+  The latter two names are kept to help migration.+- Remove `Algebra.Enumerable` module. Use `universe` package.+- Drop GHC-7.4.3 support (broken `ConstraintKinds`)+- Move `Algebra.Lattice.Free` to `Algebra.Lattice.Free.Final`+- Add concrete syntax `Algebra.Lattice.Free` and `Algebra.Heyting.Free` using+  LJT-proof search for `Eq` and `PartialOrd`+- Change `PartialOrd [a]` to be `leq = isSubsequenceOf`+ # 1.7.1.1 (2019-07-05)  - Allow newer dependencies, update cabal file

@@ -1,9 +0,0 @@-# lattices--[![Build Status](https://travis-ci.org/phadej/lattices.svg?branch=master)](https://travis-ci.org/phadej/lattices)-[![Hackage](https://img.shields.io/hackage/v/lattices.svg)](http://hackage.haskell.org/package/lattices)-[![Stackage LTS 2](http://stackage.org/package/lattices/badge/lts-2)](http://stackage.org/lts-2/package/lattices)-[![Stackage LTS 3](http://stackage.org/package/lattices/badge/lts-3)](http://stackage.org/lts-3/package/lattices)-[![Stackage Nightly](http://stackage.org/package/lattices/badge/nightly)](http://stackage.org/nightly/package/lattices)--Fine-grained library for constructing and manipulating lattices

@@ -1,18 +1,32 @@+cabal-version:      1.18 name:               lattices-version:            1.7.1.1-cabal-version:      >= 1.10+version:            2 category:           Math license:            BSD3-license-File:       LICENSE-author:             Maximilian Bolingbroke <batterseapower@hotmail.com>+license-file:       LICENSE+author:+  Maximilian Bolingbroke <batterseapower@hotmail.com>, Oleg Grenrus <oleg.grenrus@iki.fi>+ maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi> homepage:           http://github.com/phadej/lattices/ bug-reports:        http://github.com/phadej/lattices/issues-copyright:          (C) 2010-2015 Maximilian Bolingbroke+copyright:+  (C) 2010-2015 Maximilian Bolingbroke, 2016-2019 Oleg Grenrus+ build-type:         Simple-extra-source-files: README.md CHANGELOG.md-tested-with:        GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.3, GHC==8.0.2, GHC==8.2.2, GHC==8.4.3-synopsis:           Fine-grained library for constructing and manipulating lattices+extra-source-files: CHANGELOG.md+extra-doc-files:+  m2.png+  m3.png+  n5.png+  wide.png++tested-with:+  GHC ==7.6.3 || ==7.8.4 || ==7.10.3 || ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1++synopsis:+  Fine-grained library for constructing and manipulating lattices+ description:   In mathematics, a lattice is a partially ordered set in which every two   elements @x@ and @y@ have a unique supremum (also called a least upper bound, join, or @x /\\ y@)@@ -22,64 +36,83 @@   as a class for the partial order.  source-repository head-  type: git+  type:     git   location: git://github.com/phadej/lattices.git  library-  exposed-modules:  Algebra.Enumerable,-                    Algebra.Lattice,-                    Algebra.Lattice.Divisibility,-                    Algebra.Lattice.Dropped,-                    Algebra.Lattice.Free,-                    Algebra.Lattice.Levitated,-                    Algebra.Lattice.Lexicographic,-                    Algebra.Lattice.Lifted,-                    Algebra.Lattice.Op,-                    Algebra.Lattice.Ordered,-                    Algebra.PartialOrd,-                    Algebra.PartialOrd.Instances--  build-depends:    base                       >= 4.5     && < 4.12,-                    base-compat                >= 0.9.3   && < 0.11,-                    containers                 >= 0.4.2.1 && < 0.6,-                    deepseq                    >= 1.3.0.0 && < 1.5,-                    hashable                   >= 1.2.6.1 && < 1.3,-                    tagged                     >= 0.8.5   && < 0.9,-                    unordered-containers       >= 0.2.6.0 && < 0.3,-                    semigroupoids              >= 5.2.2   && < 5.4,-                    universe-base              >= 1.0     && < 1.1,-                    universe-reverse-instances >= 1.0     && < 1.1+  default-language: Haskell2010   hs-source-dirs:   src   ghc-options:      -Wall-  default-language: Haskell2010+  exposed-modules:+    Algebra.Lattice+    Algebra.Lattice.Divisibility+    Algebra.Lattice.Dropped+    Algebra.Lattice.Free+    Algebra.Lattice.Free.Final+    Algebra.Lattice.Levitated+    Algebra.Lattice.Lexicographic+    Algebra.Lattice.Lifted+    Algebra.Lattice.M2+    Algebra.Lattice.M3+    Algebra.Lattice.N5+    Algebra.Lattice.Op+    Algebra.Lattice.Ordered+    Algebra.Lattice.Unicode+    Algebra.Lattice.Wide+    Algebra.Lattice.ZeroHalfOne -  if !impl(ghc >= 8.0)-    build-depends:  semigroups                 >= 0.18.3 && < 0.19+  exposed-modules:+    Algebra.Heyting+    Algebra.Heyting.Free+    Algebra.Heyting.Free.Expr -  if !impl(ghc >= 7.10)-    build-depends:   void                       >= 0.7  && < 0.8,-                     transformers               >= 0.3  && < 0.6+  exposed-modules:+    Algebra.PartialOrd+    Algebra.PartialOrd.Instances -  if impl(ghc >= 7.4 && < 7.5)-    build-depends:  ghc-prim+  build-depends:+      base                        >=4.6      && <4.13+    , base-compat                 >=0.10.5   && <0.11+    , containers                  >=0.5.0.0  && <0.7+    , deepseq                     >=1.3.0.0  && <1.5+    , hashable                    >=1.2.7.0  && <1.3+    , integer-logarithms          >=1.0.3    && <1.1+    , QuickCheck                  >=2.12.6.1 && <2.14+    , semigroupoids               >=5.3.2    && <5.4+    , tagged                      >=0.8.6    && <0.9+    , transformers                >=0.3.0.0  && <0.6+    , universe-base               >=1.1      && <1.2+    , universe-reverse-instances  >=1.1      && <1.2+    , unordered-containers        >=0.2.8.0  && <0.3 +  if !impl(ghc >=8.0)+    build-depends: semigroups >=0.18.5 && <0.19++  if !impl(ghc >=7.10)+    build-depends: void >=0.7.2 && <0.8++  if impl(ghc >=7.4 && <7.5)+    build-depends: ghc-prim+ test-suite test-  type:                exitcode-stdio-1.0-  main-is:             Tests.hs-  hs-source-dirs:      test-  ghc-options:         -Wall-  default-language:    Haskell2010-  build-depends:       base,-                       base-compat,-                       tasty                >= 0.10  && < 1.2,-                       tasty-quickcheck     >= 0.8   && < 0.11,-                       QuickCheck           >= 2.10  && <2.12,-                       quickcheck-instances >=0.3.16 && <0.4,-                       universe-instances-base >= 1.0 && <1.1,-                       lattices,-                       containers,-                       transformers,-                       unordered-containers+  type:             exitcode-stdio-1.0+  main-is:          Tests.hs+  hs-source-dirs:   test+  ghc-options:      -Wall+  default-language: Haskell2010+  build-depends:+      base+    , base-compat+    , containers+    , lattices+    , QuickCheck+    , quickcheck-instances        >=0.3.19 && <0.4+    , tasty                       >=1.2.1  && <1.3+    , tasty-quickcheck            >=0.10   && <0.11+    , transformers+    , universe-base+    , universe-reverse-instances+    , unordered-containers -  if !impl(ghc >= 8.0)-    build-depends:  semigroups                 >= 0.18.3 && < 0.19+  if !impl(ghc >=8.0)+    build-depends: semigroups >=0.18.3 && <0.19

binary file changed (absent → 4757 bytes)

binary file changed (absent → 5473 bytes)

binary file changed (absent → 6606 bytes)

@@ -1,50 +0,0 @@-{-# LANGUAGE Safe #-}-------------------------------------------------------------------------------- |--- Module      :  Algebra.Enumerable--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke--- License     :  BSD-3-Clause (see the file LICENSE)------ Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>---------------------------------------------------------------------------------module Algebra.Enumerable {-# DEPRECATED "Use Data.Universe.Class" #-} (-    Enumerable(..), universeBounded,-    Enumerated(..)-  ) where---- | Finitely enumerable things-class Enumerable a where-    universe :: [a]--universeBounded :: (Enum a, Bounded a) => [a]-universeBounded = enumFromTo minBound maxBound----- | Wrapper used to mark where we expect to use the fact that something is Enumerable-newtype Enumerated a = Enumerated { unEnumerated :: a }-                     deriving (Eq, Ord)--instance Enumerable a => Enumerable (Enumerated a) where-    universe = map Enumerated universe----- TODO: add to this rather sorry little set of instances. Can we exploit commonality with lazy-smallcheck?--instance Enumerable Bool where-    universe = universeBounded--instance Enumerable Int where-    universe = universeBounded--instance Enumerable a => Enumerable (Maybe a) where-    universe = Nothing : map Just universe--instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where-    universe = map Left universe ++ map Right universe--instance Enumerable () where-    universe = [()]--instance (Enumerable a, Enumerable b) => Enumerable (a, b) where-    universe = [(a, b) | a <- universe, b <- universe]

@@ -0,0 +1,151 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE Safe            #-}+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Heyting+-- Copyright   :  (C) 2019 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Heyting where++import Prelude ()+import Prelude.Compat++import Algebra.Lattice+import Control.Applicative   (Const (..))+import Data.Functor.Identity (Identity (..))+import Data.Hashable         (Hashable (..))+import Data.Proxy            (Proxy (..))+import Data.Semigroup        (All (..), Any (..), Endo (..))+import Data.Tagged           (Tagged (..))+import Data.Universe.Class   (Finite (..))++import qualified Data.HashSet as HS+import qualified Data.Set     as S++-- | A Heyting algebra is a bounded lattice equipped with a+-- binary operation \(a \to b\) of implication.+--+-- /Laws/+--+-- @+-- x '==>' x        ≡ 'top'+-- x '/\' (x '==>' y) ≡ x '/\' y+-- y '/\' (x '==>' y) ≡ y+-- x '==>' (y '/\' z) ≡ (x '==>' y) '/\' (x '==>' z)+-- @+--+class BoundedLattice a => Heyting a where+    -- | Implication.+    (==>) :: a -> a -> a++    -- | Negation.+    --+    -- @+    -- 'neg' x = x '==>' 'bottom'+    -- @+    neg :: a -> a+    neg x = x ==> bottom++    -- | Equivalence.+    --+    -- @+    -- x '<=>' y = (x '==>' y) '/\' (y '==>' x)+    -- @+    (<=>) :: a -> a -> a+    x <=> y = (x ==> y) /\ (y ==> x)++infixr 5 ==>, <=>++-------------------------------------------------------------------------------+-- base+-------------------------------------------------------------------------------++instance Heyting () where+    _ ==> _ = ()+    neg _   = ()+    _ <=> _ = ()++instance Heyting Bool where+    False ==> _ = True+    True  ==> y = y++    neg   = not+    (<=>) = (==)++instance Heyting a => Heyting (b -> a) where+    f ==> g = \x -> f x ==> g x+    f <=> g = \x -> f x <=> g x+    neg f   = neg . f++-------------------------------------------------------------------------------+-- All, Any, Endo+-------------------------------------------------------------------------------++instance Heyting All where+    All a ==> All b = All (a ==> b)+    neg (All a)     = All (neg a)+    All a <=> All b = All (a <=> b)++instance Heyting Any where+    Any a ==> Any b = Any (a ==> b)+    neg (Any a)     = Any (neg a)+    Any a <=> Any b = Any (a <=> b)++instance Heyting a => Heyting (Endo a) where+    Endo a ==> Endo b = Endo (a ==> b)+    neg (Endo a)      = Endo (neg a)+    Endo a <=> Endo b = Endo (a <=> b)++-------------------------------------------------------------------------------+-- Proxy, Tagged, Const, Identity+-------------------------------------------------------------------------------++instance Heyting (Proxy a) where+    _ ==> _ = Proxy+    neg _   = Proxy+    _ <=> _ = Proxy++instance Heyting a => Heyting (Identity a) where+    Identity a ==> Identity b = Identity (a ==> b)+    neg (Identity a)          = Identity (neg a)+    Identity a <=> Identity b = Identity (a <=> b)++instance Heyting a => Heyting (Tagged b a) where+    Tagged a ==> Tagged b = Tagged (a ==> b)+    neg (Tagged a)          = Tagged (neg a)+    Tagged a <=> Tagged b = Tagged (a <=> b)++instance Heyting a => Heyting (Const a b) where+    Const a ==> Const b = Const (a ==> b)+    neg (Const a)       = Const (neg a)+    Const a <=> Const b = Const (a <=> b)++-------------------------------------------------------------------------------+-- Sets+-------------------------------------------------------------------------------++instance (Ord a, Finite a) => Heyting (S.Set a) where+    x ==> y = S.union (neg x) y++    neg xs = S.fromList [ x | x <- universeF, S.notMember x xs]++    x <=> y = S.fromList+        [ z+        | z <- universeF+        , S.member z x <=> S.member z y+        ]++instance (Eq a, Hashable a, Finite a) => Heyting (HS.HashSet a) where+    x ==> y = HS.union (neg x) y++    neg xs = HS.fromList [ x | x <- universeF, not $ HS.member x xs]++    x <=> y = HS.fromList+        [ z+        | z <- universeF+        , HS.member z x <=> HS.member z y+        ]

@@ -0,0 +1,183 @@+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Algebra.Heyting.Free (+    Free (..),+    liftFree,+    lowerFree,+    retractFree,+    substFree,+    toExpr,+    ) where++import Prelude ()+import Prelude.Compat++import Algebra.Heyting+import Algebra.Lattice+import Algebra.PartialOrd++import Control.Applicative          (liftA2)+import Control.Monad                (ap)+import Data.Data                    (Data, Typeable)+import GHC.Generics                 (Generic, Generic1)+import Math.NumberTheory.Logarithms (intLog2)++import qualified Algebra.Heyting.Free.Expr as E+import qualified Test.QuickCheck           as QC++-------------------------------------------------------------------------------+-- Free+-------------------------------------------------------------------------------++-- | Free Heyting algebra.+--+-- Note: `Eq` and `PartialOrd` instances aren't structural.+--+-- >>> Top == (Var 'x' ==> Var 'x')+-- True+--+-- >>> Var 'x' == Var 'y'+-- False+--+-- You can test for taulogogies:+--+-- >>> leq Top $ (Var 'A' /\ Var 'B' ==> Var 'C') <=>  (Var 'A' ==> Var 'B' ==> Var 'C')+-- True+--+-- >>> leq Top $ (Var 'A' /\ neg (Var 'A')) <=> Bottom+-- True+--+-- >>> leq Top $ (Var 'A' \/ neg (Var 'A')) <=> Top+-- False+--+data Free a+    = Var a+    | Bottom+    | Top+    | Free a :/\: Free a+    | Free a :\/: Free a+    | Free a :=>: Free a+  deriving (Show, Functor, Foldable, Traversable, Generic, Generic1, Data, Typeable)++infixr 6 :/\:+infixr 5 :\/:+infixr 4 :=>:++liftFree :: a -> Free a+liftFree = Var++substFree :: Free a -> (a -> Free b) -> Free b+substFree z k = go z where+    go (Var x)    = k x+    go Bottom     = Bottom+    go Top        = Top+    go (x :/\: y) = go x /\ go y+    go (x :\/: y) = go x \/ go y+    go (x :=>: y) = go x ==> go y++retractFree :: Heyting a => Free a -> a+retractFree = lowerFree id++lowerFree :: Heyting b => (a -> b) -> Free a -> b+lowerFree f = go where+    go (Var x)    = f x+    go Bottom     = bottom+    go Top        = top+    go (x :/\: y) = go x /\ go y+    go (x :\/: y) = go x \/ go y+    go (x :=>: y) = go x ==> go y++toExpr :: Free a -> E.Expr a+toExpr (Var a)    = E.Var a+toExpr Bottom     = E.Bottom+toExpr Top        = E.Top+toExpr (x :/\: y) = toExpr x E.:/\: toExpr y+toExpr (x :\/: y) = toExpr x E.:\/: toExpr y+toExpr (x :=>: y) = toExpr x E.:=>: toExpr y++-------------------------------------------------------------------------------+-- Monad+-------------------------------------------------------------------------------++instance Applicative Free where+    pure = liftFree+    (<*>) = ap++instance Monad Free where+    return = pure+    (>>=)  = substFree++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++-- instances do small local optimisations.++instance Lattice (Free a) where+    Top    /\ y      = y+    Bottom /\ _      = Bottom+    x      /\ Top    = x+    _      /\ Bottom = Bottom+    x      /\ y      = x :/\: y++    Top    \/ _      = Top+    Bottom \/ y      = y+    _      \/ Top    = Top+    x      \/ Bottom = x+    x      \/ y      = x :\/: y++instance BoundedJoinSemiLattice (Free a) where+    bottom = Bottom++instance BoundedMeetSemiLattice (Free a) where+    top = Top++instance Heyting (Free a) where+    Bottom ==> _   = Top+    Top    ==> y   = y+    _      ==> Top = Top+    x      ==> y   = x :=>: y++instance Ord a => Eq (Free a) where+    x == y = E.proofSearch (toExpr (x <=> y))++instance Ord a => PartialOrd (Free a) where+    leq x y = E.proofSearch (toExpr (x ==> y))++-------------------------------------------------------------------------------+-- Other instances+-------------------------------------------------------------------------------++instance QC.Arbitrary a => QC.Arbitrary (Free a) where+    arbitrary = QC.sized arb where+        arb n | n <= 0    = prim+              | otherwise = QC.oneof (prim : compound)+          where+            arb' = arb (sc n)+            arb'' = arb (sc (sc n)) -- make domains be smaller.++            sc = intLog2 . max 1++            compound =+                [ liftA2 (:/\:) arb' arb'+                , liftA2 (:\/:) arb' arb'+                , liftA2 (:=>:) arb'' arb'+                ]++        prim = QC.frequency+            [ (20, Var <$> QC.arbitrary)+            , (1, pure Bottom)+            , (2, pure Top)+            ]++    shrink (Var c)    = Top : map Var (QC.shrink c)+    shrink Bottom     = []+    shrink Top        = [Bottom]+    shrink (x :/\: y) = x : y : map (uncurry (:/\:)) (QC.shrink (x, y))+    shrink (x :\/: y) = x : y : map (uncurry (:\/:)) (QC.shrink (x, y))+    shrink (x :=>: y) = x : y : map (uncurry (:=>:)) (QC.shrink (x, y))

@@ -0,0 +1,280 @@+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Algebra.Heyting.Free.Expr (+    Expr (..),+    proofSearch,+    ) where++import Prelude ()+import Prelude.Compat++import Control.Monad             (ap)+import Control.Monad.Trans.State (State, evalState, get, put)+import Data.Data                 (Data, Typeable)+import Data.Set                  (Set)+import GHC.Generics              (Generic, Generic1)++import qualified Data.Set as Set++-------------------------------------------------------------------------------+-- Expr+-------------------------------------------------------------------------------++-- | Heyting algebra expression.+--+-- /Note:/ this type doesn't have 'Algebra.Heyting.Heyting' instance,+-- as its 'Eq' and 'Ord' are structural.+--+data Expr a+    = Var a+    | Bottom+    | Top+    | Expr a :/\: Expr a+    | Expr a :\/: Expr a+    | Expr a :=>: Expr a+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic, Generic1, Data, Typeable)++infixr 6 :/\:+infixr 5 :\/:+infixr 4 :=>:++instance Applicative Expr where+    pure = Var+    (<*>) = ap++instance Monad Expr where+    return = pure+    +    Var x      >>= k = k x+    Bottom     >>= _ = Bottom+    Top        >>= _ = Top+    (x :/\: y) >>= k = (x >>= k) :/\: (y >>= k)+    (x :\/: y) >>= k = (x >>= k) :\/: (y >>= k)+    (x :=>: y) >>= k = (x >>= k) :=>: (y >>= k)++-------------------------------------------------------------------------------+-- LJT proof search+-------------------------------------------------------------------------------++-- | Decide whether @x :: 'Expr' a@ is provable.+--+-- /Note:/ this doesn't construct a proof term, but merely returns a 'Bool'.+--+proofSearch :: forall a. Ord a => Expr a -> Bool+proofSearch tyGoal = evalState (emptyCtx |- fmap R tyGoal) 0+  where+    freshVar = do+        n <- get+        put (n + 1)+        return (L n)++    infix 4 |-+    infixr 3 .&&++    (.&&) :: Monad m => m Bool -> m Bool -> m Bool+    x .&& y = do+        x' <- x+        if x'+        then y+        else return False++    (|-) :: Ctx a -> Expr (Am a) -> State Int Bool++    -- Ctx ats ai ii xs |- _+    --     | traceShow (length ats, length ai, length ii, length xs) False+    --     = return False++    -- T-R+    _ctx |- Top+        = return True++    -- T-L+    Ctx ats ai ii (Top : ctx) |- ty+        = Ctx ats ai ii ctx |- ty++    -- F-L+    Ctx _ _ _ (Bottom : _ctx) |- _ty+        = return True++    -- Id-atoms+    Ctx ats _ai _ii [] |- Var a+        | Set.member a ats+        = return True++    -- Id+    Ctx _ats _ai _ii (x : _ctx) |- ty+        | x == ty+        = return True++    -- Move atoms to atoms part of context+    Ctx ats ai ii (Var a : ctx) |- ty+        = Ctx (Set.insert a ats) ai ii ctx |- ty++    -- =>-R+    Ctx ats ai ii ctx |- (a :=>: b)+        = Ctx ats ai ii (a : ctx) |- b++    -- /\-L+    Ctx ats ai ii ((x :/\: y) : ctx) |- ty+        = Ctx ats ai ii (x : y : ctx) |- ty++    -- =>-L-extra (Top)+    --+    -- \Gamma, C      |- G+    -- --------------------------+    -- \Gamma, 1 -> C |- G+    --+    Ctx ats ai ii ((Top :=>: c) : ctx) |- ty+        = Ctx ats ai ii (c : ctx) |- ty++    -- =>-L-extra (Bottom)+    --+    -- \Gamma         |- G+    -- --------------------------+    -- \Gamma, 0 -> C |- G+    --+    Ctx ats ai ii ((Bottom :=>: _) : ctx) |- ty+        = Ctx ats ai ii ctx |- ty++    -- =>-L2 (Conj)+    --+    -- \Gamma, A -> (B -> C) |- G+    -- --------------------------+    -- \Gamma, (A /\ B) -> C |- G+    --+    Ctx ats ai ii ((a :/\: b :=>: c) : ctx) |- ty+        = Ctx ats ai ii ((a :=>: b :=>: c) : ctx) |- ty++    -- =>-L3 (Disj)+    --+    -- \Gamma, A -> C, B -> C |- G+    -- ---------------------------+    -- \Gamma, (A \/ B) -> C  |- G+    --+    -- or with fresh var: (P = A \/ B, but an atom)+    --+    -- \Gamma, A -> P, B -> P, P -> C |- G+    -- -----------------------------------+    -- \Gamma, (A \/ B) -> C          |- G+    --+    Ctx ats ai ii ((a :\/: b :=>: c) : ctx) |- ty = do+        p <- Var <$> freshVar+        Ctx ats ai ii ((p :=>: c) : (a :=>: p) : (b :=>: p) : ctx) |- ty++    -- =>-L4 preparation+    --+    -- \Gamma, B -> C, A |- B    \Gamma, C |- G+    -- ------------------------------------------+    -- \Gamma, (A -> B) -> C |- G+    --+    Ctx ats ai ii (((a :=>: b) :=>: c) : ctx) |- ty+        = Ctx ats ai (Set.insert (ImplImpl a b c) ii) ctx |- ty++    -- =>-L1 preparation+    --+    -- \Gamma, X, B      |- G+    -- ----------------------+    -- \Gamma, X, X -> B |- G+    --+    Ctx ats ai ii ((Var x :=>: b) : ctx) |- ty+        = Ctx ats (Set.insert (AtomImpl x b) ai) ii ctx |- ty++    -- These two rules, (\/-L) and (/\-R), are pushed to the last, as they branch.++    -- \/-L+    Ctx ats ai ii ((x :\/: y) : ctx) |- ty+        =   Ctx ats ai ii (x : ctx) |- ty+        .&& Ctx ats ai ii (y : ctx) |- ty++    -- /\-R+    ctx |- (a :/\: b)+        =   ctx |- a+        .&& ctx |- b++    -- Last rules+    Ctx ats ai ii [] |- ty+        -- L1 completion+        | ((y, ai') : _) <- match+        = Ctx ats ai' ii [y] |- ty++        -- \/-R and =>-L4+        | not (null rest) = iter rest+      where+        match =+            [ (y, Set.delete ai' ai)+            | ai'@(AtomImpl x y) <- Set.toList ai+            , x `Set.member` ats+            ]++        -- try in order+        iter [] = return False+        iter (Right (ctx', ty') : rest') = do+            res <- ctx' |- ty'+            if res+            then return True+            else iter rest'++        iter (Left (ctxa, a, ctxb, b) : rest') = do+            res <- ctxa |- a .&& ctxb |- b+            if res+            then return True+            else iter rest'++        rest = disj ++ implImpl++        -- =>-L4+        implImpl =+            [ Left (Ctx ats ai ii' [x, y :=>: z], y, Ctx ats ai ii' [z], ty)+            | entry@(ImplImpl x y z) <- Set.toList ii+            , let ii' = Set.delete entry ii+            ]++        -- \/-R+        disj = case ty of+            a :\/: b ->+                [ Right (Ctx ats ai ii [], a)+                , Right (Ctx ats ai ii [], b)+                ]+            _ -> []++    Ctx _ _ _ [] |- (_ :\/: _)+        = error "panic! @proofSearch should be matched before"++    Ctx _ _ _ [] |- Var _+        = return False++    Ctx _ _ _ [] |- Bottom+        = return False++-------------------------------------------------------------------------------+-- Context+-------------------------------------------------------------------------------++data Am a+    = L !Int+    | R a+  deriving (Eq, Ord, Show)++data Ctx a = Ctx+    { ctxAtoms      :: Set (Am a)+    , ctxAtomImpl   :: Set (AtomImpl a)+    , ctxImplImpl   :: Set (ImplImpl a)+    , ctxHypothesis :: [Expr (Am a)]+    }+  deriving Show++emptyCtx :: Ctx l+emptyCtx = Ctx Set.empty Set.empty Set.empty []++-- [[ AtomImpl a b ]] = a => b+data AtomImpl a = AtomImpl (Am a) (Expr (Am a))+  deriving (Eq, Ord, Show)++-- [[ ImplImpl a b c ]] = (a ==> b) ==> c+data ImplImpl a = ImplImpl !(Expr (Am a)) !(Expr (Am a)) !(Expr (Am a))+  deriving (Eq, Ord, Show)

@@ -1,23 +1,12 @@-{-# LANGUAGE CPP                #-}-{-# LANGUAGE FlexibleInstances  #-}+{-# LANGUAGE ConstraintKinds    #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric      #-}-#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709-{-# OPTIONS_GHC -fno-warn-amp #-}-#endif--#define unordered_containers_SAFE MIN_VERSION_unordered_containers(0,2,6)-#define semigroupoids_SAFE (!MIN_VERSION_semigroupoids(5,2,2) || __GLASGOW_HASKELL__ >= 802)--#if __GLASGOW_HASKELL__ >= 710 && unordered_containers_SAFE && semigroupoids_SAFE+{-# LANGUAGE FlexibleInstances  #-} {-# LANGUAGE Safe               #-}-#else-{-# LANGUAGE Trustworthy        #-}-#endif ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -33,13 +22,14 @@ ---------------------------------------------------------------------------- module Algebra.Lattice (     -- * Unbounded lattices-    JoinSemiLattice(..), MeetSemiLattice(..), Lattice,+    Lattice (..),     joinLeq, joins1, meetLeq, meets1,      -- * Bounded lattices-    BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice,+    BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..),     joins, meets,     fromBool,+    BoundedLattice,      -- * Monoid wrappers     Meet(..), Join(..),@@ -54,86 +44,95 @@  import qualified Algebra.PartialOrd as PO -import Data.Universe.Class (Finite (..), Universe (..))--import Control.Monad.Zip (MonadZip (..))-import Data.Data         (Data, Typeable)-import Data.Hashable     (Hashable (..))-import Data.Proxy        (Proxy (..))-import Data.Semigroup    (All (..), Any (..), Endo (..), Semigroup (..))-import Data.Tagged       (Tagged (..))-import Data.Void         (Void)-import GHC.Generics      (Generic)--import qualified Data.IntMap as IM-import qualified Data.IntSet as IS-import qualified Data.Map    as M-import qualified Data.Set    as S--import qualified Data.HashMap.Lazy as HM-import qualified Data.HashSet      as HS- import Control.Applicative     (Const (..))+import Control.Monad.Zip       (MonadZip (..))+import Data.Data               (Data, Typeable) import Data.Functor.Identity   (Identity (..))+import Data.Hashable           (Hashable (..))+import Data.Proxy              (Proxy (..))+import Data.Semigroup          (All (..), Any (..), Endo (..), Semigroup (..)) import Data.Semigroup.Foldable (Foldable1 (..))+import Data.Tagged             (Tagged (..))+import Data.Universe.Class     (Finite (..), Universe (..))+import Data.Void               (Void)+import GHC.Generics            (Generic) +import qualified Data.HashMap.Lazy as HM+import qualified Data.HashSet      as HS+import qualified Data.IntMap       as IM+import qualified Data.IntSet       as IS+import qualified Data.Map          as M+import qualified Data.Set          as S+import qualified Test.QuickCheck   as QC+ infixr 6 /\ -- This comment needed because of CPP infixr 5 \/ --- | A algebraic structure with element joins: <http://en.wikipedia.org/wiki/Semilattice>+-- | An algebraic structure with joins and meets. ----- > Associativity: x \/ (y \/ z) == (x \/ y) \/ z--- > Commutativity: x \/ y == y \/ x--- > Idempotency:   x \/ x == x-class JoinSemiLattice a where+-- See <http://en.wikipedia.org/wiki/Lattice_(order)> and <http://en.wikipedia.org/wiki/Absorption_law>.+--+-- 'Lattice' is very symmetric, which is seen from the laws:+--+-- /Associativity/+--+-- @+-- x '\/' (y '\/' z) ≡ (x '\/' y) '\/' z+-- x '/\' (y '/\' z) ≡ (x '/\' y) '/\' z+-- @+--+-- /Commputativity/+--+-- @+-- x '\/' y ≡ y '\/' x+-- x '/\' y ≡ y '/\' x+-- @+--+-- /Idempotency/+--+-- @+-- x '\/' x ≡ x+-- x '/\' x ≡ x+-- @+--+-- /Absorption/+--+-- @+-- a '\/' (a '/\' b) ≡ a+-- a '/\' (a '\/' b) ≡ a+-- @+class Lattice a where+    -- | join     (\/) :: a -> a -> a-    (\/) = join -    join :: a -> a -> a-    join = (\/)--#if __GLASGOW_HASKELL__ >= 707-    {-# MINIMAL (\/) | join #-}-#endif-{-# DEPRECATED join "Use '\\/' infix operator" #-}+    -- | meet+    (/\) :: a -> a -> a  -- | The partial ordering induced by the join-semilattice structure-joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool+joinLeq :: (Eq a, Lattice a) => a -> a -> Bool joinLeq x y = (x \/ y) == y --- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice>------ > Associativity: x /\ (y /\ z) == (x /\ y) /\ z--- > Commutativity: x /\ y == y /\ x--- > Idempotency:   x /\ x == x-class MeetSemiLattice a where-    (/\) :: a -> a -> a-    (/\) = meet--    meet :: a -> a -> a-    meet = (/\)--#if __GLASGOW_HASKELL__ >= 707-    {-# MINIMAL (/\) | meet #-}-#endif-{-# DEPRECATED meet "Use '/\\' infix operator" #-}---- | The partial ordering induced by the meet-semilattice structure-meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool+meetLeq :: (Eq a, Lattice a) => a -> a -> Bool meetLeq x y = (x /\ y) == x ----- | The combination of two semi lattices makes a lattice if the absorption law holds:--- see <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)>------ > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a-class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where- -- | A join-semilattice with an identity element 'bottom' for '\/'. ----- > Identity: x \/ bottom == x-class JoinSemiLattice a => BoundedJoinSemiLattice a where+-- /Laws/+--+-- @+-- x '\/' 'bottom' ≡ x+-- @+--+-- /Corollary/+--+-- @+-- x '/\' 'bottom'+--   ≡⟨ identity ⟩+-- (x '/\' 'bottom') '\/' 'bottom'+--   ≡⟨ absorption ⟩+-- 'bottom'+-- @+class Lattice a => BoundedJoinSemiLattice a where     bottom :: a  -- | The join of a list of join-semilattice elements@@ -141,13 +140,28 @@ joins = getJoin . foldMap Join  -- | The join of at a list of join-semilattice elements (of length at least one)-joins1 :: (JoinSemiLattice a, Foldable1 f) => f a -> a+joins1 :: (Lattice a, Foldable1 f) => f a -> a joins1 =  getJoin . foldMap1 Join  -- | A meet-semilattice with an identity element 'top' for '/\'. ----- > Identity: x /\ top == x-class MeetSemiLattice a => BoundedMeetSemiLattice a where+-- /Laws/+--+-- @+-- x '/\' 'top' ≡ x+-- @+--+-- /Corollary/+--+-- @+-- x '\/' 'top'+--   ≡⟨ identity ⟩+-- (x '\/' 'top') '/\' 'top'+--   ≡⟨ absorption ⟩+-- 'top'+-- @+--+class Lattice a => BoundedMeetSemiLattice a where     top :: a  -- | The meet of a list of meet-semilattice elements@@ -155,11 +169,10 @@ meets = getMeet . foldMap Meet -- -- | The meet of at a list of meet-semilattice elements (of length at least one)-meets1 :: (MeetSemiLattice a, Foldable1 f) => f a -> a+meets1 :: (Lattice a, Foldable1 f) => f a -> a meets1 = getMeet . foldMap1 Meet --- | Lattices with both bounds-class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where+type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a)  -- | 'True' to 'top' and 'False' to 'bottom' fromBool :: BoundedLattice a => Bool -> a@@ -170,34 +183,24 @@ -- Sets -- -instance Ord a => JoinSemiLattice (S.Set a) where+instance Ord a => Lattice (S.Set a) where     (\/) = S.union--instance Ord a => MeetSemiLattice (S.Set a) where     (/\) = S.intersection -instance Ord a => Lattice (S.Set a)- instance Ord a => BoundedJoinSemiLattice (S.Set a) where     bottom = S.empty  instance (Ord a, Finite a) => BoundedMeetSemiLattice (S.Set a) where     top = S.fromList universeF -instance (Ord a, Finite a) => BoundedLattice (S.Set a)- -- -- IntSets -- -instance JoinSemiLattice IS.IntSet where+instance Lattice IS.IntSet where     (\/) = IS.union--instance MeetSemiLattice IS.IntSet where     (/\) = IS.intersection -instance Lattice IS.IntSet- instance BoundedJoinSemiLattice IS.IntSet where     bottom = IS.empty @@ -205,168 +208,127 @@ -- HashSet -- -instance (Eq a, Hashable a) => JoinSemiLattice (HS.HashSet a) where-    (\/) = HS.union -instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where+instance (Eq a, Hashable a) => Lattice (HS.HashSet a) where+    (\/) = HS.union     (/\) = HS.intersection -instance (Eq a, Hashable a) => Lattice (HS.HashSet a)- instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where     bottom = HS.empty  instance (Eq a, Hashable a, Finite a) => BoundedMeetSemiLattice (HS.HashSet a) where     top = HS.fromList universeF -instance (Eq a, Hashable a, Finite a) => BoundedLattice (HS.HashSet a)- -- -- Maps -- -instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where+instance (Ord k, Lattice v) => Lattice (M.Map k v) where     (\/) = M.unionWith (\/)--instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where     (/\) = M.intersectionWith (/\) -instance (Ord k, Lattice v) => Lattice (M.Map k v) where--instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where+instance (Ord k, Lattice v) => BoundedJoinSemiLattice (M.Map k v) where     bottom = M.empty  instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map k v) where     top = M.fromList (universeF `zip` repeat top) -instance (Ord k, Finite k, BoundedLattice v) => BoundedLattice (M.Map k v) where- -- -- IntMaps -- -instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where+instance Lattice v => Lattice (IM.IntMap v) where     (\/) = IM.unionWith (\/)--instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where-    bottom = IM.empty--instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where     (/\) = IM.intersectionWith (/\) -instance Lattice v => Lattice (IM.IntMap v)-+instance Lattice v => BoundedJoinSemiLattice (IM.IntMap v) where+    bottom = IM.empty  -- -- HashMaps -- -instance (Eq k, Hashable k, JoinSemiLattice v) => JoinSemiLattice (HM.HashMap k v) where-    (\/) = HM.unionWith (\/)--instance (Eq k, Hashable k, MeetSemiLattice v) => MeetSemiLattice (HM.HashMap k v) where-    (/\) = HM.intersectionWith (/\)--instance (Eq k, Hashable k, JoinSemiLattice v) => BoundedJoinSemiLattice (HM.HashMap k v) where+instance (Eq k, Hashable k, Lattice v) => BoundedJoinSemiLattice (HM.HashMap k v) where     bottom = HM.empty  instance (Eq k, Hashable k, Lattice v) => Lattice (HM.HashMap k v) where+    (\/) = HM.unionWith (\/)+    (/\) = HM.intersectionWith (/\)  instance (Eq k, Hashable k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (HM.HashMap k v) where     top = HM.fromList (universeF `zip` repeat top) -instance (Eq k, Hashable k, Finite k, BoundedLattice v) => BoundedLattice (HM.HashMap k v) where- -- -- Functions -- -instance JoinSemiLattice v => JoinSemiLattice (k -> v) where+instance Lattice v => Lattice (k -> v) where     f \/ g = \x -> f x \/ g x--instance MeetSemiLattice v => MeetSemiLattice (k -> v) where     f /\ g = \x -> f x /\ g x -instance Lattice v => Lattice (k -> v) where- instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where     bottom = const bottom  instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where     top = const top -instance BoundedLattice v => BoundedLattice (k -> v) where-+-- -- Unit-instance JoinSemiLattice () where-  _ \/ _ = ()+-- ++instance Lattice () where+    _ \/ _ = ()+    _ /\ _ = ()+ instance BoundedJoinSemiLattice () where   bottom = () -instance MeetSemiLattice () where-  _ /\ _ = ()- instance BoundedMeetSemiLattice () where   top = () -instance Lattice () where-instance BoundedLattice () where- -- -- Tuples -- -instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where+instance (Lattice a, Lattice b) => Lattice (a, b) where     (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2)--instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where     (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2) -instance (Lattice a, Lattice b) => Lattice (a, b) where- instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where     bottom = (bottom, bottom)  instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where     top = (top, top) -instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where- -- -- Bools -- -instance JoinSemiLattice Bool where+instance Lattice Bool where     (\/) = (||)--instance MeetSemiLattice Bool where     (/\) = (&&) -instance Lattice Bool where- instance BoundedJoinSemiLattice Bool where     bottom = False  instance BoundedMeetSemiLattice Bool where     top = True -instance BoundedLattice Bool where- --- Monoids --- | Monoid wrapper for JoinSemiLattice+-- | Monoid wrapper for join-'Lattice' newtype Join a = Join { getJoin :: a }   deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) -instance JoinSemiLattice a => Semigroup (Join a) where+instance Lattice a => Semigroup (Join a) where   Join a <> Join b = Join (a \/ b)  instance BoundedJoinSemiLattice a => Monoid (Join a) where   mempty = Join bottom   Join a `mappend` Join b = Join (a \/ b) -instance (Eq a, JoinSemiLattice a) => PO.PartialOrd (Join a) where+instance (Eq a, Lattice a) => PO.PartialOrd (Join a) where   leq (Join a) (Join b) = joinLeq a b  instance Functor Join where@@ -391,18 +353,18 @@ instance Finite a => Finite (Join a) where   universeF = fmap Join universeF --- | Monoid wrapper for MeetSemiLattice+-- | Monoid wrapper for meet-'Lattice' newtype Meet a = Meet { getMeet :: a }   deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) -instance MeetSemiLattice a => Semigroup (Meet a) where+instance Lattice a => Semigroup (Meet a) where   Meet a <> Meet b = Meet (a /\ b)  instance BoundedMeetSemiLattice a => Monoid (Meet a) where   mempty = Meet top   Meet a `mappend` Meet b = Meet (a /\ b) -instance (Eq a, MeetSemiLattice a) => PO.PartialOrd (Meet a) where+instance (Eq a, Lattice a) => PO.PartialOrd (Meet a) where   leq (Meet a) (Meet b) = meetLeq a b  instance Functor Meet where@@ -428,127 +390,107 @@   universeF = fmap Meet universeF  -- All-instance JoinSemiLattice All where++instance Lattice All where   All a \/ All b = All $ a \/ b+  All a /\ All b = All $ a /\ b  instance BoundedJoinSemiLattice All where   bottom = All False -instance MeetSemiLattice All where-  All a /\ All b = All $ a /\ b- instance BoundedMeetSemiLattice All where   top = All True -instance Lattice All where-instance BoundedLattice All where- -- Any-instance JoinSemiLattice Any where+instance Lattice Any where   Any a \/ Any b = Any $ a \/ b+  Any a /\ Any b = Any $ a /\ b  instance BoundedJoinSemiLattice Any where   bottom = Any False -instance MeetSemiLattice Any where-  Any a /\ Any b = Any $ a /\ b- instance BoundedMeetSemiLattice Any where   top = Any True -instance Lattice Any where-instance BoundedLattice Any where- -- Endo-instance JoinSemiLattice a => JoinSemiLattice (Endo a) where+instance Lattice a => Lattice (Endo a) where   Endo a \/ Endo b = Endo $ a \/ b+  Endo a /\ Endo b = Endo $ a /\ b  instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where   bottom = Endo bottom -instance MeetSemiLattice a => MeetSemiLattice (Endo a) where-  Endo a /\ Endo b = Endo $ a /\ b- instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where   top = Endo top -instance Lattice a => Lattice (Endo a) where-instance BoundedLattice a => BoundedLattice (Endo a) where- -- Tagged-instance JoinSemiLattice a => JoinSemiLattice (Tagged t a) where++instance Lattice a => Lattice (Tagged t a) where   Tagged a \/ Tagged b = Tagged $ a \/ b+  Tagged a /\ Tagged b = Tagged $ a /\ b  instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged t a) where   bottom = Tagged bottom -instance MeetSemiLattice a => MeetSemiLattice (Tagged t a) where-  Tagged a /\ Tagged b = Tagged $ a /\ b- instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where   top = Tagged top -instance Lattice a => Lattice (Tagged t a) where-instance BoundedLattice a => BoundedLattice (Tagged t a) where- -- Proxy-instance JoinSemiLattice (Proxy a) where+instance Lattice (Proxy a) where   _ \/ _ = Proxy+  _ /\ _ = Proxy  instance BoundedJoinSemiLattice (Proxy a) where   bottom = Proxy -instance MeetSemiLattice (Proxy a) where-  _ /\ _ = Proxy- instance BoundedMeetSemiLattice (Proxy a) where   top = Proxy -instance Lattice (Proxy a) where-instance BoundedLattice (Proxy a) where--#if MIN_VERSION_base(4,8,0) -- Identity-instance JoinSemiLattice a => JoinSemiLattice (Identity a) where-  Identity a \/ Identity b = Identity (a \/ b) -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where-  bottom = Identity bottom--instance MeetSemiLattice a => MeetSemiLattice (Identity a) where+instance Lattice a => Lattice (Identity a) where+  Identity a \/ Identity b = Identity (a \/ b)   Identity a /\ Identity b = Identity (a /\ b)  instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where   top = Identity top -instance Lattice a => Lattice (Identity a) where-instance BoundedLattice a => BoundedLattice (Identity a) where-#endif+instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where+  bottom = Identity bottom  -- Const-instance JoinSemiLattice a => JoinSemiLattice (Const a b) where+instance Lattice a => Lattice (Const a b) where   Const a \/ Const b = Const (a \/ b)+  Const a /\ Const b = Const (a /\ b)  instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where   bottom = Const bottom -instance MeetSemiLattice a => MeetSemiLattice (Const a b) where-  Const a /\ Const b = Const (a /\ b)- instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where   top = Const top -instance Lattice a => Lattice (Const a b) where-instance BoundedLattice a => BoundedLattice (Const a b) where-+------------------------------------------------------------------------------- -- Void-instance JoinSemiLattice Void where-  a \/ _ = a+------------------------------------------------------------------------------- -instance MeetSemiLattice Void where+instance Lattice Void where+  a \/ _ = a   a /\ _ = a -instance Lattice Void where+-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance Lattice QC.Property where+  (\/) = (QC..||.)+  (/\) = (QC..&&.)++instance BoundedJoinSemiLattice QC.Property where bottom = QC.property False+instance BoundedMeetSemiLattice QC.Property where top = QC.property True++-------------------------------------------------------------------------------+-- Theorems+-------------------------------------------------------------------------------  -- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>. -- Assumes that the function is monotone and does not check if that is correct.

@@ -1,20 +1,16 @@-{-# LANGUAGE CPP                #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveFoldable     #-}-{-# LANGUAGE DeriveFunctor      #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE DeriveTraversable  #-}-{-# LANGUAGE FlexibleContexts   #-}-{-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else-{-# LANGUAGE Safe               #-}-#endif+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-} ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Divisibility--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -30,12 +26,16 @@ import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq       (NFData (..))+import Control.Monad         (ap)+import Data.Data             (Data, Typeable)+import Data.Hashable         (Hashable (..))+import Data.Universe.Class   (Finite (..), Universe (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import GHC.Generics          (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Divisibility --@@ -43,9 +43,7 @@ -- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. newtype Divisibility a = Divisibility { getDivisibility :: a }   deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706            , Generic1-#endif            )  instance Applicative Divisibility where@@ -61,16 +59,34 @@  instance Hashable a => Hashable (Divisibility a) -instance Integral a => JoinSemiLattice (Divisibility a) where+instance Integral a => Lattice (Divisibility a) where   Divisibility x \/ Divisibility y = Divisibility (lcm x y) -instance Integral a => MeetSemiLattice (Divisibility a) where   Divisibility x /\ Divisibility y = Divisibility (gcd x y) -instance Integral a => Lattice (Divisibility a) where- instance Integral a => BoundedJoinSemiLattice (Divisibility a) where   bottom = Divisibility 1  instance (Eq a, Integral a) => PartialOrd (Divisibility a) where     leq (Divisibility a) (Divisibility b) = b `mod` a == 0++instance Universe a => Universe (Divisibility a) where+    universe = map Divisibility universe+instance Finite a => Finite (Divisibility a) where+    universeF = map Divisibility universeF+    cardinality = retag (cardinality :: Tagged a Natural)++instance (QC.Arbitrary a, Num a, Ord a) => QC.Arbitrary (Divisibility a) where+    arbitrary = divisibility <$> QC.arbitrary+    shrink d = filter (<d) . map divisibility . QC.shrink . getDivisibility $ d++instance QC.CoArbitrary a => QC.CoArbitrary (Divisibility a) where+    coarbitrary = QC.coarbitrary . getDivisibility++instance QC.Function a => QC.Function (Divisibility a) where+    function = QC.functionMap getDivisibility Divisibility++divisibility :: (Ord a, Num a) => a -> Divisibility a+divisibility x | x < (-1)  = Divisibility (abs x)+               | x < 1     = Divisibility 1+               | otherwise = Divisibility x

@@ -1,20 +1,16 @@-{-# LANGUAGE CPP                #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveFoldable     #-}-{-# LANGUAGE DeriveFunctor      #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE DeriveTraversable  #-}-{-# LANGUAGE FlexibleContexts   #-}-{-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else-{-# LANGUAGE Safe               #-}-#endif+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-} ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Dropped--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -23,31 +19,35 @@ module Algebra.Lattice.Dropped (     Dropped(..)   , retractDropped+  , foldDropped   ) where  import Prelude () import Prelude.Compat  import Algebra.Lattice+import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq       (NFData (..))+import Control.Monad         (ap)+import Data.Data             (Data, Typeable)+import Data.Hashable         (Hashable (..))+import Data.Universe.Class   (Finite (..), Universe (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import GHC.Generics          (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Dropped --  -- | Graft a distinct top onto an otherwise unbounded lattice. -- As a bonus, the top will be an absorbing element for the join.-data Dropped a = Top-               | Drop a+data Dropped a = Drop a+               | Top   deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706            , Generic1-#endif            )  instance Applicative Dropped where@@ -65,27 +65,58 @@  instance Hashable a => Hashable (Dropped a) -instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where+instance PartialOrd a => PartialOrd (Dropped a) where+  leq _ Top = True+  leq Top _ = False+  leq (Drop x) (Drop y) = leq x y+  comparable Top _ = True+  comparable _ Top = True+  comparable (Drop x) (Drop y) = comparable x y++instance Lattice a => Lattice (Dropped a) where     Top    \/ _      = Top     _      \/ Top    = Top     Drop x \/ Drop y = Drop (x \/ y) -instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where     Top    /\ drop_y = drop_y     drop_x /\ Top    = drop_x     Drop x /\ Drop y = Drop (x /\ y) -instance Lattice a => Lattice (Dropped a) where- instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where     bottom = Drop bottom -instance MeetSemiLattice a => BoundedMeetSemiLattice (Dropped a) where+instance Lattice a => BoundedMeetSemiLattice (Dropped a) where     top = Top -instance BoundedLattice a => BoundedLattice (Dropped a) where- -- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@. retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a-retractDropped Top       = top-retractDropped (Drop x)  = x+retractDropped = foldDropped top id++-- | Similar to @'maybe'@, but for @'Dropped'@ type.+foldDropped :: b -> (a -> b) -> Dropped a -> b+foldDropped _ f (Drop x) = f x+foldDropped y _ Top      = y++instance Universe a => Universe (Dropped a) where+    universe = Top : map Drop universe+instance Finite a => Finite (Dropped a) where+    universeF = Top : map Drop universeF+    cardinality = fmap succ (retag (cardinality :: Tagged a Natural))++instance QC.Arbitrary a => QC.Arbitrary (Dropped a) where+    arbitrary = QC.frequency+        [ (1, pure Top)+        , (9, Drop <$> QC.arbitrary)+        ]++    shrink Top      = []+    shrink (Drop x) = Top : map Drop (QC.shrink x)++instance QC.CoArbitrary a => QC.CoArbitrary (Dropped a) where+    coarbitrary Top      = QC.variant (0 :: Int)+    coarbitrary (Drop x) = QC.variant (1 :: Int) . QC.coarbitrary x++instance QC.Function a => QC.Function (Dropped a) where+    function = QC.functionMap fromDropped toDropped where+        fromDropped = foldDropped Nothing Just+        toDropped   = maybe Top Drop

@@ -1,148 +1,144 @@-{-# LANGUAGE RankNTypes #-}--------------------------------------------------------------------------------- |--- Module      :  Algebra.Lattice.Free--- License     :  BSD-3-Clause (see the file LICENSE)------ Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>----------------------------------------------------------------------------------module Algebra.Lattice.Free-  ( -- * Free join-semilattices-    FreeJoinSemiLattice-  , liftFreeJoinSemiLattice-  , lowerFreeJoinSemiLattice-  , retractFreeJoinSemiLattice--   -- * Free meet-semilattices-  , FreeMeetSemiLattice-  , liftFreeMeetSemiLattice-  , lowerFreeMeetSemiLattice-  , retractFreeMeetSemiLattice--   -- * Free lattices-  , FreeLattice-  , liftFreeLattice-  , lowerFreeLattice-  , retractFreeLattice-  ) where+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Algebra.Lattice.Free (+    Free (..),+    liftFree,+    lowerFree,+    substFree,+    retractFree,+    toExpr,+    ) where  import Prelude () import Prelude.Compat  import Algebra.Lattice-import Data.Universe.Class------- Free join-semilattices-----newtype FreeJoinSemiLattice a = FreeJoinSemiLattice-  { lowerFreeJoinSemiLattice :: forall b. JoinSemiLattice b =>-                                            (a -> b) -> b-  }--liftFreeJoinSemiLattice :: a -> FreeJoinSemiLattice a-liftFreeJoinSemiLattice a = FreeJoinSemiLattice (\inj -> inj a)--retractFreeJoinSemiLattice :: JoinSemiLattice a => FreeJoinSemiLattice a -> a-retractFreeJoinSemiLattice a = lowerFreeJoinSemiLattice a id--instance Functor FreeJoinSemiLattice where-  fmap f (FreeJoinSemiLattice g) = FreeJoinSemiLattice (\inj -> g (inj . f))-  a <$ FreeJoinSemiLattice f = FreeJoinSemiLattice (\inj -> f (const (inj a)))--instance JoinSemiLattice (FreeJoinSemiLattice a) where-  FreeJoinSemiLattice f \/ FreeJoinSemiLattice g =-    FreeJoinSemiLattice (\inj -> f inj \/ g inj)--instance BoundedJoinSemiLattice a =>-         BoundedJoinSemiLattice (FreeJoinSemiLattice a) where-  bottom = FreeJoinSemiLattice (\inj -> inj bottom)+import Algebra.PartialOrd -instance Universe a => Universe (FreeJoinSemiLattice a) where-  universe = fmap liftFreeJoinSemiLattice universe+import Control.Applicative          (liftA2)+import Control.Monad                (ap)+import Data.Data                    (Data, Typeable)+import GHC.Generics                 (Generic, Generic1)+import Math.NumberTheory.Logarithms (intLog2) -instance Finite a => Finite (FreeJoinSemiLattice a) where-  universeF = fmap liftFreeJoinSemiLattice universeF+import qualified Algebra.Heyting.Free.Expr as E+import qualified Test.QuickCheck           as QC +-------------------------------------------------------------------------------+-- Free+------------------------------------------------------------------------------- +-- | Free distributive lattice. ----- Free meet-semilattices+-- `Eq` and `PartialOrd` instances aren't structural. ----newtype FreeMeetSemiLattice a = FreeMeetSemiLattice-  { lowerFreeMeetSemiLattice :: forall b. MeetSemiLattice b =>-                                            (a -> b) -> b-  }--instance Functor FreeMeetSemiLattice where-  fmap f (FreeMeetSemiLattice g) = FreeMeetSemiLattice (\inj -> g (inj . f))-  a <$ FreeMeetSemiLattice f = FreeMeetSemiLattice (\inj -> f (const (inj a)))--liftFreeMeetSemiLattice :: a -> FreeMeetSemiLattice a-liftFreeMeetSemiLattice a = FreeMeetSemiLattice (\inj -> inj a)--retractFreeMeetSemiLattice :: MeetSemiLattice a => FreeMeetSemiLattice a -> a-retractFreeMeetSemiLattice a = lowerFreeMeetSemiLattice a id+-- >>> (Var 'x' /\ Var 'y') == (Var 'y' /\ Var 'x' /\ Var 'x')+-- True+--+-- >>> Var 'x' == Var 'y'+-- False+--+-- This is /distributive/ lattice.+--+-- >>> import Algebra.Lattice.M3 -- non distributive lattice+-- >>> let x = M3a; y = M3b; z = M3c+-- >>> let lhs = Var x \/ (Var y /\ Var z)+-- >>> let rhs = (Var x \/ Var y) /\ (Var x \/ Var z)+--+-- 'Free' is distributive so +--+-- >>> lhs == rhs+-- True+--+-- but when retracted, values are inequal+--+-- >>> retractFree lhs == retractFree rhs+-- False+--+-- >>> (retractFree lhs, retractFree rhs)+-- (M3a,M3i)+--+data Free a+    = Var a+    | Free a :/\: Free a+    | Free a :\/: Free a+  deriving (Show, Functor, Foldable, Traversable, Generic, Generic1, Data, Typeable) -instance MeetSemiLattice (FreeMeetSemiLattice a) where-  FreeMeetSemiLattice f /\ FreeMeetSemiLattice g =-    FreeMeetSemiLattice (\inj -> f inj /\ g inj)+infixr 6 :/\:+infixr 5 :\/: -instance BoundedMeetSemiLattice a =>-         BoundedMeetSemiLattice (FreeMeetSemiLattice a) where-  top = FreeMeetSemiLattice (\inj -> inj top)+liftFree :: a -> Free a+liftFree = Var -instance Universe a => Universe (FreeMeetSemiLattice a) where-  universe = fmap liftFreeMeetSemiLattice universe+retractFree :: Lattice a => Free a -> a+retractFree = lowerFree id -instance Finite a => Finite (FreeMeetSemiLattice a) where-  universeF = fmap liftFreeMeetSemiLattice universeF+substFree :: Free a -> (a -> Free b) -> Free b+substFree z k = go z where+    go (Var x)    = k x+    go (x :/\: y) = go x /\ go y+    go (x :\/: y) = go x \/ go y +lowerFree :: Lattice b => (a -> b) -> Free a -> b+lowerFree f = go where+    go (Var x)    = f x+    go (x :/\: y) = go x /\ go y+    go (x :\/: y) = go x \/ go y ------ Free lattices---+toExpr :: Free a -> E.Expr a+toExpr (Var a)    = E.Var a+toExpr (x :/\: y) = toExpr x E.:/\: toExpr y+toExpr (x :\/: y) = toExpr x E.:\/: toExpr y -newtype FreeLattice a = FreeLattice-  { lowerFreeLattice :: forall b. Lattice b =>-                                    (a -> b) -> b-  }+-------------------------------------------------------------------------------+-- Monad+------------------------------------------------------------------------------- -instance Functor FreeLattice where-  fmap f (FreeLattice g) = FreeLattice (\inj -> g (inj . f))-  a <$ FreeLattice f = FreeLattice (\inj -> f (const (inj a)))+instance Applicative Free where+    pure = liftFree+    (<*>) = ap -liftFreeLattice :: a -> FreeLattice a-liftFreeLattice a = FreeLattice (\inj -> inj a)+instance Monad Free where+    return = pure+    (>>=)  = substFree -retractFreeLattice :: Lattice a => FreeLattice a -> a-retractFreeLattice a = lowerFreeLattice a id+-------------------------------------------------------------------------------+-- Instances+------------------------------------------------------------------------------- -instance JoinSemiLattice (FreeLattice a) where-  FreeLattice f \/ FreeLattice g = FreeLattice (\inj -> f inj \/ g inj)+instance Lattice (Free a) where+    x /\ y = x :/\: y+    x \/ y = x :\/: y -instance MeetSemiLattice (FreeLattice a) where-  FreeLattice f /\ FreeLattice g = FreeLattice (\inj -> f inj /\ g inj)+instance Ord a => Eq (Free a) where+    (==) = partialOrdEq -instance Lattice (FreeLattice a)+instance Ord a => PartialOrd (Free a) where+    leq x y = E.proofSearch (toExpr x E.:=>: toExpr y) -instance BoundedJoinSemiLattice a =>-         BoundedJoinSemiLattice (FreeLattice a) where-  bottom = FreeLattice (\inj -> inj bottom)+-------------------------------------------------------------------------------+-- Other instances+------------------------------------------------------------------------------- -instance BoundedMeetSemiLattice a =>-         BoundedMeetSemiLattice (FreeLattice a) where-  top = FreeLattice (\inj -> inj top)+instance QC.Arbitrary a => QC.Arbitrary (Free a) where+    arbitrary = QC.sized arb where+        arb n | n <= 0    = prim+              | otherwise = QC.oneof (prim : compound)+          where+            arb' = arb (intLog2 (max 1 n)) -instance BoundedLattice a =>-         BoundedLattice (FreeLattice a)+            compound =+                [ liftA2 (:/\:) arb' arb'+                , liftA2 (:\/:) arb' arb'+                ] -instance Universe a => Universe (FreeLattice a) where-  universe = fmap liftFreeLattice universe+        prim = Var <$> QC.arbitrary -instance Finite a => Finite (FreeLattice a) where-  universeF = fmap liftFreeLattice universeF+    shrink (Var c)    = map Var (QC.shrink c)+    shrink (x :/\: y) = x : y : map (uncurry (:/\:)) (QC.shrink (x, y))+    shrink (x :\/: y) = x : y : map (uncurry (:\/:)) (QC.shrink (x, y))

@@ -0,0 +1,106 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes      #-}+{-# LANGUAGE Safe            #-}++----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.Free+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------++module Algebra.Lattice.Free.Final (+   -- * Free Lattice+    FLattice,+    liftFLattice,+    lowerFLattice,+    retractFLattice,+   -- * Free BoundedLattice+    FBoundedLattice,+    liftFBoundedLattice,+    lowerFBoundedLattice,+    retractFBoundedLattice,+    ) where++import Prelude ()+import Prelude.Compat++import Algebra.Lattice++import Data.Universe.Class (Finite (..), Universe (..))++-------------------------------------------------------------------------------+-- Lattice+-------------------------------------------------------------------------------++newtype FLattice a = FLattice+  { lowerFLattice :: forall b. Lattice b =>+                                    (a -> b) -> b+  }++instance Functor FLattice where+  fmap f (FLattice g) = FLattice (\inj -> g (inj . f))+  a <$ FLattice f = FLattice (\inj -> f (const (inj a)))++liftFLattice :: a -> FLattice a+liftFLattice a = FLattice (\inj -> inj a)++retractFLattice :: Lattice a => FLattice a -> a+retractFLattice a = lowerFLattice a id++instance Lattice (FLattice a) where+  FLattice f \/ FLattice g = FLattice (\inj -> f inj \/ g inj)+  FLattice f /\ FLattice g = FLattice (\inj -> f inj /\ g inj)+++instance BoundedJoinSemiLattice a =>+         BoundedJoinSemiLattice (FLattice a) where+  bottom = FLattice (\inj -> inj bottom)++instance BoundedMeetSemiLattice a =>+         BoundedMeetSemiLattice (FLattice a) where+  top = FLattice (\inj -> inj top)++instance Universe a => Universe (FLattice a) where+  universe = fmap liftFLattice universe++instance Finite a => Finite (FLattice a) where+  universeF = fmap liftFLattice universeF++-------------------------------------------------------------------------------+-- BoundedLattice+-------------------------------------------------------------------------------++newtype FBoundedLattice a = FBoundedLattice+  { lowerFBoundedLattice :: forall b. BoundedLattice b =>+                                    (a -> b) -> b+  }++instance Functor FBoundedLattice where+  fmap f (FBoundedLattice g) = FBoundedLattice (\inj -> g (inj . f))+  a <$ FBoundedLattice f = FBoundedLattice (\inj -> f (const (inj a)))++liftFBoundedLattice :: a -> FBoundedLattice a+liftFBoundedLattice a = FBoundedLattice (\inj -> inj a)++retractFBoundedLattice :: BoundedLattice a => FBoundedLattice a -> a+retractFBoundedLattice a = lowerFBoundedLattice a id++instance Lattice (FBoundedLattice a) where+  FBoundedLattice f \/ FBoundedLattice g = FBoundedLattice (\inj -> f inj \/ g inj)+  FBoundedLattice f /\ FBoundedLattice g = FBoundedLattice (\inj -> f inj /\ g inj)+++instance BoundedJoinSemiLattice (FBoundedLattice a) where+  bottom = FBoundedLattice (\_ -> bottom)++instance BoundedMeetSemiLattice (FBoundedLattice a) where+  top = FBoundedLattice (\_ -> top)++instance Universe a => Universe (FBoundedLattice a) where+  universe = fmap liftFBoundedLattice universe++instance Finite a => Finite (FBoundedLattice a) where+  universeF = fmap liftFBoundedLattice universeF

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP                #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable     #-} {-# LANGUAGE DeriveFunctor      #-}@@ -6,15 +5,12 @@ {-# LANGUAGE DeriveTraversable  #-} {-# LANGUAGE FlexibleContexts   #-} {-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Safe               #-}-#endif ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Levitated--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -23,19 +19,25 @@ module Algebra.Lattice.Levitated (     Levitated(..)   , retractLevitated+  , foldLevitated   ) where  import Prelude () import Prelude.Compat  import Algebra.Lattice+import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq     (NFData (..))+import Control.Monad       (ap)+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import Data.Universe.Class (Finite (..), Universe (..))+import GHC.Generics        (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Levitated --@@ -43,13 +45,11 @@ -- | Graft a distinct top and bottom onto an otherwise unbounded lattice. -- The top is the absorbing element for the join, and the bottom is the absorbing -- element for the meet.-data Levitated a = Top+data Levitated a = Bottom                  | Levitate a-                 | Bottom+                 | Top   deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706            , Generic1-#endif            )  instance Applicative Levitated where@@ -69,32 +69,75 @@  instance Hashable a => Hashable (Levitated a) -instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where+instance PartialOrd a => PartialOrd (Levitated a) where+  leq _ Top = True+  leq Top _ = False+  leq Bottom _ = True+  leq _ Bottom = False+  leq (Levitate x) (Levitate y) = leq x y+  comparable Top _ = True+  comparable _ Top = True+  comparable Bottom _ = True+  comparable _ Bottom = True+  comparable (Levitate x) (Levitate y) = comparable x y++instance Lattice a => Lattice (Levitated a) where     Top        \/ _          = Top     _          \/ Top        = Top     Levitate x \/ Levitate y = Levitate (x \/ y)     Bottom     \/ lev_y      = lev_y     lev_x      \/ Bottom     = lev_x -instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where     Top        /\ lev_y      = lev_y     lev_x      /\ Top        = lev_x     Levitate x /\ Levitate y = Levitate (x /\ y)     Bottom     /\ _          = Bottom     _          /\ Bottom     = Bottom -instance Lattice a => Lattice (Levitated a) where--instance JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a) where+instance Lattice a => BoundedJoinSemiLattice (Levitated a) where     bottom = Bottom -instance MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a) where+instance Lattice a => BoundedMeetSemiLattice (Levitated a) where     top = Top -instance Lattice a => BoundedLattice (Levitated a) where- -- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@.-retractLevitated :: BoundedLattice a => Levitated a -> a-retractLevitated Top           = top-retractLevitated Bottom        = bottom-retractLevitated (Levitate x)  = x+retractLevitated :: (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) => Levitated a -> a+retractLevitated = foldLevitated bottom id top++-- | Fold 'Levitated'.+foldLevitated :: b -> (a -> b) -> b -> Levitated a -> b+foldLevitated b _ _ Bottom       = b+foldLevitated _ f _ (Levitate x) = f x+foldLevitated _ _ t Top          = t++instance Universe a => Universe (Levitated a) where+    universe = Top : Bottom : map Levitate universe+instance Finite a => Finite (Levitated a) where+    universeF = Top : Bottom : map Levitate universeF+    cardinality = fmap (2 +) (retag (cardinality :: Tagged a Natural))++instance QC.Arbitrary a => QC.Arbitrary (Levitated a) where+    arbitrary = QC.frequency+        [ (1, pure Top)+        , (1, pure Bottom)+        , (9, Levitate <$> QC.arbitrary)+        ]++    shrink Top          = []+    shrink Bottom       = []+    shrink (Levitate x) = Top : Bottom : map Levitate (QC.shrink x)++instance QC.CoArbitrary a => QC.CoArbitrary (Levitated a) where+    coarbitrary Top          = QC.variant (0 :: Int)+    coarbitrary Bottom       = QC.variant (0 :: Int)+    coarbitrary (Levitate x) = QC.variant (0 :: Int) . QC.coarbitrary x++instance QC.Function a => QC.Function (Levitated a) where+    function = QC.functionMap fromLevitated toLevitated where+        fromLevitated Top          = Left True+        fromLevitated Bottom       = Left False+        fromLevitated (Levitate x) = Right x++        toLevitated (Left True)  = Top+        toLevitated (Left False) = Bottom+        toLevitated (Right x)    = Levitate x

@@ -1,20 +1,16 @@-{-# LANGUAGE CPP                #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveFoldable     #-} {-# LANGUAGE DeriveFunctor      #-} {-# LANGUAGE DeriveGeneric      #-} {-# LANGUAGE DeriveTraversable  #-} {-# LANGUAGE FlexibleContexts   #-}-{-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else {-# LANGUAGE Safe               #-}-#endif+{-# LANGUAGE TypeOperators      #-} ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Lexicographic--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -30,12 +26,16 @@ import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq     (NFData (..))+import Control.Monad       (ap, liftM2)+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import GHC.Generics        (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Lexicographic --@@ -49,15 +49,13 @@ -- -- An application of this type is versioning.  For example, a -- Last-Writer-Wins register would look like--- 'Lexicographc (Ordered Timestamp) v' where the lattice+-- @'Lexicographic' ('Algebra.Lattice.Ordered.Ordered' Timestamp) v@ where the lattice -- structure handles the, presumably rare, case of matching--- 'Timestamps'.  Typically this is done in an arbitary, but+-- @Timestamp@s.  Typically this is done in an arbitary, but -- deterministic manner. data Lexicographic k v = Lexicographic !k !v   deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706            , Generic1-#endif            )  instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where@@ -95,30 +93,25 @@ -- (3, 2) `leq` (6, 1) -- @ ---instance (PartialOrd k, JoinSemiLattice k, BoundedJoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where+instance (PartialOrd k, Lattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => Lattice (Lexicographic k v) where   l@(Lexicographic k1 v1) \/ r@(Lexicographic k2 v2)     | k1 == k2 = Lexicographic k1 (v1 \/ v2)     | k1 `leq` k2 = r     | k2 `leq` k1 = l     | otherwise   = Lexicographic (k1 \/ k2) bottom -instance (PartialOrd k, MeetSemiLattice k, BoundedMeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where   l@(Lexicographic k1 v1) /\ r@(Lexicographic k2 v2)     | k1 == k2 = Lexicographic k1 (v1 /\ v2)     | k1 `leq` k2 = l     | k2 `leq` k1 = r     | otherwise   = Lexicographic (k1 /\ k2) top -instance (PartialOrd k, Lattice k, BoundedLattice v) => Lattice (Lexicographic k v) where--instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where+instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where   bottom = Lexicographic bottom bottom -instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where+instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where   top = Lexicographic top top -instance (PartialOrd k, BoundedLattice k, BoundedLattice v) => BoundedLattice (Lexicographic k v) where- instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where   Lexicographic k1 v1 `leq` Lexicographic k2 v2     | k1   ==  k2 = v1 `leq` v2@@ -127,3 +120,21 @@   comparable (Lexicographic k1 v1) (Lexicographic k2 v2)     | k1 == k2 = comparable v1 v2     | otherwise = comparable k1 k2++instance (Universe k, Universe v) => Universe (Lexicographic k v) where+    universe = map (uncurry Lexicographic) universe+instance (Finite k, Finite v) => Finite (Lexicographic k v) where+    universeF = map (uncurry Lexicographic) universeF+    cardinality = liftM2 (*)+        (retag (cardinality :: Tagged k Natural))+        (retag (cardinality :: Tagged v Natural))++instance (QC.Arbitrary k, QC.Arbitrary v) => QC.Arbitrary (Lexicographic k v) where+    arbitrary = uncurry Lexicographic <$> QC.arbitrary+    shrink (Lexicographic k v) = uncurry Lexicographic <$> QC.shrink (k, v)++instance (QC.CoArbitrary k, QC.CoArbitrary v) => QC.CoArbitrary (Lexicographic k v) where+    coarbitrary (Lexicographic k v) = QC.coarbitrary (k, v)++instance (QC.Function k, QC.Function v) => QC.Function (Lexicographic k v) where+    function = QC.functionMap (\(Lexicographic k v) -> (k,v)) (uncurry Lexicographic)

@@ -1,20 +1,16 @@-{-# LANGUAGE CPP                #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable     #-} {-# LANGUAGE DeriveFunctor      #-} {-# LANGUAGE DeriveGeneric      #-} {-# LANGUAGE DeriveTraversable  #-} {-# LANGUAGE FlexibleContexts   #-}-{-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else {-# LANGUAGE Safe               #-}-#endif+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators      #-} ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Lifted--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -23,31 +19,35 @@ module Algebra.Lattice.Lifted (     Lifted(..)   , retractLifted+  , foldLifted   ) where  import Prelude () import Prelude.Compat  import Algebra.Lattice+import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq     (NFData (..))+import Control.Monad       (ap)+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import GHC.Generics        (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Lifted --  -- | Graft a distinct bottom onto an otherwise unbounded lattice. -- As a bonus, the bottom will be an absorbing element for the meet.-data Lifted a = Lift a-              | Bottom+data Lifted a = Bottom+              | Lift a   deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706            , Generic1-#endif            )  instance Applicative Lifted where@@ -65,27 +65,57 @@  instance Hashable a => Hashable (Lifted a) -instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where+instance PartialOrd a => PartialOrd (Lifted a) where+  leq Bottom _ = True+  leq _ Bottom = False+  leq (Lift x) (Lift y) = leq x y+  comparable Bottom _ = True+  comparable _ Bottom = True+  comparable (Lift x) (Lift y) = comparable x y++instance Lattice a => Lattice (Lifted a) where     Lift x \/ Lift y = Lift (x \/ y)     Bottom \/ lift_y = lift_y     lift_x \/ Bottom = lift_x -instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where     Lift x /\ Lift y = Lift (x /\ y)     Bottom /\ _      = Bottom     _      /\ Bottom = Bottom -instance Lattice a => Lattice (Lifted a) where--instance JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a) where+instance Lattice a => BoundedJoinSemiLattice (Lifted a) where     bottom = Bottom  instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where     top = Lift top -instance BoundedLattice a => BoundedLattice (Lifted a) where- -- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@. retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a-retractLifted Bottom    = bottom-retractLifted (Lift x)  = x+retractLifted = foldLifted bottom id++-- | Similar to @'maybe'@, but for @'Lifted'@ type.+foldLifted :: b -> (a -> b) -> Lifted a -> b+foldLifted _ f (Lift x) = f x+foldLifted y _ Bottom   = y++instance Universe a => Universe (Lifted a) where+    universe = Bottom : map Lift universe+instance Finite a => Finite (Lifted a) where+    universeF = Bottom : map Lift universeF+    cardinality = fmap succ (retag (cardinality :: Tagged a Natural))++instance QC.Arbitrary a => QC.Arbitrary (Lifted a) where+    arbitrary = QC.frequency+        [ (1, pure Bottom)+        , (9, Lift <$> QC.arbitrary)+        ]+    shrink Bottom   = []+    shrink (Lift x) = Bottom : map Lift (QC.shrink x)++instance QC.CoArbitrary a => QC.CoArbitrary (Lifted a) where+    coarbitrary Bottom      = QC.variant (0 :: Int)+    coarbitrary (Lift x) = QC.variant (1 :: Int) . QC.coarbitrary x++instance QC.Function a => QC.Function (Lifted a) where+    function = QC.functionMap fromLifted toLifted where+        fromLifted = foldLifted Nothing Just+        toLifted   = maybe Bottom Lift

@@ -0,0 +1,124 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE Safe               #-}+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.M2+-- Copyright   :  (C) 2019 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Lattice.M2 (+    M2 (..),+    toSetBool,+    fromSetBool,+    ) where++import Prelude ()+import Prelude.Compat++import Control.DeepSeq     (NFData (..))+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import GHC.Generics        (Generic)++import qualified Test.QuickCheck as QC++import Algebra.Heyting+import Algebra.Lattice+import Algebra.PartialOrd++import           Data.Set (Set)+import qualified Data.Set as Set++-- | \(M_2\) is isomorphic to \(\mathcal{P}\{\mathbb{B}\}\), i.e. powerset of 'Bool'.+--+-- <<m2.png>>+--+data M2 = M2o | M2a | M2b | M2i+  deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic)++instance PartialOrd M2 where+    M2o `leq` _   = True+    _   `leq` M2i = True+    M2a `leq` M2a = True+    M2b `leq` M2b = True+    _   `leq` _   = False++instance Lattice M2 where+    M2o \/ y   = y+    M2i \/ _   = M2i+    x   \/ M2o = x+    _   \/ M2i = M2i+    M2a \/ M2a = M2a+    M2b \/ M2b = M2b+    _   \/ _   = M2i++    M2o /\ _   = M2o+    M2i /\ y   = y+    _   /\ M2o = M2o+    x   /\ M2i = x+    M2a /\ M2a = M2a+    M2b /\ M2b = M2b+    _   /\ _   = M2o++instance BoundedJoinSemiLattice M2 where+    bottom = M2o++instance BoundedMeetSemiLattice M2 where+    top = M2i++instance Heyting M2 where+    M2o ==> _   = M2i+    M2i ==> x   = x++    M2a ==> M2o = M2b+    M2a ==> M2a = M2i+    M2a ==> M2b = M2b+    M2a ==> M2i = M2i++    M2b ==> M2o = M2a+    M2b ==> M2a = M2a+    M2b ==> M2b = M2i+    M2b ==> M2i = M2i++    neg M2o = M2i+    neg M2a = M2b+    neg M2b = M2a+    neg M2i = M2o++toSetBool :: M2 -> Set Bool+toSetBool M2o = mempty+toSetBool M2a = Set.singleton False+toSetBool M2b = Set.singleton True+toSetBool M2i = Set.fromList [True, False]++fromSetBool :: Set Bool -> M2+fromSetBool x = case Set.toList x of+    [False,True] -> M2i+    [False]      -> M2a+    [True]       -> M2b+    _            -> M2o++instance QC.Arbitrary M2 where+    arbitrary = QC.arbitraryBoundedEnum+    shrink x | x == minBound = []+             | otherwise     = [minBound .. pred x]++instance QC.CoArbitrary M2 where+    coarbitrary = QC.coarbitraryEnum++instance QC.Function M2 where+    function = QC.functionBoundedEnum++instance Universe M2 where universe = [minBound .. maxBound]+instance Finite M2 where cardinality = 4++instance NFData M2 where+    rnf x = x `seq` ()++instance Hashable M2 where+    hashWithSalt salt = hashWithSalt salt . fromEnum

@@ -0,0 +1,89 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE Safe               #-}+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.M3+-- Copyright   :  (C) 2019 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Lattice.M3 (+    M3 (..),+    ) where++import Prelude ()+import Prelude.Compat++import Control.DeepSeq     (NFData (..))+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import GHC.Generics        (Generic)++import qualified Test.QuickCheck as QC++import Algebra.Lattice+import Algebra.PartialOrd++-- | \(M_3\), is smallest non-distributive, yet modular lattice.+--+-- <<m3.png>>+--+data M3 = M3o | M3a | M3b | M3c | M3i+  deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic)++instance PartialOrd M3 where+    M3o `leq` _   = True+    _   `leq` M3i = True+    M3a `leq` M3a = True+    M3b `leq` M3b = True+    M3c `leq` M3c = True+    _   `leq` _   = False++instance Lattice M3 where+    M3o \/ y   = y+    M3i \/ _   = M3i+    x   \/ M3o = x+    _   \/ M3i = M3i+    M3a \/ M3a = M3a+    M3b \/ M3b = M3b+    M3c \/ M3c = M3c+    _   \/ _   = M3i++    M3o /\ _   = M3o+    M3i /\ y   = y+    _   /\ M3o = M3o+    x   /\ M3i = x+    M3a /\ M3a = M3a+    M3b /\ M3b = M3b+    M3c /\ M3c = M3c+    _   /\ _   = M3o++instance BoundedJoinSemiLattice M3 where+    bottom = M3o++instance BoundedMeetSemiLattice M3 where+    top = M3i++instance QC.Arbitrary M3 where+    arbitrary = QC.arbitraryBoundedEnum+    shrink x | x == minBound = []+             | otherwise     = [minBound .. pred x]++instance QC.CoArbitrary M3 where+    coarbitrary = QC.coarbitraryEnum++instance QC.Function M3 where+    function = QC.functionBoundedEnum++instance Universe M3 where universe = [minBound .. maxBound]+instance Finite M3 where cardinality = 5++instance NFData M3 where+    rnf x = x `seq` ()++instance Hashable M3 where+    hashWithSalt salt = hashWithSalt salt . fromEnum

@@ -0,0 +1,94 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE Safe               #-}+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.N5+-- Copyright   :  (C) 2019 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Lattice.N5 (+    N5 (..),+    ) where++import Prelude ()+import Prelude.Compat++import Control.DeepSeq     (NFData (..))+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import GHC.Generics        (Generic)++import qualified Test.QuickCheck as QC++import Algebra.Lattice+import Algebra.PartialOrd++-- | \(N_5\), is smallest non-modular (and non-distributive) lattice.+--+-- <<n5.png>>+--+data N5 = N5o | N5a | N5b | N5c | N5i+  deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic)++instance PartialOrd N5 where+    N5o `leq` _   = True+    _   `leq` N5i = True+    N5a `leq` N5a = True+    N5b `leq` N5a = True+    N5b `leq` N5b = True+    N5c `leq` N5c = True+    _   `leq` _   = False++instance Lattice N5 where+    N5o \/ y   = y+    N5i \/ _   = N5i+    x   \/ N5o = x+    _   \/ N5i = N5i+    N5a \/ N5a = N5a+    N5a \/ N5b = N5a+    N5b \/ N5a = N5a+    N5b \/ N5b = N5b+    N5c \/ N5c = N5c+    _   \/ _   = N5i++    N5o /\ _   = N5o+    N5i /\ y   = y+    _   /\ N5o = N5o+    x   /\ N5i = x+    N5a /\ N5a = N5a+    N5b /\ N5b = N5b+    N5a /\ N5b = N5b+    N5b /\ N5a = N5b+    N5c /\ N5c = N5c+    _   /\ _   = N5o++instance BoundedJoinSemiLattice N5 where+    bottom = N5o++instance BoundedMeetSemiLattice N5 where+    top = N5i++instance QC.Arbitrary N5 where+    arbitrary = QC.arbitraryBoundedEnum+    shrink x | x == minBound = []+             | otherwise     = [minBound .. pred x]++instance QC.CoArbitrary N5 where+    coarbitrary = QC.coarbitraryEnum++instance QC.Function N5 where+    function = QC.functionBoundedEnum++instance Universe N5 where universe = [minBound .. maxBound]+instance Finite N5 where cardinality = 5++instance NFData N5 where+    rnf x = x `seq` ()++instance Hashable N5 where+    hashWithSalt salt = hashWithSalt salt . fromEnum

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP                #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable     #-} {-# LANGUAGE DeriveFunctor      #-}@@ -6,15 +5,11 @@ {-# LANGUAGE DeriveTraversable  #-} {-# LANGUAGE FlexibleContexts   #-} {-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else {-# LANGUAGE Safe               #-}-#endif ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Op--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -30,12 +25,15 @@ import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq     (NFData (..))+import Control.Monad       (ap)+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import GHC.Generics        (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Op --@@ -43,12 +41,13 @@ -- | The opposite lattice of a given lattice.  That is, switch -- meets and joins. newtype Op a = Op { getOp :: a }-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706+  deriving ( Eq, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable            , Generic1-#endif            ) +instance Ord a => Ord (Op a) where+  compare (Op a) (Op b) = compare b a+ instance Applicative Op where   pure = return   (<*>) = ap@@ -62,22 +61,31 @@  instance Hashable a => Hashable (Op a) -instance MeetSemiLattice a => JoinSemiLattice (Op a) where+instance Lattice a => Lattice (Op a) where   Op x \/ Op y = Op (x /\ y)--instance JoinSemiLattice a => MeetSemiLattice (Op a) where   Op x /\ Op y = Op (x \/ y) -instance Lattice a => Lattice (Op a) where- instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where   bottom = Op top  instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where   top = Op bottom -instance BoundedLattice a => BoundedLattice (Op a) where- instance PartialOrd a => PartialOrd (Op a) where     Op a `leq` Op b = b `leq` a -- Note swap.     comparable (Op a) (Op b) = comparable a b++instance Universe a => Universe (Op a) where+    universe = map Op universe+instance Finite a => Finite (Op a) where+    universeF = map Op universeF++instance QC.Arbitrary a => QC.Arbitrary (Op a) where+    arbitrary = Op <$> QC.arbitrary+    shrink    = QC.shrinkMap getOp Op++instance QC.CoArbitrary a => QC.CoArbitrary (Op a) where+    coarbitrary = QC.coarbitrary . getOp++instance QC.Function a => QC.Function (Op a) where+    function = QC.functionMap getOp Op

@@ -1,20 +1,16 @@-{-# LANGUAGE CPP                #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveFoldable     #-}-{-# LANGUAGE DeriveFunctor      #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE DeriveTraversable  #-}-{-# LANGUAGE FlexibleContexts   #-}-{-# LANGUAGE TypeOperators      #-}-#if __GLASGOW_HASKELL__ < 709-{-# LANGUAGE Trustworthy        #-}-#else-{-# LANGUAGE Safe               #-}-#endif+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-} ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.Lattice.Ordered--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -27,26 +23,29 @@ import Prelude () import Prelude.Compat +import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq-import Control.Monad-import Data.Data-import Data.Hashable-import GHC.Generics+import Control.DeepSeq       (NFData (..))+import Control.Monad         (ap)+import Data.Data             (Data, Typeable)+import Data.Hashable         (Hashable (..))+import Data.Universe.Class   (Finite (..), Universe (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import GHC.Generics          (Generic, Generic1) +import qualified Test.QuickCheck as QC+ -- -- Ordered --  -- | A total order gives rise to a lattice. Join is--- max, meet is min.+-- 'max', meet is 'min'. newtype Ordered a = Ordered { getOrdered :: a }   deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable-#if __GLASGOW_HASKELL__ >= 706            , Generic1-#endif            )  instance Applicative Ordered where@@ -62,22 +61,40 @@  instance Hashable a => Hashable (Ordered a) -instance Ord a => JoinSemiLattice (Ordered a) where+instance Ord a => Lattice (Ordered a) where   Ordered x \/ Ordered y = Ordered (max x y)--instance Ord a => MeetSemiLattice (Ordered a) where   Ordered x /\ Ordered y = Ordered (min x y) -instance Ord a => Lattice (Ordered a) where- instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where   bottom = Ordered minBound  instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where   top = Ordered maxBound -instance (Ord a, Bounded a) => BoundedLattice (Ordered a) where+-- | This is interesting logic, as it satisfies both de Morgan laws;+-- but isn't Boolean: i.e. law of exluded middle doesn't hold.+--+-- Negation "smashes" value into 'minBound' or 'maxBound'.+instance (Ord a, Bounded a) => Heyting (Ordered a) where+    x ==> y | x > y     = y+            | otherwise = top  instance Ord a => PartialOrd (Ordered a) where     leq = (<=)     comparable _ _ = True++instance Universe a => Universe (Ordered a) where+    universe = map Ordered universe+instance Finite a => Finite (Ordered a) where+    universeF = map Ordered universeF+    cardinality = retag (cardinality :: Tagged a Natural)++instance QC.Arbitrary a => QC.Arbitrary (Ordered a) where+    arbitrary = Ordered <$> QC.arbitrary+    shrink    = QC.shrinkMap Ordered getOrdered++instance QC.CoArbitrary a => QC.CoArbitrary (Ordered a) where+    coarbitrary = QC.coarbitrary . getOrdered++instance QC.Function a => QC.Function (Ordered a) where+    function = QC.functionMap getOrdered Ordered

@@ -0,0 +1,29 @@+-- | This module provides Unicode variants of the operators.+--+-- Unfortunately, ⊤, ⊥, and ¬ don't fit into Haskell lexical structure well.+--+module Algebra.Lattice.Unicode where++import Algebra.Heyting+import Algebra.Lattice++infixr 6 ∧+infixr 5 ∨+infixr 4 ⟹+infix 4 ⟺++-- | Meet, alias for '/\'.+(∧) :: Lattice a => a -> a -> a+(∧) = (/\)++-- | Join, alias for '\/'.+(∨) :: Lattice a => a -> a -> a+(∨) = (\/)++-- | Implication, alias for '==>'.+(⟹) :: Heyting a => a -> a -> a+(⟹) = (==>)++-- | Equivalence, alias for '<=>'.+(⟺) :: Heyting a => a -> a -> a+(⟺) = (<=>)

@@ -0,0 +1,138 @@+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.Wide+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Lattice.Wide (+    Wide(..)+  ) where++import Prelude ()+import Prelude.Compat++import Algebra.Lattice+import Algebra.PartialOrd++import Control.DeepSeq       (NFData (..))+import Control.Monad         (ap)+import Data.Data             (Data, Typeable)+import Data.Hashable         (Hashable (..))+import Data.Universe.Class   (Finite (..), Universe (..))+import Data.Universe.Helpers (Natural, Tagged, retag)+import GHC.Generics          (Generic, Generic1)++import qualified Test.QuickCheck as QC++--+-- Wide+--++-- | Graft a distinct top and bottom onto any type.+-- The 'Top' is identity for '/\' and the absorbing element for '\/'.+-- The 'Bottom' is the identity for '\/' and and the absorbing element for '/\'.+-- Two 'Middle' values join to top, unless they are equal.+--+-- <<wide.png>>+--+data Wide a+    = Top+    | Middle a+    | Bottom+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable+           , Generic1+           )++instance Applicative Wide where+  pure = return+  (<*>) = ap++instance Monad Wide where+  return       = Middle+  Top >>= _    = Top+  Bottom >>= _ = Bottom+  Middle x >>= f = f x++instance NFData a => NFData (Wide a) where+  rnf Top      = ()+  rnf Bottom   = ()+  rnf (Middle a) = rnf a++instance Hashable a => Hashable (Wide a)++instance Eq a => Lattice (Wide a) where+  Top      \/ _        = Top+  Bottom   \/ x        = x+  Middle _ \/ Top      = Top+  Middle x \/ Bottom   = Middle x+  Middle x \/ Middle y = if x == y then Middle x else Top++  Bottom   /\ _        = Bottom+  Top      /\ x        = x+  Middle _ /\ Bottom   = Bottom+  Middle x /\ Top      = Middle x+  Middle x /\ Middle y = if x == y then Middle x else Bottom++instance Eq a => BoundedJoinSemiLattice (Wide a) where+  bottom = Bottom++instance Eq a => BoundedMeetSemiLattice (Wide a) where+  top = Top++instance Eq a => PartialOrd (Wide a) where+  leq Bottom _              = True+  leq Top Bottom            = False+  leq Top (Middle _)        = False+  leq Top Top               = True+  leq (Middle _) Bottom     = False+  leq (Middle _) Top        = True+  leq (Middle x) (Middle y) = x == y++  comparable Bottom _              = True+  comparable Top _                 = True+  comparable (Middle _) Bottom     = True+  comparable (Middle _) Top        = True+  comparable (Middle x) (Middle y) = x == y++instance Universe a => Universe (Wide a) where+    universe = Top : Bottom : map Middle universe+instance Finite a => Finite (Wide a) where+    universeF = Top : Bottom : map Middle universeF+    cardinality = fmap (2 +) (retag (cardinality :: Tagged a Natural))++instance QC.Arbitrary a => QC.Arbitrary (Wide a) where+    arbitrary = QC.frequency+        [ (1, pure Top)+        , (1, pure Bottom)+        , (9, Middle <$> QC.arbitrary)+        ]++    shrink Top        = []+    shrink Bottom     = []+    shrink (Middle x) = Top : Bottom : map Middle (QC.shrink x)++instance QC.CoArbitrary a => QC.CoArbitrary (Wide a) where+    coarbitrary Top        = QC.variant (0 :: Int)+    coarbitrary Bottom     = QC.variant (0 :: Int)+    coarbitrary (Middle x) = QC.variant (0 :: Int) . QC.coarbitrary x++instance QC.Function a => QC.Function (Wide a) where+    function = QC.functionMap fromWide toWide where+        fromWide Top        = Left True+        fromWide Bottom     = Left False+        fromWide (Middle x) = Right x++        toWide (Left True)  = Top+        toWide (Left False) = Bottom+        toWide (Right x)    = Middle x

@@ -0,0 +1,80 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE Safe               #-}+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.ZeroHalfOne+-- Copyright   :  (C) 2019 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Lattice.ZeroHalfOne (+    ZeroHalfOne (..),+    ) where++import Prelude ()+import Prelude.Compat++import Control.DeepSeq     (NFData (..))+import Data.Data           (Data, Typeable)+import Data.Hashable       (Hashable (..))+import Data.Universe.Class (Finite (..), Universe (..))+import GHC.Generics        (Generic)++import qualified Test.QuickCheck as QC++import Algebra.Heyting+import Algebra.Lattice+import Algebra.PartialOrd++-- | The simplest Heyting algebra that is not already a Boolean algebra is the+-- totally ordered set \(\{ 0, \frac{1}{2}, 1 \}\).+--+data ZeroHalfOne = Zero | Half | One+  deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic)++instance PartialOrd ZeroHalfOne where+    leq = (<=)++instance Lattice ZeroHalfOne where+    (\/) = max+    (/\) = min++instance BoundedJoinSemiLattice ZeroHalfOne where+    bottom = Zero++instance BoundedMeetSemiLattice ZeroHalfOne where+    top = One++-- | Not boolean: @'neg' 'Half' '\/' 'Half' = 'Half' /= 'One'@+instance Heyting ZeroHalfOne where+    Zero ==> _    = One+    One  ==> x    = x+    Half ==> Zero = Zero+    Half ==> _    = One++    neg Zero = One+    neg One  = Zero+    neg Half = Zero++instance QC.Arbitrary ZeroHalfOne where+    arbitrary = QC.arbitraryBoundedEnum+    shrink x | x == minBound = []+             | otherwise     = [minBound .. pred x]++instance QC.CoArbitrary ZeroHalfOne where+    coarbitrary = QC.coarbitraryEnum++instance QC.Function ZeroHalfOne where+    function = QC.functionBoundedEnum++instance Universe ZeroHalfOne where universe = [minBound .. maxBound]+instance Finite ZeroHalfOne where cardinality = 3++instance NFData ZeroHalfOne where+    rnf x = x `seq` ()++instance Hashable ZeroHalfOne where+    hashWithSalt salt = hashWithSalt salt . fromEnum

@@ -2,7 +2,7 @@ ---------------------------------------------------------------------------- -- | -- Module      :  Algebra.PartialOrd--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License     :  BSD-3-Clause (see the file LICENSE) -- -- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>@@ -24,9 +24,9 @@ import qualified Data.HashSet      as HS import qualified Data.IntMap       as IM import qualified Data.IntSet       as IS-import qualified Data.List         as L+import qualified Data.List.Compat  as L import qualified Data.Map          as M-import           Data.Monoid       (All (..))+import           Data.Monoid       (All (..), Any (..)) import qualified Data.Set          as S import           Data.Void         (Void) @@ -88,14 +88,17 @@     -- | Whether two elements are ordered with respect to the relation. A     -- default implementation is given by     ---    -- > comparable x y = leq x y || leq y x+    -- @+    -- 'comparable' x y = 'leq' x y '||' 'leq' y x+    -- @     comparable :: a -> a -> Bool     comparable x y = leq x y || leq y x --- | The equality relation induced by the partial-order structure. It must obey--- the laws+-- | The equality relation induced by the partial-order structure. It satisfies+-- the laws of an equivalence relation: -- @ -- Reflexive:  a == a+-- Symmetric:  a == b ==> b == a -- Transitive: a == b && b == c ==> a == c -- @ partialOrdEq :: PartialOrd a => a -> a -> Bool@@ -104,12 +107,22 @@ instance PartialOrd () where     leq _ _ = True +-- | @since 2+instance PartialOrd Bool where+    leq = (<=)++instance PartialOrd Any where+    leq = (<=)++instance PartialOrd All where+    leq = (<=)+ instance PartialOrd Void where     leq _ _ = True --- | @'leq' = 'Data.List.isInfixOf'@.+-- | @'leq' = 'Data.List.isSequenceOf'@. instance Eq a => PartialOrd [a] where-    leq = L.isInfixOf+    leq = L.isSubsequenceOf  instance Ord a => PartialOrd (S.Set a) where     leq = S.isSubsetOf

@@ -14,9 +14,15 @@ module Algebra.PartialOrd.Instances () where  import Algebra.PartialOrd         (PartialOrd (..))+import Data.Monoid                (Endo (..)) import Data.Universe.Class        (Finite (..)) import Data.Universe.Instances.Eq ()  -- | @Eq (k -> v)@ is from 'Data.Universe.Instances.Eq' instance (PartialOrd v, Finite k) => PartialOrd (k -> v) where     f `leq` g = all (\k -> f k `leq` g k) universeF++instance (PartialOrd v, Finite v) => PartialOrd (Endo v) where+    Endo f `leq` Endo g = f `leq` g++

@@ -1,39 +1,62 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE CPP                 #-}+{-# LANGUAGE ConstraintKinds     #-}+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE KindSignatures      #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE KindSignatures #-}-{-# OPTIONS_GHC -fno-warn-orphans #-} module Main (main) where  import Prelude () import Prelude.Compat -import Data.Maybe (listToMaybe, isJust)-import Data.Semigroup ((<>))-import Control.Monad (ap, guard)+import Control.Monad            (ap, guard)+import Data.Int                 (Int8)+import Data.List                (genericLength, nub)+import Data.Maybe               (isJust, listToMaybe)+import Data.Semigroup           (All, Any, Endo (..), (<>))+import Data.Typeable            (Typeable, typeOf)+import Data.Universe.Class      (Finite (..), Universe (..))+import Data.Universe.Helpers    (Natural, Tagged (..))+import Test.QuickCheck+       (Arbitrary (..), Property, discard, label, (=/=), (===)) import Test.QuickCheck.Function import Test.Tasty-import Test.Tasty.QuickCheck as QC+import Test.Tasty.QuickCheck    (testProperty) +import qualified Test.QuickCheck as QC++import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd -import qualified Algebra.Lattice.Divisibility as Div-import qualified Algebra.Lattice.Dropped as D-import qualified Algebra.Lattice.Levitated as L+import Algebra.Lattice.M2          (M2 (..))+import Algebra.Lattice.M3          (M3 (..))+import Algebra.Lattice.N5          (N5 (..))+import Algebra.Lattice.ZeroHalfOne (ZeroHalfOne (..))++import qualified Algebra.Heyting.Free          as HF+import qualified Algebra.Lattice.Divisibility  as Div+import qualified Algebra.Lattice.Dropped       as D+import qualified Algebra.Lattice.Free          as F+import qualified Algebra.Lattice.Levitated     as L import qualified Algebra.Lattice.Lexicographic as LO-import qualified Algebra.Lattice.Lifted as U-import qualified Algebra.Lattice.Op as Op-import qualified Algebra.Lattice.Ordered as O+import qualified Algebra.Lattice.Lifted        as U+import qualified Algebra.Lattice.Op            as Op+import qualified Algebra.Lattice.Ordered       as O+import qualified Algebra.Lattice.Wide          as W -import Data.IntMap (IntMap)-import Data.IntSet (IntSet)-import Data.Map (Map)-import Data.Set (Set) import Data.HashMap.Lazy (HashMap)-import Data.HashSet (HashSet)+import Data.HashSet      (HashSet)+import Data.IntMap       (IntMap)+import Data.IntSet       (IntSet)+import Data.Map          (Map)+import Data.Set          (Set) -import Data.Universe.Instances.Base ()+import Algebra.PartialOrd.Instances ()+import Data.Universe.Instances.Eq ()+import Data.Universe.Instances.Ord ()+import Data.Universe.Instances.Show () import Test.QuickCheck.Instances ()  -- For old GHC to work@@ -45,29 +68,79 @@  tests :: TestTree tests = testGroup "Tests"-  [ latticeLaws "M3" False (Proxy :: Proxy M3) -- non distributive lattice!-  , latticeLaws "M2" True (Proxy :: Proxy M2) -- M2-  , latticeLaws "Map" True (Proxy :: Proxy (Map Int (O.Ordered Int)))-  , latticeLaws "IntMap" True (Proxy :: Proxy (IntMap (O.Ordered Int)))-  , latticeLaws "HashMap" True (Proxy :: Proxy (HashMap Int (O.Ordered Int)))-  , latticeLaws "Set" True (Proxy :: Proxy (Set Int))-  , latticeLaws "IntSet" True (Proxy :: Proxy IntSet)-  , latticeLaws "HashSet" True (Proxy :: Proxy (HashSet Int))-  , latticeLaws "Ordered" True (Proxy :: Proxy (O.Ordered Int))-  , latticeLaws "Divisibility" True (Proxy :: Proxy (Div.Divisibility Int))-  , latticeLaws "LexOrdered" True (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int)))-  , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic (Set Bool) (Set Bool)))-  , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic M2 M2)) -- non distributive!-  , testProperty "Lexicographic M2 M2 contains M3" $ QC.property $-      isJust searchM3LexM2-  , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)-  , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)-  , monadLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))-  , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)-  , monadLaws "Op" (Proxy1 :: Proxy1 Op.Op)-  , monadLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)-  ]+    [ allLatticeLaws (LBounded Partial Modular)          (Proxy :: Proxy M3) -- non distributive lattice!+    , allLatticeLaws (LHeyting Partial IsBoolean)        (Proxy :: Proxy M2) -- M2+    , allLatticeLaws (LHeyting Partial IsBoolean)        (Proxy :: Proxy (Set Bool)) -- isomorphic to M2+    , allLatticeLaws (LBounded Partial NonModular)       (Proxy :: Proxy N5)+    , allLatticeLaws (LHeyting Total IsBoolean)          (Proxy :: Proxy ())+    , allLatticeLaws (LHeyting Total IsBoolean)          (Proxy :: Proxy Bool)+    , allLatticeLaws (LHeyting Total DeMorgan)           (Proxy :: Proxy ZeroHalfOne)+    , allLatticeLaws (LNormal Partial Distributive)      (Proxy :: Proxy (Map Int (O.Ordered Int)))+    , allLatticeLaws (LNormal Partial Distributive)      (Proxy :: Proxy (IntMap (O.Ordered Int)))+    , allLatticeLaws (LNormal Partial Distributive)      (Proxy :: Proxy (HashMap Int (O.Ordered Int)))+    , allLatticeLaws (LHeyting     Partial IsBoolean)    (Proxy :: Proxy (Set Int8))+    , allLatticeLaws (LHeyting     Partial IsBoolean)    (Proxy :: Proxy (HashSet Int8))+    , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy (Set Int))+    , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy IntSet)+    , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy (HashSet Int))+    , allLatticeLaws (LHeyting Total DeMorgan)           (Proxy :: Proxy (O.Ordered Int8))+    , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy (Div.Divisibility Int))+    , allLatticeLaws (LNormal Total Distributive)        (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int)))+    , allLatticeLaws (LBounded Partial Modular)          (Proxy :: Proxy (W.Wide Int))+    , allLatticeLaws (LBounded Partial NonModular)       (Proxy :: Proxy (LO.Lexicographic (Set Bool) (Set Bool)))+    , allLatticeLaws (LBounded Partial NonModular)       (Proxy :: Proxy (LO.Lexicographic M2 M2)) -- non distributive! +    , allLatticeLaws LNotLattice                         (Proxy :: Proxy String)++    , allLatticeLaws (LHeyting Total   IsBoolean)        (Proxy :: Proxy All)+    , allLatticeLaws (LHeyting Total   IsBoolean)        (Proxy :: Proxy Any)+    , allLatticeLaws (LHeyting Partial IsBoolean)        (Proxy :: Proxy (Endo Bool)) -- note: it's partial!+    , allLatticeLaws (LBounded Partial Modular)          (Proxy :: Proxy (Endo M3))++    , allLatticeLaws (LHeyting Partial IsBoolean)        (Proxy :: Proxy (Int8 -> Bool))+    , allLatticeLaws (LHeyting Partial IsBoolean)        (Proxy :: Proxy (Int8 -> M2))+    , allLatticeLaws (LBounded Partial Modular)          (Proxy :: Proxy (Int8 -> M3))++    , allLatticeLaws (LNormal  Partial Distributive)     (Proxy :: Proxy (F.Free Int8))+    , allLatticeLaws (LHeyting Partial NonBoolean)       (Proxy :: Proxy (HF.Free Var))++    , allLatticeLaws (LBoundedMeet Total Distributive)   (Proxy :: Proxy (D.Dropped (O.Ordered Int)))+    , allLatticeLaws (LBounded     Total Distributive)   (Proxy :: Proxy (L.Levitated (O.Ordered Int)))+    , allLatticeLaws (LBoundedJoin Total Distributive)   (Proxy :: Proxy (U.Lifted (O.Ordered Int)))+    , allLatticeLaws (LNormal      Total Distributive )  (Proxy :: Proxy (Op.Op (O.Ordered Int)))++    , testProperty "Lexicographic M2 M2 contains M3" $ QC.property $+        isJust searchM3LexM2++    , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)+    , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)+    , monadLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))+    , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)+    , monadLaws "Op" (Proxy1 :: Proxy1 Op.Op)+    , monadLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)+    , monadLaws "Wide" (Proxy1 :: Proxy1 W.Wide)+    , monadLaws "Heyting.Free" (Proxy1 :: Proxy1 HF.Free)++    , finiteLaws (Proxy :: Proxy M2)+    , finiteLaws (Proxy :: Proxy M3)+    , finiteLaws (Proxy :: Proxy N5)+    , finiteLaws (Proxy :: Proxy ZeroHalfOne)++    , finiteLaws (Proxy :: Proxy OInt8)+    , finiteLaws (Proxy :: Proxy (Div.Divisibility Int8))+    , finiteLaws (Proxy :: Proxy (W.Wide Int8))+    , finiteLaws (Proxy :: Proxy (D.Dropped OInt8))+    , finiteLaws (Proxy :: Proxy (L.Levitated OInt8))+    , finiteLaws (Proxy :: Proxy (U.Lifted OInt8))+    , finiteLaws (Proxy :: Proxy (LO.Lexicographic OInt8 OInt8))+    ]++type OInt8 = O.Ordered Int8++-------------------------------------------------------------------------------+-- Monad laws+-------------------------------------------------------------------------------+ monadLaws :: forall (m :: * -> *). ( Monad m #if !MIN_VERSION_base(4, 8, 0)                                    , Applicative m@@ -81,12 +154,12 @@           -> Proxy1 m           -> TestTree monadLaws name _ = testGroup ("Monad laws: " <> name)-  [ QC.testProperty "left identity" leftIdentityProp-  , QC.testProperty "right identity" rightIdentityProp-  , QC.testProperty "composition" compositionProp-  , QC.testProperty "Applicative pure" pureProp-  , QC.testProperty "Applicative ap" apProp-  ]+    [ testProperty "left identity" leftIdentityProp+    , testProperty "right identity" rightIdentityProp+    , testProperty "composition" compositionProp+    , testProperty "Applicative pure" pureProp+    , testProperty "Applicative ap" apProp+    ]   where     leftIdentityProp :: Int -> Fun Int (m Int) -> Property     leftIdentityProp x (Fun _ k) = (return x >>= k) === k x@@ -105,33 +178,148 @@        where f' = apply <$> f  ---------------------------------------------------------------------------------- Lattice distributive+-- Partial ord laws ------------------------------------------------------------------------------- -latticeLaws-    :: forall a. (Eq a, Show a, Arbitrary a,  Lattice a, PartialOrd a)-    => String-    -> Bool -- ^ distributive+data IsTotal a where+    Total :: Ord a          => IsTotal a+    Partial :: PartialOrd a => IsTotal a++partialOrdLaws+    :: forall a. (Eq a, Show a, Arbitrary a, PartialOrd a)+    => IsTotal a     -> Proxy a     -> TestTree-latticeLaws name distr _ = testGroup ("Lattice laws: " <> name) $-    [ QC.testProperty "leq = joinLeq" joinLeqProp-    , QC.testProperty "leq = meetLeq" meetLeqProp-    , QC.testProperty "meet is lower bound" meetLower-    , QC.testProperty "join is upper bound" joinUpper-    , QC.testProperty "meet commutes" meetComm-    , QC.testProperty "join commute" joinComm-    , QC.testProperty "meet associative" meetAssoc-    , QC.testProperty "join associative" joinAssoc-    , QC.testProperty "absorbtion 1" meetAbsorb-    , QC.testProperty "absorbtion 2" joinAbsorb-    , QC.testProperty "meet idempontent" meetIdemp-    , QC.testProperty "join idempontent" joinIdemp-    , QC.testProperty "comparableDef" comparableDef-    ] ++ if not distr then [] else-    -- Not all lattices are distributive!-    [ QC.testProperty "x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)" distrProp-    , QC.testProperty "x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)" distr2Prop+partialOrdLaws total _ = testGroup "PartialOrd" $+    [ testProperty "reflexive" reflProp+    , testProperty "anti-symmetric" antiSymProp+    , testProperty "transitive" transitiveProp+    ] ++ case total of+        Partial -> []+        Total ->+            [ testProperty "total" totalProp+            , testProperty "leq/compare agree" leqCompareProp+            ]+  where+    reflProp :: a -> Property+    reflProp x = QC.property $ leq x x++    antiSymProp :: a -> a -> Property+    antiSymProp x y+        | leq x y && leq y x = label "same" $ x === y+        | otherwise          = label "diff" $ x =/= y++    transitiveProp :: a -> a -> a -> Property+    transitiveProp x y z = case p of+        []                -> label "non-related" $ QC.property True+        ((x', _, z') : _) -> label "related" $ QC.property $ leq x' z'+      where+        p = [ (x', y', z')+            | (x', y', z') <- [(x,y,z),(y,x,z),(z,y,x),(y,z,x),(z,x,y),(x,z,y)]+            , leq x' y'+            , leq y' z'+            ]++    totalProp :: a -> a -> Property+    totalProp x y = QC.property $ leq x y || leq y x++    leqCompareProp :: Ord a => a -> a -> Property+    leqCompareProp x y = agree (leq x y) (leq y x) (compare x y)+      where+        agree True True = (=== EQ)+        agree True False = (=== LT)+        agree False True = (=== GT)+        agree False False = discard++-------------------------------------------------------------------------------+-- Lattice+-------------------------------------------------------------------------------++-- | Lattice Kind+data LKind a where+    LNotLattice   :: LKind a+    LNormal       :: Lattice a => IsTotal a -> Distr ->  LKind a+    LBoundedMeet  :: BoundedMeetSemiLattice a => IsTotal a -> Distr -> LKind a+    LBoundedJoin  :: BoundedJoinSemiLattice a => IsTotal a -> Distr -> LKind a+    LBounded      :: BoundedLattice a => IsTotal a -> Distr -> LKind a+    LHeyting      :: Heyting a => IsTotal a -> IsBoolean -> LKind a++data Distr+    = NonModular+    | Modular+    | Distributive+  deriving (Eq, Ord)++data IsBoolean+    = NonBoolean+    | DeMorgan+    | IsBoolean+  deriving (Eq, Ord)++allLatticeLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Typeable a, PartialOrd a)+    => LKind a+    -> Proxy a+    -> TestTree+allLatticeLaws ki pr = case ki of+    LNotLattice -> testGroup name $+        [partialOrdLaws Partial pr]+    LNormal t d -> testGroup name $+        partialOrdLaws t pr : allLatticeLaws' d pr+    LBoundedMeet t d -> testGroup name $+        partialOrdLaws t pr : allLatticeLaws' d pr +++        [ boundedMeetLaws pr ]+    LBoundedJoin t d -> testGroup name $+        partialOrdLaws t pr :  allLatticeLaws' d pr +++        [ boundedJoinLaws pr ]+    LBounded t d -> testGroup name $+        partialOrdLaws t pr : allLatticeLaws' d pr +++        [ boundedMeetLaws pr+        , boundedJoinLaws pr+        ]+    LHeyting t b -> testGroup name $+        partialOrdLaws t pr : allLatticeLaws' Distributive pr +++        [ boundedMeetLaws pr+        , boundedJoinLaws pr+        , heytingLaws pr+        ] +++        [ deMorganLaws pr | b >= DeMorgan ] +++        [ booleanLaws pr | b >= IsBoolean ]+  where+    name = show (typeOf (undefined :: a))++allLatticeLaws'+    :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a)+    => Distr+    -> Proxy a+    -> [TestTree]+allLatticeLaws' distr pr =+    [ latticeLaws pr ] +++    [ modularLaws pr | distr >= Modular ] +++    [ distributiveLaws pr | distr >= Distributive ]++-------------------------------------------------------------------------------+-- Lattice laws+-------------------------------------------------------------------------------++latticeLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a)+    => Proxy a+    -> TestTree+latticeLaws _ = testGroup "Lattice"+    [ testProperty "leq = joinLeq" joinLeqProp+    , testProperty "leq = meetLeq" meetLeqProp+    , testProperty "meet is lower bound" meetLower+    , testProperty "join is upper bound" joinUpper+    , testProperty "meet commutes" meetComm+    , testProperty "join commute" joinComm+    , testProperty "meet associative" meetAssoc+    , testProperty "join associative" joinAssoc+    , testProperty "absorbtion 1" meetAbsorb+    , testProperty "absorbtion 2" joinAbsorb+    , testProperty "meet idempontent" meetIdemp+    , testProperty "join idempontent" joinIdemp+    , testProperty "comparableDef" comparableDef     ]   where     joinLeqProp :: a -> a -> Property@@ -177,133 +365,257 @@     comparableDef :: a -> a -> Property     comparableDef x y = (leq x y || leq y x) === comparable x y +-------------------------------------------------------------------------------+-- Modular+-------------------------------------------------------------------------------++modularLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a)+    => Proxy a+    -> TestTree+modularLaws _ = testGroup "Modular"+    [ testProperty "(y ∧ (x ∨ z)) ∨ z = (y ∨ z) ∧ (x ∨ z)" modularProp+    ]+  where+    modularProp :: a -> a -> a -> Property+    modularProp x y z = lhs === rhs where+        lhs = (y /\ (x \/ z)) \/ z+        rhs = (y \/ z) /\ (x \/ z)++-------------------------------------------------------------------------------+-- Distributive+-------------------------------------------------------------------------------++distributiveLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a)+    => Proxy a+    -> TestTree+distributiveLaws _ = testGroup "Distributive"+    [ testProperty "x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)" distrProp+    , testProperty "x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)" distr2Prop+    ]+  where     distrProp :: a -> a -> a -> Property-    distrProp x y z = lhs === rhs-      where+    distrProp x y z = lhs === rhs where         lhs = x /\ (y \/ z)         rhs = (x /\ y) \/ (x /\ z)      distr2Prop :: a -> a -> a -> Property-    distr2Prop x y z = lhs === rhs-      where+    distr2Prop x y z = lhs === rhs where         lhs = x \/ (y /\ z)         rhs = (x \/ y) /\ (x \/ z)  ---------------------------------------------------------------------------------- Orphans+-- Bounded lattice laws ------------------------------------------------------------------------------- -instance Arbitrary a => Arbitrary (D.Dropped a) where-  arbitrary = frequency [ (1, pure D.Top)-                        , (9, D.Drop <$> arbitrary)-                        ]--instance Arbitrary a => Arbitrary (U.Lifted a) where-  arbitrary = frequency [ (1, pure U.Bottom)-                        , (9, U.Lift <$> arbitrary)-                        ]+boundedMeetLaws+    :: forall a. (Eq a, Show a, Arbitrary a, BoundedMeetSemiLattice a)+    => Proxy a+    -> TestTree+boundedMeetLaws _ = testGroup "BoundedMeetSemiLattice"+    [ testProperty "top /\\ x = x" identityLeftProp+    , testProperty "x /\\ top = x" identityRightProp+    , testProperty "top \\/ x = top" annihilationLeftProp+    , testProperty "x \\/ top = top" annihilationRightProp+    ]+  where+    identityLeftProp :: a -> Property+    identityLeftProp x = lhs === rhs where+        lhs = top /\ x+        rhs = x -instance Arbitrary a => Arbitrary (L.Levitated a) where-  arbitrary = frequency [ (1, pure L.Top)-                        , (1, pure L.Bottom)-                        , (9, L.Levitate <$> arbitrary)-                        ]+    identityRightProp :: a -> Property+    identityRightProp x = lhs === rhs where+        lhs = x /\ top+        rhs = x -instance Arbitrary a => Arbitrary (O.Ordered a) where-  arbitrary = O.Ordered <$> arbitrary-  shrink = map O.Ordered . shrink . O.getOrdered+    annihilationLeftProp :: a -> Property+    annihilationLeftProp x = lhs === rhs where+        lhs = top \/ x+        rhs = top -instance (Arbitrary a, Num a, Ord a) => Arbitrary (Div.Divisibility a) where-  arbitrary = divisibility <$> arbitrary-  shrink d = filter (<d) . map divisibility . shrink . Div.getDivisibility $ d+    annihilationRightProp :: a -> Property+    annihilationRightProp x = lhs === rhs where+        lhs = x \/ top+        rhs = top -divisibility :: (Ord a, Num a) => a -> Div.Divisibility a-divisibility x | x < (-1)  = Div.Divisibility (abs x)-               | x < 1     = Div.Divisibility 1-               | otherwise = Div.Divisibility x+boundedJoinLaws+    :: forall a. (Eq a, Show a, Arbitrary a, BoundedJoinSemiLattice a)+    => Proxy a+    -> TestTree+boundedJoinLaws _ = testGroup "BoundedJoinSemiLattice"+    [ testProperty "bottom \\/ x = x" identityLeftProp+    , testProperty "x \\/ bottom = x" identityRightProp+    , testProperty "bottom /\\ x = bottom" annihilationLeftProp+    , testProperty "x /\\ bottom = bottom" annihilationRightProp+    ]+  where+    identityLeftProp :: a -> Property+    identityLeftProp x = lhs === rhs where+        lhs = bottom \/ x+        rhs = x +    identityRightProp :: a -> Property+    identityRightProp x = lhs === rhs where+        lhs = x \/ bottom+        rhs = x -instance Arbitrary a => Arbitrary (Op.Op a) where-  arbitrary = Op.Op <$> arbitrary+    annihilationLeftProp :: a -> Property+    annihilationLeftProp x = lhs === rhs where+        lhs = bottom /\ x+        rhs = bottom -instance (Arbitrary k, Arbitrary v) => Arbitrary (LO.Lexicographic k v) where-    arbitrary = uncurry LO.Lexicographic <$> arbitrary-    shrink (LO.Lexicographic k v) = uncurry LO.Lexicographic <$> shrink (k, v)+    annihilationRightProp :: a -> Property+    annihilationRightProp x = lhs === rhs where+        lhs = x /\ bottom+        rhs = bottom  ---------------------------------------------------------------------------------- Examples+-- Heyting laws ------------------------------------------------------------------------------- --- | Non-distributive lattice-data M3 = M3_0 | M3_a | M3_b | M3_c | M3_1-  deriving (Eq, Ord, Show, Enum, Bounded)+heytingLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Heyting a, Typeable a)+    => Proxy a+    -> TestTree+heytingLaws _ = testGroup "Heyting"+    [ testProperty "neg default" negDefaultProp+    , testProperty "<=> default" equivDefaultProp+    , testProperty "x ==> x = top" idIsTopProp+    , testProperty "a /\\ (a ==> b) = a /\\ b" andDomainProp+    , testProperty "b /\\ (a ==> b) = b" andCodomainProp+    , testProperty "a ==> (b /\\ c) = (a ==> b) /\\ (a ==> c)" implDistrProp+    , testProperty "de Morgan 1" deMorganProp1+    , testProperty "weak de Morgan 2" deMorganProp2weak+    ]+  where+    negDefaultProp :: a -> Property+    negDefaultProp x = lhs === rhs where+        lhs = neg x+        rhs = x ==> bottom -instance Arbitrary M3 where-    arbitrary = QC.arbitraryBoundedEnum+    equivDefaultProp :: a -> a -> Property+    equivDefaultProp x y = lhs === rhs where+        lhs = x <=> y+        rhs = (x ==> y) /\ (y ==> x) -instance PartialOrd M3 where-    x    `leq` y    | x == y = True-    M3_0 `leq` _             = True-    _    `leq` M3_1          = True-    _    `leq` _             = False+    idIsTopProp :: a -> Property+    idIsTopProp x = lhs === rhs where+        lhs = x ==> x+        rhs = top -instance JoinSemiLattice M3 where-    x    \/ M3_0          = x-    M3_0 \/ y             = y-    _    \/ M3_1          = M3_1-    M3_1 \/ _             = M3_1-    x    \/ y | x == y    = x-              | otherwise = M3_1+    andDomainProp :: a -> a -> Property+    andDomainProp x y = lhs === rhs where+        lhs = x /\ (x ==> y)+        rhs = x /\ y -instance MeetSemiLattice M3 where-    x    /\ M3_1          = x-    M3_1 /\ y             = y-    _    /\ M3_0          = M3_0-    M3_0 /\ _             = M3_0-    x    /\ y | x == y    = x-              | otherwise = M3_0+    andCodomainProp :: a -> a -> Property+    andCodomainProp x y = lhs === rhs where+        lhs = y /\ (x ==> y)+        rhs = y -instance Lattice M3 where+    implDistrProp :: a -> a -> a -> Property+    implDistrProp x y z+        | typeOf (undefined :: a) == typeOf (undefined :: HF.Free Var)+            = QC.mapSize (min 16) $ implDistrProp' x y z+        | otherwise+            = implDistrProp' x y z --- | Set Bool, M2-data M2 = M2_0 | M2_T | M2_F | M2_1-  deriving (Eq, Ord, Show, Enum, Bounded)+    implDistrProp' :: a -> a -> a -> Property+    implDistrProp' x y z = lhs === rhs where+        lhs = x ==> (y /\ z)+        rhs = (x ==> y) /\ (x ==> z) -instance Arbitrary M2 where-    arbitrary = QC.arbitraryBoundedEnum+    deMorganProp1 :: a -> a -> Property+    deMorganProp1 x y = lhs === rhs where+        lhs = neg (x \/ y)+        rhs = neg x /\ neg y -instance PartialOrd M2 where-    x    `leq` y   | x == y  = True-    M2_0 `leq` _             = True-    _    `leq` M2_1          = True-    _    `leq` _             = False+    deMorganProp2weak :: a -> a -> Property+    deMorganProp2weak x y = lhs === rhs where+        lhs = neg (x /\ y)+        rhs = neg (neg (neg x \/ neg y)) -instance JoinSemiLattice M2 where-    x    \/ M2_0          = x-    M2_0 \/ y             = y-    _    \/ M2_1          = M2_1-    M2_1 \/ _             = M2_1-    x    \/ y | x == y    = x-              | otherwise = M2_1+-------------------------------------------------------------------------------+-- De morgan+------------------------------------------------------------------------------- -instance MeetSemiLattice M2 where-    x    /\ M2_1          = x-    M2_1 /\ y             = y-    _    /\ M2_0          = M2_0-    M2_0 /\ _             = M2_0-    x    /\ y | x == y    = x-              | otherwise = M2_0+deMorganLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Heyting a)+    => Proxy a+    -> TestTree+deMorganLaws _ = testGroup "de Morgan"+    [ testProperty "de Morgan 2" deMorganProp2+    ]+  where+    deMorganProp2 :: a -> a -> Property+    deMorganProp2 x y = lhs === rhs where+        lhs = neg (x /\ y)+        rhs = neg x \/ neg y -instance Lattice M2 where+-------------------------------------------------------------------------------+-- Boolean laws+------------------------------------------------------------------------------- -instance BoundedJoinSemiLattice M2 where-    bottom = M2_0+booleanLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Heyting a)+    => Proxy a+    -> TestTree+booleanLaws _ = testGroup "Boolean"+    [ testProperty "LEM: neg x \\/ x = top" lemProp+    , testProperty "DN: neg (neg x) = x" dnProp+    ]+  where+    lemProp :: a -> Property+    lemProp x = lhs === rhs where+        lhs = neg x \/ x+        rhs = top -instance BoundedMeetSemiLattice M2 where-    top = M2_1+    -- every element is regular, i.e. either of following equivalend conditions hold:+    -- * neg (neg x) = x+    -- * x = neg y, for some y in H -- I don't know example of this+    dnProp :: a -> Property+    dnProp x = lhs === rhs where+        lhs = neg (neg x)+        rhs = x -instance BoundedLattice M2 where+-------------------------------------------------------------------------------+-- Universe / Finite laws+------------------------------------------------------------------------------- +finiteLaws+    :: forall a. (Eq a, Show a, Arbitrary a, Typeable a, Finite a)+    => Proxy a+    -> TestTree+finiteLaws _ = testGroup name+    [ testProperty "elem x universe" elemProp+    , testProperty "length pfx = length (nub pfx)" prefixProp++    , testProperty "elem x universeF" elemFProp+    , testProperty "length (filter (== x) universeF) = 1" singleProp+    , testProperty "cardinality = Tagged (genericLength universeF)" cardinalityProp+    ]+  where+    name = show (typeOf (undefined :: a))++    elemProp :: a -> Property+    elemProp x = QC.property $ elem x universe++    elemFProp :: a -> Property+    elemFProp x = QC.property $ elem x universeF++    prefixProp :: Int -> Property+    prefixProp n =+        let pfx = take n (universe :: [a])+        in QC.counterexample (show pfx) $ length pfx === length (nub pfx)++    singleProp :: a -> Property+    singleProp x = length (filter (== x) universeF) === 1++    cardinalityProp :: Property+    cardinalityProp = cardinality === (Tagged (genericLength (universeF :: [a])) :: Tagged a Natural)+ ------------------------------------------------------------------------------- -- Lexicographic M2 search -------------------------------------------------------------------------------@@ -331,11 +643,11 @@     guard (xc `leq` x1)      -- homomorphism-    let f M3_0 = x1-        f M3_a = xa-        f M3_b = xb-        f M3_c = xc-        f M3_1 = x1+    let f M3o = x1+        f M3a = xa+        f M3b = xb+        f M3c = xc+        f M3i = x1      ma <- [minBound .. maxBound]     mb <- [minBound .. maxBound]@@ -351,3 +663,17 @@   where     xs = [ LO.Lexicographic x y | x <- ys, y <- ys ]     ys = [minBound .. maxBound]++-------------------------------------------------------------------------------+-- Variable (for Free)+-------------------------------------------------------------------------------++-- | The less variables we have, the quicker tests will be :)+data Var = A | B | C | D+  deriving (Eq, Ord, Show, Enum, Bounded, Typeable)++instance Arbitrary Var where+    arbitrary = QC.arbitraryBoundedEnum++    shrink A = []+    shrink x = [ minBound .. pred x ]

binary file changed (absent → 11918 bytes)