{-# LANGUAGE NoRebindableSyntax #-}

-- | Free star semiring — the initial encoding of 'StarSemiring'.
--
-- The counting profile: 'Plus' does /not/ collapse duplicates.
-- For the idempotent profile, see 'kleeneSimplify'.
module NumHask.Free.StarSemiring
  ( StarSemiring (..),
    zero,
    one,
    plus,
    times,
    star,
    plusS,
    embed,
    lift,
    normalize,
    eval,
    foldStarSemiring,
    fromAdditive,
    fromMultiplicative,
    kleeneSimplify,
  )
where

import Data.Set (Set)
import Data.Set qualified as S
import NumHask.Algebra.Additive qualified as NHA
import NumHask.Algebra.Multiplicative qualified as NHM
import NumHask.Algebra.Ring qualified as NHR
import NumHask.Free.Additive qualified as HA
import NumHask.Free.Multiplicative qualified as HM
import Prelude (Eq, Ord, Show, foldr1, otherwise, (.), (==))

-- $setup
-- >>> import Prelude (String)
-- >>> import Data.Bool (Bool (..), bool)

-- | Free star semiring over a carrier type.
--
-- The initial encoding of 'NumHask.Algebra.Ring.StarSemiring'.
-- Extends the free semiring with the Kleene star.
--
-- 'Negate' is absent — 'StarSemiring' requires only 'Distributive',
-- not 'Subtractive'.
data StarSemiring a
  = Zero
  | One
  | Plus (StarSemiring a) (StarSemiring a)
  | Times (StarSemiring a) (StarSemiring a)
  | Star (StarSemiring a)
  | Embed a
  deriving (StarSemiring a -> StarSemiring a -> Bool
(StarSemiring a -> StarSemiring a -> Bool)
-> (StarSemiring a -> StarSemiring a -> Bool)
-> Eq (StarSemiring a)
forall a. Eq a => StarSemiring a -> StarSemiring a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => StarSemiring a -> StarSemiring a -> Bool
== :: StarSemiring a -> StarSemiring a -> Bool
$c/= :: forall a. Eq a => StarSemiring a -> StarSemiring a -> Bool
/= :: StarSemiring a -> StarSemiring a -> Bool
Eq, Eq (StarSemiring a)
Eq (StarSemiring a) =>
(StarSemiring a -> StarSemiring a -> Ordering)
-> (StarSemiring a -> StarSemiring a -> Bool)
-> (StarSemiring a -> StarSemiring a -> Bool)
-> (StarSemiring a -> StarSemiring a -> Bool)
-> (StarSemiring a -> StarSemiring a -> Bool)
-> (StarSemiring a -> StarSemiring a -> StarSemiring a)
-> (StarSemiring a -> StarSemiring a -> StarSemiring a)
-> Ord (StarSemiring a)
StarSemiring a -> StarSemiring a -> Bool
StarSemiring a -> StarSemiring a -> Ordering
StarSemiring a -> StarSemiring a -> StarSemiring a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (StarSemiring a)
forall a. Ord a => StarSemiring a -> StarSemiring a -> Bool
forall a. Ord a => StarSemiring a -> StarSemiring a -> Ordering
forall a.
Ord a =>
StarSemiring a -> StarSemiring a -> StarSemiring a
$ccompare :: forall a. Ord a => StarSemiring a -> StarSemiring a -> Ordering
compare :: StarSemiring a -> StarSemiring a -> Ordering
$c< :: forall a. Ord a => StarSemiring a -> StarSemiring a -> Bool
< :: StarSemiring a -> StarSemiring a -> Bool
$c<= :: forall a. Ord a => StarSemiring a -> StarSemiring a -> Bool
<= :: StarSemiring a -> StarSemiring a -> Bool
$c> :: forall a. Ord a => StarSemiring a -> StarSemiring a -> Bool
> :: StarSemiring a -> StarSemiring a -> Bool
$c>= :: forall a. Ord a => StarSemiring a -> StarSemiring a -> Bool
>= :: StarSemiring a -> StarSemiring a -> Bool
$cmax :: forall a.
Ord a =>
StarSemiring a -> StarSemiring a -> StarSemiring a
max :: StarSemiring a -> StarSemiring a -> StarSemiring a
$cmin :: forall a.
Ord a =>
StarSemiring a -> StarSemiring a -> StarSemiring a
min :: StarSemiring a -> StarSemiring a -> StarSemiring a
Ord, Int -> StarSemiring a -> ShowS
[StarSemiring a] -> ShowS
StarSemiring a -> String
(Int -> StarSemiring a -> ShowS)
-> (StarSemiring a -> String)
-> ([StarSemiring a] -> ShowS)
-> Show (StarSemiring a)
forall a. Show a => Int -> StarSemiring a -> ShowS
forall a. Show a => [StarSemiring a] -> ShowS
forall a. Show a => StarSemiring a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> StarSemiring a -> ShowS
showsPrec :: Int -> StarSemiring a -> ShowS
$cshow :: forall a. Show a => StarSemiring a -> String
show :: StarSemiring a -> String
$cshowList :: forall a. Show a => [StarSemiring a] -> ShowS
showList :: [StarSemiring a] -> ShowS
Show)

-- | Additive identity.
zero :: StarSemiring a
zero :: forall a. StarSemiring a
zero = StarSemiring a
forall a. StarSemiring a
Zero

-- | Multiplicative identity.
one :: StarSemiring a
one :: forall a. StarSemiring a
one = StarSemiring a
forall a. StarSemiring a
One

-- | Addition with identity absorption.
plus :: StarSemiring a -> StarSemiring a -> StarSemiring a
plus :: forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
plus StarSemiring a
Zero StarSemiring a
b = StarSemiring a
b
plus StarSemiring a
a StarSemiring a
Zero = StarSemiring a
a
plus StarSemiring a
a StarSemiring a
b = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
Plus StarSemiring a
a StarSemiring a
b

-- | Multiplication with identity absorption.
times :: StarSemiring a -> StarSemiring a -> StarSemiring a
times :: forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
times StarSemiring a
One StarSemiring a
b = StarSemiring a
b
times StarSemiring a
a StarSemiring a
One = StarSemiring a
a
times StarSemiring a
a StarSemiring a
b = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
Times StarSemiring a
a StarSemiring a
b

-- | Kleene star with universally-lawful simplifications.
--
-- @star Zero = One@ holds in every star semiring
-- (@star 0 = 1 + 0·star 0@).  The rules @star One = One@ and
-- @star (star a) = star a@ are /not/ applied — they hold only in
-- Kleene algebra (idempotent profile), not in the counting profile
-- where @star 1 = ∞ ≠ 1@.
--
-- >>> star zero
-- One
star :: StarSemiring a -> StarSemiring a
star :: forall a. StarSemiring a -> StarSemiring a
star StarSemiring a
Zero = StarSemiring a
forall a. StarSemiring a
One
star StarSemiring a
a = StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a
Star StarSemiring a
a

-- | Positive closure: @a⁺ = a · a*@.
plusS :: StarSemiring a -> StarSemiring a
plusS :: forall a. StarSemiring a -> StarSemiring a
plusS StarSemiring a
a = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
times StarSemiring a
a (StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a
star StarSemiring a
a)

-- | Embed a carrier value as an atomic generator.
embed :: a -> StarSemiring a
embed :: forall a. a -> StarSemiring a
embed = a -> StarSemiring a
forall a. a -> StarSemiring a
Embed

-- | Lift a carrier value, absorbing additive and multiplicative identities.
--
-- >>> lift False
-- Zero
-- >>> lift True
-- One
lift :: (Eq a, NHR.StarSemiring a) => a -> StarSemiring a
lift :: forall a. (Eq a, StarSemiring a) => a -> StarSemiring a
lift a
a
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Additive a => a
NHA.zero = StarSemiring a
forall a. StarSemiring a
Zero
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Multiplicative a => a
NHM.one = StarSemiring a
forall a. StarSemiring a
One
  | Bool
otherwise = a -> StarSemiring a
forall a. a -> StarSemiring a
Embed a
a

-- | Normalize a term with respect to star-semiring laws.
--
-- >>> normalize (embed False)
-- Zero
normalize :: (Eq a, NHR.StarSemiring a) => StarSemiring a -> StarSemiring a
normalize :: forall a.
(Eq a, StarSemiring a) =>
StarSemiring a -> StarSemiring a
normalize StarSemiring a
Zero = StarSemiring a
forall a. StarSemiring a
Zero
normalize StarSemiring a
One = StarSemiring a
forall a. StarSemiring a
One
normalize (Embed a
a)
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Additive a => a
NHA.zero = StarSemiring a
forall a. StarSemiring a
Zero
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Multiplicative a => a
NHM.one = StarSemiring a
forall a. StarSemiring a
One
  | Bool
otherwise = a -> StarSemiring a
forall a. a -> StarSemiring a
Embed a
a
normalize (Plus StarSemiring a
a StarSemiring a
b) = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
plus (StarSemiring a -> StarSemiring a
forall a.
(Eq a, StarSemiring a) =>
StarSemiring a -> StarSemiring a
normalize StarSemiring a
a) (StarSemiring a -> StarSemiring a
forall a.
(Eq a, StarSemiring a) =>
StarSemiring a -> StarSemiring a
normalize StarSemiring a
b)
normalize (Times StarSemiring a
a StarSemiring a
b) = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
times (StarSemiring a -> StarSemiring a
forall a.
(Eq a, StarSemiring a) =>
StarSemiring a -> StarSemiring a
normalize StarSemiring a
a) (StarSemiring a -> StarSemiring a
forall a.
(Eq a, StarSemiring a) =>
StarSemiring a -> StarSemiring a
normalize StarSemiring a
b)
normalize (Star StarSemiring a
a) = StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a
star (StarSemiring a -> StarSemiring a
forall a.
(Eq a, StarSemiring a) =>
StarSemiring a -> StarSemiring a
normalize StarSemiring a
a)

-- | Evaluate a term into any 'NumHask.Algebra.Ring.StarSemiring'.
--
-- This is the unique homomorphism out of the free star semiring.
eval :: (NHR.StarSemiring a) => StarSemiring a -> a
eval :: forall a. StarSemiring a => StarSemiring a -> a
eval StarSemiring a
Zero = a
forall a. Additive a => a
NHA.zero
eval StarSemiring a
One = a
forall a. Multiplicative a => a
NHM.one
eval (Plus StarSemiring a
a StarSemiring a
b) = StarSemiring a -> a
forall a. StarSemiring a => StarSemiring a -> a
eval StarSemiring a
a a -> a -> a
forall a. Additive a => a -> a -> a
NHA.+ StarSemiring a -> a
forall a. StarSemiring a => StarSemiring a -> a
eval StarSemiring a
b
eval (Times StarSemiring a
a StarSemiring a
b) = StarSemiring a -> a
forall a. StarSemiring a => StarSemiring a -> a
eval StarSemiring a
a a -> a -> a
forall a. Multiplicative a => a -> a -> a
NHM.* StarSemiring a -> a
forall a. StarSemiring a => StarSemiring a -> a
eval StarSemiring a
b
eval (Star StarSemiring a
a) = a -> a
forall a. StarSemiring a => a -> a
NHR.star (StarSemiring a -> a
forall a. StarSemiring a => StarSemiring a -> a
eval StarSemiring a
a)
eval (Embed a
a) = a
a

-- ---------------------------------------------------------------------------
-- The free object is an instance of its own class — that is what
-- \"free\" means.  These instances are what let 'Circuit.Mat.Dense.starMatrix'
-- run at carrier @StarSemiring a@: Kleene's state elimination, the
-- fourth face of the four-for-one.

-- | Methods are the smart constructors, so identity absorption
-- happens during a matrix-star computation's block recursion
-- rather than after it.
--
-- >>> import qualified NumHask.Algebra.Ring as NHR
-- >>> NHR.star (one :: StarSemiring String)
-- Star One
instance NHA.Additive (StarSemiring a) where
  zero :: StarSemiring a
zero = StarSemiring a
forall a. StarSemiring a
Zero
  + :: StarSemiring a -> StarSemiring a -> StarSemiring a
(+) = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
plus

instance NHM.Multiplicative (StarSemiring a) where
  one :: StarSemiring a
one = StarSemiring a
forall a. StarSemiring a
One
  * :: StarSemiring a -> StarSemiring a -> StarSemiring a
(*) = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
times

instance NHR.StarSemiring (StarSemiring a) where
  star :: StarSemiring a -> StarSemiring a
star = StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a
star

-- | Universal property: fold with a target star semiring.
foldStarSemiring ::
  b ->
  b ->
  (b -> b -> b) ->
  (b -> b -> b) ->
  (b -> b) ->
  (a -> b) ->
  StarSemiring a ->
  b
foldStarSemiring :: forall b a.
b
-> b
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b)
-> (a -> b)
-> StarSemiring a
-> b
foldStarSemiring b
z b
o b -> b -> b
p b -> b -> b
t b -> b
s a -> b
f = StarSemiring a -> b
go
  where
    go :: StarSemiring a -> b
go StarSemiring a
Zero = b
z
    go StarSemiring a
One = b
o
    go (Plus StarSemiring a
a StarSemiring a
b) = b -> b -> b
p (StarSemiring a -> b
go StarSemiring a
a) (StarSemiring a -> b
go StarSemiring a
b)
    go (Times StarSemiring a
a StarSemiring a
b) = b -> b -> b
t (StarSemiring a -> b
go StarSemiring a
a) (StarSemiring a -> b
go StarSemiring a
b)
    go (Star StarSemiring a
a) = b -> b
s (StarSemiring a -> b
go StarSemiring a
a)
    go (Embed a
a) = a -> b
f a
a

-- | Inject an additive term into the free star semiring.
fromAdditive :: HA.Additive a -> StarSemiring a
fromAdditive :: forall a. Additive a -> StarSemiring a
fromAdditive Additive a
HA.Zero = StarSemiring a
forall a. StarSemiring a
Zero
fromAdditive (HA.Plus Additive a
a Additive a
b) = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
Plus (Additive a -> StarSemiring a
forall a. Additive a -> StarSemiring a
fromAdditive Additive a
a) (Additive a -> StarSemiring a
forall a. Additive a -> StarSemiring a
fromAdditive Additive a
b)
fromAdditive (HA.Embed a
a) = a -> StarSemiring a
forall a. a -> StarSemiring a
Embed a
a

-- | Inject a multiplicative term into the free star semiring.
fromMultiplicative :: HM.Multiplicative a -> StarSemiring a
fromMultiplicative :: forall a. Multiplicative a -> StarSemiring a
fromMultiplicative Multiplicative a
HM.One = StarSemiring a
forall a. StarSemiring a
One
fromMultiplicative (HM.Times Multiplicative a
a Multiplicative a
b) = StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
Times (Multiplicative a -> StarSemiring a
forall a. Multiplicative a -> StarSemiring a
fromMultiplicative Multiplicative a
a) (Multiplicative a -> StarSemiring a
forall a. Multiplicative a -> StarSemiring a
fromMultiplicative Multiplicative a
b)
fromMultiplicative (HM.Embed a
a) = a -> StarSemiring a
forall a. a -> StarSemiring a
Embed a
a

-- | ACIZ simplification — Associativity, Commutativity, Idempotence
-- of 'Plus', with 'Zero' absorption.
--
-- Collapses duplicates under 'Plus' and absorbs 'Zero'.  Recurse
-- into 'Times' and 'Star' children.  This is shallow: full Kleene
-- algebra canonical form (automata minimisation) is not attempted.
--
-- Sound only when evaluated into an idempotent (Kleene algebra)
-- target; for counting targets (ℕ), 'kleeneSimplify' changes the
-- value of evaluation.
--
-- >>> let x = embed "x" :: StarSemiring String
-- >>> let y = embed "y"
-- >>> -- top-level duplicate collapses
-- >>> kleeneSimplify (plus x x)
-- Embed "x"
-- >>> -- child duplicate also collapses
-- >>> kleeneSimplify (times (plus x x) y)
-- Times (Embed "x") (Embed "y")
-- >>> -- star child normalised
-- >>> kleeneSimplify (star (plus x x))
-- Star (Embed "x")
--
-- Value-preserving for idempotent targets — executable witness over
-- the 'Warshall' Kleene algebra (a law, not a proof;
-- the @Arbitrary@-powered property awaits a test-suite home rather
-- than a doctest):
--
-- >>> import NumHask.Free.Carriers (Warshall (..))
-- >>> let t = times (plus (embed (Warshall True)) (embed (Warshall True))) (embed (Warshall False))
-- >>> (eval (kleeneSimplify t), eval t)
-- (Warshall False,Warshall False)
kleeneSimplify :: (Ord a) => StarSemiring a -> StarSemiring a
kleeneSimplify :: forall a. Ord a => StarSemiring a -> StarSemiring a
kleeneSimplify = Set (StarSemiring a) -> StarSemiring a
forall a. Set (StarSemiring a) -> StarSemiring a
fromSet (Set (StarSemiring a) -> StarSemiring a)
-> (StarSemiring a -> Set (StarSemiring a))
-> StarSemiring a
-> StarSemiring a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StarSemiring a -> Set (StarSemiring a)
forall a. Ord a => StarSemiring a -> Set (StarSemiring a)
toSet
  where
    normChild :: (Ord a) => StarSemiring a -> StarSemiring a
    normChild :: forall a. Ord a => StarSemiring a -> StarSemiring a
normChild = StarSemiring a -> StarSemiring a
forall a. Ord a => StarSemiring a -> StarSemiring a
kleeneSimplify

    toSet :: (Ord a) => StarSemiring a -> Set (StarSemiring a)
    toSet :: forall a. Ord a => StarSemiring a -> Set (StarSemiring a)
toSet StarSemiring a
Zero = Set (StarSemiring a)
forall a. Set a
S.empty
    toSet (Plus StarSemiring a
a StarSemiring a
b) = Set (StarSemiring a)
-> Set (StarSemiring a) -> Set (StarSemiring a)
forall a. Ord a => Set a -> Set a -> Set a
S.union (StarSemiring a -> Set (StarSemiring a)
forall a. Ord a => StarSemiring a -> Set (StarSemiring a)
toSet StarSemiring a
a) (StarSemiring a -> Set (StarSemiring a)
forall a. Ord a => StarSemiring a -> Set (StarSemiring a)
toSet StarSemiring a
b)
    toSet (Times StarSemiring a
a StarSemiring a
b) = StarSemiring a -> Set (StarSemiring a)
forall a. a -> Set a
S.singleton (StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
Times (StarSemiring a -> StarSemiring a
forall a. Ord a => StarSemiring a -> StarSemiring a
normChild StarSemiring a
a) (StarSemiring a -> StarSemiring a
forall a. Ord a => StarSemiring a -> StarSemiring a
normChild StarSemiring a
b))
    toSet (Star StarSemiring a
a) = StarSemiring a -> Set (StarSemiring a)
forall a. a -> Set a
S.singleton (StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a
Star (StarSemiring a -> StarSemiring a
forall a. Ord a => StarSemiring a -> StarSemiring a
normChild StarSemiring a
a))
    toSet StarSemiring a
a = StarSemiring a -> Set (StarSemiring a)
forall a. a -> Set a
S.singleton StarSemiring a
a

    fromSet :: Set (StarSemiring a) -> StarSemiring a
    fromSet :: forall a. Set (StarSemiring a) -> StarSemiring a
fromSet Set (StarSemiring a)
s = case Set (StarSemiring a) -> [StarSemiring a]
forall a. Set a -> [a]
S.toList Set (StarSemiring a)
s of
      [] -> StarSemiring a
forall a. StarSemiring a
Zero
      [StarSemiring a]
xs -> (StarSemiring a -> StarSemiring a -> StarSemiring a)
-> [StarSemiring a] -> StarSemiring a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 StarSemiring a -> StarSemiring a -> StarSemiring a
forall a. StarSemiring a -> StarSemiring a -> StarSemiring a
Plus [StarSemiring a]
xs