{-# LANGUAGE Strict #-}

module Agda.Utils.StrictEndo where

import Agda.Utils.ExpandCase
import GHC.Exts (oneShot)

newtype Endo a = Endo {forall a. Endo a -> a -> a
appEndo :: a -> a}

instance Semigroup (Endo a) where
  {-# INLINE (<>) #-}
  Endo a -> a
f <> :: Endo a -> Endo a -> Endo a
<> Endo a -> a
g = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo ((a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
oneShot (\a
a -> case a -> a
g a
a of a
b -> a -> a
f a
b))

instance Monoid (Endo a) where
  {-# INLINE mempty #-}
  mempty :: Endo a
mempty = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo \a
a -> a
a

instance ExpandCase (Endo a) where
  type Result (Endo a) = a
  {-# INLINE expand #-}
  expand :: ((Endo a -> Result (Endo a)) -> Result (Endo a)) -> Endo a
expand (Endo a -> Result (Endo a)) -> Result (Endo a)
k = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo ((a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
oneShot \a
a -> (Endo a -> Result (Endo a)) -> Result (Endo a)
k ((Endo a -> a) -> Endo a -> a
forall a b. (a -> b) -> a -> b
oneShot \Endo a
act -> Endo a -> a -> a
forall a. Endo a -> a -> a
appEndo Endo a
act a
a))