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

6
-- | This module implements the @M^X@ functor, where @M@ is a monoid that
7
-- doesn't have to be a group like in "Copar.Functors.GroupValued".
8
9
10
11
--
-- 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.
12
module Copar.Functors.MonoidValued
13
14
15
16
17
  ( SlowMonoidValued(..)
  , maxIntValued
  , maxRealValued
  )
where
18
19
20
21
22
23
24

import           Data.List                      ( foldl' )
import           Data.Semigroup                 ( Max(..) )
import           Data.Functor.Classes
import           Control.Monad
import           Data.Foldable

Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
25
import qualified Data.Vector                   as V
26
import           Text.Megaparsec
27
28
import qualified Data.Text.Prettyprint     as Doc
import           Data.Text.Prettyprint     ((<+>))
29

Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
30
import qualified Data.Vector.Utils             as V
31
32
33
34
35
import           Copar.RefinementInterface
import           Copar.FunctorDescription
import qualified Copar.Parser.Lexer               as L
import           Copar.FunctorExpression.Parser
import           Copar.Coalgebra.Parser
36
import           Data.Float.Utils               ( MaxDouble(..) )
37
import           Copar.Parser.Types
38
39
import           Data.SumBag (SumBag)
import qualified Data.SumBag as SumBag
40

41
42
43
44
45
46
47
48
49
50
51
52
53
54

data SlowMonoidValued m a = SlowMonoidValued a

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)

55
-- | The @(ℤ, max)^X@ functor
56
57
58
maxIntValued :: FunctorDescription (SlowMonoidValued (Max Int))
maxIntValued = FunctorDescription
  { name = "Max-valued"
59
  , syntaxExample = "(Z, max)^X"
60
  , description = Just intHelp
61
  , functorExprParser =
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
62
    prefix
63
64
65
66
67
68
      -- 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")
          )
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
69
70
71
      >> L.symbol "^"
      >> pure SlowMonoidValued
      )
72
73
  }

74

75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
intHelp :: Doc.Doc Doc.AnsiStyle
intHelp =
  Doc.reflow ("Weighted systems with the monoid (Z, 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 "(Z, max)^X"
  <> Doc.line <> Doc.line
  <> Doc.annotate Doc.bold "Coalgebra syntax:"
  <+> Doc.reflow "'{' X ':' int, ... '}'"


91
92
93
94
95
-- | The @(ℝ, max)^X@ functor
maxRealValued :: FunctorDescription (SlowMonoidValued MaxDouble)
maxRealValued = FunctorDescription
  { name = "Max-valued"
  , syntaxExample = "(R, max)^X"
96
  , description = Just realHelp
97
98
99
100
101
102
103
104
105
106
107
108
109
  , 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
      )
  }

110
111
112
113
114
115
116
117
118
119
120
121
122
123
realHelp :: Doc.Doc Doc.AnsiStyle
realHelp =
  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, ... '}'"
124

125
type instance Label (SlowMonoidValued m) = m
126
type instance Weight (SlowMonoidValued m) = (m, SumBag m)
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
127
128
type instance F1 (SlowMonoidValued m) = m
type instance F3 (SlowMonoidValued m) = (m, m, m)
129
130
131

instance (Monoid m, Ord m) => RefinementInterface (SlowMonoidValued m) where
  init
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
132
    :: F1 (SlowMonoidValued m)
133
134
135
    -> [Label (SlowMonoidValued m)]
    -> Weight (SlowMonoidValued m)
  init _ labels =
136
    (mempty, foldl' (flip SumBag.insert) SumBag.empty labels)
137
138
139
140
141

  update
    :: [Label (SlowMonoidValued m)]
    -> Weight (SlowMonoidValued m)
    -> ( Weight (SlowMonoidValued m)
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
142
       , F3 (SlowMonoidValued m)
143
144
145
       , Weight (SlowMonoidValued m)
       )
  update labels (sumRest, counts) =
146
147
148
149
    let toS  = foldl' (flip SumBag.insert) SumBag.empty labels
        toCWithoutS = foldl' (flip SumBag.delete) counts labels
        sumS = fold toS
        sumCWithoutS = fold toS
150
        f3   = (sumRest, sumCWithoutS, sumS)
151
152
        w1   = (sumRest <> sumCWithoutS, toS)
        w2   = (sumRest <> sumS, toCWithoutS)
153
    in  (w1, f3, w2)
154
155
156


instance ParseMorphism (SlowMonoidValued (Max Int)) where
157
158
159
  parseMorphismPoint (SlowMonoidValued inner) =
    parseMorphismPointHelper inner (Max <$> (L.signed L.decimal))
      =<< (not <$> noSanityChecks)
160
161
162


instance ParseMorphism (SlowMonoidValued MaxDouble) where
163
164
165
  parseMorphismPoint (SlowMonoidValued inner) =
    parseMorphismPointHelper inner (MaxDouble <$> L.signed L.float)
      =<< (not <$> noSanityChecks)
166
167


168
169
170
171
172
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)
173

174
175
      when (V.hasDuplicates (fmap fst succs)) $
        fail "monoid valued: Duplicate edges"
176

177
178
179
180
181
182
183
      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)