packages feed

liquid-prelude (empty) → 0.8.10.1

raw patch · 14 files changed

+1528/−0 lines, 14 filesdep +bytestringdep +containersdep +liquid-basebuild-type:Customsetup-changed

Dependencies added: bytestring, containers, liquid-base, liquidhaskell

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013-2014, Ranjit Jhala++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Ranjit Jhala nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main where++import Language.Haskell.Liquid.Cabal (liquidHaskellMain)++main :: IO ()+main = liquidHaskellMain
+ liquid-prelude.cabal view
@@ -0,0 +1,37 @@+cabal-version:      1.24+name:               liquid-prelude+version:            0.8.10.1+synopsis:           General utility modules for LiquidHaskell+description:        General utility modules for LiquidHaskell.+license:            BSD3+license-file:       LICENSE+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.+author:             Ranjit Jhala, Niki Vazou, Eric Seidel+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>+category:           Language+homepage:           https://github.com/ucsd-progsys/liquidhaskell+build-type:         Custom++custom-setup+  setup-depends: Cabal, base, liquidhaskell++library+  exposed-modules:  Language.Haskell.Liquid.RTick+                    Language.Haskell.Liquid.Prelude+                    Language.Haskell.Liquid.Foreign+                    Language.Haskell.Liquid.RTick.Combinators+                    Language.Haskell.Liquid.String+                    Language.Haskell.Liquid.List+                    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.1+  default-language:   Haskell2010+  if impl(ghc >= 8.10)+    ghc-options: -fplugin=LiquidHaskell
+ src/KMeansHelper.hs view
@@ -0,0 +1,78 @@+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
@@ -0,0 +1,53 @@+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                                   @-}++-- 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))+@-}+++type Bag a = M.Map a Int++{-@ assume empty :: {v:Bag k | v = Map_default 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)++{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Map_select b k}  @-}+get :: (Ord k) => k -> Bag k -> Int+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))} @-}+put :: (Ord k) => k -> Bag k -> Bag k+put k m = M.insert k (1 + get k m) m++{-@ assume union :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Map_union m1 m2} @-}+union :: (Ord k) => Bag k -> Bag k -> Bag k+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 x xs = const () (get x xs)++{-@ assume thm_size :: xs:[k] ->  { bagSize (fromList xs) == len xs }  @-}+thm_size :: (Ord k) => [k] -> ()  +thm_size _ = ()
+ src/Language/Haskell/Liquid/Equational.hs view
@@ -0,0 +1,55 @@+module Language.Haskell.Liquid.Equational where ++-------------------------------------------------------------------------------+-- | Proof is just unit+-------------------------------------------------------------------------------++type Proof = ()++-------------------------------------------------------------------------------+-- | Casting expressions to Proof using the "postfix" `*** QED` +-------------------------------------------------------------------------------++data QED = QED ++infixl 2 ***+(***) :: a -> QED -> Proof+_ *** QED = () ++-------------------------------------------------------------------------------+-- | 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` +++{-@ (==.) :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}+(==.) :: 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 #-} ++-------------------------------------------------------------------------------+-- | Explanations+-------------------------------------------------------------------------------++infixl 3 ?++{-@ (?) :: forall a b <pa :: a -> Bool>. a<pa> -> b -> a<pa> @-}+(?) :: a -> b -> a +x ? _ = x +{-# INLINE (?)   #-} ++-------------------------------------------------------------------------------+-- | Using proofs as theorems +-------------------------------------------------------------------------------++withTheorem :: a -> Proof -> a +withTheorem z _ = z
+ src/Language/Haskell/Liquid/Foreign.hs view
@@ -0,0 +1,64 @@+{-# OPTIONS_GHC -fno-warn-unused-imports #-}+{-# LANGUAGE MagicHash #-}++{- OPTIONS_GHC -cpp #-}+{- OPTIONS_GHC -cpp -fglasgow-exts -}++module Language.Haskell.Liquid.Foreign where++import Foreign.C.Types          (CSize(..))+import Foreign.Ptr+import Foreign.ForeignPtr+import GHC.Base++import Data.Word (Word64) -- Necessary to bring in scope the evidence that Word64 = int++-- TODO: shouldn't have to re-import these (tests/pos/imp0.hs)+{- import Foreign.C.Types    -}+{- import Foreign.Ptr        -}+{- import Foreign.ForeignPtr -}+{- import GHC.Base           -}++++-----------------------------------------------------------------------------------------------++{-# NOINLINE intCSize #-}+{-@ assume intCSize :: x:Int -> {v: CSize | v = x } @-}+intCSize :: Int -> CSize+intCSize = fromIntegral++{-# NOINLINE cSizeInt #-}+{-@ assume cSizeInt :: x:CSize -> {v: Int | v = x } @-}+cSizeInt :: CSize -> Int+cSizeInt = fromIntegral+++{-@ assume mkPtr :: x:GHC.Prim.Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}+mkPtr   :: Addr# -> Ptr b+mkPtr = undefined -- Ptr x+++{-@ assume isNullPtr :: p:(Ptr a) -> {v:Bool | (v <=> (isNullPtr p)) } @-}+isNullPtr :: Ptr a -> Bool+isNullPtr p = (p == nullPtr)+{-# INLINE isNullPtr #-}++{-@ fpLen :: p:(ForeignPtr a) -> {v:Int | v = (fplen p) } @-}+fpLen :: ForeignPtr a -> Int+fpLen = undefined++{-@ pLen :: p:(Ptr a) -> {v:Int | v = (plen p) } @-}+pLen :: Ptr a -> Int+pLen = undefined++{-@ deref :: p:Ptr a -> {v:a | v = (deref p)} @-}+deref :: Ptr a -> a+deref = undefined++{-@ eqPtr :: p:PtrV a+          -> q:{v:PtrV a | (((pbase v) = (pbase p)) && ((plen v) <= (plen p)))}+          -> {v:Bool | (v <=> ((plen p) = (plen q)))}+  @-}+eqPtr :: Ptr a -> Ptr a -> Bool+eqPtr = undefined
+ src/Language/Haskell/Liquid/List.hs view
@@ -0,0 +1,7 @@+module Language.Haskell.Liquid.List (transpose) where++{-@ lazy transpose @-}+transpose                  :: Int -> [[a]] -> [[a]]+transpose _ []             = []+transpose n ([]   : xss)   = transpose n xss+transpose n ((x:xs) : xss) = (x : [h | (h:_) <- xss]) : transpose (n - 1) (xs : [ t | (_:t) <- xss])
+ src/Language/Haskell/Liquid/Prelude.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE MagicHash      #-}++module Language.Haskell.Liquid.Prelude where++-------------------------------------------------------------------+--------------------------- Arithmetic ----------------------------+-------------------------------------------------------------------++{-@ assume plus   :: x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}  @-}+{-@ assume minus  :: x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x - y} @-}+{-@ assume times  :: x:Int -> y:Int -> Int                           @-}+{-@ assume eq     :: x:Int -> y:Int -> {v:Bool | ((v) <=> x = y)}  @-}+{-@ assume neq    :: x:Int -> y:Int -> {v:Bool | ((v) <=> x != y)} @-}+{-@ assume leq    :: x:Int -> y:Int -> {v:Bool | ((v) <=> x <= y)} @-}+{-@ assume geq    :: x:Int -> y:Int -> {v:Bool | ((v) <=> x >= y)} @-}+{-@ assume lt     :: x:Int -> y:Int -> {v:Bool | ((v) <=> x < y)}  @-}+{-@ assume gt     :: x:Int -> y:Int -> {v:Bool | ((v) <=> x > y)}  @-}++{-# NOINLINE plus #-}+plus :: Int -> Int -> Int+plus x y = x + y++{-# NOINLINE minus #-}+minus :: Int -> Int -> Int+minus x y = x - y++{-# NOINLINE times #-}+times :: Int -> Int -> Int+times x y = x * y++-------------------------------------------------------------------+--------------------------- Comparisons ---------------------------+-------------------------------------------------------------------++{-# NOINLINE eq #-}+eq :: Int -> Int -> Bool+eq x y = x == y++{-# NOINLINE neq #-}+neq :: Int -> Int -> Bool+neq x y = not (x == y)++{-# NOINLINE leq #-}+leq :: Int -> Int -> Bool+leq x y = x <= y++{-# NOINLINE geq #-}+geq :: Int -> Int -> Bool+geq x y = x >= y++{-# NOINLINE lt #-}+lt :: Int -> Int -> Bool+lt x y = x < y++{-# NOINLINE gt #-}+gt :: Int -> Int -> Bool+gt x y = x > y++-------------------------------------------------------------------+------------------------ Specifications ---------------------------+-------------------------------------------------------------------+++{-@ ignore liquidAssertB @-}+{-@ assume liquidAssertB :: x:{v:Bool | v} -> {v: Bool | v} @-}+{-# NOINLINE liquidAssertB #-}+liquidAssertB :: Bool -> Bool+liquidAssertB b = b++{-@ assume liquidAssert :: {v:Bool | v} -> a -> a  @-}+{-# NOINLINE liquidAssert #-}+liquidAssert :: Bool -> a -> a+liquidAssert _ x = x++{-@ ignore liquidAssume @-}+{-@ assume liquidAssume :: b:Bool -> a -> {v: a | b}  @-}+{-# NOINLINE liquidAssume #-}+liquidAssume :: Bool -> a -> a+liquidAssume b x = if b then x else error "liquidAssume fails"++{-@ ignore liquidAssumeB @-}+{-@ assume liquidAssumeB :: forall <p :: a -> Bool>. (a<p> -> {v:Bool| v}) -> a -> a<p> @-}+liquidAssumeB :: (a -> Bool) -> a -> a+liquidAssumeB p x | p x = x+                  | otherwise = error "liquidAssumeB fails"+++{-@ ignore unsafeError @-}+{-# NOINLINE unsafeError #-}+unsafeError :: String -> a+unsafeError = error+++{-@ liquidError :: {v:String | 0 = 1} -> a  @-}+{-# NOINLINE liquidError #-}+liquidError :: String -> a+liquidError = error++{-@ assume crash  :: forall a . x:{v:Bool | v} -> a @-}+{-# NOINLINE crash #-}+crash :: Bool -> a+crash = undefined++{-# NOINLINE force #-}+force :: Bool+force = True++{-# NOINLINE choose #-}+choose :: Int -> Int+choose = undefined++-------------------------------------------------------------------+----------- Modular Arithmetic Wrappers ---------------------------+-------------------------------------------------------------------++-- tedium because fixpoint doesn't want to deal with (x mod y) only (x mod c)+{-@ assume isEven :: x:Int -> {v:Bool | ((v) <=> ((x mod 2) = 0))} @-}+{-# NOINLINE isEven #-}+isEven   :: Int -> Bool+isEven x = x `mod` 2 == 0++{-@ assume isOdd :: x:Int -> {v:Bool | ((v) <=> ((x mod 2) = 1))} @-}+{-# NOINLINE isOdd #-}+isOdd   :: Int -> Bool+isOdd x = x `mod` 2 == 1++-----------------------------------------------------------------------------------------------++{-@ 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)} @-}+infixr 8 ==>+(==>) :: Bool -> Bool -> Bool+False ==> False = True+False ==> True  = True+True  ==> True  = True+True  ==> False = False
+ src/Language/Haskell/Liquid/ProofCombinators.hs view
@@ -0,0 +1,183 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE IncoherentInstances   #-}++module Language.Haskell.Liquid.ProofCombinators (++  -- ATTENTION! `Admit` and `(==!)` are UNSAFE: they should not belong the final proof term++  -- * Proof is just a () alias+  Proof+  , toProof ++  -- * Proof constructors+  , trivial, unreachable, (***), QED(..)++  -- * Proof certificate constructors+  , (?)++  -- * 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 ++  -- * This operator does not check intermediate equalities+  , (==.) ++  -- Uncheck operator used only for proof debugging+  , (==!) -- x ==! y always succeeds++  -- * Combining Proofs+  , (&&&)+  , withProof +  , impossible +++) where++-------------------------------------------------------------------------------+-- | Proof is just a () alias -------------------------------------------------+-------------------------------------------------------------------------------++type Proof = ()++toProof :: a -> Proof+toProof _ = ()++-------------------------------------------------------------------------------+-- | Proof Construction -------------------------------------------------------+-------------------------------------------------------------------------------++-- | trivial is proof by SMT++trivial :: Proof+trivial =  ()++-- {-@ unreachable :: {v : Proof | False } @-}+unreachable :: Proof+unreachable =  ()++-- All proof terms are deleted at runtime.+{- RULE "proofs are irrelevant" forall (p :: Proof). p = () #-}++-- | proof casting+-- | `x *** QED`: x is a proof certificate* strong enough for SMT to prove your theorem+-- | `x *** Admit`: x is an unfinished proof++infixl 3 ***+{-@ assume (***) :: a -> p:QED -> { if (isAdmit p) then false else true } @-}+(***) :: a -> QED -> Proof+_ *** _ = ()++data QED = Admit | QED++{-@ measure isAdmit :: QED -> Bool @-}+{-@ Admit :: {v:QED | isAdmit v } @-}+++-------------------------------------------------------------------------------+-- | * Checked Proof Certificates ---------------------------------------------+-------------------------------------------------------------------------------++-- Any (refined) carries proof certificates.+-- For example 42 :: {v:Int | v == 42} is a certificate that+-- the value 42 is equal to 42.+-- But, this certificate will not really be used to proof any fancy theorems.++-- Below we provide a number of equational operations+-- that constuct proof certificates.++-- | Implicit equality++-- x === y returns the proof certificate that+-- result value is equal to both x and y+-- when y == x (as assumed by the operator's precondition)++infixl 3 ===+{-@ (===) :: x:a -> y:{a | y == x} -> {v:a | v == x && v == y} @-}+(===) :: a -> a -> a+_ === y  = y++infixl 3 =<=+{-@ (=<=) :: x:a -> y:{a | x <= y} -> {v:a | v == y} @-}+(=<=) :: a -> a -> a+_ =<= y  = y++infixl 3 =>=+{-@ (=>=) :: x:a -> y:{a | x >= y}  -> {v:a | v == y} @-}+(=>=) :: a -> a -> a+_ =>= y  = y++-------------------------------------------------------------------------------+-- | `?` is basically Haskell's $ and is used for the right precedence+-- | `?` lets you "add" some fact into a proof term+-------------------------------------------------------------------------------++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 `+--   returns the admitted proof certificate that result value is equals x and y+-------------------------------------------------------------------------------++infixl 3 ==!+{-@ assume (==!) :: x:a -> y:a -> {v:a | v == x && v == y} @-}+(==!) :: a -> a -> a+(==!) _ y = y+++-- | To summarize:+--+-- 	- (==!) is *only* for proof debugging+--	- (===) does not require explicit proof term+-- 	- (?)   lets you insert "lemmas" as other `Proof` values++-------------------------------------------------------------------------------+-- | * Unchecked Proof Certificates -------------------------------------------+-------------------------------------------------------------------------------++-- | 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?++infixl 3 ==.++{-# DEPRECATED (==.) "Use (===) instead" #-}++{-# INLINE (==.) #-} +(==.) :: a -> a -> a +_ ==. x = x ++-------------------------------------------------------------------------------+-- | * Combining Proof Certificates -------------------------------------------+-------------------------------------------------------------------------------++(&&&) :: Proof -> Proof -> Proof+x &&& _ = x+++{-@ withProof :: x:a -> b -> {v:a | v = x} @-}+withProof :: a -> b -> a+withProof x _ = x++{-@ impossible :: {v:a | false} -> b @-}+impossible :: a -> b+impossible _ = undefined++-------------------------------------------------------------------------------+-- | Convenient Syntax for Inductive Propositions +-------------------------------------------------------------------------------++{-@ measure prop :: a -> b           @-}+{-@ type Prop E = {v:_ | prop v = E} @-}+++
+ src/Language/Haskell/Liquid/RTick.hs view
@@ -0,0 +1,440 @@++--+-- Liquidate your assets: reasoning about resource usage in Liquid Haskell.+-- Martin A.T. Handley, Niki Vazou, and Graham Hutton.+--++{-@ LIQUID "--reflection" @-}++module Language.Haskell.Liquid.RTick+  (++  -- Tick datatype:+    Tick(..)+  -- Primitive resource operators:+  , fmap+  , pure+  , (<*>)+  , liftA2+  , return+  , (>>=)+  , (=<<)+  , eqBind+  , leqBind+  , geqBind+  , ap+  , liftM+  , liftM2+  -- Resource modifiers:+  , step+  , wait      -- step 1       . return+  , waitN     -- step (n > 0) . return+  , go        -- step (-1)    . return+  , goN       -- step (n < 0) . return+  , wmap      -- step 1       . fmap f+  , wmapN     -- step (n > 0) . fmap f+  , gmap      -- step (-1)    . fmap f+  , gmapN     -- step (n < 0) . fmap f+  , (</>)     -- step 1       . (f <*>)+  , (<//>)    -- step 2       . (f <*>)+  , (<\>)     -- step (-1)    . (f <*>)+  , (<\\>)    -- step (-2)    . (f <*>)+  , (>/=)     -- step 1       . (>>= f)+  , (=/<)     -- step 1       . (>>= f)+  , (>//=)    -- step 2       . (>>= f)+  , (=//<)    -- step 2       . (>>= f)+  , (>\=)     -- step (-1)    . (>>= f)+  , (=\<)     -- step (-1)    . (>>= f)+  , (>\\=)    -- step (-2)    . (>>= f)+  , (=\\<)    -- step (-2)    . (>>= f)+  -- Memoisation:+  , pay+  , zipWithM+++  ) where++import Prelude hiding ( Functor(..), Applicative(..), Monad(..), (=<<) )++import qualified Control.Applicative as A+import qualified Control.Monad       as M+import qualified Data.Functor        as F++--+-- The 'Tick' datatype and its corresponding resource modifiers.+--+-- See 'ResourceModifiers.hs' for proofs that all resource modifiers+-- can be defined using 'return', '(>>=) 'and 'step'.+--++-------------------------------------------------------------------------------+-- | 'Tick' datatype for recording resource usage:+-------------------------------------------------------------------------------++{-@ data Tick a = Tick { tcost :: Int, tval :: a } @-}+data Tick a = Tick { tcost :: Int, tval :: a }++-------------------------------------------------------------------------------+-- | Primitive resource operators:+-------------------------------------------------------------------------------++instance F.Functor Tick where+  fmap = fmap++{-@ reflect fmap @-}+{-@ fmap :: f:(a -> b) -> t1:Tick a+      -> { t:Tick b | Tick (tcost t1) (f (tval t1)) == t }+@-}+fmap :: (a -> b) -> Tick a -> Tick b+fmap f (Tick m x) = Tick m (f x)++instance A.Applicative Tick where+  pure  = pure+  (<*>) = (<*>)++{-@ reflect pure @-}+{-@ pure :: x:a -> { t:Tick a | x == tval t && 0 == tcost t } @-}+pure :: a -> Tick a+pure x = Tick 0 x++{-@ reflect <*> @-}+{-@ (<*>) :: t1:Tick (a -> b) -> t2:Tick a+      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&+                    tcost t1 + tcost t2 == tcost t }+@-}+infixl 4 <*>+(<*>) :: Tick (a -> b) -> Tick a -> Tick b+Tick m f <*> Tick n x = Tick (m + n) (f x)++{-@ reflect liftA2 @-}+{-@ liftA2 :: f:(a -> b -> c) -> t1:Tick a -> t2:Tick b+      -> { t:Tick c | f (tval t1) (tval t2) == tval  t &&+                      tcost t1 + tcost t2 == tcost t }+@-}+liftA2 :: (a -> b -> c) -> Tick a -> Tick b -> Tick c+liftA2 f (Tick m x) (Tick n y) = Tick (m + n) (f x y)++instance M.Monad Tick where+  return = return+  (>>=)  = (>>=)++{-@ reflect return @-}+{-@ return :: x:a -> { t:Tick a | x == tval t && 0 == tcost t } @-}+return :: a -> Tick a+return x = Tick 0 x++{-@ reflect >>= @-}+{-@ (>>=) :: t1:Tick a -> f:(a -> Tick b)+      -> { t:Tick b | tval (f (tval t1))  == tval  t &&+         tcost t1 + tcost (f (tval t1)) == tcost t }+@-}+infixl 4 >>=+(>>=) :: Tick a -> (a -> Tick b) -> Tick b+Tick m x >>= f = let Tick n y = f x in Tick (m + n) y++{-@ reflect =<< @-}+{-@ (=<<) :: f:(a -> Tick b) -> t1:Tick a+      -> { t:Tick b | tval (f (tval t1))  == tval  t &&+         tcost t1 + tcost (f (tval t1)) == tcost t }+@-}+infixl 4 =<<+(=<<) :: (a -> Tick b) -> Tick a -> Tick b+f =<< Tick m x = let Tick n y = f x in Tick (m + n) y++{-@ reflect ap @-}+{-@ ap :: t1:(Tick (a -> b)) -> t2:Tick a+      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&+                    tcost t1 + tcost t2 == tcost t }+@-}+ap :: Tick (a -> b) -> Tick a -> Tick b+ap (Tick m f) (Tick n x) = Tick (m + n) (f x)++{-@ reflect liftM @-}+{-@ liftM :: f:(a -> b) -> t1:Tick a -> { t:Tick b | tcost t1 == tcost t } @-}+liftM :: (a -> b) -> Tick a -> Tick b+liftM f (Tick m x) = Tick m (f x)++{-@ reflect liftM2 @-}+{-@ liftM2 :: f:(a -> b -> c) -> t1:Tick a -> t2:Tick b+      -> { t:Tick c | f (tval t1) (tval t2) == tval  t &&+                      tcost t1 + tcost t2 == tcost t }+@-}+liftM2 :: (a -> b -> c) -> Tick a -> Tick b -> Tick c+liftM2 f (Tick m x) (Tick n y) = Tick (m + n) (f x y)++-------------------------------------------------------------------------------++{-@ reflect eqBind @-}+{-@ eqBind :: n:Int -> t1:Tick a+      -> f:(a -> { tf:Tick b | n == tcost tf })+      -> { t:Tick b | tval (f (tval t1))  == tval  t &&+                           tcost t1 + n == tcost t }+@-}+eqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b+eqBind _ (Tick m x) f = let Tick n y = f x in Tick (m + n) y++{-@ reflect leqBind @-}+{-@ leqBind :: n:Int -> t1:Tick a+      -> f:(a -> { tf:Tick b | n >= tcost tf })+      -> { t:Tick b | tcost t1 + n >= tcost t }+@-}+leqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b+leqBind _ (Tick m x) f = let Tick n y = f x in Tick (m + n) y++{-@ reflect geqBind @-}+{-@ geqBind :: n:Int -> t1:Tick a+      -> f:(a -> { tf:Tick b | n <= tcost tf })+      -> { t2:Tick b | tcost t1 + n <= tcost t2 }+@-}+geqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b+geqBind _ (Tick m x) f = let Tick n y = f x in Tick (m + n) y++-------------------------------------------------------------------------------+-- | Resource modifiers:+-------------------------------------------------------------------------------++{-@ reflect step @-}+{-@ step :: m:Int -> t1:Tick a+      -> { t:Tick a | tval t1 == tval t && m + tcost t1 == tcost t }+@-}+step :: Int -> Tick a -> Tick a+step m (Tick n x) = Tick (m + n) x++--+-- @wait := step 1 . return@.+--+{-@ reflect wait @-}+{-@ wait :: x:a -> { t:Tick a | x == tval t && 1 == tcost t } @-}+wait :: a -> Tick a+wait x = Tick 1 x++--+-- @waitN (n > 0) := step n . return@.+--+{-@ reflect waitN @-}+{-@ waitN :: n:Nat -> x:a+      -> { t:Tick a | x == tval t && n == tcost t }+@-}+waitN :: Int -> a -> Tick a+waitN n x = Tick n x++--+-- @go := step (-1) . return@.+--+{-@ reflect go @-}+{-@ go :: x:a -> { t:Tick a | x == tval t && (-1) == tcost t } @-}+go :: a -> Tick a+go x = Tick (-1) x++--+-- @goN (n > 0) := step (-n) . return@.+--+{-@ reflect goN @-}+{-@ goN :: { n:Nat | n > 0 } -> x:a+      -> { t:Tick a | x == tval t && (-n) == tcost t }+@-}+goN :: Int -> a -> Tick a+goN n x = Tick (-n) x++--+-- @wmap f := step 1 . fmap f@.+--+{-@ reflect wmap @-}+{-@ wmap :: f:(a -> b) -> t1:Tick a+      -> { t:Tick b | Tick (1 + tcost t1) (f (tval t1)) == t }+@-}+wmap :: (a -> b) -> Tick a -> Tick b+wmap f (Tick m x) = Tick (1 + m) (f x)++--+-- @wmapN (n > 0) f := step n . fmap f@.+--+{-@ reflect wmapN @-}+{-@ wmapN :: { m:Nat | m > 0 } -> f:(a -> b) -> t1:Tick a+      -> { t:Tick b | Tick (m + tcost t1) (f (tval t1)) == t }+@-}+wmapN :: Int -> (a -> b) -> Tick a -> Tick b+wmapN m f (Tick n x) = Tick (m + n) (f x)++--+-- @gmap f := step (-1) . fmap f@.+--+{-@ reflect gmap @-}+{-@ gmap :: f:(a -> b) -> t1:Tick a+      -> { t:Tick b | Tick (tcost t1 - 1) (f (tval t1)) == t }+@-}+gmap :: (a -> b) -> Tick a -> Tick b+gmap f (Tick m x) = Tick (m - 1) (f x)++--+-- @gmapN (n > 0) f := step (-n) . fmap f@.+--+{-@ reflect gmapN @-}+{-@ gmapN :: { m:Nat | m > 0 } -> f:(a -> b) -> t1:Tick a+      -> { t:Tick b | Tick (tcost t1 - m) (f (tval t1)) == t }+@-}+gmapN :: Int -> (a -> b) -> Tick a -> Tick b+gmapN m f (Tick n x) = Tick (n - m) (f x)++--+-- \"wapp\": @(f </>) := step 1 . (f <*>)@.+--+{-@ reflect </> @-}+{-@ (</>) :: t1:(Tick (a -> b)) -> t2:Tick a+      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&+                1 + tcost t1 + tcost t2 == tcost t }+@-}+infixl 4 </>+(</>) :: Tick (a -> b) -> Tick a -> Tick b+Tick m f </> Tick n x = Tick (1 + m + n) (f x)++--+-- \"wwapp\": @(f <//>) := step 2 . (f <*>)@.+--+{-@ reflect <//> @-}+{-@ (<//>) :: t1:(Tick (a -> b)) -> t2:Tick a+      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&+                2 + tcost t1 + tcost t2 == tcost t }+@-}+infixl 4 <//>+(<//>) :: Tick (a -> b) -> Tick a -> Tick b+Tick m f <//> Tick n x = Tick (2 + m + n) (f x)++--+-- \"gapp\": @(f <\>) := step (-1) . (f <*>)@.+--+{-@ reflect <\> @-}+{-@ (<\>) :: t1:(Tick (a -> b)) -> t2:Tick a+      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&+                tcost t1 + tcost t2 - 1 == tcost t }+@-}+infixl 4 <\>+(<\>) :: Tick (a -> b) -> Tick a -> Tick b+Tick m f <\> Tick n x = Tick (m + n - 1) (f x)++--+-- \"ggapp\": @(f <\\>) := step (-2) . (f <*>)@.+--+{-@ reflect <\\> @-}+{-@ (<\\>) :: t1:(Tick (a -> b)) -> t2:Tick a+      -> { t:Tick b | (tval t1) (tval t2) == tval  t &&+                tcost t1 + tcost t2 - 2 == tcost t }+@-}+infixl 4 <\\>+(<\\>) :: Tick (a -> b) -> Tick a -> Tick b+Tick m f <\\> Tick n x = Tick (m + n - 2) (f x)++--+-- \"wbind\": @(>/= f) := step 1 . (>>= f)@.+--+{-@ reflect >/= @-}+{-@ (>/=) :: t1:Tick a -> f:(a -> Tick b)+      -> { t:Tick b | (tval (f (tval t1))      == tval  t) &&+         (1 + tcost t1 + tcost (f (tval t1))) == tcost t }+@-}+infixl 4 >/=+(>/=) :: Tick a -> (a -> Tick b) -> Tick b+Tick m x >/= f = let Tick n y = f x in Tick (1 + m + n) y++--+-- \"wbind\": @(f =/<) := step 1 . (f =<<)@.+--+{-@ reflect =/< @-}+{-@ (=/<) :: f:(a -> Tick b) -> t1:Tick a+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         1 + tcost t1 + tcost (f (tval t1)) == tcost t }+@-}+infixl 4 =/<+(=/<) :: (a -> Tick b) -> Tick a -> Tick b+f =/< Tick m x = let Tick n y = f x in Tick (1 + m + n) y++--+-- \"wwbind\": @(>//= f) := step 2 . (>>= f)@.+--+{-@ reflect >//= @-}+{-@ (>//=) :: t1:Tick a -> f:(a -> Tick b)+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         2 + tcost t1 + tcost (f (tval t1)) == tcost t }+@-}+infixl 4 >//=+(>//=) :: Tick a -> (a -> Tick b) -> Tick b+Tick m x >//= f = let Tick n y = f x in Tick (2 + m + n) y++--+-- \"wwbind\": @(f =//<) := step 2 . (f =<<)@.+--+{-@ reflect =//< @-}+{-@ (=//<) :: f:(a -> Tick b) -> t1:Tick a+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         2 + tcost t1 + tcost (f (tval t1)) == tcost t }+@-}+infixl 4 =//<+(=//<) :: (a -> Tick b) -> Tick a -> Tick b+f =//< Tick m x = let Tick n y = f x in Tick (2 + m + n) y++--+-- \"gbind\": @(>\= f) := step (-1) . (>>= f)@.+--+{-@ reflect >\= @-}+{-@ (>\=) :: t1:Tick a -> f:(a -> Tick b)+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         tcost t1 + tcost (f (tval t1)) - 1 == tcost t }+@-}+infixl 4 >\=+(>\=) :: Tick a -> (a -> Tick b) -> Tick b+Tick m x >\= f = let Tick n y = f x in Tick (m + n - 1) y++--+-- \"gbind\": @(f =\<) := step (-1) . (f =<<)@.+--+{-@ reflect =\< @-}+{-@ (=\<) :: f:(a -> Tick b) -> t1:Tick a+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         tcost t1 + tcost (f (tval t1)) - 1 == tcost t }+@-}+infixl 4 =\<+(=\<) :: (a -> Tick b) -> Tick a -> Tick b+f =\< Tick m x = let Tick n y = f x in Tick (m + n - 1) y++--+-- \"ggbind\": @(>\= f) := step (-2) . (>>= f)@.+--+{-@ reflect >\\= @-}+{-@ (>\\=) :: t1:Tick a -> f:(a -> Tick b)+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         tcost t1 + tcost (f (tval t1)) - 2 == tcost t }+@-}+infixl 4 >\\=+(>\\=) :: Tick a -> (a -> Tick b) -> Tick b+Tick m x >\\= f = let Tick n y = f x in Tick (m + n - 2) y++--+-- \"ggbind\": @(f =\\<) := step (-2) . (f =<<)@.+--+{-@ reflect =\\< @-}+{-@ (=\\<) :: f:(a -> Tick b) -> t1:Tick a+      -> { t:Tick b | tval (f (tval t1))      == tval  t &&+         tcost t1 + tcost (f (tval t1)) - 2 == tcost t }+@-}+infixl 4 =\\<+(=\\<) :: (a -> Tick b) -> Tick a -> Tick b+f =\\< Tick m x = let Tick n y = f x in Tick (m + n - 2) y++-------------------------------------------------------------------------------+-- | Memoisation:+-------------------------------------------------------------------------------++{-@ reflect pay @-}+{-@ pay :: m:Int+      -> { t1:Tick a | m <= tcost t1 }+      -> { t:Tick ({ t2 : Tick a | tcost t1 - m == tcost t2 }) | m == tcost t }+@-}+pay :: Int -> Tick a -> Tick (Tick a)+pay m (Tick n x) = Tick m (Tick (n - m) x)+++{-@ reflect zipWithM @-}+{-@ zipWithM :: f:(a -> b -> Tick c) -> x:Tick a -> y:Tick b+      -> {t:Tick c | tcost t == tcost x + tcost y + tcost (f (tval x) (tval y))} @-}+zipWithM :: (a -> b -> Tick c) -> Tick a -> Tick b -> Tick c+zipWithM f (Tick c1 x1) (Tick c2 x2) = let Tick c x = f x1 x2 in Tick (c + c1 + c2) x
+ src/Language/Haskell/Liquid/RTick/Combinators.hs view
@@ -0,0 +1,366 @@++--+-- Liquidate your assets: reasoning about resource usage in Liquid Haskell.+--++{-@ LIQUID "--reflection" @-}++module Language.Haskell.Liquid.RTick.Combinators+  (++  -- Basic:+    Proof         -- Simply the unit type.+  , QED(..)       -- 'ASS': Signify the end of an /unfinished/ proof.+                  -- 'QED': Signify the end of a /complete/ proof.+  , (&&&)         -- Combine proofs.+  , (***)         -- Discard final result at the end of a proof.+  , (?)           -- Appeal to an external theorem.+  , isAss         -- Check whether a proof is complete.+  , toProof       -- Cast to proof.+  , trivial       -- Trivial proof.+  , withTheorem   -- Appeal to an external theorem.+  -- Equational:+  , (==.)         -- Equality.+  , (==?)         -- Equality (assumption).+  , eq            -- Equality. Note: 'eq' is inlined in the logic.+  -- Inequational:+  , (<.)          -- Less than.+  , (<?)          -- Less than (assumption).+  , (<=.)         -- Less than or equal.+  , (<=?)         -- Less than or equal (assumption).+  , (>.)          -- Greater than.+  , (>?)          -- Greater than (assumption).+  , (>=.)         -- Greater than or equal.+  , (>=?)         -- Greater than or equal (assumption).+  , (<=>.)        -- Cost equivalence.+  , (<=>?)        -- Cost equivalence (assumption)+  , (>~>.)        -- Improvement.+  , (>~>?)        -- Improvement (assumption).+  , (.>==)        -- Quantified improvement.+  , (?>==)        -- Quantified improvement (assumption).+  , (<~<.)        -- Diminishment.+  , (<~<?)        -- Diminishment (assumption).+  , (.<==)        -- Quantified diminishment.+  , (?<==)        -- Quantified diminishment (assumption).+  -- Cost separators:+  , (==>.)        -- Quantified improvement.+  , (==>?)        -- Quantified improvement (assumption).+  , (==<.)        -- Quantified diminishment.+  , (==<?)        -- Quantified diminishment (assumption).+  , (==!)+  , assert+  ) where++import Language.Haskell.Liquid.RTick ( Tick(..) )++--+-- Proof combinators for extrinsic cost analysis.+--++-------------------------------------------------------------------------------+-- | Basic:+-------------------------------------------------------------------------------++{-@ assert :: b:{Bool | b} -> {b} @-}+assert :: Bool -> Proof+assert _ = ()++-- unchecked+(==!) :: a -> a -> a+_ ==! x = x+++type Proof = ()+data QED   = QED | ASS++{-@ toProof :: a -> Proof @-}+toProof :: a -> Proof+toProof _ = ()+{-# INLINE toProof #-}++{-@ trivial :: Proof @-}+trivial :: Proof+trivial = ()+{-# INLINE trivial #-}++{-@ measure isAss @-}+isAss :: QED -> Bool+isAss ASS = True+isAss QED = False++{-@ assume (***) :: a -> qed:QED -> { if (isAss qed) then false else true } @-}+infixl 1 ***+(***) :: a -> QED -> Proof+_ *** _ = ()+{-# INLINE (***) #-}++{-@ (?) :: x:a -> Proof -> { v:a | x == v } @-}+infixl 3 ?+(?) :: a -> Proof -> a+x ? _ = x+{-# INLINE (?) #-}++{-@ (&&&) :: Proof -> Proof -> Proof @-}+infixl 3 &&&+(&&&) :: Proof -> Proof -> Proof+x &&& _ = x+{-# INLINE (&&&) #-}++{-@ withTheorem :: x:a -> Proof -> { v:a | x == v } @-}+withTheorem :: a -> Proof -> a+withTheorem x _ = x+{-# INLINE withTheorem #-}++-------------------------------------------------------------------------------+-- | Equational:+-------------------------------------------------------------------------------++--+-- Equality.+--+{-@ (==.) :: x:a -> { y:a | x == y } -> { v:a | x == v && y == v } @-}+infixl 3 ==.+(==.) :: a -> a -> a+_ ==. x = x+{-# INLINE (==.) #-}++{-@ assume (==?) :: x:a -> y:a -> { v:a | x == v && y == v } @-}+infixl 3 ==?+(==?) :: a -> a -> a+_ ==? x = x+{-# INLINE (==?) #-}++--+-- Equality. Note: 'eq' is inlined in the logic, so can be used in+-- reflected functions.+--+{-@ eq :: x:a -> { y:a | x == y } -> { v:a | x == v && y == v } @-}+eq :: a -> a -> a+_ `eq` x = x+{-# INLINE eq #-}++-------------------------------------------------------------------------------+-- | Inequational:+-------------------------------------------------------------------------------++--+-- Less than.+--+{-@ (<.) :: m:a -> { n:a | m < n } -> { o:a | o == n } @-}+infixl 3 <.+(<.) :: a -> a -> a+_ <. n = n+{-# INLINE (<.) #-}++{-@ assume (<?) :: m:a -> n:a -> { o:a | o == n && m < n } @-}+infixl 3 <?+(<?) :: a -> a -> a+_ <? n = n+{-# INLINE (<?) #-}++--+-- Less than or equal.+--+{-@ (<=.) :: m:a -> { n:a | m <= n } -> { o:a | o == n } @-}+infixl 3 <=.+(<=.) :: a -> a -> a+_ <=. n = n+{-# INLINE (<=.) #-}++{-@ assume (<=?) :: m:a -> n:a -> { o:a | o == n && m <= n } @-}+infixl 3 <=?+(<=?) :: a -> a -> a+_ <=? n = n+{-# INLINE (<=?) #-}++--+-- Greater than.+--+{-@ (>.) :: m:a -> { n:a | m > n } -> { o:a | o == n } @-}+infixl 3 >.+(>.) :: a -> a -> a+_ >. y = y+{-# INLINE (>.) #-}++{-@ assume (>?) :: m:a -> n:a -> { o:a | o == n && m > n } @-}+infixl 3 >?+(>?) :: a -> a -> a+_ >? y = y+{-# INLINE (>?) #-}++--+-- Greater than or equal.+--+{-@ (>=.) :: m:a -> { n:a | m >= n } -> { o:a | o == n } @-}+infixl 3 >=.+(>=.) :: a -> a -> a+_ >=. n = n+{-# INLINE (>=.) #-}++{-@ assume (>=?) :: m:a -> n:a -> { o:a | o == n && m >= n } @-}+infixl 3 >=?+(>=?) :: a -> a -> a+_ >=? n = n+{-# INLINE (>=?) #-}++--+-- Cost equivalence.+--+{-@ predicate COSTEQ T1 T2 = tval T1 == tval T2 && tcost T1 == tcost T2 @-}++{-@ (<=>.)+      :: t1:Tick a+      -> { t2:Tick a | COSTEQ t1 t2 }+      -> { t3:Tick a | COSTEQ t1 t2 && COSTEQ t1 t3 && COSTEQ t2 t3 }+@-}+infixl 3 <=>.+(<=>.) :: Tick a -> Tick a -> Tick a+(<=>.) _ t2 = t2+{-# INLINE (<=>.) #-}++{-@ assume (<=>?)+      :: t1:Tick a -> t2:Tick a+      -> { t3:Tick a | COSTEQ t1 t2 && COSTEQ t1 t3 && t2 == t3 }+@-}+infixl 3 <=>?+(<=>?) :: Tick a -> Tick a -> Tick a+(<=>?) _ t2 = t2+{-# INLINE (<=>?) #-}++--+-- Improvement.+--+{-@ predicate IMP T1 T2 = tval T1 == tval T2 && tcost T1 >= tcost T2 @-}++{-@ (>~>.)+      :: t1:Tick a+      -> { t2:Tick a | IMP t1 t2 }+      -> { t3:Tick a | IMP t1 t2 && IMP t1 t3 && t2 == t3 }+@-}+infixl 3 >~>.+(>~>.) :: Tick a -> Tick a -> Tick a+(>~>.) _ t2 = t2+{-# INLINE (>~>.) #-}++{-@ assume (>~>?)+      :: t1:Tick a -> t2:Tick a+      -> { t3:Tick a | IMP t1 t2 && IMP t1 t3 && t2 == t3 }+@-}+infixl 3 >~>?+(>~>?) :: Tick a -> Tick a -> Tick a+(>~>?) _ t2 = t2+{-# INLINE (>~>?) #-}++--+-- Quantified improvement.+--+{-@ predicate QIMP T1 N T2 = tval T1 == tval T2 && tcost T1 == tcost T2 + N @-}++{-@ (.>==)+      :: t1:Tick a+      -> n:Int+      -> { t2:Tick a | QIMP t1 n t2 }+      -> { t3:Tick a | QIMP t1 n t2 && QIMP t1 n t3 && t2 == t3 }+@-}+infixl 3 .>==+(.>==) :: Tick a -> Int -> Tick a -> Tick a+(.>==) _ _ t2 = t2+{-# INLINE (.>==) #-}++{-@ assume (?>==)+     :: t1:Tick a -> n:Nat -> t2:Tick a+     -> { t3:Tick a | QIMP t1 n t2 && QIMP t1 n t3 && t2 == t3 }+@-}+infixl 3 ?>==+(?>==) :: Tick a -> Int -> Tick a -> Tick a+(?>==) _ _ t2 = t2+{-# INLINE (?>==) #-}++--+-- Diminishment.+--+{-@ predicate DIM T1 T2 = tval T1 == tval T2 && tcost T1 <= tcost T2 @-}++{-@ (<~<.)+      :: t1:Tick a+      -> { t2:Tick a | DIM t1 t2 }+      -> { t3:Tick a | DIM t1 t2 && DIM t1 t3 && t2 == t3 }+@-}+infixl 3 <~<.+(<~<.) :: Tick a -> Tick a -> Tick a+(<~<.) _ t2 = t2+{-# INLINE (<~<.) #-}++{-@ assume (<~<?)+     :: t1:Tick a -> t2:Tick a+     -> { t3:Tick a | DIM t1 t2 && DIM t1 t3 && t2 == t3 }+@-}+infixl 3 <~<?+(<~<?) :: Tick a -> Tick a -> Tick a+(<~<?) _ t2 = t2+{-# INLINE (<~<?) #-}++--+-- Quantified diminishment.+--+{-@ predicate QDIM T1 N T2 = tval T1 == tval T2 && tcost T1 + N == tcost T2 @-}++{-@ (.<==)+      :: t1:Tick a+      -> n:Nat+      -> { t2:Tick a | QDIM t1 n t2 }+      -> { t3:Tick a | QDIM t1 n t2 && QDIM t1 n t3 && t2 == t3 }+@-}+infixl 3 .<==+(.<==) :: Tick a -> Int -> Tick a -> Tick a+(.<==) _ _ t2 = t2+{-# INLINE (.<==) #-}++{-@ assume (?<==)+      :: t1:Tick a -> n:Nat -> t2:Tick a+      -> { t3:Tick a | QDIM t1 n t2 && QDIM t1 n t3 && t2 == t3 }+@-}+infixl 3 ?<==+(?<==) :: Tick a -> Int -> Tick a -> Tick a+(?<==) _ _ t2 = t2+{-# INLINE (?<==) #-}++-------------------------------------------------------------------------------+-- | Cost separators:+-------------------------------------------------------------------------------++--+-- Quantified improvement.+--+{-@ (==>.) :: (a -> b) -> a -> b @-}+infixl 3 ==>.+(==>.) :: (a -> b) -> a -> b+f ==>. a = f a+{-# INLINE (==>.) #-}++--+-- Quantified improvement (assumption).+--+{-@ (==>?) :: (a -> b) -> a -> b @-}+infixl 3 ==>?+(==>?) :: (a -> b) -> a -> b+f ==>? a = f a+{-# INLINE (==>?) #-}++--+-- Quantified diminishment.+--+{-@ (==<.) :: (a -> b) -> a -> b @-}+infixl 3 ==<.+(==<.) :: (a -> b) -> a -> b+f ==<. a = f a+{-# INLINE (==<.) #-}++--+-- Quantified diminishment (assumption).+--+{-@ (==<?) :: (a -> b) -> a -> b @-}+infixl 3 ==<?+(==<?) :: (a -> b) -> a -> b+f ==<? a = f a+{-# INLINE (==<?) #-}
+ src/Language/Haskell/Liquid/String.hs view
@@ -0,0 +1,62 @@+-- Support for Strings for SMT ++{-# LANGUAGE OverloadedStrings   #-}++module Language.Haskell.Liquid.String where++import qualified Data.ByteString as BS+import qualified Data.String     as ST++{-@ embed SMTString as Str @-}++data SMTString = S BS.ByteString +  deriving (Eq, Show)++{-@ invariant {s:SMTString | 0 <= stringLen s } @-}++{-@ measure stringEmp    :: SMTString @-}+{-@ measure stringLen    :: SMTString -> Int @-}+{-@ measure subString    :: SMTString -> Int -> Int -> SMTString @-}+{-@ measure concatString :: SMTString -> SMTString -> SMTString @-}+{-@ measure fromString   :: String -> SMTString @-}+{-@ measure takeString   :: Int -> SMTString -> SMTString @-}+{-@ measure dropString   :: Int -> SMTString -> 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)++{-@ assume stringEmp :: {v:SMTString | v == stringEmp  && stringLen v == 0 } @-}+stringEmp :: SMTString+stringEmp = S (BS.empty)++stringLen :: SMTString -> Int  +{-@ assume stringLen :: x:SMTString -> {v:Nat | v == stringLen x} @-}+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) +++{-@ 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 } @-} +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 +++{-@ 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 view
@@ -0,0 +1,5 @@+module Language.Haskell.Liquid.Synthesize.Error where ++{-@ err :: { v: Int | false } -> a @-}+err :: Int -> a+err s = undefined