parameterized-utils 2.1.11.0 → 2.2.0.0
raw patch · 12 files changed
+52/−38 lines, 12 filesdep +microlensdep +microlens-prodep −lens
Dependencies added: microlens, microlens-pro
Dependencies removed: lens
Files
- Changelog.md +6/−0
- parameterized-utils.cabal +4/−3
- src/Data/Parameterized/Classes.hs +1/−6
- src/Data/Parameterized/Context.hs +3/−2
- src/Data/Parameterized/Context/Safe.hs +9/−9
- src/Data/Parameterized/Context/Unsafe.hs +2/−2
- src/Data/Parameterized/Fin.hs +18/−10
- src/Data/Parameterized/List.hs +1/−1
- src/Data/Parameterized/Map.hs +1/−1
- src/Data/Parameterized/Some.hs +2/−2
- test/Test/Context.hs +3/−1
- test/Test/Some.hs +2/−1
Changelog.md view
@@ -1,5 +1,11 @@ # Changelog for the `parameterized-utils` package +## 2.2.0.0 -- 2026-01-22++ * Replace dependency on `lens` with `microlens` and `microlens-pro`.+ * Deprecate the `Iso`s `fin0Void`, `fin1Unit`, and `fin2Bool`.+ * Add `fin0Absurd :: Fin 0 -> a`.+ ## 2.1.11.0 -- *2025 Nov 4* * Add support for GHC 9.12.
parameterized-utils.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: parameterized-utils-Version: 2.1.11.0+Version: 2.2.0.0 Author: Galois Inc. Maintainer: kquick@galois.com, rscott@galois.com stability: stable@@ -59,7 +59,8 @@ , hashable >=1.2 && <1.6 , hashtables >=1.2 && <1.5 , indexed-traversable- , lens >=4.16 && <5.4+ , microlens >=0.5 && <0.6+ , microlens-pro >=0.2 && <0.3 , mtl , profunctors >=5.6 && < 5.7 , template-haskell@@ -136,7 +137,7 @@ , hashtables , hedgehog , indexed-traversable- , lens+ , microlens >=0.5 && <0.6 , mtl , parameterized-utils , tasty >= 1.2 && < 1.6
src/Data/Parameterized/Classes.hs view
@@ -65,14 +65,9 @@ import Data.Maybe (isJust) import Data.Proxy import Data.Type.Equality as Equality+import Lens.Micro (Lens', Traversal') import Data.Parameterized.Compose ()---- We define these type alias here to avoid importing Control.Lens--- modules, as this apparently causes problems with the safe Hasekll--- checking.-type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s-type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s ------------------------------------------------------------------------ -- CoercibleF
src/Data/Parameterized/Context.hs view
@@ -103,13 +103,14 @@ import Prelude hiding (unzip) import qualified Control.Applicative as App (liftA2)-import Control.Lens hiding (Index, (:>), Empty)+import Data.Function ((&)) import Data.Functor (void) import Data.Functor.Product (Product(Pair)) import Data.Kind import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import GHC.TypeLits (Nat, type (-))+import Lens.Micro (Lens', Lens, lens, (^.), (%~)) import Data.Parameterized.Classes import Data.Parameterized.Some@@ -301,7 +302,7 @@ -- ExtendBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) -- ExtendOne :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) -ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')+ctxeSize :: Lens' (CtxEmbedding ctx ctx') (Size ctx') ctxeSize = lens _ctxeSize (\s v -> s { _ctxeSize = v }) ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx')
src/Data/Parameterized/Context/Safe.hs view
@@ -110,15 +110,15 @@ ) where import qualified Control.Category as Cat-import Control.DeepSeq-import qualified Control.Lens as Lens-import Control.Monad.Identity (Identity(..))-import Data.Hashable-import Data.List (intercalate)-import Data.Maybe (listToMaybe)-import Data.Type.Equality-import Prelude hiding (init, map, null, replicate, succ, zipWith)-import Data.Kind(Type)+import Control.DeepSeq+import Control.Monad.Identity (Identity(..))+import Data.Hashable+import Data.Kind (Type)+import Data.List (intercalate)+import Data.Maybe (listToMaybe)+import Data.Type.Equality+import qualified Lens.Micro as Lens+import Prelude hiding (init, map, null, replicate, succ, zipWith) import Data.Parameterized.Classes import Data.Parameterized.Ctx
src/Data/Parameterized/Context/Unsafe.hs view
@@ -90,15 +90,15 @@ import qualified Control.Category as Cat import Control.DeepSeq import Control.Exception-import qualified Control.Lens as Lens import Control.Monad.Identity (Identity(..)) import Data.Bits import Data.Coerce import Data.Hashable+import Data.Kind (Type) import Data.List (intercalate) import Data.Proxy+import qualified Lens.Micro as Lens import Unsafe.Coerce-import Data.Kind(Type) import Data.Parameterized.Axiom import Data.Parameterized.Classes
src/Data/Parameterized/Fin.hs view
@@ -31,15 +31,16 @@ , tryEmbed , minFin , incFin+ , fin0Absurd , fin0Void , fin1Unit , fin2Bool ) where -import Control.Lens.Iso (Iso', iso)+import Data.Void (Void, absurd) import GHC.TypeNats (KnownNat)+import Lens.Micro.Pro (Iso', iso) import Numeric.Natural (Natural)-import Data.Void (Void, absurd) import Data.Parameterized.NatRepr @@ -124,15 +125,17 @@ case leqAdd2 (LeqProof :: LeqProof (i + 1) n) (LeqProof :: LeqProof 1 1) of LeqProof -> mkFin (incNat i) +-- | It is not possible to construct an element of @'Fin' 0@.+fin0Absurd :: Fin 0 -> a+fin0Absurd =+ viewFin+ (\(x :: NatRepr o) ->+ case plusComm x (knownNat @1) of+ Refl ->+ case addIsLeqLeft1 @1 @o @0 LeqProof of {})+ 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+fin0Void = iso fin0Absurd absurd fin1Unit :: Iso' (Fin 1) () fin1Unit = iso (const ()) (const minFin)@@ -146,3 +149,8 @@ ZeroNat -> False NonZeroNat -> True)) (\b -> if b then maxBound else minBound)++{-# DEPRECATED+ fin0Void, fin1Unit, fin2Bool+ "These will be removed in the next release of parameterized-utils, see #208."+#-}
src/Data/Parameterized/List.hs view
@@ -153,7 +153,7 @@ , index3 ) where -import qualified Control.Lens as Lens+import qualified Lens.Micro as Lens import Data.Foldable import Data.Kind import Prelude hiding ((!!))
src/Data/Parameterized/Map.hs view
@@ -82,13 +82,13 @@ ) where import Control.Applicative hiding (empty)-import Control.Lens (Traversal', Lens') import Control.Monad.Identity (Identity(..)) import Control.Monad (foldM) import Data.Kind (Type) import qualified Data.List as List import Data.Monoid import Prelude hiding (filter, lookup, map, traverse, null)+import Lens.Micro (Traversal', Lens') import Data.Parameterized.Classes import Data.Parameterized.Some
src/Data/Parameterized/Some.hs view
@@ -20,11 +20,11 @@ , someLens ) where -import Control.Lens (Lens', lens, (&), (^.), (.~)) import Data.Hashable-import Data.Kind+import Data.Kind (Type) import Data.Parameterized.Classes import Data.Parameterized.TraversableF+import Lens.Micro (Lens', lens, (&), (^.), (.~)) data Some (f:: k -> Type) = forall x . Some (f x)
test/Test/Context.hs view
@@ -18,7 +18,8 @@ ) where -import Control.Lens+import Data.Function ((&))+import Data.Functor.Identity (Identity(..)) import Data.Functor.Product (Product(Pair)) import Data.Kind import Data.Parameterized.Classes@@ -33,6 +34,7 @@ import Hedgehog import qualified Hedgehog.Gen as HG import Hedgehog.Range+import Lens.Micro ((%~), (.~), over) import Test.Tasty import Test.Tasty.HUnit ( (@=?), (@?=), testCaseSteps ) import Test.Tasty.Hedgehog
test/Test/Some.hs view
@@ -7,7 +7,8 @@ where import Data.Type.Equality (TestEquality(testEquality), (:~:)(Refl))-import Control.Lens (Lens', lens, view, set)+import Lens.Micro (Lens', lens, set)+import Lens.Micro.Extras (view) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertEqual, testCase)