parameterized-utils 2.1.4.0 → 2.1.5.0

raw patch · 10 files changed

+41/−15 lines, 10 filesdep ~lensPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: lens

API changes (from Hackage documentation)

Files

• Changelog.md +9/−0
• LICENSE +1/−1
• parameterized-utils.cabal +4/−4
• src/Data/Parameterized/ClassesC.hs +1/−1
• src/Data/Parameterized/Context/Unsafe.hs +1/−0
• src/Data/Parameterized/NatRepr.hs +8/−3
• src/Data/Parameterized/NatRepr/Internal.hs +2/−2
• src/Data/Parameterized/TH/GADT.hs +10/−2
• src/Data/Parameterized/Vector.hs +4/−1
• test/Test/Vector.hs +1/−1

@@ -1,5 +1,14 @@ # Changelog for the `parameterized-utils` package +## 2.1.5.0 -- *2022 Mar 08*++  * Add support for GHC 9.2.  Drop support for GHC 8.4 (or earlier).+  * Add a `Data.Parameterized.NatRepr.leqZero :: LeqProof 0 n` function.+    Starting with GHC 9.2, GHC is no longer able to conclude that+    `forall (n :: Nat). 0 <= n` due to changes in how the `(<=)` type family+    works. As a result, this fact must be asserted as an axiom, which the+    `leqZero` function accomplishes.+ ## 2.1.4.0 -- *2021 Oct 1*    * Added the `ifoldLM` and `fromSomeList`, `fromListWith`, and

@@ -1,4 +1,4 @@-Copyright (c) 2013-2016 Galois Inc.+Copyright (c) 2013-2022 Galois Inc. All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -1,11 +1,11 @@ Cabal-version: 2.2 Name:          parameterized-utils-Version:       2.1.4.0+Version:       2.1.5.0 Author:        Galois Inc. Maintainer:    kquick@galois.com stability:     stable Build-type:    Simple-Copyright:     ©2016-2021 Galois, Inc.+Copyright:     ©2016-2022 Galois, Inc. License:       BSD-3-Clause License-file:  LICENSE category:      Data Structures, Dependent Types@@ -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.7, GHC==9.0.1+tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.1  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -59,7 +59,7 @@                , hashable       >=1.2  && <1.4                , hashtables     ==1.2.*                , indexed-traversable-               , lens           >=4.16 && <5.1+               , lens           >=4.16 && <5.2                , mtl                , profunctors    >=5.6 && < 5.7                , template-haskell

@@ -9,7 +9,7 @@ These classes generally require type-level evidence for operations on their subterms, but don't actually provide it themselves (because their types are not themselves parameterized, unlike those in-"Data.Parameterized.TraverableFC").+"Data.Parameterized.TraversableFC").  Note that there is still some ambiguity around naming conventions, see <https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.

@@ -1,5 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE GADTs #-}

@@ -87,6 +87,7 @@   , testStrictLeq   , leqRefl   , leqTrans+  , leqZero   , leqAdd2   , leqSub2   , leqMulCongr@@ -347,7 +348,7 @@  -- | @LeqProof m n@ is a type whose values are only inhabited when @m@ -- is less than or equal to @n@.-data LeqProof m n where+data LeqProof (m :: Nat) (n :: Nat) where   LeqProof :: (m <= n) => LeqProof m n  -- | (<=) is a decidable relation on nats.@@ -427,6 +428,10 @@ leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0) {-# NOINLINE leqTrans #-} +-- | Zero is less than or equal to any 'Nat'.+leqZero :: LeqProof 0 n+leqZero = unsafeCoerce (LeqProof :: LeqProof 0 0)+ -- | Add both sides of two inequalities leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h) leqAdd2 x y = seq x $ seq y $ unsafeCoerce (LeqProof :: LeqProof 0 0)@@ -476,14 +481,14 @@ -- | Produce proof that adding a value to the larger element in an LeqProof -- is larger leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p)-leqAdd x _ = leqAdd2 x (LeqProof :: LeqProof 0 p)+leqAdd x _ = leqAdd2 x (leqZero @p)  leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n) leqAddPos m n = leqAdd (leqProof (Proxy :: Proxy 1) m) n  -- | Produce proof that subtracting a value from the smaller element is smaller. leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n-leqSub x _ = leqSub2 x (LeqProof :: LeqProof 0 p)+leqSub x _ = leqSub2 x (leqZero @p)  addIsLeq :: f n -> g m -> LeqProof n (n + m) addIsLeq n m = leqAdd (leqRefl n) m

@@ -24,7 +24,7 @@ import Data.Data import Data.Hashable import GHC.TypeNats-import Numeric.Natural+import qualified Numeric.Natural as Natural import Unsafe.Coerce  import Data.Parameterized.Axiom@@ -38,7 +38,7 @@ -- -- This can be used for performing dynamic checks on a type-level natural -- numbers.-newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural+newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural.Natural                                      -- ^ The underlying natural value of the number.                                    }   deriving (Hashable, Data)

@@ -8,6 +8,7 @@ -- This module declares template Haskell primitives so that it is easier -- to work with GADTs that have many constructors. ------------------------------------------------------------------------+{-# LANGUAGE CPP #-} {-# LANGUAGE DoAndIfThenElse #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -66,7 +67,7 @@   Q (Pat, [Name]) {- ^ pattern and bound names -} conPat con pre = do   nms <- newNames pre (length (constructorFields con))-  return (ConP (constructorName con) (VarP <$> nms), nms)+  return (conPCompat (constructorName con) (VarP <$> nms), nms)   -- | Return an expression corresponding to the constructor.@@ -487,7 +488,7 @@ showCon :: ExpQ -> Name -> Int -> MatchQ showCon p nm n = do   vars <- newNames "x" n-  let pat = ConP nm (VarP <$> vars)+  let pat = conPCompat nm (VarP <$> vars)   let go s e = [| $(s) . showChar ' ' . showsPrec 11 $(varE e) |]   let ctor = [| showString $(return (LitE (StringL (nameBase nm)))) |]   let rhs | null vars = ctor@@ -694,6 +695,13 @@  mkReprName :: Name -> Name mkReprName nm = mkName (nameBase nm ++ "Repr")++conPCompat :: Name -> [Pat] -> Pat+conPCompat n pats = ConP n+#if MIN_VERSION_template_haskell(2,18,0)+                           []+#endif+                           pats  -- $typePatterns --

@@ -501,7 +501,10 @@         snd <$> getCompose3 (natRecBounded (decNat h) (decNat h) base step)       }   where base :: Compose3 m ((,) b) (Vector' a) 0-        base = Compose3 $ (\(hd, b) -> (b, MkVector' (singleton hd))) <$> gen (knownNat @0) start+        base =+          case leqZero @h of { LeqProof ->+          Compose3 $ (\(hd, b) -> (b, MkVector' (singleton hd))) <$> gen (knownNat @0) start+          }         step :: forall p. (1 <= h, p <= h - 1)              => NatRepr p              -> Compose3 m ((,) b) (Vector' a) p

@@ -29,7 +29,7 @@ import           Data.Parameterized.Some import           Data.Parameterized.Vector import           Data.Semigroup-import           GHC.TypeLits+import           GHC.TypeLits (KnownNat) import           Hedgehog import qualified Hedgehog.Gen as HG import           Hedgehog.Range