packages feed

parameterized-utils 2.1.0 → 2.1.1

raw patch · 7 files changed

+120/−7 lines, 7 filesdep ~constraintsdep ~tasty

Dependency ranges changed: constraints, tasty

Files

Changelog.md view
@@ -1,5 +1,11 @@ # Changelog for the `parameterized-utils` package +## 2.1.1 -- *2020 Jul 30*++  * Added `drop` and `appendEmbeddingLeft` functions to the `Context` module.+  * Fixes/updates to haddock documentation (fixing Issue #74).+  * Allow tasty v1.3 for testing (thanks to felixonmars)+ ## 2.1.0 -- *2020 May 08*    * Added `plusAssoc` to the `NatRepr` module to produce `+` associativity evidence.
parameterized-utils.cabal view
@@ -1,5 +1,5 @@ Name:          parameterized-utils-Version:       2.1.0+Version:       2.1.1 Author:        Galois Inc. Maintainer:    jhendrix@galois.com, kquick@galois.com stability:     stable@@ -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.3, GHC==8.10.1+tested-with:   GHC==8.6.5, GHC==8.8.3, GHC==8.10.1  -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag.  When this flag is set@@ -38,7 +38,7 @@   build-depends: base >= 4.10 && < 5                , base-orphans   >=0.8.2 && <0.9                , th-abstraction >=0.3  && <0.4-               , constraints    >=0.10 && <0.12+               , constraints    >=0.10 && <0.13                , containers                , deepseq                , ghc-prim@@ -116,7 +116,7 @@                , lens                , mtl                , parameterized-utils-               , tasty == 1.2.*+               , tasty >= 1.2 && < 1.4                , tasty-ant-xml == 1.1.*                , tasty-hunit >= 0.9 && < 0.11                , tasty-hedgehog
src/Data/Parameterized/Context.hs view
@@ -56,6 +56,7 @@   , Data.Parameterized.Context.last   , Data.Parameterized.Context.view   , Data.Parameterized.Context.take+  , Data.Parameterized.Context.drop   , forIndexM   , generateSome   , generateSomeM@@ -75,6 +76,7 @@   , extendEmbeddingRight   , extendEmbeddingBoth   , appendEmbedding+  , appendEmbeddingLeft   , ctxeSize   , ctxeAssignment @@ -238,11 +240,16 @@ view :: forall f ctx . Assignment f ctx -> AssignView f ctx view = viewAssign +-- | Return the prefix of an appended 'Assignment' take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx take sz sz' asgn =   let diff = appendDiff sz' in   generate sz (\i -> asgn ! extendIndex' diff i) +-- | Return the suffix of an appended 'Assignment'+drop :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'+drop sz sz' asgn = generate sz' (\i -> asgn ! extendIndexAppendLeft sz sz' i)+ -------------------------------------------------------------------------------- -- Context embedding. @@ -310,10 +317,15 @@ extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) extendEmbeddingRight = extendEmbeddingRightDiff knownDiff +-- | Prove that the prefix of an appended context is embeddable in it appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx') appendEmbedding sz sz' = CtxEmbedding (addSize sz sz') (generate sz (extendIndex' diff))   where   diff = appendDiff sz'++-- | Prove that the suffix of an appended context is embeddable in it+appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')+appendEmbeddingLeft sz sz' = CtxEmbedding (addSize sz sz') (generate sz' (extendIndexAppendLeft sz sz'))  extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))
src/Data/Parameterized/Context/Safe.hs view
@@ -77,6 +77,7 @@   , nextIndex   , extendIndex   , extendIndex'+  , extendIndexAppendLeft   , forIndex   , forIndexRange   , intIndex@@ -308,9 +309,19 @@ extendIndex = extendIndex' knownDiff  {-# INLINE extendIndex' #-}+-- | Compute an 'Index' into a context @r@ from an 'Index' into+-- a sub-context @l@ of @r@. extendIndex' :: Diff l r -> Index l tp -> Index r tp extendIndex' DiffHere idx = idx extendIndex' (DiffThere diff) idx = IndexThere (extendIndex' diff idx)++{-# INLINE extendIndexAppendLeft #-}+-- | Compute an 'Index' into an appended context from an 'Index' into+-- its suffix.+extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp+extendIndexAppendLeft sz sz' idx = case viewIndex sz' idx of+  IndexViewLast _ -> lastIndex (addSize sz sz')+  IndexViewInit idx' -> skipIndex (extendIndexAppendLeft sz (decSize sz') idx')  -- | Given a size @n@, an initial value @v0@, and a function @f@, the -- expression @forIndex n v0 f@ calls @f@ on each index less than @n@
src/Data/Parameterized/Context/Unsafe.hs view
@@ -49,6 +49,7 @@   , nextIndex   , extendIndex   , extendIndex'+  , extendIndexAppendLeft   , forIndex   , forIndexRange   , intIndex@@ -268,8 +269,16 @@ extendIndex = extendIndex' knownDiff  {-# INLINE extendIndex' #-}+-- | Compute an 'Index' into a context @r@ from an 'Index' into+-- a sub-context @l@ of @r@. extendIndex' :: Diff l r -> Index l tp -> Index r tp extendIndex' _ = unsafeCoerce++{-# INLINE extendIndexAppendLeft #-}+-- | Compute an 'Index' into an appended context from an 'Index' into+-- its suffix.+extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp+extendIndexAppendLeft (Size l) _ (Index idx) = Index (idx + l)  -- | Given a size @n@, an initial value @v0@, and a function @f@, the -- expression @forIndex n v0 f@ is equivalent to @v0@ when @n@ is
src/Data/Parameterized/NatRepr.hs view
@@ -387,7 +387,7 @@     GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0)) {-# NOINLINE testNatCases #-} --- | The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.+-- | The strict order (\<), defined by n \< m \<-> n + 1 \<= m, is irreflexive. lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void lessThanIrreflexive a prf =   let prf1 :: LeqProof (1 + a - a) (a - a)@@ -400,7 +400,7 @@       prf4 = case prf2 of Refl -> case prf3 of { Refl -> prf1 }   in case prf4 of {} --- | The strict order on the naturals is irreflexive.+-- | The strict order on the naturals is asymmetric lessThanAsymmetric :: forall m f n                     . LeqProof (n+1) m                    -> LeqProof (m+1) n
test/Test/Context.hs view
@@ -11,6 +11,7 @@ import           Control.Lens import           Data.Parameterized.Classes import qualified Data.Parameterized.Context as C+import qualified Data.Parameterized.Ctx.Proofs as P import qualified Data.Parameterized.Context.Safe as S import qualified Data.Parameterized.Context.Unsafe as U import           Data.Parameterized.Some@@ -172,6 +173,48 @@           Just Refl -> vals1 === vals2           Nothing   -> vals1 /== vals2 +   , testProperty "take none" $ property $+     do vals1 <- forAll genSomePayloadList+        vals2 <- forAll genSomePayloadList+        vals3 <- forAll genSomePayloadList+        Some w <- return $ mkUAsgn vals1+        Some x <- return $ mkUAsgn vals2+        Some y <- return $ mkUAsgn vals3+        let z = w U.<++> x U.<++> y+        case P.leftId z of+          Refl -> let r = C.take U.zeroSize (U.size z) z in+                    assert $ isJust $ testEquality U.empty r+   , testProperty "drop none" $ property $+     do vals1 <- forAll genSomePayloadList+        vals2 <- forAll genSomePayloadList+        vals3 <- forAll genSomePayloadList+        Some w <- return $ mkUAsgn vals1+        Some x <- return $ mkUAsgn vals2+        Some y <- return $ mkUAsgn vals3+        let z = w U.<++> x U.<++> y+        case P.leftId z of+          Refl -> let r = C.drop U.zeroSize (U.size z) z in+                    assert $ isJust $ testEquality z r+   , testProperty "take all" $ property $+     do vals1 <- forAll genSomePayloadList+        vals2 <- forAll genSomePayloadList+        vals3 <- forAll genSomePayloadList+        Some w <- return $ mkUAsgn vals1+        Some x <- return $ mkUAsgn vals2+        Some y <- return $ mkUAsgn vals3+        let z = w U.<++> x U.<++> y+        let r = C.take (U.size z) U.zeroSize z+        assert $ isJust $ testEquality z r+   , testProperty "drop all" $ property $+     do vals1 <- forAll genSomePayloadList+        vals2 <- forAll genSomePayloadList+        vals3 <- forAll genSomePayloadList+        Some w <- return $ mkUAsgn vals1+        Some x <- return $ mkUAsgn vals2+        Some y <- return $ mkUAsgn vals3+        let z = w U.<++> x U.<++> y+        let r = C.drop (U.size z) U.zeroSize z+        assert $ isJust $ testEquality U.empty r    , testProperty "append_take" $ property $      do vals1 <- forAll genSomePayloadList         vals2 <- forAll genSomePayloadList@@ -180,5 +223,37 @@         let z = x U.<++> y         let x' = C.take (U.size x) (U.size y) z         assert $ isJust $ testEquality x x'-+   , testProperty "append_take_drop" $ property $+     do vals1 <- forAll genSomePayloadList+        vals2 <- forAll genSomePayloadList+        Some x <- return $ mkUAsgn vals1+        Some y <- return $ mkUAsgn vals2+        let z = x U.<++> y+        let x' = C.take (U.size x) (U.size y) z+        let y' = C.drop (U.size x) (U.size y) z+        assert $ isJust $ testEquality x x'+        assert $ isJust $ testEquality y y'+   , testProperty "append_take_drop_multiple" $ property $+     do vals1 <- forAll genSomePayloadList+        vals2 <- forAll genSomePayloadList+        vals3 <- forAll genSomePayloadList+        vals4 <- forAll genSomePayloadList+        vals5 <- forAll genSomePayloadList+        Some u <- return $ mkUAsgn vals1+        Some v <- return $ mkUAsgn vals2+        Some w <- return $ mkUAsgn vals3+        Some x <- return $ mkUAsgn vals4+        Some y <- return $ mkUAsgn vals5+        let uv = u U.<++> v+        let wxy = w U.<++> x U.<++> y+        -- let z = u C.<++> v C.<++> w C.<++> x C.<++> y+        let z = uv U.<++> wxy+        let uv' = C.take (U.size uv) (U.size wxy) z+        let wxy' = C.drop (U.size uv) (U.size wxy) z+        let withWXY = C.dropPrefix z uv (error "failed dropPrefix")+        assert $ isJust $ testEquality (u U.<++> v) uv'+        assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'+        assert $ isJust $ testEquality uv uv'+        assert $ isJust $ testEquality wxy wxy'+        withWXY $ \t -> assert $ isJust $ testEquality wxy' t    ]