{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE CPP                        #-}

-- | A module that abstracts out monoidal actions.
module Raaz.Core.MonoidalAction
       ( -- * Monoidal action
         -- $basics$
         LAction (..), Distributive, SemiR (..), (<++>), semiRSpace, semiRMonoid
         -- ** Monoidal action on functors
       , LActionF(..), DistributiveF, TwistRF(..), twistFunctorValue, twistMonoidValue
         -- * Fields
         -- $fields$
       , FieldA, FieldM, Field, computeField, runFieldM, liftToFieldM
       ) where

import Control.Arrow
import Control.Applicative
import Data.Monoid

------------------ Actions and Monoidal actions -----------------------

-- $basics$
--
-- Consider any instance @l@ of a length unit as a monoid under
-- addition. Length units acts on pointers by displacing them. It
-- turns out that this action is crucial in abstracting out many
-- pointer manipulations in our library. In particular, Applicative
-- parsers, memory allocators and data serialisers can be abstractly
-- captured using this action.
--
-- We start with setting up some terminology.  Our setting here is a
-- space of points (captured by the type @space@) on which a monoid
-- (captured by the type @m@) acts. The space which we are most
-- interested in is the space of `CryptoPtr` and the monoid that act
-- on it can be any instance of `LengthUnit` as described above.
--
-- In this module, we consider /left/ actions of monoids, although
-- right actions can be analogously defined as well. For applications
-- we have in mind, namely for parsers etc, it is sufficient to
-- restrict our attention to left actions.  The left action will be
-- written in multiplicative notation with the operator `<.>` being the
-- multiplication.

-- | A monoid @m@ acting on the left of a space. Think of a left
-- action as a multiplication with the monoid. It should satisfy the
-- law:
--
-- > 1 <.> p = p                         -- identity
-- > a <> b <.> p  = a <.> b <.> p   -- successive displacements
--
class Monoid m => LAction m space where
  (<.>) :: m -> space -> space


infixr 5 <.>

-- | An alternate symbol for <> more useful in the additive context.
(<++>) :: Monoid m => m -> m -> m
(<++>) = (<>)

infixr 5 <++>


-- | Uniform action of a monoid on a functor. The laws that should
-- be satisfied are:
--
-- > 1 <<.>> fx  = fx
-- > (a <> b) <<.>> fx  = a . (b <<.>> fx)
-- > m <<.>> fmap f u = fmap f (m <<.>> u)   -- acts uniformly
class (Monoid m, Functor f) => LActionF m f where
  (<<.>>) :: m -> f a -> f a

infixr 5 <<.>>

---------------------- The semi-direct products ------------------------

-- | A left-monoid action on a monoidal-space, i.e. the space on which
-- the monoid acts is itself a monoid, is /distributive/ if it
-- satisfies the law:
--
-- > a <.> p <> q  = (a <.> p) <> (a <.> q).
--
-- The above law implies that every element @m@ is a monoid
-- homomorphism.
class (LAction m space, Monoid space) => Distributive m space

-- | The semidirect product Space ⋊ Monoid. For monoids acting on
-- monoidal spaces distributively the semi-direct product is itself a
-- monoid. It turns out that data serialisers can essentially seen as
-- a semidirect product.
data SemiR space m = SemiR space !m

#if MIN_VERSION_base(4,11,0)

instance Distributive m space => Semigroup (SemiR space m) where
  (<>) (SemiR x a) (SemiR y b) = SemiR (x `mappend`  (a <.> y))  (a `mappend` b)

#endif

instance Distributive m space => Monoid (SemiR space m) where

  mempty = SemiR mempty mempty
  {-# INLINE mempty #-}

  mappend (SemiR x a) (SemiR y b) = SemiR (x <++>  a <.> y)  (a <> b)
  {-# INLINE mappend #-}

  mconcat = foldr mappend mempty
  {-# INLINE mconcat #-}

-- | From the an element of semi-direct product Space ⋊ Monoid return
-- the point.
semiRSpace :: SemiR space m -> space
{-# INLINE semiRSpace #-}
semiRSpace (SemiR space _) = space

-- | From the an element of semi-direct product Space ⋊ Monoid return
-- the monoid element.
semiRMonoid :: SemiR space m -> m
{-# INLINE semiRMonoid #-}
semiRMonoid (SemiR _ m) =  m

--------------------------- Twisted functors ----------------------------



-- | The generalisation of distributivity to applicative
-- functors. This generalisation is what allows us to capture
-- applicative functors like parsers. For an applicative functor, and
-- a monoid acting uniformly on it, we say that the action is
-- distributive if the following laws are satisfied:
--
-- > m <<.>> (pure a) = pure a            -- pure values are stoic
-- > m <<.>> (a <*> b) = (m <<.>> a) <*> (m <<.>> b)  -- dist
class (Applicative f, LActionF m f) => DistributiveF m f

-- | The twisted functor is essentially a generalisation of
-- semi-direct product to applicative functors.
data TwistRF f m a = TwistRF (f a) !m

-- | Get the underlying functor value.
twistFunctorValue :: TwistRF f m a -> f a
twistFunctorValue (TwistRF fa _) = fa
{-# INLINE twistFunctorValue #-}

-- | Get the underlying monoid value.
twistMonoidValue :: TwistRF f m a -> m
twistMonoidValue (TwistRF _ m) =  m
{-# INLINE twistMonoidValue #-}

instance Functor f => Functor (TwistRF f m) where
  fmap f (TwistRF x m) = TwistRF (fmap f x) m

-- Proof of functor laws.
--
-- fmap id (TwistRF (x, m)) = TwistRF (fmap id x, m)
--                          = TwistRF (x, m)
--
-- fmap (f . g)  (TwistRF fx m) = TwistRF (fmap (f . g) x, m)
--                              = TwistRF (fmap f . fmap g $ x, m)
--                              = TwistRF (fmap f (fmap g x), m)
--                              = fmap f   $ TwistRF (fmap g x,  m)
--                              = (fmap f . fmap g) (TwistRF fx) m)
--

instance DistributiveF m f => Applicative (TwistRF f m) where
  pure a = TwistRF (pure a) mempty
  {-# INLINE pure #-}

  (TwistRF f mf)  <*> (TwistRF val mval)  = TwistRF res mres
    where res  = f <*> mf <<.>> val
          mres = mf <> mval

-- Consider an expression @u = u1 <*> u2 <*> ... <ur>@ where
-- ui = TwistRF fi mi
--
-- u = TwistRF f m where m = m1 <> m2 <> .. <> mr
-- f = f1 <*> m1 f2 <*> (m1 m2) f3 ...    <*> (m1 m2 .. mr-1) fr.
--
-- We will separately verify the functor part and the monoid
-- part of the  ofNow we can verify the laws of applicative
--
--


------------------------- A generic field -----------------------------------

-- $fields$
--
-- The main goal behind looking at monoidal actions are to captures
-- concrete objects of interest to us like parsers, serialisers and
-- memory allocators. These are essentially functions with domain
-- `CryptoPtr`. For example, a parser is a function that takes a
-- `CryptoPtr`, reads @n@ bytes say and produces a result a. To
-- sequence the next parse we need to essentially keep track of this
-- @n@. If we abstract this out to the general setting we need to
-- consider functions whose domain is the space of points. We use the
-- physicist's terminology and call them fields. The action of the
-- monoid on a space of points naturally extends to fields on them
--
-- @F^g   = λ x -> F (x^g) @
--
-- For our applications, we need to define generalised fields
-- associated with arrows. This is because we often have to deal with
-- functions that have side effects (i.e. `Kleisli` arrows). However,
-- for conceptual understanding, it is sufficient to stick to ordinary
-- functions. In fact, the informal proofs that we have scattered in
-- the source all have been written only for the arrow @->@.

-- | A field on the space is a function from the points in the space
-- to some value. Here we define it for a general arrow.

type FieldA arrow = WrappedArrow arrow


-- | A field where the underlying arrow is the (->). This is normally
-- what we call a field.
type Field = FieldA (->)

-- | Compute the value of a field at a given point in the space.
computeField :: Field space b -> space -> b
computeField = unwrapArrow
{-# INLINE computeField #-}

-- | A monadic arrow field.
type FieldM monad = FieldA (Kleisli monad)

-- | Lift a monadic action to FieldM.
liftToFieldM :: (a -> m b) -> FieldM m a b
liftToFieldM = WrapArrow . Kleisli
{-# INLINE liftToFieldM #-}
-- | Runs a monadic field at a given point in the space.
runFieldM :: FieldM monad space b -> space -> monad b
runFieldM = runKleisli . unwrapArrow
{-# INLINE runFieldM #-}

-- | The action on the space translates to the action on field.
instance (Arrow arrow, LAction m space) => LActionF m (WrappedArrow arrow space) where
  m <<.>> field =   WrapArrow $ unwrapArrow field <<^ (m<.>)
  {-# INLINE (<<.>>) #-}

instance (Arrow arrow, LAction m space) => DistributiveF m (WrappedArrow arrow space)