]> Git — Sourcephile - majurity.git/blob - hjugement-protocol/Utils/Natural.hs
protocol: polish description
[majurity.git] / 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)