Some.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
-- someOne has a constraint (1 <= n) that its body does not use, by design.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

{- | From 1 to @n@ values: as many as a part of a document has room for, such
as the rows of a table of CASA Form 101-02.

The constructor is not exported (see "ReOC.Primitive.Text1"). @Some@ is
built with the prism '_Some' or, for one value, with 'someOne'. It is
'Traversable', so that its values can be changed without changing how many
there are.
-}
module ReOC.Primitive.Some (
  Some,
  _Some,
  someNonEmpty,
  someOne,
) where

import Control.Lens (Prism', prism')
import Data.List.NonEmpty (NonEmpty (..))
import Data.Proxy (Proxy (..))
import GHC.TypeNats (KnownNat, Nat, natVal, type (<=))

{- $setup
>>> :set -XDataKinds
>>> :set -XTypeApplications
>>> import Control.Lens ((^?))
-}

-- | From 1 to @n@ values.
newtype Some (n :: Nat) a
  = Some (NonEmpty a)
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

{- | From 1 to @n@ values.

>>> ('a' :| "bc") ^? _Some @3
Just (Some ('a' :| "bc"))

>>> ('a' :| "bcd") ^? _Some @3
Nothing
-}
_Some :: forall n a. (KnownNat n) => Prism' (NonEmpty a) (Some n a)
_Some =
  prism'
    someNonEmpty
    (\xs -> if fromIntegral (length xs) <= natVal (Proxy :: Proxy n) then Just (Some xs) else Nothing)

-- | The values.
someNonEmpty :: Some n a -> NonEmpty a
someNonEmpty (Some xs) =
  xs

-- | One value.
someOne :: (1 <= n) => a -> Some n a
someOne x =
  Some (x :| [])