parameterized-utils 2.3.0.0 → 2.3.1.0

raw patch · 9 files changed

+799/−352 lines, 9 filesdep +ghc-bignumdep +integer-gmpPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: ghc-bignum, integer-gmp

API changes (from Hackage documentation)

Files

• Changelog.md +11/−0
• parameterized-utils.cabal +7/−1
• src/Data/Parameterized/Fin.hs +91/−2
• src/Data/Parameterized/Map.hs +54/−5
• src/Data/Parameterized/NatRepr.hs +89/−1
• src/Data/Parameterized/NatRepr/Internal.hs +3/−0
• src/Data/Parameterized/Utils/BinTree.hs +1/−342
• src/Data/Parameterized/Utils/BinTree/Internal.hs +387/−0
• test/Test/Fin.hs +156/−1

@@ -1,5 +1,16 @@ # Changelog for the `parameterized-utils` package +## 2.3.1.0 -- 2026-08-27++* Add `Hashable` and `Num` instances for `Fin`.+* Add `mkFinModN`, `finFromNatModN`, `addFinModN`, `subFinModN`, `mulFinModN`,+  `negFinModN`, and `recipFinModN` to `Data.Parameterized.Fin`.+* Add `modNat`, `modIsLeq`, `withModLeq`, and `withRecipModNat` to+  `Data.Parameterized.NatRepr`.+* Add an `Ord` instance for `NatRepr`.+* Change the `Show` instance for `Fin` such that calling `showsPrec p` will+  parenthesize the output if `p` is sufficiently large.+ ## 2.3.0.0 -- 2026-03-06    * BREAKING: Remove the `Iso`s `fin0Void`, `fin1Unit`, and `fin2Bool`.

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          parameterized-utils-Version:       2.3.0.0+Version:       2.3.1.0 Author:        Galois Inc. Maintainer:    kquick@galois.com, rscott@galois.com stability:     stable@@ -65,6 +65,11 @@                , text                , vector         >=0.12 && < 0.14 +  if impl(ghc >= 9.0)+    build-depends: ghc-bignum >= 1.0 && < 1.5+  else+    build-depends: integer-gmp >= 1.0 && < 1.1+   hs-source-dirs: src    exposed-modules:@@ -108,6 +113,7 @@    other-modules:     Data.Parameterized.NatRepr.Internal+    Data.Parameterized.Utils.BinTree.Internal    if flag(unsafe-operations)     cpp-options: -DUNSAFE_OPS

@@ -23,21 +23,30 @@ module Data.Parameterized.Fin   ( Fin   , mkFin+  , mkFinModN   , buildFin   , countFin   , viewFin+  , finFromNatModN   , finToNat   , embed   , tryEmbed   , minFin   , incFin   , fin0Absurd+  , addFinModN+  , subFinModN+  , mulFinModN+  , negFinModN+  , recipFinModN   ) where +import Data.Hashable (Hashable(..)) import GHC.TypeNats (KnownNat) import Numeric.Natural (Natural)  import Data.Parameterized.NatRepr+import Data.Parameterized.Some (Some(..))  -- | The type @'Fin' n@ has exactly @n@ inhabitants. data Fin n =@@ -50,20 +59,60 @@ instance Ord (Fin n) where   compare i j = compare (finToNat i) (finToNat j) +instance Hashable (Fin n) where+  hashWithSalt salt (Fin i) = hashWithSalt salt i+ instance (1 <= n, KnownNat n) => Bounded (Fin n) where   minBound = Fin (knownNat @0)   maxBound =     case minusPlusCancel (knownNat @n) (knownNat @1) of       Refl -> Fin (decNat (knownNat @n)) --- | Non-lawful instance, intended only for testing.+-- | Arithmetic is performed modulo @n@.+instance (1 <= n, KnownNat n) => Num (Fin n) where+  (+) = addFinModN (knownNat @n)+  (-) = subFinModN (knownNat @n)+  (*) = mulFinModN (knownNat @n)+  negate = negFinModN (knownNat @n)++  -- | We consider all Fin values to be non-negative. Therefore, this always+  -- returns the input unchanged.+  abs = id++  -- | We consider all Fin values to be non-negative. Therefore, this always+  -- returns either 'minFin' (i.e., zero) or @'mkFinModN' n (knownNat \@1)@+  -- (i.e., one). Note that in the degenerate case of @'Fin' 1@, these values+  -- will be equal to each other.+  signum f+    | f == minFin+    = f+    | otherwise+    = mkFinModN (knownNat @n) (knownNat @1)++  -- | Negative integers are negated, reduced modulo @n@, and then negated+  -- again using 'negFinModN'.+  fromInteger i+    | i >= 0+    = finFromNatModN n (fromInteger i)+    | otherwise+    = negFinModN n (finFromNatModN n (fromInteger (negate i)))+    where+      n = knownNat @n++-- Equivalent to what a derived Show instance would be, except that we+-- intentionally do not print out the (non-exported) _getFin field name. instance Show (Fin n) where-  show i = "Fin " ++ show (finToNat i)+  showsPrec p i = showParen (p >= 11) $ showString "Fin " . shows (finToNat i)  mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n mkFin = Fin {-# INLINE mkFin #-} +-- | Construct a @'Fin' n@ value from the number @i@, where @i@ is reduced+-- modulo @n@.+mkFinModN :: (1 <= n) => NatRepr n -> NatRepr i -> Fin n+mkFinModN n i = withModLeq i n Fin+ newtype Fin' n = Fin' { getFin' :: Fin (n + 1) }  buildFin ::@@ -92,6 +141,13 @@ viewFin ::  (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r viewFin f (Fin i) = f i +-- | Construct a @'Fin' n@ value from a 'Natural' input, where the input is+-- reduced modulo @n@.+finFromNatModN :: forall n. (1 <= n) => NatRepr n -> Natural -> Fin n+finFromNatModN n i+  | Some i' <- mkNatRepr i+  = mkFinModN n i'+ finToNat :: Fin n -> Natural finToNat (Fin i) = natValue i {-# INLINABLE finToNat #-}@@ -128,3 +184,36 @@       case plusComm x (knownNat @1) of         Refl ->           case addIsLeqLeft1 @1 @o @0 LeqProof of {})++-- | Add two @'Fin' n@ values and reduce the result modulo @n@.+addFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n+addFinModN n (Fin x) (Fin y) = mkFinModN n (addNat x y)++-- | Subtract two @'Fin' n@ values and reduce the result modulo @n@.+subFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n+subFinModN n x y = addFinModN n x (negFinModN n y)++-- | Multiply two @'Fin' n@ values and reduce the result modulo @n@.+mulFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n+mulFinModN n (Fin x) (Fin y) = mkFinModN n (natMultiply x y)++-- | Given a value @i :: 'Fin' n@ value, negate it. That is, if @i@ is zero,+-- then return @i@ unchanged, and if @i@ is non-zero, then compute @n - i@.+-- This is a negation in the sense that it is an additive inverse: adding @i@+-- to its negation will yield 'minFin'.+negFinModN :: forall n. (1 <= n) => NatRepr n -> Fin n -> Fin n+negFinModN n (Fin (i :: NatRepr i))+  | LeqProof <- addIsLeqLeft1 @i @1 @n LeqProof+  = mkFinModN n (subNat n i)++-- | Given a value @i :: 'Fin' n@, compute the reciprocal (i.e., the modular+-- inverse) if one exists. That is, attempt to compute @i^-1@ such that+-- @i * i^-1@ equals @1@ modulo @n@. Note that a reciprocal will only exist if+-- @i@ and @n@ are relatively prime, i.e., if @gcd i n == 1@. If they are not+-- relatively prime, then this function will return 'Nothing'.+--+-- Note that in the degenerate case where @n == 1@, this function will always+-- return @Just 0@. The value @0@ is the only element of @'Fin' 1@, and @0@ is+-- its own reciprocal.+recipFinModN :: forall n. (1 <= n) => NatRepr n -> Fin n -> Maybe (Fin n)+recipFinModN n (Fin i) = withRecipModNat i n Fin

@@ -94,7 +94,7 @@ import           Data.Parameterized.Some import           Data.Parameterized.Pair ( Pair(..) ) import           Data.Parameterized.TraversableF-import           Data.Parameterized.Utils.BinTree+import           Data.Parameterized.Utils.BinTree.Internal   ( MaybeS(..)   , fromMaybeS   , Updated(..)@@ -106,7 +106,7 @@   , balanceR   , glue   )-import qualified Data.Parameterized.Utils.BinTree as Bin+import qualified Data.Parameterized.Utils.BinTree.Internal as Bin  ------------------------------------------------------------------------ -- * Pair@@ -115,6 +115,53 @@ comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y) {-# INLINABLE comparePairKeys #-} +-- 'MapF' is the only 'IsBinTree' instance, so specialize each polymorphic+-- 'BinTree' helper used below. This removes class-dictionary indirection+-- through 'asBin'/'bin'/'size'/'tip' in the generated Core.+{-# SPECIALIZE Bin.insert+      :: (Pair k a -> Pair k a -> Ordering)+      -> Pair k a -> MapF k a -> Updated (MapF k a) #-}+{-# SPECIALIZE Bin.delete+      :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}+{-# SPECIALIZE Bin.union+      :: (Pair k a -> Pair k a -> Ordering)+      -> MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.link+      :: Pair k a -> MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.merge :: MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE balanceL+      :: Pair k a -> MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE balanceR+      :: Pair k a -> MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE glue :: MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.filterGt+      :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}+{-# SPECIALIZE Bin.filterLt+      :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}+-- These helpers are called from the bodies of the specialized exported+-- 'BinTree' functions above, but the specializer doesn't propagate the+-- concrete instance dictionary into them, so we specialize them explicitly+-- (import site: 'Data.Parameterized.Utils.BinTree.Internal').+{-# SPECIALIZE Bin.insertMax :: Pair k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.insertMin :: Pair k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.insertR+      :: (Pair k a -> Pair k a -> Ordering)+      -> Pair k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.hedgeUnion_LB+      :: (Pair k a -> Pair k a -> Ordering)+      -> Pair k a -> MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.hedgeUnion_UB+      :: (Pair k a -> Pair k a -> Ordering)+      -> Pair k a -> MapF k a -> MapF k a -> MapF k a #-}+{-# SPECIALIZE Bin.hedgeUnion_LB_UB+      :: (Pair k a -> Pair k a -> Ordering)+      -> Pair k a -> Pair k a -> MapF k a -> MapF k a -> MapF k a #-}+-- 'deleteFindMin' and 'deleteFindMax' use an 'INLINE' pragma instead of+-- 'SPECIALIZE': they are tight recursive functions (driven by their own+-- worker 'go') whose outer wrappers are easy to inline, which resolves the+-- dictionary at each call site without introducing a lingering worker+-- ('$wdeleteFindM{in,ax}') that still receives a dictionary parameter.+ ------------------------------------------------------------------------ -- MapF @@ -147,12 +194,17 @@ instance Bin.IsBinTree (MapF k a) (Pair k a) where   asBin (Bin _ k v l r) = BinTree (Pair k v) l r   asBin Tip = TipTree+  {-# INLINE asBin #-}    tip = Tip+  {-# INLINE tip #-}+   bin (Pair k v) l r = Bin (size l + size r + 1) k v l r+  {-# INLINE bin #-}    size Tip              = 0   size (Bin sz _ _ _ _) = sz+  {-# INLINE size #-}  instance (TestEquality k, EqF a) => Eq (MapF k a) where   x == y = size x == size y && toList x == toList y@@ -409,7 +461,6 @@ insert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a insert = \k v m -> seq k $ updatedValue (Bin.insert comparePairKeys (Pair k v) m) {-# INLINABLE insert #-}--- {-# SPECIALIZE Bin.insert :: OrdF k => Pair k a -> MapF k a -> Updated (MapF k a) #-}  -- | Insert a binding into the map, replacing the existing binding if needed. insertWithImpl :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> Updated (MapF k a)@@ -445,7 +496,6 @@   where p :: OrdF k => k tp -> Pair k a -> Ordering         p k (Pair kx _) = toOrdering (compareF k kx) {-# INLINABLE delete #-}-{-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}  -- | Left-biased union of two maps. The resulting map will contain the -- union of the keys of the two arguments. When a key is contained in@@ -453,7 +503,6 @@ union :: OrdF k => MapF k a -> MapF k a -> MapF k a union t1 t2 = Bin.union comparePairKeys t1 t2 {-# INLINABLE union #-}--- {-# SPECIALIZE Bin.union compare :: OrdF k => MapF k a -> MapF k a -> MapF k a #-}  ------------------------------------------------------------------------ -- updateAtKey

@@ -25,6 +25,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -33,6 +34,7 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UnboxedSums #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-}@@ -54,8 +56,10 @@   , addNat   , subNat   , divNat+  , modNat   , halfNat   , withDivModNat+  , withRecipModNat   , natMultiply   , someNat   , mkNatRepr@@ -108,6 +112,8 @@   , addIsLeqLeft1   , dblPosIsPos   , leqMulMono+  , modIsLeq+  , withModLeq     -- * Arithmetic proof   , plusComm   , plusAssoc@@ -137,7 +143,7 @@ import Data.Void as Void import Numeric.Natural import GHC.TypeNats ( KnownNat, Nat, SomeNat(..)-                    , type (+), type (-), type (*), type (<=)+                    , type (+), type (-), type (*), type (<=), type Mod                     , someNatVal ) import Unsafe.Coerce @@ -145,6 +151,12 @@ import Data.Parameterized.NatRepr.Internal import Data.Parameterized.Some +#if MIN_VERSION_base(4,15,0)+import qualified GHC.Num.Integer as Integer+#else+import qualified GHC.Integer.GMP.Internals as GMP+#endif+ maxInt :: Natural maxInt = fromIntegral (maxBound :: Int) @@ -218,6 +230,9 @@ divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m divNat (NatRepr x) (NatRepr y) = NatRepr (div x y) +modNat :: (1 <= n) => NatRepr m -> NatRepr n -> NatRepr (Mod m n)+modNat (NatRepr x) (NatRepr y) = NatRepr (mod x y)+ withDivModNat :: forall n m a.                  NatRepr n               -> NatRepr m@@ -232,6 +247,67 @@   where     (divPart, modPart) = divMod (natValue n) (natValue m) +-- | @'withRecipModNat' n m@ computes the reciprocal (i.e., the modular+-- inverse) of @n@ mod @m@. If @n@ and @m@ are relatively prime (i.e., if+-- @gcd n m == 1@), then this will pass the reciprocal @r@ to a continuation+-- and return the result with 'Just'. Otherwise, this will return 'Nothing',+-- as a reciprocal does not exist.+withRecipModNat ::+  forall n m a.+  (1 <= m) =>+  NatRepr n ->+  NatRepr m ->+  (forall r. (r + 1 <= m, Mod (n * r) m ~ 1) => NatRepr r -> a) ->+  Maybe a+withRecipModNat n m f =+  fmap (go . mkNatRepr) (integerRecipMod (intValue n) (natValue m))+  where+    go :: Some NatRepr -> a+    go (Some (r :: NatRepr r)) =+      case ( unsafeCoerce @(LeqProof 0 0) @(LeqProof (r + 1) m) LeqProof+           , unsafeAxiom @(Mod (n * r) m) @1+           ) of+        (LeqProof, Refl) -> f r++-- | Compute the modular inverse, returning 'Nothing' when this is not+-- possible. This behaves much like 'Integer.integerRecipMod#' in @ghc-bignum@,+-- except that this returns a 'Maybe' instead of an unboxed sum to represent+-- the possibility of failure. For more details on when this can return+-- 'Nothing', see the Haddocks for 'Integer.integerRecipMod#'.+--+-- Because 'Integer.integerRecipMod#' is only defined on GHC 9.0 or later, we+-- fall back to a different implementation using the @integer-gmp@ library on+-- older versions of GHC.+#if MIN_VERSION_base(4,15,0)+integerRecipMod :: Integer -> Natural -> Maybe Natural+integerRecipMod x y+  -- Due to https://gitlab.haskell.org/ghc/ghc/-/issues/26017, old versions of+  -- GHC have a bug in which `integerRecipMod# x 1` would return (# | () #)+  -- instead of (# 0 | #) for all `x`, contrary to the function's Haddocks. We+  -- include an extra check on old versions of GHC to work around this issue.+# if !MIN_VERSION_base(4,22,0)+  | y == 1 = Just 0+# endif+  | otherwise =+      case Integer.integerRecipMod# x y of+        (# r | #)  -> Just r+        (# | () #) -> Nothing+#else+integerRecipMod :: Integer -> Natural -> Maybe Natural+integerRecipMod x y+    -- Special case for `y == 1`, which we include to make the behavior of this+    -- function match that of integerRecipMod# on GHC 9.0 or later. Without+    -- this special case, this function would always return `Nothing` when the+    -- modulus is `1`.+  | y == 1 = Just 0+  | res == 0 = Nothing+  | otherwise = Just res+  where+    -- SAFETY: GMP.recipModInteger always returns a non-negative Integer, so+    -- the call to `fromInteger @Natural` below will always succeed.+    res = fromInteger @Natural (GMP.recipModInteger x (toInteger y))+#endif+ natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m) natMultiply (NatRepr n) (NatRepr m) = NatRepr (n * m) @@ -523,6 +599,18 @@  withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a withAddLeq n m f = withLeqProof (addIsLeq n m) (f (addNat n m))++modIsLeq :: (1 <= m) => f n -> g m -> LeqProof (Mod n m + 1) m+modIsLeq _ _ = unsafeCoerce (LeqProof @0 @0)+{-# NOINLINE modIsLeq #-}++withModLeq ::+  (1 <= m) =>+  NatRepr n ->+  NatRepr m ->+  ((Mod n m + 1 <= m) => NatRepr (Mod n m) -> a) ->+  a+withModLeq n m f = withLeqProof (modIsLeq n m) (f (modNat n m))  natForEach' :: forall l h a             . NatRepr l

@@ -51,6 +51,9 @@ instance EqF NatRepr where   eqF _ _ = True +instance Ord (NatRepr x) where+   compare _ _ = EQ+ instance TestEquality NatRepr where   testEquality (NatRepr m) (NatRepr n)     | m == n = Just unsafeAxiom

@@ -3,13 +3,6 @@ Copyright        : (c) Galois, Inc 2014-2019 Maintainer       : Joe Hendrix <jhendrix@galois.com> -}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE Safe #-} module Data.Parameterized.Utils.BinTree   ( MaybeS(..)@@ -31,338 +24,4 @@   , PairS(..)   ) where -import Control.Applicative----------------------------------------------------------------------------- MaybeS---- | A strict version of 'Maybe'-data MaybeS v-   = JustS !v-   | NothingS--instance Functor MaybeS where-  fmap _ NothingS = NothingS-  fmap f (JustS v) = JustS (f v)--instance Alternative MaybeS where-  empty = NothingS-  mv@JustS{} <|> _ = mv-  NothingS <|> v = v--instance Applicative MaybeS where-  pure = JustS--  NothingS <*> _ = NothingS-  JustS{} <*> NothingS = NothingS-  JustS f <*> JustS x = JustS (f x)--fromMaybeS :: a -> MaybeS a -> a-fromMaybeS r NothingS = r-fromMaybeS _ (JustS v) = v----------------------------------------------------------------------------- Updated---- | @Updated a@ contains a value that has been flagged on whether it was--- modified by an operation.-data Updated a-   = Updated   !a-   | Unchanged !a--updatedValue :: Updated a -> a-updatedValue (Updated a) = a-updatedValue (Unchanged a) = a----------------------------------------------------------------------------- IsBinTree--data TreeApp e t-   = BinTree !e !t !t-   | TipTree--class IsBinTree t e | t -> e where-  asBin :: t -> TreeApp e t-  tip :: t--  bin :: e -> t -> t -> t-  size :: t -> Int--delta,ratio :: Int-delta = 3-ratio = 2---- | @balanceL p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.------ It assumes that @l@ and @r@ are close to being balanced, and that only--- @l@ may contain too many elements.-balanceL :: (IsBinTree c e) => e -> c -> c -> c-balanceL p l r = do-  case asBin l of-    BinTree l_pair ll lr | size l > max 1 (delta*size r) ->-      case asBin lr of-        BinTree lr_pair lrl lrr | size lr >= max 2 (ratio*size ll) ->-          bin lr_pair (bin l_pair ll lrl) (bin p lrr r)-        _ -> bin l_pair ll (bin p lr r)--    _ -> bin p l r-{-# INLINE balanceL #-}---- | @balanceR p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.------ It assumes that @l@ and @r@ are close to being balanced, and that only--- @r@ may contain too many elements.-balanceR :: (IsBinTree c e) => e -> c -> c -> c-balanceR p l r = do-  case asBin r of-    BinTree r_pair rl rr | size r > max 1 (delta*size l) ->-      case asBin rl of-        BinTree rl_pair rll rlr | size rl >= max 2 (ratio*size rr) ->-          (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr-        _ -> bin r_pair (bin p l rl) rr-    _ -> bin p l r-{-# INLINE balanceR #-}---- | Insert a new maximal element.-insertMax :: IsBinTree c e => e -> c -> c-insertMax p t =-  case asBin t of-    TipTree -> bin p tip tip-    BinTree q l r -> balanceR q l (insertMax p r)---- | Insert a new minimal element.-insertMin :: IsBinTree c e => e -> c -> c-insertMin p t =-  case asBin t of-    TipTree -> bin p tip tip-    BinTree q l r -> balanceL q (insertMin p l) r---- | @link@ is called to insert a key and value between two disjoint subtrees.-link :: IsBinTree c e => e -> c -> c -> c-link p l r =-  case (asBin l, asBin r) of-    (TipTree, _) -> insertMin p r-    (_, TipTree) -> insertMax p l-    (BinTree py ly ry, BinTree pz lz rz)-     | delta*size l < size r -> balanceL pz (link p l lz) rz-     | delta*size r < size l -> balanceR py ly (link p ry r)-     | otherwise             -> bin p l r-{-# INLINE link #-}---- | A Strict pair-data PairS f s = PairS !f !s--deleteFindMin :: IsBinTree c e => e -> c -> c -> PairS e c-deleteFindMin p l r =-  case asBin l of-    TipTree -> PairS p r-    BinTree lp ll lr ->-      case deleteFindMin lp ll lr of-        PairS q l' -> PairS q (balanceR p l' r)-{-# INLINABLE deleteFindMin #-}--deleteFindMax :: IsBinTree c e => e -> c -> c -> PairS e c-deleteFindMax p l r =-  case asBin r of-    TipTree -> PairS p l-    BinTree rp rl rr ->-      case deleteFindMax rp rl rr of-        PairS q r' -> PairS q (balanceL p l r')-{-# INLINABLE deleteFindMax #-}---- | Concatenate two trees that are ordered with respect to each other.-merge :: IsBinTree c e => c -> c -> c-merge l r =-  case (asBin l, asBin r) of-    (TipTree, _) -> r-    (_, TipTree) -> l-    (BinTree x lx rx, BinTree y ly ry)-      | delta*size l < size r -> balanceL y (merge l ly) ry-      | delta*size r < size l -> balanceR x lx (merge rx r)-      | size l > size r ->-        case deleteFindMax x lx rx of-          PairS q l' -> balanceR q l' r-      | otherwise ->-        case deleteFindMin y ly ry of-          PairS q r' -> balanceL q l r'-{-# INLINABLE merge #-}----------------------------------------------------------------------------- Ordered operations---- | @insert p m@ inserts the binding into @m@.  It returns--- an Unchanged value if the map stays the same size and an updated--- value if a new entry was inserted.-insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c-insert comp x t =-  case asBin t of-    TipTree -> Updated (bin x tip tip)-    BinTree y l r ->-      case comp x y of-        LT ->-          case insert comp x l of-            Updated l'   -> Updated   (balanceL y l' r)-            Unchanged l' -> Unchanged (bin       y l' r)-        GT ->-          case insert comp x r of-            Updated r'   -> Updated   (balanceR y l r')-            Unchanged r' -> Unchanged (bin       y l r')-        EQ -> Unchanged (bin x l r)-{-# INLINABLE insert #-}---- | @glue l r@ concatenates @l@ and @r@.------ It assumes that @l@ and @r@ are already balanced with respect to each other.-glue :: IsBinTree c e => c -> c -> c-glue l r =-  case (asBin l, asBin r) of-    (TipTree, _) -> r-    (_, TipTree) -> l-    (BinTree x lx rx, BinTree y ly ry)-     | size l > size r ->-       case deleteFindMax x lx rx of-         PairS q l' -> balanceR q l' r-     | otherwise ->-       case deleteFindMin y ly ry of-         PairS q r' -> balanceL q l r'-{-# INLINABLE glue #-}--delete :: IsBinTree c e-       => (e -> Ordering)-          -- ^ Predicate that returns whether the entry is less than, greater than, or equal-          -- to the key we are entry that we are looking for.-       -> c-       -> MaybeS c-delete k t =-  case asBin t of-    TipTree -> NothingS-    BinTree p l r ->-      case k p of-        LT -> (\l' -> balanceR p l' r) <$> delete k l-        GT -> (\r' -> balanceL p l r') <$> delete k r-        EQ -> JustS (glue l r)-{-# INLINABLE delete #-}----------------------------------------------------------------------------- filter---- | Returns only entries that are less than predicate with respect to the ordering--- and Nothing if no elements are discarded.-filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c-filterGt k t =-  case asBin t of-    TipTree -> NothingS-    BinTree x l r ->-      case k x of-        LT -> (\l' -> link x l' r) <$> filterGt k l-        GT -> filterGt k r <|> JustS r-        EQ -> JustS r-{-# INLINABLE filterGt #-}----- | @filterLt k m@ returns submap of @m@ that only contains entries--- that are smaller than @k@.  If no entries are deleted then return Nothing.-filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c-filterLt k t =-  case asBin t of-    TipTree -> NothingS-    BinTree x l r ->-      case k x of-        LT -> filterLt k l <|> JustS l-        GT -> (\r' -> link x l r') <$> filterLt k r-        EQ -> JustS l-{-# INLINABLE filterLt #-}----------------------------------------------------------------------------- Union---- | Insert a new key and value in the map if it is not already present.--- Used by 'union'.-insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c-insertR comp e m = fromMaybeS m (go e m)-  where-    go :: e -> c -> MaybeS c-    go x t =-      case asBin t of-        TipTree -> JustS (bin x tip tip)-        BinTree y l r ->-          case comp x y of-            LT -> (\l' -> balanceL y l' r) <$> go x l-            GT -> (\r' -> balanceR y l r') <$> go x r-            EQ -> NothingS-{-# INLINABLE insertR #-}---- | Union two sets-union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c-union comp t1 t2 =-  case (asBin t1, asBin t2) of-    (TipTree, _) -> t2-    (_, TipTree) -> t1-    (_, BinTree p (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp p t1-    (BinTree x l r, _) ->-      link x-           (hedgeUnion_UB comp x   l t2)-           (hedgeUnion_LB comp x r   t2)-{-# INLINABLE union #-}---- | Hedge union where we only add elements in second map if key is--- strictly above a lower bound.-hedgeUnion_LB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c-hedgeUnion_LB comp lo t1 t2 =-  case (asBin t1, asBin t2) of-    (_, TipTree) -> t1-    (TipTree, _) -> fromMaybeS t2 (filterGt (comp lo) t2)-    -- Prune left tree.-    (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB comp lo t1 r-    -- Special case when t2 is a single element.-    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1-    -- Split on left-and-right subtrees of t1.-    (BinTree x l r, _) ->-      link x-           (hedgeUnion_LB_UB comp lo x  l t2)-           (hedgeUnion_LB    comp x     r t2)-{-# INLINABLE hedgeUnion_LB #-}---- | Hedge union where we only add elements in second map if key is--- strictly below a upper bound.-hedgeUnion_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c-hedgeUnion_UB comp hi t1 t2 =-  case (asBin t1, asBin t2) of-    (_, TipTree) -> t1-    (TipTree, _) -> fromMaybeS t2 (filterLt (comp hi) t2)-    -- Prune right tree.-    (_, BinTree x l _) | comp x hi >= EQ -> hedgeUnion_UB comp hi t1 l-    -- Special case when t2 is a single element.-    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree))  -> insertR comp x t1-    -- Split on left-and-right subtrees of t1.-    (BinTree x l r, _) ->-      link x-           (hedgeUnion_UB    comp x      l t2)-           (hedgeUnion_LB_UB comp x  hi  r t2)-{-# INLINABLE hedgeUnion_UB #-}---- | Hedge union where we only add elements in second map if key is--- strictly between a lower and upper bound.-hedgeUnion_LB_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> e -> c -> c -> c-hedgeUnion_LB_UB comp lo hi t1 t2 =-  case (asBin t1, asBin t2) of-    (_, TipTree) -> t1-    -- Prune left tree.-    (_,   BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB_UB comp lo hi t1 r-    -- Prune right tree.-    (_,   BinTree k l _) | comp k hi >= EQ -> hedgeUnion_LB_UB comp lo hi t1 l-    -- When t1 becomes empty (assumes lo <= k <= hi)-    (TipTree, BinTree x l r) ->-      case (filterGt (comp lo) l, filterLt (comp hi) r) of-        -- No variables in t2 were eliminated.-        (NothingS, NothingS) -> t2-        -- Relink t2 with filtered elements removed.-        (l',r') -> link x (fromMaybeS l l') (fromMaybeS r r')-    -- Special case when t2 is a single element.-    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1-    -- Split on left-and-right subtrees of t1.-    (BinTree x l r, _) ->-      link x-           (hedgeUnion_LB_UB comp lo x  l t2)-           (hedgeUnion_LB_UB comp x  hi r t2)-{-# INLINABLE hedgeUnion_LB_UB #-}+import Data.Parameterized.Utils.BinTree.Internal

@@ -0,0 +1,387 @@+{-|+Description      : Utilities for balanced binary trees (internal module).+Copyright        : (c) Galois, Inc 2014-2019+Maintainer       : Joe Hendrix <jhendrix@galois.com>++This module exports every helper in the file so that downstream modules+can attach @SPECIALIZE@ pragmas to the internal ones (e.g. 'insertMax',+'hedgeUnion_LB'). The stable public interface is re-exported from+"Data.Parameterized.Utils.BinTree".+-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE Safe #-}+module Data.Parameterized.Utils.BinTree.Internal+  ( MaybeS(..)+  , fromMaybeS+  , Updated(..)+  , updatedValue+  , TreeApp(..)+  , IsBinTree(..)+  , balanceL+  , balanceR+  , insertMax+  , insertMin+  , link+  , PairS(..)+  , deleteFindMin+  , deleteFindMax+  , merge+  , insert+  , glue+  , delete+  , filterGt+  , filterLt+  , insertR+  , union+  , hedgeUnion_LB+  , hedgeUnion_UB+  , hedgeUnion_LB_UB+  ) where++import Control.Applicative++------------------------------------------------------------------------+-- MaybeS++-- | A strict version of 'Maybe'+data MaybeS v+   = JustS !v+   | NothingS++instance Functor MaybeS where+  fmap _ NothingS = NothingS+  fmap f (JustS v) = JustS (f v)++instance Alternative MaybeS where+  empty = NothingS+  mv@JustS{} <|> _ = mv+  NothingS <|> v = v++instance Applicative MaybeS where+  pure = JustS++  NothingS <*> _ = NothingS+  JustS{} <*> NothingS = NothingS+  JustS f <*> JustS x = JustS (f x)++fromMaybeS :: a -> MaybeS a -> a+fromMaybeS r NothingS = r+fromMaybeS _ (JustS v) = v++------------------------------------------------------------------------+-- Updated++-- | @Updated a@ contains a value that has been flagged on whether it was+-- modified by an operation.+data Updated a+   = Updated   !a+   | Unchanged !a++updatedValue :: Updated a -> a+updatedValue (Updated a) = a+updatedValue (Unchanged a) = a++------------------------------------------------------------------------+-- IsBinTree++data TreeApp e t+   = BinTree !e !t !t+   | TipTree++class IsBinTree t e | t -> e where+  asBin :: t -> TreeApp e t+  tip :: t++  bin :: e -> t -> t -> t+  size :: t -> Int++delta,ratio :: Int+delta = 3+ratio = 2++-- | @balanceL p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.+--+-- It assumes that @l@ and @r@ are close to being balanced, and that only+-- @l@ may contain too many elements.+balanceL :: (IsBinTree c e) => e -> c -> c -> c+balanceL p l r = do+  case asBin l of+    BinTree l_pair ll lr | size l > max 1 (delta*size r) ->+      case asBin lr of+        BinTree lr_pair lrl lrr | size lr >= max 2 (ratio*size ll) ->+          bin lr_pair (bin l_pair ll lrl) (bin p lrr r)+        _ -> bin l_pair ll (bin p lr r)++    _ -> bin p l r+{-# INLINE balanceL #-}++-- | @balanceR p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.+--+-- It assumes that @l@ and @r@ are close to being balanced, and that only+-- @r@ may contain too many elements.+balanceR :: (IsBinTree c e) => e -> c -> c -> c+balanceR p l r = do+  case asBin r of+    BinTree r_pair rl rr | size r > max 1 (delta*size l) ->+      case asBin rl of+        BinTree rl_pair rll rlr | size rl >= max 2 (ratio*size rr) ->+          (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr+        _ -> bin r_pair (bin p l rl) rr+    _ -> bin p l r+{-# INLINE balanceR #-}++-- | Insert a new maximal element.+insertMax :: IsBinTree c e => e -> c -> c+insertMax p t =+  case asBin t of+    TipTree -> bin p tip tip+    BinTree q l r -> balanceR q l (insertMax p r)+{-# INLINABLE insertMax #-}++-- | Insert a new minimal element.+insertMin :: IsBinTree c e => e -> c -> c+insertMin p t =+  case asBin t of+    TipTree -> bin p tip tip+    BinTree q l r -> balanceL q (insertMin p l) r+{-# INLINABLE insertMin #-}++-- | @link@ is called to insert a key and value between two disjoint subtrees.+link :: IsBinTree c e => e -> c -> c -> c+link p l r =+  case (asBin l, asBin r) of+    (TipTree, _) -> insertMin p r+    (_, TipTree) -> insertMax p l+    (BinTree py ly ry, BinTree pz lz rz)+     | delta*size l < size r -> balanceL pz (link p l lz) rz+     | delta*size r < size l -> balanceR py ly (link p ry r)+     | otherwise             -> bin p l r+{-# INLINE link #-}++-- | A Strict pair+data PairS f s = PairS !f !s++deleteFindMin :: IsBinTree c e => e -> c -> c -> PairS e c+deleteFindMin = \p0 l0 r0 ->+  let go p l r =+        case asBin l of+          TipTree -> PairS p r+          BinTree lp ll lr ->+            case go lp ll lr of+              PairS q l' -> PairS q (balanceR p l' r)+  in go p0 l0 r0+{-# INLINE deleteFindMin #-}++deleteFindMax :: IsBinTree c e => e -> c -> c -> PairS e c+deleteFindMax = \p0 l0 r0 ->+  let go p l r =+        case asBin r of+          TipTree -> PairS p l+          BinTree rp rl rr ->+            case go rp rl rr of+              PairS q r' -> PairS q (balanceL p l r')+  in go p0 l0 r0+{-# INLINE deleteFindMax #-}++-- | Concatenate two trees that are ordered with respect to each other.+merge :: IsBinTree c e => c -> c -> c+merge l r =+  case (asBin l, asBin r) of+    (TipTree, _) -> r+    (_, TipTree) -> l+    (BinTree x lx rx, BinTree y ly ry)+      | delta*size l < size r -> balanceL y (merge l ly) ry+      | delta*size r < size l -> balanceR x lx (merge rx r)+      | size l > size r ->+        case deleteFindMax x lx rx of+          PairS q l' -> balanceR q l' r+      | otherwise ->+        case deleteFindMin y ly ry of+          PairS q r' -> balanceL q l r'+{-# INLINABLE merge #-}++------------------------------------------------------------------------+-- Ordered operations++-- | @insert p m@ inserts the binding into @m@.  It returns+-- an Unchanged value if the map stays the same size and an updated+-- value if a new entry was inserted.+insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c+insert comp x t =+  case asBin t of+    TipTree -> Updated (bin x tip tip)+    BinTree y l r ->+      case comp x y of+        LT ->+          case insert comp x l of+            Updated l'   -> Updated   (balanceL y l' r)+            Unchanged l' -> Unchanged (bin       y l' r)+        GT ->+          case insert comp x r of+            Updated r'   -> Updated   (balanceR y l r')+            Unchanged r' -> Unchanged (bin       y l r')+        EQ -> Unchanged (bin x l r)+{-# INLINABLE insert #-}++-- | @glue l r@ concatenates @l@ and @r@.+--+-- It assumes that @l@ and @r@ are already balanced with respect to each other.+glue :: IsBinTree c e => c -> c -> c+glue l r =+  case (asBin l, asBin r) of+    (TipTree, _) -> r+    (_, TipTree) -> l+    (BinTree x lx rx, BinTree y ly ry)+     | size l > size r ->+       case deleteFindMax x lx rx of+         PairS q l' -> balanceR q l' r+     | otherwise ->+       case deleteFindMin y ly ry of+         PairS q r' -> balanceL q l r'+{-# INLINABLE glue #-}++delete :: IsBinTree c e+       => (e -> Ordering)+          -- ^ Predicate that returns whether the entry is less than, greater than, or equal+          -- to the key we are entry that we are looking for.+       -> c+       -> MaybeS c+delete k t =+  case asBin t of+    TipTree -> NothingS+    BinTree p l r ->+      case k p of+        LT -> (\l' -> balanceR p l' r) <$> delete k l+        GT -> (\r' -> balanceL p l r') <$> delete k r+        EQ -> JustS (glue l r)+{-# INLINABLE delete #-}++------------------------------------------------------------------------+-- filter++-- | Returns only entries that are less than predicate with respect to the ordering+-- and Nothing if no elements are discarded.+filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c+filterGt k t =+  case asBin t of+    TipTree -> NothingS+    BinTree x l r ->+      case k x of+        LT -> (\l' -> link x l' r) <$> filterGt k l+        GT -> filterGt k r <|> JustS r+        EQ -> JustS r+{-# INLINABLE filterGt #-}+++-- | @filterLt k m@ returns submap of @m@ that only contains entries+-- that are smaller than @k@.  If no entries are deleted then return Nothing.+filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c+filterLt k t =+  case asBin t of+    TipTree -> NothingS+    BinTree x l r ->+      case k x of+        LT -> filterLt k l <|> JustS l+        GT -> (\r' -> link x l r') <$> filterLt k r+        EQ -> JustS l+{-# INLINABLE filterLt #-}++------------------------------------------------------------------------+-- Union++-- | Insert a new key and value in the map if it is not already present.+-- Used by 'union'.+insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c+insertR comp e m = fromMaybeS m (go e m)+  where+    go :: e -> c -> MaybeS c+    go x t =+      case asBin t of+        TipTree -> JustS (bin x tip tip)+        BinTree y l r ->+          case comp x y of+            LT -> (\l' -> balanceL y l' r) <$> go x l+            GT -> (\r' -> balanceR y l r') <$> go x r+            EQ -> NothingS+{-# INLINABLE insertR #-}++-- | Union two sets+union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c+union comp t1 t2 =+  case (asBin t1, asBin t2) of+    (TipTree, _) -> t2+    (_, TipTree) -> t1+    (_, BinTree p (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp p t1+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_UB comp x   l t2)+           (hedgeUnion_LB comp x r   t2)+{-# INLINABLE union #-}++-- | Hedge union where we only add elements in second map if key is+-- strictly above a lower bound.+hedgeUnion_LB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c+hedgeUnion_LB comp lo t1 t2 =+  case (asBin t1, asBin t2) of+    (_, TipTree) -> t1+    (TipTree, _) -> fromMaybeS t2 (filterGt (comp lo) t2)+    -- Prune left tree.+    (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB comp lo t1 r+    -- Special case when t2 is a single element.+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1+    -- Split on left-and-right subtrees of t1.+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_LB_UB comp lo x  l t2)+           (hedgeUnion_LB    comp x     r t2)+{-# INLINABLE hedgeUnion_LB #-}++-- | Hedge union where we only add elements in second map if key is+-- strictly below a upper bound.+hedgeUnion_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c+hedgeUnion_UB comp hi t1 t2 =+  case (asBin t1, asBin t2) of+    (_, TipTree) -> t1+    (TipTree, _) -> fromMaybeS t2 (filterLt (comp hi) t2)+    -- Prune right tree.+    (_, BinTree x l _) | comp x hi >= EQ -> hedgeUnion_UB comp hi t1 l+    -- Special case when t2 is a single element.+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree))  -> insertR comp x t1+    -- Split on left-and-right subtrees of t1.+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_UB    comp x      l t2)+           (hedgeUnion_LB_UB comp x  hi  r t2)+{-# INLINABLE hedgeUnion_UB #-}++-- | Hedge union where we only add elements in second map if key is+-- strictly between a lower and upper bound.+hedgeUnion_LB_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> e -> c -> c -> c+hedgeUnion_LB_UB comp lo hi t1 t2 =+  case (asBin t1, asBin t2) of+    (_, TipTree) -> t1+    -- Prune left tree.+    (_,   BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB_UB comp lo hi t1 r+    -- Prune right tree.+    (_,   BinTree k l _) | comp k hi >= EQ -> hedgeUnion_LB_UB comp lo hi t1 l+    -- When t1 becomes empty (assumes lo <= k <= hi)+    (TipTree, BinTree x l r) ->+      case (filterGt (comp lo) l, filterLt (comp hi) r) of+        -- No variables in t2 were eliminated.+        (NothingS, NothingS) -> t2+        -- Relink t2 with filtered elements removed.+        (l',r') -> link x (fromMaybeS l l') (fromMaybeS r r')+    -- Special case when t2 is a single element.+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1+    -- Split on left-and-right subtrees of t1.+    (BinTree x l r, _) ->+      link x+           (hedgeUnion_LB_UB comp lo x  l t2)+           (hedgeUnion_LB_UB comp x  hi r t2)+{-# INLINABLE hedgeUnion_LB_UB #-}

@@ -11,11 +11,12 @@   ) where +import           Data.Hashable (hashWithSalt) import           Numeric.Natural (Natural)  import           Hedgehog import qualified Hedgehog.Gen as HG-import           Hedgehog.Range (linear)+import           Hedgehog.Range (linear, linearBounded) import           Test.Tasty (TestTree, testGroup) import           Test.Tasty.Hedgehog (testPropertyNamed) import           Test.Tasty.HUnit (assertBool, testCase)@@ -41,6 +42,14 @@          Just LeqProof -> mkFin x          Nothing -> error "Impossible" +prop_eq_hash :: Property+prop_eq_hash = property $+  do salt <- forAll (HG.int linearBounded)+     (f1, f2) <- forAll $+                 HG.filter (\(f1, f2) -> f1 == f2) $+                 (,) <$> genFin (knownNat @100) <*> genFin (knownNat @100)+     hashWithSalt salt f1 === hashWithSalt salt f2+ prop_count_true :: Property prop_count_true = property $   do Some n <- forAll (genNatRepr 100)@@ -51,6 +60,117 @@   do Some n <- forAll (genNatRepr 100)      finToNat (countFin n (\_ _ -> False)) === 0 +prop_add_comm :: Property+prop_add_comm = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     b <- forAll (genFin n10)+     (a + b) === (b + a)++prop_add_identity :: Property+prop_add_identity = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     (mkFin (knownNat @0) + a) === a++prop_add_inverse :: Property+prop_add_inverse = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     (a + negate a) === mkFin (knownNat @0)++prop_add_assoc :: Property+prop_add_assoc = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     b <- forAll (genFin n10)+     c <- forAll (genFin n10)+     a + (b + c) === (a + b) + c++prop_add_negate_sub :: Property+prop_add_negate_sub = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     b <- forAll (genFin n10)+     (a + negate b) === (a - b)++prop_sub_anticomm :: Property+prop_sub_anticomm = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     b <- forAll (genFin n10)+     (a - b) === negate (b - a)++prop_mul_comm :: Property+prop_mul_comm = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     b <- forAll (genFin n10)+     (a * b) === (b * a)++prop_mul_identity :: Property+prop_mul_identity = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     (mkFin (knownNat @1) * a) === a++prop_mul_assoc :: Property+prop_mul_assoc = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     b <- forAll (genFin n10)+     c <- forAll (genFin n10)+     a * (b * c) === (a * b) * c++prop_mul_annihilate :: Property+prop_mul_annihilate = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     (mkFin (knownNat @0) * a) === mkFin (knownNat @0)++prop_neg_inv :: Property+prop_neg_inv = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     negate (negate a) === a++prop_abs_idem :: Property+prop_abs_idem = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     abs (abs a) === abs a++prop_signum_idem :: Property+prop_signum_idem = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     signum (signum a) === signum a++prop_abs_signum :: Property+prop_abs_signum = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     (abs a * signum a) === a++prop_recip_1 :: Property+prop_recip_1 = property $+  do let n1 = knownNat @1+     a <- forAll (genFin n1)+     recipFinModN n1 a === Just (mkFin (knownNat @0))++prop_recip_10 :: Property+prop_recip_10 = property $+  do let n10 = knownNat @10+     a <- forAll (genFin n10)+     let aInv = recipFinModN n10 a+     let d = gcd (finToNat a) (natValue n10)+     case aInv of+       Nothing ->+         assert $ d >= 1+       Just aInv' ->+         do d === 1+            (a * aInv') === mkFin (knownNat @1)+ finTests :: IO TestTree finTests =   testGroup "Fin" <$>@@ -63,9 +183,44 @@           assertBool             "minBound <= maxBound (2)"             ((minBound :: Fin 2) <= (minBound :: Fin 2))+      , testCase "show (minFin @1) == \"Fin 0\"" $+          assertBool+            "show (minFin @1) == \"Fin 0\""+            (show (minFin @1) == "Fin 0")+      , testCase "show (Just (minFin @1)) == \"Just (Fin 0)\"" $+          assertBool+            "show (Just (minFin @1)) == \"Just (Fin 0)\""+            (show (Just (minFin @1)) == "Just (Fin 0)")+      , testCase "fromInteger @(Fin 7) (-1) == fromInteger 6" $+          assertBool+            "fromInteger @(Fin 7) (-1) == fromInteger 6"+            (fromInteger @(Fin 7) (-1) == fromInteger 6) +      , testPropertyNamed+          "Eq equality implies hash equality"+          "prop_eq_hash"+          prop_eq_hash+       , testPropertyNamed "count-true" "prop_count_true" prop_count_true       , testPropertyNamed "count-false" "prop_count_false" prop_count_false++      , testPropertyNamed "add-comm" "prop_add_comm" prop_add_comm+      , testPropertyNamed "add-identity" "prop_add_identity" prop_add_identity+      , testPropertyNamed "add-inverse" "prop_add_inverse" prop_add_inverse+      , testPropertyNamed "add-assoc" "prop_add_assoc" prop_add_assoc+      , testPropertyNamed "add-negate-sub" "prop_add_negate_sub" prop_add_negate_sub+      , testPropertyNamed "sub-anticomm" "prop_sub_anticomm" prop_sub_anticomm+      , testPropertyNamed "mul-comm" "prop_mul_comm" prop_mul_comm+      , testPropertyNamed "mul-identity" "prop_mul_identity" prop_mul_identity+      , testPropertyNamed "mul-annihilate" "prop_mul_annihilate" prop_mul_annihilate+      , testPropertyNamed "mul-assoc" "prop_mul_assoc" prop_mul_assoc+      , testPropertyNamed "neg-inv" "prop_neg_inv" prop_neg_inv+      , testPropertyNamed "abs-idem" "prop_abs_idem" prop_abs_idem+      , testPropertyNamed "signum-idem" "prop_signum_idem" prop_signum_idem+      , testPropertyNamed "abs-signum" "prop_abs_signum" prop_abs_signum++      , testPropertyNamed "recip-1" "prop_recip_1" prop_recip_1+      , testPropertyNamed "recip-10" "prop_recip_10" prop_recip_10  #if __GLASGOW_HASKELL__ >= 806       , testCase "Eq-Fin-laws-1" $