mirror of
https://github.com/Jaxan/ons-hs.git
synced 2025-07-01 17:17:43 +02:00
Renamed Orbit -> Nominal
This commit is contained in:
Joshua Moerman
parent
7b2ee61978
commit
4a0500ab18
10 changed files with 340 additions and 336 deletions
|
|
@ -17,9 +17,9 @@ library
|
|||
hs-source-dirs: src
|
||||
exposed-modules: EquivariantMap
|
||||
, EquivariantSet
|
||||
, Orbit
|
||||
, Orbit.Class
|
||||
, Orbit.Products
|
||||
, Nominal
|
||||
, Nominal.Class
|
||||
, Nominal.Products
|
||||
, OrbitList
|
||||
, Support
|
||||
, Support.Rat
|
||||
|
|
|
|||
|
|
@ -6,14 +6,12 @@
|
|||
|
||||
module EquivariantMap where
|
||||
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Semigroup (Semigroup)
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
|
||||
import EquivariantSet (EquivariantSet(EqSet))
|
||||
import Orbit
|
||||
import Nominal
|
||||
import Support
|
||||
|
||||
-- TODO: foldable / traversable
|
||||
|
|
@ -27,31 +25,31 @@ import Support
|
|||
-- thing is that we have to store which values are preserved under a map. This
|
||||
-- is done with the list of bit vector. Otherwise, it is an orbit-wise
|
||||
-- representation, just like sets.
|
||||
newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orb k) (Orb v, [Bool]) }
|
||||
newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orbit k) (Orbit v, [Bool]) }
|
||||
|
||||
-- Need undecidableIntances for this
|
||||
deriving instance (Eq (Orb k), Eq (Orb v)) => Eq (EquivariantMap k v)
|
||||
deriving instance (Ord (Orb k), Ord (Orb v)) => Ord (EquivariantMap k v)
|
||||
deriving instance (Show (Orb k), Show (Orb v)) => Show (EquivariantMap k v)
|
||||
deriving instance (Eq (Orbit k), Eq (Orbit v)) => Eq (EquivariantMap k v)
|
||||
deriving instance (Ord (Orbit k), Ord (Orbit v)) => Ord (EquivariantMap k v)
|
||||
deriving instance (Show (Orbit k), Show (Orbit v)) => Show (EquivariantMap k v)
|
||||
|
||||
-- Left biased...
|
||||
deriving instance Ord (Orb k) => Monoid (EquivariantMap k v)
|
||||
deriving instance Ord (Orb k) => Semigroup (EquivariantMap k v)
|
||||
deriving instance Ord (Orbit k) => Monoid (EquivariantMap k v)
|
||||
deriving instance Ord (Orbit k) => Semigroup (EquivariantMap k v)
|
||||
|
||||
-- Helper functions
|
||||
|
||||
mapel :: (Orbit k, Orbit v) => k -> v -> (Orb v, [Bool])
|
||||
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 l [] = replicate (length l) False
|
||||
bv [] l = error "Non-equivariant function"
|
||||
bv [] _ = error "Non-equivariant function"
|
||||
bv (x:xs) (y:ys) = case compare x y of
|
||||
LT -> False : bv xs (y:ys)
|
||||
EQ -> True : bv xs ys
|
||||
GT -> error "Non-equivariant function"
|
||||
|
||||
mapelInv :: (Orbit k, Orbit v) => k -> (Orb v, [Bool]) -> v
|
||||
mapelInv :: (Nominal k, Nominal v) => k -> (Orbit v, [Bool]) -> v
|
||||
mapelInv x (oy, bv) = getElement oy (Support.fromDistinctAscList . fmap fst . Prelude.filter snd $ zip (Support.toList (support x)) bv)
|
||||
|
||||
|
||||
|
|
@ -60,10 +58,10 @@ mapelInv x (oy, bv) = getElement oy (Support.fromDistinctAscList . fmap fst . Pr
|
|||
null :: EquivariantMap k v -> Bool
|
||||
null (EqMap m) = Map.null m
|
||||
|
||||
member :: (Orbit k, Ord (Orb k)) => k -> EquivariantMap k v -> Bool
|
||||
member :: (Nominal k, Ord (Orbit k)) => k -> EquivariantMap k v -> Bool
|
||||
member x (EqMap m) = Map.member (toOrbit x) m
|
||||
|
||||
lookup :: (Orbit k, Ord (Orb k), Orbit v) => k -> EquivariantMap k v -> Maybe v
|
||||
lookup :: (Nominal k, Ord (Orbit k), Nominal v) => k -> EquivariantMap k v -> Maybe v
|
||||
lookup x (EqMap m) = mapelInv x <$> Map.lookup (toOrbit x) m
|
||||
|
||||
|
||||
|
|
@ -72,13 +70,13 @@ lookup x (EqMap m) = mapelInv x <$> Map.lookup (toOrbit x) m
|
|||
empty :: EquivariantMap k v
|
||||
empty = EqMap Map.empty
|
||||
|
||||
singleton :: (Orbit k, Orbit v) => k -> v -> EquivariantMap k v
|
||||
singleton :: (Nominal k, Nominal v) => k -> v -> EquivariantMap k v
|
||||
singleton k v = EqMap (Map.singleton (toOrbit k) (mapel k v))
|
||||
|
||||
insert :: (Orbit k, Orbit v, Ord (Orb k)) => k -> v -> EquivariantMap k v -> EquivariantMap k v
|
||||
insert :: (Nominal k, Nominal v, Ord (Orbit k)) => k -> v -> EquivariantMap k v -> EquivariantMap k v
|
||||
insert k v (EqMap m) = EqMap (Map.insert (toOrbit k) (mapel k v) m)
|
||||
|
||||
delete :: (Orbit k, Ord (Orb k)) => k -> EquivariantMap k v -> EquivariantMap k v
|
||||
delete :: (Nominal k, Ord (Orbit k)) => k -> EquivariantMap k v -> EquivariantMap k v
|
||||
delete k (EqMap m) = EqMap (Map.delete (toOrbit k) m)
|
||||
|
||||
|
||||
|
|
@ -87,22 +85,22 @@ delete k (EqMap m) = EqMap (Map.delete (toOrbit k) m)
|
|||
-- Can be done with just Map.unionWith and without getElementE but is a bit
|
||||
-- harder (probably easier). Also true for related functions
|
||||
-- op should be equivariant!
|
||||
unionWith :: forall k v. (Orbit k, Orbit v, Ord (Orb k)) => (v -> v -> v) -> EquivariantMap k v -> EquivariantMap k v -> EquivariantMap k v
|
||||
unionWith :: forall k v. (Nominal k, Nominal v, Ord (Orbit k)) => (v -> v -> v) -> EquivariantMap k v -> EquivariantMap k v -> EquivariantMap k v
|
||||
unionWith op (EqMap m1) (EqMap m2) = EqMap (Map.unionWithKey opl m1 m2)
|
||||
where opl ko p1 p2 = let k = getElementE ko :: k in mapel k (mapelInv k p1 `op` mapelInv k p2)
|
||||
|
||||
intersectionWith :: forall k v1 v2 v3. (Orbit k, Orbit v1, Orbit v2, Orbit v3, Ord (Orb k)) => (v1 -> v2 -> v3) -> EquivariantMap k v1 -> EquivariantMap k v2 -> EquivariantMap k v3
|
||||
intersectionWith :: forall k v1 v2 v3. (Nominal k, Nominal v1, Nominal v2, Nominal v3, Ord (Orbit k)) => (v1 -> v2 -> v3) -> EquivariantMap k v1 -> EquivariantMap k v2 -> EquivariantMap k v3
|
||||
intersectionWith op (EqMap m1) (EqMap m2) = EqMap (Map.intersectionWithKey opl m1 m2)
|
||||
where opl ko p1 p2 = let k = getElementE ko :: k in mapel k (mapelInv k p1 `op` mapelInv k p2)
|
||||
|
||||
-- Traversal
|
||||
|
||||
-- f should be equivariant
|
||||
map :: forall k v1 v2. (Orbit k, Orbit v1, Orbit v2) => (v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2
|
||||
map :: forall k v1 v2. (Nominal k, Nominal v1, Nominal v2) => (v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2
|
||||
map f (EqMap m) = EqMap (Map.mapWithKey f2 m)
|
||||
where f2 ko p1 = let k = getElementE ko :: k in mapel k (f $ mapelInv k p1)
|
||||
|
||||
mapWithKey :: (Orbit k, Orbit v1, Orbit v2) => (k -> v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2
|
||||
mapWithKey :: (Nominal k, Nominal v1, Nominal v2) => (k -> v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2
|
||||
mapWithKey f (EqMap m) = EqMap (Map.mapWithKey f2 m)
|
||||
where f2 ko p1 = let k = getElementE ko in mapel k (f k $ mapelInv k p1)
|
||||
|
||||
|
|
@ -111,13 +109,13 @@ mapWithKey f (EqMap m) = EqMap (Map.mapWithKey f2 m)
|
|||
keysSet :: EquivariantMap k v -> EquivariantSet k
|
||||
keysSet (EqMap m) = EqSet (Map.keysSet m)
|
||||
|
||||
fromSet :: (Orbit k, Orbit v) => (k -> v) -> EquivariantSet k -> EquivariantMap k v
|
||||
fromSet :: (Nominal k, Nominal v) => (k -> v) -> EquivariantSet k -> EquivariantMap k v
|
||||
fromSet f (EqSet s) = EqMap (Map.fromSet f2 s)
|
||||
where f2 ko = let k = getElementE ko in mapel k (f k)
|
||||
|
||||
|
||||
-- Filter
|
||||
|
||||
filter :: forall k v. (Orbit k, Orbit v) => (v -> Bool) -> EquivariantMap k v -> EquivariantMap k v
|
||||
filter :: forall k v. (Nominal k, Nominal v) => (v -> Bool) -> EquivariantMap k v -> EquivariantMap k v
|
||||
filter p (EqMap m) = EqMap (Map.filterWithKey p2 m)
|
||||
where p2 ko pr = let k = getElementE ko :: k in p $ mapelInv k pr
|
||||
|
|
|
|||
|
|
@ -13,7 +13,8 @@ import Data.Set (Set)
|
|||
import qualified Data.Set as Set
|
||||
import Prelude hiding (map, product)
|
||||
|
||||
import Orbit
|
||||
import Nominal
|
||||
import OrbitList (OrbitList(..))
|
||||
|
||||
|
||||
-- Given a nominal type, we can construct equivariant sets. These simply use a
|
||||
|
|
@ -22,20 +23,20 @@ import Orbit
|
|||
-- will always work directly with elements. This way we model infinite sets.
|
||||
-- Note that functions such as toList do not return an ordered list since the
|
||||
-- representatives are chosen arbitrarily.
|
||||
newtype EquivariantSet a = EqSet { unEqSet :: Set (Orb a) }
|
||||
newtype EquivariantSet a = EqSet { unEqSet :: Set (Orbit a) }
|
||||
|
||||
-- Need undecidableIntances for this
|
||||
deriving instance Eq (Orb a) => Eq (EquivariantSet a)
|
||||
deriving instance Ord (Orb a) => Ord (EquivariantSet a)
|
||||
deriving instance Show (Orb a) => Show (EquivariantSet a)
|
||||
deriving instance Eq (Orbit a) => Eq (EquivariantSet a)
|
||||
deriving instance Ord (Orbit a) => Ord (EquivariantSet a)
|
||||
deriving instance Show (Orbit a) => Show (EquivariantSet a)
|
||||
|
||||
-- For these we rely on the instances of Set
|
||||
-- It defines the join semi-lattice structure
|
||||
deriving instance Ord (Orb a) => Monoid (EquivariantSet a)
|
||||
deriving instance Ord (Orb a) => Semigroup (EquivariantSet a)
|
||||
deriving instance Ord (Orbit a) => Monoid (EquivariantSet a)
|
||||
deriving instance Ord (Orbit a) => Semigroup (EquivariantSet a)
|
||||
|
||||
-- This action is trivial, since equivariant sets are equivariant
|
||||
deriving via (Trivial (EquivariantSet a)) instance Orbit (EquivariantSet a)
|
||||
deriving via (Trivial (EquivariantSet a)) instance Nominal (EquivariantSet a)
|
||||
|
||||
|
||||
-- Query
|
||||
|
|
@ -46,10 +47,10 @@ null = Set.null . unEqSet
|
|||
orbits :: EquivariantSet a -> Int
|
||||
orbits = Set.size . unEqSet
|
||||
|
||||
member :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> Bool
|
||||
member :: (Nominal a, Ord (Orbit a)) => a -> EquivariantSet a -> Bool
|
||||
member a = Set.member (toOrbit a) . unEqSet
|
||||
|
||||
isSubsetOf :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> Bool
|
||||
isSubsetOf :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> Bool
|
||||
isSubsetOf (EqSet s1) (EqSet s2) = Set.isSubsetOf s1 s2
|
||||
|
||||
|
||||
|
|
@ -58,86 +59,86 @@ isSubsetOf (EqSet s1) (EqSet s2) = Set.isSubsetOf s1 s2
|
|||
empty :: EquivariantSet a
|
||||
empty = EqSet Set.empty
|
||||
|
||||
singleOrbit :: Orbit a => a -> EquivariantSet a
|
||||
singleOrbit :: Nominal a => a -> EquivariantSet a
|
||||
singleOrbit = EqSet . Set.singleton . toOrbit
|
||||
|
||||
-- Insert whole orbit of a
|
||||
insert :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> EquivariantSet a
|
||||
insert :: (Nominal a, Ord (Orbit a)) => a -> EquivariantSet a -> EquivariantSet a
|
||||
insert a = EqSet . Set.insert (toOrbit a) . unEqSet
|
||||
|
||||
-- Deletes whole orbit of a
|
||||
delete :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> EquivariantSet a
|
||||
delete :: (Nominal a, Ord (Orbit a)) => a -> EquivariantSet a -> EquivariantSet a
|
||||
delete a = EqSet . Set.delete (toOrbit a) . unEqSet
|
||||
|
||||
|
||||
-- Combine
|
||||
|
||||
union :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
union :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
union a b = EqSet $ Set.union (unEqSet a) (unEqSet b)
|
||||
|
||||
-- Not symmetric, but A \ B
|
||||
difference :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
difference :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
difference a b = EqSet $ Set.difference (unEqSet a) (unEqSet b)
|
||||
|
||||
intersection :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
intersection :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
intersection a b = EqSet $ Set.intersection (unEqSet a) (unEqSet b)
|
||||
|
||||
-- Cartesian product. This is a non trivial thing and relies on the
|
||||
-- ordering of Orbit.product.
|
||||
product :: forall a b. (Orbit a, Orbit b) => EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b)
|
||||
product :: forall a b. (Nominal a, Nominal b) => EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b)
|
||||
product (EqSet sa) (EqSet sb) = EqSet . Set.fromDistinctAscList . concat
|
||||
$ Orbit.product (Proxy @a) (Proxy @b) <$> Set.toAscList sa <*> Set.toAscList sb
|
||||
$ Nominal.product (Proxy @a) (Proxy @b) <$> Set.toAscList sa <*> Set.toAscList sb
|
||||
|
||||
-- Cartesian product followed by a function (f should be equivariant)
|
||||
productWith :: (Orbit a, Orbit b, Orbit c, Ord (Orb c)) => (a -> b -> c) -> EquivariantSet a -> EquivariantSet b -> EquivariantSet c
|
||||
productWith :: (Nominal a, Nominal b, Nominal c, Ord (Orbit c)) => (a -> b -> c) -> EquivariantSet a -> EquivariantSet b -> EquivariantSet c
|
||||
productWith f as bs = map (uncurry f) $ EquivariantSet.product as bs
|
||||
|
||||
|
||||
-- Filter
|
||||
|
||||
-- f should be equivariant
|
||||
filter :: Orbit a => (a -> Bool) -> EquivariantSet a -> EquivariantSet a
|
||||
filter :: Nominal a => (a -> Bool) -> EquivariantSet a -> EquivariantSet a
|
||||
filter f (EqSet s) = EqSet . Set.filter (f . getElementE) $ s
|
||||
|
||||
-- f should be equivariant
|
||||
partition :: Orbit a => (a -> Bool) -> EquivariantSet a -> (EquivariantSet a, EquivariantSet a)
|
||||
partition :: Nominal a => (a -> Bool) -> EquivariantSet a -> (EquivariantSet a, EquivariantSet a)
|
||||
partition f (EqSet s) = both EqSet . Set.partition (f . getElementE) $ s
|
||||
where both f (a, b) = (f a, f b)
|
||||
where both g (a, b) = (g a, g b)
|
||||
|
||||
|
||||
-- Map
|
||||
|
||||
-- precondition: f is equivariant
|
||||
-- Note that f may change the ordering
|
||||
map :: (Orbit a, Orbit b, Ord (Orb b)) => (a -> b) -> EquivariantSet a -> EquivariantSet b
|
||||
map :: (Nominal a, Nominal b, Ord (Orbit b)) => (a -> b) -> EquivariantSet a -> EquivariantSet b
|
||||
map f = EqSet . Set.map (omap f) . unEqSet
|
||||
|
||||
-- precondition: f quivariant and preserves order on the orbits.
|
||||
-- This means you should know the representation to use it well
|
||||
mapMonotonic :: (Orbit a, Orbit b) => (a -> b) -> EquivariantSet a -> EquivariantSet b
|
||||
mapMonotonic :: (Nominal a, Nominal b) => (a -> b) -> EquivariantSet a -> EquivariantSet b
|
||||
mapMonotonic f = EqSet . Set.mapMonotonic (omap f) . unEqSet
|
||||
|
||||
|
||||
-- Folds
|
||||
|
||||
-- I am not sure about the preconditions for folds
|
||||
foldr :: Orbit a => (a -> b -> b) -> b -> EquivariantSet a -> b
|
||||
foldr :: Nominal a => (a -> b -> b) -> b -> EquivariantSet a -> b
|
||||
foldr f b = Set.foldr (f . getElementE) b . unEqSet
|
||||
|
||||
foldl :: Orbit a => (b -> a -> b) -> b -> EquivariantSet a -> b
|
||||
foldl f b = Set.foldl (\b -> f b . getElementE) b . unEqSet
|
||||
foldl :: Nominal a => (b -> a -> b) -> b -> EquivariantSet a -> b
|
||||
foldl f b = Set.foldl (\acc -> f acc . getElementE) b . unEqSet
|
||||
|
||||
|
||||
-- Conversion
|
||||
|
||||
toList :: Orbit a => EquivariantSet a -> [a]
|
||||
toList :: Nominal a => EquivariantSet a -> [a]
|
||||
toList = fmap getElementE . Set.toList . unEqSet
|
||||
|
||||
fromList :: (Orbit a, Ord (Orb a)) => [a] -> EquivariantSet a
|
||||
fromList :: (Nominal a, Ord (Orbit a)) => [a] -> EquivariantSet a
|
||||
fromList = EqSet . Set.fromList . fmap toOrbit
|
||||
|
||||
toOrbitList :: EquivariantSet a -> [Orb a]
|
||||
toOrbitList = Set.toList . unEqSet
|
||||
toOrbitList :: EquivariantSet a -> OrbitList a
|
||||
toOrbitList = OrbitList . Set.toList . unEqSet
|
||||
|
||||
fromOrbitList :: Ord (Orb a) => [Orb a] -> EquivariantSet a
|
||||
fromOrbitList = EqSet . Set.fromList
|
||||
fromOrbitList :: Ord (Orbit a) => OrbitList a -> EquivariantSet a
|
||||
fromOrbitList = EqSet . Set.fromList . unOrbitList
|
||||
|
|
|
|||
43
src/Nominal.hs
Normal file
43
src/Nominal.hs
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DerivingVia #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
module Nominal
|
||||
( module Nominal
|
||||
, module Nominal.Class
|
||||
) where
|
||||
|
||||
import Data.Proxy
|
||||
|
||||
import Nominal.Products
|
||||
import Nominal.Class
|
||||
import Support (def)
|
||||
|
||||
|
||||
-- We can get 'default' values, if we don't care about the support.
|
||||
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
|
||||
omap :: (Nominal a, Nominal b) => (a -> b) -> Orbit a -> Orbit b
|
||||
omap f = toOrbit . f . getElementE
|
||||
|
||||
-- Enumerate all orbits in a product A x B. In lexicographical order!
|
||||
product :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)]
|
||||
product pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> prodStrings (index pa oa) (index pb ob)
|
||||
|
||||
-- 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 pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> sepProdStrings (index pa oa) (index pb ob)
|
||||
|
||||
-- "Left product": A |x 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 pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> rincProdStrings (index pa oa) (index pb ob)
|
||||
|
||||
{-# INLINABLE product #-}
|
||||
{-# INLINABLE separatedProduct #-}
|
||||
{-# INLINABLE leftProduct #-}
|
||||
|
||||
223
src/Nominal/Class.hs
Normal file
223
src/Nominal/Class.hs
Normal file
|
|
@ -0,0 +1,223 @@
|
|||
{-# LANGUAGE DerivingVia #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
module Nominal.Class
|
||||
( Nominal(..) -- typeclass
|
||||
, Trivial(..) -- newtype wrapper for deriving instances
|
||||
, Generic(..) -- newtype wrapper for deriving instances
|
||||
, OrbPair(..) -- need to export?
|
||||
, OrbRec(..) -- need to export?
|
||||
) where
|
||||
|
||||
import Data.Void
|
||||
import Data.Proxy (Proxy(..))
|
||||
import GHC.Generics hiding (Generic)
|
||||
import qualified GHC.Generics as GHC (Generic)
|
||||
|
||||
import Support
|
||||
|
||||
|
||||
-- This is the main meat of the package. The Orbit typeclass, it gives us ways
|
||||
-- to manipulate nominal elements in sets and maps. The type class has
|
||||
-- associated data to represent an orbit of type a. This is often much easier
|
||||
-- than the type a itself. For example, all orbits of Rat are equal.
|
||||
-- Furthermore, we provide means to go back and forth between elements and
|
||||
-- orbits, and we get to know their support size. For many manipulations we
|
||||
-- need an Ord instance on the associated data type, this can often be
|
||||
-- implemented, even when the type 'a' does not have an Ord instance.
|
||||
--
|
||||
-- Laws / conditions:
|
||||
-- * index . toOrbit == size . support
|
||||
-- * getElement o s is defined if index o == Set.size s
|
||||
class Nominal a where
|
||||
type Orbit a :: *
|
||||
toOrbit :: a -> Orbit a
|
||||
support :: a -> Support
|
||||
getElement :: Orbit a -> Support -> a
|
||||
index :: Proxy a -> Orbit a -> Int
|
||||
|
||||
|
||||
-- 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 = ()
|
||||
toOrbit _ = ()
|
||||
support r = Support.singleton r
|
||||
getElement _ s = Support.min s
|
||||
index _ _ = 1
|
||||
|
||||
|
||||
-- Supports themselves are nominal. Note that this is a very important instance
|
||||
-- as all other instances can reduce to this one (and perhaps the one for
|
||||
-- products). 'Abstract types' in the original ONS library can be represented
|
||||
-- directly as T = (Trivial Int, Support). The orbit of a given support is
|
||||
-- completely specified by an integer.
|
||||
instance Nominal Support where
|
||||
type Orbit Support = Int
|
||||
toOrbit s = Support.size s
|
||||
support s = s
|
||||
getElement _ s = s
|
||||
index _ n = n
|
||||
|
||||
|
||||
-- Two general ways for deriving instances are provided:
|
||||
-- 1. A trivial instance, where the group action is trivial. This means that
|
||||
-- each value is its own orbit and is supported by the empty set.
|
||||
-- 2. A generic instance, this uses the GHC.Generis machinery. This will
|
||||
-- derive ``the right'' instance based on the algebraic data type.
|
||||
-- Neither of them is a default, so they should be derived using DerivingVia.
|
||||
-- (Available from GHC 8.6.1.) Example of both:
|
||||
-- deriving via (Trivial Bool) instance Orbit Bool
|
||||
-- deriving via (Generic (a, b)) instance (Orbit a, Orbit b) => Orbit (a, b)
|
||||
|
||||
-- For the trivial action, each element is its own orbit and is supported
|
||||
-- by the empty set.
|
||||
newtype Trivial a = Trivial { unTrivial :: a }
|
||||
instance Nominal (Trivial a) where
|
||||
type Orbit (Trivial a) = a
|
||||
toOrbit (Trivial a) = a
|
||||
support _ = Support.empty
|
||||
getElement a _ = Trivial a
|
||||
index _ _ = 0
|
||||
|
||||
|
||||
-- We can now define trivial instances for some basic types. (Some of these
|
||||
-- could equivalently be derived with generics.)
|
||||
deriving via (Trivial Void) instance Nominal Void
|
||||
deriving via (Trivial ()) instance Nominal ()
|
||||
deriving via (Trivial Bool) instance Nominal Bool
|
||||
deriving via (Trivial Char) instance Nominal Char
|
||||
deriving via (Trivial Ordering) instance Nominal Ordering
|
||||
|
||||
|
||||
-- The generic instance unfolds the algebraic data type in sums and products,
|
||||
-- these have their own instances defined below.
|
||||
newtype Generic a = Generic { unGeneric :: a }
|
||||
instance (GHC.Generic a, GNominal (Rep a)) => Nominal (Generic a) where
|
||||
type Orbit (Generic a) = GOrbit (Rep a)
|
||||
toOrbit = gtoOrbit . from . unGeneric
|
||||
support = gsupport . from . unGeneric
|
||||
getElement o s = Generic (to (ggetElement o s))
|
||||
index _ = gindex (Proxy :: Proxy (Rep a))
|
||||
|
||||
|
||||
-- Some instances we can derive via generics
|
||||
deriving via (Generic (a, b)) instance (Nominal a, Nominal b) => Nominal (a, b)
|
||||
deriving via (Generic (a, b, c)) instance (Nominal a, Nominal b, Nominal c) => Nominal (a, b, c)
|
||||
deriving via (Generic (a, b, c, d)) instance (Nominal a, Nominal b, Nominal c, Nominal d) => Nominal (a, b, c, d)
|
||||
|
||||
deriving via (Generic (Either a b)) instance (Nominal a, Nominal b) => Nominal (Either a b)
|
||||
|
||||
deriving via (Generic [a]) instance Nominal a => Nominal [a]
|
||||
deriving via (Generic (Maybe a)) instance Nominal a => Nominal (Maybe a)
|
||||
|
||||
|
||||
-- Generic class, so that custom data types can be derived
|
||||
class GNominal f where
|
||||
type GOrbit f :: *
|
||||
gtoOrbit :: f a -> GOrbit f
|
||||
gsupport :: f a -> Support
|
||||
ggetElement :: GOrbit f -> Support -> f a
|
||||
gindex :: Proxy f -> GOrbit f -> Int
|
||||
|
||||
|
||||
-- Instance for the Void type
|
||||
instance GNominal V1 where
|
||||
type GOrbit V1 = Void
|
||||
gtoOrbit _ = undefined
|
||||
gsupport _ = empty
|
||||
ggetElement _ _ = undefined
|
||||
gindex _ _ = 0
|
||||
|
||||
|
||||
-- Instance for the Uni type
|
||||
instance GNominal U1 where
|
||||
type GOrbit U1 = ()
|
||||
gtoOrbit _ = ()
|
||||
gsupport _ = empty
|
||||
ggetElement _ _ = U1
|
||||
gindex _ _ = 0
|
||||
|
||||
|
||||
-- Disjoint unions are easy: just work on either side.
|
||||
instance (GNominal f, GNominal g) => GNominal (f :+: g) where
|
||||
type GOrbit (f :+: g) = Either (GOrbit f) (GOrbit g)
|
||||
gtoOrbit (L1 a) = Left (gtoOrbit a)
|
||||
gtoOrbit (R1 b) = Right (gtoOrbit b)
|
||||
gsupport (L1 a) = gsupport a
|
||||
gsupport (R1 b) = gsupport b
|
||||
ggetElement (Left oa) s = L1 (ggetElement oa s)
|
||||
ggetElement (Right ob) s = R1 (ggetElement ob s)
|
||||
gindex proxy (Left oa) = gindex (left proxy) oa where
|
||||
left :: proxy (f :+: g) -> Proxy f
|
||||
left _ = Proxy
|
||||
gindex proxy (Right ob) = gindex (right proxy) ob where
|
||||
right :: proxy (f :+: g) -> Proxy g
|
||||
right _ = Proxy
|
||||
|
||||
|
||||
-- The cartesian product is a non-trivial instance. We represent orbits in a
|
||||
-- product as described inthe paper: with two orbits, and how the match. The
|
||||
-- matchings can be given as strings, which can be easily enumerated, in order
|
||||
-- to enumerate the whole product.
|
||||
instance (GNominal f, GNominal g) => GNominal (f :*: g) where
|
||||
type GOrbit (f :*: g) = OrbPair (GOrbit f) (GOrbit g)
|
||||
gtoOrbit ~(a :*: b) = OrbPair (gtoOrbit a) (gtoOrbit b) (bla sa sb)
|
||||
where
|
||||
sa = toList $ gsupport a
|
||||
sb = toList $ gsupport b
|
||||
bla [] ys = fmap (const GT) ys
|
||||
bla xs [] = fmap (const LT) xs
|
||||
bla (x:xs) (y:ys) = case compare x y of
|
||||
LT -> LT : (bla xs (y:ys))
|
||||
EQ -> EQ : (bla xs ys)
|
||||
GT -> GT : (bla (x:xs) ys)
|
||||
gsupport ~(a :*: b) = (gsupport a) `union` (gsupport b)
|
||||
ggetElement (OrbPair oa ob l) s = (ggetElement oa $ toSet ls) :*: (ggetElement ob $ toSet rs)
|
||||
where
|
||||
~(ls, rs) = partitionOrd fst . zip l . toList $ s
|
||||
toSet = fromDistinctAscList . fmap snd
|
||||
gindex _ (OrbPair _ _ l) = length l
|
||||
|
||||
data OrbPair a b = OrbPair !a !b ![Ordering]
|
||||
deriving (Eq, Ord, Show, GHC.Generic)
|
||||
|
||||
-- Could be in prelude or some other general purpose lib
|
||||
partitionOrd :: (a -> Ordering) -> [a] -> ([a], [a])
|
||||
partitionOrd p xs = foldr (selectOrd p) ([], []) xs
|
||||
|
||||
selectOrd :: (a -> Ordering) -> a -> ([a], [a]) -> ([a], [a])
|
||||
selectOrd f x ~(ls, rs) = case f x of
|
||||
LT -> (x : ls, rs)
|
||||
EQ -> (x : ls, x : rs)
|
||||
GT -> (ls, x : rs)
|
||||
|
||||
|
||||
instance Nominal a => GNominal (K1 c a) where
|
||||
-- Cannot use (Orb a) here, that may lead to a recursive type
|
||||
-- So we use the type OrbRec a instead (which uses Orb a one step later).
|
||||
type GOrbit (K1 c a) = OrbRec a
|
||||
gtoOrbit (K1 x) = OrbRec (toOrbit x)
|
||||
gsupport (K1 x) = support x
|
||||
ggetElement (OrbRec x) s = K1 $ getElement x s
|
||||
gindex _ (OrbRec o) = index (Proxy :: Proxy a) o
|
||||
|
||||
newtype OrbRec a = OrbRec (Orbit a)
|
||||
deriving GHC.Generic
|
||||
deriving instance Eq (Orbit a) => Eq (OrbRec a)
|
||||
deriving instance Ord (Orbit a) => Ord (OrbRec a)
|
||||
deriving instance Show (Orbit a) => Show (OrbRec a)
|
||||
|
||||
|
||||
instance GNominal f => GNominal (M1 i c f) where
|
||||
type GOrbit (M1 i c f) = GOrbit f
|
||||
gtoOrbit (M1 x) = gtoOrbit x
|
||||
gsupport (M1 x) = gsupport x
|
||||
ggetElement x s = M1 $ ggetElement x s
|
||||
gindex _ o = gindex (Proxy :: Proxy f) o
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
module Orbit.Products where
|
||||
module Nominal.Products where
|
||||
|
||||
import Control.Applicative
|
||||
import Data.MemoTrie
|
||||
78
src/Orbit.hs
78
src/Orbit.hs
|
|
@ -1,78 +0,0 @@
|
|||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
|
||||
module Orbit
|
||||
( module Orbit
|
||||
, module Orbit.Class
|
||||
) where
|
||||
|
||||
import Data.Proxy
|
||||
|
||||
import Support (Support, Rat(..))
|
||||
import qualified Support
|
||||
|
||||
import Orbit.Products
|
||||
import Orbit.Class
|
||||
|
||||
|
||||
-- We can get 'default' values, if we don't care about the support.
|
||||
getElementE :: forall a. Orbit a => Orb a -> a
|
||||
getElementE orb = getElement orb (Support.def (index (Proxy :: Proxy a) orb))
|
||||
|
||||
-- We can `map` orbits to orbits for equivariant functions
|
||||
omap :: (Orbit a, Orbit b) => (a -> b) -> Orb a -> Orb b
|
||||
omap f = toOrbit . f . getElementE
|
||||
|
||||
-- We can construct orbits from rational numbers. There is exactly one orbit,
|
||||
-- so this can be represented by the unit type.
|
||||
instance Orbit Rat where
|
||||
type Orb Rat = ()
|
||||
toOrbit _ = ()
|
||||
support r = Support.singleton r
|
||||
getElement _ s = Support.min s
|
||||
index _ _ = 1
|
||||
|
||||
|
||||
-- Supports themselves are nominal. Note that this is a very important instance
|
||||
-- as all other instances can reduce to this one (and perhaps the one for
|
||||
-- products). 'Abstract types' in the original ONS library can be represented
|
||||
-- directly as T = (Trivial Int, Support). The orbit of a given support is
|
||||
-- completely specified by an integer.
|
||||
instance Orbit Support where
|
||||
type Orb Support = Int
|
||||
toOrbit s = Support.size s
|
||||
support s = s
|
||||
getElement _ s = s
|
||||
index _ n = n
|
||||
|
||||
|
||||
-- Some instances we can derive via generics
|
||||
deriving instance (Orbit a, Orbit b) => Orbit (Either a b)
|
||||
|
||||
deriving instance Orbit ()
|
||||
deriving instance (Orbit a, Orbit b) => Orbit (a, b)
|
||||
deriving instance (Orbit a, Orbit b, Orbit c) => Orbit (a, b, c)
|
||||
deriving instance (Orbit a, Orbit b, Orbit c, Orbit d) => Orbit (a, b, c, d)
|
||||
|
||||
deriving instance Orbit a => Orbit [a]
|
||||
deriving instance Orbit a => Orbit (Maybe a)
|
||||
|
||||
|
||||
-- Enumerate all orbits in a product A x B. In lexicographical order!
|
||||
product :: (Orbit a, Orbit b) => Proxy a -> Proxy b -> Orb a -> Orb b -> [Orb (a,b)]
|
||||
product pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> prodStrings (index pa oa) (index pb ob)
|
||||
|
||||
-- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.}
|
||||
separatedProduct :: (Orbit a, Orbit b) => Proxy a -> Proxy b -> Orb a -> Orb b -> [Orb (a,b)]
|
||||
separatedProduct pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> sepProdStrings (index pa oa) (index pb ob)
|
||||
|
||||
-- "Left product": A |x B = { (a,b) | C supports a => C supports b }
|
||||
leftProduct :: (Orbit a, Orbit b) => Proxy a -> Proxy b -> Orb a -> Orb b -> [Orb (a,b)]
|
||||
leftProduct pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> rincProdStrings (index pa oa) (index pb ob)
|
||||
|
||||
{-# INLINABLE product #-}
|
||||
{-# INLINABLE separatedProduct #-}
|
||||
{-# INLINABLE leftProduct #-}
|
||||
|
||||
|
|
@ -1,183 +0,0 @@
|
|||
{-# LANGUAGE DerivingVia #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE DefaultSignatures #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
module Orbit.Class where
|
||||
|
||||
import Data.Void
|
||||
import Data.Proxy (Proxy(..))
|
||||
import GHC.Generics
|
||||
|
||||
import Support
|
||||
|
||||
-- This is the main meat of the package. The Orbit typeclass, it gives us ways
|
||||
-- to manipulate nominal elements in sets and maps. The type class has
|
||||
-- associated data to represent an orbit of type a. This is often much easier
|
||||
-- than the type a itself. For example, all orbits of Rat are equal.
|
||||
-- Furthermore, we provide means to go back and forth between elements and
|
||||
-- orbits, and we get to know their support size. For many manipulations we
|
||||
-- need an Ord instance on the associated data type, this can often be
|
||||
-- implemented, even when the type 'a' does not have an Ord instance.
|
||||
--
|
||||
-- Laws / conditions:
|
||||
-- * index . toOrbit == size . support
|
||||
-- * getElement o s is defined if index o == Set.size s
|
||||
class Orbit a where
|
||||
type Orb a :: *
|
||||
toOrbit :: a -> Orb a
|
||||
support :: a -> Support
|
||||
getElement :: Orb a -> Support -> a
|
||||
index :: Proxy a -> Orb a -> Int
|
||||
|
||||
-- We provide default implementations for generic types
|
||||
-- This enables us to derive Orbit instances by the Haskell compiler
|
||||
-- default Orb a :: (Generic a, GOrbit (Rep a)) => *
|
||||
type Orb a = GOrb (Rep a)
|
||||
|
||||
default toOrbit :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => a -> Orb a
|
||||
toOrbit = gtoOrbit . from
|
||||
|
||||
default support :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => a -> Support
|
||||
support = gsupport . from
|
||||
|
||||
default getElement :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => Orb a -> Support -> a
|
||||
getElement o s = to (ggetElement o s)
|
||||
|
||||
default index :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => Proxy a -> Orb a -> Int
|
||||
index _ = gindex (Proxy :: Proxy (Rep a))
|
||||
|
||||
{-# INLINABLE toOrbit #-}
|
||||
{-# INLINABLE support #-}
|
||||
{-# INLINABLE getElement #-}
|
||||
{-# INLINABLE index #-}
|
||||
|
||||
|
||||
-- Data structure for the discrete nominal sets with a trivial action.
|
||||
newtype Trivial a = Trivial { unTrivial :: a }
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
-- For the trivial action, each element is its own orbit and is supported
|
||||
-- by the empty set.
|
||||
instance Orbit (Trivial a) where
|
||||
type Orb (Trivial a) = a
|
||||
toOrbit (Trivial a) = a
|
||||
support _ = Support.empty
|
||||
getElement a _ = Trivial a
|
||||
index _ _ = 0
|
||||
|
||||
|
||||
-- We can now define trivial instances for some basic types.
|
||||
-- This uses a new Haskell extension (ghc 8.6.1)
|
||||
deriving via (Trivial Bool) instance Orbit Bool
|
||||
|
||||
|
||||
|
||||
-- Generic class, so that custom data types can be derived
|
||||
class GOrbit f where
|
||||
type GOrb f :: *
|
||||
gtoOrbit :: f a -> GOrb f
|
||||
gsupport :: f a -> Support
|
||||
ggetElement :: GOrb f -> Support -> f a
|
||||
gindex :: Proxy f -> GOrb f -> Int
|
||||
|
||||
|
||||
-- Instance for the Void type
|
||||
instance GOrbit V1 where
|
||||
type GOrb V1 = Void
|
||||
gtoOrbit v = undefined
|
||||
gsupport _ = empty
|
||||
ggetElement v _ = undefined
|
||||
gindex _ _ = 0
|
||||
|
||||
|
||||
-- Instance for the Uni type
|
||||
instance GOrbit U1 where
|
||||
type GOrb U1 = ()
|
||||
gtoOrbit _ = ()
|
||||
gsupport _ = empty
|
||||
ggetElement _ _ = U1
|
||||
gindex _ _ = 0
|
||||
|
||||
|
||||
-- Disjoint unions are easy: just work on either side.
|
||||
instance (GOrbit f, GOrbit g) => GOrbit (f :+: g) where
|
||||
type GOrb (f :+: g) = Either (GOrb f) (GOrb g)
|
||||
gtoOrbit (L1 a) = Left (gtoOrbit a)
|
||||
gtoOrbit (R1 b) = Right (gtoOrbit b)
|
||||
gsupport (L1 a) = gsupport a
|
||||
gsupport (R1 b) = gsupport b
|
||||
ggetElement (Left oa) s = L1 (ggetElement oa s)
|
||||
ggetElement (Right ob) s = R1 (ggetElement ob s)
|
||||
gindex proxy (Left oa) = gindex (left proxy) oa where
|
||||
left :: proxy (f :+: g) -> Proxy f
|
||||
left _ = Proxy
|
||||
gindex proxy (Right ob) = gindex (right proxy) ob where
|
||||
right :: proxy (f :+: g) -> Proxy g
|
||||
right _ = Proxy
|
||||
|
||||
|
||||
-- The cartesian product is a non-trivial instance. We represent orbits in a
|
||||
-- product as described inthe paper: with two orbits, and how the match. The
|
||||
-- matchings can be given as strings, which can be easily enumerated, in order
|
||||
-- to enumerate the whole product.
|
||||
instance (GOrbit f, GOrbit g) => GOrbit (f :*: g) where
|
||||
type GOrb (f :*: g) = OrbPair (GOrb f) (GOrb g)
|
||||
gtoOrbit ~(a :*: b) = OrbPair (gtoOrbit a) (gtoOrbit b) (bla sa sb)
|
||||
where
|
||||
sa = toList $ gsupport a
|
||||
sb = toList $ gsupport b
|
||||
bla [] ys = fmap (const GT) ys
|
||||
bla xs [] = fmap (const LT) xs
|
||||
bla (x:xs) (y:ys) = case compare x y of
|
||||
LT -> LT : (bla xs (y:ys))
|
||||
EQ -> EQ : (bla xs ys)
|
||||
GT -> GT : (bla (x:xs) ys)
|
||||
gsupport ~(a :*: b) = (gsupport a) `union` (gsupport b)
|
||||
ggetElement (OrbPair oa ob l) s = (ggetElement oa $ toSet ls) :*: (ggetElement ob $ toSet rs)
|
||||
where
|
||||
~(ls, rs) = partitionOrd fst . zip l . toList $ s
|
||||
toSet = fromDistinctAscList . fmap snd
|
||||
gindex _ (OrbPair _ _ l) = length l
|
||||
|
||||
data OrbPair a b = OrbPair !a !b ![Ordering]
|
||||
deriving (Show, Eq, Ord, Generic)
|
||||
|
||||
-- Could be in prelude or some other general purpose lib
|
||||
partitionOrd :: (a -> Ordering) -> [a] -> ([a], [a])
|
||||
partitionOrd p xs = foldr (selectOrd p) ([], []) xs
|
||||
|
||||
selectOrd :: (a -> Ordering) -> a -> ([a], [a]) -> ([a], [a])
|
||||
selectOrd f x ~(ls, rs) = case f x of
|
||||
LT -> (x : ls, rs)
|
||||
EQ -> (x : ls, x : rs)
|
||||
GT -> (ls, x : rs)
|
||||
|
||||
|
||||
instance Orbit a => GOrbit (K1 c a) where
|
||||
-- Cannot use (Orb a) here, that may lead to a recursive type
|
||||
-- So we use the type OrbRec a instead (which uses Orb a one step later).
|
||||
type GOrb (K1 c a) = OrbRec a
|
||||
gtoOrbit (K1 x) = OrbRec (toOrbit x)
|
||||
gsupport (K1 x) = support x
|
||||
ggetElement (OrbRec x) s = K1 $ getElement x s
|
||||
gindex p (OrbRec o) = index (Proxy :: Proxy a) o
|
||||
|
||||
newtype OrbRec a = OrbRec (Orb a)
|
||||
deriving (Generic)
|
||||
deriving instance Show (Orb a) => Show (OrbRec a)
|
||||
deriving instance Ord (Orb a) => Ord (OrbRec a)
|
||||
deriving instance Eq (Orb a) => Eq (OrbRec a)
|
||||
|
||||
|
||||
instance GOrbit f => GOrbit (M1 i c f) where
|
||||
type GOrb (M1 i c f) = GOrb f
|
||||
gtoOrbit (M1 x) = gtoOrbit x
|
||||
gsupport (M1 x) = gsupport x
|
||||
ggetElement x s = M1 $ ggetElement x s
|
||||
gindex p o = gindex (Proxy :: Proxy f) o
|
||||
|
|
@ -10,15 +10,15 @@ import qualified Data.List.Ordered as LO
|
|||
import Data.Proxy
|
||||
import Prelude hiding (map, product)
|
||||
|
||||
import Orbit
|
||||
import Nominal
|
||||
import Support
|
||||
|
||||
|
||||
newtype OrbitList a = OrbitList { unOrbitList :: [Orb a] }
|
||||
newtype OrbitList a = OrbitList { unOrbitList :: [Orbit a] }
|
||||
|
||||
deriving instance Eq (Orb a) => Eq (OrbitList a)
|
||||
deriving instance Ord (Orb a) => Ord (OrbitList a)
|
||||
deriving instance Show (Orb a) => Show (OrbitList a)
|
||||
deriving instance Eq (Orbit a) => Eq (OrbitList a)
|
||||
deriving instance Ord (Orbit a) => Ord (OrbitList a)
|
||||
deriving instance Show (Orbit a) => Show (OrbitList a)
|
||||
|
||||
null :: OrbitList a -> Bool
|
||||
null (OrbitList x) = L.null x
|
||||
|
|
@ -26,20 +26,20 @@ null (OrbitList x) = L.null x
|
|||
empty :: OrbitList a
|
||||
empty = OrbitList []
|
||||
|
||||
singleOrbit :: Orbit a => a -> OrbitList a
|
||||
singleOrbit :: Nominal a => a -> OrbitList a
|
||||
singleOrbit a = OrbitList [toOrbit a]
|
||||
|
||||
rationals :: OrbitList Rat
|
||||
rationals = singleOrbit (Rat 0)
|
||||
|
||||
-- f should be equivariant
|
||||
map :: (Orbit a, Orbit b) => (a -> b) -> OrbitList a -> OrbitList b
|
||||
map :: (Nominal a, Nominal b) => (a -> b) -> OrbitList a -> OrbitList b
|
||||
map f (OrbitList as) = OrbitList $ L.map (omap f) as
|
||||
|
||||
productWith :: forall a b c. (Orbit a, Orbit b, Orbit c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c
|
||||
productWith :: forall a b c. (Nominal a, Nominal b, Nominal c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c
|
||||
productWith f (OrbitList as) (OrbitList bs) = map (uncurry f) (OrbitList (concat $ product (Proxy :: Proxy a) (Proxy :: Proxy b) <$> as <*> bs))
|
||||
|
||||
filter :: Orbit a => (a -> Bool) -> OrbitList a -> OrbitList a
|
||||
filter :: Nominal a => (a -> Bool) -> OrbitList a -> OrbitList a
|
||||
filter f = OrbitList . L.filter (f . getElementE) . unOrbitList
|
||||
|
||||
|
||||
|
|
@ -47,17 +47,17 @@ type SortedOrbitList a = OrbitList a
|
|||
-- the above map and productWith preserve ordering if `f` is order preserving
|
||||
-- on orbits and filter is always order preserving
|
||||
|
||||
union :: Ord (Orb a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a
|
||||
union :: Ord (Orbit a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a
|
||||
union (OrbitList x) (OrbitList y) = OrbitList (LO.union x y)
|
||||
|
||||
unionAll :: Ord (Orb a) => [SortedOrbitList a] -> SortedOrbitList a
|
||||
unionAll :: Ord (Orbit a) => [SortedOrbitList a] -> SortedOrbitList a
|
||||
unionAll = OrbitList . LO.unionAll . fmap unOrbitList
|
||||
|
||||
minus :: Ord (Orb a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a
|
||||
minus :: Ord (Orbit a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a
|
||||
minus (OrbitList x) (OrbitList y) = OrbitList (LO.minus x y)
|
||||
|
||||
-- decompose a into b and c (should be order preserving), and then throw away b
|
||||
projectWith :: (Orbit a, Orbit b, Orbit c, Eq (Orb b), Ord (Orb c)) => (a -> (b, c)) -> SortedOrbitList a -> SortedOrbitList c
|
||||
projectWith :: (Nominal a, Nominal b, Nominal c, Eq (Orbit b), Ord (Orbit c)) => (a -> (b, c)) -> SortedOrbitList a -> SortedOrbitList c
|
||||
projectWith f = unionAll . fmap OrbitList . groupOnFst . splitOrbs . unOrbitList . map f
|
||||
where
|
||||
splitOrbs = fmap (\o -> (omap fst o, omap snd o))
|
||||
|
|
|
|||
|
|
@ -5,14 +5,14 @@
|
|||
import Control.DeepSeq
|
||||
import Criterion.Main
|
||||
|
||||
import Orbit
|
||||
import Nominal
|
||||
import Support
|
||||
import EquivariantSet
|
||||
import EquivariantMap
|
||||
|
||||
instance NFData Rat
|
||||
|
||||
(\/) :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
(\/) :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
|
||||
(\/) = EquivariantSet.union
|
||||
|
||||
bigset :: (Rat, Rat, Rat, _) -> Bool
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue