packages feed

liquid-prelude 0.9.2.8.2 → 0.9.10.1.2

raw patch · 5 files changed

+79/−53 lines, 5 filesdep ~liquidhaskell

Dependency ranges changed: liquidhaskell

Files

liquid-prelude.cabal view
@@ -1,6 +1,6 @@ cabal-version:      1.24 name:               liquid-prelude-version:            0.9.2.8.2+version:            0.9.10.1.2 synopsis:           General utility modules for LiquidHaskell description:        General utility modules for LiquidHaskell. license:            BSD3@@ -30,5 +30,5 @@                     , ghc-prim                     , bytestring           >= 0.10.12.1                     , containers           >= 0.6.4.1-                    , liquidhaskell        >= 0.9.2.8+                    , liquidhaskell        >= 0.9.10.1.2   default-language:   Haskell2010
src/Language/Haskell/Liquid/Bag.hs view
@@ -1,56 +1,71 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}+ module Language.Haskell.Liquid.Bag where  import qualified Data.Map      as M -{-@ embed   Data.Map.Map as Map_t                                         @-}--{-@ measure Map_default :: Int -> Bag a                                   @-}-{-@ measure Map_union   :: Bag a -> Bag a -> Bag a                        @-}-{-@ measure Map_select  :: Data.Map.Map k v -> k -> v                     @-}-{-@ measure Map_store   :: Data.Map.Map k v -> k -> v -> Data.Map.Map k v @-}-{-@ measure bagSize     :: Bag k -> Int                                   @-}+{-@ embed   Bag as Bag_t                             @-}+{-@ measure bagSize       :: Bag a -> Int            @-}  -- if I just write measure fromList the measure definition is not imported {-@ measure fromList :: [k] -> Bag k-      fromList ([])   = (Map_default 0)-      fromList (x:xs) = Map_store (fromList xs) x (1 + (Map_select (fromList xs) x))+      fromList ([])   = (Bag_empty 0)+      fromList (x:xs) = Bag_union (fromList xs) (Bag_sng x 1) @-}  -{-@ type Bag a = Data.Map.Map a Nat @-}-type Bag a = M.Map a Int+-- TODO newtype doesn't work because LH still expands the definition+-- https://github.com/ucsd-progsys/liquidhaskell/issues/2332+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq -{-@ assume empty :: {v:Bag k | v = Map_default 0} @-}+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}+{-@ define empty                = (Bag_empty 0) @-} empty :: Bag k-empty = M.empty--{-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}-bagSize :: Bag k -> Int -bagSize b = sum (M.elems b) --{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-} -fromList :: (Ord k) => [k] -> Bag k -fromList []     = empty-fromList (x:xs) = put x (fromList xs)+empty = Bag M.empty -{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Map_select b k}  @-}+{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count k b}  @-}+{-@ define get               k      b                    = (Bag_count k b) @-} get :: (Ord k) => k -> Bag k -> Int-get k m = M.findWithDefault 0 k m+get k b = M.findWithDefault 0 k (toMap b) -{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Map_store b k (1 + (Map_select b k))} @-}-{-@ ignore put @-}+{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}+{-@ define put               k      b                      = (Bag_union b (Bag_sng k 1)) @-} put :: (Ord k) => k -> Bag k -> Bag k-put k m = M.insert k (1 + get k m) m+put k b = Bag (M.insert k (1 + get k b) (toMap b)) -{-@ assume union :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Map_union m1 m2} @-}+{-@ assume union :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union a b} @-}+{-@ define union               a          b                      = (Bag_union a b) @-} union :: (Ord k) => Bag k -> Bag k -> Bag k-union m1 m2 = M.union m1 m2+union b1 b2 = Bag (M.unionWith (+) (toMap b1) (toMap b2)) -{-@ thm_emp :: x:k -> xs:Bag k ->  { Language.Haskell.Liquid.Bag.empty /= put x xs }  @-}+{-@ assume unionMax :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union_max a b} @-}+{-@ define unionMax               a          b                      = (Bag_union_max a b) @-}+unionMax :: (Ord k) => Bag k -> Bag k -> Bag k+unionMax b1 b2 = Bag (M.unionWith max (toMap b1) (toMap b2))++{-@ assume interMin :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_inter_min a b} @-}+{-@ define interMin               a          b                      = (Bag_inter_min a b) @-}+interMin :: (Ord k) => Bag k -> Bag k -> Bag k+interMin b1 b2 = Bag (M.intersectionWith min (toMap b1) (toMap b2))++{-@ assume sub :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bool | v = Bag_sub a b} @-}+{-@ define sub               a          b                     = (Bag_sub a b) @-}+sub :: (Ord k) => Bag k -> Bag k -> Bool+sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)++{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-}+fromList :: (Ord k) => [k] -> Bag k+fromList []     = empty+fromList (x:xs) = put x (fromList xs)++{-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}+bagSize :: Bag k -> Int+bagSize b = sum (M.elems (toMap b))++{-@ thm_emp :: x:k -> xs:Bag k -> { empty /= put x xs } @-} 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 }  @-}-thm_size :: (Ord k) => [k] -> ()  -thm_size _ = () +{-@ assume thm_size :: xs:[k] -> { bagSize (fromList xs) == len xs } @-}+thm_size :: (Ord k) => [k] -> ()+thm_size _ = ()
src/Language/Haskell/Liquid/Foreign.hs view
@@ -35,7 +35,7 @@ cSizeInt = fromIntegral  -{-@ assume mkPtr :: x:GHC.Prim.Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}+{-@ assume mkPtr :: x:Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-} mkPtr   :: Addr# -> Ptr b mkPtr = undefined -- Ptr x
src/Language/Haskell/Liquid/Prelude.hs view
@@ -134,10 +134,18 @@ safeZipWith _ []     []     = [] safeZipWith _ _ _ = error "safeZipWith: cannot happen!" -{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p =>  q)} @-}+{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p => q)} @-} infixr 8 ==> (==>) :: Bool -> Bool -> Bool False ==> False = True False ==> True  = True True  ==> True  = True True  ==> False = False++{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p <=> q)} @-}+infixr 8 <=>+(<=>) :: Bool -> Bool -> Bool+False <=> False = True+False <=> True  = False+True  <=> True  = True+True  <=> False = False
src/Language/Haskell/Liquid/ProofCombinators.hs view
@@ -10,7 +10,7 @@    -- * Proof is just a () alias   Proof-  , toProof +  , toProof    -- * Proof constructors   , trivial, unreachable, (***), QED(..)@@ -21,18 +21,18 @@   -- * These two operators check all intermediate equalities   , (===) -- proof of equality is implicit eg. x === y   , (=<=) -- proof of equality is implicit eg. x <= y-  , (=>=)  -- proof of equality is implicit eg. x =>= y +  , (=>=)  -- proof of equality is implicit eg. x =>= y    -- * This operator does not check intermediate equalities-  , (==.) +  , (==.)    -- Uncheck operator used only for proof debugging   , (==!) -- x ==! y always succeeds    -- * Combining Proofs   , (&&&)-  , withProof -  , impossible +  , withProof+  , impossible    -- * PLE-specific   , pleUnfold@@ -75,8 +75,10 @@  data QED = Admit | QED -{-@ measure isAdmit :: QED -> Bool @-}-{-@ Admit :: {v:QED | isAdmit v } @-}+{-@ measure isAdmit @-}+isAdmit :: QED -> Bool+isAdmit Admit = True+isAdmit QED   = False   -------------------------------------------------------------------------------@@ -120,9 +122,9 @@ infixl 3 ?  {-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}-(?) :: a -> b -> a -x ? _ = x -{-# INLINE (?)   #-} +(?) :: a -> b -> a+x ? _ = x+{-# INLINE (?)   #-}  ------------------------------------------------------------------------------- -- | Assumed equality@@ -149,13 +151,13 @@ -- | The above operators check each intermediate proof step. --   The operator `==.` below accepts an optional proof term --   argument, but does not check intermediate steps.---   So, using `==.` the proofs are faster, but the error messages worse. +--   So, using `==.` the proofs are faster, but the error messages worse.  infixl 3 ==. -{-# INLINE (==.) #-} -(==.) :: a -> a -> a -_ ==. x = x +{-# INLINE (==.) #-}+(==.) :: a -> a -> a+_ ==. x = x  ------------------------------------------------------------------------------- -- | * Combining Proof Certificates -------------------------------------------@@ -165,7 +167,8 @@ x &&& _ = x  -{-@ withProof :: x:a -> b -> {v:a | v = x} @-}+{-@        withProof :: x:a -> b -> {v:a | v = x} @-}+{-@ define withProof    x      y            = (x) @-} withProof :: a -> b -> a withProof x _ = x @@ -174,7 +177,7 @@ impossible _ = undefined  ---------------------------------------------------------------------------------- | Convenient Syntax for Inductive Propositions +-- | Convenient Syntax for Inductive Propositions -------------------------------------------------------------------------------  {-@ measure prop :: a -> b           @-}