module Morley.Util.PeanoNatural
( PeanoNatural (Zero, Succ, One, Two)
, toPeanoNatural
, toPeanoNatural'
, fromPeanoNatural
, singPeanoVal
, eqPeanoNat
, singPeanoNat
) where
import Data.Singletons (SingI(..))
import Data.Type.Equality (TestEquality(..), (:~:))
import GHC.TypeNats (Nat)
import Morley.Util.Peano (Peano, SingIPeano, SingNat(..), ToPeano, pattern S, pattern Z)
import Text.PrettyPrint.Leijen.Text (integer)
import Morley.Michelson.Printer.Util
data PeanoNatural (n :: Peano) = PN !(SingNat n) !Natural
deriving stock instance Show (PeanoNatural n)
deriving stock instance Eq (PeanoNatural n)
instance RenderDoc (PeanoNatural n) where
renderDoc :: RenderContext -> PeanoNatural n -> Doc
renderDoc RenderContext
_ = Integer -> Doc
integer (Integer -> Doc)
-> (PeanoNatural n -> Integer) -> PeanoNatural n -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer)
-> (PeanoNatural n -> Natural) -> PeanoNatural n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PeanoNatural n -> Natural
forall (n :: Nat). PeanoNatural n -> Natural
fromPeanoNatural
instance NFData (PeanoNatural n) where
rnf :: PeanoNatural n -> ()
rnf (PN SingNat n
s Natural
_) = SingNat n -> ()
forall a. NFData a => a -> ()
rnf SingNat n
s
data MatchPS n where
PS_Match :: PeanoNatural n -> MatchPS ('S n)
PS_Mismatch :: MatchPS n
matchPS :: PeanoNatural n -> MatchPS n
matchPS :: forall (n :: Nat). PeanoNatural n -> MatchPS n
matchPS (PN (SS Sing n
m) Natural
k) = PeanoNatural n -> MatchPS ('S n)
forall (n :: Nat). PeanoNatural n -> MatchPS ('S n)
PS_Match (SingNat n -> Natural -> PeanoNatural n
forall (n :: Nat). SingNat n -> Natural -> PeanoNatural n
PN Sing n
SingNat n
m (Natural
k Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1))
matchPS PeanoNatural n
_ = MatchPS n
forall (n :: Nat). MatchPS n
PS_Mismatch
pattern Zero :: () => (n ~ 'Z) => PeanoNatural n
pattern $bZero :: forall (n :: Nat). (n ~ 'Z) => PeanoNatural n
$mZero :: forall {r} {n :: Nat}.
PeanoNatural n -> ((n ~ 'Z) => r) -> (Void# -> r) -> r
Zero = PN SZ 0
pattern Succ :: () => (n ~ 'S m) => PeanoNatural m -> PeanoNatural n
pattern $bSucc :: forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
$mSucc :: forall {r} {n :: Nat}.
PeanoNatural n
-> (forall {m :: Nat}. (n ~ 'S m) => PeanoNatural m -> r)
-> (Void# -> r)
-> r
Succ s <- (matchPS -> PS_Match s) where
Succ (PN SingNat m
n Natural
k) = SingNat ('S m) -> Natural -> PeanoNatural ('S m)
forall (n :: Nat). SingNat n -> Natural -> PeanoNatural n
PN (Sing m -> SingNat ('S m)
forall (n :: Nat). Sing n -> SingNat ('S n)
SS Sing m
SingNat m
n) (Natural
kNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
1)
{-# COMPLETE Zero, Succ #-}
pattern One :: () => (n ~ ('S 'Z)) => PeanoNatural n
pattern $bOne :: forall (n :: Nat). (n ~ 'S 'Z) => PeanoNatural n
$mOne :: forall {r} {n :: Nat}.
PeanoNatural n -> ((n ~ 'S 'Z) => r) -> (Void# -> r) -> r
One = Succ Zero
pattern Two :: () => (n ~ ('S ('S 'Z))) => PeanoNatural n
pattern $bTwo :: forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
$mTwo :: forall {r} {n :: Nat}.
PeanoNatural n -> ((n ~ 'S ('S 'Z)) => r) -> (Void# -> r) -> r
Two = Succ One
fromPeanoNatural :: forall n. PeanoNatural n -> Natural
fromPeanoNatural :: forall (n :: Nat). PeanoNatural n -> Natural
fromPeanoNatural (PN SingNat n
_ Natural
n) = Natural
n
singPeanoVal :: forall (n :: Peano). SingNat n -> Natural
singPeanoVal :: forall (n :: Nat). SingNat n -> Natural
singPeanoVal = \case
SingNat n
SZ -> Natural
0
SS Sing n
a -> Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ SingNat n -> Natural
forall (n :: Nat). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
a
toPeanoNatural :: forall n. SingI n => PeanoNatural n
toPeanoNatural :: forall (n :: Nat). SingI n => PeanoNatural n
toPeanoNatural = let pSing :: Sing n
pSing = forall {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @n in
SingNat n -> Natural -> PeanoNatural n
forall (n :: Nat). SingNat n -> Natural -> PeanoNatural n
PN Sing n
SingNat n
pSing (Natural -> PeanoNatural n) -> Natural -> PeanoNatural n
forall a b. (a -> b) -> a -> b
$ SingNat n -> Natural
forall (n :: Nat). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
pSing
toPeanoNatural'
:: forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' :: forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' = forall (n :: Nat). SingI n => PeanoNatural n
toPeanoNatural @(ToPeano n)
eqPeanoNat :: PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)
eqPeanoNat :: forall (a :: Nat) (b :: Nat).
PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)
eqPeanoNat (PN SingNat a
a Natural
_) (PN SingNat b
b Natural
_) = SingNat a -> SingNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SingNat a
a SingNat b
b
singPeanoNat :: PeanoNatural a -> SingNat a
singPeanoNat :: forall (a :: Nat). PeanoNatural a -> SingNat a
singPeanoNat (PN SingNat a
n Natural
_) = SingNat a
n