From c177d5954807db3e9cb150e0969646eaef8ad0f0 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 3 Jan 2019 17:22:50 +0100 Subject: [PATCH] Clean up and Stub for LStar --- app/LStar.hs | 56 +++++++++++++++++++++++++++++++++++++++++++ ons-hs.cabal | 11 ++++++++- src/EquivariantMap.hs | 45 +++++++++++++++++++++------------- src/Nominal.hs | 5 ---- src/Nominal/Class.hs | 6 ++--- src/OrbitList.hs | 39 +++++++++++++++++++++++++----- 6 files changed, 129 insertions(+), 33 deletions(-) create mode 100644 app/LStar.hs diff --git a/app/LStar.hs b/app/LStar.hs new file mode 100644 index 0000000..8543802 --- /dev/null +++ b/app/LStar.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Main where + +import Nominal hiding (product) +import Support (Rat(..)) +import OrbitList +import EquivariantMap (EquivariantMap, lookup, fromSet) +import EquivariantSet (fromOrbitList, toList) + +import Prelude hiding (filter, null, elem, lookup, product, Word, map) + +type Word a = [a] +type Alph a = OrbitList a +type Rows a = OrbitList (Word a) +type Columns a = OrbitList (Word a) +type Table a = EquivariantMap (Word a, Word a) Bool + +unequalRows :: (Nominal a, Ord (Orbit a)) => Word a -> Word a -> Columns a -> Table a -> Bool +unequalRows s0 t0 suffs table = + False `elem` ( productWith (\(s, t) e -> lookup (s, e) table == lookup (t, e) table) (singleOrbit (s0, t0)) suffs ) + + +equalRows :: (Nominal a, Ord (Orbit a)) => Word a -> Word a -> Columns a -> Table a -> Bool +equalRows s0 t0 suffs table = not (unequalRows s0 t0 suffs table) + +closed :: (Nominal a, Ord (Orbit a)) => Word a -> Rows a -> Columns a -> Table a -> Bool +closed t prefs suffs table = + null (filter (\(t, s) -> unequalRows t s suffs table) (product (singleOrbit t) prefs)) + +nonClosedness :: (Nominal a, Ord (Orbit a)) => Rows a -> Rows a -> Columns a -> Table a -> Rows a +nonClosedness prefs prefsExt suffs table = + filter (\t -> not (closed t prefs suffs table)) prefsExt + +inconsistencies :: (Nominal a, Ord a, Ord (Orbit a)) => Rows a -> Columns a -> Table a -> Alph a -> OrbitList (([a], [a]), (a, Word a)) +inconsistencies prefs suffs table alph = + filter (\((s, t), (a, e)) -> lookup (s ++ [a], e) table /= lookup (t ++ [a], e) table) candidatesExt + where + candidates = filter (\(s, t) -> s < t && equalRows s t suffs table) (product prefs prefs) + candidatesExt = product candidates (product alph suffs) + + +-- Example to test +accept [Rat a, Rat b] = a == b +accept _ = False + +main :: IO () +main = do + let alph = rationals + prefs = singleOrbit [] `union` map (\r -> [r]) alph + prefsExt = productWith (\p a -> p ++ [a]) prefs alph + suffs = singleOrbit [] + table = fromSet (\(a, b) -> accept (a ++ b)) . fromOrbitList $ product (prefs `union` prefsExt) (suffs) + print (toList . fromOrbitList $ (nonClosedness prefs prefsExt suffs table)) + print (toList . fromOrbitList $ (inconsistencies prefs suffs table alph)) + diff --git a/ons-hs.cabal b/ons-hs.cabal index bd7c3f8..d185662 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -31,7 +31,7 @@ library , MemoTrie default-language: Haskell2010 -executable ons-hs-exe +executable ons-hs-solver hs-source-dirs: app main-is: Main.hs ghc-options: -threaded -rtsopts -with-rtsopts=-N @@ -40,6 +40,15 @@ executable ons-hs-exe ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2 default-language: Haskell2010 +executable ons-hs-lstar + hs-source-dirs: app + main-is: LStar.hs + ghc-options: -threaded -rtsopts -with-rtsopts=-N + build-depends: base + , ons-hs + ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2 + default-language: Haskell2010 + benchmark ons-hs-bench type: exitcode-stdio-1.0 hs-source-dirs: test diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs index 19db4ea..f3966d5 100644 --- a/src/EquivariantMap.hs +++ b/src/EquivariantMap.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -10,10 +11,11 @@ import Data.Semigroup (Semigroup) import Data.Map (Map) import qualified Data.Map as Map -import EquivariantSet (EquivariantSet(EqSet)) +import EquivariantSet (EquivariantSet(..)) import Nominal import Support + -- TODO: foldable / traversable -- TODO: adjust / alter / update -- TODO: -WithKey functions @@ -21,6 +23,7 @@ import Support -- TODO: cleanup (usage of getElelemtE is not necessary) -- TODO: replace [Bool] by Vec Bool if better? + -- 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 @@ -32,25 +35,13 @@ 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... +-- Defined by the join-semilattice structure of Map. +-- This is left biased. deriving instance Ord (Orbit k) => Monoid (EquivariantMap k v) deriving instance Ord (Orbit k) => Semigroup (EquivariantMap k v) --- Helper functions - -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 [] _ = 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 :: (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) +-- This action is trivial, since equivariant maps are equivariant +deriving via (Trivial (EquivariantMap k v)) instance Nominal (EquivariantMap k v) -- Query @@ -93,6 +84,7 @@ intersectionWith :: forall k v1 v2 v3. (Nominal k, Nominal v1, Nominal v2, Nomin 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 @@ -104,6 +96,7 @@ mapWithKey :: (Nominal k, Nominal v1, Nominal v2) => (k -> v1 -> v2) -> Equivari 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) + -- Conversion keysSet :: EquivariantMap k v -> EquivariantSet k @@ -119,3 +112,21 @@ fromSet f (EqSet s) = EqMap (Map.fromSet f2 s) 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 + + +-- Helper functions + +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 [] _ = 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 :: (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) + diff --git a/src/Nominal.hs b/src/Nominal.hs index 45e0b27..19edcf5 100644 --- a/src/Nominal.hs +++ b/src/Nominal.hs @@ -1,9 +1,4 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DerivingVia #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} module Nominal ( module Nominal diff --git a/src/Nominal/Class.hs b/src/Nominal/Class.hs index de5f5a6..608f651 100644 --- a/src/Nominal/Class.hs +++ b/src/Nominal/Class.hs @@ -23,7 +23,7 @@ import qualified GHC.Generics as GHC (Generic) import Support --- This is the main meat of the package. The Orbit typeclass, it gives us ways +-- This is the main meat of the package. The Nominal 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. @@ -72,9 +72,7 @@ instance Nominal Support where -- 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) +-- (Available from GHC 8.6.1.) -- For the trivial action, each element is its own orbit and is supported -- by the empty set. diff --git a/src/OrbitList.hs b/src/OrbitList.hs index 211932c..21d54fa 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} @@ -11,18 +12,29 @@ import Data.Proxy import Prelude hiding (map, product) import Nominal -import Support - +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 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) + + +-- Query null :: OrbitList a -> Bool null (OrbitList x) = L.null x +elem :: (Nominal a, Eq (Orbit a)) => a -> OrbitList a -> Bool +elem x = L.elem (toOrbit x) . unOrbitList + + +-- Construction + empty :: OrbitList a empty = OrbitList [] @@ -32,21 +44,35 @@ singleOrbit a = OrbitList [toOrbit a] rationals :: OrbitList Rat rationals = singleOrbit (Rat 0) + +-- Map / Filter / ... + -- f should be equivariant 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. (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 :: Nominal a => (a -> Bool) -> OrbitList a -> OrbitList a filter f = OrbitList . L.filter (f . getElementE) . unOrbitList +-- Combinations + +product :: forall a b. (Nominal a, Nominal b) => OrbitList a -> OrbitList b -> OrbitList (a, b) +product (OrbitList as) (OrbitList bs) = OrbitList . concat $ (Nominal.product (Proxy :: Proxy a) (Proxy :: Proxy b) <$> as <*> bs) + +productWith :: (Nominal a, Nominal b, Nominal c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c +productWith f as bs = map (uncurry f) (OrbitList.product as bs) + + +-- Sorted Lists + 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 +-- Combinations + union :: Ord (Orbit a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a union (OrbitList x) (OrbitList y) = OrbitList (LO.union x y) @@ -56,7 +82,8 @@ unionAll = OrbitList . LO.unionAll . fmap unOrbitList 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 +-- decompose a into b and c, and then throw away b. +-- f should be equivariant and order preserving on orbits 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