{-# 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,
    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 (..),
    FlipOrdering,
    sFlipOrdering,
  )
where

import Data.Coerce (coerce)
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 Numeric.Natural
import Text.Read (readMaybe)

{- | 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 :: (String -> Q Exp)
-> (String -> Q Pat)
-> (String -> Q Type)
-> (String -> Q [Dec])
-> QuasiQuoter
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 $(litT $ numTyLit 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 $(litT $ numTyLit 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 -> TyLitQ -> Q Type
litT (TyLitQ -> Q Type) -> TyLitQ -> Q Type
forall a b. (a -> b) -> a -> b
$ Integer -> TyLitQ
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
toNatural :: SNat n -> Natural
toNatural = SNat n -> Natural
coerce

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

deriving instance Show SomeSNat

instance Eq SomeSNat where
  SomeSNat (SNat Natural
n) == :: SomeSNat -> SomeSNat -> Bool
== SomeSNat (SNat Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m
  SomeSNat (SNat Natural
n) /= :: SomeSNat -> SomeSNat -> Bool
/= SomeSNat (SNat Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
m

toSomeSNat :: Natural -> SomeSNat
toSomeSNat :: Natural -> SomeSNat
toSomeSNat Natural
n = case Natural -> SomeNat
someNatVal Natural
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 :: Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Natural
n forall (n :: Nat). KnownNat n => SNat n -> r
act = case Natural -> SomeNat
someNatVal Natural
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 :: 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