Commit 7fe7c5e7 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢

Merge branch 'minimize' [#33]

parents 62e1a264 b213aa49
......@@ -5,3 +5,5 @@
.dir-locals.el
/bin/
/TAGS
/cabal.project.local
/.hspec-failures
......@@ -37,6 +37,7 @@ library
, Data.SumBag
, Data.Bits.Monoid
, Copar.RefinementInterface
, Copar.MinimizationInterface
, Copar.Functors
, Copar.FunctorDescription
, Copar.FunctorPrinter
......@@ -65,6 +66,7 @@ library
, Copar.Coalgebra.Parser.Class
, Copar.Coalgebra.Parser.Internal
, Copar.Coalgebra.Printer
, Copar.Minimize
, Copar.PartitionPrinter
, Copar.Dot
, Copar.PrettyShow
......
......@@ -9,3 +9,11 @@ For example, a file called `foo` containing a coalgebra should have a `.out`
file with the output of:
stack exec copar refine < foo
Similarly, `.mini` files contain the output of CoPaR's `minimize` command, when
applied to the original file. This is also checked as part of the test suite.
## ui-tests
In this subdirectory there are further example snippets which might not be
necessarily useful as examples, as they are mostly used for testing.
{f, n}xX^{a, b}
s0_q1_q2: (n, {a: s0_q1_q2, b: s1_q3})
s1_q3: (f, {a: s0_q1_q2, b: s0_q1_q2})
\ No newline at end of file
P(XxX)
s00_a1_a2_a3: {(s00_a1_a2_a3, s00_a1_a2_a3)}
s01_b1_b4: {(s02_b2_b3_bot, s02_b2_b3_bot)}
s02_b2_b3_bot: {}
s03_c1_c10_c2_c3_c4_c5_c6_c7_c8_c9: {(s03_c1_c10_c2_c3_c4_c5_c6_c7_c8_c9, s02_b2_b3_bot)}
s04_d1: {(s06_d2, s02_b2_b3_bot)}
s05_d10: {(s04_d1, s04_d1)}
s06_d2: {(s07_d3, s02_b2_b3_bot)}
s07_d3: {(s08_d4, s02_b2_b3_bot)}
s08_d4: {(s09_d5, s02_b2_b3_bot)}
s09_d5: {(s10_d6, s02_b2_b3_bot)}
s10_d6: {(s11_d7, s02_b2_b3_bot)}
s11_d7: {(s12_d8, s02_b2_b3_bot)}
s12_d8: {(s13_d9, s02_b2_b3_bot)}
s13_d9: {(s05_d10, s02_b2_b3_bot)}
\ No newline at end of file
P(X)
x: { x, y }
y: { x }
z: { x, y }
\ No newline at end of file
C^X
s0: {s0: 1.0 + 1.0i, s1: 1.0 + 1.0i}
s1: {}
\ No newline at end of file
{square, circle, triangle}xP(X)
s0: (triangle, {s2, s3})
s1: (square, {})
s2: (circle, {})
s3: (circle, {s1})
s4: (circle, {s2})
s5: (triangle, {s2, s3, s4})
# a non-determ. automaton parsing binary trees
Ƥ(X×X)
bot: {}
d1: { (d2,bot) }
d2: { (d3,bot) }
d3: { (d4,bot) }
d4: { (d5,bot) }
d5: { (d6,bot) }
d6: { (d7,bot) }
d7: { (d8,bot) }
d8: { (d9,bot) }
d9: { (d10,bot) }
d10: { (d3,d3) }
{circled, normal} x Ƥ(ƤX)
a1: (normal, {{a1}})
\ No newline at end of file
{init, non_init} x Ƥ({a,b} + {f}×X×X)
q_i: (init, { inj1 (f, q_a, q_b), inj1 (f, q_b, q_a) })
q_a: (non_init, { inj0 a })
q_b: (non_init, { inj0 b })
......@@ -9,7 +9,8 @@
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Copar.Coalgebra.Parser
( parseMorphisms
( anonymizeSymbols
, parseMorphisms
, morphismsParser
, SymbolTable(..)
, module Copar.Coalgebra.Parser.Class
......@@ -26,6 +27,7 @@ import Control.Monad.State.Strict (execStateT, MonadState)
import qualified Data.HashMap.Strict as M
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.List as List
import Lens.Micro.Platform
import Text.Megaparsec hiding (State)
import qualified Data.Vector as V
......@@ -43,6 +45,8 @@ import qualified Copar.Parser.Lexer as L
import Copar.Parser.Types
import Copar.Coalgebra.Parser.Class
import GHC.Float (integerLogBase)
import Text.Printf
class HasSanityChecks m where
-- | When this returns 'True', morphism parsers are allowed (encouraged) to skip
......@@ -93,6 +97,16 @@ checkUndefinedRefs = use (symbolTable . to M.toList . to (filter isUndefined)) >
newtype SymbolTable = SymbolTable { fromSymbolTable :: M.HashMap State Text }
deriving (Show,Eq,Ord,NFData)
anonymizeSymbols :: SymbolTable -> SymbolTable
anonymizeSymbols symTbl = SymbolTable $ M.fromList (map anonymize
(zip [(0 :: Int)..] (List.sortOn snd $ M.toList table)))
where
anonymize (idx, (k, _)) =
( k
, T.pack (printf "s%0*d" ((+1) . (integerLogBase 10) . toInteger $ M.size table) idx)
)
table = fromSymbolTable symTbl
finalizeState :: forall f.
ParserState (Label f) (F1 f) -> (SymbolTable, Encoding (Label (Desorted f)) (F1 (Desorted f)))
finalizeState state =
......
......@@ -45,7 +45,7 @@ printEncoding encoding symbols sorts =
list <- MV.replicate (size encoding) []
V.rforM_ edges $
\edge -> MV.modify list ((desortedLabel @f (label edge), printState (to edge)):) (from edge)
V.freeze list
V.freeze list
printState :: State -> Build.Builder
printState state = maybe (morphismPoint state) Build.fromText (HM.lookup state (fromSymbolTable symbols))
......@@ -32,12 +32,14 @@ import Type.Reflection
import Copar.FunctorExpression.Parser
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.Coalgebra.Parser.Class
import Copar.Coalgebra.Printer
import Copar.PrettyShow
type Suitable f
= ( RefinementInterface f
, MinimizationInterface f
, ParseMorphism f
, PrintMorphism f
, Eq1 f
......
......@@ -49,6 +49,7 @@ import Copar.Coalgebra.Parser
import Copar.Coalgebra.Printer
import qualified Copar.Parser.Lexer as L
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.Functors.Polynomial hiding ( PolyF1(..) )
import qualified Copar.Functors.Polynomial as Poly
import qualified Copar.Functors.SomeFunctor as SF
......@@ -58,6 +59,7 @@ import Copar.Parser.Types
import qualified Data.Vector.Utils as V
import Data.Primitive.SmallArray
import Data.Function (on)
data Inner f a = Direct a | Absorbed (f a)
......@@ -253,7 +255,26 @@ instance RefinementInterface f => RefinementInterface (AbsorbingPolynomial f) wh
doUpdate _ PolyWeightToSub =
(PolyWeightToSub, PolyF3ToSub, PolyWeightToRest)
instance MinimizationInterface f => MinimizationInterface (AbsorbingPolynomial f) where
merge (AbsorbingPolynomial poly) lbls =
concatMap updateInner
$ NonEmpty.groupBy ((==) `on` labelIdx)
$ NonEmpty.sortBy (compare `on` labelIdx) lbls
where
labelIdx (PolyLabel i _) = i
updateInner :: NonEmpty (PolyLabel f) -> [PolyLabel f]
updateInner ((PolyLabel i (Just inner)):|ll) = map (\v -> PolyLabel i (Just v)) $ merge (innerFunctor i) (inner:|(innerLbls ll))
updateInner ((PolyLabel i Nothing):|ll) = (PolyLabel i Nothing):ll
innerLbls l = map (\(PolyLabel _ lbl) -> fromJust lbl) l
innerFunctors = V.fromList $ toList poly
innerFunctor :: Int -> f ()
innerFunctor i = case innerFunctors V.! i of
Direct _ -> undefined -- If labels exist for i this has to be an absorbed functor.
Absorbed f -> f
-- | Parse morphism for inner functor
--
-- If the inner value is just a variable, return (Nothing, [(x, Nothing)]). If
......
......@@ -23,6 +23,7 @@ import qualified Data.Text.Prettyprint as Doc
import Data.Text.Prettyprint ((<+>))
import Copar.RefinementInterface
import Copar.MinimizationInterface
import qualified Copar.Parser.Lexer as L
import Copar.FunctorExpression.Parser
import Copar.Coalgebra.Parser
......@@ -79,3 +80,6 @@ instance ParseMorphism Bag where
instance RefinementInterface Bag where
init = init @(GroupValued Int)
update = update @(GroupValued Int)
instance MinimizationInterface Bag where
merge _ = merge (GroupValued @Int ())
......@@ -24,6 +24,7 @@ import Copar.FunctorExpression.Parser
import Copar.Functors.GroupValued
import qualified Copar.Parser.Lexer as L
import Copar.RefinementInterface
import Copar.MinimizationInterface
newtype Distribution x = Distribution x
......@@ -88,3 +89,6 @@ instance RefinementInterface Distribution where
!toCwithoutS = w - toS
!f3 = mkGroupF3 toCwithoutS toS
in (toS, f3, toCwithoutS)
instance MinimizationInterface Distribution where
merge _ = merge (GroupValued @EqDouble ())
......@@ -26,6 +26,7 @@ import Data.Foldable.Utils
import Data.Ratio
import Data.Functor.Classes
import qualified Data.List as List
import Data.Vector (Vector)
import qualified Data.Vector as V
import Text.Megaparsec
......@@ -38,6 +39,7 @@ import qualified Data.Text.Lazy.Builder.Int as Build
import Data.Float.Utils (EqDouble(..))
import qualified Data.Vector.Utils as V
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.Coalgebra.Parser
import Copar.Coalgebra.Printer
import Copar.FunctorExpression.Parser
......@@ -234,7 +236,7 @@ parseMorphismPointHelper inner weightParser sanity = do
{-# SPECIALIZE parseMorphismPointHelper :: MorphParser l f1 Int -> MorphParser l f1 EqDouble -> Bool -> MorphParser l f1 (EqDouble, Vector (Int, EqDouble)) #-}
instance PrintMorphism (GroupValued Int) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where printElem (value, state) = state <> ": " <> Build.decimal value
instance ParseMorphism (GroupValued Int) where
......@@ -243,7 +245,7 @@ instance ParseMorphism (GroupValued Int) where
=<< (not <$> noSanityChecks)
instance PrintMorphism (GroupValued EqDouble) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where printElem (EqDouble value, state) = state <> ": " <> printFloat value
instance ParseMorphism (GroupValued EqDouble) where
......@@ -252,7 +254,7 @@ instance ParseMorphism (GroupValued EqDouble) where
=<< (not <$> noSanityChecks)
instance PrintMorphism (GroupValued OrderedComplex) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where
printElem (OrderedComplex value, state) =
state <> ": " <>
......@@ -266,7 +268,7 @@ instance ParseMorphism (GroupValued OrderedComplex) where
=<< (not <$> noSanityChecks)
instance PrintMorphism (GroupValued (Ratio Int)) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where
printElem (value, state) =
state <> ": " <>
......@@ -295,3 +297,6 @@ instance (IsGroupF3 m, Ord m, Num m) => RefinementInterface (GroupValued m) wher
, mkGroupF3 toCwithoutS toS
, toCwithoutS
)
instance (IsGroupF3 m, Ord m, Num m) => MinimizationInterface (GroupValued m) where
merge _ weights = filter (/=0) [sum weights]
......@@ -38,6 +38,7 @@ import qualified Data.Text.Lazy.Builder.Int as Build
import qualified Data.Vector.Utils as V
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.FunctorDescription
import qualified Copar.Parser.Lexer as L
import Copar.FunctorExpression.Parser
......@@ -211,6 +212,9 @@ instance (Monoid m, Ord m) => RefinementInterface (SlowMonoidValued m) where
w2 = (sumRest <> sumS, toCWithoutS)
in (w1, f3, w2)
instance (Monoid m, Ord m) => MinimizationInterface (SlowMonoidValued m) where
merge _ lbls = filter (/=mempty) [fold lbls]
instance PrintMorphism (SlowMonoidValued (Max Int)) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printEdge edges <> "}"
where printEdge ((Max value), state) = state <> ": " <> Build.decimal value
......
......@@ -25,7 +25,6 @@ import Data.Bifunctor
import Data.Foldable.Utils
import Data.Foldable (fold)
import Data.Traversable (mapAccumL)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Word (Word8)
......@@ -38,7 +37,7 @@ import Data.Either ( lefts
import qualified Data.Vector.Utils as V
import Data.Text (Text)
import Data.Maybe (fromJust)
import qualified Data.List as List
import Data.Vector (Vector)
import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as VU
......@@ -58,6 +57,7 @@ import Copar.Coalgebra.Printer
import qualified Copar.Parser.Lexer as L
import Copar.Parser.Types
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.FunctorExpression.Parser
import Copar.FunctorDescription
......@@ -303,32 +303,36 @@ printSumPoint (Sum sum) f1 edges =
printProductPoint :: Product () -> F1 Polynomial -> [(Label Polynomial, Build.Builder)] -> Build.Builder
printProductPoint (Product prod) f1 edges' =
let inner = sepFold ", " id (snd (mapAccumL printFactor (0, edges') prod))
let inner = sepFold ", " id (snd (mapAccumL printFactor (0, 0) prod))
in if NonEmpty.length prod /= 1 then "(" <> inner <> ")" else inner
where
printFactor :: (Int, [(Label Polynomial, Build.Builder)])
edges = V.fromList . map snd $ List.sortOn fst edges'
printFactor :: (Int, Int)
-> Factor ()
-> ((Int, [(Label Polynomial, Build.Builder)]), Build.Builder)
printFactor (ct, edges) (Const IntSet) = ((ct + 1, edges), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Const NatSet) = ((ct + 1, edges), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Const (FiniteNatSet _)) = ((ct + 1, edges), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Const (ExplicitSet elems)) =
((ct + 1, edges), Build.fromText $ elems V.! (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Identity ()) = ((ct, rest), snd var)
where (var, rest) = fromJust $ List.uncons edges
printFactor (ct, edges) (Exponential () (ExplicitExp elems)) =
let ((ct', edges'), elems') = mapAccumL (printExp Build.fromText) (ct, edges) elems
in ((ct', edges'), "{" <> sepFold ", " id elems' <> "}")
printFactor (ct, edges) (Exponential () (FiniteNatExp size)) =
let ((ct', edges'), elems') = mapAccumL (printExp Build.decimal) (ct, edges) (take size [(0 :: Int)..])
in ((ct', edges'), "{" <> sepFold ", " id elems' <> "}")
-> ((Int, Int), Build.Builder)
printFactor (ct, edge) (Const IntSet) = ((ct + 1, edge), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Const NatSet) = ((ct + 1, edge), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Const (FiniteNatSet _)) = ((ct + 1, edge), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Const (ExplicitSet elems)) =
((ct + 1, edge), Build.fromText $ elems V.! (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Identity ()) = ((ct, edge + 1), edges V.! edge)
printFactor (ct, edge) (Exponential () (ExplicitExp elems)) =
let ((ct', edge'), elems') = mapAccumL (printExp Build.fromText) (ct, edge) elems
in ((ct', edge'), "{" <> sepFold ", " id elems' <> "}")
printFactor (ct, edge) (Exponential () (FiniteNatExp size)) =
let ((ct', edge'), elems') = mapAccumL (printExp Build.decimal) (ct, edge) (take size [(0 :: Int)..])
in ((ct', edge'), "{" <> sepFold ", " id elems' <> "}")
printExp :: (a -> Build.Builder)
-> (Int, [(Label Polynomial, Build.Builder)])
-> (Int, Int)
-> a
-> ((Int, [(Label Polynomial, Build.Builder)]), Build.Builder)
printExp toBuilder (ct, edges) elem = ((ct, rest), toBuilder elem <> ": " <> snd var)
where (var, rest) = fromJust $ List.uncons edges
-> ((Int, Int), Build.Builder)
printExp toBuilder (ct, edge) elem =
((ct, edge + 1), toBuilder elem <> ": " <> edges V.! edge)
instance MinimizationInterface Polynomial where
merge _ = NonEmpty.toList
instance ParseMorphism Polynomial where
parseMorphismPoint (Polynomial expr) = parseSum1 expr
......
......@@ -16,6 +16,7 @@ import Data.Bits
import Data.Foldable.Utils
import Text.Megaparsec
import Data.List as List
import qualified Data.Vector as V
import qualified Data.Vector.Utils as V
import Data.Eq.Deriving (deriveEq1)
......@@ -24,6 +25,7 @@ import qualified Data.Text.Prettyprint as Doc
import Data.Text.Prettyprint ((<+>))
import Copar.RefinementInterface
import Copar.MinimizationInterface
import qualified Copar.Parser.Lexer as L
import Copar.FunctorExpression.Parser
import Copar.Coalgebra.Parser
......@@ -83,7 +85,7 @@ type instance F1 Powerset = Bool
type instance F3 Powerset = PowerF3
instance PrintMorphism Powerset where
printMorphismPoint _ _ edges = "{" <> sepFold ", " snd edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " snd (List.sortOn snd edges) <> "}"
instance ParseMorphism Powerset where
parseMorphismPoint (Powerset inner) = do
......@@ -126,3 +128,6 @@ instance RefinementInterface Powerset where
!weightToCwithoutS = packWeight (toRest || toS > 0) toCwithoutS
in
(weightToS, f3, weightToCwithoutS)
instance MinimizationInterface Powerset where
merge _ _ = [()]
......@@ -40,6 +40,7 @@ import Copar.FunctorExpression.Parser
import Copar.PrettyShow
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.FunctorDescription
......@@ -200,6 +201,20 @@ instance RefinementInterface SomeFunctor where
Just HRefl -> Just l
#endif
instance MinimizationInterface SomeFunctor where
merge (SomeFunctor (f :: f' ())) lbls =
#ifdef RELEASE
map SomeLabel (unsafeCoerce (merge f (unsafeCoerce lbls)))
#else
map (SomeLabel (typeRep @f')) $ merge f (fmap isSameType lbls)
where
isSameType :: SomeLabel -> Label f'
isSameType (SomeLabel f2 l) = case eqTypeRep f2 $ typeRep @f' of
-- this case should not happen.
Nothing -> error "Inconsistent internal state: Labels for different functors in SomeFunctor"
Just HRefl -> l
#endif
instance PrintMorphism SomeFunctor where
printMorphismPoint (SomeFunctor (f :: f' ())) f1 edges =
printMorphismPoint f (mapF1 f1) (mapMaybe mapEdges edges)
......@@ -228,5 +243,4 @@ instance ParseMorphism SomeFunctor where
#else
let newSuccs = V.map (\(x, y) -> (x, SomeLabel fRep y)) succs
#endif
return (newF1, newSuccs)
module Copar.MinimizationInterface
( MinimizationInterface(..)
) where
import Copar.RefinementInterface
import Data.List.NonEmpty
class RefinementInterface f => MinimizationInterface f where
-- | Merges the given labels.
--
-- Note: As merge [] = [] would always hold,
-- we can instead use NonEmpty here which simplifies the
-- implementation and is slightly more performant.
merge :: f () -> NonEmpty (Label f) -> [Label f]
module Copar.Minimize (minimize) where
import qualified Data.HashMap.Strict as HM
import Data.MorphismEncoding as Encoding
import Data.Partition
import qualified Data.Text as T
import Data.Foldable.Utils
import qualified Data.Vector as V
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe (mapMaybe)
import Copar.FunctorExpression.Type
import Copar.FunctorExpression.Desorting
import Copar.FunctorExpression.Sorts (Sort, sortTable)
import Copar.Coalgebra.Parser
import Copar.RefinementInterface
import Copar.MinimizationInterface
import GHC.Float (integerLogBase)
import Text.Printf
-- | Minimizes the given coalgebra by merging equivalent states.
minimize :: forall f. (Foldable f, Functor f, MinimizationInterface f)
=> FunctorExpression f Sort
-> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> SymbolTable
-> Partition
-> (Encoding (Label (Desorted f)) (F1 (Desorted f)), SymbolTable)
minimize f encoding symbolTable part =
( minimizeEncoding f encoding part
, minimizeSymbolTable symbolTable (toBlocks part)
)
-- | Minimizes the given encoding based on the given `Partition` by merging labels using
-- the `MinimizationInterface` of `f`.
minimizeEncoding :: forall f. (Foldable f, Functor f, MinimizationInterface f)
=> FunctorExpression f Sort
-> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> Partition
-> Encoding (Label (Desorted f)) (F1 (Desorted f))
minimizeEncoding f encoding part =
Encoding.new
-- States are only in the same block if they have the same F1, so
-- we can just use the F1 of the first state of each block here.
(V.fromList $ map getF1 (toBlocks part))
-- Merge edges with the same origin and target using `f`s `MinimizationInterface`.
((combineEdges encoding (sortTable f) part) . V.toList $ edges encoding)
where
getF1 (v:_) = structure encoding V.! v
getF1 _ = undefined -- This is unreachable, there are no empty blocks.
combineEdges :: forall f. (MinimizationInterface f)
=> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> V.Vector (f ())
-> Partition
-> [Edge (Label (Desorted f))]
-> V.Vector (Edge (Label (Desorted f)))
combineEdges encoding sorts part edges =
-- All relevant groups of edges which we have to `merge`.
let groupedEdges =
NonEmpty.groupBy (\a b -> from a == from b && to a == to b) $
sortEdges (mapMaybe (updateEdge part) edges)
in V.fromList . List.concat $ map mergeEdges groupedEdges
where
-- The functor sort of the given state.
--
-- As we have already updated the states here, we have to first look
-- at the original `state` which is the first state of the relevant block.
partitionSort state = fromEnum (sortedSort $ typeOf encoding (head $ statesOfBlock part (Block state))) - 1
mergeEdges :: NonEmpty (Edge (Label (Desorted f))) -> [Edge (Label (Desorted f))]
mergeEdges (e:|ll) = map
-- Edges in a group only differ in their `Label`, so we can reuse the first edge
-- to rebuild after unwrapping the `label` of each element.
(\v -> Edge (from e) (mapDesortedLabel @f @f (const v) $ label e) (to e))
(merge (sorts V.! (partitionSort $ from e)) (NonEmpty.map (desortedLabel @f . label) (e:|ll)))
sortEdges :: [Edge lbl] -> [Edge lbl]
sortEdges = List.sortBy (\a b -> compare (from a, to a) (from b, to b))
-- | Removes all edges which are not at the front of a block and updates `from` and `to` for the
-- remaining ones.
updateEdge :: Partition -> Edge f -> Maybe (Edge f)
updateEdge part e =
let block = blockOfState part $ from e
in if head (statesOfBlock part block) == from e then
Just (Edge (fromBlock block) (label e) (fromBlock (blockOfState part $ to e))) else Nothing
-- | Merges the symbols of all states in a given block.
--
-- We try quite hard to keep all of this deterministic, so we sort both the names of all states
-- in a block as well as padding the block numbers with zero so that the block number `09` remains in front of `10`.
minimizeSymbolTable :: SymbolTable -> [[State]] -> SymbolTable
minimizeSymbolTable symbols part =
SymbolTable { fromSymbolTable = HM.fromList partitions }
where
partitions = map (\(v, (i, n)) -> (i, T.pack (printf "s%0*d" ((+1) . (integerLogBase 10) . toInteger $ length blocks) v) <> "_" <> n))
$ zip [(0 :: Int)..] blocks
blocks = (filter ((/=mempty) . snd) (List.sortOn snd (zip [0..] (map nameBlock part))))
nameBlock block = sepFold "_" id (List.sort (mapMaybe (flip HM.lookup (fromSymbolTable symbols)) block))
......@@ -28,9 +28,9 @@ module Data.Partition
import Data.Foldable (toList)
import Control.Monad (forM_)
import Control.Monad.ST (runST)
import Control.DeepSeq
import qualified Data.HashMap.Strict as M
import qualified Data.Set as S
import Data.Vector (Vector)
import qualified Data.Vector as V
......@@ -110,12 +110,12 @@ fromBlocks states = -- TODO Check validity of input
-- | Return the partition as list of blocks, where each block is represented by
-- its elements.
toBlocks :: Partition -> [[State]]
toBlocks :: Partition -> [[State]] -- TODO directly return a Vector here instead
toBlocks p =
let
blockMap = V.ifoldr' (\s (Block b) m -> M.insertWith (++) b [s] m) M.empty (stateAssignment p)
in
M.elems blockMap
map reverse $ V.toList (runST $ do
blocks <- VM.replicate (numBlocks p) []
V.imapM_ (\st block -> VM.modify blocks (st:) (fromBlock block)) (stateAssignment p)
V.freeze blocks)
-- | The block that the given state is in.
blockOfState :: Partition -> State -> Block
......
......@@ -35,12 +35,13 @@ import qualified Data.MorphismEncoding as Encoding
import Copar.FunctorExpression.Sorts (Sort, sortedSort, sortTable)
import qualified Data.Partition as Partition
import Copar.Functors.SomeFunctor (SomeFunctor)