liquid-containers 0.6.2.1 → 0.6.4.1
raw patch · 2 files changed
+27/−23 lines, 2 filesdep ~containersdep ~liquidhaskellnew-uploader
Dependency ranges changed: containers, liquidhaskell
Files
- liquid-containers.cabal +5/−4
- src/Data/Set.spec +22/−19
liquid-containers.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.24 name: liquid-containers-version: 0.6.2.1+version: 0.6.4.1 synopsis: LiquidHaskell specs for the containers package description: LiquidHaskell specs for the containers package. license: BSD3@@ -15,7 +15,7 @@ data-files: src/Data/Set.spec custom-setup- setup-depends: Cabal, base, liquidhaskell+ setup-depends: Cabal<4, base<5, liquidhaskell library exposed-modules: Data.Containers.ListUtils@@ -49,9 +49,10 @@ Utils.Containers.Internal.StrictPair hs-source-dirs: src build-depends: liquid-base < 5- , containers >= 0.6.2.1 && < 0.7- , liquidhaskell >= 0.8.10.1+ , containers >= 0.6.4.1 && < 0.7+ , liquidhaskell >= 0.9.0.2 default-language: Haskell2010 default-extensions: PackageImports if impl(ghc >= 8.10) ghc-options: -fplugin=LiquidHaskell+
src/Data/Set.spec view
@@ -2,38 +2,38 @@ embed Data.Set.Internal.Set as Set_Set -// -----------------------------------------------------------------------------------------------// -- | Logical Set Operators: Interpreted "natively" by the SMT solver --------------------------// ----------------------------------------------------------------------------------------------+// ----------------------------------------------------------------------------------------------+// -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------+// ---------------------------------------------------------------------------------------------- -// union+// union measure Set_cup :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -// intersection+// intersection measure Set_cap :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -// difference+// difference measure Set_dif :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -// singleton+// singleton measure Set_sng :: a -> (Data.Set.Internal.Set a) -// emptiness test+// emptiness test measure Set_emp :: (Data.Set.Internal.Set a) -> GHC.Types.Bool -// empty set+// empty set measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Internal.Set a) -// membership test+// membership test measure Set_mem :: a -> (Data.Set.Internal.Set a) -> GHC.Types.Bool -// inclusion test+// inclusion test measure Set_sub :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> GHC.Types.Bool -// ----------------------------------------------------------------------------------------------// -- | Refined Types for Data.Set Operations ---------------------------------------------------// ---------------------------------------------------------------------------------------------+// ---------------------------------------------------------------------------------------------+// -- | Refined Types for Data.Set Operations --------------------------------------------------+// --------------------------------------------------------------------------------------------- isSubsetOf :: (GHC.Classes.Ord a) => x:(Data.Set.Internal.Set a) -> y:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_sub x y} member :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_mem x xs}@@ -49,11 +49,14 @@ difference :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs ys} fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Internal.Set a | v = listElts xs}+toList :: GHC.Classes.Ord a => s:Data.Set.Internal.Set a -> {xs:[a] | s = listElts xs} -// ----------------------------------------------------------------------------------------------// -- | The set of elements in a list -----------------------------------------------------------// ---------------------------------------------------------------------------------------------+// ---------------------------------------------------------------------------------------------+// -- | The set of elements in a list ----------------------------------------------------------+// --------------------------------------------------------------------------------------------- measure listElts :: [a] -> (Data.Set.Internal.Set a)-listElts([]) = {v | (Set_emp v)}-listElts(x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }+ listElts [] = {v | (Set_emp v)}+ listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }++