Commit 74c8b14e authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢

Refactor MonoidValued module to reduce code duplication

parent 1ae4befb
......@@ -28,8 +28,9 @@ import Data.Foldable
import qualified Data.Vector as V
import Text.Megaparsec
import qualified Data.Text.Prettyprint as Doc
import Data.Text.Prettyprint ((<+>))
import qualified Data.Text.Prettyprint as Doc
import Data.Text.Prettyprint ( (<+>) )
import Data.Text ( Text )
import qualified Data.Vector.Utils as V
import Copar.RefinementInterface
......@@ -59,29 +60,43 @@ deriving instance Functor (SlowMonoidValued m)
deriving instance Foldable (SlowMonoidValued m)
deriving instance Traversable (SlowMonoidValued m)
-- | The @(ℤ, max)^X@ functor
maxIntValued :: FunctorDescription (SlowMonoidValued (Max Int))
maxIntValued = FunctorDescription
{ name = "Max-valued"
, syntaxExample = "(Z, max)^X"
, description = Just maxIntHelp
data MonoidValuedDescription m = MonoidValued
{ mvName :: Text
, mvDescription :: Text
, mvSet :: (Text, Text) -- (ascii, unicode)
, mvOperation :: Text
, mvTerm :: Text
}
makeMonoidValued
:: MonoidValuedDescription m -> FunctorDescription (SlowMonoidValued m)
makeMonoidValued desc = FunctorDescription
{ name = mvName desc <> "-valued"
, syntaxExample = syntax fst <> " | " <> syntax snd
, description = Just (makeMVHelp desc)
, functorExprParser =
prefix
-- We need this try here, so that parenthesis can still be parsed as
-- normal if they don't contain exactly (Z, max)
( try
(L.parens
((L.symbol "Z" <|> L.symbol "ℤ") >> L.comma >> L.symbol "max")
( (L.symbol (fst (mvSet desc)) <|> L.symbol (snd (mvSet desc)))
>> L.comma
>> L.symbol (mvOperation desc)
)
)
>> L.symbol "^"
>> pure SlowMonoidValued
)
}
where syntax f = functorSyntax (f (mvSet desc)) (mvOperation desc)
functorSyntax :: Text -> Text -> Text
functorSyntax s o = "(" <> s <> ", " <> o <> ")^X"
maxIntHelp :: Doc.Doc Doc.AnsiStyle
maxIntHelp =
Doc.reflow ("Weighted systems with the monoid (Z, max).")
makeMVHelp :: MonoidValuedDescription m -> Doc.Doc Doc.AnsiStyle
makeMVHelp desc =
Doc.reflow ("Weighted systems with " <> mvDescription desc)
<> Doc.line <> Doc.line
<> Doc.reflow "This is similar to all the group valued functors (int, real, \
\etc) but isn't actually a group as it lacks an inverse. Thus \
......@@ -89,191 +104,77 @@ maxIntHelp =
\asymptotically slower than for the others."
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Functor syntax:"
<+> Doc.reflow "(Z, max)^X"
<+> Doc.reflow (syntax fst <> " | " <> syntax snd)
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Coalgebra syntax:"
<+> Doc.reflow "'{' X ':' int, ... '}'"
<+> Doc.reflow ("'{' X ':' " <> mvTerm desc <> ", ... '}'")
where syntax f = functorSyntax (f (mvSet desc)) (mvOperation desc)
-- | The @(ℤ, max)^X@ functor
maxIntValued :: FunctorDescription (SlowMonoidValued (Max Int))
maxIntValued = makeMonoidValued $ MonoidValued
{ mvName = "Max"
, mvSet = ("Z", "ℤ")
, mvOperation = "max"
, mvDescription = "the monoid (Z, max)"
, mvTerm = "int"
}
-- | The @(ℤ, min)^X@ functor
minIntValued :: FunctorDescription (SlowMonoidValued (Min Int))
minIntValued = FunctorDescription
{ name = "Min-valued"
, syntaxExample = "(Z, min)^X"
, description = Just minIntHelp
, functorExprParser =
prefix
-- We need this try here, so that parenthesis can still be parsed as
-- normal if they don't contain exactly (Z, min)
( try
(L.parens
((L.symbol "Z" <|> L.symbol "ℤ") >> L.comma >> L.symbol "min")
)
>> L.symbol "^"
>> pure SlowMonoidValued
)
minIntValued = makeMonoidValued $ MonoidValued
{ mvName = "Min"
, mvSet = ("Z", "ℤ")
, mvOperation = "min"
, mvDescription = "the monoid (Z, min)"
, mvTerm = "int"
}
minIntHelp :: Doc.Doc Doc.AnsiStyle
minIntHelp =
Doc.reflow ("Weighted systems with the monoid (Z, min).")
<> Doc.line <> Doc.line
<> Doc.reflow "This is similar to all the group valued functors (int, real, \
\etc) but isn't actually a group as it lacks an inverse. Thus \
\the refinement interface implementation for this functor is\
\asymptotically slower than for the others."
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Functor syntax:"
<+> Doc.reflow "(Z, min)^X"
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Coalgebra syntax:"
<+> Doc.reflow "'{' X ':' int, ... '}'"
-- | The @(ℝ, max)^X@ functor
maxRealValued :: FunctorDescription (SlowMonoidValued MaxDouble)
maxRealValued = FunctorDescription
{ name = "Max-valued"
, syntaxExample = "(R, max)^X"
, description = Just maxRealHelp
, functorExprParser =
prefix
-- We need this try here, so that parenthesis can still be parsed as
-- normal if they don't contain exactly (Z, max)
( try
(L.parens
((L.symbol "R" <|> L.symbol "ℝ") >> L.comma >> L.symbol "max")
)
>> L.symbol "^"
>> pure SlowMonoidValued
)
maxRealValued = makeMonoidValued $ MonoidValued
{ mvName = "Max"
, mvSet = ("R", "ℝ")
, mvOperation = "max"
, mvDescription = "the monoid (R, max)"
, mvTerm = "real"
}
maxRealHelp :: Doc.Doc Doc.AnsiStyle
maxRealHelp =
Doc.reflow ("Weighted systems with the monoid (R, max).")
<> Doc.line <> Doc.line
<> Doc.reflow "This is similar to all the group valued functors (int, real, \
\etc) but isn't actually a group as it lacks an inverse. Thus \
\the refinement interface implementation for this functor is \
\asymptotically slower than for the others."
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Functor syntax:"
<+> Doc.reflow "(R, max)^X"
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Coalgebra syntax:"
<+> Doc.reflow "'{' X ':' real, ... '}'"
-- | The @(ℝ, max)^X@ functor
minRealValued :: FunctorDescription (SlowMonoidValued MinDouble)
minRealValued = FunctorDescription
{ name = "Min-valued"
, syntaxExample = "(R, min)^X"
, description = Just minRealHelp
, functorExprParser =
prefix
-- We need this try here, so that parenthesis can still be parsed as
-- normal if they don't contain exactly (Z, min)
( try
(L.parens
((L.symbol "R" <|> L.symbol "ℝ") >> L.comma >> L.symbol "min")
)
>> L.symbol "^"
>> pure SlowMonoidValued
)
minRealValued = makeMonoidValued $ MonoidValued
{ mvName = "Min"
, mvSet = ("R", "ℝ")
, mvOperation = "min"
, mvDescription = "the monoid (R, min)"
, mvTerm = "real"
}
minRealHelp :: Doc.Doc Doc.AnsiStyle
minRealHelp =
Doc.reflow ("Weighted systems with the monoid (R, min).")
<> Doc.line <> Doc.line
<> Doc.reflow "This is similar to all the group valued functors (int, real, \
\etc) but isn't actually a group as it lacks an inverse. Thus \
\the refinement interface implementation for this functor is \
\asymptotically slower than for the others."
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Functor syntax:"
<+> Doc.reflow "(R, min)^X"
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Coalgebra syntax:"
<+> Doc.reflow "'{' X ':' real, ... '}'"
-- | The @(ℕ, and)^X@ functor
andWordValued :: FunctorDescription (SlowMonoidValued (BitAnd Word))
andWordValued = FunctorDescription
{ name = "BitAnd-valued"
, syntaxExample = "(N, and)^X"
, description = Just andWordHelp
, functorExprParser =
prefix
-- We need this try here, so that parenthesis can still be parsed as
-- normal if they don't contain exactly (N, and)
( try
(L.parens
((L.symbol "N" <|> L.symbol "ℕ") >> L.comma >> L.symbol "and")
)
>> L.symbol "^"
>> pure SlowMonoidValued
)
andWordValued = makeMonoidValued $ MonoidValued
{ mvName = "BitAnd"
, mvSet = ("N", "ℕ")
, mvOperation = "and"
, mvDescription = "bitvectors and bitwise 'and' as monoid weight"
, mvTerm = "0xCAFE"
}
andWordHelp :: Doc.Doc Doc.AnsiStyle
andWordHelp =
Doc.reflow ("Weighted systems with bitvectors and bitwise 'and' as monoid weight.")
<> Doc.line <> Doc.line
<> Doc.reflow "This is similar to all the group valued functors (int, real, \
\etc) but isn't actually a group as it lacks an inverse. Thus \
\the refinement interface implementation for this functor is \
\asymptotically slower than for the others."
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Functor syntax:"
<+> Doc.reflow "(N, and)^X"
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Coalgebra syntax:"
<+> Doc.reflow "'{' X ':' 0xCAFE, ... '}'"
-- | The @(ℕ, or)^X@ functor
orWordValued :: FunctorDescription (SlowMonoidValued (BitOr Word))
orWordValued = FunctorDescription
{ name = "BitOr-valued"
, syntaxExample = "(N, or)^X"
, description = Just orWordHelp
, functorExprParser =
prefix
-- We need this try here, so that parenthesis can still be parsed as
-- normal if they don't contain exactly (N, or)
( try
(L.parens
((L.symbol "N" <|> L.symbol "ℕ") >> L.comma >> L.symbol "or")
)
>> L.symbol "^"
>> pure SlowMonoidValued
)
orWordValued = makeMonoidValued $ MonoidValued
{ mvName = "BitOr"
, mvSet = ("N", "ℕ")
, mvOperation = "or"
, mvDescription = "bitvectors and bitwise 'or' as monoid weight"
, mvTerm = "0xCAFE"
}
orWordHelp :: Doc.Doc Doc.AnsiStyle
orWordHelp =
Doc.reflow ("Weighted systems with bitvectors or bitwise 'or' as monoid weight.")
<> Doc.line <> Doc.line
<> Doc.reflow "This is similar to all the group valued functors (int, real, \
\etc) but isn't actually a group as it lacks an inverse. Thus \
\the refinement interface implementation for this functor is \
\asymptotically slower than for the others."
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Functor syntax:"
<+> Doc.reflow "(N, or)^X"
<> Doc.line <> Doc.line
<> Doc.annotate Doc.bold "Coalgebra syntax:"
<+> Doc.reflow "'{' X ':' 0xCAFE, ... '}'"
type instance Label (SlowMonoidValued m) = m
type instance Weight (SlowMonoidValued m) = (m, SumBag m)
type instance F1 (SlowMonoidValued m) = m
......@@ -306,41 +207,28 @@ instance (Monoid m, Ord m) => RefinementInterface (SlowMonoidValued m) where
instance ParseMorphism (SlowMonoidValued (Max Int)) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner (Max <$> (L.signed L.decimal))
=<< (not <$> noSanityChecks)
parseMorphismPoint = parseMorphismPointHelper (Max <$> (L.signed L.decimal))
instance ParseMorphism (SlowMonoidValued (Min Int)) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner (Min <$> (L.signed L.decimal))
=<< (not <$> noSanityChecks)
parseMorphismPoint = parseMorphismPointHelper (Min <$> (L.signed L.decimal))
instance ParseMorphism (SlowMonoidValued MaxDouble) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner (MaxDouble <$> L.signed L.float)
=<< (not <$> noSanityChecks)
parseMorphismPoint = parseMorphismPointHelper (MaxDouble <$> L.signed L.float)
instance ParseMorphism (SlowMonoidValued MinDouble) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner (MinDouble <$> L.signed L.float)
=<< (not <$> noSanityChecks)
parseMorphismPoint = parseMorphismPointHelper (MinDouble <$> L.signed L.float)
instance ParseMorphism (SlowMonoidValued (BitAnd Word)) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner L.hex =<< (not <$> noSanityChecks)
parseMorphismPoint = parseMorphismPointHelper L.hex
instance ParseMorphism (SlowMonoidValued (BitOr Word)) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner L.hex =<< (not <$> noSanityChecks)
parseMorphismPoint = parseMorphismPointHelper L.hex
parseMorphismPointHelper :: (HasSanityChecks m, MonadParser m, Ord x, Monoid w) => m w -> SlowMonoidValued w (m x) -> m (w, V.Vector (x, w))
parseMorphismPointHelper weightParser (SlowMonoidValued inner) = do
sanity <- not <$> noSanityChecks
parseMorphismPointHelper :: (MonadParser m, Ord x, Monoid w) => m x -> m w -> Bool -> m (w, V.Vector (x, w))
parseMorphismPointHelper inner weightParser sanity = do
!successors <- case sanity of
True -> do
succs <- V.sortOn fst . V.fromList <$> L.braces (edge `sepBy` L.comma)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment