{-# LANGUAGE UndecidableInstances #-}

-- | Provides the 'UniqueSeqNE' type.
module Charon.Data.UniqueSeqNE.Internal
  ( -- * Type
    UniqueSeqNE (MkUniqueSeqNE, ..),

    -- * Operations
    union,

    -- * Utils
    notHSetMember,
  )
where

import Charon.Prelude
import Data.HashSet qualified as HSet
import Data.Sequence qualified as Seq

-- | Like 'UniqueSeq' except carries the invariant that it is non-empty.
data UniqueSeqNE a = UnsafeUniqueSeqNE
  { forall a. UniqueSeqNE a -> NESeq a
seq :: NESeq a,
    forall a. UniqueSeqNE a -> HashSet a
set :: HashSet a
  }
  deriving stock (UniqueSeqNE a -> UniqueSeqNE a -> Bool
(UniqueSeqNE a -> UniqueSeqNE a -> Bool)
-> (UniqueSeqNE a -> UniqueSeqNE a -> Bool) -> Eq (UniqueSeqNE a)
forall a. Eq a => UniqueSeqNE a -> UniqueSeqNE a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => UniqueSeqNE a -> UniqueSeqNE a -> Bool
== :: UniqueSeqNE a -> UniqueSeqNE a -> Bool
$c/= :: forall a. Eq a => UniqueSeqNE a -> UniqueSeqNE a -> Bool
/= :: UniqueSeqNE a -> UniqueSeqNE a -> Bool
Eq, Int -> UniqueSeqNE a -> ShowS
[UniqueSeqNE a] -> ShowS
UniqueSeqNE a -> String
(Int -> UniqueSeqNE a -> ShowS)
-> (UniqueSeqNE a -> String)
-> ([UniqueSeqNE a] -> ShowS)
-> Show (UniqueSeqNE a)
forall a. Show a => Int -> UniqueSeqNE a -> ShowS
forall a. Show a => [UniqueSeqNE a] -> ShowS
forall a. Show a => UniqueSeqNE a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> UniqueSeqNE a -> ShowS
showsPrec :: Int -> UniqueSeqNE a -> ShowS
$cshow :: forall a. Show a => UniqueSeqNE a -> String
show :: UniqueSeqNE a -> String
$cshowList :: forall a. Show a => [UniqueSeqNE a] -> ShowS
showList :: [UniqueSeqNE a] -> ShowS
Show)

pattern MkUniqueSeqNE :: NESeq a -> HashSet a -> UniqueSeqNE a
pattern $mMkUniqueSeqNE :: forall {r} {a}.
UniqueSeqNE a -> (NESeq a -> HashSet a -> r) -> ((# #) -> r) -> r
MkUniqueSeqNE seq set <- UnsafeUniqueSeqNE seq set

{-# COMPLETE MkUniqueSeqNE #-}

instance Foldable UniqueSeqNE where
  foldr :: forall a b. (a -> b -> b) -> b -> UniqueSeqNE a -> b
foldr a -> b -> b
f b
x (UnsafeUniqueSeqNE NESeq a
seq HashSet a
_) = (a -> b -> b) -> b -> NESeq a -> b
forall a b. (a -> b -> b) -> b -> NESeq a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
x NESeq a
seq

instance (Hashable a) => Semigroup (UniqueSeqNE a) where
  <> :: UniqueSeqNE a -> UniqueSeqNE a -> UniqueSeqNE a
(<>) = UniqueSeqNE a -> UniqueSeqNE a -> UniqueSeqNE a
forall a.
Hashable a =>
UniqueSeqNE a -> UniqueSeqNE a -> UniqueSeqNE a
union

instance
  (k ~ A_Getter, b ~ NESeq a, c ~ NESeq a) =>
  LabelOptic "seq" k (UniqueSeqNE a) (UniqueSeqNE a) b c
  where
  labelOptic :: Optic k NoIx (UniqueSeqNE a) (UniqueSeqNE a) b c
labelOptic = (UniqueSeqNE a -> b) -> Getter (UniqueSeqNE a) b
forall s a. (s -> a) -> Getter s a
to (\(UnsafeUniqueSeqNE NESeq a
seq HashSet a
_) -> b
NESeq a
seq)

instance
  (k ~ A_Getter, b ~ HashSet a, c ~ HashSet a) =>
  LabelOptic "set" k (UniqueSeqNE a) (UniqueSeqNE a) b c
  where
  labelOptic :: Optic k NoIx (UniqueSeqNE a) (UniqueSeqNE a) b c
labelOptic = (UniqueSeqNE a -> b) -> Getter (UniqueSeqNE a) b
forall s a. (s -> a) -> Getter s a
to (\(UnsafeUniqueSeqNE NESeq a
_ HashSet a
set) -> b
HashSet a
set)

union :: forall a. (Hashable a) => UniqueSeqNE a -> UniqueSeqNE a -> UniqueSeqNE a
union :: forall a.
Hashable a =>
UniqueSeqNE a -> UniqueSeqNE a -> UniqueSeqNE a
union (UnsafeUniqueSeqNE (a
x :<|| Seq a
xseq) HashSet a
_) (UnsafeUniqueSeqNE (a
y :<|| Seq a
yseq) HashSet a
_) =
  NESeq a -> HashSet a -> UniqueSeqNE a
forall a. NESeq a -> HashSet a -> UniqueSeqNE a
UnsafeUniqueSeqNE (a
x a -> Seq a -> NESeq a
forall a. a -> Seq a -> NESeq a
:<|| Seq a
newSeq) HashSet a
newSet
  where
    -- Given union (x : xs) (y : ys), we want (x : xs <> y : ys), eliminating
    -- duplicates. To do this, we iterate through (xs <> y : ys), building our
    -- new Seq/Set, only prepending x at the end.
    (Seq a
newSeq, HashSet a
newSet) = ((Seq a, HashSet a) -> a -> (Seq a, HashSet a))
-> (Seq a, HashSet a) -> Seq a -> (Seq a, HashSet a)
forall b a. (b -> a -> b) -> b -> Seq a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Seq a, HashSet a) -> a -> (Seq a, HashSet a)
go (Seq a
forall a. Seq a
Seq.empty, a -> HashSet a
forall a. Hashable a => a -> HashSet a
HSet.singleton a
x) (Seq a
xseq Seq a -> Seq a -> Seq a
forall a. Semigroup a => a -> a -> a
<> (a
y a -> Seq a -> Seq a
forall a. a -> Seq a -> Seq a
:<| Seq a
yseq))

    go :: (Seq a, HashSet a) -> a -> (Seq a, HashSet a)
    go :: (Seq a, HashSet a) -> a -> (Seq a, HashSet a)
go (Seq a
accSeq, HashSet a
accSet) a
z
      | a -> HashSet a -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
notHSetMember a
z HashSet a
accSet = (Seq a
accSeq Seq a -> a -> Seq a
forall a. Seq a -> a -> Seq a
:|> a
z, a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HSet.insert a
z HashSet a
accSet)
      | Bool
otherwise = (Seq a
accSeq, HashSet a
accSet)

notHSetMember :: (Hashable a) => a -> HashSet a -> Bool
notHSetMember :: forall a. Hashable a => a -> HashSet a -> Bool
notHSetMember a
x = Bool -> Bool
not (Bool -> Bool) -> (HashSet a -> Bool) -> HashSet a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> HashSet a -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HSet.member a
x