{-# 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 #-}
module Data.Type.Natural
(
Nat,
KnownNat,
SNat (Succ, Zero),
sNat,
sNatP,
toNatural,
SomeSNat (..),
toSomeSNat,
withSNat,
withKnownNat,
natVal,
natVal',
someNatVal,
SomeNat (..),
(%~),
Equality (..),
type (===),
viewNat,
zeroOrSucc,
ZeroOrSucc (..),
Succ,
sSucc,
S,
Pred,
sPred,
sS,
Zero,
sZero,
One,
sOne,
type (+),
(%+),
type (-),
(%-),
type (*),
(%*),
Div,
sDiv,
Mod,
sMod,
type (^),
(%^),
type (-.),
(%-.),
Log2,
sLog2,
type (<=?),
type (<=),
(%<=?),
type (<?),
type (<),
(%<?),
type (>=?),
type (>=),
(%>=?),
type (>?),
type (>),
(%>?),
CmpNat,
sCmpNat,
sCompare,
Min,
sMin,
Max,
sMax,
induction,
snat,
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)
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