liquid-prelude 0.9.0.2 → 0.9.2.5

raw patch · 3 files changed

+9/−13 lines, 3 filesdep +basedep +ghc-primdep −liquid-basedep ~bytestringdep ~liquidhaskell

Dependencies added: base, ghc-prim

Dependencies removed: liquid-base

Dependency ranges changed: bytestring, liquidhaskell

Files

• liquid-prelude.cabal +6/−7
• src/Language/Haskell/Liquid/Bag.hs +3/−1
• src/Language/Haskell/Liquid/Synthesize/Error.hs +0/−5

@@ -1,6 +1,6 @@ cabal-version:      1.24 name:               liquid-prelude-version:            0.9.0.2+version:            0.9.2.5 synopsis:           General utility modules for LiquidHaskell description:        General utility modules for LiquidHaskell. license:            BSD3@@ -13,7 +13,7 @@ build-type:         Custom  custom-setup-  setup-depends: Cabal<4, base<5, liquidhaskell+  setup-depends: Cabal<4, base<5, liquidhaskell-boot  library   exposed-modules:  Language.Haskell.Liquid.RTick@@ -25,14 +25,13 @@                     Language.Haskell.Liquid.Equational                     Language.Haskell.Liquid.Bag                     Language.Haskell.Liquid.ProofCombinators-                    Language.Haskell.Liquid.Synthesize.Error                     KMeansHelper   hs-source-dirs:     src-  build-depends:      liquid-base          < 5-                    , bytestring           >= 0.10.12.1 && < 0.11+  build-depends:      base          < 5+                    , ghc-prim+                    , bytestring           >= 0.10.12.1 && < 0.12                     , containers           >= 0.6.4.1  && < 0.7-                    , liquidhaskell        >= 0.9.0.2+                    , liquidhaskell        >= 0.9.2.5   default-language:   Haskell2010   if impl(ghc >= 8.10)     ghc-options: -fplugin=LiquidHaskell-  

@@ -17,6 +17,7 @@ @-}  +{-@ type Bag a = Data.Map.Map a Nat @-} type Bag a = M.Map a Int  {-@ assume empty :: {v:Bag k | v = Map_default 0} @-}@@ -37,6 +38,7 @@ get k m = M.findWithDefault 0 k m  {-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Map_store b k (1 + (Map_select b k))} @-}+{-@ ignore put @-} put :: (Ord k) => k -> Bag k -> Bag k put k m = M.insert k (1 + get k m) m @@ -45,7 +47,7 @@ union m1 m2 = M.union m1 m2  {-@ thm_emp :: x:k -> xs:Bag k ->  { Language.Haskell.Liquid.Bag.empty /= put x xs }  @-}-thm_emp :: (Ord k) => k -> Bag k -> ()  +thm_emp :: (Ord k) => k -> Bag k -> () thm_emp x xs = const () (get x xs)  {-@ assume thm_size :: xs:[k] ->  { bagSize (fromList xs) == len xs }  @-}

@@ -1,5 +0,0 @@-module Language.Haskell.Liquid.Synthesize.Error where --{-@ err :: { v: Int | false } -> a @-}-err :: Int -> a-err s = undefined