diff --git a/app/ExampleAutomata.hs b/app/ExampleAutomata.hs index 4095759..15aae19 100644 --- a/app/ExampleAutomata.hs +++ b/app/ExampleAutomata.hs @@ -62,19 +62,21 @@ doubleWordAut n = Automaton {..} where -- alphetbet for the Fifo queue example -data Fifo = Put Atom | Get Atom +data FifoA = Put Atom | Get Atom deriving (Eq, Ord, Show, GHC.Generic) - deriving Nominal via Generic Fifo + deriving Nominal via Generic FifoA -instance ToStr Fifo where +instance ToStr FifoA where toStr (Put a) = "Put " ++ toStr a toStr (Get a) = "Get " ++ toStr a -instance FromStr Fifo where +instance FromStr FifoA where fromStr ('P':'u':'t':' ':a) = let (x, r) = fromStr a in (Put x, r) fromStr ('G':'e':'t':' ':a) = let (x, r) = fromStr a in (Get x, r) fromStr _ = error "Cannot parse Fifo" +fifoAlph = map Put rationals <> map Get rationals + data FifoS = FifoS [Atom] [Atom] deriving (Eq, Ord, GHC.Generic) deriving Nominal via Generic FifoS @@ -82,8 +84,6 @@ data FifoS = FifoS [Atom] [Atom] instance ToStr FifoS where toStr (FifoS l1 l2) = "F " ++ toStr l1 ++ " - " ++ toStr l2 -fifoAlph = map Put rationals <> map Get rationals - fifoAut n = Automaton {..} where states0 = filter (\(FifoS l1 l2) -> length l1 + length l2 <= n) $ productWith (\l1 l2 -> FifoS l1 l2) (words n) (words n) states = fromList [Nothing] <> map Just states0 diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs index 50229cd..174d54a 100644 --- a/src/EquivariantMap.hs +++ b/src/EquivariantMap.hs @@ -28,8 +28,10 @@ import Support -- Very similar to EquivariantSet, but then the map analogue. The important -- 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. +-- representation, just like sets. This action is trivial, since equivariant +-- maps are equivariant. newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orbit k) (Orbit v, [Bool]) } + deriving Nominal via Trivial (EquivariantMap k v) -- Need undecidableIntances for this deriving instance (Eq (Orbit k), Eq (Orbit v)) => Eq (EquivariantMap k v) @@ -41,9 +43,6 @@ deriving instance (Show (Orbit k), Show (Orbit v)) => Show (EquivariantMap k v) deriving instance Ord (Orbit k) => Monoid (EquivariantMap k v) deriving instance Ord (Orbit k) => Semigroup (EquivariantMap k v) --- This action is trivial, since equivariant maps are equivariant -deriving via (Trivial (EquivariantMap k v)) instance Nominal (EquivariantMap k v) - -- Query diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs index 489f89c..9936491 100644 --- a/src/EquivariantSet.hs +++ b/src/EquivariantSet.hs @@ -22,8 +22,10 @@ import OrbitList (OrbitList(..)) -- represented. Although internally it is just a set of orbits, the interface -- 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. +-- representatives are chosen arbitrarily. This action is trivial, since +-- equivariant sets are equivariant :-). newtype EquivariantSet a = EqSet { unEqSet :: Set (Orbit a) } + deriving Nominal via Trivial (EquivariantSet a) -- Need undecidableIntances for this deriving instance Eq (Orbit a) => Eq (EquivariantSet a) @@ -35,9 +37,6 @@ deriving instance Show (Orbit a) => Show (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 Nominal (EquivariantSet a) - -- Query diff --git a/src/Nominal/Class.hs b/src/Nominal/Class.hs index bd22f98..e813c82 100644 --- a/src/Nominal/Class.hs +++ b/src/Nominal/Class.hs @@ -87,12 +87,12 @@ instance Nominal (Trivial a) where -- 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 Int) instance Nominal Int -- NB: Trivial instance! -deriving via (Trivial Ordering) instance Nominal Ordering +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 Int instance Nominal Int -- NB: Trivial instance! +deriving via Trivial Ordering instance Nominal Ordering -- The generic instance unfolds the algebraic data type in sums and products, @@ -107,14 +107,12 @@ instance (GHC.Generic a, GNominal (Rep a)) => Nominal (Generic a) where -- 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) +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 diff --git a/src/OrbitList.hs b/src/OrbitList.hs index 1ebc35d..b7142a8 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -18,11 +18,11 @@ import Support (Rat(..)) -- Similar to EquivariantSet, but merely a list structure. It is an -- equivariant data type, so the Nominal instance is trivial. newtype OrbitList a = OrbitList { unOrbitList :: [Orbit a] } + deriving Nominal via Trivial (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) -deriving via (Trivial (OrbitList a)) instance Nominal (OrbitList a) -- Simply concatenation of the list deriving instance Semigroup (OrbitList a)