MonoidValued.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}

-- | This module implements the @M^X@ functor, where @M@ is a monoid that
-- doesn't have to be a group like in "Copar.Functors.GroupValued".
--
-- 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.
module Copar.Functors.MonoidValued
  ( SlowMonoidValued(..)
  , maxIntValued
  , maxRealValued
  )
where

import           Data.List                      ( foldl' )
import           Data.Semigroup                 ( Max(..) )
import           Data.Functor.Classes
import           Control.Monad
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.Vector.Utils             as V
import           Copar.RefinementInterface
import           Copar.FunctorDescription
import qualified Copar.Parser.Lexer               as L
import           Copar.FunctorExpression.Parser
import           Copar.Coalgebra.Parser
import           Data.Float.Utils               ( MaxDouble(..) )
import           Copar.Parser.Types
import           Data.SumBag (SumBag)
import qualified Data.SumBag as SumBag


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)

-- | The @(ℤ, max)^X@ functor
maxIntValued :: FunctorDescription (SlowMonoidValued (Max Int))
maxIntValued = FunctorDescription
  { name = "Max-valued"
  , syntaxExample = "(Z, max)^X"
  , description = Just intHelp
  , 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 "^"
      >> pure SlowMonoidValued
      )
  }


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, ... '}'"


-- | The @(ℝ, max)^X@ functor
maxRealValued :: FunctorDescription (SlowMonoidValued MaxDouble)
maxRealValued = FunctorDescription
  { name = "Max-valued"
  , syntaxExample = "(R, max)^X"
  , description = Just realHelp
  , 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
      )
  }

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, ... '}'"

type instance Label (SlowMonoidValued m) = m
type instance Weight (SlowMonoidValued m) = (m, SumBag m)
type instance F1 (SlowMonoidValued m) = m
type instance F3 (SlowMonoidValued m) = (m, m, m)

instance (Monoid m, Ord m) => RefinementInterface (SlowMonoidValued m) where
  init
    :: F1 (SlowMonoidValued m)
    -> [Label (SlowMonoidValued m)]
    -> Weight (SlowMonoidValued m)
  init _ labels =
    (mempty, foldl' (flip SumBag.insert) SumBag.empty labels)

  update
    :: [Label (SlowMonoidValued m)]
    -> Weight (SlowMonoidValued m)
    -> ( Weight (SlowMonoidValued m)
       , F3 (SlowMonoidValued m)
       , Weight (SlowMonoidValued m)
       )
  update labels (sumRest, counts) =
    let toS  = foldl' (flip SumBag.insert) SumBag.empty labels
        toCWithoutS = foldl' (flip SumBag.delete) counts labels
        sumS = fold toS
        sumCWithoutS = fold toS
        f3   = (sumRest, sumCWithoutS, sumS)
        w1   = (sumRest <> sumCWithoutS, toS)
        w2   = (sumRest <> sumS, toCWithoutS)
    in  (w1, f3, w2)


instance ParseMorphism (SlowMonoidValued (Max Int)) where
  parseMorphismPoint (SlowMonoidValued inner) =
    parseMorphismPointHelper inner (Max <$> (L.signed L.decimal))
      =<< (not <$> noSanityChecks)


instance ParseMorphism (SlowMonoidValued MaxDouble) where
  parseMorphismPoint (SlowMonoidValued inner) =
    parseMorphismPointHelper inner (MaxDouble <$> L.signed L.float)
      =<< (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)

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

      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)