Skip to content

Commit

Permalink
asd Merge branch 'master' of github.com:ucsd-progsys/liquidhaskell
Browse files Browse the repository at this point in the history
  • Loading branch information
ranjitjhala committed Jul 14, 2015
2 parents ea5f9b9 + 99d6783 commit c681594
Show file tree
Hide file tree
Showing 30 changed files with 751 additions and 483 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -39,3 +39,4 @@ css/

*.smt2
.liquid
.dir-locals.el
4 changes: 4 additions & 0 deletions HLint.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
import "hint" HLint.Default
import "hint" HLint.Dollar

ignore "Eta reduce"
20 changes: 18 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -81,11 +83,25 @@ 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



lint:
hlint --colour --report .

Expand Down
11 changes: 6 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -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.
Expand Down
11 changes: 11 additions & 0 deletions TODO.markdown
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
60 changes: 30 additions & 30 deletions benchmarks/icfp15/neg/DBMovies.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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] @-}
Expand All @@ -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) @-}

Expand All @@ -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

Expand Down Expand Up @@ -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 @-}
Expand All @@ -146,7 +146,7 @@ mk_star_table s = [("star" := s) += empty]
-------------------------------------------------------------------------------


{-@ measure toInt :: Value -> Int
{-@ measure toInt :: Value -> Int
toInt(I n) = n
@-}

Expand Down
Loading

0 comments on commit c681594

Please sign in to comment.