packages feed

parameterized-utils 2.1.9.0 → 2.1.10.0

raw patch · 15 files changed

+128/−5 lines, 15 filesdep ~basenew-uploader

Dependency ranges changed: base

Files

Changelog.md view
@@ -1,5 +1,17 @@ # Changelog for the `parameterized-utils` package +## 2.1.10.0 -- *2025 Mar 20*++  * New instances for types from `base`:++    - `{Functor,Foldable,Traversable}F` instances for `Product`, `Proxy`, `Sum`+    - `{Functor,Foldable,Traversable}FC` instances for `Alt`, `Ap`++  * `{Functor,Foldable,Traversable}FC` instances for `TypeAp`++  * `EqF` instances for `Assignment`, `BoolRepr`, `Index`, `List`, `NatRepr`,+    `Nonce`, `PairRepr`, `PeanoRepr`, and `SymbolRepr`+ ## 2.1.9.0 -- *2024 Sep 19*    * Add support for GHC 9.10.
parameterized-utils.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          parameterized-utils-Version:       2.1.9.0+Version:       2.1.10.0 Author:        Galois Inc. Maintainer:    kquick@galois.com, rscott@galois.com stability:     stable@@ -16,7 +16,7 @@   intended for things like expression libraries where one wishes   to leverage the Haskell type-checker to improve type-safety by encoding   the object language type system into data kinds.-extra-source-files: Changelog.md+extra-doc-files: Changelog.md homepage:      https://github.com/GaloisInc/parameterized-utils bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.5, GHC==9.6.1, GHC==9.8.1, GHC==9.10.1@@ -50,7 +50,7 @@  library   import: bldflags-  build-depends: base >= 4.10 && < 5+  build-depends: base >= 4.12 && < 5                , base-orphans   >=0.8.2 && <0.10                , th-abstraction >=0.4.2 && <0.8                , constraints    >=0.10 && <0.15@@ -58,7 +58,7 @@                , deepseq                , ghc-prim                , hashable       >=1.2  && <1.6-               , hashtables     >=1.2  && <1.4+               , hashtables     >=1.2  && <1.5                , indexed-traversable                , lens           >=4.16 && <5.4                , mtl
src/Data/Parameterized/BoolRepr.hs view
@@ -74,6 +74,9 @@ instance Eq (BoolRepr m) where   _ == _ = True +instance EqF BoolRepr where+  eqF _ _ = True+ instance TestEquality BoolRepr where   testEquality TrueRepr TrueRepr   = Just Refl   testEquality FalseRepr FalseRepr = Just Refl
src/Data/Parameterized/ClassesC.hs view
@@ -20,6 +20,9 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeOperators #-} +-- See https://github.com/GaloisInc/parameterized-utils/issues/149+{-# OPTIONS_GHC -Wno-trustworthy-safe #-}+ module Data.Parameterized.ClassesC   ( TestEqualityC(..)   , OrdC(..)
src/Data/Parameterized/Context/Safe.hs view
@@ -282,6 +282,9 @@ instance Eq (Index ctx tp) where   idx1 == idx2 = isJust (testEquality idx1 idx2) +instance EqF (Index ctx) where+  eqF idx1 idx2 = isJust (testEquality idx1 idx2)+ instance TestEquality (Index ctx) where   testEquality (IndexHere _) (IndexHere _) = Just Refl   testEquality (IndexHere _) (IndexThere _) = Nothing@@ -546,6 +549,11 @@  instance TestEquality f => Eq (Assignment f ctx) where   x == y = isJust (testEquality x y)++instance EqF f => EqF (Assignment f) where+  eqF AssignmentEmpty AssignmentEmpty = True+  eqF (AssignmentExtend ctx1 x1) (AssignmentExtend ctx2 x2) =+    eqF ctx1 ctx2 && eqF x1 x2  testEq :: (forall x y. f x -> f y -> Maybe (x :~: y))        -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
src/Data/Parameterized/Context/Unsafe.hs view
@@ -247,6 +247,9 @@ instance Eq (Index ctx tp) where   Index i == Index j = i == j +instance EqF (Index ctx) where+  eqF (Index i) (Index j) = i == j+ instance TestEquality (Index ctx) where   testEquality (Index i) (Index j)     | i == j = Just unsafeAxiom@@ -829,6 +832,14 @@    testEqualityFC test (Assignment x) (Assignment y) = do      Refl <- testEqualityFC test x y      return Refl++instance EqF f => EqF (Assignment f) where+  eqF x y =+    case (viewAssign x, viewAssign y) of+      (AssignEmpty, AssignEmpty) ->+        True+      (AssignExtend ctx1 x1, AssignExtend ctx2 x2) ->+        eqF ctx1 ctx2 && eqF x1 x2  instance TestEquality f => TestEquality (Assignment f) where   testEquality = testEqualityFC testEquality
src/Data/Parameterized/DataKind.hs view
@@ -37,6 +37,9 @@ instance ( ShowF f, ShowF g ) => ShowF (PairRepr f g)  deriving instance ( Eq (f a), Eq (g b) ) => Eq (PairRepr f g '(a, b))+instance ( EqF f, EqF g ) => EqF (PairRepr f g) where+  eqF (PairRepr a1 b1) (PairRepr a2 b2) =+    eqF a1 a2 && eqF b1 b2 instance ( TestEquality f, TestEquality g ) => TestEquality (PairRepr f g) where   testEquality =     $(TH.structuralTypeEquality [t|PairRepr|]
src/Data/Parameterized/List.hs view
@@ -214,6 +214,12 @@     pure Refl   testEquality _ _ = Nothing +instance EqF f => EqF (List f) where+  eqF Nil Nil =+    True+  eqF (xh :< xl) (yh :< yl) =+    eqF xh yh && eqF xl yl+ instance OrdF f => OrdF (List f) where   compareF Nil Nil = EQF   compareF Nil _ = LTF
src/Data/Parameterized/NatRepr/Internal.hs view
@@ -48,6 +48,9 @@ instance Eq (NatRepr m) where   _ == _ = True +instance EqF NatRepr where+  eqF _ _ = True+ instance TestEquality NatRepr where   testEquality (NatRepr m) (NatRepr n)     | m == n = Just unsafeAxiom
src/Data/Parameterized/Nonce.hs view
@@ -131,6 +131,9 @@ --  the nonce abstraction. type role Nonce nominal nominal +instance EqF (Nonce s) where+  eqF x y = isJust (testEquality x y)+ instance TestEquality (Nonce s) where   testEquality x y | indexValue x == indexValue y = Just unsafeAxiom                    | otherwise = Nothing
src/Data/Parameterized/Nonce/Unsafe.hs view
@@ -64,6 +64,9 @@ --  the nonce abstraction. type role Nonce nominal +instance EqF Nonce where+  eqF x y = isJust (testEquality x y)+ instance TestEquality Nonce where   testEquality x y | indexValue x == indexValue y = Just unsafeAxiom                    | otherwise = Nothing
src/Data/Parameterized/Peano.hs view
@@ -219,6 +219,9 @@ instance Eq (PeanoRepr m) where   _ == _ = True +instance EqF PeanoRepr where+  eqF _ _ = True+ instance TestEquality PeanoRepr where #ifdef UNSAFE_OPS   testEquality (PeanoRepr m) (PeanoRepr n)
src/Data/Parameterized/SymbolRepr.hs view
@@ -95,6 +95,8 @@ -- symbol instance Eq (SymbolRepr x) where    _ == _ = True+instance EqF SymbolRepr where+   eqF _ _ = True instance Ord (SymbolRepr x) where    compare _ _ = EQ
src/Data/Parameterized/TraversableF.hs view
@@ -35,8 +35,11 @@ import Control.Monad.Identity import Data.Coerce import Data.Functor.Compose (Compose(..))+import Data.Functor.Product (Product(Pair))+import Data.Functor.Sum (Sum(InL, InR)) import Data.Kind-import Data.Monoid+import Data.Monoid hiding (Product, Sum)+import Data.Proxy (Proxy(Proxy)) import GHC.Exts (build)  import Data.Parameterized.TraversableFC@@ -48,6 +51,17 @@ instance FunctorF (Const x) where   fmapF _ = coerce +instance (FunctorF f, FunctorF g) => FunctorF (Product f g) where+  fmapF f (Pair x y) = Pair (fmapF f x) (fmapF f y)++instance FunctorF Proxy where+  fmapF _ = coerce+  {-# INLINE fmapF #-}++instance (FunctorF f, FunctorF g) => FunctorF (Sum f g) where+  fmapF f (InL x) = InL (fmapF f x)+  fmapF f (InR x) = InR (fmapF f x)+ ------------------------------------------------------------------------ -- FoldableF @@ -125,6 +139,17 @@ instance FoldableF (Const x) where   foldMapF _ _ = mempty +instance (FoldableF f, FoldableF g) => FoldableF (Product f g) where+  foldMapF f (Pair x y) = foldMapF f x <> foldMapF f y++instance FoldableF Proxy where+  foldMapF _ _ = mempty+  {-# INLINE foldMapF #-}++instance (FoldableF f, FoldableF g) => FoldableF (Sum f g) where+  foldMapF f (InL x) = foldMapF f x+  foldMapF f (InR y) = foldMapF f y+ ------------------------------------------------------------------------ -- TraversableF @@ -136,6 +161,17 @@  instance TraversableF (Const x) where   traverseF _ (Const x) = pure (Const x)++instance (TraversableF f, TraversableF g) => TraversableF (Product f g) where+  traverseF f (Pair x y) = Pair <$> traverseF f x <*> traverseF f y++instance TraversableF Proxy where+  traverseF _ _ = pure Proxy+  {-# INLINE traverseF #-}++instance (TraversableF f, TraversableF g) => TraversableF (Sum f g) where+  traverseF f (InL x) = InL <$> traverseF f x+  traverseF f (InR y) = InR <$> traverseF f y  -- | Flipped 'traverseF' forF :: (TraversableF t, Applicative m) => t e -> (forall s . e s -> m (f s)) -> m (t f)
src/Data/Parameterized/TraversableFC.hs view
@@ -55,6 +55,15 @@   fmapFC :: forall f g. (forall x. f x -> g x) ->                         (forall x. t f x -> t g x) +instance FunctorFC Alt where+  fmapFC f (Alt a) = Alt (f a)++instance FunctorFC Ap where+  fmapFC f (Ap a) = Ap (f a)++instance FunctorFC TypeAp where+  fmapFC f (TypeAp a) = TypeAp (f a)+ -- | A parameterized class for types which can be shown, when given --   functions to show parameterized subterms. class ShowFC (t :: (k -> Type) -> l -> Type) where@@ -161,6 +170,15 @@ lengthFC :: FoldableFC t => t f x -> Int lengthFC = foldrFC (const (+1)) 0 +instance FoldableFC Alt where+  foldMapFC toMonoid (Alt x) = toMonoid x++instance FoldableFC Ap where+  foldMapFC toMonoid (Ap x) = toMonoid x++instance FoldableFC TypeAp where+  foldMapFC toMonoid (TypeAp x) = toMonoid x+ ------------------------------------------------------------------------ -- TraversableF @@ -206,3 +224,12 @@   t f x -> (forall y. f y -> m (g y)) -> m (t g x) forFC v f = traverseFC f v {-# INLINE forFC #-}++instance TraversableFC Alt where+  traverseFC f (Alt x) = Alt <$> f x++instance TraversableFC Ap where+  traverseFC f (Ap x) = Ap <$> f x++instance TraversableFC TypeAp where+  traverseFC f (TypeAp x) = TypeAp <$> f x