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

Implement bitvectors and bitwise 'and' as monoid-valued functor

parent bd3e3a96
......@@ -18,6 +18,7 @@ import Copar.Functors.MonoidValued ( maxIntValued
, minIntValued
, maxRealValued
, minRealValued
, andWordValued
)
import Copar.Functors.SomeFunctor
......@@ -27,6 +28,7 @@ registeredFunctors =
, someFunctor minIntValued
, someFunctor maxRealValued
, someFunctor minRealValued
, someFunctor andWordValued
]
, [ someFunctor intValued
, someFunctor realValued
......
......@@ -15,6 +15,7 @@ module Copar.Functors.MonoidValued
, minIntValued
, maxRealValued
, minRealValued
, andWordValued
)
where
......@@ -41,6 +42,7 @@ import Data.Float.Utils ( MaxDouble(..)
import Copar.Parser.Types
import Data.SumBag (SumBag)
import qualified Data.SumBag as SumBag
import Data.Bits.Monoid
data SlowMonoidValued m a = SlowMonoidValued a
......@@ -199,6 +201,42 @@ minRealHelp =
<+> 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
)
}
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, ... '}'"
type instance Label (SlowMonoidValued m) = m
type instance Weight (SlowMonoidValued m) = (m, SumBag m)
type instance F1 (SlowMonoidValued m) = m
......@@ -254,6 +292,11 @@ instance ParseMorphism (SlowMonoidValued MinDouble) where
=<< (not <$> noSanityChecks)
instance ParseMorphism (SlowMonoidValued (BitAnd Word)) where
parseMorphismPoint (SlowMonoidValued inner) =
parseMorphismPointHelper inner L.hex =<< (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
......
......@@ -24,6 +24,7 @@ import Copar.FunctorExpression.Desorting
import qualified Data.Partition as Part
import Copar.Algorithm
import Data.Float.Utils
import Data.Bits.Monoid
spec :: Spec
spec = do
......@@ -35,6 +36,8 @@ spec = do
minRealParseSpec
maxRealRefineSpec
minRealRefineSpec
andWordParseSpec
andWordRefineSpec
maxIntParseSpec :: Spec
......@@ -274,3 +277,62 @@ minRealRefineSpec = describe "minReal refine" $ do
let Right enc = p "x: {x: 1.1, y: 3.1}\ny: {x: 1.1, y: 2.1}"
part <- stToIO (refine proxy enc True)
(Part.toBlocks part) `shouldMatchList` [[0, 1]]
andWordParseSpec :: Spec
andWordParseSpec = describe "bit-and parsing" $ do
it "can parse (N, and)^X as functor expression"
$ parseFunctorExpression [[functorExprParser andWordValued]] "" "(N, and)^X"
`shouldParse` (Functor 1 (SlowMonoidValued Variable))
it "can parse (ℕ, and)^X as functor expression"
$ parseFunctorExpression [[functorExprParser andWordValued]] "" "(ℕ, and)^X"
`shouldParse` (Functor 1 (SlowMonoidValued Variable))
it "nests correctly in functor expressions"
$ parseFunctorExpression [[functorExprParser andWordValued]]
""
"(N, and)^((N, and)^X)"
`shouldParse` (Functor
1
(SlowMonoidValued (Functor 1 (SlowMonoidValued Variable)))
)
it "still parses parenthesis in functor expressions correctly" $ do
parseFunctorExpression [[functorExprParser andWordValued]] "" "((N, and)^X)"
`shouldParse` (Functor 1 (SlowMonoidValued Variable))
parseFunctorExpression [[functorExprParser andWordValued]] "" "(N, and)^(X)"
`shouldParse` (Functor 1 (SlowMonoidValued Variable))
let p = fmap snd . parseMorphisms
(Functor 1 (SlowMonoidValued @(BitAnd Word) Variable))
EnableSanityChecks
""
it "parses an empty successor list"
$ p "x: {}"
`shouldParse` encoding [Sorted 1 mempty] []
it "parses a simple example"
$ p "x: {x: 0xA0, y: 0x0A}\ny: {}"
`shouldParse` encoding [Sorted 1 0, Sorted 1 mempty]
[(0, (Sorted 1 0xA0), 0), (0, (Sorted 1 0x0A), 1)]
it "fails on duplicate edges" $ p `shouldFailOn` "x: {x: 0xA, x: 0xA}"
andWordRefineSpec :: Spec
andWordRefineSpec = describe "andWord refine" $ do
let p = fmap snd
. parseMorphisms (Functor 1 (SlowMonoidValued @(BitAnd Word) Variable)) EnableSanityChecks ""
proxy = Proxy @(Desorted (SlowMonoidValued (BitAnd Word)))
it "it distinguishes different meets with equal sums" $ do
let Right enc = p "x: {x: 0xAA, y: 0xCC}\ny: {x: 0xBB, y: 0xBB}"
part <- stToIO (refine proxy enc True)
(Part.toBlocks part) `shouldMatchList` [[0], [1]]
it "identifies equal meets with different sums" $ do
let Right enc = p "x: {x: 0xA0, y: 0x0A}\ny: {x: 0x0B, y: 0xB0}"
part <- stToIO (refine proxy enc True)
(Part.toBlocks part) `shouldMatchList` [[0, 1]]
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