hjugement-protocol/Utils/Natural.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 module Utils.Natural
   4  ( (+<=)
   5  , nat
   6  , Index(..)
   7  , (<=)
   8  , (<=?)
   9  , (+)
  10  , (-)
  11  , module GHC.TypeNats
  12  , Known
  13  ) where
  14
  15 import Data.Bool
  16 import Data.Eq (Eq(..))
  17 import Data.Maybe (Maybe(..), isJust)
  18 import Data.Proxy (Proxy(..))
  19 import GHC.TypeNats
  20 import Numeric.Natural (Natural)
  21 import Text.Show (Show(..))
  22 import Unsafe.Coerce (unsafeCoerce)
  23 import qualified Data.Ord as Ord
  24 import qualified Prelude as Num
  25
  26 import Utils.Constraint
  27
  28 -- | Convenient wrapper around 'natVal' to be used with @TypeApplications@.
  29 nat :: forall (n::Nat). KnownNat n => Natural
  30 nat = natVal (Proxy::Proxy n)
  31
  32 -- * Type 'Known'
  33 -- | Convenient alias.
  34 type Known = KnownNat
  35
  36 -- * Proofs
  37 -- | Proofs implied by @(i'+'j'<='n)@
  38 (+<=) :: (i+j<=n) => Proof (i<=n, j<=n, j<=n-i, i<=n-j)
  39 (+<=) = unsafeCoerce (Proof::Proof ((),(),(),()))
  40
  41 -- | Proofs implied by @(i'<='j)@.
  42 (<=) :: forall i j.
  43  KnownNat i => KnownNat j =>
  44  (i<=j) => Proof ( KnownNat (j-i)
  45                  , ((j-i)+i) ~ j
  46                  , ((i+j)-i) ~ j
  47                  , (i+(j-i)) ~ j )
  48 (<=) | SomeNat (_jmi::Proxy jmi) <- someNatVal (nat @j Num.- nat @i)
  49      = unsafeCoerce (Proof::Proof (KnownNat jmi, (), (), ()))
  50
  51 -- ** Operators
  52 (+) :: forall i j. KnownNat i => KnownNat j => Proof (KnownNat (i+j))
  53 (+) | SomeNat (_ipj::Proxy ipj) <- someNatVal (nat @i Num.+ nat @j)
  54     = unsafeCoerce (Proof::Proof (KnownNat ipj))
  55
  56 infixl 6 -
  57 (-) :: forall i j. (j<=i) => KnownNat i => KnownNat j => Proof (KnownNat (i-j))
  58 (-) | SomeNat (_imj::Proxy imj) <- someNatVal (nat @i Num.- nat @j)
  59     = unsafeCoerce (Proof::Proof (KnownNat imj))
  60
  61 infix 4 <=?
  62 (<=?) :: forall i j.
  63  KnownNat i => KnownNat j =>
  64  Maybe (Proof ( i<=j
  65               , KnownNat (j-i)
  66               , ((j-i)+i) ~ j
  67               , ((i+j)-i) ~ j
  68               , (i+(j-i)) ~ j ))
  69 (<=?) | nat @i Ord.<= nat @j
  70       , SomeNat (_jmi::Proxy jmi) <- someNatVal (nat @j Num.- nat @i)
  71       = Just (unsafeCoerce (Proof::Proof ((),KnownNat jmi,(),(),())))
  72       | otherwise = Nothing
  73
  74 -- * Type 'Index'
  75 data Index len where
  76  Index :: (KnownNat i, (i+1<=len)) => Proxy i -> Index len
  77 instance Eq (Index len) where
  78         Index i == Index j = isJust (sameNat i j)
  79 instance Show (Index len) where
  80         showsPrec p (Index i) = showsPrec p (natVal i)