From 83f6025acf847de0e9cae335fc98bffa41848646 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 11 Nov 2024 16:47:14 +0100 Subject: [PATCH] Cleaned up project a little bit --- README.md | 5 ++++ app/FileAutomata.hs | 4 +-- app/FoSolver.hs | 4 +-- app/IO.hs | 20 ++++++------- app/Minimise.hs | 7 ++--- app/Teacher.hs | 3 +- ons-hs.cabal | 10 +++---- src/EquivariantMap.hs | 11 +++---- src/EquivariantSet.hs | 1 + src/Nominal.hs | 63 ++++++++++++++--------------------------- src/Nominal/Atom.hs | 25 ++++++++++++++++ src/Nominal/Class.hs | 7 +++-- src/Nominal/Products.hs | 35 +++++++++++++++++++++++ src/Nominal/Support.hs | 62 ++++++++++++++++++++++++++++++++++++++++ src/OrbitList.hs | 15 +++++----- src/Permutable.hs | 8 +++--- src/Quotient.hs | 15 +++++----- src/Support.hs | 15 ---------- src/Support/OrdList.hs | 42 --------------------------- src/Support/Rat.hs | 16 ----------- src/Support/Set.hs | 37 ------------------------ test/Bench.hs | 27 +++++++++--------- test/Spec.hs | 6 ++-- test/SpecMap.hs | 25 ++++++++-------- test/SpecPermutable.hs | 4 +-- test/SpecSet.hs | 39 +++++++++++++------------ test/SpecUtils.hs | 8 +++--- 27 files changed, 252 insertions(+), 262 deletions(-) create mode 100644 src/Nominal/Atom.hs create mode 100644 src/Nominal/Support.hs delete mode 100644 src/Support.hs delete mode 100644 src/Support/OrdList.hs delete mode 100644 src/Support/Rat.hs delete mode 100644 src/Support/Set.hs diff --git a/README.md b/README.md index bf1d6a9..2002b51 100644 --- a/README.md +++ b/README.md @@ -114,6 +114,11 @@ values, that can be much faster. ## Changelog +version 0.4 (2024-11-11): +* Changed from rational number to integers (for performance). +* Cleaned up module structure and API. +* Started writing some haddock. + version 0.3.1.0 (2024-11-06): * More types of products * Stuff to do permutations (not only monotone ones) diff --git a/app/FileAutomata.hs b/app/FileAutomata.hs index 4acb325..493fcef 100644 --- a/app/FileAutomata.hs +++ b/app/FileAutomata.hs @@ -17,9 +17,9 @@ import Text.Megaparsec.Char as P import qualified Text.Megaparsec.Char.Lexer as L import OrbitList -import Nominal (Atom) +import Nominal import Nominal.Class -import Support (Support, def) +import Nominal.Support (def) import Automata import qualified EquivariantSet as Set import qualified EquivariantMap as Map diff --git a/app/FoSolver.hs b/app/FoSolver.hs index 6f79da4..3a10995 100644 --- a/app/FoSolver.hs +++ b/app/FoSolver.hs @@ -1,7 +1,7 @@ {-# LANGUAGE PatternSynonyms #-} import OrbitList hiding (head) -import Support (Rat) +import Nominal import Prelude (Show, Ord, Eq, Int, IO, print, otherwise, (.), ($), (!!), (+), (-), Bool, head, tail) import qualified Prelude as P @@ -81,7 +81,7 @@ forAll p = not (exists (not p)) -- Here is the solver. It keeps track of a nominal set. -- If that sets is empty in the end, the formula does not hold. -type Context = SortedOrbitList [Rat] +type Context = SortedOrbitList [Atom] extend, drop :: Context -> Context extend ctx = productWith (:) rationals ctx diff --git a/app/IO.hs b/app/IO.hs index dbe0ccd..fcc62d3 100644 --- a/app/IO.hs +++ b/app/IO.hs @@ -6,11 +6,11 @@ import Data.Char (isSpace) import Data.Ratio import Data.List (intersperse) -import Nominal import Automata -import Support (Rat(..), Support(..)) -import OrbitList as L (toList) import EquivariantMap as M (toList) +import Nominal +import Nominal.Support as Support +import OrbitList as L (toList) -- I do not want to give weird Show instances for basic types, so I create my @@ -20,13 +20,11 @@ class FromStr a where fromStr :: String -> (a, String) -- Should always print integers, this is not a problem for the things we build -- from getElementE (since it returns elements with support from 1 to n). -instance ToStr Rat where - toStr (Rat r) = case denominator r of - 1 -> show (numerator r) - _ -> error "Can only show integers" +instance ToStr Atom where + toStr = show instance ToStr Support where - toStr (Support s) = "{" ++ toStr s ++ "}" + toStr s = "{" ++ toStr (Support.toList s) ++ "}" instance ToStr Bool where toStr b = show b instance ToStr Int where toStr i = show i @@ -46,8 +44,8 @@ instance (Nominal q, Nominal a, ToStr q, ToStr a) => ToStr (Automaton q a) where ", acceptance = " ++ toStr (M.toList acceptance) ++ ", transition = " ++ toStr (M.toList transition) ++ " }" -instance FromStr Rat where - fromStr str = (Rat (read l % 1), r) +instance FromStr Atom where + fromStr str = (atom (read l), r) where (l, r) = break isSpace str instance FromStr a => FromStr [a] where @@ -55,7 +53,7 @@ instance FromStr a => FromStr [a] where fromStr str = (a : l, emptyStr) where (a, str2) = fromStr str - (l, emptyStr) = fromStr (dropWhile isSpace str2) + (l, emptyStr) = fromStr (dropWhile isSpace str2) newtype MQ a = MQ a deriving (Eq, Ord, Show) diff --git a/app/Minimise.hs b/app/Minimise.hs index 0f2898e..1d03808 100644 --- a/app/Minimise.hs +++ b/app/Minimise.hs @@ -6,20 +6,19 @@ {-# language UndecidableInstances #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} +import EquivariantMap ((!)) import ExampleAutomata import FileAutomata import IO -import Quotient import OrbitList -import EquivariantMap ((!)) +import Quotient import qualified EquivariantMap as Map import qualified EquivariantSet as Set +import Prelude as P hiding (map, product, words, filter, foldr) import System.Environment import System.IO -import Prelude as P hiding (map, product, words, filter, foldr) - -- Version A: works on equivalence relations minimiseA :: _ => OrbitList a -> Automaton q a -> Automaton _ a diff --git a/app/Teacher.hs b/app/Teacher.hs index c0d360a..831ad7f 100644 --- a/app/Teacher.hs +++ b/app/Teacher.hs @@ -11,7 +11,6 @@ import ExampleAutomata import IO import Nominal (Atom) import OrbitList qualified -import Support (Rat (..)) data Example = Fifo Int @@ -19,7 +18,7 @@ data Example main :: IO () main = - let ex = Fifo 2 + let ex = DoubleWord 2 in case ex of Fifo n -> teach "FIFO" (fifoFun n) (fifoCex n) DoubleWord n -> teach "ATOMS" (doubleFun n) (doubleCex n) diff --git a/ons-hs.cabal b/ons-hs.cabal index d64aed4..e259f2f 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 name: ons-hs -version: 0.3.1.0 +version: 0.4.0.0-dev synopsis: Implementation of the ONS (Ordered Nominal Sets) library in Haskell description: Nominal sets are structured infinite sets. They have symmetries which make them finitely representable. This library provides basic manipulation of them for the total order symmetry. It includes: products, sums, maps and sets. Can work with custom data types. homepage: https://github.com/Jaxan/ons-hs @@ -26,15 +26,13 @@ library EquivariantMap, EquivariantSet, Nominal, + Nominal.Atom, Nominal.Class, Nominal.Products, + Nominal.Support, OrbitList, Permutable, - Quotient, - Support, - Support.OrdList, - Support.Rat, - Support.Set + Quotient build-depends: data-ordlist, MemoTrie diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs index b3d3b06..3886824 100644 --- a/src/EquivariantMap.hs +++ b/src/EquivariantMap.hs @@ -1,20 +1,21 @@ {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} module EquivariantMap where -import Data.Semigroup (Semigroup) import Data.Map (Map) -import qualified Data.Map as Map +import Data.Map qualified as Map import Data.Maybe (fromMaybe) +import Data.Semigroup (Semigroup) import EquivariantSet (EquivariantSet(..)) import Nominal -import Support +import Nominal.Support as Support -- TODO: foldable / traversable @@ -135,7 +136,7 @@ filter p (EqMap m) = EqMap (Map.filterWithKey p2 m) mapel :: (Nominal k, Nominal v) => k -> v -> (Orbit v, [Bool]) mapel k v = (toOrbit v, bv (Support.toList (support k)) (Support.toList (support v))) -bv :: [Rat] -> [Rat] -> [Bool] +bv :: [Atom] -> [Atom] -> [Bool] bv l [] = replicate (length l) False bv [] _ = error "Non-equivariant function" bv (x:xs) (y:ys) = case compare x y of @@ -144,5 +145,5 @@ bv (x:xs) (y:ys) = case compare x y of GT -> error "Non-equivariant function" mapelInv :: (Nominal k, Nominal v) => k -> (Orbit v, [Bool]) -> v -mapelInv x (oy, bs) = getElement oy (Support.fromDistinctAscList . fmap fst . Prelude.filter snd $ zip (Support.toList (support x)) bs) +mapelInv x (oy, bs) = getElement oy (fromDistinctAscList . fmap fst . Prelude.filter snd $ zip (Support.toList (support x)) bs) diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs index fc9b036..c0e673a 100644 --- a/src/EquivariantSet.hs +++ b/src/EquivariantSet.hs @@ -14,6 +14,7 @@ import qualified Data.Set as Set import Prelude hiding (map, product) import Nominal +import Nominal.Products as Nominal import OrbitList (OrbitList(..)) diff --git a/src/Nominal.hs b/src/Nominal.hs index 54730ae..ed21d13 100644 --- a/src/Nominal.hs +++ b/src/Nominal.hs @@ -1,54 +1,33 @@ {-# LANGUAGE ScopedTypeVariables #-} -module Nominal - ( module Nominal - , module Nominal.Class - ) where +module Nominal ( + -- * Atoms + -- | Re-exports from "Nominal.Atom". + Atom, + atom, + -- * Support + -- | Re-exports from "Nominal.Support". + Support, + -- * The Nominal type class + Nominal (..), + Trivially (..), + Generically (..), + -- * Helper functions + module Nominal, +) where import Data.Proxy -import Nominal.Products +import Nominal.Atom import Nominal.Class -import Support (Rat, def) +import Nominal.Products +import Nominal.Support -type Atom = Rat - --- We can get 'default' values, if we don't care about the support. +-- | We can construct a "default" element from an orbit. In this case, the +-- support is chosen arbitrarily. getElementE :: forall a. Nominal a => Orbit a -> a getElementE orb = getElement orb (def (index (Proxy :: Proxy a) orb)) --- We can `map` orbits to orbits for equivariant functions +-- | We can `map` orbits to orbits for equivariant functions. omap :: (Nominal a, Nominal b) => (a -> b) -> Orbit a -> Orbit b omap f = toOrbit . f . getElementE - --- General combinator -productG :: (Nominal a, Nominal b) => (Int -> Int -> [[Ordering]]) -> Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -productG strs pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> strs (index pa oa) (index pb ob) - --- Enumerate all orbits in a product A x B. -product :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -product = productG prodStrings - --- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.} -separatedProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -separatedProduct = productG sepProdStrings - --- "Left product": A ⫂ B = { (a,b) | C supports a => C supports b } -leftProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -leftProduct = productG lsupprProdStrings - --- "Right product": A ⫁ B = { (a,b) | C supports a <= C supports b } -rightProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -rightProduct = productG rsupplProdStrings - --- Strictly increasing product = { (a,b) | all elements in a < all elements in b } -increasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -increasingProduct = productG incrSepProdStrings - --- Strictly decreasing product = { (a,b) | all elements in a > elements in b } -decreasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -decreasingProduct = productG decrSepProdStrings - --- Strictly decreasing product = { (a,b) | all elements in a > elements in b } -testProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] -testProduct = productG testProdStrings diff --git a/src/Nominal/Atom.hs b/src/Nominal/Atom.hs new file mode 100644 index 0000000..094fd5e --- /dev/null +++ b/src/Nominal/Atom.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE DerivingVia #-} + +module Nominal.Atom where + +-- * Atoms + +-- $Atoms +-- Module with the 'Atom' type. This is re-exported from the "Nominal" module, +-- and it often suffices to only import "Nominal". + +-- | This is the type of atoms of our "ordered nominal sets" library. +-- Theoretically, you should think of atoms these as rational numbers, forming +-- a dense linear order. They can be compared for equality and order. +-- In the implementation, however, we represent them as integers, because in +-- any given situation only a finite number of atoms occur and we can choose +-- integral points. The library will always do this automatically, and I +-- noticed that in all applications, integers also suffice from the user +-- perspective. +newtype Atom = Atom {unAtom :: Int} + deriving (Eq, Ord) + deriving Show via Int + +-- | Creates an atom with the value specified by the integer. +atom :: Int -> Atom +atom = Atom diff --git a/src/Nominal/Class.hs b/src/Nominal/Class.hs index b4d696c..ce84359 100644 --- a/src/Nominal/Class.hs +++ b/src/Nominal/Class.hs @@ -20,7 +20,8 @@ import Data.Proxy (Proxy(..)) import Data.Void import GHC.Generics -import Support +import Nominal.Atom +import Nominal.Support as Support -- This is the main meat of the package. The Nominal typeclass, it gives us ways @@ -45,8 +46,8 @@ class Nominal a where -- We can construct orbits from rational numbers. There is exactly one orbit, -- so this can be represented by the unit type. -instance Nominal Rat where - type Orbit Rat = () +instance Nominal Atom where + type Orbit Atom = () toOrbit _ = () support r = Support.singleton r getElement _ s = Support.min s diff --git a/src/Nominal/Products.hs b/src/Nominal/Products.hs index 445b808..09d96e7 100644 --- a/src/Nominal/Products.hs +++ b/src/Nominal/Products.hs @@ -2,6 +2,9 @@ module Nominal.Products where import Control.Applicative import Data.MemoTrie +import Data.Proxy + +import Nominal.Class -- Enumerates strings to compute all possible combinations. Here `LT` means the -- "current" element goes to the left, `EQ` goes to both, and `GT` goes to the @@ -68,6 +71,38 @@ testProdStrings = mgen (0 :: Int) where <|> (GT :) <$> mgen (k-1) n (m-1) +-- General combinator +productG :: (Nominal a, Nominal b) => (Int -> Int -> [[Ordering]]) -> Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +productG strs pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> strs (index pa oa) (index pb ob) + +-- Enumerate all orbits in a product A x B. +product :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +product = productG prodStrings + +-- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.} +separatedProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +separatedProduct = productG sepProdStrings + +-- "Left product": A ⫂ B = { (a,b) | C supports a => C supports b } +leftProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +leftProduct = productG lsupprProdStrings + +-- "Right product": A ⫁ B = { (a,b) | C supports a <= C supports b } +rightProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +rightProduct = productG rsupplProdStrings + +-- Strictly increasing product = { (a,b) | all elements in a < all elements in b } +increasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +increasingProduct = productG incrSepProdStrings + +-- Strictly decreasing product = { (a,b) | all elements in a > elements in b } +decreasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +decreasingProduct = productG decrSepProdStrings + +-- Strictly decreasing product = { (a,b) | all elements in a > elements in b } +testProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)] +testProduct = productG testProdStrings + {- NOTE on performance: Previously, I had INLINABLE and SPECIALIZE pragmas for all above definitions. But with benchmarking, I concluded that they do not make any difference. So diff --git a/src/Nominal/Support.hs b/src/Nominal/Support.hs new file mode 100644 index 0000000..ab7a82b --- /dev/null +++ b/src/Nominal/Support.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE DerivingVia #-} + +module Nominal.Support where + +import qualified Data.List as List +import qualified Data.List.Ordered as OrdList + +import Nominal.Atom + +-- * Support + +-- | A support is a finite set of 'Atom's. In the implementation, it is +-- represented by a sorted list. +newtype Support = Support {unSupport :: [Atom]} + deriving (Eq, Ord) + deriving Show via [Atom] + +-- ** Queries + +size :: Support -> Int +size = List.length . unSupport + +null :: Support -> Bool +null = List.null . unSupport + +min :: Support -> Atom +min = List.head . unSupport + +-- ** Construction + +empty :: Support +empty = Support [] + +singleton :: Atom -> Support +singleton r = Support [r] + +-- | Returns a "default" support with n elements. +def :: Int -> Support +def n = fromDistinctAscList . fmap (Atom . fromIntegral) $ [1 .. n] + +-- ** Set operations + +union :: Support -> Support -> Support +union (Support x) (Support y) = Support (OrdList.union x y) + +intersect :: Support -> Support -> Support +intersect (Support x) (Support y) = Support (OrdList.isect x y) + +toList :: Support -> [Atom] +toList = unSupport + +-- ** Conversion to/from lists + +fromList, fromAscList, fromDistinctAscList :: [Atom] -> Support +fromList = Support . OrdList.nubSort +fromAscList = Support . OrdList.nub +fromDistinctAscList = Support + +{- NOTE: I have tried using a `Data.Set` data structure for supports, but it +was slower. Using lists is fast enough, perhaps other data structures like +vectors could be considered at some point. +-} diff --git a/src/OrbitList.hs b/src/OrbitList.hs index c801ff1..6fd3f78 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -13,7 +13,8 @@ import Data.Proxy import Prelude hiding (map, product) import Nominal -import Support (Rat(..)) +import Nominal.Products as Nominal +import Nominal.Class -- Similar to EquivariantSet, but merely a list structure. It is an -- equivariant data type, so the Nominal instance is trivial. @@ -53,26 +54,26 @@ empty = OrbitList [] singleOrbit :: Nominal a => a -> OrbitList a singleOrbit a = OrbitList [toOrbit a] -rationals :: OrbitList Rat -rationals = singleOrbit (Rat 0) +rationals :: OrbitList Atom +rationals = singleOrbit (atom 0) cons :: Nominal a => a -> OrbitList a -> OrbitList a cons a (OrbitList l) = OrbitList (toOrbit a : l) -repeatRationals :: Int -> OrbitList [Rat] +repeatRationals :: Int -> OrbitList [Atom] repeatRationals 0 = singleOrbit [] repeatRationals n = productWith (:) rationals (repeatRationals (n-1)) -distinctRationals :: Int -> OrbitList [Rat] +distinctRationals :: Int -> OrbitList [Atom] distinctRationals 0 = singleOrbit [] distinctRationals n = map (uncurry (:)) . OrbitList.separatedProduct rationals $ (distinctRationals (n-1)) -increasingRationals :: Int -> OrbitList [Rat] +increasingRationals :: Int -> OrbitList [Atom] increasingRationals 0 = singleOrbit [] increasingRationals n = map (uncurry (:)) . OrbitList.increasingProduct rationals $ (increasingRationals (n-1)) -- Bell numbers -repeatRationalUpToPerm :: Int -> OrbitList [Rat] +repeatRationalUpToPerm :: Int -> OrbitList [Atom] repeatRationalUpToPerm 0 = singleOrbit [] repeatRationalUpToPerm 1 = map pure rationals repeatRationalUpToPerm n = OrbitList.map (uncurry (:)) (OrbitList.increasingProduct rationals (repeatRationalUpToPerm (n-1))) <> OrbitList.map (uncurry (:)) (OrbitList.rightProduct rationals (repeatRationalUpToPerm (n-1))) diff --git a/src/Permutable.hs b/src/Permutable.hs index 8b7ad65..edf4f8f 100644 --- a/src/Permutable.hs +++ b/src/Permutable.hs @@ -6,13 +6,13 @@ import Data.List (permutations) import Data.Map.Strict qualified as Map import Nominal -import Support +import Nominal.Support (toList) --------------------------------- --------------------------------- -- Invariant: No element occurs more than once -newtype Perm = Perm (Map.Map Rat Rat) +newtype Perm = Perm (Map.Map Atom Atom) deriving (Eq, Ord, Show) identity :: Perm @@ -56,7 +56,7 @@ bind comp (Permuted f a) = case comp a of Permuted g b -> shrink $ Permuted (compose g f) b allPermutations :: Support -> [Perm] -allPermutations (Support xs) = fmap (reduce . Perm . Map.fromList . zip xs) . permutations $ xs +allPermutations xs = fmap (reduce . Perm . Map.fromList . zip (toList xs)) . permutations $ toList xs -- Returns a lazy list allPermuted :: Nominal a => a -> [Permuted a] @@ -75,7 +75,7 @@ class Permutable a where instance Permutable (Permuted a) where act = join -instance Permutable Rat where +instance Permutable Atom where act (Permuted (Perm m) p) = Map.findWithDefault p p m -- TODO: make all this generic diff --git a/src/Quotient.hs b/src/Quotient.hs index e0b4db5..c28a76f 100644 --- a/src/Quotient.hs +++ b/src/Quotient.hs @@ -1,13 +1,14 @@ -{-# language FlexibleContexts #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ImportQualifiedPost #-} module Quotient where -import Nominal (Nominal(..)) -import Support (Support, intersect) -import OrbitList import EquivariantMap (EquivariantMap) -import qualified EquivariantMap as Map +import EquivariantMap qualified as Map import EquivariantSet (EquivariantSet) -import qualified EquivariantSet as Set +import EquivariantSet qualified as Set +import Nominal hiding (product) +import Nominal.Support (intersect) +import OrbitList import Prelude (Bool, Int, Ord, (.), (<>), (+), ($), fst, snd, fmap, uncurry) @@ -32,7 +33,7 @@ quotientf :: (Nominal a, Ord (Orbit a)) quotientf k f ls = go k Map.empty empty (toList ls) where go n phi acc [] = (phi, acc, n) - go n phi acc (a:as) = + go n phi acc (a:as) = let y0 = filter (uncurry f) (product (singleOrbit a) (fromList as)) y1 = filter (uncurry f) (product (singleOrbit a) (singleOrbit a)) y2 = map (\(a1, a2) -> (a2, (n, support a1 `intersect` support a2))) (y1 <> y0) diff --git a/src/Support.hs b/src/Support.hs deleted file mode 100644 index b26c606..0000000 --- a/src/Support.hs +++ /dev/null @@ -1,15 +0,0 @@ -module Support - ( module Support - , module Support.OrdList - , module Support.Rat - ) where - -import Support.OrdList -import Support.Rat - --- A support is a set of rational numbers, which can always be ordered. There --- are several implementations: Ordered Lists, Sets, ...? This module chooses --- the implementation. Change the import and export to experiment. - -def :: Int -> Support -def n = fromDistinctAscList . fmap (Rat . toRational) $ [1..n] diff --git a/src/Support/OrdList.hs b/src/Support/OrdList.hs deleted file mode 100644 index d7e93b8..0000000 --- a/src/Support/OrdList.hs +++ /dev/null @@ -1,42 +0,0 @@ -module Support.OrdList where - -import qualified Data.List as List -import qualified Data.List.Ordered as OrdList - -import Support.Rat - --- always sorted -newtype Support = Support { unSupport :: [Rat] } - deriving (Eq, Ord) - -instance Show Support where - show = show . unSupport - -size :: Support -> Int -size = List.length . unSupport - -null :: Support -> Bool -null = List.null . unSupport - -min :: Support -> Rat -min = List.head . unSupport - -empty :: Support -empty = Support [] - -union :: Support -> Support -> Support -union (Support x) (Support y) = Support (OrdList.union x y) - -intersect :: Support -> Support -> Support -intersect (Support x) (Support y) = Support (OrdList.isect x y) - -singleton :: Rat -> Support -singleton r = Support [r] - -toList :: Support -> [Rat] -toList = unSupport - -fromList, fromAscList, fromDistinctAscList :: [Rat] -> Support -fromList = Support . OrdList.nubSort -fromAscList = Support . OrdList.nub -fromDistinctAscList = Support diff --git a/src/Support/Rat.hs b/src/Support/Rat.hs deleted file mode 100644 index 11e071c..0000000 --- a/src/Support/Rat.hs +++ /dev/null @@ -1,16 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} - -module Support.Rat where - -import GHC.Generics (Generic) - --- We take some model of the dense linear order. The rationals are a natural --- choice. (Note that every countable model is order-isomorphic, so it doesn't --- matter so much in the end.) I wrap it in a newtype, so we will only use the --- Ord instances, and because it's not very nice to work with type synonyms. --- Show instance included for debugging. -newtype Rat = Rat { unRat :: Rational } - deriving (Eq, Ord, Generic) - -instance Show Rat where - show (Rat x) = show x diff --git a/src/Support/Set.hs b/src/Support/Set.hs deleted file mode 100644 index c23647e..0000000 --- a/src/Support/Set.hs +++ /dev/null @@ -1,37 +0,0 @@ -module Support.Set where - -import Data.Set (Set) -import qualified Data.Set as Set - -import Support.Rat - --- Tree-based ordered set -newtype Support = Support { unSupport :: Set Rat } - -size :: Support -> Int -size = Set.size . unSupport - -null :: Support -> Bool -null = Set.null . unSupport - -min :: Support -> Rat -min = Set.findMin . unSupport - -empty :: Support -empty = Support Set.empty - -union :: Support -> Support -> Support -union (Support x) (Support y) = Support (Set.union x y) - -singleton :: Rat -> Support -singleton = Support . Set.singleton - -toList :: Support -> [Rat] -toList = Set.toAscList . unSupport - -fromList, fromAscList, fromDistinctAscList :: [Rat] -> Support -fromList = Support . Set.fromList -fromAscList = Support . Set.fromAscList -fromDistinctAscList = Support . Set.fromDistinctAscList - - diff --git a/test/Bench.hs b/test/Bench.hs index 96264a5..3f30127 100644 --- a/test/Bench.hs +++ b/test/Bench.hs @@ -8,22 +8,23 @@ import Test.Tasty.Bench import EquivariantMap import EquivariantSet import Nominal +import Nominal.Atom import OrbitList (repeatRationals, size) -import Support -instance NFData Rat +instance NFData Atom where + rnf = rwhnf . unAtom (\/) :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a (\/) = EquivariantSet.union -bigset :: (Rat, Rat, Rat, _) -> Bool +bigset :: (Atom, Atom, Atom, _) -> Bool bigset (p, q, r, t) = EquivariantSet.member t s where s1 = singleOrbit ((p, p), p) \/ singleOrbit ((p, p), q) \/ singleOrbit ((p, q), r) s2 = singleOrbit (p, q) \/ singleOrbit (q, r) \/ singleOrbit (r, p) s = EquivariantSet.product s1 s2 -bigmap :: (Rat, Rat, _) -> Maybe (Rat, (Rat, Rat)) +bigmap :: (Atom, Atom, _) -> Maybe (Atom, (Atom, Atom)) bigmap (p, q, t) = EquivariantMap.lookup t m3 where s = EquivariantSet.product (EquivariantSet.singleOrbit (p, q)) (EquivariantSet.singleOrbit (q, p)) @@ -38,18 +39,18 @@ main = defaultMain [ bgroup "bigmap" - [ bench "1 y" $ nf bigmap (Rat 1, Rat 2, (((Rat 1, Rat 23), (Rat 5, Rat 4)), ((Rat 2, Rat 3), (Rat 54, Rat 43)))) -- found - , bench "2 n" $ nf bigmap (Rat 1, Rat 2, (((Rat 1, Rat 23), (Rat 5, Rat 4)), ((Rat 2, Rat 3), (Rat 54, Rat 65)))) -- not found - , bench "3 y" $ nf bigmap (Rat 1, Rat 2, (((Rat 1, Rat 100), (Rat 90, Rat 20)), ((Rat 30, Rat 80), (Rat 70, Rat 65)))) -- found - , bench "4 y" $ nf bigmap (Rat 1, Rat 2, (((Rat 1, Rat 100), (Rat 100, Rat 1)), ((Rat 1, Rat 100), (Rat 100, Rat 1)))) -- found - , bench "5 y" $ nf bigmap (Rat 1, Rat 2, (((Rat 100, Rat 1), (Rat 1, Rat 100)), ((Rat 200, Rat 2), (Rat 2, Rat 200)))) -- found + [ bench "1 y" $ nf bigmap (atom 1, atom 2, (((atom 1, atom 23), (atom 5, atom 4)), ((atom 2, atom 3), (atom 54, atom 43)))) -- found + , bench "2 n" $ nf bigmap (atom 1, atom 2, (((atom 1, atom 23), (atom 5, atom 4)), ((atom 2, atom 3), (atom 54, atom 65)))) -- not found + , bench "3 y" $ nf bigmap (atom 1, atom 2, (((atom 1, atom 100), (atom 90, atom 20)), ((atom 30, atom 80), (atom 70, atom 65)))) -- found + , bench "4 y" $ nf bigmap (atom 1, atom 2, (((atom 1, atom 100), (atom 100, atom 1)), ((atom 1, atom 100), (atom 100, atom 1)))) -- found + , bench "5 y" $ nf bigmap (atom 1, atom 2, (((atom 100, atom 1), (atom 1, atom 100)), ((atom 200, atom 2), (atom 2, atom 200)))) -- found ] , bgroup "bigset" - [ bench "1 y" $ nf bigset (Rat 1, Rat 2, Rat 3, (((Rat 1, Rat 1), Rat 1), (Rat 1, Rat 2))) -- found - , bench "2 y" $ nf bigset (Rat 1, Rat 2, Rat 3, (((Rat 37, Rat 37), Rat 42), (Rat 1, Rat 2))) -- found - , bench "3 n" $ nf bigset (Rat 1, Rat 2, Rat 3, (((Rat 37, Rat 31), Rat 42), (Rat 1, Rat 2))) -- not found - , bench "4 y" $ nf bigset (Rat 1, Rat 2, Rat 3, (((Rat 1, Rat 2), Rat 3), (Rat 5, Rat 4))) -- found + [ bench "1 y" $ nf bigset (atom 1, atom 2, atom 3, (((atom 1, atom 1), atom 1), (atom 1, atom 2))) -- found + , bench "2 y" $ nf bigset (atom 1, atom 2, atom 3, (((atom 37, atom 37), atom 42), (atom 1, atom 2))) -- found + , bench "3 n" $ nf bigset (atom 1, atom 2, atom 3, (((atom 37, atom 31), atom 42), (atom 1, atom 2))) -- not found + , bench "4 y" $ nf bigset (atom 1, atom 2, atom 3, (((atom 1, atom 2), atom 3), (atom 5, atom 4))) -- found ] , bgroup "counting orbits" diff --git a/test/Spec.hs b/test/Spec.hs index 1990c1f..50b2db0 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -5,10 +5,8 @@ import Test.Tasty.HUnit hiding (assert) import Test.Tasty.QuickCheck as QC import Prelude (Eq (..), IO, Int, length, show, (!!), ($), (<>)) -import Nominal (Nominal (..)) +import Nominal import OrbitList (repeatRationals, size) -import Support (Rat (..)) - import SpecMap import SpecPermutable import SpecSet @@ -31,4 +29,4 @@ a000670 = [1, 1, 3, 13, 75, 541, 4683, 47293, 545835, 7087261, 102247563, 162263 -- TODO: Add more quickcheck tests qcTests :: TestTree -qcTests = testGroup "QuickCheck" [QC.testProperty "all atoms in same orbit" $ \p q -> toOrbit (p :: Rat) == toOrbit (q :: Rat)] +qcTests = testGroup "QuickCheck" [QC.testProperty "all atoms in same orbit" $ \p q -> toOrbit (p :: Atom) == toOrbit (q :: Atom)] diff --git a/test/SpecMap.hs b/test/SpecMap.hs index c24da95..d081841 100644 --- a/test/SpecMap.hs +++ b/test/SpecMap.hs @@ -9,8 +9,7 @@ import Prelude (const, ($)) import EquivariantMap import EquivariantSet qualified as EqSet -import Support - +import Nominal (atom) import SpecUtils mapTests :: TestTree @@ -19,25 +18,25 @@ mapTests = testGroup "Map" [unitTests] unitTests :: TestTree unitTests = testCase "Examples" $ do let - p = Rat 1 - q = Rat 2 + p = atom 1 + q = atom 2 s = EqSet.product (EqSet.singleOrbit (p, q)) (EqSet.singleOrbit (q, p)) s2 = EqSet.product s s m1 = fromSet (\(((_, b), (_, d)), (_, (_, h))) -> (b, (d, h))) s2 - assert isJust $ lookup (((Rat 1, Rat 2), (Rat 2, Rat 1)), ((Rat 1, Rat 2), (Rat 3, Rat 2))) m1 - assert isNothing $ lookup (((Rat 1, Rat 2), (Rat 2, Rat 1)), ((Rat 1, Rat 2), (Rat 1, Rat 2))) m1 + assert isJust $ lookup (((atom 1, atom 2), (atom 2, atom 1)), ((atom 1, atom 2), (atom 3, atom 2))) m1 + assert isNothing $ lookup (((atom 1, atom 2), (atom 2, atom 1)), ((atom 1, atom 2), (atom 1, atom 2))) m1 let s3 = EqSet.map (\((a, b), (c, d)) -> ((b, a), (d, c))) s2 m2 = fromSet (\(((_, b), (_, d)), (_, (_, h))) -> (b, (d, h))) s3 - assert isJust $ lookup (((Rat 6, Rat 1), (Rat 1, Rat 5)), ((Rat 4, Rat 1), (Rat 1, Rat 3))) m2 - assert isNothing $ lookup (((Rat 1, Rat 2), (Rat 2, Rat 1)), ((Rat 1, Rat 2), (Rat 4, Rat 2))) m2 + assert isJust $ lookup (((atom 6, atom 1), (atom 1, atom 5)), ((atom 4, atom 1), (atom 1, atom 3))) m2 + assert isNothing $ lookup (((atom 1, atom 2), (atom 2, atom 1)), ((atom 1, atom 2), (atom 4, atom 2))) m2 let m3 = unionWith const m1 m2 - assert isJust $ lookup (((Rat 1, Rat 23), (Rat 5, Rat 4)), ((Rat 2, Rat 3), (Rat 54, Rat 43))) m3 - assert isNothing $ lookup (((Rat 1, Rat 23), (Rat 5, Rat 4)), ((Rat 2, Rat 3), (Rat 54, Rat 65))) m3 - assert isJust $ lookup (((Rat 1, Rat 100), (Rat 90, Rat 20)), ((Rat 30, Rat 80), (Rat 70, Rat 65))) m3 - assert isJust $ lookup (((Rat 1, Rat 100), (Rat 100, Rat 1)), ((Rat 1, Rat 100), (Rat 100, Rat 1))) m3 - assert isJust $ lookup (((Rat 100, Rat 1), (Rat 1, Rat 100)), ((Rat 200, Rat 2), (Rat 2, Rat 200))) m3 + assert isJust $ lookup (((atom 1, atom 23), (atom 5, atom 4)), ((atom 2, atom 3), (atom 54, atom 43))) m3 + assert isNothing $ lookup (((atom 1, atom 23), (atom 5, atom 4)), ((atom 2, atom 3), (atom 54, atom 65))) m3 + assert isJust $ lookup (((atom 1, atom 100), (atom 90, atom 20)), ((atom 30, atom 80), (atom 70, atom 65))) m3 + assert isJust $ lookup (((atom 1, atom 100), (atom 100, atom 1)), ((atom 1, atom 100), (atom 100, atom 1))) m3 + assert isJust $ lookup (((atom 100, atom 1), (atom 1, atom 100)), ((atom 200, atom 2), (atom 2, atom 200))) m3 diff --git a/test/SpecPermutable.hs b/test/SpecPermutable.hs index 8a07208..c8c6564 100644 --- a/test/SpecPermutable.hs +++ b/test/SpecPermutable.hs @@ -7,8 +7,6 @@ import Test.Tasty.HUnit hiding (assert) import Nominal import Permutable -import Support (Rat (..)) - import SpecUtils permutableTests :: TestTree @@ -21,7 +19,7 @@ assocTest n = assert and $ [lhs f g == rhs f g | f <- perms, g <- perms] where - element = fmap (Rat . toRational) $ [1 .. n] + element = fmap atom $ [1 .. n] supp = support element perms = allPermutations supp lhs f g = act (Permuted (compose f g) element) diff --git a/test/SpecSet.hs b/test/SpecSet.hs index eaee1c7..08da0ec 100644 --- a/test/SpecSet.hs +++ b/test/SpecSet.hs @@ -5,8 +5,7 @@ import Test.Tasty.HUnit hiding (assert) import Prelude (id, not, ($)) import EquivariantSet -import Support (Rat (..)) - +import Nominal (atom) import SpecUtils setTests :: TestTree @@ -15,28 +14,28 @@ setTests = testGroup "Set" [unitTests] unitTests :: TestTree unitTests = testCase "Examples" $ do let - p = Rat 1 - q = Rat 2 + p = atom 1 + q = atom 2 s = product (singleOrbit (p, q)) (singleOrbit (q, p)) - assert id $ member ((Rat 1, Rat 2), (Rat 5, Rat 4)) s - assert not $ member ((Rat 5, Rat 2), (Rat 5, Rat 4)) s - assert id $ member ((Rat 1, Rat 2), (Rat 2, Rat 1)) s - assert id $ member ((Rat 3, Rat 4), (Rat 2, Rat 1)) s + assert id $ member ((atom 1, atom 2), (atom 5, atom 4)) s + assert not $ member ((atom 5, atom 2), (atom 5, atom 4)) s + assert id $ member ((atom 1, atom 2), (atom 2, atom 1)) s + assert id $ member ((atom 3, atom 4), (atom 2, atom 1)) s let s2 = product s s - assert id $ member (((Rat 1, Rat 2), (Rat 5, Rat 4)), ((Rat 1, Rat 2), (Rat 5, Rat 4))) s2 - assert id $ member (((Rat 1, Rat 2), (Rat 5, Rat 4)), ((Rat 1, Rat 2), (Rat 5, Rat 1))) s2 - assert id $ member (((Rat 1, Rat 2), (Rat 5, Rat 4)), ((Rat 1, Rat 200), (Rat 5, Rat 1))) s2 - assert id $ member (((Rat 0, Rat 27), (Rat 5, Rat 4)), ((Rat 1, Rat 200), (Rat 5, Rat 1))) s2 - assert not $ member (((Rat 0, Rat 27), (Rat 5, Rat 4)), ((Rat 1, Rat 200), (Rat 5, Rat 5))) s2 + assert id $ member (((atom 1, atom 2), (atom 5, atom 4)), ((atom 1, atom 2), (atom 5, atom 4))) s2 + assert id $ member (((atom 1, atom 2), (atom 5, atom 4)), ((atom 1, atom 2), (atom 5, atom 1))) s2 + assert id $ member (((atom 1, atom 2), (atom 5, atom 4)), ((atom 1, atom 200), (atom 5, atom 1))) s2 + assert id $ member (((atom 0, atom 27), (atom 5, atom 4)), ((atom 1, atom 200), (atom 5, atom 1))) s2 + assert not $ member (((atom 0, atom 27), (atom 5, atom 4)), ((atom 1, atom 200), (atom 5, atom 5))) s2 let s3 = map (\((a, b), (c, d)) -> ((b, a), (d, c))) s2 - assert id $ member (((Rat 5, Rat 4), (Rat 1, Rat 2)), ((Rat 5, Rat 4), (Rat 1, Rat 2))) s3 - assert id $ member (((Rat 2, Rat 1), (Rat 4, Rat 5)), ((Rat 2, Rat 1), (Rat 4, Rat 5))) s3 + assert id $ member (((atom 5, atom 4), (atom 1, atom 2)), ((atom 5, atom 4), (atom 1, atom 2))) s3 + assert id $ member (((atom 2, atom 1), (atom 4, atom 5)), ((atom 2, atom 1), (atom 4, atom 5))) s3 let - r = Rat 3 + r = atom 3 s4 = singleOrbit ((p, p), p) `union` singleOrbit ((p, p), q) `union` singleOrbit ((p, q), r) s5 = singleOrbit (p, q) `union` singleOrbit (q, r) `union` singleOrbit (r, p) @@ -44,7 +43,7 @@ unitTests = testCase "Examples" $ do assert not $ product (singleOrbit p) (singleOrbit p) `isSubsetOf` s5 let s6 = product s4 s5 - assert id $ member (((Rat 1, Rat 1), Rat 1), (Rat 1, Rat 2)) s6 - assert id $ member (((Rat 37, Rat 37), Rat 42), (Rat 1, Rat 2)) s6 - assert not $ member (((Rat 37, Rat 31), Rat 42), (Rat 1, Rat 2)) s6 - assert id $ member (((Rat 1, Rat 2), Rat 3), (Rat 5, Rat 4)) s6 + assert id $ member (((atom 1, atom 1), atom 1), (atom 1, atom 2)) s6 + assert id $ member (((atom 37, atom 37), atom 42), (atom 1, atom 2)) s6 + assert not $ member (((atom 37, atom 31), atom 42), (atom 1, atom 2)) s6 + assert id $ member (((atom 1, atom 2), atom 3), (atom 5, atom 4)) s6 diff --git a/test/SpecUtils.hs b/test/SpecUtils.hs index 0d95fa8..89d357f 100644 --- a/test/SpecUtils.hs +++ b/test/SpecUtils.hs @@ -5,11 +5,11 @@ module SpecUtils where import Test.Tasty.HUnit hiding (assert) import Test.Tasty.QuickCheck as QC -import Support (Rat (..)) +import Nominal.Atom assert :: HasCallStack => (a -> Bool) -> a -> IO () assert f x = assertBool "" (f x) -instance Arbitrary Rat where - arbitrary = Rat <$> arbitrary - shrink (Rat p) = Rat <$> shrink p +instance Arbitrary Atom where + arbitrary = atom <$> arbitrary + shrink (Atom p) = atom <$> shrink p