AtMost.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}

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

The constructor is not exported (see "ReOC.Primitive.Text1"). @AtMost@ is
built with the prism '_AtMost' or, for no values, with 'atMostNone'. It is
'Traversable', so that its values can be changed without changing how many
there are.
-}
module ReOC.Primitive.AtMost (
  AtMost,
  _AtMost,
  atMostList,
  atMostNone,
) where

import Control.Lens (Prism', prism')
import Data.Proxy (Proxy (..))
import GHC.TypeNats (KnownNat, Nat, natVal)

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

-- | From 0 to @n@ values.
newtype AtMost (n :: Nat) a
  = AtMost [a]
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

{- | From 0 to @n@ values.

>>> "ab" ^? _AtMost @2
Just (AtMost "ab")

>>> "abc" ^? _AtMost @2
Nothing
-}
_AtMost :: forall n a. (KnownNat n) => Prism' [a] (AtMost n a)
_AtMost =
  prism'
    atMostList
    (\xs -> if fromIntegral (length xs) <= natVal (Proxy :: Proxy n) then Just (AtMost xs) else Nothing)

-- | The values.
atMostList :: AtMost n a -> [a]
atMostList (AtMost xs) =
  xs

-- | No values.
atMostNone :: AtMost n a
atMostNone =
  AtMost []