{-# language DataKinds #-}
{-# language ExplicitForAll #-}
{-# language KindSignatures #-}
{-# language MagicHash #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language TypeOperators #-}
module Arithmetic.Nat
(
plus
, monus
, succ
, testEqual
, testLessThan
, testLessThanEqual
, testZero
, (=?)
, (<?)
, (<=?)
, zero
, one
, two
, three
, constant
, demote
, with
) where
import Prelude hiding (succ)
import Arithmetic.Types
import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte))
import Arithmetic.Unsafe (Nat(Nat),type (<)(Lt))
import GHC.Exts (Proxy#,proxy#)
import GHC.TypeNats (type (+),KnownNat,natVal')
(<?) :: Nat a -> Nat b -> Maybe (a < b)
{-# inline (<?) #-}
<? :: Nat a -> Nat b -> Maybe (a < b)
(<?) = Nat a -> Nat b -> Maybe (a < b)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a < b)
testLessThan
(<=?) :: Nat a -> Nat b -> Maybe (a <= b)
{-# inline (<=?) #-}
<=? :: Nat a -> Nat b -> Maybe (a <= b)
(<=?) = Nat a -> Nat b -> Maybe (a <= b)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a <= b)
testLessThanEqual
(=?) :: Nat a -> Nat b -> Maybe (a :=: b)
{-# inline (=?) #-}
=? :: Nat a -> Nat b -> Maybe (a :=: b)
(=?) = Nat a -> Nat b -> Maybe (a :=: b)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Maybe (a :=: b)
testEqual
testLessThan :: Nat a -> Nat b -> Maybe (a < b)
{-# inline testLessThan #-}
testLessThan :: Nat a -> Nat b -> Maybe (a < b)
testLessThan (Nat Int
x) (Nat Int
y) = if Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y
then (a < b) -> Maybe (a < b)
forall a. a -> Maybe a
Just a < b
forall (a :: Nat) (b :: Nat). a < b
Lt
else Maybe (a < b)
forall a. Maybe a
Nothing
testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
{-# inline testLessThanEqual #-}
testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
testLessThanEqual (Nat Int
x) (Nat Int
y) = if Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
y
then (a <= b) -> Maybe (a <= b)
forall a. a -> Maybe a
Just a <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
else Maybe (a <= b)
forall a. Maybe a
Nothing
testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
{-# inline testEqual #-}
testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
testEqual (Nat Int
x) (Nat Int
y) = if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y
then (a :=: b) -> Maybe (a :=: b)
forall a. a -> Maybe a
Just a :=: b
forall (a :: Nat) (b :: Nat). a :=: b
Eq
else Maybe (a :=: b)
forall a. Maybe a
Nothing
testZero :: Nat a -> Either (0 :=: a) (0 < a)
{-# inline testZero #-}
testZero :: Nat a -> Either (0 :=: a) (0 < a)
testZero (Nat Int
x) = case Int
x of
Int
0 -> (0 :=: a) -> Either (0 :=: a) (0 < a)
forall a b. a -> Either a b
Left 0 :=: a
forall (a :: Nat) (b :: Nat). a :=: b
Eq
Int
_ -> (0 < a) -> Either (0 :=: a) (0 < a)
forall a b. b -> Either a b
Right 0 < a
forall (a :: Nat) (b :: Nat). a < b
Lt
plus :: Nat a -> Nat b -> Nat (a + b)
{-# inline plus #-}
plus :: Nat a -> Nat b -> Nat (a + b)
plus (Nat Int
x) (Nat Int
y) = Int -> Nat (a + b)
forall (n :: Nat). Int -> Nat n
Nat (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y)
succ :: Nat a -> Nat (a + 1)
{-# inline succ #-}
succ :: Nat a -> Nat (a + 1)
succ Nat a
n = Nat a -> Nat 1 -> Nat (a + 1)
forall (a :: Nat) (b :: Nat). Nat a -> Nat b -> Nat (a + b)
plus Nat a
n Nat 1
one
monus :: Nat a -> Nat b -> Maybe (Difference a b)
{-# inline monus #-}
monus :: Nat a -> Nat b -> Maybe (Difference a b)
monus (Nat Int
a) (Nat Int
b) = let c :: Int
c = Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b in if Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0
then Difference a b -> Maybe (Difference a b)
forall a. a -> Maybe a
Just (Nat Any -> ((Any + b) :=: a) -> Difference a b
forall (a :: Nat) (b :: Nat) (c :: Nat).
Nat c -> ((c + b) :=: a) -> Difference a b
Difference (Int -> Nat Any
forall (n :: Nat). Int -> Nat n
Nat Int
c) (Any + b) :=: a
forall (a :: Nat) (b :: Nat). a :=: b
Eq)
else Maybe (Difference a b)
forall a. Maybe a
Nothing
zero :: Nat 0
{-# inline zero #-}
zero :: Nat 0
zero = Int -> Nat 0
forall (n :: Nat). Int -> Nat n
Nat Int
0
one :: Nat 1
{-# inline one #-}
one :: Nat 1
one = Int -> Nat 1
forall (n :: Nat). Int -> Nat n
Nat Int
1
two :: Nat 2
{-# inline two #-}
two :: Nat 2
two = Int -> Nat 2
forall (n :: Nat). Int -> Nat n
Nat Int
2
three :: Nat 3
{-# inline three #-}
three :: Nat 3
three = Int -> Nat 3
forall (n :: Nat). Int -> Nat n
Nat Int
3
constant :: forall n. KnownNat n => Nat n
{-# inline constant #-}
constant :: Nat n
constant = Int -> Nat n
forall (n :: Nat). Int -> Nat n
Nat (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy# n -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n)))
demote :: Nat n -> Int
{-# inline demote #-}
demote :: Nat n -> Int
demote (Nat Int
n) = Int
n
with :: Int -> (forall n. Nat n -> a) -> a
{-# inline with #-}
with :: Int -> (forall (n :: Nat). Nat n -> a) -> a
with Int
i forall (n :: Nat). Nat n -> a
f = Nat Any -> a
forall (n :: Nat). Nat n -> a
f (Int -> Nat Any
forall (n :: Nat). Int -> Nat n
Nat Int
i)