diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for containers-verified + +## 0.5.11.0 -- 2018-03-15 + +* First version. diff --git a/Data/IntSet.hs b/Data/IntSet.hs new file mode 100644 --- /dev/null +++ b/Data/IntSet.hs @@ -0,0 +1,90 @@ +{-# OPTIONS_HADDOCK not-home #-} +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Please see the documentation of 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 diff --git a/Data/Map.hs b/Data/Map.hs new file mode 100644 --- /dev/null +++ b/Data/Map.hs @@ -0,0 +1,188 @@ +{-# OPTIONS_HADDOCK not-home #-} +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Please see the documentation of 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 diff --git a/Data/Set.hs b/Data/Set.hs new file mode 100644 --- /dev/null +++ b/Data/Set.hs @@ -0,0 +1,101 @@ +{-# OPTIONS_HADDOCK not-home #-} +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Please see the documentation of 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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/containers-verified.cabal b/containers-verified.cabal new file mode 100644 --- /dev/null +++ b/containers-verified.cabal @@ -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 , parts of the + library were + formally verified using 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 + 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 +