{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Grisette.Utils.Parameterized
(
unsafeAxiom,
NatRepr,
natValue,
unsafeMkNatRepr,
natRepr,
decNat,
predNat,
incNat,
addNat,
subNat,
divNat,
halfNat,
KnownProof (..),
hasRepr,
withKnownProof,
unsafeKnownProof,
knownAdd,
LeqProof (..),
withLeqProof,
unsafeLeqProof,
testLeq,
leqRefl,
leqSucc,
leqTrans,
leqZero,
leqAdd2,
leqAdd,
leqAddPos,
)
where
import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
import GHC.Natural (Natural)
import GHC.TypeNats
( Div,
KnownNat,
Nat,
SomeNat (SomeNat),
natVal,
someNatVal,
type (+),
type (-),
type (<=),
)
import Unsafe.Coerce (unsafeCoerce)
unsafeAxiom :: forall a b. a :~: b
unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom = (a :~: a) -> a :~: b
forall a b. a -> b
unsafeCoerce (forall (a :: k). a :~: a
forall {k} (a :: k). a :~: a
Refl @a)
newtype NatRepr (n :: Nat) = NatRepr Natural
natValue :: NatRepr n -> Natural
natValue :: forall (n :: Nat). NatRepr n -> Nat
natValue (NatRepr Nat
n) = Nat
n
unsafeMkNatRepr :: Natural -> NatRepr n
unsafeMkNatRepr :: forall (n :: Nat). Nat -> NatRepr n
unsafeMkNatRepr = Nat -> NatRepr n
forall (n :: Nat). Nat -> NatRepr n
NatRepr
natRepr :: forall n. (KnownNat n) => NatRepr n
natRepr :: forall (n :: Nat). KnownNat n => NatRepr n
natRepr = Nat -> NatRepr n
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
decNat :: (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat :: forall (n :: Nat). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat (NatRepr Nat
n) = Nat -> NatRepr (n - 1)
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
predNat :: NatRepr (n + 1) -> NatRepr n
predNat :: forall (n :: Nat). NatRepr (n + 1) -> NatRepr n
predNat (NatRepr Nat
n) = Nat -> NatRepr n
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
incNat :: NatRepr n -> NatRepr (n + 1)
incNat :: forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
incNat (NatRepr Nat
n) = Nat -> NatRepr (n + 1)
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)
addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat :: forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (NatRepr Nat
m) (NatRepr Nat
n) = Nat -> NatRepr (m + n)
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n)
subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat :: forall (n :: Nat) (m :: Nat).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat (NatRepr Nat
m) (NatRepr Nat
n) = Nat -> NatRepr (m - n)
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n)
divNat :: (1 <= n) => NatRepr m -> NatRepr n -> NatRepr (Div m n)
divNat :: forall (n :: Nat) (m :: Nat).
(1 <= n) =>
NatRepr m -> NatRepr n -> NatRepr (Div m n)
divNat (NatRepr Nat
m) (NatRepr Nat
n) = Nat -> NatRepr (Div m n)
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
m Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
n)
halfNat :: NatRepr (n + n) -> NatRepr n
halfNat :: forall (n :: Nat). NatRepr (n + n) -> NatRepr n
halfNat (NatRepr Nat
n) = Nat -> NatRepr n
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Nat
n Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
2)
data KnownProof (n :: Nat) where
KnownProof :: (KnownNat n) => KnownProof n
withKnownProof :: KnownProof n -> ((KnownNat n) => r) -> r
withKnownProof :: forall (n :: Nat) r. KnownProof n -> (KnownNat n => r) -> r
withKnownProof KnownProof n
p KnownNat n => r
r = case KnownProof n
p of KnownProof n
KnownProof -> r
KnownNat n => r
r
unsafeKnownProof :: Natural -> KnownProof n
unsafeKnownProof :: forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof Nat
nVal = NatRepr n -> KnownProof n
forall (n :: Nat). NatRepr n -> KnownProof n
hasRepr (Nat -> NatRepr n
forall (n :: Nat). Nat -> NatRepr n
NatRepr Nat
nVal)
hasRepr :: forall n. NatRepr n -> KnownProof n
hasRepr :: forall (n :: Nat). NatRepr n -> KnownProof n
hasRepr (NatRepr Nat
nVal) =
case Nat -> SomeNat
someNatVal Nat
nVal of
SomeNat (Proxy n
Proxy :: Proxy n') ->
case n :~: n
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: n :~: n' of
n :~: n
Refl -> KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof
knownAdd :: forall m n. KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd :: forall (m :: Nat) (n :: Nat).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd KnownProof m
KnownProof KnownProof n
KnownProof = forall (n :: Nat). NatRepr n -> KnownProof n
hasRepr @(m + n) (Nat -> NatRepr (m + n)
forall (n :: Nat). Nat -> NatRepr n
NatRepr (Proxy m -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)))
data LeqProof (m :: Nat) (n :: Nat) where
LeqProof :: (m <= n) => LeqProof m n
withLeqProof :: LeqProof m n -> ((m <= n) => r) -> r
withLeqProof :: forall (m :: Nat) (n :: Nat) r.
LeqProof m n -> ((m <= n) => r) -> r
withLeqProof LeqProof m n
p (m <= n) => r
r = case LeqProof m n
p of LeqProof m n
LeqProof -> r
(m <= n) => r
r
unsafeLeqProof :: forall m n. LeqProof m n
unsafeLeqProof :: forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof = LeqProof 0 0 -> LeqProof m n
forall a b. a -> b
unsafeCoerce (forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof @0 @0)
testLeq :: NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq :: forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr Nat
m) (NatRepr Nat
n) =
case Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Nat
m Nat
n of
Ordering
LT -> Maybe (LeqProof m n)
forall a. Maybe a
Nothing
Ordering
EQ -> LeqProof m n -> Maybe (LeqProof m n)
forall a. a -> Maybe a
Just LeqProof m n
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
Ordering
GT -> LeqProof m n -> Maybe (LeqProof m n)
forall a. a -> Maybe a
Just LeqProof m n
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
leqRefl :: f n -> LeqProof n n
leqRefl :: forall (f :: Nat -> *) (n :: Nat). f n -> LeqProof n n
leqRefl f n
_ = LeqProof n n
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
leqSucc :: f n -> LeqProof n (n + 1)
leqSucc :: forall (f :: Nat -> *) (n :: Nat). f n -> LeqProof n (n + 1)
leqSucc f n
_ = LeqProof n (n + 1)
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
leqTrans :: LeqProof a b -> LeqProof b c -> LeqProof a c
leqTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat).
LeqProof a b -> LeqProof b c -> LeqProof a c
leqTrans LeqProof a b
_ LeqProof b c
_ = LeqProof a c
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
leqZero :: LeqProof 0 n
leqZero :: forall (n :: Nat). LeqProof 0 n
leqZero = LeqProof 0 n
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
leqAdd2 :: LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh)
leqAdd2 :: forall (xl :: Nat) (xh :: Nat) (yl :: Nat) (yh :: Nat).
LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh)
leqAdd2 LeqProof xl xh
_ LeqProof yl yh
_ = LeqProof (xl + yl) (xh + yh)
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
leqAdd :: LeqProof m n -> f o -> LeqProof m (n + o)
leqAdd :: forall (m :: Nat) (n :: Nat) (f :: Nat -> *) (o :: Nat).
LeqProof m n -> f o -> LeqProof m (n + o)
leqAdd LeqProof m n
_ f o
_ = LeqProof m (n + o)
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof
leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
leqAddPos :: forall (m :: Nat) (n :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos p m
_ q n
_ = LeqProof 1 (m + n)
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof