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 Control.Applicative (Applicative(..))
  16 import Data.Bool
  17 import Data.Eq (Eq(..))
  18 import Data.Foldable (Foldable)
  19 import Data.Function ((.), flip)
  20 import Data.Functor (Functor(..), (<$>))
  21 import Data.Int (Int)
  22 import Data.Maybe (Maybe(..), isJust)
  23 import Data.Monoid (Monoid(..))
  24 import Data.Proxy (Proxy(..))
  25 import Data.Traversable (Traversable(..))
  26 import Data.Tuple (fst, snd)
  27 import Data.Type.Equality ((:~:)(..))
  28 import GHC.TypeNats
  29 import Numeric.Natural (Natural)
  30 import Text.Show (Show(..))
  31 import Unsafe.Coerce (unsafeCoerce)
  32 import qualified Data.Ord as Ord
  33 import qualified Prelude as Num
  34
  35 import Utils.Constraint
  36
  37 -- | Convenient wrapper around 'natVal' to be used with @TypeApplications@.
  38 nat :: forall (n::Nat). KnownNat n => Natural
  39 nat = natVal (Proxy::Proxy n)
  40
  41 -- * Type 'Known'
  42 -- | Convenient alias.
  43 type Known = KnownNat
  44
  45 -- * Proofs
  46 -- | Proofs implied by @(i'+'j'<='n)@
  47 (+<=) :: (i+j<=n) => Proof (i<=n, j<=n, j<=n-i, i<=n-j)
  48 (+<=) = unsafeCoerce (Proof::Proof ((),(),(),()))
  49
  50 -- | Proofs implied by @(i'<='j)@.
  51 (<=) :: forall i j.
  52  KnownNat i => KnownNat j =>
  53  (i<=j) => Proof ( KnownNat (j-i)
  54                  , ((j-i)+i) ~ j
  55                  , ((i+j)-i) ~ j
  56                  , (i+(j-i)) ~ j )
  57 (<=) | SomeNat (_jmi::Proxy jmi) <- someNatVal (nat @j Num.- nat @i)
  58      = unsafeCoerce (Proof::Proof (KnownNat jmi, (), (), ()))
  59
  60 -- ** Operators
  61 (+) :: forall i j. KnownNat i => KnownNat j => Proof (KnownNat (i+j))
  62 (+) | SomeNat (_ipj::Proxy ipj) <- someNatVal (nat @i Num.+ nat @j)
  63     = unsafeCoerce (Proof::Proof (KnownNat ipj))
  64
  65 infixl 6 -
  66 (-) :: forall i j. (j<=i) => KnownNat i => KnownNat j => Proof (KnownNat (i-j))
  67 (-) | SomeNat (_imj::Proxy imj) <- someNatVal (nat @i Num.- nat @j)
  68     = unsafeCoerce (Proof::Proof (KnownNat imj))
  69
  70 infix 4 <=?
  71 (<=?) :: forall i j.
  72  KnownNat i => KnownNat j =>
  73  Maybe (Proof ( i<=j
  74               , KnownNat (j-i)
  75               , ((j-i)+i) ~ j
  76               , ((i+j)-i) ~ j
  77               , (i+(j-i)) ~ j ))
  78 (<=?) | nat @i Ord.<= nat @j
  79       , SomeNat (_jmi::Proxy jmi) <- someNatVal (nat @j Num.- nat @i)
  80       = Just (unsafeCoerce (Proof::Proof ((),KnownNat jmi,(),(),())))
  81       | otherwise = Nothing
  82
  83 -- * Type 'Index'
  84 data Index len where
  85  Index :: (KnownNat i, (i+1<=len)) => Proxy i -> Index len
  86 instance Eq (Index len) where
  87         Index i == Index j = isJust (sameNat i j)
  88 instance Show (Index len) where
  89         showsPrec p (Index i) = showsPrec p (natVal i)