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

    @'FinMap' n a@ conceptually (see NOTE) a map with @'Data.Parameterized.Fin.Fin'
    n@ keys, implying a maximum size of @n@. Here's how 'FinMap' compares to other
    map-like types:

    * @'FinMap' n a@ is conceptually isomorphic to a
      @'Data.Parameterized.Vector' n ('Maybe' a)@, but can be more space-efficient
      especially if @n@ is large and the vector is populated with a small number of
      'Just' values.
    * @'FinMap'@ is less general than 'Data.Map.Map', because it has a fixed key
      type (@'Data.Parameterized.Fin.Fin' n@).
    * @'FinMap' n a@ is similar to @'Data.IntMap.IntMap' a@, but it provides a
      static guarantee of a maximum size, and its operations (such as 'size') allow
      the recovery of more type-level information.
    * @'FinMap'@ is dissimilar from "Data.Parameterized.Map.MapF" in that neither
      the key nor value type of 'FinMap' is parameterized.

    The type parameter @n@ doesn't track the /current/ number of key-value pairs in
    a @'FinMap' n@ (i.e., the size of the map), but rather /an upper bound/.
    'insert' and 'delete' don't alter @n@, whereas 'incMax' does - despite the fact
    that it has no effect on the keys and values in the 'FinMap'.

    The 'FinMap' interface has two implementations:

    * The implementation in "Data.Parameterized.FinMap.Unsafe" is backed by an
      'Data.IntMap.IntMap', and must have a size of at most @'maxBound' :: 'Int'@.
      This module uses unsafe operations like 'Unsafe.Coerce.unsafeCoerce'
      internally for the sake of time and space efficiency.
    * The implementation in "Data.Parameterized.FinMap.Safe" is backed by an
      @'Data.Map.Map' ('Data.Parameterized.Fin.Fin' n)@. All of its functions are
      implemented using safe operations.

    The implementation in 'Data.Parameterized.FinMap.Unsafe.FinMap' is property
    tested against that in 'Data.Parameterized.FinMap.Safe.FinMap' to ensure
    they have the same behavior.

    In this documentation, /W/ is used in big-O notations the same way as in the
    "Data.IntMap" documentation.

    NOTE: Where the word "conceptually" is used, it implies that this correspondence
    is not literally true, but is true modulo some details such as differences
    between bounded types like 'Int' and unbounded types like 'Integer'.

    Several of the functions in both implementations are marked @INLINE@ or
    @INLINABLE@. There are three reasons for this:

    * Some of these just have very small definitions and so inlining is likely more
      beneficial than harmful.
    * Some participate in @RULES@ relevant to functions used in their
      implementations.
    * They are thin wrappers (often just newtype wrappers) around functions marked
      @INLINE@, which should therefore also be inlined.
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}

    module Data.Parameterized.FinMap
      (
    #ifdef UNSAFE_OPS
        module Data.Parameterized.FinMap.Unsafe
    #else
        module Data.Parameterized.FinMap.Safe
    #endif
      ) where

    #ifdef UNSAFE_OPS
    import Data.Parameterized.FinMap.Unsafe
    #else
    import Data.Parameterized.FinMap.Safe
    #endif