parameterized-utils 2.1.3.0 → 2.1.4.0

raw patch · 25 files changed

+1187/−45 lines, 25 filesdep +hedgehog-classesdep +indexed-traversabledep +profunctorsPVP ok

version bump matches the API change (PVP)

Dependencies added: hedgehog-classes, indexed-traversable, profunctors

API changes (from Hackage documentation)

Files

• Changelog.md +25/−0
• parameterized-utils.cabal +16/−3
• src/Data/Parameterized/Axiom.hs +48/−0
• src/Data/Parameterized/Classes.hs +10/−1
• src/Data/Parameterized/Context/Safe.hs +11/−0
• src/Data/Parameterized/Context/Unsafe.hs +13/−1
• src/Data/Parameterized/Ctx/Proofs.hs +3/−3
• src/Data/Parameterized/Fin.hs +111/−0
• src/Data/Parameterized/List.hs +70/−2
• src/Data/Parameterized/NatRepr.hs +13/−12
• src/Data/Parameterized/NatRepr/Internal.hs +3/−2
• src/Data/Parameterized/Nonce.hs +2/−2
• src/Data/Parameterized/Nonce/Unsafe.hs +2/−1
• src/Data/Parameterized/Peano.hs +6/−5
• src/Data/Parameterized/SymbolRepr.hs +2/−1
• src/Data/Parameterized/TH/GADT.hs +243/−0
• src/Data/Parameterized/TraversableFC.hs +6/−1
• src/Data/Parameterized/TraversableFC/WithIndex.hs +175/−0
• src/Data/Parameterized/Vector.hs +57/−2
• test/Test/Context.hs +53/−1
• test/Test/Fin.hs +68/−0
• test/Test/List.hs +29/−0
• test/Test/TH.hs +83/−0
• test/Test/Vector.hs +132/−8
• test/UnitTest.hs +6/−0

@@ -1,5 +1,30 @@ # Changelog for the `parameterized-utils` package +## 2.1.4.0 -- *2021 Oct 1*++  * Added the `ifoldLM` and `fromSomeList`, `fromListWith`, and+    `fromListWithM` functions to the `List` module.+  * Fix the description of the laws of the `OrdF` class.+  * Fix a bug in which `Data.Parameterized.Vector.{join,joinWith,joinWithM}`+    and `Data.Parameterized.NatRepr.plusAssoc` could crash at runtime if+    compiled without optimizations.+  * Add a `Data.Parameterized.Axiom` module providing `unsafeAxiom` and+    `unsafeHeteroAxiom`, which can construct proofs of equality between types+    that GHC isn't able to prove on its own. These functions are unsafe if used+    improperly, so the responsibility is on the programmer to ensure that these+    functions are used appropriately.+  * Various `Proxy` enhancements: adds `KnownRepr`, `EqF`, and `ShowF` instances.+  * Adds `mkRepr` and `mkKnownReprs` Template Haskell functions.+  * Added `TraversableFC.WithIndex` module which provides the+    `FunctorFCWithIndex`, `FoldableFCWithIndex`, and+    `TraversableFCWithIndex` classes, with instances defined for+    `Assignment` and `List`.+  * Added `indicesUpTo`, and `indicesOf` as well as `iterateN` and `iterateNM`+    for the `Vector` module.+  * Added `Data.Parameterized.Fin` for finite types which can be used+    to index into a `Vector n` or other size-indexed datatypes.++ ## 2.1.3.0 -- *2021 Mar 23*    * Add support for GHC 9.

@@ -1,8 +1,8 @@ Cabal-version: 2.2 Name:          parameterized-utils-Version:       2.1.3.0+Version:       2.1.4.0 Author:        Galois Inc.-Maintainer:    jhendrix@galois.com, kquick@galois.com+Maintainer:    kquick@galois.com stability:     stable Build-type:    Simple Copyright:     ©2016-2021 Galois, Inc.@@ -19,7 +19,7 @@ extra-source-files: Changelog.md homepage:      https://github.com/GaloisInc/parameterized-utils bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues-tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.1+tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.1  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -58,8 +58,10 @@                , ghc-prim                , hashable       >=1.2  && <1.4                , hashtables     ==1.2.*+               , indexed-traversable                , lens           >=4.16 && <5.1                , mtl+               , profunctors    >=5.6 && < 5.7                , template-haskell                , text                , vector         ==0.12.*@@ -69,6 +71,7 @@   exposed-modules:     Data.Parameterized     Data.Parameterized.All+    Data.Parameterized.Axiom     Data.Parameterized.BoolRepr     Data.Parameterized.Classes     Data.Parameterized.ClassesC@@ -80,6 +83,7 @@     Data.Parameterized.Ctx.Proofs     Data.Parameterized.DataKind     Data.Parameterized.DecidableEq+    Data.Parameterized.Fin     Data.Parameterized.HashTable     Data.Parameterized.List     Data.Parameterized.Map@@ -94,6 +98,7 @@     Data.Parameterized.TH.GADT     Data.Parameterized.TraversableF     Data.Parameterized.TraversableFC+    Data.Parameterized.TraversableFC.WithIndex     Data.Parameterized.Utils.BinTree     Data.Parameterized.Utils.Endian     Data.Parameterized.Vector@@ -114,14 +119,18 @@   main-is: UnitTest.hs   other-modules:     Test.Context+    Test.Fin+    Test.List     Test.NatRepr     Test.SymbolRepr+    Test.TH     Test.Vector    build-depends: base                , hashable                , hashtables                , hedgehog+               , indexed-traversable                , ghc-prim                , lens                , mtl@@ -130,3 +139,7 @@                , tasty-ant-xml == 1.1.*                , tasty-hunit >= 0.9 && < 0.11                , tasty-hedgehog++  if impl(ghc >= 8.6)+    build-depends:+      hedgehog-classes

@@ -0,0 +1,48 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Unsafe #-}+{-|+Copyright        : (c) Galois, Inc 2014-2021++An unsafe module that provides functionality for constructing equality proofs+that GHC cannot prove on its own.+-}+module Data.Parameterized.Axiom+  ( unsafeAxiom, unsafeHeteroAxiom+  ) where++import Data.Type.Equality+import Unsafe.Coerce (unsafeCoerce)++-- | Assert a proof of equality between two types.+-- This is unsafe if used improperly, so use this with caution!+unsafeAxiom :: forall a b. a :~: b+unsafeAxiom = unsafeCoerce (Refl @a)+{-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]++-- | Assert a proof of heterogeneous equality between two types.+-- This is unsafe if used improperly, so use this with caution!+unsafeHeteroAxiom :: forall a b. a :~~: b+unsafeHeteroAxiom = unsafeCoerce (HRefl @a)+{-# NOINLINE unsafeHeteroAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]++{-+Note [Mark unsafe axioms as NOINLINE]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+We take care to mark definitions that use unsafeCoerce to construct proofs+(e.g., unsafeAxiom = unsafeCoerce Refl) as NOINLINE. There are at least two+good reasons to do so:++1. On old version of GHC (prior to 9.0), GHC was liable to optimize+   `unsafeCoerce` too aggressively, leading to unsound runtime behavior.+   See https://gitlab.haskell.org/ghc/ghc/-/issues/16893 for an example.++2. If GHC too heavily optimizes a program which cases on a proof of equality,+   where the equality is between two types that can be determined not to be+   equal statically (e.g., case (unsafeAxiom :: Bool :~: Int) of ...), then the+   optimized program can crash at runtime. See+   https://gitlab.haskell.org/ghc/ghc/-/issues/16310. Using NOINLINE is+   sufficient to work around the issue.+-}

@@ -12,6 +12,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -103,6 +104,9 @@ instance Eq a => EqF (Const a) where   eqF (Const x) (Const y) = x == y +instance EqF Proxy where+  eqF _ _ = True+ ------------------------------------------------------------------------ -- PolyEq @@ -174,7 +178,7 @@ -- -- Furthermore, when @x@ and @y@ both have type @(k tp)@, we expect: ----- * @compareF x y == EQF@ equals @compare x y@ when @Ord (k tp)@ has an instance.+-- * @toOrdering (compareF x y)@ equals @compare x y@ when @Ord (k tp)@ has an instance. -- * @isJust (testEquality x y)@ equals @x == y@ when @Eq (k tp)@ has an instance. -- -- Minimal complete definition: either 'compareF' or 'leqF'.@@ -272,6 +276,8 @@  instance Show x => ShowF (Const x) +instance ShowF Proxy+ ------------------------------------------------------------------------ -- IxedF @@ -357,3 +363,6 @@ -- kind @k@. class KnownRepr (f :: k -> Type) (ctx :: k) where   knownRepr :: f ctx++instance KnownRepr Proxy ctx where+  knownRepr = Proxy

@@ -124,6 +124,7 @@ import Data.Parameterized.NatRepr import Data.Parameterized.Some import Data.Parameterized.TraversableFC+import Data.Parameterized.TraversableFC.WithIndex  ------------------------------------------------------------------------ -- Size@@ -615,6 +616,15 @@ instance TraversableFC Assignment where   traverseFC f = traverseF f +instance FunctorFCWithIndex Assignment where+  imapFC = imapFCDefault++instance FoldableFCWithIndex Assignment where+  ifoldMapFC = ifoldMapFCDefault++instance TraversableFCWithIndex Assignment where+  itraverseFC = traverseWithIndex+ -- | Map assignment map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c map f = fmapFC f@@ -650,6 +660,7 @@ zipWith f = \x y -> runIdentity $ zipWithM (\u v -> pure (f u v)) x y {-# INLINE zipWith #-} +-- | This is a specialization of 'itraverseFC'. traverseWithIndex :: Applicative m                   => (forall tp . Index ctx tp -> f tp -> m (g tp))                   -> Assignment f ctx

@@ -98,6 +98,7 @@ import           Unsafe.Coerce import           Data.Kind(Type) +import           Data.Parameterized.Axiom import           Data.Parameterized.Classes import           Data.Parameterized.Ctx import           Data.Parameterized.Ctx.Proofs@@ -105,6 +106,7 @@ import           Data.Parameterized.NatRepr.Internal (NatRepr(NatRepr)) import           Data.Parameterized.Some import           Data.Parameterized.TraversableFC+import           Data.Parameterized.TraversableFC.WithIndex  ------------------------------------------------------------------------ -- Size@@ -245,7 +247,7 @@  instance TestEquality (Index ctx) where   testEquality (Index i) (Index j)-    | i == j = Just (unsafeCoerce Refl)+    | i == j = Just unsafeAxiom     | otherwise = Nothing  instance Ord (Index ctx tp) where@@ -926,6 +928,16 @@ instance TraversableFC Assignment where   traverseFC = \f (Assignment x) -> Assignment <$> traverse_bin f x   {-# INLINE traverseFC #-}++instance FunctorFCWithIndex Assignment where+  imapFC = imapFCDefault++instance FoldableFCWithIndex Assignment where+  ifoldMapFC = ifoldMapFCDefault++instance TraversableFCWithIndex Assignment where+  itraverseFC = traverseWithIndex+  traverseWithIndex :: Applicative m                   => (forall tp . Index ctx tp -> f tp -> m (g tp))

@@ -13,12 +13,12 @@   ) where  import Data.Type.Equality-import Unsafe.Coerce +import Data.Parameterized.Axiom import Data.Parameterized.Ctx  leftId :: p x -> (EmptyCtx <+> x) :~: x-leftId _ = unsafeCoerce Refl+leftId _ = unsafeAxiom  assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z-assoc _ _ _ = unsafeCoerce Refl+assoc _ _ _ = unsafeAxiom

@@ -0,0 +1,111 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++{-|+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+  , viewFin+  , finToNat+  , embed+  , tryEmbed+  , minFin+  , 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+  i == j = finToNat i == finToNat j++instance Ord (Fin n) where+  compare i j = compare (finToNat i) (finToNat j)++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.+instance Show (Fin n) where+  show i = "Fin " ++ show (finToNat i)++mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n+mkFin = Fin++viewFin ::  (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r+viewFin f (Fin i) = f i++finToNat :: Fin n -> Natural+finToNat (Fin i) = natValue i++embed :: forall n m. (n <= m) => Fin n -> Fin m+embed =+  viewFin+    (\(x :: NatRepr o) ->+      case leqTrans (LeqProof :: LeqProof (o + 1) n) (LeqProof :: LeqProof n m) of+        LeqProof -> Fin x+    )++tryEmbed :: NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)+tryEmbed n m i =+  case testLeq n m of+    Just LeqProof -> Just (embed i)+    Nothing -> Nothing++-- | The smallest element of @'Fin' n@+minFin :: (1 <= n) => Fin n+minFin = Fin (knownNat @0)++fin0Void :: Iso' (Fin 0) Void+fin0Void =+  iso+    (viewFin+      (\(x :: NatRepr o) ->+        case plusComm x (knownNat @1) of+          Refl ->+            case addIsLeqLeft1 @1 @o @0 LeqProof of {}))+    absurd++fin1Unit :: Iso' (Fin 1) ()+fin1Unit = iso (const ()) (const minFin)++fin2Bool :: Iso' (Fin 2) Bool+fin2Bool =+  iso+    (viewFin+      (\n ->+         case isZeroNat n of+           ZeroNat -> False+           NonZeroNat -> True))+    (\b -> if b then maxBound else minBound)

@@ -129,15 +129,20 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Data.Parameterized.List   ( List(..)+  , fromSomeList+  , fromListWith+  , fromListWithM   , Index(..)   , indexValue   , (!!)   , update   , indexed   , imap+  , ifoldlM   , ifoldr   , izipWith   , itraverse@@ -149,11 +154,15 @@   ) where  import qualified Control.Lens as Lens+import           Data.Foldable import           Data.Kind import           Prelude hiding ((!!))+import           Unsafe.Coerce (unsafeCoerce)  import           Data.Parameterized.Classes+import           Data.Parameterized.Some import           Data.Parameterized.TraversableFC+import           Data.Parameterized.TraversableFC.WithIndex  -- | Parameterized list of elements. data List :: (k -> Type) -> [k] -> Type where@@ -185,6 +194,18 @@   traverseFC _ Nil = pure Nil   traverseFC f (h :< r) = (:<) <$> f h <*> traverseFC f r +type instance IndexF   (List (f :: k -> Type) sh) = Index sh+type instance IxValueF (List (f :: k -> Type) sh) = f++instance FunctorFCWithIndex List where+  imapFC = imap++instance FoldableFCWithIndex List where+  ifoldrFC = ifoldr++instance TraversableFCWithIndex List where+  itraverseFC = itraverse+ instance TestEquality f => TestEquality (List f) where   testEquality Nil Nil = Just Refl   testEquality (xh :< xl) (yh :< yl) = do@@ -202,17 +223,38 @@     lexCompareF xl yl $     EQF - instance KnownRepr (List f) '[] where   knownRepr = Nil  instance (KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f) (s ': sh) where   knownRepr = knownRepr :< knownRepr +-- | Apply function to list to yield a parameterized list.+fromListWith :: forall a f . (a -> Some f) -> [a] -> Some (List f)+fromListWith f = foldr g (Some Nil)+  where g :: a -> Some (List f) -> Some (List f)+        g x (Some r) = viewSome (\h -> Some (h :< r)) (f x)++-- | Apply monadic action to list to yield a parameterized list.+fromListWithM :: forall a f m+                  .  Monad m+                  => (a -> m (Some f))+                  -> [a]+                  -> m (Some (List f))+fromListWithM f = foldrM g (Some Nil)+  where g :: a -> Some (List f) -> m (Some (List f))+        g x (Some r) = viewSome (\h -> Some (h :< r)) <$> f x++-- | Map from list of Some to Some list+fromSomeList :: [Some f] -> Some (List f)+fromSomeList = fromListWith id++{-# INLINABLE fromListWith #-}+{-# INLINABLE fromListWithM #-}+ -------------------------------------------------------------------------------- -- * Indexed operations - -- | Represents an index into a type-level list. Used in place of integers to --   1. ensure that the given index *does* exist in the list --   2. guarantee that it has the given kind@@ -294,6 +336,8 @@  -- | Map over the elements in the list, and provide the index into -- each element along with the element itself.+--+-- This is a specialization of 'imapFC'. imap :: forall f g l      . (forall x . Index l x -> f x -> g x)      -> List f l@@ -309,7 +353,29 @@         Nil -> Nil         e :< rest -> f (g IndexHere) e :< go (g . IndexThere) rest +-- | Left fold with an additional index.+ifoldlM :: forall sh a b m+        . Monad m+        => (forall tp . b -> Index sh tp -> a tp -> m b)+        -> b+        -> List a sh+        -> m b+ifoldlM _ b Nil = pure b+ifoldlM f b0 (a0 :< r0) = f b0 IndexHere a0 >>= go IndexHere r0+  where+    go :: forall tps tp+        . Index sh tp+       -> List a tps+       -> b+       -> m b+    go _ Nil b = pure b+    go idx (a :< rest) b =+      let idx' = unsafeCoerce (IndexThere idx)+       in f b idx' a >>= go idx' rest+ -- | Right-fold with an additional index.+--+-- This is a specialization of 'ifoldrFC'. ifoldr :: forall sh a b . (forall tp . Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b ifoldr f seed0 l = go id l seed0   where@@ -342,6 +408,8 @@           f (g IndexHere) a b :< go (g . IndexThere) as' bs'  -- | Traverse with an additional index.+--+-- This is a specialization of 'itraverseFC'. itraverse :: forall a b sh t           . Applicative t           => (forall tp . Index sh tp -> a tp -> t (b tp))

@@ -136,6 +136,7 @@ import GHC.TypeNats as TypeNats import Unsafe.Coerce +import Data.Parameterized.Axiom import Data.Parameterized.NatRepr.Internal import Data.Parameterized.Some @@ -155,7 +156,7 @@ withKnownNat (NatRepr nVal) v =   case someNatVal nVal of     SomeNat (Proxy :: Proxy n') ->-      case unsafeCoerce (Refl :: n :~: n) :: n :~: n' of+      case unsafeAxiom :: n :~: n' of         Refl -> v  data IsZeroNat n where@@ -223,7 +224,7 @@ withDivModNat n m f =   case ( Some (NatRepr divPart), Some (NatRepr modPart)) of      ( Some (divn :: NatRepr div), Some (modn :: NatRepr mod) )-       -> case unsafeCoerce (Refl :: 0 :~: 0) of+       -> case unsafeAxiom of             (Refl :: (n :~: ((div * m) + mod))) -> f divn modn   where     (divPart, modPart) = divMod (natValue n) (natValue m)@@ -302,15 +303,15 @@  -- | Produce evidence that @+@ is commutative. plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m-plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n)+plusComm _ _ = unsafeAxiom  -- | Produce evidence that @+@ is associative. plusAssoc :: forall f m g n h o . f m -> g n -> h o -> m+(n+o) :~: (m+n)+o-plusAssoc = unsafeCoerce (Refl :: m+(n+o) :~: m+(n+o))+plusAssoc _ _ _ = unsafeAxiom  -- | Produce evidence that @*@ is commutative. mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)-mulComm _ _ = unsafeCoerce Refl+mulComm _ _ = unsafeAxiom  mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n) mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of@@ -318,14 +319,14 @@  -- | Cancel an add followed by a subtract plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m-plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m)+plusMinusCancel _ _ = unsafeAxiom  minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m-minusPlusCancel _ _ = unsafeCoerce (Refl :: m :~: m)+minusPlusCancel _ _ = unsafeAxiom  addMulDistribRight :: forall n m p f g h. f n -> g m -> h p                     -> ((n * p) + (m * p)) :~: ((n + m) * p)-addMulDistribRight _n _m _p = unsafeCoerce Refl+addMulDistribRight _n _m _p = unsafeAxiom   @@ -338,7 +339,7 @@ withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p                     -> ( (((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a withSubMulDistribRight _n _m _p f =-  case unsafeCoerce (Refl :: 0 :~: 0) of+  case unsafeAxiom of     (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f  ------------------------------------------------------------------------@@ -363,7 +364,7 @@               -> Either (LeqProof (m+1) n) (m :~: n) testStrictLeq (NatRepr m) (NatRepr n)   | m < n = Left (unsafeCoerce (LeqProof :: LeqProof 0 0))-  | otherwise = Right (unsafeCoerce (Refl :: m :~: m))+  | otherwise = Right unsafeAxiom {-# NOINLINE testStrictLeq #-}  -- As for NatComparison above, but works with LeqProof@@ -610,8 +611,8 @@  mulCancelR ::   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)-mulCancelR _ _ _ = unsafeCoerce Refl+mulCancelR _ _ _ = unsafeAxiom  -- | Used in @Vector@ lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)-lemmaMul = unsafeCoerce Refl+lemmaMul _ _ = unsafeAxiom

@@ -27,6 +27,7 @@ import Numeric.Natural import Unsafe.Coerce +import Data.Parameterized.Axiom import Data.Parameterized.Classes import Data.Parameterized.DecidableEq @@ -49,12 +50,12 @@  instance TestEquality NatRepr where   testEquality (NatRepr m) (NatRepr n)-    | m == n = Just (unsafeCoerce Refl)+    | m == n = Just unsafeAxiom     | otherwise = Nothing  instance DecidableEq NatRepr where   decEq (NatRepr m) (NatRepr n)-    | m == n    = Left $ unsafeCoerce Refl+    | m == n    = Left unsafeAxiom     | otherwise = Right $         \x -> seq x $ error "Impossible [DecidableEq on NatRepr]" 

@@ -48,11 +48,11 @@ import Data.Kind import Data.IORef import Data.STRef-import Data.Typeable import Data.Word import Unsafe.Coerce import System.IO.Unsafe (unsafePerformIO) +import Data.Parameterized.Axiom import Data.Parameterized.Classes import Data.Parameterized.Some @@ -129,7 +129,7 @@ type role Nonce nominal nominal  instance TestEquality (Nonce s) where-  testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl)+  testEquality x y | indexValue x == indexValue y = Just unsafeAxiom                    | otherwise = Nothing  instance OrdF (Nonce s) where

@@ -43,6 +43,7 @@ import Data.Word import Unsafe.Coerce +import Data.Parameterized.Axiom import Data.Parameterized.Classes  -- | A simple type that for getting fresh indices in the 'ST' monad.@@ -64,7 +65,7 @@ type role Nonce nominal  instance TestEquality Nonce where-  testEquality x y | indexValue x == indexValue y = unsafeCoerce (Just Refl)+  testEquality x y | indexValue x == indexValue y = Just unsafeAxiom                    | otherwise = Nothing  instance OrdF Nonce where

@@ -88,6 +88,7 @@ import           Data.Word  #ifdef UNSAFE_OPS+import           Data.Parameterized.Axiom import           Unsafe.Coerce(unsafeCoerce) #endif @@ -221,7 +222,7 @@ instance TestEquality PeanoRepr where #ifdef UNSAFE_OPS   testEquality (PeanoRepr m) (PeanoRepr n)-    | m == n = Just (unsafeCoerce Refl)+    | m == n = Just unsafeAxiom     | otherwise = Nothing #else   testEquality ZRepr ZRepr = Just Refl@@ -235,7 +236,7 @@ instance DecidableEq PeanoRepr where #ifdef UNSAFE_OPS   decEq (PeanoRepr m) (PeanoRepr n)-    | m == n    = Left $ unsafeCoerce Refl+    | m == n    = Left unsafeAxiom     | otherwise = Right $         \x -> seq x $ error "Impossible [DecidableEq on PeanoRepr]" #else@@ -452,7 +453,7 @@   Assignment f t1 -> Assignment f t2 ->   CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1) #ifdef UNSAFE_OPS-plusCtxSizeAxiom _t1 _t2 = unsafeCoerce Refl+plusCtxSizeAxiom _t1 _t2 = unsafeAxiom #else plusCtxSizeAxiom t1 t2 =   case viewAssign t2 of@@ -467,7 +468,7 @@   PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->   Minus n (Plus t' t) :~: Minus (Minus n t') t #ifdef UNSAFE_OPS-minusPlusAxiom _n _t _t' = unsafeCoerce Refl+minusPlusAxiom _n _t _t' = unsafeAxiom #else minusPlusAxiom n t t' = case peanoView t' of   ZRepr -> Refl@@ -484,7 +485,7 @@   PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->   Lt (Plus t' t) n :~: 'True #ifdef UNSAFE_OPS-ltMinusPlusAxiom _n _t _t' = unsafeCoerce Refl+ltMinusPlusAxiom _n _t _t' = unsafeAxiom #else ltMinusPlusAxiom n t t' = case peanoView n of   SRepr m -> case peanoView t' of

@@ -44,6 +44,7 @@ import           Data.Proxy import qualified Data.Text as Text +import           Data.Parameterized.Axiom import           Data.Parameterized.Classes import           Data.Parameterized.Some @@ -81,7 +82,7 @@  instance TestEquality SymbolRepr where    testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)-      | x == y    = Just (unsafeCoerce (Refl :: x :~: x))+      | x == y    = Just unsafeAxiom       | otherwise = Nothing instance OrdF SymbolRepr where    compareF (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)

@@ -25,6 +25,10 @@   , structuralHash   , structuralHashWithSalt   , PolyEq(..)+    -- * Repr generators (\"singletons\")+    -- $reprs+  , mkRepr+  , mkKnownReprs     -- * Template haskell utilities that may be useful in other contexts.   , DataD   , lookupDataType'@@ -493,6 +497,204 @@ matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ matchShowCtor p con = showCon p (constructorName con) (length (constructorFields con)) +-- | Generate a \"repr\" or singleton type from a data kind. For nullary+-- constructors, this works as follows:+--+-- @+-- data T1 = A | B | C+-- \$(mkRepr ''T1)+-- ======>+-- data T1Repr (tp :: T1)+--   where+--     ARepr :: T1Repr 'A+--     BRepr :: T1Repr 'B+--     CRepr :: T1Repr 'C+-- @+--+-- For constructors with fields, we assume each field type @T@ already has a+-- corresponding repr type @TRepr :: T -> *@.+--+-- @+-- data T2 = T2_1 T1 | T2_2 T1+-- \$(mkRepr ''T2)+-- ======>+-- data T2Repr (tp :: T2)+--   where+--     T2_1Repr :: T1Repr tp -> T2Repr ('T2_1 tp)+--     T2_2Repr :: T1Repr tp -> T2Repr ('T2_2 tp)+-- @+--+-- Constructors with multiple fields work fine as well:+--+-- @+-- data T3 = T3 T1 T2+-- \$(mkRepr ''T3)+-- ======>+-- data T3Repr (tp :: T3)+--   where+--     T3Repr :: T1Repr tp1 -> T2Repr tp2 -> T3Repr ('T3 tp1 tp2)+-- @+--+-- This is generally compatible with other \"repr\" types provided by+-- @parameterized-utils@, such as @NatRepr@ and @PeanoRepr@:+--+-- @+-- data T4 = T4_1 Nat | T4_2 Peano+-- \$(mkRepr ''T4)+-- ======>+-- data T4Repr (tp :: T4)+--   where+--     T4Repr :: NatRepr tp1 -> PeanoRepr tp2 -> T4Repr ('T4 tp1 tp2)+-- @+--+-- The data kind must be \"simple\", i.e. it must be monomorphic and only+-- contain user-defined data constructors (no lists, tuples, etc.). For example,+-- the following will not work:+--+-- @+-- data T5 a = T5 a+-- \$(mkRepr ''T5)+-- ======>+-- Foo.hs:1:1: error:+--     Exception when trying to run compile-time code:+--       mkRepr cannot be used on polymorphic data kinds.+-- @+--+-- Similarly, this will not work:+--+-- @+-- data T5 = T5 [Nat]+-- \$(mkRepr ''T5)+-- ======>+-- Foo.hs:1:1: error:+--     Exception when trying to run compile-time code:+--       mkRepr cannot be used on this data kind.+-- @+--+-- Note that at a minimum, you will need the following extensions to use this macro:+--+-- @+-- {-\# LANGUAGE DataKinds \#-}+-- {-\# LANGUAGE GADTs \#-}+-- {-\# LANGUAGE KindSignatures \#-}+-- {-\# LANGUAGE TemplateHaskell \#-}+-- @+mkRepr :: Name -> DecsQ+mkRepr typeName = do+  let reprTypeName = mkReprName typeName+      varName = mkName "tp"+  info <- lookupDataType' typeName+  let gc ci = do+        let ctorName = constructorName ci+            reprCtorName = mkReprName ctorName+            ctorFieldTypeNames = getCtorName <$> constructorFields ci+            ctorFieldReprNames = mkReprName <$> ctorFieldTypeNames+        -- Generate a list of type variables to be supplied as type arguments+        -- for each repr argument.+        tvars <- replicateM (length (constructorFields ci)) (newName "tp")+        let appliedType =+              foldl AppT (PromotedT (constructorName ci)) (VarT <$> tvars)+            ctorType = AppT (ConT reprTypeName) appliedType+            ctorArgTypes =+              zipWith (\n v -> (Bang NoSourceUnpackedness NoSourceStrictness, AppT (ConT n) (VarT v))) ctorFieldReprNames tvars+        return $ GadtC+          [reprCtorName]+          ctorArgTypes+          ctorType+  ctors <- mapM gc (datatypeCons info)+  return $ [ DataD [] reprTypeName+             [kindedTV varName (ConT typeName)]+             Nothing+             ctors+             []+           ]+  where getCtorName :: Type -> Name+        getCtorName c = case c of+          ConT nm -> nm+          VarT _ -> error $ "mkRepr cannot be used on polymorphic data kinds."+          _ -> error $ "mkRepr cannot be used on this data kind."++-- | Generate @KnownRepr@ instances for each constructor of a data kind. Given a+-- data kind @T@, we assume a repr type @TRepr (t :: T)@ is in scope with+-- structure that perfectly matches @T@ (using 'mkRepr' to generate the repr+-- type will guarantee this).+--+-- Given data kinds @T1@, @T2@, and @T3@ from the documentation of 'mkRepr', and+-- the associated repr types @T1Repr@, @T2Repr@, and @T3Repr@, we can use+-- 'mkKnownReprs' to generate these instances like so:+--+-- @+-- \$(mkKnownReprs ''T1)+-- ======>+-- instance KnownRepr T1Repr 'A where+--   knownRepr = ARepr+-- instance KnownRepr T1Repr 'B where+--   knownRepr = BRepr+-- instance KnownRepr T1Repr 'C where+--   knownRepr = CRepr+-- @+--+-- @+-- \$(mkKnownReprs ''T2)+-- ======>+-- instance KnownRepr T1Repr tp =>+--          KnownRepr T2Repr ('T2_1 tp) where+--   knownRepr = T2_1Repr knownRepr+-- @+--+-- @+-- \$(mkKnownReprs ''T3)+-- ======>+-- instance (KnownRepr T1Repr tp1, KnownRepr T2Repr tp2) =>+--          KnownRepr T3Repr ('T3_1 tp1 tp2) where+--   knownRepr = T3_1Repr knownRepr knownRepr+-- @+--+-- The same restrictions that apply to 'mkRepr' also apply to 'mkKnownReprs'.+-- The data kind must be \"simple\", i.e. it must be monomorphic and only+-- contain user-defined data constructors (no lists, tuples, etc.).+--+-- Note that at a minimum, you will need the following extensions to use this macro:+--+-- @+-- {-\# LANGUAGE DataKinds \#-}+-- {-\# LANGUAGE GADTs \#-}+-- {-\# LANGUAGE KindSignatures \#-}+-- {-\# LANGUAGE MultiParamTypeClasses \#-}+-- {-\# LANGUAGE TemplateHaskell \#-}+-- @+--+-- Also, 'mkKnownReprs' must be used in the same module as the definition of+-- the repr type (not necessarily for the data kind).+mkKnownReprs :: Name -> DecsQ+mkKnownReprs typeName = do+  kr <- [t|KnownRepr|]+  let krFName = mkName "knownRepr"+      reprTypeName = mkReprName typeName+  typeInfo <- lookupDataType' typeName+  reprInfo <- lookupDataType' reprTypeName+  forM (zip (datatypeCons typeInfo) (datatypeCons reprInfo)) $ \(tci, rci) -> do+    vars <- replicateM (length (constructorFields tci)) (newName "tp")+    krReqs <- forM (zip (constructorFields tci) vars) $ \(tfld, v) -> do+      let fldReprName = mkReprName (getCtorName tfld)+      return $ AppT (AppT kr (ConT fldReprName)) (VarT v)+    let appliedType =+          foldl AppT (PromotedT (constructorName tci)) (VarT <$> vars)+        krConstraint = AppT (AppT kr (ConT reprTypeName)) appliedType+        krExp = foldl AppE (ConE (constructorName rci)) $+          map (const (VarE krFName)) vars+        krDec = FunD krFName [Clause [] (NormalB krExp) []]++    return $ InstanceD Nothing krReqs krConstraint [krDec]+  where getCtorName :: Type -> Name+        getCtorName c = case c of+          ConT nm -> nm+          VarT _ -> error $ "mkKnownReprs cannot be used on polymorphic data kinds."+          _ -> error $ "mkKnownReprs cannot be used on this data kind."++mkReprName :: Name -> Name+mkReprName nm = mkName (nameBase nm ++ "Repr")+ -- $typePatterns -- -- The Template Haskell instance generators 'structuralEquality',@@ -532,3 +734,44 @@ -- -- The use of 'DataArg' says that the type parameter of the 'NatRepr' must -- be the same as the second type parameter of @T@.++-- $reprs+--+-- When working with data kinds with run-time representatives, we encourage+-- users of @parameterized-utils@ to use the following convention. Given a data+-- kind defined by+--+-- @+-- data T = ...+-- @+--+-- users should also supply a GADT @TRepr@ parameterized by @T@, e.g.+--+-- @+-- data TRepr (t :: T) where ...+-- @+--+-- Each constructor of @TRepr@ should correspond to a constructor of @T@. If @T@+-- is defined by+--+-- @+-- data T = A | B Nat+-- @+--+-- we have a corresponding+--+-- @+-- data TRepr (t :: T) where+--   ARepr :: TRepr 'A+--   BRepr :: NatRepr w -> TRepr ('B w)+-- @+--+-- Assuming the user of @parameterized-utils@ follows this convention, we+-- provide the Template Haskell construct 'mkRepr' to automate the creation of+-- the @TRepr@ GADT. We also provide 'mkKnownReprs', which generates 'KnownRepr'+-- instances for that GADT type. See the documentation for those two functions+-- for more detailed explanations.+--+-- NB: These macros are inspired by the corresponding macros provided by+-- @singletons-th@, and the \"repr\" programming idiom is very similar to the one+-- used by @singletons@.

@@ -45,7 +45,12 @@  import Data.Parameterized.Classes --- | A parameterized type that is a function on all instances.+-- | A parameterized type that is a functor on all instances.+--+-- Laws:+--+-- [Identity]    @'fmapFC' 'id' == 'id'@+-- [Composition] @'fmapFC' (f . g) == 'fmapFC' f . 'fmapFC' g@ class FunctorFC (t :: (k -> Type) -> l -> Type) where   fmapFC :: forall f g. (forall x. f x -> g x) ->                         (forall x. t f x -> t g x)

@@ -0,0 +1,175 @@+------------------------------------------------------------------------+-- |+-- Module           : Data.Parameterized.TraversableFC.WithIndex+-- Copyright        : (c) Galois, Inc 2021+-- Maintainer       : Langston Barrett+-- Description      : 'TraversableFC' classes, but with indices.+--+-- As in the package indexed-traversable.+------------------------------------------------------------------------+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module Data.Parameterized.TraversableFC.WithIndex+  ( FunctorFCWithIndex(..)+  , FoldableFCWithIndex(..)+  , ifoldlMFC+  , ifoldrMFC+  , iallFC+  , ianyFC+  , TraversableFCWithIndex(..)+  , imapFCDefault+  , ifoldMapFCDefault+  ) where++import Data.Functor.Const (Const(Const, getConst))+import Data.Functor.Identity (Identity(Identity, runIdentity))+import Data.Kind+import Data.Monoid (All(..), Any(..), Endo(Endo), appEndo, Dual(Dual, getDual))+import Data.Profunctor.Unsafe ((#.))+import GHC.Exts (build)++import Data.Parameterized.Classes+import Data.Parameterized.TraversableFC++class FunctorFC t => FunctorFCWithIndex (t :: (k -> Type) -> l -> Type) where+  -- | Like 'fmapFC', but with an index.+  --+  -- @+  -- 'fmapFC' f ≡ 'imapFC' ('const' f)+  -- @+  imapFC ::+    forall f g z.+    (forall x. IndexF (t f z) x -> f x -> g x)+    -> t f z+    -> t g z++------------------------------------------------------------------------++class (FoldableFC t, FunctorFCWithIndex t) => FoldableFCWithIndex (t :: (k -> Type) -> l -> Type) where++  -- | Like 'foldMapFC', but with an index.+  --+  -- @+  -- 'foldMapFC' f ≡ 'ifoldMapFC' ('const' f)+  -- @+  ifoldMapFC ::+    forall f m z.+    Monoid m =>+    (forall x. IndexF (t f z) x -> f x -> m) ->+    t f z ->+    m+  ifoldMapFC f = ifoldrFC (\i x -> mappend (f i x)) mempty++  -- | Like 'foldrFC', but with an index.+  ifoldrFC ::+    forall z f b.+    (forall x. IndexF (t f z) x -> f x -> b -> b) ->+    b ->+    t f z ->+    b+  ifoldrFC f z t = appEndo (ifoldMapFC (\i x -> Endo (f i x)) t) z++  -- | Like 'foldlFC', but with an index.+  ifoldlFC ::+    forall f b z.+    (forall x. IndexF (t f z) x -> b -> f x -> b) ->+    b ->+    t f z ->+    b+  ifoldlFC f z t =+    appEndo (getDual (ifoldMapFC (\i e -> Dual (Endo (\r -> f i r e))) t)) z++  -- | Like 'ifoldrFC', but with an index.+  ifoldrFC' ::+    forall f b z.+    (forall x. IndexF (t f z) x -> f x -> b -> b) ->+    b ->+    t f z ->+    b+  ifoldrFC' f0 z0 xs = ifoldlFC (f' f0) id xs z0+    where f' f i k x z = k $! f i x z++  -- | Like 'ifoldlFC', but with an index.+  ifoldlFC' :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)+  ifoldlFC' f0 z0 xs = foldrFC (f' f0) id xs z0+    where f' f x k z = k $! f z x++  -- | Convert structure to list.+  itoListFC ::+    forall f a z.+    (forall x. IndexF (t f z) x -> f x -> a) ->+    t f z ->+    [a]+  itoListFC f t = build (\c n -> ifoldrFC (\i e v -> c (f i e) v) n t)++-- | Like 'foldlMFC', but with an index.+ifoldlMFC ::+  FoldableFCWithIndex t =>+  Monad m =>+  (forall x. IndexF (t f z) x -> b -> f x -> m b) ->+  b ->+  t f z ->+  m b+ifoldlMFC f z0 xs = ifoldlFC (\i k x z -> f i z x >>= k) return xs z0++-- | Like 'foldrMFC', but with an index.+ifoldrMFC ::+  FoldableFCWithIndex t =>+  Monad m =>+  (forall x. IndexF (t f z) x -> f x -> b -> m b) ->+  b ->+  t f z ->+  m b+ifoldrMFC f z0 xs = ifoldlFC (\i k x z -> f i x z >>= k) return xs z0++-- | Like 'allFC', but with an index.+iallFC ::+  FoldableFCWithIndex t =>+  (forall x. IndexF (t f z) x -> f x -> Bool) ->+  t f z ->+  Bool+iallFC p = getAll #. ifoldMapFC (\i x -> All (p i x))++-- | Like 'anyFC', but with an index.+ianyFC ::+  FoldableFCWithIndex t =>+  (forall x. IndexF (t f z) x -> f x -> Bool) ->+  t f z -> Bool+ianyFC p = getAny #. ifoldMapFC (\i x -> Any (p i x))++------------------------------------------------------------------------++class (TraversableFC t, FoldableFCWithIndex t) => TraversableFCWithIndex (t :: (k -> Type) -> l -> Type) where+  -- | Like 'traverseFC', but with an index.+  --+  -- @+  -- 'traverseFC' f ≡ 'itraverseFC' ('const' f)+  -- @+  itraverseFC ::+    forall m z f g.+    Applicative m =>+    (forall x. IndexF (t f z) x -> f x -> m (g x)) ->+    t f z ->+    m (t g z)++imapFCDefault ::+  forall t f g z.+  TraversableFCWithIndex t =>+  (forall x. IndexF (t f z) x -> f x -> g x)+  -> t f z+  -> t g z+imapFCDefault f = runIdentity #. itraverseFC (\i x -> Identity (f i x))+{-# INLINEABLE imapFCDefault #-}++ifoldMapFCDefault ::+  forall t m z f.+  TraversableFCWithIndex t =>+  Monoid m =>+  (forall x. IndexF (t f z) x -> f x -> m) ->+  t f z ->+  m+ifoldMapFCDefault f = getConst #. itraverseFC (\i x -> Const (f i x))+{-# INLINEABLE ifoldMapFCDefault #-}

@@ -1,4 +1,5 @@ {-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# Language PatternGuards #-} {-# Language PolyKinds #-} {-# Language TypeApplications, ScopedTypeVariables #-}@@ -36,6 +37,10 @@   , elemAtMaybe   , elemAtUnsafe +    -- * Indexing with Fin+  , indicesUpTo+  , indicesOf+     -- * Update   , insertAt   , insertAtMaybe@@ -74,6 +79,8 @@   , unfoldrM   , unfoldrWithIndex   , unfoldrWithIndexM+  , iterateN+  , iterateNM      -- * Splitting and joining     -- ** General@@ -90,15 +97,19 @@   ) where  import qualified Data.Vector as Vector-import Data.Functor.Compose import Data.Coerce+import Data.Foldable.WithIndex (FoldableWithIndex(ifoldMap))+import Data.Functor.Compose+import Data.Functor.WithIndex (FunctorWithIndex(imap)) import Data.Vector.Mutable (MVector) import qualified Data.Vector.Mutable as MVector import Control.Monad.ST import Data.Functor.Identity+import Data.Parameterized.Fin import Data.Parameterized.NatRepr import Data.Parameterized.NatRepr.Internal import Data.Proxy+import Data.Traversable.WithIndex (TraversableWithIndex(itraverse)) import Prelude hiding (length,reverse,zipWith) import Numeric.Natural @@ -150,7 +161,36 @@ elemAtUnsafe n (Vector xs) = xs Vector.! n {-# INLINE elemAtUnsafe #-} +-------------------------------------------------------------------------------- +indicesUpTo :: NatRepr n -> Vector (n + 1) (Fin (n + 1))+indicesUpTo n =+  iterateN+    n+    (viewFin+      (\x ->+        case testStrictLeq (incNat x) (incNat n) of+          Left LeqProof -> mkFin (incNat x)+          Right Refl -> mkFin n))+    (case addPrefixIsLeq n (knownNat @1) of+       LeqProof -> mkFin (knownNat @0))++indicesOf :: Vector n a -> Vector n (Fin n)+indicesOf v@(Vector _) = -- Pattern match to bring 1 <= n into scope+  case minusPlusCancel (length v) (knownNat @1) of+    Refl -> indicesUpTo (decNat (length v))++instance FunctorWithIndex (Fin n) (Vector n) where+  imap f v = zipWith f (indicesOf v) v++instance FoldableWithIndex (Fin n) (Vector n) where+  ifoldMap f v = foldMap (uncurry f) (imap (,) v)++instance TraversableWithIndex (Fin n) (Vector n) where+  itraverse f v = traverse (uncurry f) (imap (,) v)++--------------------------------------------------------------------------------+ -- | Insert an element at the given index. -- @O(n)@. insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a@@ -320,7 +360,6 @@   zs  = Vector.generate len (\i -> let v = if even i then xs else ys                                    in v Vector.! (i `div` 2)) - --------------------------------------------------------------------------------  {- | Move the elements around, as specified by the given function.@@ -519,6 +558,22 @@        -> b        -> Vector (h + 1) a unfoldr h gen start = unfoldrWithIndex h (\_ v -> gen v) start++-- | Build a vector by repeatedly applying a monadic function to a seed value.+--+-- Compare to 'Vector.iterateNM'.+iterateNM :: Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)+iterateNM h f start =+  case isZeroNat h of+    ZeroNat -> pure (singleton start)+    NonZeroNat -> cons start <$> unfoldrM (predNat h) (fmap dup . f) start+  where dup x = (x, x)++-- | Build a vector by repeatedly applying a function to a seed value.+--+-- Compare to 'Vector.iterateN'+iterateN :: NatRepr n -> (a -> a) -> a -> Vector (n + 1) a+iterateN h f start = runIdentity (iterateNM h (Identity . f) start)  -------------------------------------------------------------------------------- 

@@ -3,6 +3,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -27,6 +28,7 @@ import qualified Data.Parameterized.Ctx.Proofs as P import           Data.Parameterized.Some import           Data.Parameterized.TraversableFC+import           Data.Parameterized.TraversableFC.WithIndex import           Hedgehog import qualified Hedgehog.Gen as HG import           Hedgehog.Range@@ -58,13 +60,25 @@  instance ShowF Payload - twiddle :: Payload a -> Payload a twiddle (IntPayload n) = IntPayload (n+1) twiddle (StringPayload str) = StringPayload (str++"asdf") twiddle (BoolPayload b) = BoolPayload (not b) +twaddle :: Payload a -> Payload a+twaddle (IntPayload n) = IntPayload (n-1)+twaddle (StringPayload str) = StringPayload (reverse str)+twaddle (BoolPayload b) = BoolPayload (not b) +newtype Fun = Fun (forall a. Payload a -> Payload a)++instance Show Fun where+  show _ = "unshowable"++-- | Functions for e.g. testing functor laws+funs :: [Fun]+funs = [Fun twiddle, Fun twaddle, Fun id]+ ---------------------------------------------------------------------- -- Create another parameterized type for testing.  This one is not a -- GADT, which will require some interesting implementation tricks.@@ -323,6 +337,44 @@         let (x', x'') = C.unzip zipped         assert $ isJust $ testEquality x x'         assert $ isJust $ testEquality x x''++   , testProperty "fmapFC_identity" $ property $+     do Some x <- mkUAsgn <$> forAll genSomePayloadList+        assert $ isJust $ testEquality x (fmapFC id x)++   , testProperty "fmapFC_assoc" $ property $+     do Some x <- mkUAsgn <$> forAll genSomePayloadList+        Fun f <- forAll $ HG.element funs+        Fun g <- forAll $ HG.element funs+        assert $ isJust $ testEquality+                            (fmapFC g (fmapFC f x))+                            (fmapFC (g . f) x)++   , testProperty "imapFC_index_noop" $ property $+     do Some x <- mkUAsgn <$> forAll genSomePayloadList+        assert $+          isJust $+            testEquality x (imapFC (\idx _ -> x U.! idx) x)++   , testProperty "imapFC/fmapFC" $ property $+     do Some x <- mkUAsgn <$> forAll genSomePayloadList+        Fun f <- forAll $ HG.element funs+        assert $ isJust $ testEquality+                            (fmapFC f x)+                            (imapFC (const f) x)++   , testProperty "ifoldMapFC/foldMapFC" $ property $+     do Some x <- mkUAsgn <$> forAll genSomePayloadList+        assert $ foldMapFC show x == ifoldMapFC (const show) x++   , testProperty "itraverseFC/traverseFC" $ property $+     do Some x <- mkUAsgn <$> forAll genSomePayloadList+        Fun f <- forAll $ HG.element funs+        let f' :: forall a. Payload a -> Identity (Payload a)+            f' = Identity . f+        assert $ isJust $ testEquality+                            (runIdentity (traverseFC f' x))+                            (runIdentity (itraverseFC (const f') x))     , testCaseSteps "explicit indexing (unsafe)" $ \step -> do        let mkUPayload :: U.Assignment Payload TestCtx

@@ -0,0 +1,68 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# Language CPP #-}++module Test.Fin+  ( finTests+  , genFin+  )+where++import           Numeric.Natural (Natural)++import           Hedgehog+import qualified Hedgehog.Gen as HG+import           Hedgehog.Range (linear)+import           Test.Tasty (TestTree, testGroup)+import           Test.Tasty.HUnit (assertBool, testCase)++import           Data.Parameterized.NatRepr+import           Data.Parameterized.Fin+import           Data.Parameterized.Some (Some(Some))++#if __GLASGOW_HASKELL__ >= 806+import qualified Hedgehog.Classes as HC+#endif++genFin :: (0 <= n, Monad m) => NatRepr n -> GenT m (Fin n)+genFin n =+  do x0 <- HG.integral (linear 0 ((natValue n) - 1 :: Natural))+     Some x <- return (mkNatRepr x0)+     return $+       case testLeq (incNat x) n of+         Just LeqProof -> mkFin x+         Nothing -> error "Impossible"++finTests :: IO TestTree+finTests =+  testGroup "Fin" <$>+    return+      [ testCase "minBound <= maxBound (1)" $+          assertBool+            "minBound <= maxBound (1)"+            ((minBound :: Fin 1) <= (minBound :: Fin 1))+      , testCase "minBound <= maxBound (2)" $+          assertBool+            "minBound <= maxBound (2)"+            ((minBound :: Fin 2) <= (minBound :: Fin 2))++#if __GLASGOW_HASKELL__ >= 806+      , testCase "Eq-Fin-laws-1" $+          assertBool "Eq-Fin-laws-1" =<<+            HC.lawsCheck (HC.eqLaws (genFin (knownNat @1)))++      , testCase "Ord-Fin-laws-1" $+          assertBool "Ord-Fin-laws-1" =<<+            HC.lawsCheck (HC.ordLaws (genFin (knownNat @1)))++      , testCase "Eq-Fin-laws-10" $+          assertBool "Eq-Fin-laws-10" =<<+            HC.lawsCheck (HC.eqLaws (genFin (knownNat @10)))++      , testCase "Ord-Fin-laws-10" $+          assertBool "Ord-Fin-laws-10" =<<+            HC.lawsCheck (HC.ordLaws (genFin (knownNat @10)))+#endif+      ]

@@ -0,0 +1,29 @@+module Test.List+  ( tests+  ) where++import           Control.Monad.Identity+import           Data.Functor.Const+import qualified Data.Parameterized.List as PL+import           Data.Parameterized.Some+import           Test.Tasty+import           Test.Tasty.HUnit++-- | Test ifoldlM indexing is correct by summing a list using it.+testIfoldlMSum :: [Integer] -> TestTree+testIfoldlMSum l =+  testCase ("ifoldlMSum " ++ show l) $+    case PL.fromListWith (Some . Const) l of+      Some pl ->+        let expected = sum l+            actual = PL.ifoldlM (\r i v -> Identity $ r + if pl PL.!! i == v then getConst v else 0) 0 pl+        in expected @?= runIdentity actual+++tests :: TestTree+tests = testGroup "List"+  [ testIfoldlMSum []+  , testIfoldlMSum [1]+  , testIfoldlMSum [1,2]+  , testIfoldlMSum [1,2,3]+  ]

@@ -0,0 +1,83 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}++module Test.TH+  ( thTests+  )+where++import           Test.Tasty+import           Test.Tasty.HUnit++import           Control.Monad (when)+import           Data.Parameterized.Classes+import           Data.Parameterized.NatRepr+import           Data.Parameterized.TH.GADT+import           GHC.TypeNats++data T1 = A | B | C+$(mkRepr ''T1)+$(mkKnownReprs ''T1)+$(return [])+instance TestEquality T1Repr where+  testEquality = $(structuralTypeEquality [t|T1Repr|] [])+deriving instance Show (T1Repr t)++data T2 = T2_1 T1 | T2_2 Nat+$(mkRepr ''T2)+$(mkKnownReprs ''T2)+$(return [])+instance TestEquality T2Repr where+  testEquality = $(structuralTypeEquality [t|T2Repr|]+                    [ (AnyType, [|testEquality|]) ])+deriving instance Show (T2Repr t)++eqTest :: (TestEquality f, Show (f a), Show (f b)) => f a -> f b -> IO ()+eqTest a b =+  when (not (isJust (testEquality a b))) $ assertFailure $ show a ++ " /= " ++ show b++neqTest :: (TestEquality f, Show (f a), Show (f b)) => f a -> f b -> IO ()+neqTest a b =+  when (isJust (testEquality a b)) $ assertFailure $ show a ++ " == " ++ show b++thTests :: IO TestTree+thTests = testGroup "TH" <$> return+  [ testCase "Repr equality test" $ do+      -- T1+      ARepr `eqTest` ARepr+      ARepr `neqTest` BRepr+      BRepr `eqTest` BRepr+      BRepr `neqTest` CRepr+      -- T2+      T2_1Repr ARepr `eqTest` T2_1Repr ARepr+      T2_2Repr (knownNat @5) `eqTest` T2_2Repr (knownNat @5)+      T2_1Repr ARepr `neqTest` T2_1Repr CRepr+      T2_2Repr (knownNat @5) `neqTest` T2_2Repr (knownNat @9)+      T2_1Repr BRepr `neqTest` T2_2Repr (knownNat @4)++  , testCase "KnownRepr test" $ do+      -- T1+      let aRepr = knownRepr :: T1Repr 'A+          bRepr = knownRepr :: T1Repr 'B+          cRepr = knownRepr :: T1Repr 'C+      aRepr `eqTest` ARepr+      bRepr `eqTest` BRepr+      cRepr `eqTest` CRepr+      --T2+      let t2ARepr = knownRepr :: T2Repr ('T2_1 'A)+          t2BRepr = knownRepr :: T2Repr ('T2_1 'B)+          t25Repr = knownRepr :: T2Repr ('T2_2 5)+      t2ARepr `eqTest` T2_1Repr ARepr+      t2BRepr `eqTest` T2_1Repr BRepr+      t25Repr `eqTest` T2_2Repr (knownNat @5)+      t2ARepr `neqTest` t2BRepr+      t2ARepr `neqTest` t25Repr+      t2BRepr `neqTest` t25Repr+  ]

@@ -1,3 +1,4 @@+{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE TypeApplications #-} {-# Language CPP #-} {-# Language DataKinds #-}@@ -18,9 +19,12 @@ where  import           Data.Functor.Const (Const(..))+import           Data.Functor.WithIndex (imap)+import           Data.Foldable.WithIndex (ifoldMap) import           Data.Maybe (isJust) import qualified Data.List as List import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.Fin import           Data.Parameterized.NatRepr import           Data.Parameterized.Some import           Data.Parameterized.Vector@@ -29,15 +33,42 @@ import           Hedgehog import qualified Hedgehog.Gen as HG import           Hedgehog.Range-import           Prelude hiding (take, reverse)+import           Numeric.Natural (Natural)+import           Prelude hiding (take, reverse, length) import qualified Prelude as P+import           Test.Fin (genFin) import           Test.Tasty import           Test.Tasty.Hedgehog import           Test.Context (genSomePayloadList, mkUAsgn) +#if __GLASGOW_HASKELL__ >= 806+import qualified Hedgehog.Classes as HC+import           Test.Tasty.HUnit (assertBool, testCase)+#endif -genVector :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)-genVector genElem =+data SomeVector a = forall n. SomeVector (Vector n a)++instance Show a => Show (SomeVector a) where+  show (SomeVector v) = show v++genVectorOfLength :: (Monad m) => NatRepr n -> GenT m a -> GenT m (Vector (n + 1) a)+genVectorOfLength n genElem =+  do let w = widthVal n+     l <- HG.list (linear (w + 1) (w + 1)) genElem+     case testLeq (knownNat @1) (incNat n) of+       Nothing -> error "testLeq in genSomeVector"+       Just LeqProof ->+         case fromList (incNat n) l of+           Just v -> return v+           Nothing -> error ("fromList failure for size " <> show w)++genSomeVector :: (Monad m) => GenT m a -> GenT m (SomeVector a)+genSomeVector genElem =+  do Some len <- mkNatRepr <$> HG.integral (linear 0 (99 :: Natural))+     SomeVector <$> genVectorOfLength len genElem++genVectorKnownLength :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)+genVectorKnownLength genElem =   do let n = knownNat          w = widthVal n      l <- HG.list (constant w w) genElem@@ -48,17 +79,33 @@ genOrdering :: Monad m => GenT m Ordering genOrdering = HG.element [ LT, EQ, GT ] - instance Show (a -> b) where   show _ = "unshowable" +-- Used to test e.g., 'fmap (g . f) = fmap g . fmap f' and 'imap (const f) =+-- fmap f'.+orderingEndomorphisms :: [Ordering -> Ordering]+orderingEndomorphisms =+  [ const EQ+  , id+  , \case+      EQ -> EQ+      LT -> GT+      GT -> LT+  , \case+      LT -> EQ+      EQ -> GT+      GT -> LT+  ]  -- We use @Ordering@ just because it's simple vecTests :: IO TestTree vecTests = testGroup "Vector" <$> return   [ testProperty "reverse100" $ property $-    do v <- forAll $ genVector @100 genOrdering-       v === (reverse $ reverse v)+    do SomeVector v <- forAll $ genSomeVector genOrdering+       case testLeq (knownNat @1) (length v) of+         Nothing -> pure ()+         Just LeqProof -> v === (reverse $ reverse v)   , testProperty "reverseSingleton" $ property $     do l <- (:[]) <$> forAll genOrdering        Just v <- return $ fromList (knownNat @1) l@@ -66,7 +113,7 @@    , testProperty "split-join" $ property $     do let n = knownNat @5-       v <- forAll $ genVector @(5 * 5) genOrdering+       v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering        v === (join n $ split n (knownNat @5) v)    -- @cons@ is the same for vectors or lists@@ -145,4 +192,81 @@                           testEquality                             (a Ctx.! Ctx.lastIndex sz) lastElem)                    (getConst (a' Ctx.! Ctx.lastIndex sz))-    ]++  -- NOTE: We don't use hedgehog-classes here, because the way the types work+  -- would require this to only tests vectors of some fixed size.+  --+  -- Also, for 'fmap-compose', hedgehog-classes only tests two fixed functions+  -- over integers.+  , testProperty "fmap-id" $ property $+    do SomeVector v <- forAll $ genSomeVector genOrdering+       fmap id v === v++  , testProperty "fmap-compose" $ property $+    do SomeVector v <- forAll $ genSomeVector genOrdering+       f <- forAll $ HG.element orderingEndomorphisms+       g <- forAll $ HG.element orderingEndomorphisms+       fmap (g . f) v === fmap g (fmap f v)++  , testProperty "iterateN-range" $ property $+    do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))+       toList (iterateN len (+1) 0) === [0..(natValue len)]++  , testProperty "indicesOf-range" $ property $+    do SomeVector v <- forAll $ genSomeVector genOrdering+       toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]++  , testProperty "imap-const" $ property $+    do f <- forAll $ HG.element orderingEndomorphisms+       SomeVector v <- forAll $ genSomeVector genOrdering+       imap (const f) v === fmap f v++  , testProperty "ifoldMap-const" $ property $+    do let funs :: [ Ordering -> String ]+           funs = [const "s", show]+       f <- forAll $ HG.element funs+       SomeVector v <- forAll $ genSomeVector genOrdering+       ifoldMap (const f) v === foldMap f v++  , testProperty "imap-const-indicesOf" $ property $+    do SomeVector v <- forAll $ genSomeVector genOrdering+       imap const v === indicesOf v++  , testProperty "imap-elemAt" $ property $+    do SomeVector v <- forAll $ genSomeVector genOrdering+       imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v++  , testProperty "Ord-Eq-VectorIndex" $ property $+    do i <- forAll $ genFin (knownNat @10)+       j <- forAll $ genFin (knownNat @10)+       (i == j) === (compare i j == EQ)++#if __GLASGOW_HASKELL__ >= 806+  -- Test a few different sizes since the types force each test to use a+  -- specific size vector.+  , testCase "Eq-Vector-laws-1" $+      assertBool "Eq-Vector-laws-1" =<<+        HC.lawsCheck (HC.eqLaws (genVectorKnownLength @1 genOrdering))+  , testCase "Eq-Vector-laws-10" $+      assertBool "Eq-Vector-laws-10" =<<+        HC.lawsCheck (HC.eqLaws (genVectorKnownLength @10 genOrdering))+  , testCase "Show-Vector-laws-1" $+      assertBool "Show-Vector-laws-1" =<<+        HC.lawsCheck (HC.showLaws (genVectorKnownLength @1 genOrdering))+  , testCase "Show-Vector-laws-10" $+      assertBool "Show-Vector-laws-10" =<<+        HC.lawsCheck (HC.showLaws (genVectorKnownLength @10 genOrdering))+  , testCase "Foldable-Vector-laws-1" $+      assertBool "Foldable-Vector-laws-1" =<<+        HC.lawsCheck (HC.foldableLaws (genVectorKnownLength @1))+  , testCase "Foldable-Vector-laws-10" $+      assertBool "Foldable-Vector-laws-10" =<<+        HC.lawsCheck (HC.foldableLaws (genVectorKnownLength @10))+  , testCase "Traversable-Vector-laws-1" $+      assertBool "Traversable-Vector-laws-1" =<<+        HC.lawsCheck (HC.traversableLaws (genVectorKnownLength @1))+  , testCase "Traversable-Vector-laws-10" $+      assertBool "Traversable-Vector-laws-10" =<<+        HC.lawsCheck (HC.traversableLaws (genVectorKnownLength @10))+#endif+  ]

@@ -3,8 +3,11 @@ import Test.Tasty.Runners.AntXML  import qualified Test.Context+import qualified Test.Fin+import qualified Test.List import qualified Test.NatRepr import qualified Test.SymbolRepr+import qualified Test.TH import qualified Test.Vector  main :: IO ()@@ -20,7 +23,10 @@ tests :: IO TestTree tests = testGroup "ParameterizedUtils" <$> sequence   [ Test.Context.contextTests+  , pure Test.List.tests+  , Test.Fin.finTests   , Test.NatRepr.natTests   , Test.SymbolRepr.symbolTests+  , Test.TH.thTests   , Test.Vector.vecTests   ]