{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}

-- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@
module Data.Type.Natural
  ( -- * Type-level naturals

    -- ** @Nat@, singletons and KnownNat manipulation,
    Nat,
    KnownNat,
    SNat (Succ, Zero),
    sNat,
    sNatP,
    toNatural,
    SomeSNat (..),
    toSomeSNat,
    withSNat,
    withKnownNat,
    fromSNat,
    natVal,
    natVal',
    someNatVal,
    SomeNat (..),
    (%~),
    Equality (..),
    type (===),

    -- *** Pattens and Views
    viewNat,
    zeroOrSucc,
    ZeroOrSucc (..),

    -- ** Promtoed and singletonised operations

    -- *** Arithmetic
    Succ,
    sSucc,
    S,
    Pred,
    sPred,
    sS,
    Zero,
    sZero,
    One,
    sOne,
    type (+),
    (%+),
    type (-),
    (%-),
    type (*),
    (%*),
    Div,
    sDiv,
    Mod,
    sMod,
    type (^),
    (%^),
    type (-.),
    (%-.),
    Log2,
    sLog2,

    -- *** Ordering
    type (<=?),
    type (<=),
    (%<=?),
    type (<?),
    type (<),
    (%<?),
    type (>=?),
    type (>=),
    (%>=?),
    type (>?),
    type (>),
    (%>?),
    CmpNat,
    sCmpNat,
    sCompare,
    Min,
    sMin,
    Max,
    sMax,
    induction,

    -- * QuasiQuotes
    snat,

    -- * Singletons for auxiliary types
    SBool (..),
    SOrdering (..),
    OrderingI(..),
    fromOrderingI,
    toOrderingI,
    FlipOrdering,
    sFlipOrdering,
  )
where

import Data.Proxy (Proxy)
import Data.Type.Natural.Core
import Data.Type.Natural.Lemma.Arithmetic
import Data.Type.Natural.Lemma.Order
import Language.Haskell.TH (litT, numTyLit)
import Language.Haskell.TH.Quote
import Text.Read (readMaybe)
import Data.Ord (comparing)
import Data.Function (on)

{- | Quotesi-quoter for SNatleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression.

  For example: @[snat|12|] '%+' [snat| 5 |]@.
-}
snat :: QuasiQuoter
snat :: QuasiQuoter
snat =
  QuasiQuoter
    { quoteExp :: String -> Q Exp
quoteExp = \String
str ->
        case String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
str of
          Just Integer
n -> [|sNat :: SNat $(Q TyLit -> Q Type
forall (m :: Type -> Type). Quote m => m TyLit -> m Type
litT (Q TyLit -> Q Type) -> Q TyLit -> Q Type
forall a b. (a -> b) -> a -> b
$ Integer -> Q TyLit
forall (m :: Type -> Type). Quote m => Integer -> m TyLit
numTyLit Integer
n)|]
          Maybe Integer
Nothing -> String -> Q Exp
forall a. HasCallStack => String -> a
error String
"Must be natural literal"
    , quotePat :: String -> Q Pat
quotePat = \String
str ->
        case String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
str of
          Just Integer
n -> [p|((%~ (sNat :: SNat $(Q TyLit -> Q Type
forall (m :: Type -> Type). Quote m => m TyLit -> m Type
litT (Q TyLit -> Q Type) -> Q TyLit -> Q Type
forall a b. (a -> b) -> a -> b
$ Integer -> Q TyLit
forall (m :: Type -> Type). Quote m => Integer -> m TyLit
numTyLit Integer
n))) -> Equal)|]
          Maybe Integer
Nothing -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"Must be natural literal"
    , quoteType :: String -> Q Type
quoteType = \String
str ->
        case String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
str of
          Just Integer
n -> Q TyLit -> Q Type
forall (m :: Type -> Type). Quote m => m TyLit -> m Type
litT (Q TyLit -> Q Type) -> Q TyLit -> Q Type
forall a b. (a -> b) -> a -> b
$ Integer -> Q TyLit
forall (m :: Type -> Type). Quote m => Integer -> m TyLit
numTyLit Integer
n
          Maybe Integer
Nothing -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"Must be natural literal"
    , quoteDec :: String -> Q [Dec]
quoteDec = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"No declaration Quotes for Nat"
    }

toNatural :: SNat n -> Natural
{-# DEPRECATED toNatural "Use fromSNat instead" #-}
toNatural :: forall (n :: Nat). SNat n -> Nat
toNatural = SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat

data SomeSNat where
  SomeSNat :: KnownNat n => SNat n -> SomeSNat

deriving instance Show SomeSNat

instance Eq SomeSNat where
  == :: SomeSNat -> SomeSNat -> Bool
(==) = Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Nat -> Nat -> Bool)
-> (SomeSNat -> Nat) -> SomeSNat -> SomeSNat -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` \(SomeSNat SNat n
n) -> SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n
  {-# INLINE (==) #-}

instance Ord SomeSNat where
  compare :: SomeSNat -> SomeSNat -> Ordering
compare = (SomeSNat -> Nat) -> SomeSNat -> SomeSNat -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (\(SomeSNat SNat n
n) -> SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n)
  {-# INLINE compare #-}

toSomeSNat :: Natural -> SomeSNat
toSomeSNat :: Nat -> SomeSNat
toSomeSNat Nat
n = case Nat -> SomeNat
someNatVal Nat
n of
  SomeNat Proxy n
pn -> SNat n -> (KnownNat n => SomeSNat) -> SomeSNat
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => SomeSNat) -> SomeSNat)
-> (KnownNat n => SomeSNat) -> SomeSNat
forall a b. (a -> b) -> a -> b
$ SNat n -> SomeSNat
forall (n :: Nat). KnownNat n => SNat n -> SomeSNat
SomeSNat SNat n
sn
    where
      sn :: SNat n
sn = Proxy n -> SNat n
forall (n :: Nat) (pxy :: Nat -> Type).
KnownNat n =>
pxy n -> SNat n
sNatP Proxy n
pn

withSNat :: Natural -> (forall n. KnownNat n => SNat n -> r) -> r
withSNat :: forall r.
Nat -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Nat
n forall (n :: Nat). KnownNat n => SNat n -> r
act = case Nat -> SomeNat
someNatVal Nat
n of
  SomeNat (Proxy n
pn :: Proxy n) -> SNat n -> (KnownNat n => r) -> r
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => r) -> r) -> (KnownNat n => r) -> r
forall a b. (a -> b) -> a -> b
$ SNat n -> r
forall (n :: Nat). KnownNat n => SNat n -> r
act SNat n
sn
    where
      sn :: SNat n
sn = Proxy n -> SNat n
forall (n :: Nat) (pxy :: Nat -> Type).
KnownNat n =>
pxy n -> SNat n
sNatP Proxy n
pn

sNatP :: KnownNat n => pxy n -> SNat n
sNatP :: forall (n :: Nat) (pxy :: Nat -> Type).
KnownNat n =>
pxy n -> SNat n
sNatP = SNat n -> pxy n -> SNat n
forall a b. a -> b -> a
const SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat