{-|
Copyright        : (c) Galois, Inc 2014-2018
Maintainer       : Joe Hendrix <jhendrix@galois.com>

This internal module exports the 'NatRepr' type and its constructor. It is intended
for use only within parameterized-utils, and is excluded from the module export list.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Data.Parameterized.NatRepr.Internal where

import Data.Data
import Data.Hashable
import GHC.TypeNats
import Numeric.Natural
import Unsafe.Coerce

import Data.Parameterized.Classes
import Data.Parameterized.DecidableEq

------------------------------------------------------------------------
-- Nat

-- | A runtime presentation of a type-level 'Nat'.
--
-- This can be used for performing dynamic checks on a type-level natural
-- numbers.
newtype NatRepr (n::Nat) = NatRepr { NatRepr n -> Natural
natValue :: Natural
                                     -- ^ The underlying natural value of the number.
                                   }
  deriving (Int -> NatRepr n -> Int
NatRepr n -> Int
(Int -> NatRepr n -> Int)
-> (NatRepr n -> Int) -> Hashable (NatRepr n)
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall (n :: Nat). Int -> NatRepr n -> Int
forall (n :: Nat). NatRepr n -> Int
hash :: NatRepr n -> Int
$chash :: forall (n :: Nat). NatRepr n -> Int
hashWithSalt :: Int -> NatRepr n -> Int
$chashWithSalt :: forall (n :: Nat). Int -> NatRepr n -> Int
Hashable, Typeable (NatRepr n)
DataType
Constr
Typeable (NatRepr n)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NatRepr n))
-> (NatRepr n -> Constr)
-> (NatRepr n -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NatRepr n)))
-> ((forall b. Data b => b -> b) -> NatRepr n -> NatRepr n)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r)
-> (forall u. (forall d. Data d => d -> u) -> NatRepr n -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> NatRepr n -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n))
-> Data (NatRepr n)
NatRepr n -> DataType
NatRepr n -> Constr
(forall b. Data b => b -> b) -> NatRepr n -> NatRepr n
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NatRepr n)
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NatRepr n -> u
forall u. (forall d. Data d => d -> u) -> NatRepr n -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
forall (n :: Nat). KnownNat n => Typeable (NatRepr n)
forall (n :: Nat). KnownNat n => NatRepr n -> DataType
forall (n :: Nat). KnownNat n => NatRepr n -> Constr
forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> NatRepr n -> NatRepr n
forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> NatRepr n -> u
forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> NatRepr n -> [u]
forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
forall (n :: Nat) (m :: * -> *).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NatRepr n)
forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)
forall (n :: Nat) (t :: * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (NatRepr n))
forall (n :: Nat) (t :: * -> * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NatRepr n))
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NatRepr n)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (NatRepr n))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NatRepr n))
$cNatRepr :: Constr
$tNatRepr :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
$cgmapMo :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
gmapMp :: (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
$cgmapMp :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
gmapM :: (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
$cgmapM :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)
gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u
$cgmapQi :: forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> NatRepr n -> u
gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u]
$cgmapQ :: forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> NatRepr n -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
$cgmapQr :: forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
$cgmapQl :: forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NatRepr n -> r
gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n
$cgmapT :: forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> NatRepr n -> NatRepr n
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NatRepr n))
$cdataCast2 :: forall (n :: Nat) (t :: * -> * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NatRepr n))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n))
$cdataCast1 :: forall (n :: Nat) (t :: * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (NatRepr n))
dataTypeOf :: NatRepr n -> DataType
$cdataTypeOf :: forall (n :: Nat). KnownNat n => NatRepr n -> DataType
toConstr :: NatRepr n -> Constr
$ctoConstr :: forall (n :: Nat). KnownNat n => NatRepr n -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NatRepr n)
$cgunfold :: forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NatRepr n)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)
$cgfoldl :: forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)
$cp1Data :: forall (n :: Nat). KnownNat n => Typeable (NatRepr n)
Data)

type role NatRepr nominal

instance Eq (NatRepr m) where
  NatRepr m
_ == :: NatRepr m -> NatRepr m -> Bool
== NatRepr m
_ = Bool
True

instance TestEquality NatRepr where
  testEquality :: NatRepr a -> NatRepr b -> Maybe (a :~: b)
testEquality (NatRepr Natural
m) (NatRepr Natural
n)
    | Natural
m Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
    | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance DecidableEq NatRepr where
  decEq :: NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void)
decEq (NatRepr Natural
m) (NatRepr Natural
n)
    | Natural
m Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n    = (a :~: b) -> Either (a :~: b) ((a :~: b) -> Void)
forall a b. a -> Either a b
Left ((a :~: b) -> Either (a :~: b) ((a :~: b) -> Void))
-> (a :~: b) -> Either (a :~: b) ((a :~: b) -> Void)
forall a b. (a -> b) -> a -> b
$ (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl
    | Bool
otherwise = ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
forall a b. b -> Either a b
Right (((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void))
-> ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
forall a b. (a -> b) -> a -> b
$
        \a :~: b
x -> (a :~: b) -> Void -> Void
seq a :~: b
x (Void -> Void) -> Void -> Void
forall a b. (a -> b) -> a -> b
$ [Char] -> Void
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible [DecidableEq on NatRepr]"

compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
m NatRepr n
n =
  case Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NatRepr m -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr m
m) (NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n) of
    Ordering
LT -> (NatRepr 0 -> NatComparison 0 1)
-> NatRepr Any -> NatComparison m n
forall a b. a -> b
unsafeCoerce (((0 + 1) <= (0 + (0 + 1))) =>
NatRepr 0 -> NatComparison 0 (0 + (0 + 1))
forall (x :: Nat) (y :: Nat).
((x + 1) <= (x + (y + 1))) =>
NatRepr y -> NatComparison x (x + (y + 1))
NatLT @0 @0) (Natural -> NatRepr Any
forall (n :: Nat). Natural -> NatRepr n
NatRepr (NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- NatRepr m -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr m
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1))
    Ordering
EQ -> NatComparison Any Any -> NatComparison m n
forall a b. a -> b
unsafeCoerce  NatComparison Any Any
forall (x :: Nat). NatComparison x x
NatEQ
    Ordering
GT -> (NatRepr 0 -> NatComparison 1 0)
-> NatRepr Any -> NatComparison m n
forall a b. a -> b
unsafeCoerce (((0 + 1) <= (0 + (0 + 1))) =>
NatRepr 0 -> NatComparison (0 + (0 + 1)) 0
forall (x :: Nat) (y :: Nat).
((x + 1) <= (x + (y + 1))) =>
NatRepr y -> NatComparison (x + (y + 1)) x
NatGT @0 @0) (Natural -> NatRepr Any
forall (n :: Nat). Natural -> NatRepr n
NatRepr (NatRepr m -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr m
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1))

-- | Result of comparing two numbers.
data NatComparison m n where
  -- First number is less than second.
  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))
  NatEQ :: NatComparison x x
  -- First number is greater than second.
  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x

instance OrdF NatRepr where
  compareF :: NatRepr x -> NatRepr y -> OrderingF x y
compareF NatRepr x
x NatRepr y
y =
    case NatRepr x -> NatRepr y -> NatComparison x y
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr x
x NatRepr y
y of
      NatLT NatRepr y
_ -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
      NatComparison x y
NatEQ -> OrderingF x y
forall k (x :: k). OrderingF x x
EQF
      NatGT NatRepr y
_ -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

instance PolyEq (NatRepr m) (NatRepr n) where
  polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n)
polyEqF NatRepr m
x NatRepr n
y = ((m :~: n) -> NatRepr m :~: NatRepr n)
-> Maybe (m :~: n) -> Maybe (NatRepr m :~: NatRepr n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\m :~: n
Refl -> NatRepr m :~: NatRepr n
forall k (a :: k). a :~: a
Refl) (Maybe (m :~: n) -> Maybe (NatRepr m :~: NatRepr n))
-> Maybe (m :~: n) -> Maybe (NatRepr m :~: NatRepr n)
forall a b. (a -> b) -> a -> b
$ NatRepr m -> NatRepr n -> Maybe (m :~: n)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr m
x NatRepr n
y

instance Show (NatRepr n) where
  show :: NatRepr n -> [Char]
show (NatRepr Natural
n) = Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
n

instance ShowF NatRepr

instance HashableF NatRepr where
  hashWithSaltF :: Int -> NatRepr tp -> Int
hashWithSaltF = Int -> NatRepr tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt

-- | This generates a NatRepr from a type-level context.
knownNat :: forall n . KnownNat n => NatRepr n
knownNat :: NatRepr n
knownNat = Natural -> NatRepr n
forall (n :: Nat). Natural -> NatRepr n
NatRepr (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n))

instance (KnownNat n) => KnownRepr NatRepr n where
  knownRepr :: NatRepr n
knownRepr = NatRepr n
forall (n :: Nat). KnownNat n => NatRepr n
knownNat