{-|
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 qualified Numeric.Natural as Natural
import Unsafe.Coerce

import Data.Parameterized.Axiom
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 { forall (n :: Nat). NatRepr n -> Nat
natValue :: Natural.Natural
                                     -- ^ The underlying natural value of the number.
                                   }
  deriving (Int -> NatRepr n -> Int
NatRepr n -> Int
forall {n :: Nat}. Eq (NatRepr n)
forall (n :: Nat). Int -> NatRepr n -> Int
forall (n :: Nat). NatRepr n -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
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, NatRepr n -> DataType
NatRepr n -> Constr
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 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 (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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
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 :: forall (a :: Nat) (b :: Nat).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
testEquality (NatRepr Nat
m) (NatRepr Nat
n)
    | Nat
m forall a. Eq a => a -> a -> Bool
== Nat
n = forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
    | Bool
otherwise = forall a. Maybe a
Nothing

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

compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
compareNat :: forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr m
m NatRepr n
n =
  case forall a. Ord a => a -> a -> Ordering
compare (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr m
m) (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
n) of
    Ordering
LT -> forall a b. a -> b
unsafeCoerce (forall (x :: Nat) (y :: Nat).
((x + 1) <= (x + (y + 1))) =>
NatRepr y -> NatComparison x (x + (y + 1))
NatLT @0 @0) (forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
n forall a. Num a => a -> a -> a
- forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr m
m forall a. Num a => a -> a -> a
- Nat
1))
    Ordering
EQ -> forall a b. a -> b
unsafeCoerce  forall (x :: Nat). NatComparison x x
NatEQ
    Ordering
GT -> forall a b. a -> b
unsafeCoerce (forall (x :: Nat) (y :: Nat).
((x + 1) <= (x + (y + 1))) =>
NatRepr y -> NatComparison (x + (y + 1)) x
NatGT @0 @0) (forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr m
m forall a. Num a => a -> a -> a
- forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
n forall a. Num a => a -> a -> a
- Nat
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 :: forall (x :: Nat) (y :: Nat).
NatRepr x -> NatRepr y -> OrderingF x y
compareF NatRepr x
x NatRepr y
y =
    case forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat NatRepr x
x NatRepr y
y of
      NatLT NatRepr y
_ -> forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      NatComparison x y
NatEQ -> forall {k} (x :: k). OrderingF x x
EQF
      NatGT NatRepr 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\m :~: n
Refl -> forall {k} (a :: k). a :~: a
Refl) forall a b. (a -> b) -> a -> b
$ 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 Nat
n) = forall a. Show a => a -> [Char]
show Nat
n

instance ShowF NatRepr

instance HashableF NatRepr where
  hashWithSaltF :: forall (n :: Nat). Int -> NatRepr n -> Int
hashWithSaltF = 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 :: forall (n :: Nat). KnownNat n => NatRepr n
knownNat = forall (n :: Nat). Nat -> NatRepr n
NatRepr (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

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