{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--aux-inline" @-}
{-@ LIQUID "--ple" @-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Maybe.Semigroup where
import           Prelude                 hiding ( Functor(..)
                                                , Applicative(..)
                                                , Monad(..)
                                                , Foldable(..)
                                                , Maybe(..)
                                                , Monoid(..)
                                                , Semigroup(..)
                                                , Either(..)
                                                , id
                                                , flip
                                                , const
                                                , apply
                                                )
import           Liquid.ProofCombinators
import Data.Function
import Data.Maybe
import Data.Semigroup.Classes
import Data.List.NonEmpty
import Data.List


instance Semigroup (First a) where
  First Nothing `mappend` b = b
  a `mappend` _ = a
  sconcat (NonEmpty h t) = foldlList mappend h t

instance VSemigroup (First a) where
  lawAssociative _ _ _ = ()
  lawSconcat _ = ()

instance Monoid (First a) where
  mempty = First Nothing
  mconcat = foldrList mappend mempty

instance VMonoid (First a) where
  lawEmpty (First Nothing) = ()
  lawEmpty _ = ()
  lawMconcat _ = ()


instance Semigroup (Last a) where
  a `mappend` Last Nothing = a
  _ `mappend` b = b
  sconcat (NonEmpty h t) = foldlList mappend h t

instance VSemigroup (Last a) where
  lawAssociative _ _ _ = ()
  lawSconcat _ = ()

instance Monoid (Last a) where
  mempty = Last Nothing
  mconcat = foldrList mappend mempty

instance VMonoid (Last a) where
  lawEmpty (Last Nothing) = ()
  lawEmpty _ = ()
  lawMconcat _ = ()

-- -- Dual First and Last are isomorphic
instance Semigroup a => Semigroup (Maybe a) where
  Nothing `mappend` b = b
  a `mappend` Nothing = a
  Just a `mappend` Just b = Just (a `mappend` b)
  sconcat (NonEmpty h t) = foldlList mappend h t
  
  
instance Semigroup a => Monoid (Maybe a) where
  mempty = Nothing
  mconcat = foldrList mappend mempty

instance VSemigroup a => VSemigroup (Maybe a) where
  lawAssociative (Just x) (Just y) (Just z) = lawAssociative x y z
  lawAssociative _ _ _ = ()
  lawSconcat _ = ()

instance VMonoid a => VMonoid (Maybe a) where
  lawMconcat xs = mconcat xs `cast` ()
  lawEmpty Nothing = ()
  
  lawEmpty (Just x) = () -- lawEmpty x `cast` ()