From 3df9e273bfc1de463cd9553b516ce00e907a1fc8 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 21 Jan 2019 14:39:25 +0100 Subject: [PATCH] Renamed a bunch of stuff --- app/ExampleAutomata.hs | 101 ++++++++++++++++++++++++++ app/{Main.hs => FoSolver.hs} | 2 - app/{OnsAutomata.hs => IO.hs} | 48 ++---------- app/LStar.hs | 8 +- app/Minimise.hs | 75 +------------------ ons-hs.cabal | 14 ++-- src/Automata.hs | 27 +++++++ src/Nominal.hs | 3 +- app/OnsQuotient.hs => src/Quotient.hs | 18 +++-- 9 files changed, 162 insertions(+), 134 deletions(-) create mode 100644 app/ExampleAutomata.hs rename app/{Main.hs => FoSolver.hs} (99%) rename app/{OnsAutomata.hs => IO.hs} (58%) create mode 100644 src/Automata.hs rename app/OnsQuotient.hs => src/Quotient.hs (66%) diff --git a/app/ExampleAutomata.hs b/app/ExampleAutomata.hs new file mode 100644 index 0000000..4095759 --- /dev/null +++ b/app/ExampleAutomata.hs @@ -0,0 +1,101 @@ +{-# language DeriveGeneric #-} +{-# language DerivingVia #-} +{-# language FlexibleContexts #-} +{-# language RecordWildCards #-} +{-# language UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-missing-signatures #-} + +module ExampleAutomata + ( module ExampleAutomata + , module Automata + ) where + +import Nominal hiding (product) +import Automata +import IO +import OrbitList +import qualified EquivariantMap as Map +import qualified EquivariantSet as Set + +import Data.Foldable (fold) +import qualified GHC.Generics as GHC +import Prelude as P hiding (map, product, words, filter, foldr) + +-- All example automata follow below + +-- words of length <= m +words m = fold $ go (m+1) (singleOrbit []) where + go 0 _ = [] + go k acc = acc : go (k-1) (productWith (:) rationals acc) + +fromKeys f = Map.fromSet f . Set.fromOrbitList + + +data DoubleWord = Store [Atom] | Check [Atom] | Accept | Reject + deriving (Eq, Ord, GHC.Generic) + deriving Nominal via Generic DoubleWord + +instance ToStr DoubleWord where + toStr (Store w) = "S " ++ toStr w + toStr (Check w) = "C " ++ toStr w + toStr Accept = "A" + toStr Reject = "R" + +doubleWordAut 0 = Automaton {..} where + states = fromList [Accept, Reject] + initialState = Accept + acceptance = fromKeys (Accept ==) states + transition = fromKeys (const Reject) $ product states rationals +doubleWordAut n = Automaton {..} where + states = fromList [Accept, Reject] <> map Store (words (n-1)) <> map Check (productWith (:) rationals (words (n-1))) + initialState = Store [] + acceptance = fromKeys (Accept ==) states + trans Accept _ = Reject + trans Reject _ = Reject + trans (Store l) a + | length l + 1 < n = Store (a:l) + | otherwise = Check (reverse (a:l)) + trans (Check (a:as)) b + | a == b = if (P.null as) then Accept else Check as + | otherwise = Reject + transition = fromKeys (uncurry trans) $ product states rationals + + +-- alphetbet for the Fifo queue example +data Fifo = Put Atom | Get Atom + deriving (Eq, Ord, Show, GHC.Generic) + deriving Nominal via Generic Fifo + +instance ToStr Fifo where + toStr (Put a) = "Put " ++ toStr a + toStr (Get a) = "Get " ++ toStr a + +instance FromStr Fifo 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" + +data FifoS = FifoS [Atom] [Atom] + deriving (Eq, Ord, GHC.Generic) + deriving Nominal via Generic FifoS + +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 + initialState = Just (FifoS [] []) + acceptance = fromKeys (Nothing /=) states + trans Nothing _ = Nothing + trans (Just (FifoS l1 l2)) (Put a) + | length l1 + length l2 >= n = Nothing + | otherwise = Just (FifoS (a:l1) l2) + trans (Just (FifoS [] [])) (Get _) = Nothing + trans (Just (FifoS l1 [])) (Get b) = trans (Just (FifoS [] (reverse l1))) (Get b) + trans (Just (FifoS l1 (a:l2))) (Get b) + | a == b = Just (FifoS l1 l2) + | otherwise = Nothing + transition = fromKeys (uncurry trans) $ product states fifoAlph diff --git a/app/Main.hs b/app/FoSolver.hs similarity index 99% rename from app/Main.hs rename to app/FoSolver.hs index 7e431db..6f79da4 100644 --- a/app/Main.hs +++ b/app/FoSolver.hs @@ -1,7 +1,5 @@ {-# LANGUAGE PatternSynonyms #-} -module Main where - import OrbitList hiding (head) import Support (Rat) diff --git a/app/OnsAutomata.hs b/app/IO.hs similarity index 58% rename from app/OnsAutomata.hs rename to app/IO.hs index 0007454..3d39ab1 100644 --- a/app/OnsAutomata.hs +++ b/app/IO.hs @@ -1,45 +1,16 @@ -{-# language DeriveGeneric #-} -{-# language DerivingVia #-} -{-# language FlexibleContexts #-} {-# language RecordWildCards #-} -{-# language UndecidableInstances #-} -module OnsAutomata where + +module IO where import Data.Char (isSpace) import Data.Ratio import Data.List (intersperse) import Nominal +import Automata import Support (Rat(..), Support(..)) -import OrbitList as L (OrbitList, toList) -import EquivariantMap as M (EquivariantMap, toList, (!)) - -import Prelude hiding (print, Word) -import qualified GHC.Generics as GHC - - -type Word a = [a] - --- states, initial state, acceptance, transition -data Automaton q a = Automaton - { states :: OrbitList q - , initialState :: q - , acceptance :: EquivariantMap q Bool - , transition :: EquivariantMap (q, a) q - } - -accepts :: (Nominal q, Ord (Orbit q), Nominal a, Ord (Orbit a)) - => Automaton q a -> Word a -> Bool -accepts aut l = go (initialState aut) l - where - go s [] = acceptance aut ! s - go s (a:w) = go (transition aut ! (s, a)) w - - --- alphetbet for the Fifo queue example -data Fifo = Put Rat | Get Rat - deriving (Eq, Ord, Show, GHC.Generic) - deriving Nominal via Generic Fifo +import OrbitList as L (toList) +import EquivariantMap as M (toList) -- I do not want to give weird Show instances for basic types, so I create my @@ -57,10 +28,6 @@ instance ToStr Rat where instance ToStr Support where toStr (Support s) = "{" ++ toStr s ++ "}" -instance ToStr Fifo where - toStr (Put a) = "Put " ++ toStr a - toStr (Get a) = "Get " ++ toStr a - instance ToStr Bool where toStr b = show b instance ToStr Int where toStr i = show i instance ToStr a => ToStr [a] where @@ -88,8 +55,3 @@ instance FromStr a => FromStr [a] where where (a, str2) = fromStr str (l, emptyStr) = fromStr (dropWhile isSpace str2) - -instance FromStr Fifo 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" diff --git a/app/LStar.hs b/app/LStar.hs index 1c818fa..c769b1d 100644 --- a/app/LStar.hs +++ b/app/LStar.hs @@ -3,11 +3,9 @@ {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} -module Main where - -import OnsAutomata -import OnsQuotient - +import ExampleAutomata +import IO +import Quotient import OrbitList import EquivariantMap (EquivariantMap(..), lookup, (!)) import qualified EquivariantMap as Map diff --git a/app/Minimise.hs b/app/Minimise.hs index 3e7dc24..2875faf 100644 --- a/app/Minimise.hs +++ b/app/Minimise.hs @@ -6,17 +6,14 @@ {-# language UndecidableInstances #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} -import Nominal hiding (product) -import Support (Rat(..), Support) -import OnsAutomata -import OnsQuotient +import ExampleAutomata +import IO +import Quotient import OrbitList import EquivariantMap ((!)) import qualified EquivariantMap as Map import qualified EquivariantSet as Set -import Data.Foldable (fold) -import qualified GHC.Generics as GHC import Prelude as P hiding (map, product, words, filter, foldr) @@ -78,69 +75,3 @@ main :: IO () main = do putStrLn . toStr $ (minimiseB (doubleWordAut 4) rationals) -- putStrLn . toStr $ (minimiseB (fifoAut 4) fifoAlph) - - --- All example automata follow below - --- words of length <= m -words m = fold $ go (m+1) (singleOrbit []) where - go 0 acc = [] - go k acc = acc : go (k-1) (productWith (:) rationals acc) - -fromKeys f = Map.fromSet f . Set.fromOrbitList - - -data DoubleWord = Store [Rat] | Check [Rat] | Accept | Reject - deriving (Eq, Ord, GHC.Generic) - deriving Nominal via Generic DoubleWord - -instance ToStr DoubleWord where - toStr (Store w) = "S " ++ toStr w - toStr (Check w) = "C " ++ toStr w - toStr Accept = "A" - toStr Reject = "R" - -doubleWordAut 0 = Automaton {..} where - states = fromList [Accept, Reject] - initialState = Accept - acceptance = fromKeys (Accept ==) states - transition = fromKeys (const Reject) $ product states rationals -doubleWordAut n = Automaton {..} where - states = fromList [Accept, Reject] <> map Store (words (n-1)) <> map Check (productWith (:) rationals (words (n-1))) - initialState = Store [] - acceptance = fromKeys (Accept ==) states - trans Accept _ = Reject - trans Reject _ = Reject - trans (Store l) a - | length l + 1 < n = Store (a:l) - | otherwise = Check (reverse (a:l)) - trans (Check (a:as)) b - | a == b = if (P.null as) then Accept else Check as - | otherwise = Reject - transition = fromKeys (uncurry trans) $ product states rationals - - -data FifoS = FifoS [Rat] [Rat] - deriving (Eq, Ord, GHC.Generic) - deriving Nominal via Generic FifoS - -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 - initialState = Just (FifoS [] []) - acceptance = fromKeys (Nothing /=) states - trans Nothing _ = Nothing - trans (Just (FifoS l1 l2)) (Put a) - | length l1 + length l2 >= n = Nothing - | otherwise = Just (FifoS (a:l1) l2) - trans (Just (FifoS [] [])) (Get _) = Nothing - trans (Just (FifoS l1 [])) (Get b) = trans (Just (FifoS [] (reverse l1))) (Get b) - trans (Just (FifoS l1 (a:l2))) (Get b) - | a == b = Just (FifoS l1 l2) - | otherwise = Nothing - transition = fromKeys (uncurry trans) $ product states fifoAlph diff --git a/ons-hs.cabal b/ons-hs.cabal index 37dd830..8635101 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -15,12 +15,14 @@ cabal-version: >=1.10 library hs-source-dirs: src - exposed-modules: EquivariantMap + exposed-modules: Automata + , EquivariantMap , EquivariantSet , Nominal , Nominal.Class , Nominal.Products , OrbitList + , Quotient , Support , Support.Rat , Support.OrdList @@ -33,7 +35,7 @@ library executable ons-hs-solver hs-source-dirs: app - main-is: Main.hs + main-is: FoSolver.hs build-depends: base , ons-hs ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2 @@ -45,8 +47,8 @@ executable ons-hs-lstar build-depends: base , mtl , ons-hs - other-modules: OnsAutomata - , OnsQuotient + other-modules: ExampleAutomata + , IO ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2 default-language: Haskell2010 @@ -56,8 +58,8 @@ executable ons-hs-minimise build-depends: base , mtl , ons-hs - other-modules: OnsAutomata - , OnsQuotient + other-modules: ExampleAutomata + , IO ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2 default-language: Haskell2010 diff --git a/src/Automata.hs b/src/Automata.hs new file mode 100644 index 0000000..3ed393a --- /dev/null +++ b/src/Automata.hs @@ -0,0 +1,27 @@ +{-# language FlexibleContexts #-} + +module Automata where + +import Nominal (Nominal(..)) +import OrbitList (OrbitList) +import EquivariantMap (EquivariantMap, (!)) + +import Prelude hiding (Word) + + +type Word a = [a] + +-- states, initial state, acceptance, transition +data Automaton q a = Automaton + { states :: OrbitList q + , initialState :: q + , acceptance :: EquivariantMap q Bool + , transition :: EquivariantMap (q, a) q + } + +accepts :: (Nominal q, Ord (Orbit q), Nominal a, Ord (Orbit a)) + => Automaton q a -> Word a -> Bool +accepts aut l = go (initialState aut) l + where + go s [] = acceptance aut ! s + go s (a:w) = go (transition aut ! (s, a)) w diff --git a/src/Nominal.hs b/src/Nominal.hs index 19edcf5..19839e7 100644 --- a/src/Nominal.hs +++ b/src/Nominal.hs @@ -9,8 +9,9 @@ import Data.Proxy import Nominal.Products import Nominal.Class -import Support (def) +import Support (Rat, def) +type Atom = Rat -- We can get 'default' values, if we don't care about the support. getElementE :: forall a. Nominal a => Orbit a -> a diff --git a/app/OnsQuotient.hs b/src/Quotient.hs similarity index 66% rename from app/OnsQuotient.hs rename to src/Quotient.hs index 7a9d9a2..e0b4db5 100644 --- a/app/OnsQuotient.hs +++ b/src/Quotient.hs @@ -1,26 +1,34 @@ {-# language FlexibleContexts #-} -module OnsQuotient where +module Quotient where import Nominal (Nominal(..)) import Support (Support, intersect) import OrbitList -import EquivariantMap (EquivariantMap(..)) +import EquivariantMap (EquivariantMap) import qualified EquivariantMap as Map -import EquivariantSet (EquivariantSet(..)) +import EquivariantSet (EquivariantSet) import qualified EquivariantSet as Set import Prelude (Bool, Int, Ord, (.), (<>), (+), ($), fst, snd, fmap, uncurry) + +{- Computes the quotient of some set (given as OrbitList) and equivalence + relations. Returns the quotientmap and the set of images. The non-trivial + part is computing the least support, this is done by iteratively + intersecting supports. -} + type QuotientType = (Int, Support) type QuotientMap a = EquivariantMap a QuotientType -- Computes a quotient map given an equivalence relation -quotient :: (Nominal a, Ord (Orbit a)) => EquivariantSet (a, a) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType) +quotient :: (Nominal a, Ord (Orbit a)) + => EquivariantSet (a, a) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType) quotient equiv = post . quotientf 0 (\a b -> (a, b) `Set.member` equiv) where post (a, b, _) = (a, map fst b) -- f should be equivariant and an equivalence relation -quotientf :: (Nominal a, Ord (Orbit a)) => Int -> (a -> a -> Bool) -> OrbitList a -> (QuotientMap a, OrbitList (QuotientType, EquivariantSet a), Int) +quotientf :: (Nominal a, Ord (Orbit a)) + => Int -> (a -> a -> Bool) -> OrbitList a -> (QuotientMap a, OrbitList (QuotientType, EquivariantSet a), Int) quotientf k f ls = go k Map.empty empty (toList ls) where go n phi acc [] = (phi, acc, n)