diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,6 @@ +module Main where + +import Language.Haskell.Liquid.Cabal (liquidHaskellMain) + +main :: IO () +main = liquidHaskellMain diff --git a/liquid-prelude.cabal b/liquid-prelude.cabal new file mode 100644 --- /dev/null +++ b/liquid-prelude.cabal @@ -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 +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 diff --git a/src/KMeansHelper.hs b/src/KMeansHelper.hs new file mode 100644 --- /dev/null +++ b/src/KMeansHelper.hs @@ -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" + diff --git a/src/Language/Haskell/Liquid/Bag.hs b/src/Language/Haskell/Liquid/Bag.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/Bag.hs @@ -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 _ = () diff --git a/src/Language/Haskell/Liquid/Equational.hs b/src/Language/Haskell/Liquid/Equational.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/Equational.hs @@ -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 Bool>. a -> b -> a @-} +(?) :: a -> b -> a +x ? _ = x +{-# INLINE (?) #-} + +------------------------------------------------------------------------------- +-- | Using proofs as theorems +------------------------------------------------------------------------------- + +withTheorem :: a -> Proof -> a +withTheorem z _ = z diff --git a/src/Language/Haskell/Liquid/Foreign.hs b/src/Language/Haskell/Liquid/Foreign.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/Foreign.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/List.hs b/src/Language/Haskell/Liquid/List.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/List.hs @@ -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]) diff --git a/src/Language/Haskell/Liquid/Prelude.hs b/src/Language/Haskell/Liquid/Prelude.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/Prelude.hs @@ -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

Bool>. (a

-> {v:Bool| v}) -> a -> a

@-} +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 diff --git a/src/Language/Haskell/Liquid/ProofCombinators.hs b/src/Language/Haskell/Liquid/ProofCombinators.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/ProofCombinators.hs @@ -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 Bool, pb :: b -> Bool>. a -> b -> a @-} +(?) :: 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} @-} + + + diff --git a/src/Language/Haskell/Liquid/RTick.hs b/src/Language/Haskell/Liquid/RTick.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/RTick.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/RTick/Combinators.hs b/src/Language/Haskell/Liquid/RTick/Combinators.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/RTick/Combinators.hs @@ -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. + , (.) -- 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. + , (<~.) -- Quantified improvement. + , (==>?) -- Quantified improvement (assumption). + , (==<.) -- Quantified diminishment. + , (== {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 ( n:a -> { o:a | o == n && m < n } @-} +infixl 3 a -> 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 (<~ t2:Tick a + -> { t3:Tick a | DIM t1 t2 && DIM t1 t3 && t2 == t3 } +@-} +infixl 3 <~ Tick a -> 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). +-- +{-@ (== b) -> a -> b @-} +infixl 3 == b) -> a -> b +f == 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 diff --git a/src/Language/Haskell/Liquid/Synthesize/Error.hs b/src/Language/Haskell/Liquid/Synthesize/Error.hs new file mode 100644 --- /dev/null +++ b/src/Language/Haskell/Liquid/Synthesize/Error.hs @@ -0,0 +1,5 @@ +module Language.Haskell.Liquid.Synthesize.Error where + +{-@ err :: { v: Int | false } -> a @-} +err :: Int -> a +err s = undefined