{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Parameterized.Fin
( Fin
, mkFin
, buildFin
, countFin
, viewFin
, finToNat
, embed
, tryEmbed
, minFin
, incFin
, fin0Void
, fin1Unit
, fin2Bool
) where
import Control.Lens.Iso (Iso', iso)
import GHC.TypeNats (KnownNat)
import Numeric.Natural (Natural)
import Data.Void (Void, absurd)
import Data.Parameterized.NatRepr
data Fin n =
forall i. (i + 1 <= n) => Fin { ()
_getFin :: NatRepr i }
instance Eq (Fin n) where
Fin n
i == :: Fin n -> Fin n -> Bool
== Fin n
j = Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
i Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
j
instance Ord (Fin n) where
compare :: Fin n -> Fin n -> Ordering
compare Fin n
i Fin n
j = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
i) (Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
j)
instance (1 <= n, KnownNat n) => Bounded (Fin n) where
minBound :: Fin n
minBound = NatRepr 0 -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0)
maxBound :: Fin n
maxBound =
case NatRepr n -> NatRepr 1 -> ((n - 1) + 1) :~: n
forall (f :: Natural -> *) (m :: Natural) (g :: Natural -> *)
(n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of
((n - 1) + 1) :~: n
Refl -> NatRepr (n - 1) -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin (NatRepr n -> NatRepr (n - 1)
forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @n))
instance Show (Fin n) where
show :: Fin n -> String
show Fin n
i = String
"Fin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Fin n -> Natural
forall (n :: Natural). Fin n -> Natural
finToNat Fin n
i)
mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n
mkFin :: forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin = NatRepr i -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin
{-# INLINE mkFin #-}
newtype Fin' n = Fin' { forall (n :: Natural). Fin' n -> Fin (n + 1)
getFin' :: Fin (n + 1) }
buildFin ::
forall m.
NatRepr m ->
(forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Fin (n + 1 + 1)) ->
Fin (m + 1)
buildFin :: forall (m :: Natural).
NatRepr m
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
buildFin NatRepr m
m forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)
f =
let f' :: forall k. (k + 1 <= m) => NatRepr k -> Fin' k -> Fin' (k + 1)
f' :: forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> Fin' k -> Fin' (k + 1)
f' = (\NatRepr k
n (Fin' Fin (k + 1)
fin) -> Fin ((k + 1) + 1) -> Fin' (k + 1)
forall (n :: Natural). Fin (n + 1) -> Fin' n
Fin' (NatRepr k -> Fin (k + 1) -> Fin ((k + 1) + 1)
forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)
f NatRepr k
n Fin (k + 1)
fin))
in Fin' m -> Fin (m + 1)
forall (n :: Natural). Fin' n -> Fin (n + 1)
getFin' (NatRepr m
-> Fin' 0
-> (forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> Fin' k -> Fin' (k + 1))
-> Fin' m
forall (m :: Natural) (f :: Natural -> *).
NatRepr m
-> f 0
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> f n -> f (n + 1))
-> f m
natRecStrictlyBounded NatRepr m
m (Fin (0 + 1) -> Fin' 0
forall (n :: Natural). Fin (n + 1) -> Fin' n
Fin' Fin 1
Fin (0 + 1)
forall (n :: Natural). (1 <= n) => Fin n
minFin) NatRepr n -> Fin' n -> Fin' (n + 1)
forall (k :: Natural).
((k + 1) <= m) =>
NatRepr k -> Fin' k -> Fin' (k + 1)
f')
countFin ::
NatRepr m ->
(forall n. (n + 1 <= m) => NatRepr n -> Fin (n + 1) -> Bool) ->
Fin (m + 1)
countFin :: forall (m :: Natural).
NatRepr m
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Bool)
-> Fin (m + 1)
countFin NatRepr m
m forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Bool
f =
NatRepr m
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
forall (m :: Natural).
NatRepr m
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
buildFin NatRepr m
m ((forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1))
-> (forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1))
-> Fin (m + 1)
forall a b. (a -> b) -> a -> b
$
\NatRepr n
n Fin (n + 1)
count ->
if NatRepr n -> Fin (n + 1) -> Bool
forall (n :: Natural).
((n + 1) <= m) =>
NatRepr n -> Fin (n + 1) -> Bool
f NatRepr n
n Fin (n + 1)
count
then Fin (n + 1) -> Fin ((n + 1) + 1)
forall (n :: Natural). Fin n -> Fin (n + 1)
incFin Fin (n + 1)
count
else case Fin (n + 1) -> LeqProof (n + 1) ((n + 1) + 1)
forall (f :: Natural -> *) (z :: Natural).
f z -> LeqProof z (z + 1)
leqSucc Fin (n + 1)
count of
LeqProof (n + 1) ((n + 1) + 1)
LeqProof -> Fin (n + 1) -> Fin ((n + 1) + 1)
forall (n :: Natural) (m :: Natural). (n <= m) => Fin n -> Fin m
embed Fin (n + 1)
count
viewFin :: (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r
viewFin :: forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r
f (Fin NatRepr i
i) = NatRepr i -> r
forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r
f NatRepr i
i
finToNat :: Fin n -> Natural
finToNat :: forall (n :: Natural). Fin n -> Natural
finToNat (Fin NatRepr i
i) = NatRepr i -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr i
i
{-# INLINABLE finToNat #-}
embed :: forall n m. (n <= m) => Fin n -> Fin m
embed :: forall (n :: Natural) (m :: Natural). (n <= m) => Fin n -> Fin m
embed =
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> Fin m)
-> Fin n -> Fin m
forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin
(\(NatRepr i
x :: NatRepr o) ->
case LeqProof (i + 1) n -> LeqProof n m -> LeqProof (i + 1) m
forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof (i + 1) n
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (o + 1) n) (LeqProof n m
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof n m) of
LeqProof (i + 1) m
LeqProof -> NatRepr i -> Fin m
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin NatRepr i
x
)
tryEmbed :: NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
tryEmbed :: forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
tryEmbed NatRepr n
n NatRepr m
m Fin n
i =
case NatRepr n -> NatRepr m -> Maybe (LeqProof n m)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq NatRepr n
n NatRepr m
m of
Just LeqProof n m
LeqProof -> Fin m -> Maybe (Fin m)
forall a. a -> Maybe a
Just (Fin n -> Fin m
forall (n :: Natural) (m :: Natural). (n <= m) => Fin n -> Fin m
embed Fin n
i)
Maybe (LeqProof n m)
Nothing -> Maybe (Fin m)
forall a. Maybe a
Nothing
minFin :: (1 <= n) => Fin n
minFin :: forall (n :: Natural). (1 <= n) => Fin n
minFin = NatRepr 0 -> Fin n
forall (n :: Natural) (i :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
Fin (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0)
{-# INLINABLE minFin #-}
incFin :: forall n. Fin n -> Fin (n + 1)
incFin :: forall (n :: Natural). Fin n -> Fin (n + 1)
incFin (Fin (NatRepr i
i :: NatRepr i)) =
case LeqProof (i + 1) n
-> LeqProof 1 1 -> LeqProof ((i + 1) + 1) (n + 1)
forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
(y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (LeqProof (i + 1) n
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (i + 1) n) (LeqProof 1 1
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 1) of
LeqProof ((i + 1) + 1) (n + 1)
LeqProof -> NatRepr (i + 1) -> Fin (n + 1)
forall (i :: Natural) (n :: Natural).
((i + 1) <= n) =>
NatRepr i -> Fin n
mkFin (NatRepr i -> NatRepr (i + 1)
forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr i
i)
fin0Void :: Iso' (Fin 0) Void
fin0Void :: Iso' (Fin 0) Void
fin0Void =
(Fin 0 -> Void) -> (Void -> Fin 0) -> Iso' (Fin 0) Void
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
((forall (i :: Natural). ((i + 1) <= 0) => NatRepr i -> Void)
-> Fin 0 -> Void
forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin
(\(NatRepr i
x :: NatRepr o) ->
case NatRepr i -> NatRepr 1 -> (i + 1) :~: (1 + i)
forall (f :: Natural -> *) (m :: Natural) (g :: Natural -> *)
(n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr i
x (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) of
(i + 1) :~: (1 + i)
Refl ->
case forall (n :: Natural) (n' :: Natural) (m :: Natural).
LeqProof (n + n') m -> LeqProof n m
addIsLeqLeft1 @1 @o @0 LeqProof (i + 1) 0
LeqProof (1 + i) 0
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof of {}))
Void -> Fin 0
forall a. Void -> a
absurd
fin1Unit :: Iso' (Fin 1) ()
fin1Unit :: Iso' (Fin 1) ()
fin1Unit = (Fin 1 -> ()) -> (() -> Fin 1) -> Iso' (Fin 1) ()
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (() -> Fin 1 -> ()
forall a b. a -> b -> a
const ()) (Fin 1 -> () -> Fin 1
forall a b. a -> b -> a
const Fin 1
forall (n :: Natural). (1 <= n) => Fin n
minFin)
fin2Bool :: Iso' (Fin 2) Bool
fin2Bool :: Iso' (Fin 2) Bool
fin2Bool =
(Fin 2 -> Bool) -> (Bool -> Fin 2) -> Iso' (Fin 2) Bool
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
((forall (i :: Natural). ((i + 1) <= 2) => NatRepr i -> Bool)
-> Fin 2 -> Bool
forall (n :: Natural) r.
(forall (i :: Natural). ((i + 1) <= n) => NatRepr i -> r)
-> Fin n -> r
viewFin
(\NatRepr i
n ->
case NatRepr i -> IsZeroNat i
forall (n :: Natural). NatRepr n -> IsZeroNat n
isZeroNat NatRepr i
n of
IsZeroNat i
ZeroNat -> Bool
False
IsZeroNat i
NonZeroNat -> Bool
True))
(\Bool
b -> if Bool
b then Fin 2
forall a. Bounded a => a
maxBound else Fin 2
forall a. Bounded a => a
minBound)