containers-verified (empty) → 0.5.11.0
raw patch · 7 files changed
+470/−0 lines, 7 filesdep +containerssetup-changed
Dependencies added: containers
Files
- ChangeLog.md +5/−0
- Data/IntSet.hs +90/−0
- Data/Map.hs +188/−0
- Data/Set.hs +101/−0
- LICENSE +20/−0
- Setup.hs +2/−0
- containers-verified.cabal +64/−0
+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for containers-verified++## 0.5.11.0 -- 2018-03-15++* First version.
+ Data/IntSet.hs view
@@ -0,0 +1,90 @@+{-# OPTIONS_HADDOCK not-home #-}+{-# LANGUAGE PackageImports #-}+{-# LANGUAGE NoImplicitPrelude #-}++-- | Please see the documentation of <http://hackage.haskell.org/package/containers containers> for details.+module Data.IntSet (+-- -- * Strictness properties+-- -- $strictness++ -- * Set type+ IntSet -- instance Eq,Show+ , Key++ -- * Operators+ , (\\)++ -- * Query+ , IS.null+ , size+ , member+ , notMember+-- , lookupLT+-- , lookupGT+-- , lookupLE+-- , lookupGE+ , isSubsetOf+ , isProperSubsetOf+ , disjoint++ -- * Construction+ , empty+ , singleton+ , insert+ , delete++ -- * Combine+ , union+-- , unions+ , difference+ , intersection++ -- * Filter+ , IS.filter+ , partition+ , split+ , splitMember+-- , splitRoot++ -- * Map+-- , IS.map++ -- * Folds+ , IS.foldr+ , IS.foldl+ -- ** Strict folds+ , foldr'+ , foldl'+ -- ** Legacy folds+ , fold++-- -- * Min\/Max+-- , findMin+-- , findMax+-- , deleteMin+-- , deleteMax+-- , deleteFindMin+-- , deleteFindMax+-- , maxView+-- , minView++ -- * Conversion++ -- ** List+ , elems+ , toList+ , fromList++ -- ** Ordered list+ , toAscList+ , toDescList+-- , fromAscList+-- , fromDistinctAscList++-- -- * Debugging+-- , showTree+-- , showTreeWith++ ) where++import "containers" Data.IntSet as IS
+ Data/Map.hs view
@@ -0,0 +1,188 @@+{-# OPTIONS_HADDOCK not-home #-}+{-# LANGUAGE PackageImports #-}+{-# LANGUAGE NoImplicitPrelude #-}++-- | Please see the documentation of <http://hackage.haskell.org/package/containers containers> for details.+module Data.Map+ (+ -- * Map type+ Map -- instance Eq,Show,Read++ -- * Construction+ , empty+ , singleton+ , fromSet++-- -- ** From Unordered Lists+-- , fromList+-- , fromListWith+-- , fromListWithKey++-- -- ** From Ascending Lists+-- , fromAscList+-- , fromAscListWith+-- , fromAscListWithKey+-- , fromDistinctAscList++-- -- ** From Descending Lists+-- , fromDescList+-- , fromDescListWith+-- , fromDescListWithKey+-- , fromDistinctDescList++ -- * Insertion+ , insert+-- , insertWith+-- , insertWithKey+-- , insertLookupWithKey++ -- * Deletion\/Update+ , delete+-- , adjust+-- , adjustWithKey+-- , update+-- , updateWithKey+-- , updateLookupWithKey+-- , alter+-- , alterF++ -- * Query+ -- ** Lookup+ , lookup+-- , (!?)+-- , (!)+-- , findWithDefault+ , member+-- , notMember+-- , lookupLT+-- , lookupGT+-- , lookupLE+-- , lookupGE++ -- ** Size+ , null+-- , size++ -- * Combine++ -- ** Union+ , union+-- , unionWith+-- , unionWithKey+-- , unions+-- , unionsWith++ -- ** Difference+ , difference+-- , (\\)+-- , differenceWith+-- , differenceWithKey++ -- ** Intersection+ , intersection+-- , intersectionWith+-- , intersectionWithKey++-- -- ** Unsafe general combining function+--+-- , mergeWithKey++-- -- * Traversal+-- -- ** Map+-- , map+-- , mapWithKey+-- , traverseWithKey+-- , traverseMaybeWithKey+-- , mapAccum+-- , mapAccumWithKey+-- , mapAccumRWithKey+-- , mapKeys+-- , mapKeysWith+-- , mapKeysMonotonic++-- -- * Folds+-- , foldr+-- , foldl+-- , foldrWithKey+-- , foldlWithKey+-- , foldMapWithKey++-- -- ** Strict folds+-- , foldr'+-- , foldl'+-- , foldrWithKey'+-- , foldlWithKey'++-- -- * Conversion+-- , elems+-- , keys+-- , assocs+-- , keysSet++ -- ** Lists+-- , toList++ -- ** Ordered lists+-- , toAscList+-- , toDescList++-- -- * Filter+-- , filter+-- , filterWithKey+-- , restrictKeys+-- , withoutKeys+-- , partition+-- , partitionWithKey+-- , takeWhileAntitone+-- , dropWhileAntitone+-- , spanAntitone++-- , mapMaybe+-- , mapMaybeWithKey+-- , mapEither+-- , mapEitherWithKey++ , split+-- , splitLookup+-- , splitRoot++-- -- * Submap+-- , isSubmapOf, isSubmapOfBy+-- , isProperSubmapOf, isProperSubmapOfBy++-- -- * Indexed+-- , lookupIndex+-- , findIndex+-- , elemAt+-- , updateAt+-- , deleteAt+-- , take+-- , drop+-- , splitAt++-- -- * Min\/Max+-- , lookupMin+-- , lookupMax+-- , findMin+-- , findMax+-- , deleteMin+-- , deleteMax+-- , deleteFindMin+-- , deleteFindMax+-- , updateMin+-- , updateMax+-- , updateMinWithKey+-- , updateMaxWithKey+-- , minView+-- , maxView+-- , minViewWithKey+-- , maxViewWithKey++-- , insertWith'+-- , insertWithKey'+-- , insertLookupWithKey'+-- , fold+-- , foldWithKey+ ) where++import "containers" Data.Map
+ Data/Set.hs view
@@ -0,0 +1,101 @@+{-# OPTIONS_HADDOCK not-home #-}+{-# LANGUAGE PackageImports #-}+{-# LANGUAGE NoImplicitPrelude #-}++-- | Please see the documentation of <http://hackage.haskell.org/package/containers containers> for details.+module Data.Set (+ -- * Set type+ Set -- instance Eq,Ord,Show,Read,Data,Typeable++ -- * Operators+-- , (\\)++ -- * Query+ , S.null+ , size+ , member+ , notMember+-- , lookupLT+-- , lookupGT+-- , lookupLE+-- , lookupGE+ , isSubsetOf+-- , isProperSubsetOf+ , disjoint++ -- * Construction+ , empty+ , singleton+ , insert+ , delete+-- , powerSet++ -- * Combine+ , union+ , unions+ , difference+ , intersection+-- , cartesianProduct+-- , disjointUnion++ -- * Filter+ , S.filter+-- , takeWhileAntitone+-- , dropWhileAntitone+-- , spanAntitone+ , partition+ , split+ , splitMember+-- , splitRoot++-- -- * Indexed+-- , lookupIndex+-- , findIndex+-- , elemAt+-- , deleteAt+ , S.take+ , S.drop+ , S.splitAt++-- -- * Map+-- , S.map+ , mapMonotonic++ -- * Folds+ , S.foldr+ , S.foldl+-- -- ** Strict folds+-- , foldr'+-- , foldl'+-- -- ** Legacy folds+-- , fold++-- -- * Min\/Max+ , lookupMin+ , lookupMax+-- , findMin+-- , findMax+-- , deleteMin+-- , deleteMax+-- , deleteFindMin+-- , deleteFindMax+ , maxView+ , minView++-- -- * Conversion++-- -- ** List+ , elems+ , toList+-- , fromList++-- -- ** Ordered list+ , toAscList+ , toDescList+ , fromAscList+ , fromDescList+ , fromDistinctAscList+ , fromDistinctDescList+ ) where++import Data.Set.Internal as S
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2018 Joachim Breitner++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ containers-verified.cabal view
@@ -0,0 +1,64 @@+name: containers-verified+version: 0.5.11.0+synopsis: Formally verified drop-in replacement of containers+description:+ In the context of the <https://deepspec.org/main DeepSpec project>, parts of the+ <http://hackage.haskell.org/package/containers containers> library were+ formally verified using <https://github.com/antalsz/hs-to-coq hs-to-coq> and+ the interactive theorem prover Coq.+ .+ This package depends on precisely the verified version of containers and+ re-exports the verified parts of the API, with module name and function name+ unchanged.+ .+ If you happen to use only the verified subset of the API, then you can simply change+ @containers@ to @containers-verified@ in your @.cabal@ file and earn bragging+ rights about using verified data structures in your project. Because the+ types from @containers@ are re-exported, you can still interface with other+ libraries that depend on @containers@ directly.+ .+ If you happen to need additional modules or functions, you will have to+ depend on both @containers@ and @containers-verified@, and use+ <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#package-qualified-imports package-qualified imports> to disambiguate.+ .+ This package does not re-export any of the @….Internals@ modules.+ .+ We cannot control which type class instances are re-exported; these therefore+ may give you access to unverified code. Also, the @conatiners@ code contains+ some CPP directives; these can enable different code on your machine than the+ code that we verified (e.g. different bit-widths).+ .+ To learn more about what exactly has been verified, and how wide the+ formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq+ to non-trivial Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao+ Li, Christine Rizkallah, John Wiegley and Stephanie Weirich.++ .+ The long-term maintenance plan for this package is not fleshed out yet, and+ certainly depends on user-demand. Let us know your needs! (And your+ technical or financial abilities to contribute...)+++homepage: https://github.com/nomeata/containers-verified+license: MIT+license-file: LICENSE+author: Joachim Breitner+maintainer: mail@joachim-breitner.de+copyright: 2018 Joachim Breitner+category: Data+build-type: Simple+extra-source-files: ChangeLog.md+cabal-version: >=1.10++library+ build-depends: containers ==0.5.11.0+ default-language: Haskell2010+ exposed-modules:+ Data.Set+ Data.IntSet+ Data.Map++source-repository head+ type: git+ location: http://github.com/nomeata/containers-verified+