Clean up and Stub for LStar

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))
+

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

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)
+

src/Nominal.hs

@@ -1,9 +1,4 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
 
 module Nominal
   ( module Nominal

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.

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