Positive.hs

{-# LANGUAGE DeriveLift #-}
{-# OPTIONS_GHC -Wall #-}

{- | A whole number greater than zero.

The constructor is not exported (see "ReOC.Primitive.Text1"). A @Positive@
is built with the prism '_Positive' or with 'positiveLiteral'.
-}
module ReOC.Primitive.Positive (
  Positive,
  _Positive,
  positiveNatural,
  positiveLiteral,
) where

import Control.Lens (Prism', preview, prism')
import Language.Haskell.TH.Syntax (Code (..), Lift, Q, liftTyped)
import Numeric.Natural (Natural)

{- $setup
>>> import Control.Lens ((^?))
-}

-- | A whole number greater than zero.
newtype Positive
  = Positive Natural
  deriving (Eq, Ord, Show, Lift)

{- | A whole number greater than zero.

>>> (3 :: Natural) ^? _Positive
Just (Positive 3)

>>> (0 :: Natural) ^? _Positive
Nothing
-}
_Positive :: Prism' Natural Positive
_Positive =
  prism'
    positiveNatural
    (\n -> if n > 0 then Just (Positive n) else Nothing)

-- | The number of a @Positive@.
positiveNatural :: Positive -> Natural
positiveNatural (Positive n) =
  n

{- | A @Positive@ literal, checked when the program is compiled:

> $$(positiveLiteral 90)
-}
positiveLiteral :: Natural -> Code Q Positive
positiveLiteral n =
  maybe
    (Code (fail "positiveLiteral: 0 is not positive"))
    liftTyped
    (preview _Positive n)