liquid-prelude 0.8.10.2 → 0.9.14.1
raw patch · 12 files changed
Files
- liquid-prelude.cabal +7/−10
- src/KMeansHelper.hs +0/−78
- src/Language/Haskell/Liquid/Bag.hs +50/−32
- src/Language/Haskell/Liquid/Equational.hs +21/−20
- src/Language/Haskell/Liquid/Foreign.hs +2/−1
- src/Language/Haskell/Liquid/List.hs +1/−0
- src/Language/Haskell/Liquid/Prelude.hs +11/−2
- src/Language/Haskell/Liquid/ProofCombinators.hs +65/−25
- src/Language/Haskell/Liquid/RTick.hs +1/−0
- src/Language/Haskell/Liquid/RTick/Combinators.hs +1/−0
- src/Language/Haskell/Liquid/String.hs +14/−13
- src/Language/Haskell/Liquid/Synthesize/Error.hs +0/−5
liquid-prelude.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.24 name: liquid-prelude-version: 0.8.10.2+version: 0.9.14.1 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, base, liquidhaskell+ setup-depends: Cabal<4, base<5, liquidhaskell-boot library exposed-modules: Language.Haskell.Liquid.RTick@@ -25,13 +25,10 @@ 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.0.0 && < 0.11- , containers >= 0.6.0.0 && < 0.7- , liquidhaskell >= 0.8.10.2+ build-depends: base < 5+ , ghc-prim+ , bytestring >= 0.10.12.1+ , containers >= 0.6.4.1+ , liquidhaskell >= 0.9.14.1 default-language: Haskell2010- if impl(ghc >= 8.10)- ghc-options: -fplugin=LiquidHaskell
− src/KMeansHelper.hs
@@ -1,78 +0,0 @@-module KMeansHelper where--import Prelude hiding (zipWith)-import Data.List (sort, span, minimumBy)-import Data.Function (on)-import Data.Ord (comparing)-import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError)----- | Fixed-Length Lists--{-@ type List a N = {v : [a] | (len v) = N} @-}----- | N Dimensional Points--{-@ type Point N = List Double N @-}--{-@ type NonEmptyList a = {v : [a] | (len v) > 0} @-}---- | Clustering --{-@ type Clustering a = [(NonEmptyList a)] @-}----------------------------------------------------------------------- | Grouping By a Predicate ----------------------------------------------------------------------------------------------------------{-@ groupBy :: (a -> a -> Bool) -> [a] -> (Clustering a) @-}-groupBy _ [] = []-groupBy eq (x:xs) = (x:ys) : groupBy eq zs- where (ys,zs) = span (eq x) xs----------------------------------------------------------------------- | Partitioning By a Size -----------------------------------------------------------------------------------------------------------{-@ type PosInt = {v: Int | v > 0 } @-}--{-@ partition :: size:PosInt -> xs:[a] -> (Clustering a) / [len xs] @-}--partition size [] = []-partition size ys@(_:_) = zs : partition size zs'- where- zs = take size ys- zs' = drop size ys---------------------------------------------------------------------------- | Safe Zipping -------------------------------------------------------------------------------------------------------------------------------{-@ zipWith :: (a -> b -> c) -> xs:[a] -> (List b (len xs)) -> (List c (len xs)) @-}-zipWith f (a:as) (b:bs) = f a b : zipWith f as bs-zipWith _ [] [] = []---- Other cases only for exposition-zipWith _ (_:_) [] = liquidError "Dead Code"-zipWith _ [] (_:_) = liquidError "Dead Code"---------------------------------------------------------------------------- | "Matrix" Transposition ---------------------------------------------------------------------------------------------------------------------{-@ type Matrix a Rows Cols = (List (List a Cols) Rows) @-}--{-@ transpose :: c:Int -> r:PosInt -> Matrix a r c -> Matrix a c r @-}--transpose :: Int -> Int -> [[a]] -> [[a]]-transpose 0 _ _ = []-transpose c r ((x:xs) : xss) = (x : map head xss) : transpose (c-1) r (xs : map tail xss)---- Or, with comprehensions--- transpose c r ((x:xs):xss) = (x : [ xs' | (x':_) <- xss ]) : transpose (c-1) r (xs : [xs' | (_ : xs') <- xss])---- Not needed, just for exposition-transpose c r ([] : _) = liquidError "dead code"-transpose c r [] = liquidError "dead code"-
src/Language/Haskell/Liquid/Bag.hs view
@@ -1,53 +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 = 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))} @-}+{-@ 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 } @-}-thm_emp :: (Ord k) => k -> Bag k -> () +{-@ 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/Equational.hs view
@@ -1,4 +1,5 @@-module Language.Haskell.Liquid.Equational where +{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}+module Language.Haskell.Liquid.Equational where ------------------------------------------------------------------------------- -- | Proof is just unit@@ -7,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@@ -43,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
src/Language/Haskell/Liquid/Foreign.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} {-# OPTIONS_GHC -fno-warn-unused-imports #-} {-# LANGUAGE MagicHash #-} @@ -34,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/List.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} module Language.Haskell.Liquid.List (transpose) where {-@ lazy transpose @-}
src/Language/Haskell/Liquid/Prelude.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} {-# LANGUAGE MagicHash #-} module Language.Haskell.Liquid.Prelude where@@ -126,17 +127,25 @@ ----------------------------------------------------------------------------------------------- -{-@ 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 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
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeFamilies #-}@@ -9,7 +10,7 @@ -- * Proof is just a () alias Proof- , toProof + , toProof -- * Proof constructors , trivial, unreachable, (***), QED(..)@@ -20,19 +21,21 @@ -- * 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 ) where @@ -72,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 -------------------------------------------------------------------------------@@ -110,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 (?) #-} +(?) :: 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 ------------------------------------------------------------------------------- @@ -135,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 -------------------------------------------@@ -146,15 +175,13 @@ -- | The above operators check each intermediate proof step. -- The operator `==.` below accepts an optional proof term -- argument, but does not check intermediate steps.--- TODO: What is it USEFUL FOR?+-- So, using `==.` the proofs are faster, but the error messages worse. infixl 3 ==. -{-# DEPRECATED (==.) "Use (===) instead" #-}--{-# INLINE (==.) #-} -(==.) :: a -> a -> a -_ ==. x = x +{-# INLINE (==.) #-}+(==.) :: a -> a -> a+_ ==. x = x ------------------------------------------------------------------------------- -- | * Combining Proof Certificates -------------------------------------------@@ -164,7 +191,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 @@ -173,11 +201,23 @@ impossible _ = undefined ---------------------------------------------------------------------------------- | Convenient Syntax for Inductive Propositions +-- | Convenient Syntax for Inductive Propositions ------------------------------------------------------------------------------- {-@ measure prop :: a -> b @-} {-@ type Prop E = {v:_ | prop v = E} @-} +-- New syntax for "inductive propositions", aka indexed types, it+-- should be used in place of `Prop` that is kept for backward+-- compatibility.+{-@ type Ix typ E = {v:typ | prop v = E} @-} +-------------------------------------------------------------------------------+-- PLE-specific+------------------------------------------------------------------------------- +-- | Forces PLE to unfold a function application if the body of the function+-- starts with an application of @pleUnfold@.+{-@ reflect pleUnfold @-}+pleUnfold :: a -> a+pleUnfold x = x
src/Language/Haskell/Liquid/RTick.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} -- -- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
src/Language/Haskell/Liquid/RTick/Combinators.hs view
@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-} -- -- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
src/Language/Haskell/Liquid/String.hs view
@@ -1,4 +1,5 @@--- Support for Strings for SMT +{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}+-- Support for Strings for SMT {-# LANGUAGE OverloadedStrings #-} @@ -9,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 } @-}@@ -24,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)@@ -33,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
− src/Language/Haskell/Liquid/Synthesize/Error.hs
@@ -1,5 +0,0 @@-module Language.Haskell.Liquid.Synthesize.Error where --{-@ err :: { v: Int | false } -> a @-}-err :: Int -> a-err s = undefined