{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses,
	FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.OneOrMore.Internal (
	-- * Type
	OneOrMore,
	-- * Property
	-- ** Basic Property
	Projectable, Insertable,
	-- ** Expandable and Collapsable
	Expandable, Collapsable,
	-- ** Mergeable
	Mergeable, Selectable(..),
	-- * Function
	-- ** Single Type
	pattern Singleton, unSingleton,
	-- ** Multiple Type
	project, (>-), (>-.),
	-- ** Expand and Collapse
	expand, collapse,
	-- ** Merge
	merge, merge', merge_, merge_' ) where

import Data.Kind (Type)
import Data.Type.Set.Internal (Set(Nil, (:~)), Singleton, (:-), (:+:))

---------------------------------------------------------------------------

-- * ONE OR MORE TYPE
-- * BASIC PROPERTY
--	+ PROJECTABLE
--	+ INSERTABLE
-- * EXPANDABLE AND COLLAPSABLE
--	+ EXPANDABLE
--	+ COLLAPSABLE
--		- COLLAPSABLE 0
--		- COLLAPSABLE
-- * MERGEABLE

---------------------------------------------------------------------------
-- ONE OR MORE TYPE
---------------------------------------------------------------------------

data OneOrMore :: Set Type -> Type where
	Empty :: OneOrMore 'Nil
	(:.) :: Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)

---------------------------------------------------------------------------
-- BASIC PROPERTY
---------------------------------------------------------------------------

-- PROJECTABLE

class Projectable (as :: Set Type) a where project :: OneOrMore as -> Maybe a
instance Projectable 'Nil a where project :: OneOrMore 'Nil -> Maybe a
project OneOrMore 'Nil
_ = forall a. Maybe a
Nothing
instance Projectable (a ':~ as) a where project :: OneOrMore (a ':~ as) -> Maybe a
project (Maybe a
x :. OneOrMore as
_) = Maybe a
x
instance {-# OVERLAPPABLE #-} Projectable as a =>
	Projectable (a' ':~ as) a where project :: OneOrMore (a' ':~ as) -> Maybe a
project (Maybe a
_ :. OneOrMore as
xs) = forall (as :: Set (*)) a.
Projectable as a =>
OneOrMore as -> Maybe a
project OneOrMore as
xs

{-# COMPLETE Singleton #-}

pattern Singleton :: a -> OneOrMore (Singleton a)
pattern $bSingleton :: forall a. a -> OneOrMore (Singleton a)
$mSingleton :: forall {r} {a}.
OneOrMore (Singleton a) -> (a -> r) -> ((# #) -> r) -> r
Singleton x = Just x :. Empty

unSingleton :: OneOrMore (Singleton a) -> a
unSingleton :: forall a. OneOrMore (Singleton a) -> a
unSingleton (Singleton a
x) = a
x

-- INSERTABLE

infixr 5 >-

class Insertable a (as :: Set Type) (as' :: Set Type) where
	(>-.) :: a -> OneOrMore as -> OneOrMore as'

instance Insertable a as (a ':~ as) where a
x >-. :: a -> OneOrMore as -> OneOrMore (a ':~ as)
>-. OneOrMore as
xs = forall a. a -> Maybe a
Just a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. OneOrMore as
xs

instance {-# OVERLAPPABLE #-} Insertable a as as' =>
	Insertable a (a' ':~ as) (a' ':~ as') where
	a
x >-. :: a -> OneOrMore (a' ':~ as) -> OneOrMore (a' ':~ as')
>-. (Maybe a
y :. OneOrMore as
xs) = Maybe a
y forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. (a
x forall a (as :: Set (*)) (as' :: Set (*)).
Insertable a as as' =>
a -> OneOrMore as -> OneOrMore as'
>-. OneOrMore as
xs)

(>-) :: Insertable a as (a :- as) => a -> OneOrMore as -> OneOrMore (a :- as)
>- :: forall a (as :: Set (*)).
Insertable a as (a :- as) =>
a -> OneOrMore as -> OneOrMore (a :- as)
(>-) = forall a (as :: Set (*)) (as' :: Set (*)).
Insertable a as as' =>
a -> OneOrMore as -> OneOrMore as'
(>-.)

---------------------------------------------------------------------------
-- EXPANDABLE AND COLLAPSABLE
---------------------------------------------------------------------------

-- EXPANDABLE

class Expandable (as :: Set Type) (as' :: Set Type) where
	expand :: OneOrMore as -> OneOrMore as'

instance Nihil as => Expandable (a ':~ 'Nil) (a ':~ as) where
	expand :: OneOrMore (a ':~ 'Nil) -> OneOrMore (a ':~ as)
expand (Maybe a
x :. OneOrMore as
Empty) = Maybe a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)). Nihil as => OneOrMore as
nihil

instance {-# OVERLAPPABLE #-} Expandable as as' =>
	Expandable (a ':~ as) (a ':~ as') where
	expand :: OneOrMore (a ':~ as) -> OneOrMore (a ':~ as')
expand (Maybe a
x :. OneOrMore as
xs) = Maybe a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)).
Expandable as as' =>
OneOrMore as -> OneOrMore as'
expand OneOrMore as
xs

instance {-# OVERLAPPABLE #-} Expandable (a ':~ as) as' =>
	Expandable (a ':~ as) (a' ':~ as') where
	expand :: OneOrMore (a ':~ as) -> OneOrMore (a' ':~ as')
expand OneOrMore (a ':~ as)
xs = forall a. Maybe a
Nothing forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)).
Expandable as as' =>
OneOrMore as -> OneOrMore as'
expand OneOrMore (a ':~ as)
xs

class Nihil as where nihil :: OneOrMore as
instance Nihil 'Nil where nihil :: OneOrMore 'Nil
nihil = OneOrMore 'Nil
Empty
instance Nihil as => Nihil (a ':~ as) where nihil :: OneOrMore (a ':~ as)
nihil = forall a. Maybe a
Nothing forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)). Nihil as => OneOrMore as
nihil

-- COLLAPSABLE

-- COLLAPSABLE 0

class Collapsable0 (as :: Set Type) (as' :: Set Type) where
	collapse0 :: OneOrMore as -> OneOrMore as'

instance Collapsable0 as 'Nil where collapse0 :: OneOrMore as -> OneOrMore 'Nil
collapse0 = forall a b. a -> b -> a
const OneOrMore 'Nil
Empty

instance {-# OVERLAPPABLE #-} Collapsable0 as as' =>
	Collapsable0 (a ':~ as) (a ':~ as') where
	collapse0 :: OneOrMore (a ':~ as) -> OneOrMore (a ':~ as')
collapse0 (Maybe a
x :. OneOrMore as
xs) = Maybe a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)).
Collapsable0 as as' =>
OneOrMore as -> OneOrMore as'
collapse0 OneOrMore as
xs

instance {-# OVERLAPPABLE #-} Collapsable0 as (a' ':~ as') =>
	Collapsable0 (a ':~ as) (a' ':~ as') where
	collapse0 :: OneOrMore (a ':~ as) -> OneOrMore (a' ':~ as')
collapse0 (Maybe a
_ :. OneOrMore as
xs) = forall (as :: Set (*)) (as' :: Set (*)).
Collapsable0 as as' =>
OneOrMore as -> OneOrMore as'
collapse0 OneOrMore as
xs

-- COLLAPSABLE

class Collapsable (as :: Set Type) (as' :: Set Type) where
	collapse :: OneOrMore as -> Maybe (OneOrMore as')

instance Collapsable 'Nil 'Nil where collapse :: OneOrMore 'Nil -> Maybe (OneOrMore 'Nil)
collapse = forall a b. a -> b -> a
const forall a. Maybe a
Nothing

instance (Collapsable0 as as', Collapsable as as') =>
	Collapsable (a ':~ as) (a ':~ as') where
	collapse :: OneOrMore (a ':~ as) -> Maybe (OneOrMore (a ':~ as'))
collapse = \case
		Just a
x :. OneOrMore as
xs -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)).
Collapsable0 as as' =>
OneOrMore as -> OneOrMore as'
collapse0 OneOrMore as
xs
		Maybe a
Nothing :. OneOrMore as
xs -> (forall a. Maybe a
Nothing forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (as :: Set (*)) (as' :: Set (*)).
Collapsable as as' =>
OneOrMore as -> Maybe (OneOrMore as')
collapse OneOrMore as
xs

instance {-# OVERLAPPABLE #-} Collapsable as as' =>
	Collapsable (a ':~ as) as' where
	collapse :: OneOrMore (a ':~ as) -> Maybe (OneOrMore as')
collapse (Maybe a
_ :. OneOrMore as
xs) = forall (as :: Set (*)) (as' :: Set (*)).
Collapsable as as' =>
OneOrMore as -> Maybe (OneOrMore as')
collapse OneOrMore as
xs

---------------------------------------------------------------------------
-- MERGEABLE
---------------------------------------------------------------------------

class Mergeable (as :: Set Type) (as' :: Set Type) (mrg :: Set Type) where
	merge_ :: OneOrMore as -> OneOrMore as' -> OneOrMore mrg

instance Mergeable 'Nil 'Nil 'Nil where merge_ :: OneOrMore 'Nil -> OneOrMore 'Nil -> OneOrMore 'Nil
merge_ OneOrMore 'Nil
Empty OneOrMore 'Nil
Empty = OneOrMore 'Nil
Empty

instance (Selectable a, Mergeable as as' mrg) =>
	Mergeable (a ':~ as) (a ':~ as') (a ':~ mrg) where
	merge_ :: OneOrMore (a ':~ as)
-> OneOrMore (a ':~ as') -> OneOrMore (a ':~ mrg)
merge_ (Just a
x :. OneOrMore as
xs) (Just a
x' :. OneOrMore as
xs') =
		forall a. a -> Maybe a
Just (a
x forall a. Selectable a => a -> a -> a
`select` a
x') forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
merge_ OneOrMore as
xs OneOrMore as
xs'
	merge_ (Maybe a
mx :. OneOrMore as
xs) (Maybe a
Nothing :. OneOrMore as
xs') = Maybe a
mx forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
merge_ OneOrMore as
xs OneOrMore as
xs'
	merge_ (Maybe a
Nothing :. OneOrMore as
xs) (Maybe a
mx' :. OneOrMore as
xs') = Maybe a
mx' forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
merge_ OneOrMore as
xs OneOrMore as
xs'

instance {-# OVERLAPPABLE #-} Mergeable as as' mrg =>
	Mergeable (a ':~ as) as'  (a ':~ mrg) where
	merge_ :: OneOrMore (a ':~ as) -> OneOrMore as' -> OneOrMore (a ':~ mrg)
merge_ (Maybe a
x :. OneOrMore as
xs) OneOrMore as'
xs' = Maybe a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
merge_ OneOrMore as
xs OneOrMore as'
xs'

instance {-# OVERLAPPABLE #-} Mergeable as as' mrg =>
	Mergeable as (a ':~ as') (a ':~ mrg) where
	merge_ :: OneOrMore as -> OneOrMore (a ':~ as') -> OneOrMore (a ':~ mrg)
merge_ OneOrMore as
xs (Maybe a
x :. OneOrMore as
xs') = Maybe a
x forall a (as :: Set (*)).
Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)
:. forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
merge_ OneOrMore as
xs OneOrMore as
xs'

class Selectable a where select :: a -> a -> a
instance {-# OVERLAPPABLE #-} Ord a => Selectable a where select :: a -> a -> a
select = forall a. Ord a => a -> a -> a
min

merge_' :: (Mergeable as as' mrg, Expandable as mrg, Expandable as' mrg ) =>
	Maybe (OneOrMore as) -> Maybe (OneOrMore as') -> Maybe (OneOrMore mrg)
Maybe (OneOrMore as)
ml merge_' :: forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
(Mergeable as as' mrg, Expandable as mrg, Expandable as' mrg) =>
Maybe (OneOrMore as)
-> Maybe (OneOrMore as') -> Maybe (OneOrMore mrg)
`merge_'` Maybe (OneOrMore as')
mr = case (Maybe (OneOrMore as)
ml, Maybe (OneOrMore as')
mr) of
	(Just OneOrMore as
l, Just OneOrMore as'
r) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ OneOrMore as
l forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
`merge_` OneOrMore as'
r
	(Just OneOrMore as
l, Maybe (OneOrMore as')
Nothing) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (as :: Set (*)) (as' :: Set (*)).
Expandable as as' =>
OneOrMore as -> OneOrMore as'
expand OneOrMore as
l
	(Maybe (OneOrMore as)
Nothing, Just OneOrMore as'
r) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (as :: Set (*)) (as' :: Set (*)).
Expandable as as' =>
OneOrMore as -> OneOrMore as'
expand OneOrMore as'
r
	(Maybe (OneOrMore as)
Nothing, Maybe (OneOrMore as')
Nothing) -> forall a. Maybe a
Nothing

merge :: Mergeable as as' (as :+: as') =>
	OneOrMore as -> OneOrMore as' -> OneOrMore (as :+: as')
merge :: forall (as :: Set (*)) (as' :: Set (*)).
Mergeable as as' (as :+: as') =>
OneOrMore as -> OneOrMore as' -> OneOrMore (as :+: as')
merge = forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
Mergeable as as' mrg =>
OneOrMore as -> OneOrMore as' -> OneOrMore mrg
merge_

merge' :: (
	Mergeable as as' (as :+: as'),
	Expandable as (as :+: as'), Expandable as' (as :+: as') ) =>
	Maybe (OneOrMore as) -> Maybe (OneOrMore as') -> Maybe (OneOrMore (as :+: as'))
merge' :: forall (as :: Set (*)) (as' :: Set (*)).
(Mergeable as as' (as :+: as'), Expandable as (as :+: as'),
 Expandable as' (as :+: as')) =>
Maybe (OneOrMore as)
-> Maybe (OneOrMore as') -> Maybe (OneOrMore (as :+: as'))
merge' = forall (as :: Set (*)) (as' :: Set (*)) (mrg :: Set (*)).
(Mergeable as as' mrg, Expandable as mrg, Expandable as' mrg) =>
Maybe (OneOrMore as)
-> Maybe (OneOrMore as') -> Maybe (OneOrMore mrg)
merge_'