asd Merge branch 'develop' of github.com:ucsd-progsys/liquidhaskell i…

…nto develop

INSTALL.md

@@ -51,6 +51,7 @@ This requires that you have installed [stack][stack] (which we strongly recommen
 
     cabal sandbox init
     cabal sandbox add-source ./liquid-fixpoint
+    cabal sandbox add-source ./liquiddesugar
     cabal install
 
 ## Troubleshooting

README.md

@@ -3,6 +3,10 @@
 
 [![Hackage](https://img.shields.io/hackage/v/liquidhaskell.svg)](https://hackage.haskell.org/package/liquidhaskell) [![Hackage-Deps](https://img.shields.io/hackage-deps/v/liquidhaskell.svg)](http://packdeps.haskellers.com/feed?needle=liquidhaskell) [![Build Status](https://img.shields.io/circleci/project/ucsd-progsys/liquidhaskell/master.svg)](https://circleci.com/gh/ucsd-progsys/liquidhaskell)
 
+Main Web site
+-------------
+
+The UCSD web site for liquid haskell is [here](https://ucsd-progsys.github.io/liquidhaskell-blog/)
 
 Examples
 --------

TODO.markdown

@@ -1,4 +1,8 @@
-- CHECK IF DEFAULT OPTION STAYS (ie on nunberic should not do rewrite)
+- Reader 
+  - Applicative crashing 
+  - Functor crashing 
+  - Functor.NoEx 
+  - Monad (...)
 
 TODO
 ====

benchmarks/pldi17/pos/ApplicativeList.hs

@@ -119,12 +119,15 @@ composition xss@(C x xs) yss@(C y ys) zss@(C z zs)
          ==. seq xss (seq yss zss)
 
 composition N yss zss
-   = toProof $
-      seq (seq (seq (pure compose) N) yss) zss
-        ==. seq (seq N yss) zss                  ? seq_nill (pure compose)
-        ==. seq N zss
-        ==. N
-        ==. seq N (seq yss zss)
+   =   seq (seq (seq (pure compose) N) yss) zss  
+   ==. seq (seq (seq (C compose N) N) yss) zss
+   ==. seq (seq (append (fmap compose N) (seq N N)) yss) zss
+   ==. seq (seq (append N (seq N N)) yss) zss
+   ==. seq (seq (seq N N) yss) zss
+   ==. seq (seq N yss) zss
+   ==. seq yss zss
+   ==. seq N (seq yss zss)
+   *** QED 
 
 composition xss N zss
    = toProof $

benchmarks/proofautomation/pos/AlphaEquivalence.hs

@@ -0,0 +1,54 @@
+{-@ LIQUID "--higherorder"     @-}
+{-@ LIQUID "--totality"        @-}
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--alphaequivalence"  @-}
+{-@ LIQUID "--betaequivalence"  @-}
+
+{-# LANGUAGE IncoherentInstances   #-}
+{-# LANGUAGE FlexibleContexts #-}
+module ApplicativeReader where
+
+import Prelude hiding (fmap, id, seq, pure)
+
+import Language.Haskell.Liquid.ProofCombinators
+import Helper (lambda_expand)
+
+{-@ axiomatize seq @-}
+seq :: (r -> (a -> b)) -> (r -> a) ->  (Reader r b)
+seq f x =  Reader (\r -> (f r) (x r))
+
+
+{-@ data Reader r a = Reader { runIdentity :: r -> a } @-}
+data Reader r a     = Reader { runIdentity :: r -> a }
+
+
+{-
+This cannot be verified, as it creates the query 
+
+;; vv = Reader (lam @2. ((lam @1. x @1) @2) (y @2))
+;; dd = Reader (lam @1. (d1nc @1) (y @1))
+;; d1nc = lam @1. (x @1)
+
+-}
+
+
+
+
+{-@ composition' :: x: (r -> (a -> a))
+                -> y:(r -> a)
+                -> { ((
+                   (\r2:r -> ((\r1:r ->  (x r1)) (r2)) (y r2))
+                         )                                    
+                  == 
+                   ((\r3:r ->  (x r3) ( y r3))
+                         ) )
+                   } @-}
+composition' :: Arg r => (r -> (a -> a)) -> (r-> a) -> Proof
+composition' x y
+  =   simpleProof 
+
+
+
+{-@ assume (===.) :: x:a -> y:{a | x == y} -> {x == y} @-}
+(===.) :: a -> a -> Proof 
+_ ===. _ = undefined 

benchmarks/proofautomation/pos/ApplicativeId.hs

@@ -0,0 +1,77 @@
+{-@ LIQUID "--higherorder"     @-}
+{-@ LIQUID "--totality"        @-}
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--higherorderqs" @-}
+{-@ LIQUID "--automatic-instances=liquidinstances" @-}
+
+
+
+{-# LANGUAGE IncoherentInstances   #-}
+{-# LANGUAGE FlexibleContexts #-}
+module FunctorList where
+
+import Prelude hiding (fmap, id, pure, seq)
+
+import Language.Haskell.Liquid.ProofCombinators
+
+
+-- | Applicative Laws :
+-- | identity      pure id <*> v = v
+-- | composition   pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
+-- | homomorphism  pure f <*> pure x = pure (f x)
+-- | interchange   u <*> pure y = pure ($ y) <*> u
+
+
+{-@ reflect pure @-}
+pure :: a -> Identity a
+pure x = Identity x
+
+{-@ reflect seq @-}
+seq :: Identity (a -> b) -> Identity a -> Identity b
+seq (Identity f) (Identity x) = Identity (f x)
+
+{-@ reflect id @-}
+id :: a -> a
+id x = x
+
+{-@ reflect idollar @-}
+idollar :: a -> (a -> b) -> b
+idollar x f = f x
+
+{-@ reflect compose @-}
+compose :: (b -> c) -> (a -> b) -> a -> c
+compose f g x = f (g x)
+
+{-@ data Identity a = Identity { runIdentity :: a } @-}
+data Identity a = Identity a
+
+-- | Identity
+{-@ identity :: x:Identity a -> { seq (pure id) x == x } @-}
+identity :: Identity a -> Proof
+identity (Identity x)
+  =   trivial 
+
+-- | Composition
+
+{-@ composition :: x:Identity (a -> a)
+                -> y:Identity (a -> a)
+                -> z:Identity a
+                -> { (seq (seq (seq (pure compose) x) y) z) == seq x (seq y z) } @-}
+composition :: Identity (a -> a) -> Identity (a -> a) -> Identity a -> Proof
+composition (Identity x) (Identity y) (Identity z)
+  =   trivial 
+
+-- | homomorphism  pure f <*> pure x = pure (f x)
+
+{-@ homomorphism :: f:(a -> a) -> x:a
+                 -> { seq (pure f) (pure x) == pure (f x) } @-}
+homomorphism :: (a -> a) -> a -> Proof
+homomorphism f x
+  =   trivial 
+
+interchange :: Identity (a -> a) -> a -> Proof
+{-@ interchange :: u:(Identity (a -> a)) -> y:a
+     -> { seq u (pure y) == seq (pure (idollar y)) u }
+  @-}
+interchange (Identity f) x
+  =   trivial 

benchmarks/proofautomation/pos/ApplicativeList.hs

@@ -0,0 +1,199 @@
+{-@ LIQUID "--higherorder"     @-}
+{-@ LIQUID "--totality"        @-}
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--automatic-instances=liquidinstances" @-}
+
+
+{-# LANGUAGE IncoherentInstances   #-}
+{-# LANGUAGE FlexibleContexts #-}
+module ListFunctors where
+
+import Prelude hiding (fmap, id, seq, pure)
+
+import Language.Haskell.Liquid.ProofCombinators
+
+-- | Applicative Laws :
+-- | identity      pure id <*> v = v
+-- | composition   pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
+-- | homomorphism  pure f <*> pure x = pure (f x)
+-- | interchange   u <*> pure y = pure ($ y) <*> u
+
+
+{-@ axiomatize pure @-}
+pure :: a -> L a
+pure x = C x N
+
+{-@ axiomatize seq @-}
+seq :: L (a -> b) -> L a -> L b
+seq (C f fs) xs
+  = append (fmap f xs) (seq fs xs)
+seq N xs
+  = N
+
+{-@ axiomatize append @-}
+append :: L a -> L a -> L a
+append N ys
+  = ys
+append (C x xs) ys
+  = C x (append xs ys)
+
+{-@ axiomatize fmap @-}
+fmap f N        = N
+fmap f (C x xs) = C (f x) (fmap f xs)
+
+{-@ axiomatize id @-}
+id :: a -> a
+id x = x
+
+{-@ axiomatize idollar @-}
+idollar :: a -> (a -> b) -> b
+idollar x f = f x
+
+{-@ axiomatize compose @-}
+compose :: (b -> c) -> (a -> b) -> a -> c
+compose f g x = f (g x)
+
+
+{-@ automatic-instances identity @-}
+
+-- | Identity
+{-@ identity :: x:L a -> { seq (pure id) x == x } @-}
+identity :: L a -> Proof
+identity xs
+  = fmap_id xs &&& prop_append_neutral xs
+
+-- | Composition
+
+{-@ composition :: x:L (a -> a)
+                -> y:L (a -> a)
+                -> z:L a
+                -> { seq (seq (seq (pure compose) x) y) z == seq x (seq y z) } @-}
+composition :: L (a -> a) -> L (a -> a) -> L a -> Proof
+
+composition N ys zs 
+  =  seq_nill (pure compose)
+
+composition (C x xs) ys zs 
+  =   prop_append_neutral (fmap compose (C x xs))
+  &&& prop_append_neutral (fmap compose (C x xs))
+  &&& seq_append (fmap (compose x) ys) (seq (fmap compose xs) ys) zs
+  &&& seq_fmap x ys zs
+  &&& prop_append_neutral (fmap compose xs)
+  &&& composition xs ys zs
+
+-- | homomorphism  pure f <*> pure x = pure (f x)
+
+{-@ homomorphism :: f:(a -> a) -> x:a
+                 -> {  seq (pure f) (pure x) == pure (f x) } @-}
+homomorphism :: (a -> a) -> a -> Proof
+homomorphism f x
+  = prop_append_neutral (C (f x) N)
+
+-- | interchange
+
+
+interchange :: L (a -> a) -> a -> Proof
+{-@ interchange :: u:(L (a -> a)) -> y:a
+     -> { seq u (pure y) == seq (pure (idollar y)) u }
+  @-}
+interchange N y
+  = seq_nill (pure (idollar y))
+
+interchange (C x xs) y
+   = prop_append_neutral (fmap (idollar y) (C x xs)) 
+            &&& seq_one' (idollar y) xs 
+            &&& interchange xs y
+            &&& seq_prop xs y 
+
+
+{-@ seq_prop :: xs:L (a -> a) -> y:a -> {seq xs (C y N) == seq xs (pure y)} @-}
+seq_prop :: L (a -> a) -> a -> Proof 
+seq_prop _ _ = trivial 
+
+
+
+data L a = N | C a (L a)
+{-@ data L [llen]
+    = N | C {x :: a, xs :: L a } @-}
+
+{-@ measure llen @-}
+llen :: L a -> Int
+{-@ llen :: L a -> Nat @-}
+llen N        = 0
+llen (C _ xs) = 1 + llen xs
+
+
+-- | TODO: Cuurently I cannot improve proofs
+-- | HERE I duplicate the code...
+
+-- TODO: remove stuff out of HERE
+
+{-@ seq_nill :: fs:L (a -> b) -> {v:Proof | seq fs N == N } @-}
+seq_nill :: L (a -> b) -> Proof
+seq_nill N
+  = trivial 
+seq_nill (C x xs)
+  = seq_nill xs
+
+{-@ append_fmap :: f:(a -> b) -> xs:L a -> ys: L a
+   -> {append (fmap f xs) (fmap f ys) == fmap f (append xs ys) } @-}
+append_fmap :: (a -> b) -> L a -> L a -> Proof
+append_fmap _ N _         = trivial 
+append_fmap f (C _ xs) ys = append_fmap f xs ys  
+
+seq_fmap :: (a -> a) -> L (a -> a) -> L a -> Proof
+{-@ seq_fmap :: f: (a -> a) -> fs:L (a -> a) -> xs:L a
+         -> { seq (fmap (compose f) fs) xs == fmap f (seq fs xs) }
+  @-}
+seq_fmap _ N _         = trivial
+seq_fmap f (C g gs) xs
+  =   seq_fmap f gs xs 
+  &&& append_fmap f (fmap g xs) (seq gs xs) 
+  &&& map_fusion0 f g xs
+
+{-@ append_distr :: xs:L a -> ys:L a -> zs:L a
+   -> {v:Proof | append xs (append ys zs) == append (append xs ys) zs } @-}
+append_distr :: L a -> L a -> L a -> Proof
+append_distr N _ _ = trivial
+append_distr (C _ xs) ys zs = append_distr xs ys zs 
+
+
+{-@ seq_one' :: f:((a -> b) -> b) -> xs:L (a -> b) -> {fmap f xs == seq (pure f) xs} @-}
+seq_one' :: ((a -> b) -> b) -> L (a -> b) -> Proof
+seq_one' _ N = trivial
+seq_one' f (C _ xs) = seq_one' f xs 
+
+{-@ seq_one :: xs:L (a -> b) -> {v:Proof | fmap compose xs == seq (pure compose) xs} @-}
+seq_one :: L (a -> b) -> Proof
+seq_one N = trivial
+seq_one (C _ xs) = seq_one xs 
+
+{-@ seq_append :: fs1:L (a -> b) -> fs2: L (a -> b) -> xs: L a
+   -> { seq (append fs1 fs2) xs == append (seq fs1 xs) (seq fs2 xs) } @-}
+seq_append :: L (a -> b) -> L (a -> b) -> L a -> Proof
+seq_append N _ _ = trivial 
+seq_append (C f1 fs1) fs2 xs 
+  = append_distr (fmap f1 xs) (seq fs1 xs) (seq fs2 xs) &&& seq_append fs1 fs2 xs 
+
+{-@ map_fusion0 :: f:(a -> a) -> g:(a -> a) -> xs:L a
+    -> {v:Proof | fmap (compose f g) xs == fmap f (fmap g xs) } @-}
+map_fusion0 :: (a -> a) -> (a -> a) -> L a -> Proof
+map_fusion0 _ _ N = trivial
+map_fusion0 f g (C _ xs) = map_fusion0 f g xs
+
+
+-- | FunctorList
+{-@ fmap_id :: xs:L a -> {v:Proof | fmap id xs == id xs } @-}
+fmap_id :: L a -> Proof
+fmap_id N
+  = trivial
+fmap_id (C x xs)
+  = fmap_id xs
+
+-- imported from Append
+prop_append_neutral :: L a -> Proof
+{-@ prop_append_neutral :: xs:L a -> {v:Proof | append xs N == xs }  @-}
+prop_append_neutral N
+  = trivial 
+prop_append_neutral (C x xs)
+  = prop_append_neutral xs