MonoidValued.hs 8.09 KB
Newer Older
1
{-# LANGUAGE FlexibleContexts #-}
2 3 4
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}

5
-- | This module implements the @M^X@ functor, where @M@ is a monoid that
6
-- doesn't have to be a group like in "Copar.Functors.GroupValued".
7 8 9 10
--
-- The 'RefinementInterface' implementation for such functors doesn't fulfil the
-- same runtime complexity criteria as the other functors and it also uses tons
-- of space, but it works and satisfies the axioms.
11
module Copar.Functors.MonoidValued
12 13
  ( SlowMonoidValued(..)
  , maxIntValued
14
  , minIntValued
15
  , maxRealValued
16
  , minRealValued
17
  , andWordValued 
18
  , orWordValued
19 20
  )
where
21

22
import           Data.List                      ( foldl', intersperse )
23
import           Data.Semigroup                 ( Max(..), Min(..) )
24 25 26
import           Data.Functor.Classes
import           Control.Monad
import           Data.Foldable
27
import           Data.Word
28

Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
29
import qualified Data.Vector                   as V
30
import           Text.Megaparsec
31 32 33
import qualified Data.Text.Prettyprint         as Doc
import           Data.Text.Prettyprint          ( (<+>) )
import           Data.Text                      ( Text )
34

Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
35
import qualified Data.Vector.Utils             as V
36 37 38 39 40
import           Copar.RefinementInterface
import           Copar.FunctorDescription
import qualified Copar.Parser.Lexer               as L
import           Copar.FunctorExpression.Parser
import           Copar.Coalgebra.Parser
41 42 43
import           Data.Float.Utils               ( MaxDouble(..)
                                                , MinDouble(..)
                                                )
44
import           Copar.Parser.Types
45 46
import           Data.SumBag (SumBag)
import qualified Data.SumBag as SumBag
47
import           Data.Bits.Monoid
48

49

50
newtype SlowMonoidValued m a = SlowMonoidValued a
51 52 53 54 55 56 57 58 59 60 61 62

instance Eq1 (SlowMonoidValued m) where
  liftEq f (SlowMonoidValued a1) (SlowMonoidValued a2) = f a1 a2

instance Show1 (SlowMonoidValued m) where
  liftShowsPrec f _ i (SlowMonoidValued a) = f i a

deriving instance Show (SlowMonoidValued m ())
deriving instance Functor (SlowMonoidValued m)
deriving instance Foldable (SlowMonoidValued m)
deriving instance Traversable (SlowMonoidValued m)

63 64 65
data MonoidValuedDescription m = MonoidValued
  { mvName :: Text
  , mvDescription :: Text
66
  , mvSet :: [Text] -- often [ascii, unicode]
67 68 69 70 71 72 73 74
  , mvOperation :: Text
  , mvTerm :: Text
  }

makeMonoidValued
  :: MonoidValuedDescription m -> FunctorDescription (SlowMonoidValued m)
makeMonoidValued desc = FunctorDescription
  { name = mvName desc <> "-valued"
75
  , syntaxExample = fold (intersperse " | " (map syntax (mvSet desc)))
76
  , description = Just (makeMVHelp desc)
77
  , functorExprParser =
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
78
    prefix
79 80 81 82
      -- 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
83
            ((choice (map L.symbol (mvSet desc)))
84 85 86
            >> L.comma
            >> L.symbol (mvOperation desc)
            )
87
          )
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
88 89 90
      >> L.symbol "^"
      >> pure SlowMonoidValued
      )
91
  }
92
  where syntax x = functorSyntax x (mvOperation desc)
93

94 95
functorSyntax :: Text -> Text -> Text
functorSyntax s o = "(" <> s <> ", " <> o <> ")^X"
96

97 98 99
makeMVHelp :: MonoidValuedDescription m -> Doc.Doc Doc.AnsiStyle
makeMVHelp desc =
  Doc.reflow ("Weighted systems with " <> mvDescription desc)
100 101 102 103 104 105 106
  <> 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:"
107
  <+> Doc.reflow (fold (intersperse " | " (map syntax (mvSet desc))))
108 109
  <> Doc.line <> Doc.line
  <> Doc.annotate Doc.bold "Coalgebra syntax:"
110
  <+> Doc.reflow ("'{' X ':' " <> mvTerm desc <> ", ... '}'")
111
  where syntax x = functorSyntax x (mvOperation desc)
112

113 114 115 116
-- | The @(ℤ, max)^X@ functor
maxIntValued :: FunctorDescription (SlowMonoidValued (Max Int))
maxIntValued = makeMonoidValued $ MonoidValued
  { mvName = "Max"
117
  , mvSet = ["Z", "ℤ"]
118 119 120 121
  , mvOperation = "max"
  , mvDescription = "the monoid (Z, max)"
  , mvTerm = "int"
  }
122

123 124
-- | The @(ℤ, min)^X@ functor
minIntValued :: FunctorDescription (SlowMonoidValued (Min Int))
125 126
minIntValued = makeMonoidValued $ MonoidValued
  { mvName = "Min"
127
  , mvSet = ["Z", "ℤ"]
128 129 130
  , mvOperation = "min"
  , mvDescription = "the monoid (Z, min)"
  , mvTerm = "int"
131 132 133
  }


134 135
-- | The @(ℝ, max)^X@ functor
maxRealValued :: FunctorDescription (SlowMonoidValued MaxDouble)
136 137
maxRealValued = makeMonoidValued $ MonoidValued
  { mvName = "Max"
138
  , mvSet = ["R", "ℝ"]
139 140 141
  , mvOperation = "max"
  , mvDescription = "the monoid (R, max)"
  , mvTerm = "real"
142 143
  }

144 145 146

-- | The @(ℝ, max)^X@ functor
minRealValued :: FunctorDescription (SlowMonoidValued MinDouble)
147 148
minRealValued = makeMonoidValued $ MonoidValued
  { mvName = "Min"
149
  , mvSet = ["R", "ℝ"]
150 151 152
  , mvOperation = "min"
  , mvDescription = "the monoid (R, min)"
  , mvTerm = "real"
153 154 155
  }


156 157
-- | The @(Word, and)^X@ functor
andWordValued :: FunctorDescription (SlowMonoidValued (BitAnd Word64))
158 159
andWordValued = makeMonoidValued $ MonoidValued
  { mvName = "BitAnd"
160
  , mvSet = ["Word"]
161 162 163
  , mvOperation = "and"
  , mvDescription = "bitvectors and bitwise 'and' as monoid weight"
  , mvTerm = "0xCAFE"
164 165 166
  }


167 168
-- | The @(Word, or)^X@ functor
orWordValued :: FunctorDescription (SlowMonoidValued (BitOr Word64))
169 170
orWordValued = makeMonoidValued $ MonoidValued
  { mvName = "BitOr"
171
  , mvSet = ["Word"]
172 173 174
  , mvOperation = "or"
  , mvDescription = "bitvectors and bitwise 'or' as monoid weight"
  , mvTerm = "0xCAFE"
175 176 177
  }


178
type instance Label (SlowMonoidValued m) = m
179
type instance Weight (SlowMonoidValued m) = (m, SumBag m)
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
180 181
type instance F1 (SlowMonoidValued m) = m
type instance F3 (SlowMonoidValued m) = (m, m, m)
182 183 184

instance (Monoid m, Ord m) => RefinementInterface (SlowMonoidValued m) where
  init
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
185
    :: F1 (SlowMonoidValued m)
186 187 188
    -> [Label (SlowMonoidValued m)]
    -> Weight (SlowMonoidValued m)
  init _ labels =
189
    (mempty, foldl' (flip SumBag.insert) SumBag.empty labels)
190 191 192 193 194

  update
    :: [Label (SlowMonoidValued m)]
    -> Weight (SlowMonoidValued m)
    -> ( Weight (SlowMonoidValued m)
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
195
       , F3 (SlowMonoidValued m)
196 197 198
       , Weight (SlowMonoidValued m)
       )
  update labels (sumRest, counts) =
199 200 201
    let toS  = foldl' (flip SumBag.insert) SumBag.empty labels
        toCWithoutS = foldl' (flip SumBag.delete) counts labels
        sumS = fold toS
Thorsten Wißmann's avatar
Thorsten Wißmann committed
202
        sumCWithoutS = fold toCWithoutS
203
        f3   = (sumRest, sumCWithoutS, sumS)
204 205
        w1   = (sumRest <> sumCWithoutS, toS)
        w2   = (sumRest <> sumS, toCWithoutS)
206
    in  (w1, f3, w2)
207 208 209


instance ParseMorphism (SlowMonoidValued (Max Int)) where
210
  parseMorphismPoint = parseMorphismPointHelper (Max <$> (L.signed L.decimal))
211

212
instance ParseMorphism (SlowMonoidValued (Min Int)) where
213
  parseMorphismPoint = parseMorphismPointHelper (Min <$> (L.signed L.decimal))
214

215
instance ParseMorphism (SlowMonoidValued MaxDouble) where
216
  parseMorphismPoint = parseMorphismPointHelper (MaxDouble <$> L.signed L.float)
217

218
instance ParseMorphism (SlowMonoidValued MinDouble) where
219
  parseMorphismPoint = parseMorphismPointHelper (MinDouble <$> L.signed L.float)
220

221
instance ParseMorphism (SlowMonoidValued (BitAnd Word64)) where
222
  parseMorphismPoint = parseMorphismPointHelper L.hex
223

224
instance ParseMorphism (SlowMonoidValued (BitOr Word64)) where
225 226
  parseMorphismPoint = parseMorphismPointHelper L.hex

227

228 229 230
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
231

232 233 234
  !successors <- case sanity of
    True -> do
      succs <- V.sortOn fst . V.fromList <$> L.braces (edge `sepBy` L.comma)
235

236 237
      when (V.hasDuplicates (fmap fst succs)) $
        fail "monoid valued: Duplicate edges"
238

239 240 241 242 243 244 245
      return succs

    False -> V.fromList <$> L.braces (edge `sepBy` L.comma)

  let !f1 = fold (V.map snd successors)
  return (f1, successors)
  where edge = (,) <$> inner <*> (L.colon *> weightParser)