Internal.hs

{-|
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 { natValue :: Natural.Natural
                                     -- ^ The underlying natural value of the number.
                                   }
  deriving (Hashable, Data)

type role NatRepr nominal

instance Eq (NatRepr m) where
  _ == _ = True

instance EqF NatRepr where
  eqF _ _ = True

instance TestEquality NatRepr where
  testEquality (NatRepr m) (NatRepr n)
    | m == n = Just unsafeAxiom
    | otherwise = Nothing

instance DecidableEq NatRepr where
  decEq (NatRepr m) (NatRepr n)
    | m == n    = Left unsafeAxiom
    | otherwise = Right $
        \x -> seq x $ error "Impossible [DecidableEq on NatRepr]"

compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
compareNat m n =
  case compare (natValue m) (natValue n) of
    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))
    EQ -> unsafeCoerce  NatEQ
    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 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 x y =
    case compareNat x y of
      NatLT _ -> LTF
      NatEQ -> EQF
      NatGT _ -> GTF

instance PolyEq (NatRepr m) (NatRepr n) where
  polyEqF x y = fmap (\Refl -> Refl) $ testEquality x y

instance Show (NatRepr n) where
  show (NatRepr n) = show n

instance ShowF NatRepr

instance HashableF NatRepr where
  hashWithSaltF = hashWithSalt

-- | This generates a NatRepr from a type-level context.
knownNat :: forall n . KnownNat n => NatRepr n
knownNat = NatRepr (natVal (Proxy :: Proxy n))

instance (KnownNat n) => KnownRepr NatRepr n where
  knownRepr = knownNat