liquid-prelude 0.9.12.2.1 → 0.9.14.1

raw patch · 5 files changed

+67/−43 lines, 5 filesdep ~liquidhaskellPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: liquidhaskell

API changes (from Hackage documentation)

Files

• liquid-prelude.cabal +2/−2
• src/Language/Haskell/Liquid/Equational.hs +20/−20
• src/Language/Haskell/Liquid/Prelude.hs +1/−1
• src/Language/Haskell/Liquid/ProofCombinators.hs +31/−7
• src/Language/Haskell/Liquid/String.hs +13/−13

@@ -1,6 +1,6 @@ cabal-version:      1.24 name:               liquid-prelude-version:            0.9.12.2.1+version:            0.9.14.1 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.12.2.1+                    , liquidhaskell        >= 0.9.14.1   default-language:   Haskell2010

@@ -1,5 +1,5 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}-module Language.Haskell.Liquid.Equational where +module Language.Haskell.Liquid.Equational where  ------------------------------------------------------------------------------- -- | Proof is just unit@@ -8,34 +8,34 @@ type Proof = ()  ---------------------------------------------------------------------------------- | Casting expressions to Proof using the "postfix" `*** QED` +-- | Casting expressions to Proof using the "postfix" `*** QED` ------------------------------------------------------------------------------- -data QED = QED +data QED = QED  infixl 2 *** (***) :: a -> QED -> Proof-_ *** QED = () +_ *** QED = ()  ---------------------------------------------------------------------------------- | Equational Reasoning operators --- | The `eq` operator is inlined in the logic, so can be used in reflected --- | functions while ignoring the equality steps. +-- | Equational Reasoning operators+-- | The `eq` operator is inlined in the logic, so can be used in reflected+-- | functions while ignoring the equality steps. ------------------------------------------------------------------------------- -infixl 3 ==., `eq` +infixl 3 ==., `eq`   {-@ (==.) :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}-(==.) :: a -> a -> a -_ ==. x = x -{-# INLINE (==.) #-} +(==.) :: a -> a -> a+_ ==. x = x+{-# INLINE (==.) #-}   {-@ eq :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}-eq :: a -> a -> a -_ `eq` x = x -{-# INLINE eq #-} +eq :: a -> a -> a+_ `eq` x = x+{-# INLINE eq #-}  ------------------------------------------------------------------------------- -- | Explanations@@ -44,13 +44,13 @@ infixl 3 ?  {-@ (?) :: forall a b <pa :: a -> Bool>. a<pa> -> b -> a<pa> @-}-(?) :: a -> b -> a -x ? _ = x -{-# INLINE (?)   #-} +(?) :: a -> b -> a+x ? _ = x+{-# INLINE (?)   #-}  ---------------------------------------------------------------------------------- | Using proofs as theorems +-- | Using proofs as theorems ------------------------------------------------------------------------------- -withTheorem :: a -> Proof -> a -withTheorem z _ = z +withTheorem :: a -> Proof -> a+withTheorem z _ = z

@@ -127,7 +127,7 @@  ----------------------------------------------------------------------------------------------- -{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs} +{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs}                 -> {v : [c] | len v = len xs } @-} safeZipWith :: (a->b->c) -> [a]->[b]->[c] safeZipWith f (a:as) (b:bs) = f a b : safeZipWith f as bs

@@ -115,20 +115,44 @@ _ =>= y  = y  ---------------------------------------------------------------------------------- | `?` is basically Haskell's $ and is used for the right precedence--- | `?` lets you "add" some fact into a proof term+-- | @e ? lemma@ lets you use the type of @lemma@ when checking that @e@ haskell+-- has some expected refinement type.+--+-- Schematically, @?@ allows to use @q x@ to check that @e@ satisfies @p x e@+-- in the following function.+--+-- > f :: x:t0 -> {v:t1 | p x v}+-- > f x = e ? lemma x+-- >   where+-- >     lemma :: y:t0 -> { q y }+-- >     lemma = ...+--+-- While @?@ is defined as Haskell's 'const', @?@ is optimized by Liquid+-- Haskell. The 'const' function, on the other hand, would incur some extra+-- verification overhead because Liquid Haskell needs to go through the trouble+-- of checking that @const e lemma@ is actually @e@.+--+-- === At a lower level+--+-- Liquid Haskell treats @e ? lemma@ as+--+-- > let fresh0 = e+-- >  in let fresh1 = lemma+-- >      in fresh0+--+-- Which makes the @fresh1@ binding available in the environment of whatever+-- constraints arise in the inner occurrence of @fresh0@. -------------------------------------------------------------------------------  infixl 3 ? -{-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-} (?) :: a -> b -> a x ? _ = x {-# INLINE (?)   #-}  ------------------------------------------------------------------------------- -- | Assumed equality--- 	`x ==! y `+--      `x ==! y ` --   returns the admitted proof certificate that result value is equals x and y ------------------------------------------------------------------------------- @@ -140,9 +164,9 @@  -- | To summarize: ----- 	- (==!) is *only* for proof debugging---	- (===) does not require explicit proof term--- 	- (?)   lets you insert "lemmas" as other `Proof` values+--      - (==!) is *only* for proof debugging+--      - (===) does not require explicit proof term+--      - (?)   lets you insert "lemmas" as other `Proof` values  ------------------------------------------------------------------------------- -- | * Unchecked Proof Certificates -------------------------------------------

@@ -1,5 +1,5 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}--- Support for Strings for SMT +-- Support for Strings for SMT  {-# LANGUAGE OverloadedStrings   #-} @@ -10,7 +10,7 @@  {-@ embed SMTString as Str @-} -data SMTString = S BS.ByteString +data SMTString = S BS.ByteString   deriving (Eq, Show)  {-@ invariant {s:SMTString | 0 <= stringLen s } @-}@@ -25,7 +25,7 @@  ---------------------------------- -{-@ assume concatString :: x:SMTString -> y:SMTString +{-@ assume concatString :: x:SMTString -> y:SMTString                  -> {v:SMTString | v == concatString x y && stringLen v == stringLen x + stringLen y } @-} concatString :: SMTString -> SMTString -> SMTString concatString (S s1) (S s2) = S (s1 `BS.append` s2)@@ -34,30 +34,30 @@ stringEmp :: SMTString stringEmp = S (BS.empty) -stringLen :: SMTString -> Int  +stringLen :: SMTString -> Int {-@ assume stringLen :: x:SMTString -> {v:Nat | v == stringLen x} @-}-stringLen (S s) = BS.length s +stringLen (S s) = BS.length s   {-@ assume subString  :: s:SMTString -> offset:Int -> ln:Int -> {v:SMTString | v == subString s offset ln } @-}-subString :: SMTString -> Int -> Int -> SMTString -subString (S s) o l = S (BS.take l $ BS.drop o s) +subString :: SMTString -> Int -> Int -> SMTString+subString (S s) o l = S (BS.take l $ BS.drop o s)  -{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-} +{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-} takeString :: Int -> SMTString -> SMTString takeString i (S s) = S (BS.take i s) -{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-} +{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-} dropString :: Int -> SMTString -> SMTString dropString i (S s) = S (BS.drop i s)   {-@ assume fromString :: i:String -> {o:SMTString | i == o && o == fromString i} @-} fromString :: String -> SMTString-fromString = S . ST.fromString +fromString = S . ST.fromString  -{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-} -isNullString :: SMTString -> Bool -isNullString (S s) = BS.length s == 0 +{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-}+isNullString :: SMTString -> Bool+isNullString (S s) = BS.length s == 0