    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE EmptyCase #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-|
    Copyright        : (c) Galois, Inc 2021

    @'Fin' n@ is a finite type with exactly @n@ elements. Essentially, they bundle a
    'NatRepr' that has an existentially-quantified type parameter with a proof that
    its parameter is less than some fixed natural.

    They are useful in combination with types of a fixed size. For example 'Fin' is
    used as the index in the 'Data.Functor.WithIndex.FunctorWithIndex' instance for
    'Data.Parameterized.Vector'. As another example, a @Map ('Fin' n) a@ is a @Map@
    that naturally has a fixed size bound of @n@.
    -}
    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

    -- | The type @'Fin' n@ has exactly @n@ inhabitants.
    data Fin n =
      -- GHC 8.6 and 8.4 require parentheses around 'i + 1 <= 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))

    -- | Non-lawful instance, intended only for testing.
    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')

    -- | Count all of the numbers up to @m@ that meet some condition.
    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

    -- | The smallest element of @'Fin' n@
    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)