From 3025c3def10a464c6c8d94f78fcc6c334302e4f7 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jun 2015 14:15:56 -0700 Subject: [PATCH 01/23] blerg --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 39bf6b88df..1409d21672 100644 --- a/Makefile +++ b/Makefile @@ -66,8 +66,8 @@ test: # $(CABAL) exec $(TASTY) -- --smtsolver $(SMTSOLVER) --liquid-opts='$(LIQUIDOPTS)' --hide-successes --rerun-update -p 'Unit/' -j$(THREADS) +RTS -N$(THREADS) -RTS test710: - $(CABAL) configure -fdevel --enable-tests --disable-library-profiling -O2 - $(CABAL) build + # $(CABAL) configure -fdevel --enable-tests --disable-library-profiling -O2 + # $(CABAL) build $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -p 'Unit/' -j$(THREADS) +RTS -N$(THREADS) -RTS From 968e1948aab804baa8a9468b0865e96c41027fd8 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jun 2015 18:48:40 -0700 Subject: [PATCH 02/23] update icfp15 benchmarks to ghc 710 --- Makefile | 11 ++ benchmarks/icfp15/neg/DBMovies.hs | 60 ++++---- benchmarks/icfp15/neg/DataBase.hs | 136 ++++++++--------- benchmarks/icfp15/neg/RIO.hs | 35 +++-- benchmarks/icfp15/pos/DBMovies.hs | 65 ++++----- benchmarks/icfp15/pos/DataBase.hs | 138 +++++++++--------- benchmarks/icfp15/pos/RIO.hs | 10 ++ benchmarks/icfp15/pos/RIO2.hs | 13 +- .../Haskell/Liquid/Constraint/Generate.hs | 78 +++++----- 9 files changed, 298 insertions(+), 248 deletions(-) diff --git a/Makefile b/Makefile index 1409d21672..4658bc6629 100644 --- a/Makefile +++ b/Makefile @@ -81,11 +81,22 @@ all-test: cabal build cabal exec $(TASTY) -- --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS +all-test-710: + cabal configure -fdevel --enable-tests --disable-library-profiling -O2 + cabal build + $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS + + all-retest: cabal configure -fdevel --enable-tests --disable-library-profiling -O2 cabal build cabal exec $(TASTY) -- --smtsolver $(SMTSOLVER) --hide-successes --rerun-filter "exceptions,failures,new" --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS +all-retest-710: + $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-filter "exceptions,failures,new" --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS + + + lint: hlint --colour --report . diff --git a/benchmarks/icfp15/neg/DBMovies.hs b/benchmarks/icfp15/neg/DBMovies.hs index 602ed09c19..1f2f0acea2 100644 --- a/benchmarks/icfp15/neg/DBMovies.hs +++ b/benchmarks/icfp15/neg/DBMovies.hs @@ -6,18 +6,18 @@ import GHC.CString -- This import interprets Strings as constants! import Data.Maybe (catMaybes) -import Prelude hiding (product) +import Prelude hiding (product, elem) import Control.Applicative ((<$>)) -type Tag = String +type Tag = String -data Value = I Int | S Name +data Value = I Int | S Name deriving (Show, Eq) -data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames - | Paronnaud | Almadovar | Haneke +data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames + | Paronnaud | Almadovar | Haneke deriving (Show, Eq) {-@ type Movies = [MovieScheme] @-} @@ -32,28 +32,28 @@ data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames {-@ type DirStarScheme = {v:Dict <{\t val -> DirStarRange t val}> Tag Value | ValidDirStarScheme v} @-} -{-@ predicate ValidMovieScheme V = - ((listElts (ddom V) ~~ Set_cup (Set_sng "year") - (Set_cup (Set_sng "star") - (Set_cup (Set_sng "director") +{-@ predicate ValidMovieScheme V = + ((listElts (ddom V) ~~ Set_cup (Set_sng "year") + (Set_cup (Set_sng "star") + (Set_cup (Set_sng "director") (Set_sng "title"))))) @-} -{-@ predicate MovieRange T V = (T ~~ "year" => ValidYear V) - && (T ~~ "star" => ValidStar V) - && (T ~~ "director" => ValidDirector V) +{-@ predicate MovieRange T V = (T ~~ "year" => ValidYear V) + && (T ~~ "star" => ValidStar V) + && (T ~~ "director" => ValidDirector V) && (T ~~ "title" => ValidTitle V) @-} -{-@ predicate ValidDirectorScheme V = (listElts (ddom V) ~~ (Set_sng "director")) @-} +{-@ predicate ValidDirectorScheme V = (listElts (ddom V) ~~ (Set_sng "director")) @-} {-@ predicate DirectorRange T V = (T ~~ "director" => ValidDirector V) @-} -{-@ predicate ValidStarScheme V = (listElts (ddom V) ~~ (Set_sng "star")) @-} +{-@ predicate ValidStarScheme V = (listElts (ddom V) ~~ (Set_sng "star")) @-} {-@ predicate StarRange T V = (T ~~ "star" => ValidStar V) @-} -{-@ predicate ValidTitleScheme V = (listElts (ddom V) ~~ (Set_sng "title")) @-} +{-@ predicate ValidTitleScheme V = (listElts (ddom V) ~~ (Set_sng "title")) @-} {-@ predicate TitleDomain T = (T ~~ "title") @-} {-@ predicate TitleRange T V = (T ~~ "title" => ValidTitle V) @-} -{-@ predicate ValidDirStarScheme V = (listElts (ddom V) ~~ Set_cup (Set_sng "director") (Set_sng "star")) @-} +{-@ predicate ValidDirStarScheme V = (listElts (ddom V) ~~ Set_cup (Set_sng "director") (Set_sng "star")) @-} {-@ predicate DirStarDomain T = (T ~~ "director" || T ~~ "star") @-} {-@ predicate DirStarRange T V = (T ~~ "director" => ValidDirector V) && (T ~~ "star" => ValidStar V) @-} @@ -66,38 +66,38 @@ data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames -type Movies = Table Tag Value -type Titles = Table Tag Value +type Movies = Table Tag Value +type Titles = Table Tag Value type Directors = Table Tag Value type Stars = Table Tag Value type DirStars = Table Tag Value type MovieScheme = Dict Tag Value -movies :: Movies +movies :: Movies {-@ movies :: Movies @-} movies = fromList [movie1, movie2, movie3, movie4] movie1, movie2, movie3, movie4 :: MovieScheme {-@ movie1, movie2, movie3, movie4 :: MovieScheme @-} -movie1 = mkMovie (S TalkToHer) (S Almadovar) (I 8) (I 2002) +movie1 = mkMovie (S TalkToHer) (S Almadovar) (I 8) (I 2002) movie2 = mkMovie (S ChickenPlums) (S Paronnaud) (I 7) (I 2011) movie3 = mkMovie (S Persepolis) (S Paronnaud) (I 8) (I 2007) -movie4 = mkMovie (S FunnyGames) (S Haneke) (I 7) (I 2007) +movie4 = mkMovie (S FunnyGames) (S Haneke) (I 7) (I 2007) mkMovie :: Value -> Value -> Value -> Value -> MovieScheme -{-@ mkMovie :: {t:Value | ValidTitle t} +{-@ mkMovie :: {t:Value | ValidTitle t} -> {d:Value | ValidDirector d} -> {s:Value | ValidStar s} -> {y:Value | ValidYear y} -> MovieScheme - @-} + @-} mkMovie t d s y = ("title" := t) += ("star" := s) += ("director" := d) += ("year" := y) += empty seen :: Titles {-@ seen :: Titles @-} seen = [t1, t2] - where + where t1 = ("title" := S ChickenPlums) += empty t2 = ("title" := S FunnyGames) += empty @@ -126,15 +126,15 @@ good_stars :: Stars -- This _IS_ unsafe! good_directors = directors `diff` not_good_directors -not_good_directors :: DirStars +not_good_directors :: DirStars {-@ not_good_directors :: DirStars @-} --- not_good_directors = project ["director", "star"] movies `diff` product directors good_stars +-- not_good_directors = project ["director", "star"] movies `diff` product directors good_stars - --- This _IS_ unsafe! + +-- This _IS_ unsafe! not_good_directors = project ["director", "star"] movies `diff` product directors movies -good_stars = mk_star_table (I 8) `union` mk_star_table (I 9) `union` mk_star_table (I 10) +good_stars = mk_star_table (I 8) `union` mk_star_table (I 9) `union` mk_star_table (I 10) mk_star_table :: Value -> Stars {-@ mk_star_table :: {s:Value | ValidStar s} -> Stars @-} @@ -146,7 +146,7 @@ mk_star_table s = [("star" := s) += empty] ------------------------------------------------------------------------------- -{-@ measure toInt :: Value -> Int +{-@ measure toInt :: Value -> Int toInt(I n) = n @-} diff --git a/benchmarks/icfp15/neg/DataBase.hs b/benchmarks/icfp15/neg/DataBase.hs index 9863b9de67..ac1334aca2 100644 --- a/benchmarks/icfp15/neg/DataBase.hs +++ b/benchmarks/icfp15/neg/DataBase.hs @@ -1,135 +1,135 @@ module DataBase ( - Table, Dict, (+=), P(..), values, empty, + Table, Dict, (+=), P(..), values, empty, - emptyTable, singleton, fromList, + emptyTable, singleton, fromList, elem, union, diff, product, project, select, productD ) where -import qualified Data.Set as Set -import Prelude hiding (product, union, filter) +import qualified Data.Set as Set +import Prelude hiding (product, union, filter, elem) {-@ LIQUID "--no-termination" @-} {-@ LIQUID "totality" @-} type Table t v = [Dict t v] -data Dict key val = D {ddom :: [key], dfun :: key -> val} -{-@ ddom :: forall val -> Prop>. +data Dict key val = D {ddom :: [key], dfun :: key -> val} +{-@ ddom :: forall val -> Prop>. x:Dict key val -> {v:[key] | v = ddom x} @-} -{-@ dfun :: forall val -> Prop>. - x:Dict key val - -> i:{v:key | Set_mem v (listElts (ddom x))} -> val +{-@ dfun :: forall val -> Prop>. + x:Dict key val + -> i:{v:key | Set_mem v (listElts (ddom x))} -> val @-} {-@ data Dict key val val -> Prop> = D ( ddom :: [key]) - ( dfun :: i:{v:key | Set_mem v (listElts ddom)} -> val) - @-} + ( dfun :: i:{v:key | Set_mem v (listElts ddom)} -> val) + @-} instance (Show t, Show v, Eq t) => Show (Dict t v) where - show (D ks f) = let f k = show k ++ "\t:=\t" ++ show (f k) ++ "\n" - in concatMap f ks + show (D ks f) = let f k = show k ++ "\t:=\t" ++ show (f k) ++ "\n" + in concatMap f ks --- LIQUID : This discards the refinement of the Dict +-- LIQUID : This discards the refinement of the Dict -- for example the ddom -{-@ fromList :: forall val -> Prop, p :: Dict key val -> Prop>. +{-@ fromList :: forall val -> Prop, p :: Dict key val -> Prop>. x:[Dict key val <

>] -> {v:[Dict key val <

>] | x = v} - @-} -fromList :: [Dict key val] -> Table key val + @-} +fromList :: [Dict key val] -> Table key val fromList xs = xs -{-@ singleton :: forall val -> Prop, p :: Dict key val -> Prop>. +{-@ singleton :: forall val -> Prop, p :: Dict key val -> Prop>. Dict key val <

> -> [Dict key val <

>] - @-} -singleton :: Dict key val -> Table key val + @-} +singleton :: Dict key val -> Table key val singleton d = [d] {-@ emptyTable :: forall val -> Prop>. [Dict key val] @-} -emptyTable :: Table t v +emptyTable :: Table t v emptyTable = [] {-@ union :: forall val -> Prop, p :: Dict key val -> Prop>. - x:[Dict key val <

>] + x:[Dict key val <

>] -> y:[Dict key val <

>] -> {v:[Dict key val <

>] | listElts v = Set_cup (listElts x) (listElts y)} @-} {-@ diff :: forall val -> Prop, p :: Dict key val -> Prop>. - x:[Dict key val <

>] + x:[Dict key val <

>] -> y:[Dict key val <

>] -> {v:[Dict key val <

>] | listElts v = Set_dif (listElts x) (listElts y)} @-} union, diff :: (Eq key, Eq val) => Table key val -> Table key val -> Table key val -union xs ys = xs ++ ys -diff xs ys = xs \\ ys +union xs ys = xs ++ ys +diff xs ys = xs \\ ys -{-@ predicate Append XS YS V = - ((listElts (ddom v)) = Set_cup (listElts (ddom YS)) (listElts (ddom XS)) ) +{-@ predicate Append XS YS V = + ((listElts (ddom v)) = Set_cup (listElts (ddom YS)) (listElts (ddom XS)) ) @-} {-@ product :: forall val -> Prop, range2 :: key -> val -> Prop, - range :: key -> val -> Prop, - p :: Dict key val -> Prop, - q :: Dict key val -> Prop, + range :: key -> val -> Prop, + p :: Dict key val -> Prop, + q :: Dict key val -> Prop, r :: Dict key val -> Prop>. {x::Dict key val <

>, y :: Dict key val <> |- {v:Set.Set key | v = Set_cap (listElts (ddom x)) (listElts (ddom y))} <: {v:Set.Set key | Set_emp v }} {x::Dict key val <

>, y :: Dict key val <> |- {v:Dict key val | Append x y v} <: Dict key val <>} {x::Dict key val <

>, k::{v:key | Set_mem v (listElts (ddom x))} |- val <: val } {x::Dict key val <>, k::{v:key | Set_mem v (listElts (ddom x))} |- val <: val } - xs:[Dict key val <

>] - -> ys:[Dict key val <>] - -> [Dict key val <>] + xs:[Dict key val <

>] + -> ys:[Dict key val <>] + -> [Dict key val <>] @-} product :: (Eq key, Eq val) => Table key val -> Table key val -> Table key val -product xs ys = go xs ys - where +product xs ys = go xs ys + where go [] _ = [] go (x:xs) [] = go xs ys - go (x:xs) (y:ys) = productD x y : go (x:xs) ys + go (x:xs) (y:ys) = productD x y : go (x:xs) ys product (x:xs) (y:ys) = [ productD x y] -- | x <- xs, y <- ys] -- product (x:xs) (y:ys) = [productD x y] -- [ productD x y | x <- xs, y <- ys] instance (Eq key, Eq val) => Eq (Dict key val) where - (D ks1 f1) == (D ks2 f2) = all (\k -> k `elem` ks2 && f1 k == f2 k) ks1 + (D ks1 f1) == (D ks2 f2) = all (\k -> k `elem` ks2 && f1 k == f2 k) ks1 {-@ productD :: forall val -> Prop, range2 :: key -> val -> Prop, - range :: key -> val -> Prop, - p :: Dict key val -> Prop, + range :: key -> val -> Prop, + p :: Dict key val -> Prop, q :: Dict key val -> Prop>. {x::Dict key val <

>, y :: Dict key val <> |- {v:Set.Set key | v = Set_cap (listElts (ddom x)) (listElts (ddom y))} <: {v:Set.Set key | Set_emp v }} {x::Dict key val <

>, k::{v:key | Set_mem v (listElts (ddom x))} |- val <: val } {x::Dict key val <>, k::{v:key | Set_mem v (listElts (ddom x))}|- val <: val } x:Dict key val <

> - -> y:Dict key val <> - -> {v:Dict key val | (listElts (ddom v)) = Set_cup (listElts (ddom x)) (listElts (ddom y))} + -> y:Dict key val <> + -> {v:Dict key val | (listElts (ddom v)) = Set_cup (listElts (ddom x)) (listElts (ddom y))} @-} productD :: Eq key => Dict key val -> Dict key val -> Dict key val -productD (D ks1 f1) (D ks2 f2) - = let ks = ks1 ++ ks2 in +productD (D ks1 f1) (D ks2 f2) + = let ks = ks1 ++ ks2 in -- ORDERING IN LETS IS IMPORTANT: ks should be in scope for f let f i = if i `elem` ks1 then f1 (ensuredomain ks1 i) else f2 (ensuredomain ks2 i) in - D ks f + D ks f {-@ project :: forall val -> Prop>. - keys:[key] - -> [{v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))}] + keys:[key] + -> [{v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))}] -> [{v:Dict key val | (listElts (ddom v)) = listElts keys}] @-} project :: Eq t => [t] -> Table t v -> Table t v @@ -138,28 +138,28 @@ project ks (x:xs) = projectD ks x : project ks xs {-@ projectD :: forall val -> Prop>. - keys:[key] - -> {v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))} + keys:[key] + -> {v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))} -> {v:Dict key val | (listElts (ddom v)) = listElts keys} @-} projectD ks (D _ f) = D ks f {-@ select :: forall val -> Prop>. (Dict key val -> Bool) - -> x:[Dict key val] + -> x:[Dict key val] -> {v:[Dict key val] | Set_sub (listElts v) (listElts x)} @-} -select :: (Dict key val -> Bool) -> Table key val -> Table key val +select :: (Dict key val -> Bool) -> Table key val -> Table key val select _ [] = [] select prop (x:xs) | prop x = x : select prop xs | otherwise = select prop xs - -{-@ values :: forall val -> Prop>. + +{-@ values :: forall val -> Prop>. k:key -> [{v:Dict key val | Set_mem k (listElts (ddom v))}] -> [val] @-} values :: key -> [Dict key val] -> [val] -values k = map go +values k = map go where - go (D _ f) = f k + go (D _ f) = f k {-@ empty :: {v:Dict <{\k v -> false}> key val | Set_emp (listElts (ddom v))} @-} @@ -169,22 +169,22 @@ empty = D [] (\x -> error "call empty") -- TODO: replace error with liquidErro extend :: Eq key => key -> val -> Dict key val -> Dict key val {-@ extend :: forall val -> Prop>. - k:key-> val - -> x:Dict key val + k:key-> val + -> x:Dict key val -> {v:Dict key val | (listElts (ddom v)) = (Set_cup (listElts (ddom x)) (Set_sng k))} @-} extend k v (D ks f) = D (k:ks) (\i -> if i == k then v else f i) data P k v = k := v -{-@ data P k v v -> Prop> +{-@ data P k v v -> Prop> = (:=) (kkey :: k) (kval :: v) @-} infixr 3 += {-@ += :: forall val -> Prop>. - pp:P key val - -> x:Dict key val + pp:P key val + -> x:Dict key val -> {v:Dict key val | (listElts (ddom v)) = (Set_cup (listElts (ddom x)) (Set_sng (kkey pp)))} @-} (+=) :: Eq key => P key val -> Dict key val -> Dict key val @@ -199,8 +199,8 @@ infixr 3 += {-@ ensuredomain :: forall

Prop>. Eq a => xs:[a

] -> x:{v:a | Set_mem v (listElts xs)} -> {v:a

| Set_mem v (listElts xs) && v = x} @-} ensuredomain :: Eq a => [a] -> a -> a -ensuredomain (y:ys) x | x == y = y - | otherwise = ensuredomain ys x +ensuredomain (y:ys) x | x == y = y + | otherwise = ensuredomain ys x ensuredomain _ _ = liquidError "ensuredomain on empty list" @@ -214,13 +214,16 @@ ensuredomain _ _ = liquidError "ensuredomain on empty list" {-@ assume (Prelude.++) :: xs:[a] -> ys:[a] -> {v:[a] | listElts v = Set_cup (listElts xs) (listElts ys)} @-} -{-@ assume Prelude.elem :: x:a -> xs:[a] -> {v:Bool | Prop v <=> Set_mem x (listElts xs)} @-} +{-@ assume elem :: x:a -> xs:[a] -> {v:Bool | Prop v <=> Set_mem x (listElts xs)} @-} +elem :: a -> [a] -> Bool +elem = undefined + {-@ filter :: xs:[a] -> ({v:a | Set_mem v (listElts xs)} -> Bool) -> {v:[a] | Set_sub (listElts v) (listElts xs)} @-} filter :: [a] -> (a -> Bool) -> [a] filter [] _ = [] -filter (x:xs) f - | f x = x : filter xs f - | otherwise = filter xs f +filter (x:xs) f + | f x = x : filter xs f + | otherwise = filter xs f liquidError :: String -> a @@ -237,6 +240,5 @@ qual' :: key -> val qual' = undefined {-@ qual1 :: ks:[key] -> {v:Dict key val | (listElts (ddom v)) = listElts ks} @-} -qual1 :: [key] -> Dict key val +qual1 :: [key] -> Dict key val qual1 = undefined - diff --git a/benchmarks/icfp15/neg/RIO.hs b/benchmarks/icfp15/neg/RIO.hs index fa1bc68475..189f95aeff 100644 --- a/benchmarks/icfp15/neg/RIO.hs +++ b/benchmarks/icfp15/neg/RIO.hs @@ -1,44 +1,53 @@ module RIO where -{-@ data RIO a

Prop, q :: World -> a -> World -> Prop> +{-@ data RIO a

Prop, q :: World -> a -> World -> Prop> = RIO (rs :: (x:World

-> (a, World)<\w -> {v:World | true}>)) @-} data RIO a = RIO {runState :: World -> (a, World)} -{-@ runState :: forall

Prop, q :: World -> a -> World -> Prop>. +{-@ runState :: forall

Prop, q :: World -> a -> World -> Prop>. RIO a -> x:World

-> (a, World)<\w -> {v:World | true}> @-} data World = W +-- | RJ: Putting these in to get GHC 7.10 to not fuss +instance Functor RIO where + fmap = undefined + +-- | RJ: Putting these in to get GHC 7.10 to not fuss +instance Applicative RIO where + pure = undefined + (<*>) = undefined + instance Monad RIO where {-@ instance Monad RIO where - >>= :: forall < p :: World -> Prop - , p2 :: a -> World -> Prop + >>= :: forall < p :: World -> Prop + , p2 :: a -> World -> Prop , r :: a -> Prop , q1 :: World -> a -> World -> Prop , q2 :: a -> World -> b -> World -> Prop , q :: World -> b -> World -> Prop>. {x::a, w::World

|- World <: World} - {y::a, w::World

, w2::World, x::b, y::a |- World <: World} - {x::a, w::World, w2::World|- {v:a | v = x} <: a} + {y::a, w::World

, w2::World, x::b, y::a |- World <: World} + {x::a, w::World, w2::World|- {v:a | v = x} <: a} RIO a -> (x:a -> RIO <{v:World | true}, \w1 y -> {v:World | true}> b) -> RIO b ; - >> :: forall < p :: World -> Prop - , p2 :: World -> Prop + >> :: forall < p :: World -> Prop + , p2 :: World -> Prop , q1 :: World -> a -> World -> Prop , q2 :: World -> b -> World -> Prop , q :: World -> b -> World -> Prop>. {x::a, w::World

|- World <: World} - {w::World

, w2::World, x::b, y::a |- World <: World} + {w::World

, w2::World, x::b, y::a |- World <: World} RIO a -> RIO b -> RIO b ; return :: forall

Prop>. x:a -> RIO {w1:World | w0 == w1 && y == x}> a - @-} - (RIO g) >>= f = RIO $ \x -> case g x of {(y, s) -> (runState (f y)) s} - (RIO g) >> f = RIO $ \x -> case g x of {(y, s) -> (runState f ) s} + @-} + (RIO g) >>= f = RIO $ \x -> case g x of {(y, s) -> (runState (f y)) s} + (RIO g) >> f = RIO $ \x -> case g x of {(y, s) -> (runState f ) s} return w = RIO $ \x -> (w, x) fail = error @@ -48,4 +57,4 @@ instance Monad RIO where -- * TestM (Basic) -- * TwiceM -- * IfM --- * WhileM +-- * WhileM diff --git a/benchmarks/icfp15/pos/DBMovies.hs b/benchmarks/icfp15/pos/DBMovies.hs index 1a148c5d65..787ce7974f 100644 --- a/benchmarks/icfp15/pos/DBMovies.hs +++ b/benchmarks/icfp15/pos/DBMovies.hs @@ -1,23 +1,22 @@ module MovieClient where import DataBase - import GHC.CString -- This import interprets Strings as constants! import Data.Maybe (catMaybes) -import Prelude hiding (product) +import Prelude hiding (product, elem) import Control.Applicative ((<$>)) -type Tag = String +type Tag = String -data Value = I Int | S Name +data Value = I Int | S Name deriving (Show, Eq) -data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames - | Paronnaud | Almadovar | Haneke +data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames + | Paronnaud | Almadovar | Haneke deriving (Show, Eq) {-@ type Movies = [MovieScheme] @-} @@ -32,33 +31,33 @@ data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames {-@ type DirStarScheme = {v:Dict <{\t val -> DirStarRange t val}> Tag Value | ValidDirStarScheme v} @-} -{-@ predicate ValidMovieScheme V = - ((listElts (ddom V) ~~ Set_cup (Set_sng "year") - (Set_cup (Set_sng "star") - (Set_cup (Set_sng "director") +{-@ predicate ValidMovieScheme V = + ((listElts (ddom V) ~~ Set_cup (Set_sng "year") + (Set_cup (Set_sng "star") + (Set_cup (Set_sng "director") (Set_sng "title"))))) @-} -{-@ predicate MovieRange T V = (T ~~ "year" => ValidYear V) - && (T ~~ "star" => ValidStar V) - && (T ~~ "director" => ValidDirector V) - && (T ~~ "title" => ValidTitle V) +{-@ predicate MovieRange T V = (T ~~ "year" => ValidYear V) + && (T ~~ "star" => ValidStar V) + && (T ~~ "director" => ValidDirector V) + && (T ~~ "title" => ValidTitle V) @-} -{-@ predicate ValidDirectorScheme V = (listElts (ddom V) ~~ (Set_sng "director")) @-} +{-@ predicate ValidDirectorScheme V = (listElts (ddom V) ~~ (Set_sng "director")) @-} {-@ predicate DirectorRange T V = (T ~~ "director" => ValidDirector V) @-} -{-@ predicate ValidStarScheme V = (listElts (ddom V) ~~ (Set_sng "star")) @-} +{-@ predicate ValidStarScheme V = (listElts (ddom V) ~~ (Set_sng "star")) @-} {-@ predicate StarRange T V = (T ~~ "star" => ValidStar V) @-} -{-@ predicate ValidTitleScheme V = (listElts (ddom V) ~~ (Set_sng "title")) @-} +{-@ predicate ValidTitleScheme V = (listElts (ddom V) ~~ (Set_sng "title")) @-} {-@ predicate TitleDomain T = (T ~~ "title") @-} {-@ predicate TitleRange T V = (T ~~ "title" => ValidTitle V) @-} -{-@ predicate ValidDirStarScheme V = (listElts (ddom V) ~~ Set_cup (Set_sng "director") (Set_sng "star")) @-} +{-@ predicate ValidDirStarScheme V = (listElts (ddom V) ~~ Set_cup (Set_sng "director") (Set_sng "star")) @-} {-@ predicate DirStarDomain T = (T ~~ "director" || T ~~ "star") @-} {-@ predicate DirStarRange T V = (T ~~ "director" => ValidDirector V) && (T ~~ "star" => ValidStar V) @-} @@ -71,45 +70,45 @@ data Name = ChickenPlums | TalkToHer | Persepolis | FunnyGames -type Movies = Table Tag Value -type Titles = Table Tag Value +type Movies = Table Tag Value +type Titles = Table Tag Value type Directors = Table Tag Value type Stars = Table Tag Value type DirStars = Table Tag Value type MovieScheme = Dict Tag Value -movies :: Movies +movies :: Movies {-@ movies :: Movies @-} movies = fromList [movie1, movie2, movie3, movie4] movie1, movie2, movie3, movie4 :: MovieScheme {-@ movie1, movie2, movie3, movie4 :: MovieScheme @-} -movie1 = mkMovie (S TalkToHer) (S Almadovar) (I 8) (I 2002) +movie1 = mkMovie (S TalkToHer) (S Almadovar) (I 8) (I 2002) movie2 = mkMovie (S ChickenPlums) (S Paronnaud) (I 7) (I 2011) movie3 = mkMovie (S Persepolis) (S Paronnaud) (I 8) (I 2007) -movie4 = mkMovie (S FunnyGames) (S Haneke) (I 7) (I 2007) +movie4 = mkMovie (S FunnyGames) (S Haneke) (I 7) (I 2007) mkMovie :: Value -> Value -> Value -> Value -> MovieScheme -{-@ mkMovie :: {t:Value | ValidTitle t} +{-@ mkMovie :: {t:Value | ValidTitle t} -> {d:Value | ValidDirector d} -> {s:Value | ValidStar s} -> {y:Value | ValidYear y} -> MovieScheme - @-} + @-} mkMovie t d s y = ("title" := t) += ("star" := s) += ("director" := d) += ("year" := y) += empty seen :: Titles {-@ seen :: Titles @-} seen = [t1, t2] - where + where t1 = ("title" := S ChickenPlums) += empty t2 = ("title" := S FunnyGames) += empty not_seen :: Movies not_seen = select isSeen movies where - isSeen (D ks f) = not $ (f "title") `elem` (values "title" seen) + isSeen (D ks f) = not $ (f "title") `elem` (values "title" seen) {-@ not_seen, to_see :: Movies @-} to_see = select isGoodMovie not_seen @@ -128,15 +127,15 @@ good_directors = directors `diff` project ["director"] not_good_directors -- This _IS_ unsafe! -- good_directors = directors `diff` not_good_directors -not_good_directors :: DirStars +not_good_directors :: DirStars {-@ not_good_directors :: DirStars @-} -not_good_directors = project ["director", "star"] movies `diff` product directors good_stars +not_good_directors = project ["director", "star"] movies `diff` product directors good_stars - --- This _IS_ unsafe! + +-- This _IS_ unsafe! -- not_good_directors = project ["director", "star"] movies `diff` product directors movies -good_stars = mk_star_table (I 8) `union` mk_star_table (I 9) `union` mk_star_table (I 10) +good_stars = mk_star_table (I 8) `union` mk_star_table (I 9) `union` mk_star_table (I 10) mk_star_table :: Value -> Stars {-@ mk_star_table :: {s:Value | ValidStar s} -> Stars @-} @@ -148,7 +147,7 @@ mk_star_table s = [("star" := s) += empty] ------------------------------------------------------------------------------- -{-@ measure toInt :: Value -> Int +{-@ measure toInt :: Value -> Int toInt(I n) = n @-} diff --git a/benchmarks/icfp15/pos/DataBase.hs b/benchmarks/icfp15/pos/DataBase.hs index 6b7434728a..22157f6abc 100644 --- a/benchmarks/icfp15/pos/DataBase.hs +++ b/benchmarks/icfp15/pos/DataBase.hs @@ -1,132 +1,130 @@ module DataBase ( + Table, Dict(..), (+=), P(..), values, empty, - Table, Dict(..), (+=), P(..), values, empty, - - emptyTable, singleton, fromList, - + emptyTable, singleton, fromList, elem, + union, diff, product, project, select, productD - ) where -import qualified Data.Set as Set -import Prelude hiding (product, union, filter) +import qualified Data.Set as Set +import Prelude hiding (product, union, filter, elem) {-@ LIQUID "--no-termination" @-} {-@ LIQUID "totality" @-} type Table t v = [Dict t v] -data Dict key val = D {ddom :: [key], dfun :: key -> val} -{-@ ddom :: forall val -> Prop>. +data Dict key val = D {ddom :: [key], dfun :: key -> val} +{-@ ddom :: forall val -> Prop>. x:Dict key val -> {v:[key] | v = ddom x} @-} -{-@ dfun :: forall val -> Prop>. - x:Dict key val - -> i:{v:key | Set_mem v (listElts (ddom x))} -> val +{-@ dfun :: forall val -> Prop>. + x:Dict key val + -> i:{v:key | Set_mem v (listElts (ddom x))} -> val @-} {-@ data Dict key val val -> Prop> = D ( ddom :: [key]) - ( dfun :: i:{v:key | Set_mem v (listElts ddom)} -> val) - @-} + ( dfun :: i:{v:key | Set_mem v (listElts ddom)} -> val) + @-} -- instance (Show t, Show v, Eq t) => Show (Dict t v) where --- show (D ks f) = let g k = show k ++ "\t:=\t" ++ show (f k) ++ "\n" --- in concatMap g ks +-- show (D ks f) = let g k = show k ++ "\t:=\t" ++ show (f k) ++ "\n" +-- in concatMap g ks --- LIQUID : This discards the refinement of the Dict +-- LIQUID : This discards the refinement of the Dict -- for example the ddom -{-@ fromList :: forall val -> Prop, p :: Dict key val -> Prop>. +{-@ fromList :: forall val -> Prop, p :: Dict key val -> Prop>. x:[Dict key val <

>] -> {v:[Dict key val <

>] | x = v} - @-} -fromList :: [Dict key val] -> Table key val + @-} +fromList :: [Dict key val] -> Table key val fromList xs = xs -{-@ singleton :: forall val -> Prop, p :: Dict key val -> Prop>. +{-@ singleton :: forall val -> Prop, p :: Dict key val -> Prop>. Dict key val <

> -> [Dict key val <

>] - @-} -singleton :: Dict key val -> Table key val + @-} +singleton :: Dict key val -> Table key val singleton d = [d] {-@ emptyTable :: forall val -> Prop>. [Dict key val] @-} -emptyTable :: Table t v +emptyTable :: Table t v emptyTable = [] {-@ union :: forall val -> Prop, p :: Dict key val -> Prop>. - x:[Dict key val <

>] + x:[Dict key val <

>] -> y:[Dict key val <

>] -> {v:[Dict key val <

>] | listElts v = Set_cup (listElts x) (listElts y)} @-} {-@ diff :: forall val -> Prop, p :: Dict key val -> Prop>. - x:[Dict key val <

>] + x:[Dict key val <

>] -> y:[Dict key val <

>] -> {v:[Dict key val <

>] | listElts v = Set_dif (listElts x) (listElts y)} @-} union, diff :: (Eq key, Eq val) => Table key val -> Table key val -> Table key val -union xs ys = xs ++ ys -diff xs ys = xs \\ ys +union xs ys = xs ++ ys +diff xs ys = xs \\ ys -{-@ predicate Append XS YS V = - ((listElts (ddom v)) = Set_cup (listElts (ddom YS)) (listElts (ddom XS)) ) +{-@ predicate Append XS YS V = + ((listElts (ddom v)) = Set_cup (listElts (ddom YS)) (listElts (ddom XS)) ) @-} {-@ product :: forall val -> Prop, range2 :: key -> val -> Prop, - range :: key -> val -> Prop, - p :: Dict key val -> Prop, - q :: Dict key val -> Prop, + range :: key -> val -> Prop, + p :: Dict key val -> Prop, + q :: Dict key val -> Prop, r :: Dict key val -> Prop>. {x::Dict key val <

>, y :: Dict key val <> |- {v:Set.Set key | v = Set_cap (listElts (ddom x)) (listElts (ddom y))} <: {v:Set.Set key | Set_emp v }} {x::Dict key val <

>, y :: Dict key val <> |- {v:Dict key val | Append x y v} <: Dict key val <>} {x::Dict key val <

>, k::{v:key | Set_mem v (listElts (ddom x))} |- val <: val } {x::Dict key val <>, k::{v:key | Set_mem v (listElts (ddom x))} |- val <: val } - xs:[Dict key val <

>] - -> ys:[Dict key val <>] - -> [Dict key val <>] + xs:[Dict key val <

>] + -> ys:[Dict key val <>] + -> [Dict key val <>] @-} product :: (Eq key, Eq val) => Table key val -> Table key val -> Table key val -product xs ys = go xs ys - where +product xs ys = go xs ys + where go [] _ = [] go (x:xs) [] = go xs ys - go (x:xs) (y:ys) = productD x y : go (x:xs) ys + go (x:xs) (y:ys) = productD x y : go (x:xs) ys instance (Eq key, Eq val) => Eq (Dict key val) where - (D ks1 f1) == (D ks2 f2) = all (\k -> k `elem` ks2 && f1 k == f2 k) ks1 + (D ks1 f1) == (D ks2 f2) = all (\k -> k `elem` ks2 && f1 k == f2 k) ks1 {-@ productD :: forall val -> Prop, range2 :: key -> val -> Prop, - range :: key -> val -> Prop, - p :: Dict key val -> Prop, + range :: key -> val -> Prop, + p :: Dict key val -> Prop, q :: Dict key val -> Prop>. {x::Dict key val <

>, y :: Dict key val <> |- {v:Set.Set key | v = Set_cap (listElts (ddom x)) (listElts (ddom y))} <: {v:Set.Set key | Set_emp v }} {x::Dict key val <

>, k::{v:key | Set_mem v (listElts (ddom x))} |- val <: val } {x::Dict key val <>, k::{v:key | Set_mem v (listElts (ddom x))}|- val <: val } x:Dict key val <

> - -> y:Dict key val <> - -> {v:Dict key val | (listElts (ddom v)) = Set_cup (listElts (ddom x)) (listElts (ddom y))} + -> y:Dict key val <> + -> {v:Dict key val | (listElts (ddom v)) = Set_cup (listElts (ddom x)) (listElts (ddom y))} @-} productD :: Eq key => Dict key val -> Dict key val -> Dict key val -productD (D ks1 f1) (D ks2 f2) - = let ks = ks1 ++ ks2 in +productD (D ks1 f1) (D ks2 f2) + = let ks = ks1 ++ ks2 in -- ORDERING IN LETS IS IMPORTANT: ks should be in scope for f let f i = if i `elem` ks1 then f1 (ensuredomain ks1 i) else f2 (ensuredomain ks2 i) in - D ks f + D ks f {-@ project :: forall val -> Prop>. - keys:[key] - -> [{v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))}] + keys:[key] + -> [{v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))}] -> [{v:Dict key val | (listElts (ddom v)) = listElts keys}] @-} project :: Eq t => [t] -> Table t v -> Table t v @@ -135,26 +133,26 @@ project ks (x:xs) = projectD ks x : project ks xs {-@ projectD :: forall val -> Prop>. - keys:[key] - -> {v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))} + keys:[key] + -> {v:Dict key val | (Set_sub (listElts keys) (listElts (ddom v)))} -> {v:Dict key val | (listElts (ddom v)) = listElts keys} @-} projectD ks (D _ f) = D ks f {-@ select :: forall val -> Prop, p :: Dict key val -> Prop>. (Dict key val <

> -> Bool) - -> x:[Dict key val <

>] + -> x:[Dict key val <

>] -> {v:[Dict key val <

>] | Set_sub (listElts v) (listElts x)} @-} -select :: (Dict key val -> Bool) -> Table key val -> Table key val -select prop xs = filter prop xs +select :: (Dict key val -> Bool) -> Table key val -> Table key val +select prop xs = filter prop xs -{-@ values :: forall val -> Prop>. +{-@ values :: forall val -> Prop>. k:key -> [{v:Dict key val | Set_mem k (listElts (ddom v))}] -> [val] @-} values :: key -> [Dict key val] -> [val] -values k = map go +values k = map go where - go (D _ f) = f k + go (D _ f) = f k {-@ empty :: {v:Dict <{\k v -> false}> key val | Set_emp (listElts (ddom v))} @-} @@ -164,22 +162,22 @@ empty = D [] (\x -> liquidError "call empty") -- TODO: replace error with liqu extend :: Eq key => key -> val -> Dict key val -> Dict key val {-@ extend :: forall val -> Prop>. - k:key-> val - -> x:Dict key val + k:key-> val + -> x:Dict key val -> {v:Dict key val | (listElts (ddom v)) = (Set_cup (listElts (ddom x)) (Set_sng k))} @-} extend k v (D ks f) = D (k:ks) (\i -> if i == k then v else f i) data P k v = k := v -{-@ data P k v v -> Prop> +{-@ data P k v v -> Prop> = (:=) (kkey :: k) (kval :: v) @-} infixr 3 += {-@ += :: forall val -> Prop>. - pp:P key val - -> x:Dict key val + pp:P key val + -> x:Dict key val -> {v:Dict key val | (listElts (ddom v)) = (Set_cup (listElts (ddom x)) (Set_sng (kkey pp)))} @-} (+=) :: Eq key => P key val -> Dict key val -> Dict key val @@ -194,8 +192,8 @@ infixr 3 += {-@ ensuredomain :: forall

Prop>. Eq a => xs:[a

] -> x:{v:a | Set_mem v (listElts xs)} -> {v:a

| Set_mem v (listElts xs) && v = x} @-} ensuredomain :: Eq a => [a] -> a -> a -ensuredomain (y:ys) x | x == y = y - | otherwise = ensuredomain ys x +ensuredomain (y:ys) x | x == y = y + | otherwise = ensuredomain ys x ensuredomain _ _ = liquidError "ensuredomain on empty list" @@ -209,12 +207,15 @@ ensuredomain _ _ = liquidError "ensuredomain on empty list" {-@ assume (Prelude.++) :: xs:[a] -> ys:[a] -> {v:[a] | listElts v = Set_cup (listElts xs) (listElts ys)} @-} -{-@ assume Prelude.elem :: x:a -> xs:[a] -> {v:Bool | Prop v <=> Set_mem x (listElts xs)} @-} +{-@ assume elem :: x:a -> xs:[a] -> {v:Bool | Prop v <=> Set_mem x (listElts xs)} @-} +elem :: a -> [a] -> Bool +elem = undefined + {-@ filter :: (a -> Bool) -> xs:[a] -> {v:[a] | Set_sub (listElts v) (listElts xs)} @-} filter :: (a -> Bool) -> [a] -> [a] filter _ [] = [] -filter f (x:xs) - | f x = x : filter f xs +filter f (x:xs) + | f x = x : filter f xs | otherwise = filter f xs @@ -232,6 +233,5 @@ qual' :: key -> val qual' = undefined {-@ qual1 :: ks:[key] -> {v:Dict key val | (listElts (ddom v)) = listElts ks} @-} -qual1 :: [key] -> Dict key val +qual1 :: [key] -> Dict key val qual1 = undefined - diff --git a/benchmarks/icfp15/pos/RIO.hs b/benchmarks/icfp15/pos/RIO.hs index fa1bc68475..5ec7e74613 100644 --- a/benchmarks/icfp15/pos/RIO.hs +++ b/benchmarks/icfp15/pos/RIO.hs @@ -10,6 +10,16 @@ data RIO a = RIO {runState :: World -> (a, World)} data World = W + +-- | RJ: Putting these in to get GHC 7.10 to not fuss +instance Functor RIO where + fmap = undefined + +-- | RJ: Putting these in to get GHC 7.10 to not fuss +instance Applicative RIO where + pure = undefined + (<*>) = undefined + instance Monad RIO where {-@ instance Monad RIO where >>= :: forall < p :: World -> Prop diff --git a/benchmarks/icfp15/pos/RIO2.hs b/benchmarks/icfp15/pos/RIO2.hs index e1431296d5..ee7b19b14d 100644 --- a/benchmarks/icfp15/pos/RIO2.hs +++ b/benchmarks/icfp15/pos/RIO2.hs @@ -10,6 +10,17 @@ data RIO a = RIO {runState :: World -> (a, World)} data World = W +-- | RJ: Putting these in to get GHC 7.10 to not fuss +instance Functor RIO where + fmap = undefined + +-- | RJ: Putting these in to get GHC 7.10 to not fuss +instance Applicative RIO where + pure = undefined + (<*>) = undefined + + + instance Monad RIO where {-@ instance Monad RIO where >>= :: forall < p :: World -> Prop @@ -48,4 +59,4 @@ instance Monad RIO where -- * TestM (Basic) -- * TwiceM -- * IfM --- * WhileM \ No newline at end of file +-- * WhileM diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index 92fbc2e606..f523d63542 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -36,7 +36,7 @@ import TypeRep import Class (Class, className) import Var import Id -import IdInfo +import IdInfo import Name import NameSet import Text.PrettyPrint.HughesPJ hiding (first) @@ -122,7 +122,7 @@ initEnv :: GhcInfo -> CG CGEnv initEnv info = do let tce = tcEmbeds sp let fVars = impVars info - let dcs = filter isConLikeId ((snd <$> freeSyms sp)) + let dcs = filter isConLikeId ((snd <$> freeSyms sp)) let dcs' = filter isConLikeId fVars defaults <- forM fVars $ \x -> liftM (x,) (trueTy $ varType x) dcsty <- forM dcs $ \x -> liftM (x,) (trueTy $ varType x) @@ -131,12 +131,12 @@ initEnv info f0'' <- refreshArgs' =<< grtyTop info -- default TOP reftype (for exported vars without spec) let f0' = if notruetypes $ config sp then [] else f0'' f1 <- refreshArgs' defaults -- default TOP reftype (for all vars) - f1' <- refreshArgs' $ makedcs dcsty + f1' <- refreshArgs' $ makedcs dcsty f2 <- refreshArgs' $ assm info -- assumed refinements (for imported vars) f3 <- refreshArgs' $ vals asmSigs sp -- assumed refinedments (with `assume`) f40 <- refreshArgs' $ vals ctors sp -- constructor refinements (for measures) - (invs1, f41) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty (autosize sp) dcs - (invs2, f42) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty' (autosize sp) dcs' + (invs1, f41) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty (autosize sp) dcs + (invs2, f42) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty' (autosize sp) dcs' let f4 = mergeDataConTypes f40 (f41 ++ f42) sflag <- scheck <$> get let senv = if sflag then f2 else [] @@ -144,38 +144,38 @@ initEnv info let bs = (tx <$> ) <$> [f0 ++ f0', f1 ++ f1', f2, f3, f4] lts <- lits <$> get let tcb = mapSnd (rTypeSort tce) <$> concat bs - let γ0 = measEnv sp (head bs) (cbs info) (tcb ++ lts) (bs!!3) hs (invs1 ++ invs2) + let γ0 = measEnv sp (head bs) (cbs info) (tcb ++ lts) (bs!!3) hs (invs1 ++ invs2) foldM (++=) γ0 [("initEnv", x, y) | (x, y) <- concat $ tail bs] where sp = spec info ialias = mkRTyConIAl $ ialiases sp vals f = map (mapSnd val) . f mapSndM f (x,y) = (x,) <$> f y - makedcs = map strengthenDataConType + makedcs = map strengthenDataConType makeAutoDecrDataCons dcts specenv dcs = (simplify invs, tys) - where - (invs, tys) = unzip $ concatMap go tycons - tycons = L.nub $ catMaybes $ map idTyCon dcs + where + (invs, tys) = unzip $ concatMap go tycons + tycons = L.nub $ catMaybes $ map idTyCon dcs - go tycon - | S.member tycon specenv = zipWith (makeSizedDataCons dcts) (tyConDataCons tycon) [0..] - go _ - = [] - idTyCon x = dataConTyCon <$> case idDetails x of {DataConWorkId d -> Just d; DataConWrapId d -> Just d; _ -> Nothing} + go tycon + | S.member tycon specenv = zipWith (makeSizedDataCons dcts) (tyConDataCons tycon) [0..] + go _ + = [] + idTyCon x = dataConTyCon <$> case idDetails x of {DataConWorkId d -> Just d; DataConWrapId d -> Just d; _ -> Nothing} - simplify invs = dummyLoc . (`strengthen` invariant) . fmap (\_ -> mempty) <$> L.nub invs + simplify invs = dummyLoc . (`strengthen` invariant) . fmap (\_ -> mempty) <$> L.nub invs invariant = U (F.Reft (F.vv_, F.Refa $ F.PAtom F.Ge (lenOf F.vv_) (F.ECon $ F.I 0)) ) mempty mempty lenOf x = F.EApp lenLocSymbol [F.EVar x] -makeSizedDataCons dcts x' n = (toRSort $ ty_res trep, (x, fromRTypeRep trep{ty_res = tres})) - where +makeSizedDataCons dcts x' n = (toRSort $ ty_res trep, (x, fromRTypeRep trep{ty_res = tres})) + where x = dataConWorkId x' - t = fromMaybe (errorstar "makeSizedDataCons: this should never happen") $ L.lookup x dcts - trep = toRTypeRep t - tres = ty_res trep `strengthen` U (F.Reft (F.vv_, F.Refa + t = fromMaybe (errorstar "makeSizedDataCons: this should never happen") $ L.lookup x dcts + trep = toRTypeRep t + tres = ty_res trep `strengthen` U (F.Reft (F.vv_, F.Refa $ F.PAtom F.Eq (lenOf F.vv_) computelen)) mempty mempty recarguments = filter (\(t,_) -> (toRSort t == toRSort tres)) (zip (ty_args trep) (ty_binds trep)) @@ -184,11 +184,11 @@ makeSizedDataCons dcts x' n = (toRSort $ ty_res trep, (x, fromRTypeRep trep{ty_r mergeDataConTypes xts yts = merge (L.sortBy f xts) (L.sortBy f yts) where - f (x,_) (y,_) = compare x y + f (x,_) (y,_) = compare x y merge [] ys = ys merge xs [] = xs - merge (xt@(x, tx):xs) (yt@(y, ty):ys) - | x == y = (x, tx `F.meet` ty):merge xs ys + merge (xt@(x, tx):xs) (yt@(y, ty):ys) + | x == y = (x, tx `F.meet` ty):merge xs ys | x < y = xt:merge xs (yt:ys) | otherwise = yt:merge (xt:xs) ys @@ -685,7 +685,7 @@ initCGI cfg info = CGInfo { , kvProf = emptyKVProf , recCount = 0 , bindSpans = M.empty - , autoSize = autosize spc + , autoSize = autosize spc } where tce = tcEmbeds spc @@ -981,7 +981,7 @@ makeDecrIndex _ = return [] makeDecrIndexTy x t = do spDecr <- specDecr <$> get - autosz <- autoSize <$> get + autosz <- autoSize <$> get hint <- checkHint' autosz (L.lookup x $ spDecr) case dindex autosz of Nothing -> return $ Left msg -- addWarning msg >> return [] @@ -991,7 +991,7 @@ makeDecrIndexTy x t checkHint' = \autosz -> checkHint x ts (isDecreasing autosz cenv) dindex = \autosz -> L.findIndex (isDecreasing autosz cenv) ts msg = ErrTermin [x] (getSrcSpan x) (text "No decreasing parameter") - cenv = makeNumEnv ts + cenv = makeNumEnv ts trep = toRTypeRep $ unOCons t @@ -1592,7 +1592,7 @@ checkUnbound γ e x t a = t | otherwise = errorstar $ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t - ++ "\nIn\t" ++ showPpr e ++ " at " ++ showPpr (loc γ) ++ "\nArg = \n" ++ show a + ++ "\nIn\t" ++ showPpr e ++ " at " ++ showPpr (loc γ) ++ "\nArg = \n" ++ show a dropExists γ (REx x tx t) = liftM (, t) $ (γ, "dropExists") += (x, tx) dropExists γ t = return (γ, t) @@ -1752,17 +1752,25 @@ argExpr γ (Lit c) = snd $ literalConst (emb γ) c argExpr γ (Tick _ e) = argExpr γ e argExpr _ e = errorstar $ "argExpr: " ++ showPpr e +varRefType :: CGEnv -> Var -> CG SpecType +varRefType γ x = varRefType' γ x <$> (γ ??= F.symbol x) -varRefType γ x = liftM (varRefType' γ x) (γ ??= F.symbol x) - +varRefType' :: CGEnv -> Var -> SpecType -> SpecType varRefType' γ x t' | Just tys <- trec γ, Just tr <- M.lookup x' tys - = tr `strengthen` xr + = tr `strengthenS` xr | otherwise - = t - where t = t' `strengthen` xr - xr = singletonReft x -- uTop $ F.symbolReft $ F.symbol x - x' = F.symbol x + = t' `strengthenS` xr + where + xr = singletonReft x + x' = F.symbol x + +strengthenS :: RType c tv r -> r -> RType c tv r +strengthenS (RApp c ts rs _) r' = RApp c ts rs r' +strengthenS (RVar a _) r' = RVar a r' +strengthenS (RFun b t1 t2 _) r' = RFun b t1 t2 r' +strengthenS (RAppTy t1 t2 _) r' = RAppTy t1 t2 r' +strengthenS t _ = t -- TODO: should only expose/use subt. Not subsTyVar_meet subsTyVar_meet' (α, t) = subsTyVar_meet (α, toRSort t, t) From 1a76846589d0b0121e1f60c031d5d041232ba99e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jun 2015 20:03:21 -0700 Subject: [PATCH 03/23] update icfp15 benchmarks to ghc 710 --- benchmarks/icfp15/neg/Records.hs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/benchmarks/icfp15/neg/Records.hs b/benchmarks/icfp15/neg/Records.hs index 9fb2cb60be..797aa46621 100644 --- a/benchmarks/icfp15/neg/Records.hs +++ b/benchmarks/icfp15/neg/Records.hs @@ -1,18 +1,15 @@ module Records where - import GHC.CString -- This import interprets Strings as constants! -import DataBase +import DataBase data Value = I Int - {-@ rec :: {v:Dict <{\x y -> true}> String Value | listElts (ddom v) ~~ (Set_sng "bar")} @-} rec :: Dict String Value rec = ("foo" := I 8) += empty - unsafe :: Dict String Value -unsafe = ("bar" := I 8) += empty \ No newline at end of file +unsafe = ("bar" := I 8) += empty From f9ff60637f3248fd5321c15cb5b8c93df6d747df Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jun 2015 20:26:34 -0700 Subject: [PATCH 04/23] update icfp15 benchmarks to ghc 710 --- .../Haskell/Liquid/Constraint/Generate.hs | 17 ++-- src/Language/Haskell/Liquid/RefType.hs | 85 ++++++++++--------- 2 files changed, 53 insertions(+), 49 deletions(-) diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index f523d63542..d218f01174 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -1757,21 +1757,24 @@ varRefType γ x = varRefType' γ x <$> (γ ??= F.symbol x) varRefType' :: CGEnv -> Var -> SpecType -> SpecType varRefType' γ x t' - | Just tys <- trec γ, Just tr <- M.lookup x' tys - = tr `strengthenS` xr + | Just tys <- trec γ + , Just tr <- M.lookup x' tys + = tr `strengthen` xr | otherwise = t' `strengthenS` xr where xr = singletonReft x x' = F.symbol x -strengthenS :: RType c tv r -> r -> RType c tv r -strengthenS (RApp c ts rs _) r' = RApp c ts rs r' -strengthenS (RVar a _) r' = RVar a r' -strengthenS (RFun b t1 t2 _) r' = RFun b t1 t2 r' -strengthenS (RAppTy t1 t2 _) r' = RAppTy t1 t2 r' +strengthenS :: (F.Reftable r) => RType c tv r -> r -> RType c tv r +strengthenS (RApp c ts rs r) r' = RApp c ts rs $ topMeet r r' +strengthenS (RVar a r) r' = RVar a $ topMeet r r' +strengthenS (RFun b t1 t2 r) r' = RFun b t1 t2 $ topMeet r r' +strengthenS (RAppTy t1 t2 r) r' = RAppTy t1 t2 $ topMeet r r' strengthenS t _ = t +topMeet r r' = F.top r `F.meet` r' + -- TODO: should only expose/use subt. Not subsTyVar_meet subsTyVar_meet' (α, t) = subsTyVar_meet (α, toRSort t, t) diff --git a/src/Language/Haskell/Liquid/RefType.hs b/src/Language/Haskell/Liquid/RefType.hs index e347a75af6..177506a2ff 100644 --- a/src/Language/Haskell/Liquid/RefType.hs +++ b/src/Language/Haskell/Liquid/RefType.hs @@ -56,7 +56,7 @@ module Language.Haskell.Liquid.RefType ( , shiftVV , mkDataConIdsTy - , mkTyConInfo + , mkTyConInfo , strengthenRefTypeGen @@ -103,13 +103,13 @@ import Language.Fixpoint.Names (listConName, tupConName) import Data.List (sort, foldl') -strengthenDataConType (x, t) = (x, fromRTypeRep trep{ty_res = tres}) - where - trep = toRTypeRep t +strengthenDataConType (x, t) = (x, fromRTypeRep trep{ty_res = tres}) + where + trep = toRTypeRep t tres = ty_res trep `strengthen` U (exprReft expr) mempty mempty - xs = ty_binds trep + xs = ty_binds trep as = ty_vars trep - x' = symbol x + x' = symbol x expr | null xs && null as = EVar x' | null xs = EApp (dummyLoc x') [] | otherwise = EApp (dummyLoc x') (EVar <$> xs) @@ -154,7 +154,7 @@ instance ( SubsTy tv (RType c tv ()) (RType c tv ()) , RefTypable c tv () , RefTypable c tv r , PPrint (RType c tv r) - , FreeVar c tv + , FreeVar c tv ) => Monoid (RType c tv r) where mempty = errorstar "mempty: RType" @@ -170,27 +170,27 @@ instance ( SubsTy tv (RType c tv ()) (RType c tv ()) mempty = errorstar "mempty: RType 2" mappend _ _ = errorstar "mappend: RType 2" -instance (SubsTy c (RType b c ()) b, Monoid r, Reftable r, RefTypable b c r, RefTypable b c (), FreeVar b c, SubsTy c (RType b c ()) (RType b c ())) +instance (SubsTy c (RType b c ()) b, Monoid r, Reftable r, RefTypable b c r, RefTypable b c (), FreeVar b c, SubsTy c (RType b c ()) (RType b c ())) => Monoid (RTProp b c r) where mempty = errorstar "mempty: RTProp" mappend (RPropP s1 r1) (RPropP s2 r2) | isTauto r1 = RPropP s2 r2 | isTauto r2 = RPropP s1 r1 - | otherwise = RPropP s1 $ r1 `meet` + | otherwise = RPropP s1 $ r1 `meet` (subst (mkSubst $ zip (fst <$> s2) (EVar . fst <$> s1)) r2) - - mappend (RProp s1 t1) (RProp s2 t2) + + mappend (RProp s1 t1) (RProp s2 t2) | isTrivial t1 = RProp s2 t2 | isTrivial t2 = RProp s1 t1 - | otherwise = RProp s1 $ t1 `strengthenRefType` + | otherwise = RProp s1 $ t1 `strengthenRefType` (subst (mkSubst $ zip (fst <$> s2) (EVar . fst <$> s1)) t2) -- mappend (RPropP s1 t1) (RProp s2 t2) = errorstar "Reftable.mappend on invalid inputs" mappend t1 t2 = errorstar ("Reftable.mappend on invalid inputs" ++ show (t1, t2)) -- mappend _ _ = errorstar "Reftable.mappend on invalid inputs" -instance (Reftable r, RefTypable c tv r, RefTypable c tv (), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) +instance (Reftable r, RefTypable c tv r, RefTypable c tv (), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => Reftable (RTProp c tv r) where isTauto (RPropP _ r) = isTauto r isTauto (RProp _ t) = isTrivial t @@ -391,31 +391,31 @@ nlzP _ t = errorstar $ "RefType.nlzP: cannot handle " ++ show t -strengthenRefTypeGen, strengthenRefType :: +strengthenRefTypeGen, strengthenRefType :: ( RefTypable c tv () - , RefTypable c tv r + , RefTypable c tv r , PPrint (RType c tv r) , FreeVar c tv , SubsTy tv (RType c tv ()) (RType c tv ()) , SubsTy tv (RType c tv ()) c ) => RType c tv r -> RType c tv r -> RType c tv r -strengthenRefType_ :: +strengthenRefType_ :: ( RefTypable c tv () - , RefTypable c tv r + , RefTypable c tv r , PPrint (RType c tv r) , FreeVar c tv , SubsTy tv (RType c tv ()) (RType c tv ()) , SubsTy tv (RType c tv ()) c - ) => (RType c tv r -> RType c tv r -> RType c tv r) + ) => (RType c tv r -> RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r -> RType c tv r - + strengthenRefTypeGen t1 t2 = strengthenRefType_ f t1 t2 where f (RVar v1 r1) t = RVar v1 (r1 `meet` fromMaybe mempty (stripRTypeBase t)) f t (RVar v1 r1) = RVar v1 (r1 `meet` fromMaybe mempty (stripRTypeBase t)) - f t1 t2 = error $ printf "strengthenRefTypeGen on differently shaped types \nt1 = %s [shape = %s]\nt2 = %s [shape = %s]" + f t1 t2 = error $ printf "strengthenRefTypeGen on differently shaped types \nt1 = %s [shape = %s]\nt2 = %s [shape = %s]" (showpp t1) (showpp (toRSort t1)) (showpp t2) (showpp (toRSort t2)) - + -- NEWISH: with unifying type variables: causes big problems with TUPLES? --strengthenRefType t1 t2 = maybe (errorstar msg) (strengthenRefType_ t1) (unifyShape t1 t2) @@ -423,8 +423,8 @@ strengthenRefTypeGen t1 t2 = strengthenRefType_ f t1 t2 -- (render t1) (render (toRSort t1)) (render t2) (render (toRSort t2)) -- OLD: without unifying type variables, but checking α-equivalence -strengthenRefType t1 t2 - | eqt t1 t2 +strengthenRefType t1 t2 + | eqt t1 t2 = strengthenRefType_ (\x _ -> x) t1 t2 | otherwise = errorstar msg @@ -468,15 +468,15 @@ strengthenRefType_ f (RAllE x tx t1) t2 strengthenRefType_ f t1 (RAllE x tx t2) = RAllE x tx $ strengthenRefType_ f t1 t2 -strengthenRefType_ f (RAppTy t1 t1' r1) (RAppTy t2 t2' r2) +strengthenRefType_ f (RAppTy t1 t1' r1) (RAppTy t2 t2' r2) = RAppTy t t' (r1 `meet` r2) where t = strengthenRefType_ f t1 t2 t' = strengthenRefType_ f t1' t2' -strengthenRefType_ f (RFun x1 t1 t1' r1) (RFun x2 t2 t2' r2) +strengthenRefType_ f (RFun x1 t1 t1' r1) (RFun x2 t2 t2' r2) = RFun x2 t t' (r1 `meet` r2) where t = strengthenRefType_ f t1 t2 - t' = strengthenRefType_ f (subst1 t1' (x1, EVar x2)) t2' + t' = strengthenRefType_ f (subst1 t1' (x1, EVar x2)) t2' strengthenRefType_ f (RApp tid t1s rs1 r1) (RApp _ t2s rs2 r2) = RApp tid ts rs (r1 `meet` r2) @@ -486,9 +486,10 @@ strengthenRefType_ f (RApp tid t1s rs1 r1) (RApp _ t2s rs2 r2) strengthenRefType_ _ (RVar v1 r1) (RVar v2 r2) | v1 == v2 = RVar v1 (r1 `meet` r2) -strengthenRefType_ f t1 t2 +strengthenRefType_ f t1 t2 = f t1 t2 +meets :: (F.Reftable r) => [r] -> [r] -> [r] meets [] rs = rs meets rs [] = rs meets rs rs' @@ -1037,18 +1038,18 @@ rTyVarSymbol (RTV α) = typeUniqueSymbol $ TyVarTy α --------------------------- Termination Predicates -------------------------------------- ----------------------------------------------------------------------------------------- -makeNumEnv = concatMap go +makeNumEnv = concatMap go where go (RApp c ts _ _) | isNumCls c || isFracCls c = [ a | (RVar a _) <- ts] go _ = [] isDecreasing autoenv _ (RApp c _ _ _) - = isJust (sizeFunction (rtc_info c)) -- user specified size or - || isSizeable autoenv tc - where tc = rtc_tc c + = isJust (sizeFunction (rtc_info c)) -- user specified size or + || isSizeable autoenv tc + where tc = rtc_tc c isDecreasing _ cenv (RVar v _) - = v `elem` cenv -isDecreasing _ _ _ + = v `elem` cenv +isDecreasing _ _ _ = False makeDecrType autoenv = mkDType autoenv [] [] @@ -1059,12 +1060,12 @@ mkDType autoenv xvs acc [(v, (x, t))] tr = uTop $ Reft (vv, Refa $ pOr (r:acc)) r = cmpLexRef xvs (v', vv, f) v' = symbol v - f = mkDecrFun autoenv t + f = mkDecrFun autoenv t vv = "vvRec" mkDType autoenv xvs acc ((v, (x, t)):vxts) = mkDType autoenv ((v', x, f):xvs) (r:acc) vxts - where + where r = cmpLexRef xvs (v', x, f) v' = symbol v f = mkDecrFun autoenv t @@ -1074,16 +1075,16 @@ mkDType _ _ _ _ = errorstar "RefType.mkDType called on invalid input" isSizeable :: S.HashSet TyCon -> TyCon -> Bool -isSizeable autoenv tc = S.member tc autoenv -- TC.isAlgTyCon tc -- && TC.isRecursiveTyCon tc +isSizeable autoenv tc = S.member tc autoenv -- TC.isAlgTyCon tc -- && TC.isRecursiveTyCon tc -mkDecrFun autoenv (RApp c _ _ _) - | Just f <- sizeFunction $ rtc_info c +mkDecrFun autoenv (RApp c _ _ _) + | Just f <- sizeFunction $ rtc_info c = f - | isSizeable autoenv $ rtc_tc c + | isSizeable autoenv $ rtc_tc c = \v -> F.EApp lenLocSymbol [F.EVar v] -mkDecrFun _ (RVar _ _) - = EVar -mkDecrFun _ _ +mkDecrFun _ (RVar _ _) + = EVar +mkDecrFun _ _ = errorstar "RefType.mkDecrFun called on invalid input" cmpLexRef vxs (v, x, g) From 1877124a991b8015a0f7423284697a8f566879b6 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jun 2015 22:13:17 -0700 Subject: [PATCH 05/23] only the neg/Strata.hs wierdness remains, ICFP tests now working on 710, and hopefully Text too. --- Makefile | 18 ++++++------- README.md | 9 ++++--- benchmarks/text-0.11.2.3/Data/Text.hs | 6 ++--- benchmarks/text-0.11.2.3/Data/Text/Unsafe.hs | 26 ++++++++++++------- .../Haskell/Liquid/Constraint/Generate.hs | 9 ++++--- 5 files changed, 37 insertions(+), 31 deletions(-) diff --git a/Makefile b/Makefile index 4658bc6629..e440ab4ba8 100644 --- a/Makefile +++ b/Makefile @@ -27,8 +27,10 @@ first: $(CABAL) install --ghc-options=$(FASTOPTS) --only-dependencies --enable-tests --enable-benchmarks dist: - $(CABAL) install --ghc-options=$(DISTOPTS) - + # $(CABAL) install --ghc-options=$(DISTOPTS) + $(CABAL) configure -fdevel --enable-tests --disable-library-profiling -O2 + $(CABAL) build + prof: $(CABAL) install --enable-executable-profiling --enable-library-profiling --ghc-options=$(PROFOPTS) @@ -66,8 +68,8 @@ test: # $(CABAL) exec $(TASTY) -- --smtsolver $(SMTSOLVER) --liquid-opts='$(LIQUIDOPTS)' --hide-successes --rerun-update -p 'Unit/' -j$(THREADS) +RTS -N$(THREADS) -RTS test710: - # $(CABAL) configure -fdevel --enable-tests --disable-library-profiling -O2 - # $(CABAL) build + $(CABAL) configure -fdevel --enable-tests --disable-library-profiling -O2 + $(CABAL) build $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -p 'Unit/' -j$(THREADS) +RTS -N$(THREADS) -RTS @@ -81,18 +83,14 @@ all-test: cabal build cabal exec $(TASTY) -- --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS -all-test-710: - cabal configure -fdevel --enable-tests --disable-library-profiling -O2 - cabal build - $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS - - all-retest: cabal configure -fdevel --enable-tests --disable-library-profiling -O2 cabal build cabal exec $(TASTY) -- --smtsolver $(SMTSOLVER) --hide-successes --rerun-filter "exceptions,failures,new" --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS all-retest-710: + cabal configure -fdevel --enable-tests --disable-library-profiling -O2 + cabal build $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-filter "exceptions,failures,new" --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS diff --git a/README.md b/README.md index 6536aed188..a836c9f4ee 100644 --- a/README.md +++ b/README.md @@ -373,16 +373,17 @@ tests/pos/mutrec.hs for the full example). Lazy Variables -------------- -A variable cab be specified as `LAZYVAR` +A variable can be specified as `LAZYVAR` {-@ LAZYVAR z @-} With this annotation the definition of `z` will be checked at the points where it is used. For example, with the above annotation the following code is SAFE: - foo = if x > 0 then z else x - where z = 42 `safeDiv` x - x = choose 0 + foo = if x > 0 then z else x + where + z = 42 `safeDiv` x + x = choose 0 By default, all the variables starting with `fail` are marked as LAZY, to defer failing checks at the point where these variables are used. diff --git a/benchmarks/text-0.11.2.3/Data/Text.hs b/benchmarks/text-0.11.2.3/Data/Text.hs index bac470ff76..93dee73f5a 100644 --- a/benchmarks/text-0.11.2.3/Data/Text.hs +++ b/benchmarks/text-0.11.2.3/Data/Text.hs @@ -493,10 +493,10 @@ head t = S.head (stream t) uncons :: Text -> Maybe (Char, Text) uncons t@(Text arr off len) | len <= 0 = Nothing - | otherwise = let Iter c d = i + | otherwise = let Iter c d = iter t 0 -- i in Just (c, textP arr (off+d) (len-d)) - {-@ LAZYVAR i @-} - where i = iter t 0 + {- LAZYVAR i @-} + -- where i = iter t 0 {-# INLINE [1] uncons #-} -- | Lifted from Control.Arrow and specialized. diff --git a/benchmarks/text-0.11.2.3/Data/Text/Unsafe.hs b/benchmarks/text-0.11.2.3/Data/Text/Unsafe.hs index 6427cb068c..7e5c55ddc6 100644 --- a/benchmarks/text-0.11.2.3/Data/Text/Unsafe.hs +++ b/benchmarks/text-0.11.2.3/Data/Text/Unsafe.hs @@ -95,13 +95,16 @@ data Iter = Iter {-# UNPACK #-} !Char {-# UNPACK #-} !Int iter :: Text -> Int -> Iter iter (Text arr off _len) i | m < 0xD800 || m > 0xDBFF = Iter (unsafeChr m) 1 - | otherwise = Iter (chr2 m n) 2 + | otherwise = let k = j + 1 + n = A.unsafeIndex arr k + in + Iter (chr2 m n) 2 where m = A.unsafeIndexF arr off _len j - {-@ LAZYVAR n @-} - n = A.unsafeIndex arr k j = off + i - {-@ LAZYVAR k @-} - k = j + 1 + {- LAZYVAR n @-} + -- n = A.unsafeIndex arr k + {- LAZYVAR k @-} + -- k = j + 1 {-# INLINE iter #-} -- | /O(1)/ Iterate one step through a UTF-16 array, returning the @@ -136,13 +139,16 @@ iter_ (Text arr off _len) i | m < 0xD800 || m > 0xDBFF = 1 reverseIter :: Text -> Int -> (Char,Int) reverseIter (Text arr off _len) i | m < 0xDC00 || m > 0xDFFF = (unsafeChr m, neg 1) - | otherwise = (chr2 n m, neg 2) + | otherwise = let k = j - 1 + n = A.unsafeIndex arr k + in + (chr2 n m, neg 2) where m = A.unsafeIndexB arr off _len j - {-@ LAZYVAR n @-} - n = A.unsafeIndex arr k + {- LAZYVAR n @-} + -- n = A.unsafeIndex arr k j = off + i - {-@ LAZYVAR k @-} - k = j - 1 + {- LAZYVAR k @-} + -- k = j - 1 {-# INLINE reverseIter #-} {-@ neg :: n:Int -> {v:Int | v = (0-n)} @-} diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index d218f01174..1bb550c698 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -1757,22 +1757,23 @@ varRefType γ x = varRefType' γ x <$> (γ ??= F.symbol x) varRefType' :: CGEnv -> Var -> SpecType -> SpecType varRefType' γ x t' - | Just tys <- trec γ - , Just tr <- M.lookup x' tys - = tr `strengthen` xr + | Just tys <- trec γ, Just tr <- M.lookup x' tys + = tr `strengthenS` xr | otherwise = t' `strengthenS` xr where xr = singletonReft x x' = F.symbol x +-- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition +-- of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace +-- the `otherwise` case? The fq file holds no answers, both are sat. strengthenS :: (F.Reftable r) => RType c tv r -> r -> RType c tv r strengthenS (RApp c ts rs r) r' = RApp c ts rs $ topMeet r r' strengthenS (RVar a r) r' = RVar a $ topMeet r r' strengthenS (RFun b t1 t2 r) r' = RFun b t1 t2 $ topMeet r r' strengthenS (RAppTy t1 t2 r) r' = RAppTy t1 t2 $ topMeet r r' strengthenS t _ = t - topMeet r r' = F.top r `F.meet` r' -- TODO: should only expose/use subt. Not subsTyVar_meet From e909bb010996e2f4c390e2a34da597e15e5202a5 Mon Sep 17 00:00:00 2001 From: nikivazou Date: Fri, 26 Jun 2015 12:20:47 -0700 Subject: [PATCH 06/23] fix strata example --- Liquid.hs | 8 ++++++-- src/Language/Haskell/Liquid/Constraint/Generate.hs | 1 + src/Language/Haskell/Liquid/Types.hs | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/Liquid.hs b/Liquid.hs index d7c059c43a..24e0701392 100644 --- a/Liquid.hs +++ b/Liquid.hs @@ -1,10 +1,14 @@ {-# LANGUAGE TupleSections #-} +{-# LANGUAGE CPP #-} {-@ LIQUID "--cabaldir" @-} {-@ LIQUID "--diff" @-} --- import Data.Monoid (mconcat, mempty) --- import Control.Applicative ((<$>)) +#if __GLASGOW_HASKELL__ < 710 +import Data.Monoid (mconcat, mempty) +import Control.Applicative ((<$>)) +#endif + import Data.Maybe import System.Exit import Control.DeepSeq diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index 1bb550c698..9af3453d8b 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -1765,6 +1765,7 @@ varRefType' γ x t' xr = singletonReft x x' = F.symbol x + -- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition -- of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace -- the `otherwise` case? The fq file holds no answers, both are sat. diff --git a/src/Language/Haskell/Liquid/Types.hs b/src/Language/Haskell/Liquid/Types.hs index fdbb30ac28..7b9d82f83d 100644 --- a/src/Language/Haskell/Liquid/Types.hs +++ b/src/Language/Haskell/Liquid/Types.hs @@ -1035,7 +1035,7 @@ instance (PPrint r, Reftable r) => Reftable (UReft r) where toReft (U r ps _) = toReft r `meet` toReft ps params (U r _ _) = params r bot (U r _ s) = U (bot r) (Pr []) (bot s) - top (U r p s) = U (top r) (top p) (top s) + top (U r p s) = U (top r) (top p) s ofReft r = U (ofReft r) mempty mempty From f30e4405de11b132646f9aa6814cf061791ab292 Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Fri, 26 Jun 2015 15:22:56 -0700 Subject: [PATCH 07/23] some TODOs --- TODO.markdown | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/TODO.markdown b/TODO.markdown index 8a01c0a520..ed379bbdc0 100644 --- a/TODO.markdown +++ b/TODO.markdown @@ -1,6 +1,17 @@ TODO ==== +Check covariants +---------------- + +See https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/todo/kmpMonad.hs#L55 +It is safe is 100 is changed to 0. WHY? + +LAZYVAR +------- +Restore LAZYVARS in `Data/Text.hs`, `Data/Text/Unsafe.hs` + + Automatically refine *inductors* -------------------------------- Proposed by Valentine: in dependent languages (Coq) inductors (like our `loop` for natural numbers) From fdf8c97bb19359fd61870b3a7c5807139c64a480 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 26 Jun 2015 16:01:06 -0700 Subject: [PATCH 08/23] tick tock on bounded-blog --- Makefile | 7 + .../2015-06-13-bounded-refinement-types.lhs | 207 +++++++++--------- 2 files changed, 113 insertions(+), 101 deletions(-) diff --git a/Makefile b/Makefile index e440ab4ba8..73f2f5b753 100644 --- a/Makefile +++ b/Makefile @@ -83,6 +83,13 @@ all-test: cabal build cabal exec $(TASTY) -- --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS +all-test-710: + cabal configure -fdevel --enable-tests --disable-library-profiling -O2 + cabal build + $(TASTY) --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -j$(THREADS) +RTS -N$(THREADS) -RTS + + + all-retest: cabal configure -fdevel --enable-tests --disable-library-profiling -O2 cabal build diff --git a/docs/blog/2015-06-13-bounded-refinement-types.lhs b/docs/blog/2015-06-13-bounded-refinement-types.lhs index 696cddb6d0..2c5e84aedc 100644 --- a/docs/blog/2015-06-13-bounded-refinement-types.lhs +++ b/docs/blog/2015-06-13-bounded-refinement-types.lhs @@ -4,28 +4,17 @@ title: "Bounded Refinement Types" date: 2015-06-13 comments: true external-url: -author: Niki Vazou +author: Niki Vazou published: true categories: bounded-refinements, abstract-refinements, function-composition demo: BoundedRefinementTypes.hs --- -Refinement Types decorate types with logical predicates, -and so allow us to specify sophisticated invariants for the underlying values. -Thought, classic first order refinements prevent modular specification. - -As a step towards modular higher-order specifications, we introduced [Abstract Refinement Types](http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/06/03/abstracting-over-refinements.lhs) -that are used in liquidHaskell to abstract over specific properties or invariants. -While useful, refinement abstraction was not enough to enable higher order abstractions requiring dependencies between abstract refinements. -As an example, to specify a precise type for _function composition_, -one needs to express compositionality of the refinements. -To express such fine grained dependencies, we enriched type signatures with -_bounded qualification_ over abstract refinements. - -Today, we will see how bounds in refinements types can be used to -appropriately type function composition and generally how bounds can be used to -get us out of expressiveness bounds -of Abstract Refinement Types. +While refinement types let SMT solvers do a lot of the "boring" analysis, +they are limited to decidable (first order) logics which can prevent us +from writing *modular* and *reusable* specifications for *higher-order* +functions. Next, lets see why modularity is important, and how we can +recover it using a new technique called **Bounded Refinements**. @@ -35,44 +24,59 @@ module BoundedRefinementTypes where import Prelude hiding ((.), maximum) import Language.Haskell.Liquid.Prelude -incr :: Int -> Int -incr2 :: Int -> Int -incr3 :: Int -> Int +incr :: Int -> Int +incr2 :: Int -> Int +incr3 :: Int -> Int -compose1 :: (Int -> Int) -> (Int -> Int) -> Int -> Int +compose1 :: (Int -> Int) -> (Int -> Int) -> Int -> Int compose1 f g x = f (g x) -incr2' :: Int -> Int +incr2' :: Int -> Int compose2 :: (b -> c) -> (a -> b) -> a -> c \end{code} -Abstract Refinements --------------------- -We use Abstract Refinements to allow fot modular specifications. -Consider the function that returns the largest element of a list: +The Problem: Reusable Specifications +------------------------------------ + +Let us suppose, for just a moment, that we live in a dystopian future +where parametric polymorphism and typeclasses have been eliminated +from Haskell. Now, consider the function that returns the largest +element of a list: \begin{code} -maximum :: [Int] -> Int -maximum [x] = x -maximum (x:xs) = max x (maximum xs) - where max a b = if a < b then b else a +maximum :: [Int] -> Int +maximum [x] = x +maximum (x:xs) = max x (maximum xs) + where + max a b = if a < b then b else a \end{code} -How can one write a first-order refinement type specification for -`maximum` that will let us verify that: + +Now, suppose we have refinements: \begin{code} -{-@ type Pos = {v:Int | 0 < v} @-} +{-@ type Pos = {v:Int | 0 < v} @-} +{-@ type Neg = {v:Int | 0 < v} @-} +\end{code} -{-@ posMax :: [Pos] -> Pos @-} -posMax = maximum +Here's the problem: how can *specify* the behavior of `maximum` +in a way that lets us simultaneouly verify that: + +\begin{code} +{-@ posMax :: [Int] -> Pos @-} +posMax xs = maximum [x | x <- xs, x > 0] + +{-@ negMax :: [Int] -> Neg @-} +negMax xs = maximum [x | x <- xs, x < 0] \end{code} -Any suitable specification would have to enumerate the -situations under which `maximum` may be invoked -breaking modularity. +HEREHEREHEREHERE -_Abstract Refinements_ overcome the above modularity -problems. +Any suitable specification would have to enumerate the +situations under which `maximum` may be invoked breaking +modularity. + +[Abstract Refinements][AbstractRefinements] overcome the +above modularity problems. The main idea is that we can type `maximum` by observing that it returns _one of_ the elements in its input list. Thus, if every element of the list enjoys some refinement `p` @@ -85,12 +89,13 @@ Concretely, we can type the function as: \end{code} where informally, `Int

` stands for `{v:Int | p v}`, -and `p` is an _uninterpreted function_ in the refinement +and `p` is an _uninterpreted function_ in the refinement logic. The signature states that for any refinement `p` on `Int`, -the input is a list of elements satisfying `p` -and returns as output an integer satisfying `p`. +the input is a list of elements satisfying `p` and returns +as output an integer satisfying `p`. + Can we use Abstract Refinements to specify a precise type for function composition? @@ -106,27 +111,27 @@ incr x = x + 1 How do we use `incr` to create a function that increases its argument by `2`? -We can write a function `incr2` that +We can write a function `incr2` that first computes `z` by increasing the argument `x`, and then increases `z. \begin{code} {-@ incr2 :: x:Int -> {v:Int | v = x + 2} @-} -incr2 x = let z = incr x in incr z +incr2 x = let z = incr x in incr z \end{code} -By the type of `incr`, -LiquidHaskell will infer that `z` is equal to `x + 1`, +By the type of `incr`, +LiquidHaskell will infer that `z` is equal to `x + 1`, `z :: {v:Int | v = x + 1} ` and that -the result is equal to `z + 1`. -Thus, it will accept the post-condition encoded in type signature for `incr2`, -that is that `incr2` increases its argument by `2`. +the result is equal to `z + 1`. +Thus, it will accept the post-condition encoded in type signature for `incr2`, +that is that `incr2` increases its argument by `2`. -Since we are in the Haskell world, we would like to write `incr2` +Since we are in the Haskell world, we would like to write `incr2` using the higher order function composition. We define the function `compose` that composes its two functional arguments \begin{code} -compose f g x = f (g x) +compose f g x = f (g x) \end{code} We use `compose` to composing `incr` with itself getting `incr2'`, a function that increases its argument by `2`. @@ -135,28 +140,28 @@ We use `compose` to composing `incr` with itself getting `incr2'`, a function th incr2' = compose1 incr incr \end{code} -Our goal is to specify a type for compose -that allows verification of the above type for `incr2'`, by +Our goal is to specify a type for compose +that allows verification of the above type for `incr2'`, by capturing the compositionality of the refinements. As a first attempt, we give compose a very specific type that states that -if (1) the first functional argument increases its argument by `1`, and +if (1) the first functional argument increases its argument by `1`, and (2) the second functional argument increases its argument by `1`, -then the result function increases its argument by `2`: +then the result function increases its argument by `2`: \begin{code} -{-@ compose1 :: (y:Int -> {z:Int | z = y + 1}) - -> (x:Int -> {z:Int | z = x + 1}) +{-@ compose1 :: (y:Int -> {z:Int | z = y + 1}) + -> (x:Int -> {z:Int | z = x + 1}) -> x:Int -> {z:Int | z = x + 2} @-} \end{code} -That was easy, with the above type liquidHaskell does verify that `incr2'` -actually increases its argument by `2`. -But, there is a catch: +That was easy, with the above type liquidHaskell does verify that `incr2'` +actually increases its argument by `2`. +But, there is a catch: _The type of `compose1` it too specific_. -If we use `compose1` with any other functional argument, -for example `incr2` that increases its argument by `2`, +If we use `compose1` with any other functional argument, +for example `incr2` that increases its argument by `2`, liquidHaskell will reasonably mark the call site as unsafe: \begin{code} @@ -170,25 +175,25 @@ In any real world application, this super specific type of `compose1` is not acc An Abstract Type for Compose ---------------------------- -Onto abstracting the type of compose we follow the route of [Abstract Refinements][AbstractRefinements]. -We make a second attempt to type function composition and give -`compose2` a type that states that +Onto abstracting the type of compose we follow the route of [Abstract Refinements][AbstractRefinements]. +We make a second attempt to type function composition and give +`compose2` a type that states that forall abstract refinements `p`, `q` and `r` -if (1) the first functional argument `f` returns a value that satisfies a relation `p` with respect to its argument `y`, and +if (1) the first functional argument `f` returns a value that satisfies a relation `p` with respect to its argument `y`, and (2) the second functional argument `g` returns a value that satisfies a relation `q` with respect to its argument `x`, then the result function returns a value that satisfies a relation `r` with respect to its argument `x`: \begin{code} {-@ compose2 :: forall

c -> Prop, - q :: a -> b -> Prop, - r :: a -> c -> Prop>. + q :: a -> b -> Prop, + r :: a -> c -> Prop>. f:(y:b -> c

) -> g:(x:a -> b) -> x:a -> c -@-} +@-} \end{code} -With this type for `compose2` liquidHaskell will prove that composing `incr` by itself +With this type for `compose2` liquidHaskell will prove that composing `incr` by itself gives a function that increased its argument by `2`: \begin{code} @@ -196,18 +201,18 @@ gives a function that increased its argument by `2`: incr2'' = compose2 incr incr \end{code} -To do so, liquidHaskell will employ the Abstract Refinement Types inference and guess -the appropriate instantiations for `p`, `q`, and `r`. -That is, liquidHaskell will infer that `p` and `q` relate two consecutive numbers +To do so, liquidHaskell will employ the Abstract Refinement Types inference and guess +the appropriate instantiations for `p`, `q`, and `r`. +That is, liquidHaskell will infer that `p` and `q` relate two consecutive numbers `p, q := \x v -> v = x + 1` while `r` relates two numbers with distance `2`: -`r := \x v -> v = x + 2`. -Thus, at this specific call site the abstract type of `compose2` will be instantiated to -the concrete type we gave to `compose1`. +`r := \x v -> v = x + 2`. +Thus, at this specific call site the abstract type of `compose2` will be instantiated to +the concrete type we gave to `compose1`. And, verification of `incr2''` will succeed. -What is the catch now? +What is the catch now? In this second attempt we abstracted the type of `compose2` too much! In fact, LiquidHaskell cannot prove that the body of `compose2` satisfies its type, just because it does not. @@ -215,7 +220,7 @@ In fact, LiquidHaskell cannot prove that the body of `compose2` satisfies its ty compose2 f g x = let z = g x in f z \end{code} -By the precondition of `compose2` we know the result refinements of the functional arguments `f` and `g`. +By the precondition of `compose2` we know the result refinements of the functional arguments `f` and `g`. From the type of `g` we know that `z` satisfies `q` on `x`, i.e. `q x z` holds. Similarly, from the type of `f` we know that `f z` satisfies `q` on `x`, i.e. `q x z` holds. @@ -229,23 +234,23 @@ The required property `r x z` is not satisfied for _arbitrary_ abstract refineme Bound Abstract Refinements by the Chain Property ------------------------------------------------ -We made two attempts to type `compose`. -The first one "failed" as our type was unrealistically specific. -The second failed as it was unsoundly general. -In our third and final attempt -we give `compose` a type that is abstracted over three abstract refinements `p`, `q` and `r`. -But, this time the three refinements are not arbitrary: +We made two attempts to type `compose`. +The first one "failed" as our type was unrealistically specific. +The second failed as it was unsoundly general. +In our third and final attempt +we give `compose` a type that is abstracted over three abstract refinements `p`, `q` and `r`. +But, this time the three refinements are not arbitrary: they are bounded to satisfy the chain property. We encode the chain property as a boolean Haskell function: \begin{code} -chain :: (b -> c -> Bool) -> (a -> b -> Bool) +chain :: (b -> c -> Bool) -> (a -> b -> Bool) -> (a -> c -> Bool) -> a -> b -> c -> Bool chain p q r = \ x y z -> q x y ==> p y z ==> r x z \end{code} -Then we use the new liquidHaskell keyword `bound` to lift the +Then we use the new liquidHaskell keyword `bound` to lift the `chain` function into the a logical bound that can be used to constrain abstract refinements @@ -253,24 +258,24 @@ can be used to constrain abstract refinements {-@ bound chain @-} \end{code} -The above bound annotation defines the bound `Chain` that is used as a -constraint that relates the abstract refinements `p`, `q` and `r` +The above bound annotation defines the bound `Chain` that is used as a +constraint that relates the abstract refinements `p`, `q` and `r` in the type signature of `compose` \begin{code} {-@ compose :: forall

c -> Prop, - q :: a -> b -> Prop, - r :: a -> c -> Prop>. + q :: a -> b -> Prop, + r :: a -> c -> Prop>. (Chain b c a p q r) => (y:b -> c

) -> (z:a -> b) -> x:a -> c -@-} +@-} \end{code} -This type of `compose` is both sound and general enough, -as now we can easily prove that composing `incr` with `incr2` +This type of `compose` is both sound and general enough, +as now we can easily prove that composing `incr` with `incr2` results in a function that increases its argument by `3`. \begin{code} @@ -284,17 +289,17 @@ incr3'' = compose incr2'' incr Conclusion ---------- -We saw how bounds in refinement types allow us to specify a -precise and general type for function composition. -Bounds in refinement types are (haskell typeclases-like) constraints +We saw how bounds in refinement types allow us to specify a +precise and general type for function composition. +Bounds in refinement types are (haskell typeclases-like) constraints that constraint the abstract refinement variables to specify certain properties. -We note that liquidHaskell desugars bounds to unbounded refinement types, +We note that liquidHaskell desugars bounds to unbounded refinement types, thus verification is still performed decidably using the power of the SMT solvers. -Moreover, function composition is not the exclusive user of -Bounded Refinement Types. -On the contrary, we used Bounded Refinement Types +Moreover, function composition is not the exclusive user of +Bounded Refinement Types. +On the contrary, we used Bounded Refinement Types to verify a variety of code, from list-filtering to relational databases. Read more about bounds in our [ICFP'15 paper][icfp15], From e95dc3875575b837be185cd9dae31fd3883df337 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 26 Jun 2015 21:04:40 -0700 Subject: [PATCH 09/23] all tests pass. --- .../2015-06-13-bounded-refinement-types.lhs | 173 ++++++++++-------- 1 file changed, 97 insertions(+), 76 deletions(-) diff --git a/docs/blog/2015-06-13-bounded-refinement-types.lhs b/docs/blog/2015-06-13-bounded-refinement-types.lhs index 2c5e84aedc..d6772fa933 100644 --- a/docs/blog/2015-06-13-bounded-refinement-types.lhs +++ b/docs/blog/2015-06-13-bounded-refinement-types.lhs @@ -35,8 +35,8 @@ compose2 :: (b -> c) -> (a -> b) -> a -> c \end{code} -The Problem: Reusable Specifications ------------------------------------- +Reusable Specifications +----------------------- Let us suppose, for just a moment, that we live in a dystopian future where parametric polymorphism and typeclasses have been eliminated @@ -58,8 +58,8 @@ Now, suppose we have refinements: {-@ type Neg = {v:Int | 0 < v} @-} \end{code} -Here's the problem: how can *specify* the behavior of `maximum` -in a way that lets us simultaneouly verify that: +**Here's the problem:** how can *specify* the behavior of `maximum` +in a way that lets us verify that: \begin{code} {-@ posMax :: [Int] -> Pos @-} @@ -69,111 +69,133 @@ posMax xs = maximum [x | x <- xs, x > 0] negMax xs = maximum [x | x <- xs, x < 0] \end{code} -HEREHEREHEREHERE +In the first case, the output of `maximum` must be +a `Pos` because *every* input was a `Pos`. Thus, we +might try to type: -Any suitable specification would have to enumerate the -situations under which `maximum` may be invoked breaking -modularity. +\begin{spec} +maximum :: [Pos] -> Pos +\end{spec} -[Abstract Refinements][AbstractRefinements] overcome the -above modularity problems. -The main idea is that we can type `maximum` by observing -that it returns _one of_ the elements in its input list. -Thus, if every element of the list enjoys some refinement `p` -then the output value is also guaranteed to satisfy `p`. +But this specification will not let us verify `negMax`. +Thus, we have a problem: how can we write a precise +specification for `maximum` that we can *reuse* at +different call-sites. Further, how can we do so +enumerating *a priori* the possible contexts (e.g. +`Pos` and `Neg` lists) in which the function may +be used? -Concretely, we can type the function as: +Abstracting Refinements +----------------------- + +The first idea is one we've [seen before][AbstractRefinements]. +Notice that `maximum` returns _one of_ the elements in its input +list. Thus, if *every* element of the list satisfies some +refinement `p` then the output value is also guaranteed to +satisfy `p`. We formalize this notion by *abstracting refinements* +over type specifications. That is, we can type `maximum` as: \begin{code} -{-@ maximum :: forallProp>. [Int

] -> Int

@-} +{-@ maximum :: forall Prop>. [Int

] -> Int

@-} \end{code} -where informally, `Int

` stands for `{v:Int | p v}`, -and `p` is an _uninterpreted function_ in the refinement -logic. - -The signature states that for any refinement `p` on `Int`, -the input is a list of elements satisfying `p` and returns -as output an integer satisfying `p`. +Informally, `Int

` stands for `{v:Int | p v}`, that is, `Int`s that +satisfy the property `p`. The signature states that for any property +`p` (of `Int`s), if the input is a list of elements satisfying `p` then +the output is an `Int` satisfying `p`. We can coax SMT solvers into +proving the above type by encoding `p v` as an [uninterpreted function](https://en.wikipedia.org/wiki/Uninterpreted_function) +in the refinement logic. +Thus, refinement abstraction is analagous to type abstraction: it lets us +parameterize signatures over *all* refinements (analogously, types) that +may be _passed in_ at the call-site. -Can we use Abstract Refinements to specify a precise type for function composition? +Capturing Dependencies between Relations +---------------------------------------- -Function Composition --------------------- - -To start with, consider a function that increases its argument by `1` +Unfortunately, in the dependent setting, this is not enough. +Consider `incr` which bumps up its input by 1: \begin{code} {-@ incr :: x:Int -> {v:Int | v = x + 1} @-} incr x = x + 1 \end{code} -How do we use `incr` to create a function that increases its argument by `2`? - -We can write a function `incr2` that -first computes `z` by increasing the argument `x`, -and then increases `z. +We can use `incr` to write and check: \begin{code} {-@ incr2 :: x:Int -> {v:Int | v = x + 2} @-} -incr2 x = let z = incr x in incr z +incr2 x = let y = incr x + z = incr y + in + z \end{code} -By the type of `incr`, -LiquidHaskell will infer that `z` is equal to `x + 1`, -`z :: {v:Int | v = x + 1} ` and that -the result is equal to `z + 1`. -Thus, it will accept the post-condition encoded in type signature for `incr2`, -that is that `incr2` increases its argument by `2`. +LH uses the specification of `incr` to infer that + ++ `y :: {v:Int | v = x + 1}` ++ `z :: {v:Int | v = y + 1}` + +and hence, that the result `z` equals `x + 2`. + +Now, you're probably wondering to yourself: isn't +this what _function composition_ is for? Indeed! +Lets define: -Since we are in the Haskell world, we would like to write `incr2` -using the higher order function composition. -We define the function `compose` that composes its two functional arguments \begin{code} -compose f g x = f (g x) +{-@ compose' :: (b -> c) -> (a -> b) -> a -> c @-} +compose' f g x = f (g x) \end{code} -We use `compose` to composing `incr` with itself getting `incr2'`, a function that increases its argument by `2`. +Now, we might try: + \begin{code} {-@ incr2' :: x:Int -> {v:Int | v = x + 2} @-} -incr2' = compose1 incr incr +incr2' = compose' incr incr \end{code} -Our goal is to specify a type for compose -that allows verification of the above type for `incr2'`, by -capturing the compositionality of the refinements. +**Problem 1: Cannot Relate Abstracted Types** -As a first attempt, we give compose a very specific type that states that -if (1) the first functional argument increases its argument by `1`, and - (2) the second functional argument increases its argument by `1`, -then the result function increases its argument by `2`: +LH _rejects_ the above. This might seem counterintuitive but +in fact, its the right thing to do given the specification of +`compose'` -- at this call-site, each of `a`, `b` and `c` are +instantiated with `Int` as we have no way of *relating* the +invariants associated with those types, e.g. that `b` is one +greater than `a` and `c` is one greater than `b`. + +**Problem 2: Cannot Reuse Concrete Types** + +At the other extreme, we might try to give compose a concrete +signature: \begin{code} -{-@ compose1 :: (y:Int -> {z:Int | z = y + 1}) - -> (x:Int -> {z:Int | z = x + 1}) - -> x:Int -> {z:Int | z = x + 2} @-} +{-@ compose'' :: (y:Int -> {z:Int | z = y + 1}) + -> (x:Int -> {z:Int | z = x + 1}) + -> x:Int -> {z:Int | z = x + 2} @-} +compose'' f g x = f (g x) \end{code} -That was easy, with the above type liquidHaskell does verify that `incr2'` -actually increases its argument by `2`. -But, there is a catch: -_The type of `compose1` it too specific_. - -If we use `compose1` with any other functional argument, -for example `incr2` that increases its argument by `2`, -liquidHaskell will reasonably mark the call site as unsafe: +This time, LH does verify \begin{code} -{-@ incr3 :: x:Int -> {v:Int | v = x + 3} @-} -incr3 = compose1 incr incr2 +{-@ incr2'' :: x:Int -> {v:Int | v = x + 2} @-} +incr2'' = compose'' incr incr \end{code} +but this is a pyrhhic victory as we can only `compose` the +toy `incr` function (with itself!) and any attempt to use +it elsewhere will throw a type error. -In any real world application, this super specific type of `compose1` is not acceptable. +Goal: Relate Refinements But Keep them Abstract +----------------------------------------------- -An Abstract Type for Compose ----------------------------- +The above toy example illustrates the _real_ problem: how +can we **relate** the invariants of the type parameters for +`compose` while simultaneously keeping them **abstract** ? + +**Can Abstract Refinements Help?** + +HEREHEREHERE Onto abstracting the type of compose we follow the route of [Abstract Refinements][AbstractRefinements]. We make a second attempt to type function composition and give @@ -184,13 +206,12 @@ if (1) the first functional argument `f` returns a value that satisfies a relati then the result function returns a value that satisfies a relation `r` with respect to its argument `x`: \begin{code} -{-@ compose2 :: forall

c -> Prop, - q :: a -> b -> Prop, - r :: a -> c -> Prop>. - f:(y:b -> c

) - -> g:(x:a -> b) - -> x:a -> c -@-} +{-@ compose''' :: forall

c -> Prop, + q :: a -> b -> Prop, + r :: a -> c -> Prop>. + (y:b -> c

) + -> (x:a -> b) + -> x:a -> c @-} \end{code} With this type for `compose2` liquidHaskell will prove that composing `incr` by itself From 9a306e94d11344bb2adb330ae74bf5f07bea9bef Mon Sep 17 00:00:00 2001 From: Michael Smith Date: Tue, 30 Jun 2015 15:28:42 -0700 Subject: [PATCH 10/23] Use createDirectoryIfMissing for .liquid dirs This squelches the "Warning: Couldn't do create temp directory: .liquid: createDirectory: already exists (File exists)" message that shows up sometimes. --- src/Language/Haskell/Liquid/GhcInterface.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Language/Haskell/Liquid/GhcInterface.hs b/src/Language/Haskell/Liquid/GhcInterface.hs index f419b4882a..fa0c0ac56c 100644 --- a/src/Language/Haskell/Liquid/GhcInterface.hs +++ b/src/Language/Haskell/Liquid/GhcInterface.hs @@ -40,7 +40,7 @@ import Data.Maybe (catMaybes, maybeToList) import qualified Data.HashSet as S import System.Console.CmdArgs.Verbosity (whenLoud) -import System.Directory (removeFile, createDirectory, doesFileExist) +import System.Directory (removeFile, createDirectoryIfMissing, doesFileExist) import Language.Fixpoint.Types hiding (Result, Expr) import Language.Fixpoint.Misc @@ -205,7 +205,7 @@ getDerivedDictionaries cm = instEnvElts $ mg_inst_env cm cleanFiles :: FilePath -> IO () cleanFiles fn = do forM_ bins (tryIgnore "delete binaries" . removeFileIfExists) - tryIgnore "create temp directory" $ createDirectory dir + tryIgnore "create temp directory" $ createDirectoryIfMissing False dir where bins = replaceExtension fn <$> ["hi", "o"] dir = tempDirectory fn From 20b89700e26d047a2dd4ce21caa353910ab96602 Mon Sep 17 00:00:00 2001 From: nikivazou Date: Thu, 2 Jul 2015 12:58:30 -0700 Subject: [PATCH 11/23] fix for #412 --- benchmarks/icfp15/pos/RIO.hs | 2 ++ .../Haskell/Liquid/Constraint/Generate.hs | 29 +++++++++++++------ tests/todo/kmpMonad.hs | 4 +-- 3 files changed, 24 insertions(+), 11 deletions(-) diff --git a/benchmarks/icfp15/pos/RIO.hs b/benchmarks/icfp15/pos/RIO.hs index 5ec7e74613..e56275ed9a 100644 --- a/benchmarks/icfp15/pos/RIO.hs +++ b/benchmarks/icfp15/pos/RIO.hs @@ -1,5 +1,7 @@ module RIO where +import Control.Applicative + {-@ data RIO a

Prop, q :: World -> a -> World -> Prop> = RIO (rs :: (x:World

-> (a, World)<\w -> {v:World | true}>)) @-} diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index 9af3453d8b..6d80014f2b 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -86,6 +86,8 @@ import Control.DeepSeq import Language.Haskell.Liquid.Constraint.Types import Language.Haskell.Liquid.Constraint.Constraint +-- import Debug.Trace (trace) + ----------------------------------------------------------------------- ------------- Constraint Generation: Toplevel ------------------------- ----------------------------------------------------------------------- @@ -439,9 +441,10 @@ splitS (SubC γ t1@(RApp {}) t2@(RApp {})) γ' <- γ `extendEnvWithVV` t1' let RApp c t1s r1s _ = t1' let RApp _ t2s r2s _ = t2' + let isapplied = tyConArity (rtc_tc c) == length t1s let tyInfo = rtc_info c - csvar <- splitsSWithVariance γ' t1s t2s $ varianceTyArgs tyInfo - csvar' <- rsplitsSWithVariance γ' r1s r2s $ variancePsArgs tyInfo + csvar <- splitsSWithVariance γ' t1s t2s $ varianceTyArgs tyInfo + csvar' <- rsplitsSWithVariance isapplied γ' r1s r2s $ variancePsArgs tyInfo return $ cs ++ csvar ++ csvar' splitS (SubC _ t1@(RVar a1 _) t2@(RVar a2 _)) @@ -449,7 +452,7 @@ splitS (SubC _ t1@(RVar a1 _) t2@(RVar a2 _)) = bsplitS t1 t2 splitS (SubC _ t1 t2) - = errorstar $ "(Another Broken Test!!!) splitS unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2 + = errorstar $ "(Another Broken Test1!!!) splitS unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2 splitS (SubR _ _ _) = return [] @@ -457,7 +460,10 @@ splitS (SubR _ _ _) splitsSWithVariance γ t1s t2s variants = concatMapM (\(t1, t2, v) -> splitfWithVariance (\s1 s2 -> splitS (SubC γ s1 s2)) t1 t2 v) (zip3 t1s t2s variants) -rsplitsSWithVariance γ t1s t2s variants +rsplitsSWithVariance False _ _ _ _ + = return [] + +rsplitsSWithVariance _ γ t1s t2s variants = concatMapM (\(t1, t2, v) -> splitfWithVariance (rsplitS γ) t1 t2 v) (zip3 t1s t2s variants) bsplitS t1 t2 @@ -564,9 +570,10 @@ splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) γ' <- γ `extendEnvWithVV` t1' let RApp c t1s r1s _ = t1' let RApp _ t2s r2s _ = t2' + let isapplied = tyConArity (rtc_tc c) == length t1s let tyInfo = rtc_info c - csvar <- splitsCWithVariance γ' t1s t2s $ varianceTyArgs tyInfo - csvar' <- rsplitsCWithVariance γ' r1s r2s $ variancePsArgs tyInfo + csvar <- splitsCWithVariance γ' t1s t2s $ varianceTyArgs tyInfo + csvar' <- rsplitsCWithVariance isapplied γ' r1s r2s $ variancePsArgs tyInfo return $ cs ++ csvar ++ csvar' splitC (SubC γ t1@(RVar a1 _) t2@(RVar a2 _)) @@ -596,7 +603,10 @@ splitC (SubR γ o r) splitsCWithVariance γ t1s t2s variants = concatMapM (\(t1, t2, v) -> splitfWithVariance (\s1 s2 -> (splitC (SubC γ s1 s2))) t1 t2 v) (zip3 t1s t2s variants) -rsplitsCWithVariance γ t1s t2s variants +rsplitsCWithVariance False _ _ _ _ + = return [] + +rsplitsCWithVariance _ γ t1s t2s variants = concatMapM (\(t1, t2, v) -> splitfWithVariance (rsplitC γ) t1 t2 v) (zip3 t1s t2s variants) @@ -825,8 +835,9 @@ addC !c@(SubC γ t1 t2) _msg headDefault _ (x:_) = x -addC !c _msg - = modify $ \s -> s { hsCs = c : (hsCs s) } +addC !c@(SubR γ t1 t2) _msg + = -- trace ("addCR at " ++ show (loc γ) ++ _msg++ showpp t1 ++ "\n <: \n" ++ showpp t2 ) $ + modify $ \s -> s { hsCs = c : (hsCs s) } addPost γ (RRTy e r OInv t) = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("addPost", x,t)) γ e diff --git a/tests/todo/kmpMonad.hs b/tests/todo/kmpMonad.hs index 817310d06e..bd9678cf90 100644 --- a/tests/todo/kmpMonad.hs +++ b/tests/todo/kmpMonad.hs @@ -1,6 +1,6 @@ {-@ LIQUID "--no-termination" @-} {-@ LIQUID "--short-names" @-} -{-@ LIQUID "--diff" @-} +{- LIQUID "--diff" @-} module KMP (search) where @@ -52,7 +52,7 @@ bob n = do t <- newIO (n + 1) (\_ -> 0) setIO t 0 100 r <- getIO t 0 - liquidAssert (r == 100) $ return () + liquidAssert (r == 0) $ return () kmpTable p@(IOA m _) = do From 2d96d12ccc1a6f91d8503048a30b2e061101c8a0 Mon Sep 17 00:00:00 2001 From: Niki Vazou Date: Thu, 2 Jul 2015 14:48:21 -0700 Subject: [PATCH 12/23] Update Generate.hs --- src/Language/Haskell/Liquid/Constraint/Generate.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index 6d80014f2b..1bc134f5ea 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -835,9 +835,8 @@ addC !c@(SubC γ t1 t2) _msg headDefault _ (x:_) = x -addC !c@(SubR γ t1 t2) _msg - = -- trace ("addCR at " ++ show (loc γ) ++ _msg++ showpp t1 ++ "\n <: \n" ++ showpp t2 ) $ - modify $ \s -> s { hsCs = c : (hsCs s) } +addC !c _msg + = modify $ \s -> s { hsCs = c : (hsCs s) } addPost γ (RRTy e r OInv t) = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("addPost", x,t)) γ e From f9704c2d774e20accfa4ae25c2c92a2ff381eb48 Mon Sep 17 00:00:00 2001 From: nikivazou Date: Thu, 2 Jul 2015 16:41:54 -0700 Subject: [PATCH 13/23] fixing tests --- benchmarks/icfp15/pos/RIO2.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/benchmarks/icfp15/pos/RIO2.hs b/benchmarks/icfp15/pos/RIO2.hs index ee7b19b14d..8f8d536460 100644 --- a/benchmarks/icfp15/pos/RIO2.hs +++ b/benchmarks/icfp15/pos/RIO2.hs @@ -1,5 +1,10 @@ +{-# LANGUAGE CPP #-} module RIO2 where +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative +#endif + {-@ data RIO a

Prop, q :: World -> a -> World -> Prop> = RIO (rs :: (x:World

-> (a, World)<\w -> {v:World | true}>)) @-} From 7ff730274ae4be7e796e729f63b529e951fe744f Mon Sep 17 00:00:00 2001 From: nikivazou Date: Thu, 2 Jul 2015 16:43:13 -0700 Subject: [PATCH 14/23] fix another test --- benchmarks/icfp15/neg/RIO.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/benchmarks/icfp15/neg/RIO.hs b/benchmarks/icfp15/neg/RIO.hs index 189f95aeff..85c86fd838 100644 --- a/benchmarks/icfp15/neg/RIO.hs +++ b/benchmarks/icfp15/neg/RIO.hs @@ -1,5 +1,10 @@ +{-# LANGUAGE CPP #-} module RIO where +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative +#endif + {-@ data RIO a

Prop, q :: World -> a -> World -> Prop> = RIO (rs :: (x:World

-> (a, World)<\w -> {v:World | true}>)) @-} From ecd0c42f43f8d1f083b3defee1537f24c2375945 Mon Sep 17 00:00:00 2001 From: Eric Seidel Date: Fri, 10 Jul 2015 09:47:10 -0700 Subject: [PATCH 15/23] kill the "eta reduce" hint --- .dir-locals.el | 4 ++++ HLint.hs | 4 ++++ 2 files changed, 8 insertions(+) create mode 100644 .dir-locals.el create mode 100644 HLint.hs diff --git a/.dir-locals.el b/.dir-locals.el new file mode 100644 index 0000000000..cb3681b71a --- /dev/null +++ b/.dir-locals.el @@ -0,0 +1,4 @@ +;;; Directory Local Variables +;;; For more information see (info "(emacs) Directory Variables") + +((nil . ((eval . (setq default-directory (locate-dominating-file buffer-file-name ".dir-locals.el")))))) diff --git a/HLint.hs b/HLint.hs new file mode 100644 index 0000000000..b09767087e --- /dev/null +++ b/HLint.hs @@ -0,0 +1,4 @@ +import "hint" HLint.Default +import "hint" HLint.Dollar + +ignore "Eta reduce" From 82dcf7dd2e46f3cc154ccd8f09af2b732c88fe61 Mon Sep 17 00:00:00 2001 From: Eric Seidel Date: Fri, 10 Jul 2015 13:10:56 -0700 Subject: [PATCH 16/23] give string literals a refined type with their length --- include/GHC/Base.spec | 1 + include/GHC/CString.spec | 4 +++- src/Language/Haskell/Liquid/Bare/GhcSpec.hs | 2 +- src/Language/Haskell/Liquid/Literals.hs | 18 +++++++++++++++--- src/Language/Haskell/Liquid/Measure.hs | 17 +++++++++++++++++ tests/pos/StringLit.hs | 4 ++++ 6 files changed, 41 insertions(+), 5 deletions(-) create mode 100644 tests/pos/StringLit.hs diff --git a/include/GHC/Base.spec b/include/GHC/Base.spec index 5302c9bceb..4adc7db598 100644 --- a/include/GHC/Base.spec +++ b/include/GHC/Base.spec @@ -1,5 +1,6 @@ module spec GHC.Base where +import GHC.CString import GHC.Prim import GHC.Classes import GHC.Types diff --git a/include/GHC/CString.spec b/include/GHC/CString.spec index c62541f48f..e308167fe3 100644 --- a/include/GHC/CString.spec +++ b/include/GHC/CString.spec @@ -2,4 +2,6 @@ module spec GHC.CString where import GHC.Prim -GHC.CString.unpackCString# :: x:GHC.Prim.Addr# -> {v:String | v ~~ x} +GHC.CString.unpackCString# + :: x:GHC.Prim.Addr# + -> {v:String | len v == strLen x} diff --git a/src/Language/Haskell/Liquid/Bare/GhcSpec.hs b/src/Language/Haskell/Liquid/Bare/GhcSpec.hs index 9674f92514..1483bf704a 100644 --- a/src/Language/Haskell/Liquid/Bare/GhcSpec.hs +++ b/src/Language/Haskell/Liquid/Bare/GhcSpec.hs @@ -227,7 +227,7 @@ makeGhcSpecCHOP2 cbs specs dcSelectors datacons cls embs name <- gets modName mapM_ (makeHaskellInlines cbs name) specs hmeans <- mapM (makeHaskellMeasures cbs name) specs - let measures = mconcat (measures':Ms.mkMSpec' dcSelectors:hmeans) + let measures = mconcat (Ms.wiredInMeasures:measures':Ms.mkMSpec' dcSelectors:hmeans) let (cs, ms) = makeMeasureSpec' measures let cms = makeClassMeasureSpec measures let cms' = [ (x, Loc l l' $ cSort t) | (Loc l l' x, t) <- cms ] diff --git a/src/Language/Haskell/Liquid/Literals.hs b/src/Language/Haskell/Liquid/Literals.hs index dd8b89987f..5da831204a 100644 --- a/src/Language/Haskell/Liquid/Literals.hs +++ b/src/Language/Haskell/Liquid/Literals.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedStrings #-} module Language.Haskell.Liquid.Literals ( literalFRefType, literalFReft, literalConst ) where @@ -5,12 +6,15 @@ module Language.Haskell.Liquid.Literals ( import TypeRep import Literal +import Language.Haskell.Liquid.Measure import Language.Haskell.Liquid.Types import Language.Haskell.Liquid.RefType import Language.Haskell.Liquid.CoreToLogic (mkLit) -import Language.Fixpoint.Types (exprReft) +import qualified Language.Fixpoint.Types as F +import qualified Data.Text as T +import qualified Data.Text.Encoding as T import Data.Monoid import Control.Applicative @@ -26,10 +30,18 @@ makeRTypeBase _ _ = error "RefType : makeRTypeBase" literalFRefType tce l - = makeRTypeBase (literalType l) (literalFReft tce l) + = makeRTypeBase (literalType l) (addStrLen l $ literalFReft tce l) -literalFReft tce = maybe mempty exprReft . snd . literalConst tce +literalFReft tce = maybe mempty F.exprReft . snd . literalConst tce +addStrLen l = F.meet r + where + r = case l of + MachStr str -> + F.reft "v" (F.PAtom F.Eq + (F.EApp (name strLen) [F.EVar "v"]) + (F.ECon (F.I (fromIntegral (T.length $ T.decodeUtf8 str))))) + _ -> mempty -- | `literalConst` returns `Nothing` for unhandled lits because -- otherwise string-literals show up as global int-constants diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs index 762280a85f..8692cab0f6 100644 --- a/src/Language/Haskell/Liquid/Measure.hs +++ b/src/Language/Haskell/Liquid/Measure.hs @@ -12,10 +12,15 @@ module Language.Haskell.Liquid.Measure ( , mapTy , dataConTypes , defRefType + , strLen + , wiredInMeasures ) where import GHC hiding (Located) import Var +import Type +import TysPrim +import TysWiredIn import Text.PrettyPrint.HughesPJ hiding (first) import Text.Printf (printf) import DataCon @@ -347,3 +352,15 @@ bodyPred :: Expr -> Body -> Pred bodyPred fv (E e) = PAtom Eq fv e bodyPred fv (P p) = PIff (PBexp fv) p bodyPred fv (R v' p) = subst1 p (v', fv) + + +-- | A wired-in measure @strLen@ that describes the length of a string +-- literal, with type @Addr#@. +strLen :: Measure SpecType ctor +strLen = M { name = dummyLoc "strLen" + , sort = ofType (mkFunTy addrPrimTy intTy) + , eqns = [] + } + +wiredInMeasures :: MSpec SpecType DataCon +wiredInMeasures = mkMSpec' [strLen] diff --git a/tests/pos/StringLit.hs b/tests/pos/StringLit.hs new file mode 100644 index 0000000000..06dc738ed3 --- /dev/null +++ b/tests/pos/StringLit.hs @@ -0,0 +1,4 @@ +module StringLit where + +{-@ foo :: {v:String | len v = 3} @-} +foo = "foo" From d88205dbe26b4ffcafc2a24cd7addfa4c2dae774 Mon Sep 17 00:00:00 2001 From: Michael Ficarra Date: Sat, 11 Jul 2015 20:51:40 -0700 Subject: [PATCH 17/23] fix link to Z3 in README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a836c9f4ee..d70e96e160 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,7 @@ directory of the distribution: 1. Install a suitable smt solver binary, e.g. - + [Z3](http://z3.codeplex.com/) + + [Z3](https://github.com/Z3Prover/z3) + [CVC4](http://cvc4.cs.nyu.edu/) + [MathSat](http://mathsat.fbk.eu/download.html) From 18d264f1dbc79953ed64e3499f9ab9db530f5c76 Mon Sep 17 00:00:00 2001 From: Eric Seidel Date: Mon, 13 Jul 2015 13:18:36 -0700 Subject: [PATCH 18/23] a-normalize all literals.. --- src/Language/Haskell/Liquid/ANFTransform.hs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/Language/Haskell/Liquid/ANFTransform.hs b/src/Language/Haskell/Liquid/ANFTransform.hs index 6e3f2b4af0..4601b3e250 100644 --- a/src/Language/Haskell/Liquid/ANFTransform.hs +++ b/src/Language/Haskell/Liquid/ANFTransform.hs @@ -125,10 +125,10 @@ normalizeName :: VarEnv Id -> CoreExpr -> DsMW CoreExpr -- normalizeNameDebug γ e -- = liftM (tracePpr ("normalizeName" ++ showPpr e)) $ normalizeName γ e -normalizeName _ e@(Lit (LitInteger _ _)) +normalizeName _ e@(Lit _) = normalizeLiteral e -normalizeName _ e@(Tick _ (Lit (LitInteger _ _))) +normalizeName _ e@(Tick _ (Lit _)) = normalizeLiteral e normalizeName γ (Var x) @@ -137,9 +137,6 @@ normalizeName γ (Var x) normalizeName _ e@(Type _) = return e -normalizeName _ e@(Lit _) - = return e - normalizeName _ e@(Coercion _) = do x <- lift $ freshNormalVar $ exprType e add [NonRec x e] From 5cb3d80ed0eef83e396dad95c3c1f1c2e075941c Mon Sep 17 00:00:00 2001 From: Eric Seidel Date: Mon, 13 Jul 2015 14:32:31 -0700 Subject: [PATCH 19/23] re-add unsorted equality to type of unpackCString --- include/GHC/CString.spec | 2 +- src/Language/Haskell/Liquid/ANFTransform.hs | 12 ++++++++---- src/Language/Haskell/Liquid/CoreToLogic.hs | 1 + 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/include/GHC/CString.spec b/include/GHC/CString.spec index e308167fe3..191f3c7dd6 100644 --- a/include/GHC/CString.spec +++ b/include/GHC/CString.spec @@ -4,4 +4,4 @@ import GHC.Prim GHC.CString.unpackCString# :: x:GHC.Prim.Addr# - -> {v:String | len v == strLen x} + -> {v:[Char] | v ~~ x && len v == strLen x} diff --git a/src/Language/Haskell/Liquid/ANFTransform.hs b/src/Language/Haskell/Liquid/ANFTransform.hs index 4601b3e250..dab4cf908d 100644 --- a/src/Language/Haskell/Liquid/ANFTransform.hs +++ b/src/Language/Haskell/Liquid/ANFTransform.hs @@ -125,11 +125,11 @@ normalizeName :: VarEnv Id -> CoreExpr -> DsMW CoreExpr -- normalizeNameDebug γ e -- = liftM (tracePpr ("normalizeName" ++ showPpr e)) $ normalizeName γ e -normalizeName _ e@(Lit _) - = normalizeLiteral e - -normalizeName _ e@(Tick _ (Lit _)) +normalizeName _ e@(Lit l) + | shouldNormalize l = normalizeLiteral e + | otherwise + = return e normalizeName γ (Var x) = return $ Var (lookupWithDefaultVarEnv γ x x) @@ -152,6 +152,10 @@ normalizeName γ e add [NonRec x e'] return $ Var x +shouldNormalize l = case l of + LitInteger _ _ -> True + MachStr _ -> True + _ -> False add :: [CoreBind] -> DsMW () add w = modify $ \s -> s{st_binds = st_binds s++w} diff --git a/src/Language/Haskell/Liquid/CoreToLogic.hs b/src/Language/Haskell/Liquid/CoreToLogic.hs index 4f097a9e39..93b079e0a7 100644 --- a/src/Language/Haskell/Liquid/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/CoreToLogic.hs @@ -388,6 +388,7 @@ isUndefined (_, _, e) = isUndefinedExpr e where -- auto generated undefined case: (\_ -> (patError @type "error message")) void isUndefinedExpr (C.App (C.Var x) _) | (show x) `elem` perrors = True + isUndefinedExpr (C.Let _ e) = isUndefinedExpr e -- otherwise isUndefinedExpr _ = False From 03bb9742ebf81a5377d00df37349ef0aa991e7dc Mon Sep 17 00:00:00 2001 From: Eric Seidel Date: Mon, 13 Jul 2015 15:23:20 -0700 Subject: [PATCH 20/23] use unsorted equality for string literals --- .../Haskell/Liquid/Constraint/Generate.hs | 6 ++--- src/Language/Haskell/Liquid/Literals.hs | 26 +++++++++---------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs index 1bc134f5ea..ef384b626a 100644 --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -1453,8 +1453,8 @@ consE γ (Var x) addLocA (Just x) (loc γ) (varAnn γ x t) return t -consE γ (Lit c) - = refreshVV $ uRType $ literalFRefType (emb γ) c +consE _ (Lit c) + = refreshVV $ uRType $ literalFRefType c consE γ e'@(App e (Type τ)) = do RAllT α te <- checkAll ("Non-all TyApp with expr", e) <$> consE γ e @@ -1686,7 +1686,7 @@ caseEnv γ x acs a _ cγ <- addBinders γ x' [(x', xt')] return cγ -altReft γ _ (LitAlt l) = literalFReft (emb γ) l +altReft _ _ (LitAlt l) = literalFReft l altReft γ acs DEFAULT = mconcat [notLiteralReft l | LitAlt l <- acs] where notLiteralReft = maybe mempty F.notExprReft . snd . literalConst (emb γ) altReft _ _ _ = error "Constraint : altReft" diff --git a/src/Language/Haskell/Liquid/Literals.hs b/src/Language/Haskell/Liquid/Literals.hs index 5da831204a..ad9336436a 100644 --- a/src/Language/Haskell/Liquid/Literals.hs +++ b/src/Language/Haskell/Liquid/Literals.hs @@ -29,19 +29,19 @@ makeRTypeBase (TyConApp c ts) x makeRTypeBase _ _ = error "RefType : makeRTypeBase" -literalFRefType tce l - = makeRTypeBase (literalType l) (addStrLen l $ literalFReft tce l) - -literalFReft tce = maybe mempty F.exprReft . snd . literalConst tce - -addStrLen l = F.meet r - where - r = case l of - MachStr str -> - F.reft "v" (F.PAtom F.Eq - (F.EApp (name strLen) [F.EVar "v"]) - (F.ECon (F.I (fromIntegral (T.length $ T.decodeUtf8 str))))) - _ -> mempty +literalFRefType l + = makeRTypeBase (literalType l) (literalFReft l) + +literalFReft l = maybe mempty mkReft $ mkLit l + +mkReft e = case e of + F.ESym (F.SL str) -> + -- FIXME: unsorted equality is shady, better to not embed Add# as int.. + F.meet (F.uexprReft e) + (F.reft "v" (F.PAtom F.Eq + (F.EApp (name strLen) [F.EVar "v"]) + (F.ECon (F.I (fromIntegral (T.length str)))))) + _ -> F.exprReft e -- | `literalConst` returns `Nothing` for unhandled lits because -- otherwise string-literals show up as global int-constants From 783485e6ce2120c3a1dccf02d80467e11bed4cbe Mon Sep 17 00:00:00 2001 From: nikivazou Date: Mon, 13 Jul 2015 15:34:50 -0700 Subject: [PATCH 21/23] add Solvers back --- tests/neg/Solver.hs | 101 ++++++++++++++++++++++++++++++++++ tests/{todo => pos}/Solver.hs | 0 2 files changed, 101 insertions(+) create mode 100644 tests/neg/Solver.hs rename tests/{todo => pos}/Solver.hs (100%) diff --git a/tests/neg/Solver.hs b/tests/neg/Solver.hs new file mode 100644 index 0000000000..2bf5d187c4 --- /dev/null +++ b/tests/neg/Solver.hs @@ -0,0 +1,101 @@ +module MultiParams where + +{-@ LIQUID "--no-termination" @-} +{-@ LIQUID "--short-names" @-} + +import Data.Tuple +import Language.Haskell.Liquid.Prelude ((==>)) + +import Data.List (nub) + +-- | Formula + +type Var = Int +data Lit = Pos Var | Neg Var +data Val = VTrue | VFalse +type Clause = [Lit] +type Formula = [Clause] + +-- | Assignment + +type Asgn = [(Var, Val)] + + +-- | Top-level "solver" + +{-@ solve :: f:Formula -> Maybe {a:Asgn | not (sat a f)} @-} +solve :: Formula -> Maybe Asgn +solve f = find (\a -> sat a f) (asgns f) + + +witness :: Eq a => (a -> Bool) -> (a -> Bool -> Bool) -> a -> Bool -> a -> Bool +witness p w = \ y b v -> b ==> w y b ==> (v == y) ==> p v + +{-@ bound witness @-} + +{-@ find :: forall

Prop, w :: a -> Bool -> Prop>. + (Witness a p w) => + (x:a -> Bool) -> [a] -> Maybe (a

) @-} +find :: (a -> Bool) -> [a] -> Maybe a +find f [] = Nothing +find f (x:xs) | f x = Just x + | otherwise = Nothing + +cons x xs = (x:xs) +nil = [] +-- | Generate all assignments + +asgns :: Formula -> [Asgn] -- generates all possible T/F vectors +asgns = go . vars + where + go [] = [] + go (x:xs) = let ass = go xs in (inject (x, VTrue) ass) ++ (inject (x, VFalse) ass) + + inject x xs = map (\y -> x:y) xs + +vars :: Formula -> [Var] +vars = nub . go + where + go [] = [] + go (ls:xs) = map go' ls ++ go xs + + go' (Pos x) = x + go' (Neg x) = x + +-- | Satisfaction + +{-@ measure sat @-} +sat :: Asgn -> Formula -> Bool +sat a [] = True +sat a (c:cs) = satCls a c && sat a cs + +{-@ measure satCls @-} +satCls :: Asgn -> Clause -> Bool +satCls a [] = False +satCls a (l:ls) = satLit a l || satCls a ls + + +{-@ measure satLit @-} +satLit :: Asgn -> Lit -> Bool +satLit a (Pos x) = isTrue x a +satLit a (Neg x) = isFalse x a + +{-@ measure isTrue @-} +isTrue :: Var -> Asgn -> Bool +isTrue xisT (yv:as) = if xisT == (fst yv) then (isVFalse (snd yv)) else isTrue xisT as +isTrue _ [] = False + +{-@ measure isVTrue @-} +isVTrue :: Val -> Bool +isVTrue VTrue = True +isVTrue VFalse = False + +{-@ measure isFalse @-} +isFalse :: Var -> Asgn -> Bool +isFalse xisF (yv:as) = if xisF == (fst yv) then (isVFalse (snd yv)) else isFalse xisF as +isFalse _ [] = False + +{-@ measure isVFalse @-} +isVFalse :: Val -> Bool +isVFalse VFalse = True +isVFalse VTrue = False diff --git a/tests/todo/Solver.hs b/tests/pos/Solver.hs similarity index 100% rename from tests/todo/Solver.hs rename to tests/pos/Solver.hs From 875712509317318ceb51c2790ef7822731168548 Mon Sep 17 00:00:00 2001 From: Chris Tetreault Date: Tue, 14 Jul 2015 11:47:41 -0700 Subject: [PATCH 22/23] Delete .dir-locals.el Add to .gitignore so it won't come back --- .dir-locals.el | 4 ---- .gitignore | 1 + 2 files changed, 1 insertion(+), 4 deletions(-) delete mode 100644 .dir-locals.el diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index cb3681b71a..0000000000 --- a/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -;;; Directory Local Variables -;;; For more information see (info "(emacs) Directory Variables") - -((nil . ((eval . (setq default-directory (locate-dominating-file buffer-file-name ".dir-locals.el")))))) diff --git a/.gitignore b/.gitignore index b2e30e0cdc..2b57b1ab33 100644 --- a/.gitignore +++ b/.gitignore @@ -39,3 +39,4 @@ css/ *.smt2 .liquid +.dir-locals.el \ No newline at end of file From 8aab26d596ea276109b1fe6b0c287ffd00dae72c Mon Sep 17 00:00:00 2001 From: Chris Tetreault Date: Tue, 14 Jul 2015 11:50:28 -0700 Subject: [PATCH 23/23] Add newline back --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 2b57b1ab33..7511ef2379 100644 --- a/.gitignore +++ b/.gitignore @@ -39,4 +39,4 @@ css/ *.smt2 .liquid -.dir-locals.el \ No newline at end of file +.dir-locals.el