qed (empty) → 0.0
raw patch · 21 files changed
+3253/−0 lines, 21 filesdep +basedep +deepseqdep +directorysetup-changed
Dependencies added: base, deepseq, directory, exceptions, extra, filepath, haskell-src-exts, qed, transformers, uniplate
Files
- CHANGES.txt +4/−0
- LICENSE +30/−0
- README.md +5/−0
- Setup.hs +2/−0
- imports/Builtin.hs +15/−0
- imports/List.hs +223/−0
- imports/Maybe.hs +56/−0
- imports/Monad.hs +86/−0
- imports/Prelude.hs +1198/−0
- qed.cabal +54/−0
- src/Proof/Exp/Core.hs +282/−0
- src/Proof/Exp/HSE.hs +161/−0
- src/Proof/Exp/Prop.hs +55/−0
- src/Proof/QED.hs +461/−0
- src/Proof/QED/Internal.hs +17/−0
- src/Proof/QED/Trusted.hs +90/−0
- src/Proof/QED/Type.hs +175/−0
- src/Proof/Util.hs +60/−0
- test/Classes.hs +131/−0
- test/HLint.hs +121/−0
- test/Main.hs +27/−0
+ CHANGES.txt view
@@ -0,0 +1,4 @@+Changelog for QED++0.0+ Initial version
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Neil Mitchell 2015.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Neil Mitchell nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,5 @@+# QED Prover [](https://hackage.haskell.org/package/qed) [](https://travis-ci.org/ndmitchell/qed)++Experiments writing a proof system, particularly designed to prove properties about Haskell code, such as the [HLint rewrite rules](https://github.com/ndmitchell/hlint/blob/master/data/Default.hs).++Tom Ellis described the approach as "coinduction on the execution".
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ imports/Builtin.hs view
@@ -0,0 +1,15 @@+module Builtin where++error x = bottom++bottom = bottom+++-- | The Monoid that is lawful, normalising, but no more+(<>) = (++)+mempty = []++newtype Identity a = Identity a++return = Identity+a >>= b = case a of Identity a -> b a
+ imports/List.hs view
@@ -0,0 +1,223 @@+module List ( + elemIndex, elemIndices,+ find, findIndex, findIndices,+ nub, nubBy, delete, deleteBy, (\\), deleteFirstsBy,+ union, unionBy, intersect, intersectBy,+ intersperse, transpose, partition, group, groupBy,+ inits, tails, isPrefixOf, isSuffixOf,+ mapAccumL, mapAccumR,+ sort, sortBy, insert, insertBy, maximumBy, minimumBy,+ genericLength, genericTake, genericDrop,+ genericSplitAt, genericIndex, genericReplicate,+ zip4, zip5, zip6, zip7,+ zipWith4, zipWith5, zipWith6, zipWith7,+ unzip4, unzip5, unzip6, unzip7, unfoldr,++ -- ...and what the Prelude exports+ -- []((:), []), -- This is built-in syntax+ map, (++), concat, filter,+ head, last, tail, init, null, length, (!!),+ foldl, foldl1, scanl, scanl1, foldr, foldr1, scanr, scanr1,+ iterate, repeat, replicate, cycle,+ take, drop, splitAt, takeWhile, dropWhile, span, break,+ lines, words, unlines, unwords, reverse, and, or,+ any, all, elem, notElem, lookup,+ sum, product, maximum, minimum, concatMap, + zip, zip3, zipWith, zipWith3, unzip, unzip3+ ) where++import Maybe( listToMaybe )++instance Monoid a where+ mempty = []+ mappend = (++)++infix 5 \\++elemIndex :: Eq a => a -> [a] -> Maybe Int+elemIndex x = findIndex (x ==)+ +elemIndices :: Eq a => a -> [a] -> [Int]+elemIndices x = findIndices (x ==)+ +find :: (a -> Bool) -> [a] -> Maybe a+find p = listToMaybe . filter p++findIndex :: (a -> Bool) -> [a] -> Maybe Int+findIndex p = listToMaybe . findIndices p++findIndices :: (a -> Bool) -> [a] -> [Int]+findIndices p xs = [ i | (x,i) <- zip xs [0..], p x ]++nub :: Eq a => [a] -> [a]+nub = nubBy (==)++nubBy :: (a -> a -> Bool) -> [a] -> [a]+nubBy eq x = case x of+ [] -> []+ (x:xs) -> x : nubBy eq (filter (\y -> not (eq x y)) xs)++delete :: Eq a => a -> [a] -> [a]+delete = deleteBy (==)++deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]+deleteBy eq x ys = case ys of+ [] -> []+ (y:ys) -> if x `eq` y then ys else y : deleteBy eq x ys++(\\) :: Eq a => [a] -> [a] -> [a]+(\\) = foldl (flip delete)++deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]+deleteFirstsBy eq = foldl (flip (deleteBy eq))++union :: Eq a => [a] -> [a] -> [a]+union = unionBy (==) ++unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]+unionBy eq xs ys = xs ++ deleteFirstsBy eq (nubBy eq ys) xs++intersect :: Eq a => [a] -> [a] -> [a]+intersect = intersectBy (==)++intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]+intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]++intersperse :: a -> [a] -> [a]+intersperse sep xs = case xs of+ [] -> []+ x:xs -> case xs of+ [] -> [x]+ _:_ -> x : sep : intersperse sep xs++-- transpose is lazy in both rows and columns,+-- and works for non-rectangular 'matrices'+-- For example, transpose [[1,2],[3,4,5],[]] = [[1,3],[2,4],[5]]+-- Note that [h | (h:t) <- xss] is not the same as (map head xss)+-- because the former discards empty sublists inside xss+transpose :: [[a]] -> [[a]]+transpose xs = case xs of+ [] -> []+ x:xss -> case x of+ [] -> transpose xss+ (x:xs) -> (x : [h | (h:t) <- xss]) : + transpose (xs : [t | (h:t) <- xss])++partition :: (a -> Bool) -> [a] -> ([a],[a])+partition p xs = (filter p xs, filter (not . p) xs)++-- group splits its list argument into a list of lists of equal, adjacent+-- elements. e.g.,+-- group "Mississippi" == ["M","i","ss","i","ss","i","pp","i"]+group :: Eq a => [a] -> [[a]]+group = groupBy (==)++groupBy :: (a -> a -> Bool) -> [a] -> [[a]]+groupBy eq xs = case xs of+ [] -> []+ (x:xs) -> let o = span (eq x) xs in (x:fst o) : groupBy eq (snd o)++-- inits xs returns the list of initial segments of xs, shortest first.+-- e.g., inits "abc" == ["","a","ab","abc"]+inits :: [a] -> [[a]]+inits xs = case xs of+ [] -> [[]]+ (x:xs) -> [[]] ++ map (x:) (inits xs)++-- tails xs returns the list of all final segments of xs, longest first.+-- e.g., tails "abc" == ["abc", "bc", "c",""]+tails :: [a] -> [[a]]+tails xxs = case xxs of+ [] -> [[]]+ (_:xs) -> xxs : tails xs++isPrefixOf :: Eq a => [a] -> [a] -> Bool+isPrefixOf xs ys = case xs of+ [] -> True+ x:xs -> case ys of+ [] -> False+ y:ys -> x == y && isPrefixOf xs ys++isSuffixOf :: Eq a => [a] -> [a] -> Bool+isSuffixOf x y = reverse x `isPrefixOf` reverse y++mapAccumL :: (a -> b -> (a, c)) -> a -> [b] -> (a, [c])+mapAccumL f s xs = case xs of+ [] -> (s, [])+ (x:xs) ->+ let s'_y = f s x in+ let s''_ys = mapAccumL f (fst s'_y) xs in+ (fst s''_ys, snd s'_y : snd s''_ys)++mapAccumR :: (a -> b -> (a, c)) -> a -> [b] -> (a, [c])+mapAccumR f s xs = case xs of+ [] -> (s, [])+ (x:xs) -> + let s'_ys = mapAccumR f s xs in+ let s''_y = f (fst s'_ys) x in+ (fst s''_y, snd s''_y:snd s''_ys)++unfoldr :: (b -> Maybe (a,b)) -> b -> [a]+unfoldr f b = case f b of+ Nothing -> []+ Just ab -> case ab of (a,b) -> a : unfoldr f b++sort :: (Ord a) => [a] -> [a]+sort = sortBy compare++sortBy :: (a -> a -> Ordering) -> [a] -> [a]+sortBy cmp = foldr (insertBy cmp) []++insert :: (Ord a) => a -> [a] -> [a]+insert = insertBy compare++insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]+insertBy cmp x xs = case ys of+ [] -> [x]+ y:ys' -> case cmp x y of+ GT -> y : insertBy cmp x ys'+ EQ -> x : ys+ LT -> x : ys++maximumBy :: (a -> a -> Ordering) -> [a] -> a+maximumBy cmp xs = case xs of+ [] -> error "List.maximumBy: empty list"+ _:_ -> foldl1 (\x y -> case cmp x y of GT -> x; EQ -> y; LT -> y) xs++minimumBy :: (a -> a -> Ordering) -> [a] -> a+minimumBy cmp xs = case xs of+ [] -> error "List.minimumBy: empty list"+ _:_ -> foldl1 (\x y -> case cmp x y of GT -> y; EQ -> x; LT -> x) xs++genericLength :: (Integral a) => [b] -> a+genericLength xs = case xs of+ [] -> 0+ (x:xs) -> 1 + genericLength xs++genericTake :: (Integral a) => a -> [b] -> [b]+genericTake n xs = case xs of+ [] -> []+ x:xs -> if n == 0 then []+ else if n > 0 then x : genericTake (n-1) xs+ else error "List.genericTake: negative argument"++genericDrop :: (Integral a) => a -> [b] -> [b]+genericDrop n xs = if n == 0 then xs else case xs of+ [] -> []+ _:xs -> if n > 0 then genericDrop (n-1) xs else error "List.genericDrop: negative argument"++genericSplitAt :: (Integral a) => a -> [b] -> ([b],[b])+genericSplitAt n xs = if n == 0 then ([],xs) else case xs of+ [] -> ([],[])+ x:xs -> let o = genericSplitAt (n-1) xs in+ if n > 0 then (x:fst o, snd o) else error "List.genericSplitAt: negative argument"++genericIndex :: (Integral a) => [b] -> a -> b+genericIndex xs n = case xs of+ [] -> error "List.genericIndex: index too large"+ x:xs -> if n == 0 then x+ else if n > 0 then genericIndex xs (n-1)+ else error "List.genericIndex: negative argument"++genericReplicate :: (Integral a) => a -> b -> [b]+genericReplicate n x = genericTake n (repeat x)
+ imports/Maybe.hs view
@@ -0,0 +1,56 @@++module Maybe(+ isJust, isNothing,+ fromJust, fromMaybe, listToMaybe, maybeToList,+ catMaybes, mapMaybe,++ -- ...and what the Prelude exports+ Maybe(Nothing, Just),+ maybe+ ) where++instance Eq a => Eq (Maybe a) where+ (==) = eqMaybe++eqMaybe x y = case x of+ Nothing -> case y of+ Nothing -> True+ Just _ -> False+ Just x -> case y of+ Nothing -> False+ Just y -> x == y++isJust :: Maybe a -> Bool+isJust x = case x of+ (Just a) -> True+ Nothing -> False++isNothing :: Maybe a -> Bool+isNothing = not . isJust++fromJust :: Maybe a -> a+fromJust x = case x of+ (Just a) -> a+ Nothing -> error "Maybe.fromJust: Nothing"++fromMaybe :: a -> Maybe a -> a+fromMaybe d x = case x of+ Nothing -> d+ Just a -> a++maybeToList :: Maybe a -> [a]+maybeToList x = case x of+ Nothing -> []+ Just a -> [a]++listToMaybe :: [a] -> Maybe a+listToMaybe = case x of+ [] -> Nothing+ (a:_) -> Just a+ +catMaybes :: [Maybe a] -> [a]+catMaybes ms = [ m | Just m <- ms ]+-- concatMap (\x -> case x of Nothing -> []; Just m -> [m]) ms++mapMaybe :: (a -> Maybe b) -> [a] -> [b]+mapMaybe f = catMaybes . map f
+ imports/Monad.hs view
@@ -0,0 +1,86 @@+module Monad (+ MonadPlus(mzero, mplus),+ join, guard, when, unless, ap,+ msum,+ filterM, mapAndUnzipM, zipWithM, zipWithM_, foldM, + liftM, liftM2, liftM3, liftM4, liftM5,++ -- ...and what the Prelude exports+ Monad((>>=), (>>), return, fail),+ Functor(fmap),+ mapM, mapM_, sequence, sequence_, (=<<), + ) where+++-- The MonadPlus class definition++class (Monad m) => MonadPlus m where+ mzero :: m a+ mplus :: m a -> m a -> m a+++-- Instances of MonadPlus++instance MonadPlus Maybe where+ mzero = Nothing++ Nothing `mplus` ys = ys+ xs `mplus` ys = xs++instance MonadPlus [] where+ mzero = []+ mplus = (++)+++-- Functions +++msum :: MonadPlus m => [m a] -> m a+msum xs = foldr mplus mzero xs++join :: (Monad m) => m (m a) -> m a+join x = x >>= id++when :: (Monad m) => Bool -> m () -> m ()+when p s = if p then s else return ()++unless :: (Monad m) => Bool -> m () -> m ()+unless p s = when (not p) s++ap :: (Monad m) => m (a -> b) -> m a -> m b+ap = liftM2 ($)++guard :: MonadPlus m => Bool -> m ()+guard p = if p then return () else mzero++mapAndUnzipM :: (Monad m) => (a -> m (b,c)) -> [a] -> m ([b], [c])+mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip++zipWithM :: (Monad m) => (a -> b -> m c) -> [a] -> [b] -> m [c]+zipWithM f xs ys = sequence (zipWith f xs ys)++zipWithM_ :: (Monad m) => (a -> b -> m c) -> [a] -> [b] -> m ()+zipWithM_ f xs ys = sequence_ (zipWith f xs ys)++foldM :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m a+foldM f a xs = case xs of+ [] -> return a+ x:xs -> f a x >>= \ y -> foldM f y xs++filterM :: Monad m => (a -> m Bool) -> [a] -> m [a]+filterM p xs = case xs of+ [] -> return []+ x:xs ->+ p x >>= \b ->+ filterM p xs >>= \ys ->+ return (if b then (x:ys) else ys)++liftM :: (Monad m) => (a -> b) -> (m a -> m b)+liftM f = \a -> a >>= \a' -> return (f a')++liftM2 :: (Monad m) => (a -> b -> c) -> (m a -> m b -> m c)+liftM2 f = \a b -> a >>= \a' -> b >>= \b' -> return (f a' b')++liftM3 :: (Monad m) => (a -> b -> c -> d) ->+ (m a -> m b -> m c -> m d)+liftM3 f = \a b c -> a >>= \a' -> b >>= \b' -> c >>= \c' -> return (f a' b' c')
+ imports/Prelude.hs view
@@ -0,0 +1,1198 @@+module Prelude (+ module PreludeList, module PreludeText, module PreludeIO,+ Bool(False, True),+ Maybe(Nothing, Just),+ Either(Left, Right),+ Ordering(LT, EQ, GT),+ Char, String, Int, Integer, Float, Double, Rational, IO,++-- These built-in types are defined in the Prelude, but+-- are denoted by built-in syntax, and cannot legally+-- appear in an export list.+-- List type: []((:), [])+-- Tuple types: (,)((,)), (,,)((,,)), etc.+-- Trivial type: ()(())+-- Functions: (->)++ Eq((==), (/=)),+ Ord(compare, (<), (<=), (>=), (>), max, min),+ Enum(succ, pred, toEnum, fromEnum, enumFrom, enumFromThen,+ enumFromTo, enumFromThenTo),+ Bounded(minBound, maxBound),+ Num((+), (-), (*), negate, abs, signum, fromInteger),+ Real(toRational),+ Integral(quot, rem, div, mod, quotRem, divMod, toInteger),+ Fractional((/), recip, fromRational),+ Floating(pi, exp, log, sqrt, (**), logBase, sin, cos, tan,+ asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh),+ RealFrac(properFraction, truncate, round, ceiling, floor),+ RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,+ encodeFloat, exponent, significand, scaleFloat, isNaN,+ isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),+ Monad((>>=), (>>), return, fail),+ Functor(fmap),+ mapM, mapM_, sequence, sequence_, (=<<), + maybe, either,+ (&&), (||), not, otherwise,+ subtract, even, odd, gcd, lcm, (^), (^^), + fromIntegral, realToFrac, + fst, snd, curry, uncurry, id, const, (.), flip, ($), until,+ asTypeOf, error, undefined,+ seq, ($!)+ ) where++import PreludeBuiltin -- Contains all `prim' values+import UnicodePrims( primUnicodeMaxChar ) -- Unicode primitives+import PreludeList+import PreludeText+import PreludeIO+import Ratio( Rational )++infixr 9 .+infixr 8 ^, ^^, **+infixl 7 *, /, `quot`, `rem`, `div`, `mod`+infixl 6 +, -++-- The (:) operator is built-in syntax, and cannot legally be given+-- a fixity declaration; but its fixity is given by:+-- infixr 5 :++infix 4 ==, /=, <, <=, >=, >+infixr 3 &&+infixr 2 ||+infixl 1 >>, >>=+infixr 1 =<<+infixr 0 $, $!, `seq`++-- Standard types, classes, instances and related functions++-- Equality and Ordered classes+++class Eq a where+ (==), (/=) :: a -> a -> Bool++ -- Minimal complete definition:+ -- (==) or (/=)+ x /= y = not (x == y)+ x == y = not (x /= y)+++class (Eq a) => Ord a where+ compare :: a -> a -> Ordering+ (<), (<=), (>=), (>) :: a -> a -> Bool+ max, min :: a -> a -> a++ -- Minimal complete definition:+ -- (<=) or compare+ -- Using compare can be more efficient for complex types.+ compare x y = if x == y then EQ else if x <= y then LT else GT++ x <= y = compare x y /= GT+ x < y = compare x y == LT+ x >= y = compare x y /= LT+ x > y = compare x y == GT++-- note that (min x y, max x y) = (x,y) or (y,x)+ max x y = if x <= y then y else x+ min x y = if x <= y then x else y++-- Enumeration and Bounded classes+++class Enum a where+ succ, pred :: a -> a+ toEnum :: Int -> a+ fromEnum :: a -> Int+ enumFrom :: a -> [a] -- [n..]+ enumFromThen :: a -> a -> [a] -- [n,n'..]+ enumFromTo :: a -> a -> [a] -- [n..m]+ enumFromThenTo :: a -> a -> a -> [a] -- [n,n'..m]++ -- Minimal complete definition:+ -- toEnum, fromEnum+--+-- NOTE: these default methods only make sense for types+-- that map injectively into Int using fromEnum+-- and toEnum.+ succ = toEnum . (+1) . fromEnum+ pred = toEnum . (subtract 1) . fromEnum+ enumFrom x = map toEnum [fromEnum x ..]+ enumFromTo x y = map toEnum [fromEnum x .. fromEnum y]+ enumFromThen x y = map toEnum [fromEnum x, fromEnum y ..]+ enumFromThenTo x y z = + map toEnum [fromEnum x, fromEnum y .. fromEnum z]+++class Bounded a where+ minBound :: a+ maxBound :: a++-- Numeric classes+++class (Eq a, Show a) => Num a where+ (+), (-), (*) :: a -> a -> a+ negate :: a -> a+ abs, signum :: a -> a+ fromInteger :: Integer -> a++ -- Minimal complete definition:+ -- All, except negate or (-)+ x - y = x + negate y+ negate x = 0 - x+++class (Num a, Ord a) => Real a where+ toRational :: a -> Rational+++class (Real a, Enum a) => Integral a where+ quot, rem :: a -> a -> a + div, mod :: a -> a -> a+ quotRem, divMod :: a -> a -> (a,a)+ toInteger :: a -> Integer++ -- Minimal complete definition:+ -- quotRem, toInteger+ n `quot` d = fst $ quotRem n d+ n `rem` d = snd $ quotRem n d+ n `div` d = fst $ divMod n d+ n `mod` d = snd $ divMod n d+ divMod n d = if signum r == - signum d then (q-1, r+d) else qr+ where qr = quotRem n d+ q = fst qr+ r = snd qr+++class (Num a) => Fractional a where+ (/) :: a -> a -> a+ recip :: a -> a+ fromRational :: Rational -> a++ -- Minimal complete definition:+ -- fromRational and (recip or (/))+ recip x = 1 / x+ x / y = x * recip y+++class (Fractional a) => Floating a where+ pi :: a+ exp, log, sqrt :: a -> a+ (**), logBase :: a -> a -> a+ sin, cos, tan :: a -> a+ asin, acos, atan :: a -> a+ sinh, cosh, tanh :: a -> a+ asinh, acosh, atanh :: a -> a++ -- Minimal complete definition:+ -- pi, exp, log, sin, cos, sinh, cosh+ -- asin, acos, atan+ -- asinh, acosh, atanh+ x ** y = exp (log x * y)+ logBase x y = log y / log x+ sqrt x = x ** 0.5+ tan x = sin x / cos x+ tanh x = sinh x / cosh x++++class (Real a, Fractional a) => RealFrac a where+ properFraction :: (Integral b) => a -> (b,a)+ truncate, round :: (Integral b) => a -> b+ ceiling, floor :: (Integral b) => a -> b++ -- Minimal complete definition:+ -- properFraction+ truncate x = fst $ properFraction x+ ++class (RealFrac a, Floating a) => RealFloat a where+ floatRadix :: a -> Integer+ floatDigits :: a -> Int+ floatRange :: a -> (Int,Int)+ decodeFloat :: a -> (Integer,Int)+ encodeFloat :: Integer -> Int -> a+ exponent :: a -> Int+ significand :: a -> a+ scaleFloat :: Int -> a -> a+ isNaN, isInfinite, isDenormalized, isNegativeZero, isIEEE+ :: a -> Bool+ atan2 :: a -> a -> a++ -- Minimal complete definition:+ -- All except exponent, significand, + -- scaleFloat, atan2+-- Numeric functions+++subtract :: (Num a) => a -> a -> a+subtract = flip (-)+++even, odd :: (Integral a) => a -> Bool+even n = n `rem` 2 == 0+odd = not . even+++++fromIntegral :: (Integral a, Num b) => a -> b+fromIntegral = fromInteger . toInteger+++realToFrac :: (Real a, Fractional b) => a -> b+realToFrac = fromRational . toRational++-- Monadic classes+++class Functor f where+ fmap :: (a -> b) -> f a -> f b+++class Monad m where+ (>>=) :: m a -> (a -> m b) -> m b+ (>>) :: m a -> m b -> m b+ return :: a -> m a+ fail :: String -> m a++ -- Minimal complete definition:+ -- (>>=), return+ m >> k = m >>= \_ -> k+ fail s = error s+++sequence :: Monad m => [m a] -> m [a] +sequence = foldr (\p q -> p >>= \x -> q >>= \y -> return (x:y)) (return [])+++sequence_ :: Monad m => [m a] -> m () +sequence_ = foldr (>>) (return ())++-- The xxxM functions take list arguments, but lift the function or+-- list element to a monad type++mapM :: Monad m => (a -> m b) -> [a] -> m [b]+mapM f as = sequence (map f as)+++mapM_ :: Monad m => (a -> m b) -> [a] -> m ()+mapM_ f as = sequence_ (map f as)+++(=<<) :: Monad m => (a -> m b) -> m a -> m b+f =<< x = x >>= f+++-- Trivial type+++-- data () = () deriving (Eq, Ord, Enum, Bounded)+-- Not legal Haskell; for illustration only++-- Function type++-- identity function++id :: a -> a+id x = x++-- constant function++const :: a -> b -> a+const x y = x++-- function composition++(.) :: (b -> c) -> (a -> b) -> a -> c+f . g = \ x -> f (g x)++-- flip f takes its (first) two arguments in the reverse order of f.++flip :: (a -> b -> c) -> b -> a -> c+flip f x y = f y x+++seq :: a -> b -> b+seq = ... -- Primitive++-- right-associating infix application operators +-- (useful in continuation-passing style)++($), ($!) :: (a -> b) -> a -> b+f $ x = f x+f $! x = x `seq` f x+++-- Boolean type+++data Bool = False | True deriving (Eq, Ord, Enum, Read, Show, Bounded)++-- Boolean functions+++(&&), (||) :: Bool -> Bool -> Bool+x && y = case x of True -> y; False -> False+x || y = case x of True -> True; False -> y++not :: Bool -> Bool+not x = case x of True -> False; False -> True+++otherwise :: Bool+otherwise = True+++-- Character type+++-- data Char = ... 'a' | 'b' ... -- Unicode values+++instance Eq Char where+ c == c' = fromEnum c == fromEnum c'+++instance Ord Char where+ c <= c' = fromEnum c <= fromEnum c'+++instance Enum Char where+ toEnum = primIntToChar+ fromEnum = primCharToInt+ enumFrom c = map toEnum [fromEnum c .. fromEnum (maxBound::Char)]+ enumFromThen c c' = map toEnum [fromEnum c, fromEnum c' .. fromEnum lastChar]+ where lastChar :: Char+ lastChar | c' < c = minBound+ | otherwise = maxBound+++instance Bounded Char where+ minBound = '\0'+ maxBound = primUnicodeMaxChar+++type String = [Char]+++-- Maybe type+++data Maybe a = Nothing | Just a deriving (Eq, Ord, Read, Show)+++maybe :: b -> (a -> b) -> Maybe a -> b+maybe n f x = case x of Nothing -> n; Just x -> f x+++instance Functor Maybe where+ fmap f Nothing = Nothing+ fmap f (Just x) = Just (f x)+ ++instance Monad Maybe where+ (Just x) >>= k = k x+ Nothing >>= k = Nothing+ return = Just+ fail s = Nothing++-- Either type+++data Either a b = Left a | Right b deriving (Eq, Ord, Read, Show)+++either :: (a -> c) -> (b -> c) -> Either a b -> c+either f g x = case x of Left x -> f x; Right y -> g y++-- IO type+++data IO a -- abstract+++instance Functor IO where+ fmap f x = x >>= (return . f)+++instance Monad IO where+ (>>=) = ...+ return = ...+ fail s = ioError (userError s)++-- Ordering type+++data Ordering = LT | EQ | GT+ deriving (Eq, Ord, Enum, Read, Show, Bounded)+++-- Standard numeric types. The data declarations for these types cannot+-- be expressed directly in Haskell since the constructor lists would be+-- far too large.+++data Int ++instance Eq Int where ++instance Ord Int where ++instance Num Int where ++instance Real Int where ++instance Integral Int where ++instance Enum Int where ++instance Bounded Int where +++data Integer ++instance Eq Integer where ++instance Ord Integer where++instance Num Integer where++instance Real Integer where++instance Integral Integer where++instance Enum Integer where+++data Float++instance Eq Float where++instance Ord Float where++instance Num Float where++instance Real Float where++instance Fractional Float where++instance Floating Float where++instance RealFrac Float where++instance RealFloat Float where+++data Double++instance Eq Double where++instance Ord Double where++instance Num Double where++instance Real Double where++instance Fractional Double where++instance Floating Double where++instance RealFrac Double where++instance RealFloat Double where++-- The Enum instances for Floats and Doubles are slightly unusual.+-- The `toEnum' function truncates numbers to Int. The definitions+-- of enumFrom and enumFromThen allow floats to be used in arithmetic+-- series: [0,0.1 .. 0.95]. However, roundoff errors make these somewhat+-- dubious. This example may have either 10 or 11 elements, depending on+-- how 0.1 is represented.+++instance Enum Float where+ succ x = x+1+ pred x = x-1+ toEnum = fromIntegral+ fromEnum = fromInteger . truncate -- may overflow+ enumFrom = numericEnumFrom+ enumFromThen = numericEnumFromThen+ enumFromTo = numericEnumFromTo+ enumFromThenTo = numericEnumFromThenTo+++instance Enum Double where+ succ x = x+1+ pred x = x-1+ toEnum = fromIntegral+ fromEnum = fromInteger . truncate -- may overflow+ enumFrom = numericEnumFrom+ enumFromThen = numericEnumFromThen+ enumFromTo = numericEnumFromTo+ enumFromThenTo = numericEnumFromThenTo+++numericEnumFrom :: (Fractional a) => a -> [a]++numericEnumFromThen :: (Fractional a) => a -> a -> [a]++numericEnumFromTo :: (Fractional a, Ord a) => a -> a -> [a]++numericEnumFromThenTo :: (Fractional a, Ord a) => a -> a -> a -> [a]+numericEnumFrom = iterate (+1)+numericEnumFromThen n m = iterate (+(m-n)) n+numericEnumFromTo n m = takeWhile (<= m+1/2) (numericEnumFrom n)+numericEnumFromThenTo n n' m = takeWhile p (numericEnumFromThen n n')+ where+ p = if n' >= n then (<= m + (n'-n)/2) else (>= m + (n'-n)/2)++-- Lists+++-- data [a] = [] | a : [a] deriving (Eq, Ord)+-- Not legal Haskell; for illustration only+++instance Functor [] where+ fmap = map+++instance Monad [] where+ m >>= k = concat (map k m)+ return x = [x]+ fail s = []++-- Tuples+++--data (a,b) = (a,b) deriving (Eq, Ord, Bounded)++--data (a,b,c) = (a,b,c) deriving (Eq, Ord, Bounded)+-- Not legal Haskell; for illustration only++-- component projections for pairs:+-- (NB: not provided for triples, quadruples, etc.)++fst :: (a,b) -> a+fst (x,y) = x+++snd :: (a,b) -> b+snd (x,y) = y++-- curry converts an uncurried function to a curried function;+-- uncurry converts a curried function to a function on pairs.++curry :: ((a, b) -> c) -> a -> b -> c+curry f x y = f (x, y)+++uncurry :: (a -> b -> c) -> ((a, b) -> c)+uncurry f p = f (fst p) (snd p)++-- Misc functions++-- until p f yields the result of applying f until p holds.++until :: (a -> Bool) -> (a -> a) -> a -> a+until p f x = if p x then x else until p f (f x)++-- asTypeOf is a type-restricted version of const. It is usually used+-- as an infix operator, and its typing forces its first argument+-- (which is usually overloaded) to have the same type as the second.++asTypeOf :: a -> a -> a+asTypeOf = const++-- error stops execution and displays an error message+++error :: String -> a+error = primError++-- It is expected that compilers will recognize this and insert error+-- messages that are more appropriate to the context in which undefined +-- appears. +++undefined :: a+undefined = error "Prelude.undefined"+++infixl 9 !!+infixr 5 +++infix 4 `elem`, `notElem`++-- Map and append++map :: (a -> b) -> [a] -> [b]+map f x = case x of [] -> []; (x:xs) -> f x : map f xs+++(++) :: [a] -> [a] -> [a]+xs ++ ys = case xs of [] -> ys; (x:xs) -> x : (xs ++ ys)+++filter :: (a -> Bool) -> [a] -> [a]+filter p xs = case xs of+ [] -> []+ x:xs -> if p x then x : filter p xs else filter p xs+++concat :: [[a]] -> [a]+concat xss = foldr (++) [] xss+++concatMap :: (a -> [b]) -> [a] -> [b]+concatMap f = concat . map f++-- head and tail extract the first element and remaining elements,+-- respectively, of a list, which must be non-empty. last and init+-- are the dual functions working from the end of a finite list,+-- rather than the beginning.+++head :: [a] -> a+head x = case x of+ (x:_) -> x+ [] -> error "Prelude.head: empty list"+++tail :: [a] -> [a]+tail x = case x of+ (_:xs) -> xs+ [] -> error "Prelude.tail: empty list"+++last :: [a] -> a+last x = case x of+ [] -> error "Prelude.last: empty list"+ x:xs -> case xs of+ [] -> x+ _:_ -> last xs+++init :: [a] -> [a]+init x = case x of+ [] -> error "Prelude.init: empty list"+ x:xs -> case xs of+ [] -> []+ _:_ -> x : init xs+++null :: [a] -> Bool+null x = case x of [] -> True; (_:_) -> False++-- length returns the length of a finite list as an Int.++length :: [a] -> Int+length xs = case xs of+ [] -> 0+ _:l -> 1 + length l++-- List index (subscript) operator, 0-origin++(!!) :: [a] -> Int -> a+(!!) xs n = if n < 0 then error "Prelude.!!: negative index"+ else case x of+ [] -> error "Prelude.!!: index too large"+ x:xs -> if n == 0 then x else xs !! (n-1)++-- foldl, applied to a binary operator, a starting value (typically the+-- left-identity of the operator), and a list, reduces the list using+-- the binary operator, from left to right:+-- foldl f z [x1, x2, ..., xn] == (...((z `f` x1) `f` x2) `f`...) `f` xn+-- foldl1 is a variant that has no starting value argument, and thus must+-- be applied to non-empty lists. scanl is similar to foldl, but returns+-- a list of successive reduced values from the left:+-- scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]+-- Note that last (scanl f z xs) == foldl f z xs.+-- scanl1 is similar, again without the starting element:+-- scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]+++foldl :: (a -> b -> a) -> a -> [b] -> a+foldl f z x = case x of+ [] -> z+ (x:xs) -> foldl f (f z x) xs+++foldl1 :: (a -> a -> a) -> [a] -> a+foldl1 f x = case x of+ [] -> error "Prelude.foldl1: empty list"+ (x:xs) -> foldl f x xs+++scanl :: (a -> b -> a) -> a -> [b] -> [a]+scanl f q xs = q : (case xs of+ [] -> []+ x:xs -> scanl f (f q x) xs)+++scanl1 :: (a -> a -> a) -> [a] -> [a]+scanl1 f x = case x of+ [] -> []+ (x:xs) -> scanl f x xs++-- foldr, foldr1, scanr, and scanr1 are the right-to-left duals of the+-- above functions.+++foldr :: (a -> b -> b) -> b -> [a] -> b+foldr f z x = case x of+ [] -> z+ (x:xs) -> f x (foldr f z xs)+++foldr1 :: (a -> a -> a) -> [a] -> a+foldr1 f x = case x of+ [] -> error "Prelude.foldr1: empty list"+ x:xs -> case xs of+ [] -> x+ _:_ -> f x (foldr1 f xs)+++scanr :: (a -> b -> b) -> b -> [a] -> [b]+scanr f q0 x = case x of+ [] -> [q0]+ (x:xs) -> let qs = scanr f q0 xs in f x (head qs) : qs++scanr1 :: (a -> a -> a) -> [a] -> [a]+scanr1 f x = case x of+ [] -> []+ x:xs -> case xs of+ [] -> [x]+ _:_ -> let qs = scanr1 f xs in f x (head qs) : qs++-- iterate f x returns an infinite list of repeated applications of f to x:+-- iterate f x == [x, f x, f (f x), ...]++iterate :: (a -> a) -> a -> [a]+iterate f x = x : iterate f (f x)++-- repeat x is an infinite list, with x the value of every element.++repeat :: a -> [a]+repeat x = x : repeat x++-- replicate n x is a list of length n with x the value of every element++replicate :: Int -> a -> [a]+replicate n x = take n (repeat x)++-- cycle ties a finite list into a circular one, or equivalently,+-- the infinite repetition of the original list. It is the identity+-- on infinite lists.+++cycle :: [a] -> [a]+cycle xs = case xs of+ [] -> error "Prelude.cycle: empty list"+ _:_ -> xs ++ cycle xs++-- take n, applied to a list xs, returns the prefix of xs of length n,+-- or xs itself if n > length xs. drop n xs returns the suffix of xs+-- after the first n elements, or [] if n > length xs. splitAt n xs+-- is equivalent to (take n xs, drop n xs).+++take :: Int -> [a] -> [a]+take n xs = if n <= 0 then []+ else case xs of+ [] -> []+ x:xs -> x : take (n-1) xs+++drop :: Int -> [a] -> [a]+drop n xs = if n <= 0 then xs+ else case xs of+ [] -> []+ x:xs -> drop (n-1) xs+++splitAt :: Int -> [a] -> ([a],[a])+splitAt n xs = (take n xs, drop n xs)++-- takeWhile, applied to a predicate p and a list xs, returns the longest+-- prefix (possibly empty) of xs of elements that satisfy p. dropWhile p xs+-- returns the remaining suffix. span p xs is equivalent to +-- (takeWhile p xs, dropWhile p xs), while break p uses the negation of p.+++takeWhile :: (a -> Bool) -> [a] -> [a]+takeWhile p xs = case xs of+ [] -> []+ x:xs -> if p x then x : takeWhile p xs else []+++dropWhile :: (a -> Bool) -> [a] -> [a]+dropWhile p xs = case xs of+ [] -> []+ x:xs' -> if p x then dropWhile p xs' else xs+++span, break :: (a -> Bool) -> [a] -> ([a],[a])+span p xs = case xs of+ [] -> ([],[])+ x:xs' -> let ys_zs = span p xs'+ in if p x then (x:fst ys_zs, snd ys_zs)+ else ([],xs)++break p = span (not . p)++-- lines breaks a string up into a list of strings at newline characters.+-- The resulting strings do not contain newlines. Similary, words+-- breaks a string up into a list of words, which were delimited by+-- white space. unlines and unwords are the inverse operations.+-- unlines joins lines with terminating newlines, and unwords joins+-- words with separating spaces.+++lines :: String -> [String]+lines s = if null s then [] else let ls = break (== '\n') s+ in fst ls : case snd ls of+ [] -> []+ (_:s'') -> lines s''+++words :: String -> [String]+words s = let s' = dropWhile isSpace s in+ case s' of+ [] -> []+ _:_ -> let ws = break isSpace s' in+ fst ws : words (snd ws)+++unlines :: [String] -> String+unlines = concatMap (++ "\n")+++unwords :: [String] -> String+unwords ws = case ws of+ [] -> ""+ _:_ -> foldr1 (\w s -> w ++ ' ':s) ws++-- reverse xs returns the elements of xs in reverse order. xs must be finite.++reverse :: [a] -> [a]+reverse = foldl (flip (:)) []++-- and returns the conjunction of a Boolean list. For the result to be+-- True, the list must be finite; False, however, results from a False+-- value at a finite index of a finite or infinite list. or is the+-- disjunctive dual of and.++and, or :: [Bool] -> Bool+and = foldr (&&) True+or = foldr (||) False++-- Applied to a predicate and a list, any determines if any element+-- of the list satisfies the predicate. Similarly, for all.++any, all :: (a -> Bool) -> [a] -> Bool+any p = or . map p+all p = and . map p++-- elem is the list membership predicate, usually written in infix form,+-- e.g., x `elem` xs. notElem is the negation.++elem, notElem :: (Eq a) => a -> [a] -> Bool+elem x = any (== x)+notElem x = all (/= x)++-- lookup key assocs looks up a key in an association list.++lookup :: (Eq a) => a -> [(a,b)] -> Maybe b+lookup key xs = case xs of+ [] -> Nothing+ xy:xys -> case xy of+ (x,y) -> if key == x then Just y else lookup key xys++-- sum and product compute the sum or product of a finite list of numbers.++sum, product :: (Num a) => [a] -> a+sum = foldl (+) 0 +product = foldl (*) 1++-- maximum and minimum return the maximum or minimum value from a list,+-- which must be non-empty, finite, and of an ordered type.++maximum, minimum :: (Ord a) => [a] -> a+maximum xs = case xs of+ [] -> error "Prelude.maximum: empty list"+ _:_ -> foldl1 max xs++minimum xs = case xs of+ [] -> error "Prelude.minimum: empty list"+ _:_ -> foldl1 min xs++-- zip takes two lists and returns a list of corresponding pairs. If one+-- input list is short, excess elements of the longer list are discarded.+-- zip3 takes three lists and returns a list of triples. Zips for larger+-- tuples are in the List library+++zip :: [a] -> [b] -> [(a,b)]+zip = zipWith (,)+++zip3 :: [a] -> [b] -> [c] -> [(a,b,c)]+zip3 = zipWith3 (,,)++-- The zipWith family generalises the zip family by zipping with the+-- function given as the first argument, instead of a tupling function.+-- For example, zipWith (+) is applied to two lists to produce the list+-- of corresponding sums.+++zipWith :: (a->b->c) -> [a]->[b]->[c]+zipWith z as bs =+ case as of+ [] -> []+ a:as -> case bs of+ [] -> []+ b:bs -> z a b : zipWith z as bs+++zipWith3 :: (a->b->c->d) -> [a]->[b]->[c]->[d]+zipWith3 z as bs cs = case as of+ [] -> []+ a:as -> case bs of+ [] -> []+ b:bs -> case cs of+ [] -> []+ c:cs -> z a b c : zipWith3 z as bs cs+++-- unzip transforms a list of pairs into a pair of lists. +++unzip :: [(a,b)] -> ([a],[b])+unzip = foldr (\ab asbs -> case ab of (a,b) -> (a:fst asbs,b:snd asbs)) ([],[])+++unzip3 :: [(a,b,c)] -> ([a],[b],[c])+unzip3 = foldr (\abc o -> case abc of (a,b,c) -> (a:fst3 o,b:snd3 o,c:thd3 o))+ ([],[],[])++fst3 x = case x of (x,_,_) -> x+snd3 x = case x of (_,x,_) -> x+thd3 x = case x of (_,_,x) -> x+++type ReadS a = String -> [(a,String)]++type ShowS = String -> String+++class Read a where+ readsPrec :: Int -> ReadS a+ readList :: ReadS [a]+++class Show a where+ showsPrec :: Int -> a -> ShowS+ show :: a -> String + showList :: [a] -> ShowS++reads :: (Read a) => ReadS a+reads = readsPrec 0+++shows :: (Show a) => a -> ShowS+shows = showsPrec 0+++showChar :: Char -> ShowS+showChar = (:)+++showString :: String -> ShowS+showString = (++)+++showParen :: Bool -> ShowS -> ShowS+showParen b p = if b then showChar '(' . p . showChar ')' else p+++-- This lexer is not completely faithful to the Haskell lexical syntax.+-- Current limitations:+-- Qualified names are not handled properly+-- Octal and hexidecimal numerics are not recognized as a single token+-- Comments are not treated properly+++instance Show Int where+ showsPrec n = showsPrec n . toInteger+ -- Converting to Integer avoids+ -- possible difficulty with minInt+++instance Read Int where+ readsPrec p r = [(fromInteger i, t) | (i,t) <- readsPrec p r]+ -- Reading at the Integer type avoids+ -- possible difficulty with minInt+++instance Show Integer where+ showsPrec = showSigned showInt+++instance Read Integer where+ readsPrec p = readSigned readDec+++instance Show Float where + showsPrec p = showFloat+ ++instance Read Float where+ readsPrec p = readSigned readFloat+++instance Show Double where+ showsPrec p = showFloat+++instance Read Double where+ readsPrec p = readSigned readFloat+++instance Show () where+ showsPrec p () = showString "()"+++instance Read () where+ readsPrec p = readParen False+ (\r -> [((),t) | ("(",s) <- lex r,+ (")",t) <- lex s ] )++instance Show Char where+ showsPrec p '\'' = showString "'\\''"+ showsPrec p c = showChar '\'' . showLitChar c . showChar '\''++ showList cs = showChar '"' . showl cs+ where showl "" = showChar '"'+ showl ('"':cs) = showString "\\\"" . showl cs+ showl (c:cs) = showLitChar c . showl cs+++instance Read Char where+ readsPrec p = readParen False+ (\r -> [(c,t) | ('\'':s,t)<- lex r,+ (c,"\'") <- readLitChar s])++ readList = readParen False (\r -> [(l,t) | ('"':s, t) <- lex r,+ (l,_) <- readl s ])+ where readl ('"':s) = [("",s)]+ readl ('\\':'&':s) = readl s+ readl s = [(c:cs,u) | (c ,t) <- readLitChar s,+ (cs,u) <- readl t ]+++instance (Show a) => Show [a] where+ showsPrec p = showList+++instance (Read a) => Read [a] where+ readsPrec p = readList++-- Tuples+++instance (Show a, Show b) => Show (a,b) where+ showsPrec p (x,y) = showChar '(' . shows x . showChar ',' .+ shows y . showChar ')'+++instance (Read a, Read b) => Read (a,b) where+ readsPrec p = readParen False+ (\r -> [((x,y), w) | ("(",s) <- lex r,+ (x,t) <- reads s,+ (",",u) <- lex t,+ (y,v) <- reads u,+ (")",w) <- lex v ] )++-- Other tuples have similar Read and Show instances++type FilePath = String+++data IOError -- The internals of this type are system dependent+++instance Show IOError where++instance Eq IOError where+++ioError :: IOError -> IO a +ioError = primIOError+ ++userError :: String -> IOError+userError = primUserError+ ++catch :: IO a -> (IOError -> IO a) -> IO a +catch = primCatch+ ++putChar :: Char -> IO ()+putChar = primPutChar+ ++putStr :: String -> IO ()+putStr s = mapM_ putChar s+ ++putStrLn :: String -> IO ()+putStrLn s = putStr s >> putStr "\n"+ ++print :: Show a => a -> IO ()+print x = putStrLn (show x)+ ++getChar :: IO Char+getChar = primGetChar+ ++getLine :: IO String+getLine = getChar >>= \c -> + if c == '\n' then return "" else + getLine >>= \s -> + return (c:s)+ ++getContents :: IO String+getContents = primGetContents+++interact :: (String -> String) -> IO ()+-- The hSetBuffering ensures the expected interactive behaviour+interact f = hSetBuffering stdin NoBuffering >>+ hSetBuffering stdout NoBuffering >>+ getContents >>= \s ->+ putStr (f s)+++readFile :: FilePath -> IO String+readFile = primReadFile+ ++writeFile :: FilePath -> String -> IO ()+writeFile = primWriteFile+ ++appendFile :: FilePath -> String -> IO ()+appendFile = primAppendFile++ -- raises an exception instead of an error+++readLn :: Read a => IO a+readLn = getLine >>= \l ->+ readIO l >>= \r ->+ return r
+ qed.cabal view
@@ -0,0 +1,54 @@+cabal-version: >= 1.8+build-type: Simple+name: qed+version: 0.0+license: BSD3+license-file: LICENSE+category: Theorem Provers+author: Neil Mitchell <ndmitchell@gmail.com>+maintainer: Neil Mitchell <ndmitchell@gmail.com>+copyright: Neil Mitchell 2015+synopsis: Simple prover+description:+ A prototype proof system.+homepage: https://github.com/ndmitchell/qed#readme+bug-reports: https://github.com/ndmitchell/qed/issues+data-files:+ imports/*.hs+extra-doc-files:+ README.md+ CHANGES.txt+tested-with: GHC==7.10.1, GHC==7.8.4++source-repository head+ type: git+ location: https://github.com/ndmitchell/qed.git++library+ build-depends:+ base == 4.*, filepath, directory, deepseq,+ transformers, exceptions,+ uniplate, extra,+ haskell-src-exts+ hs-source-dirs: src+ exposed-modules:+ Proof.QED+ Proof.QED.Internal+ other-modules:+ Paths_qed+ Proof.Exp.Core+ Proof.Exp.HSE+ Proof.Exp.Prop+ Proof.QED.Trusted+ Proof.QED.Type+ Proof.Util++test-suite qed-test+ type: exitcode-stdio-1.0+ main-is: Main.hs+ build-depends: base, qed, transformers+ hs-source-dirs: test++ other-modules:+ Classes+ HLint
+ src/Proof/Exp/Core.hs view
@@ -0,0 +1,282 @@+{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable, PatternGuards, TupleSections, ViewPatterns #-}++-- | Module for defining and manipulating expressions.+module Proof.Exp.Core(+ Var(..), Con(..), Exp(..), Pat(..),+ fromApps, fromLams, fromLets, lets, lams, apps,+ isVar,+ vars, varsP, free, subst, relabel, relabelAvoid, fresh,+ equivalent,+ fromExp, fromName,+ simplifyExp+ ) where++import Data.Maybe+import Data.List+import Data.Data+import Control.Monad+import Control.Monad.Trans.State+import Data.Char+import Control.Arrow+import Language.Haskell.Exts hiding (Exp,Name,Pat,Var,Let,App,Case,Con,name,parse,Pretty)+import qualified Language.Haskell.Exts as H+import Proof.Exp.HSE+import Control.DeepSeq+import Proof.Util hiding (fresh)+import Data.Generics.Uniplate.Data+import Control.Applicative+import Prelude+++---------------------------------------------------------------------+-- TYPE++newtype Var = V {fromVar :: String} deriving (Data,Typeable,Eq,Show,Ord,NFData)+newtype Con = C {fromCon :: String} deriving (Data,Typeable,Eq,Show,Ord,NFData)++data Exp+ = Var Var+ | Con Con+ | App Exp Exp+ | Let Var Exp Exp -- non-recursive+ | Lam Var Exp+ | Case Exp [(Pat,Exp)]+ deriving (Data,Typeable,Eq,Ord)++data Pat+ = PCon Con [Var]+ | PWild+ deriving (Data,Typeable,Eq,Ord)++instance Read Exp where+ readsPrec = simpleReadsPrec $ fromExp . deflate . fromParseResult . parseExp++instance Show Exp where+ show = prettyPrint . unparen . inflate . toExp+ where unparen (Paren x) = x+ unparen x = x++++isVar Var{} = True; isVar _ = False++instance NFData Exp where+ rnf (Var a) = rnf a+ rnf (Con a) = rnf a+ rnf (App a b) = rnf2 a b+ rnf (Let a b c) = rnf3 a b c+ rnf (Lam a b) = rnf2 a b+ rnf (Case a b) = rnf2 a b++instance NFData Pat where+ rnf (PCon a b) = rnf2 a b+ rnf PWild = ()++caseCon :: Exp -> Maybe ([(Var,Exp)], Exp)+caseCon o@(Case (fromApps -> (Con c, xs)) alts) = Just $ headNote (error $ "Malformed case: " ++ show o) $ mapMaybe f alts+ where f (PWild, x) = Just ([], x)+ f (PCon c2 vs, x) | c /= c2 = Nothing+ | length vs /= length xs = error "Malformed arity"+ | otherwise = Just (zip vs xs, x)+caseCon _ = Nothing++apps x (y:ys) = apps (App x y) ys+apps x [] = x++lams (y:ys) x = Lam y $ lams ys x+lams [] x = x++lets [] x = x+lets ((a,b):ys) x = Let a b $ lets ys x+++fromLets (Let x y z) = ((x,y):a, b)+ where (a,b) = fromLets z+fromLets x = ([], x)++fromLams (Lam x y) = (x:a, b)+ where (a,b) = fromLams y+fromLams x = ([], x)++fromApps (App x y) = (a,b ++ [y])+ where (a,b) = fromApps x+fromApps x = (x,[])++---------------------------------------------------------------------+-- BINDING AWARE OPERATIONS++vars :: Exp -> [Var]+vars = universeBi++varsP :: Pat -> [Var]+varsP = universeBi++free :: Exp -> [Var]+free (Var x) = [x]+free (App x y) = nub $ free x ++ free y+free (Lam x y) = delete x $ free y+free (Case x y) = nub $ free x ++ concat [free b \\ varsP a | (a,b) <- y]+free (Let a b y) = nub $ free b ++ delete a (free y)+free _ = []+++subst :: [(Var,Exp)] -> Exp -> Exp+subst [] x = x+subst ren e = case e of+ Var x -> fromMaybe (Var x) $ lookup x ren+ App x y -> App (f [] x) (f [] y)+ Lam x y -> Lam x (f [x] y)+ Case x y -> Case (f [] x) [(a, f (varsP a) b) | (a,b) <- y]+ Let a b y -> Let a (f [] b) $ f [a] y+ x -> x+ where f del x = subst (filter (flip notElem del . fst) ren) x+++relabel :: Exp -> Exp+relabel x = relabelAvoid (free x) x++relabelAvoid :: [Var] -> Exp -> Exp+relabelAvoid xs x = evalState (f [] x) (fresh xs)+ where+ f :: [(Var,Var)] -> Exp -> State [Var] Exp+ f mp (Lam v x) = do i <- var; Lam i <$> f ((v,i):mp) x+ f mp (Let v x y) = do i <- var; Let i <$> f mp x <*> f ((v,i):mp) y+ f mp (Case x alts) = Case <$> f mp x <*> mapM (g mp) alts+ f mp (App x y) = App <$> f mp x <*> f mp y+ f mp (Var x) = return $ Var $ fromMaybe x $ lookup x mp+ f mp x = return x++ g mp (PWild, x) = (PWild,) <$> f mp x+ g mp (PCon c vs, x) = do is <- replicateM (length vs) var; (PCon c is,) <$> f (zip vs is ++ mp) x++ var = do s:ss <- get; put ss; return s++fresh :: [Var] -> [Var]+fresh used = map V (concatMap f [1..]) \\ used+ where f 1 = map return ['a'..'z']+ f i = [a ++ b | a <- f 1, b <- f (i-1)]+++eval :: Exp -> Exp+eval = relabel . nf . relabel+ where+ whnf (Let v x y) = whnf $ subst [(v,x)] y+ whnf (App (whnf -> Lam v x) y) = whnf $ subst [(v,y)] x+ whnf (App (whnf -> Case x alts) y) = whnf $ Case x $ map (second $ flip App y) alts+ whnf (Case (whnf -> x) alts) | Just (bs, bod) <- caseCon $ Case x alts = whnf $ subst bs bod+ whnf (Case (whnf -> Case x alts1) alts2) = Case x [(a, Case b alts2) | (a,b) <- alts1]+ whnf x = x++ nf = descend nf . whnf+++equivalent :: String -> Exp -> Exp -> Exp+equivalent = equivalentOn eval+++---------------------------------------------------------------------+-- SIMPLIFY++simplifyExp :: Exp -> Exp+simplifyExp = \(relabel -> x) -> equivalent "simplify" x $ idempotent "simplify" fs x+ where+ fs = transform f++ f o@(App (fromLets -> (bs@(_:_), Lam v z)) q) = fs $ Let v q $ lets bs z+ f o@(Case (Let v x y) alts) = fs $ Let v x $ Case y alts+ {-+ -- True, but a bit different to the others, since it is information propagation+ -- Nothing requries it yet+ f o@(Case (Var v) alts) | map g alts /= alts = fs $ Case (Var v) $ map g alts+ where g (PCon c vs, x) | v `notElem` vs = (PCon c vs, subst [(v, apps (Con c) $ map Var vs)] x)+ g x = x+ -}+ f (App (Lam v x) y) = f $ Let v y x+ f (Let v x y) | cheap x || linear v y = fs $ subst [(v,x)] y+ f o@(Case (Case on alts1) alts2) = fs $ Case on $ map g alts1+ where g (PWild, c) = (PWild, Case c alts2)+ g (PCon a vs, c) = (PCon a vs, Case c alts2)+ f x | Just ((unzip -> (vs, xs)), bod) <- caseCon x = fs $ lets (zip vs xs) bod+ f x = x++cheap (Var _) = True+cheap (Con _) = True+cheap (Lam _ _) = True+cheap _ = False+++linear :: Var -> Exp -> Bool+linear v x = count v x <= 1++count :: Var -> Exp -> Int+count v (Var x) = if v == x then 1 else 0+count v (Lam w y) = if v == w then 0 else count v y * 2 -- lambda count is infinite, but 2 is close enough+count v (Let w x y) = count v x + (if v == w then 0 else count v y)+count v (Case x alts) = count v x + maximum [if v `elem` varsP p then 0 else count v c | (p,c) <- alts]+count v (App x y) = count v x + count v y+count v _ = 0+++---------------------------------------------------------------------+-- FROM HSE++fromDecl :: Decl -> [(Var,Exp)]+fromDecl (PatBind _ (PVar f) (UnGuardedRhs x) (BDecls [])) = [(V $ fromName f, fromExp x)]+fromDecl TypeSig{} = []+fromDecl DataDecl{} = []+fromDecl TypeDecl{} = []+fromDecl x = error $ "Unhandled fromDecl: " ++ show x++fromExp :: H.Exp -> Exp+fromExp (Lambda _ [PVar (Ident x)] bod) = Lam (V x) $ fromExp bod+fromExp (H.App x y) = App (fromExp x) (fromExp y)+fromExp (H.Var (UnQual x)) = Var $ V $ fromName x+fromExp (H.Con (UnQual x)) = Con $ C $ fromName x+fromExp (Paren x) = fromExp x+fromExp (H.Case x xs) = Case (fromExp x) $ map fromAlt xs+fromExp (H.Let (BDecls [d]) x) | [(a,b)] <- fromDecl d = Let a b $ fromExp x+fromExp x = error $ "Unhandled fromExp: " ++ show x++fromName :: H.Name -> String+fromName (Ident x) = x+fromName (Symbol x) = x++fromAlt :: Alt -> (Pat, Exp)+fromAlt (Alt _ pat (UnGuardedRhs bod) (BDecls [])) = (fromPat pat, fromExp bod)+fromAlt x = error $ "Unhandled fromAlt: " ++ show x++fromPat :: H.Pat -> Pat+fromPat (PParen x) = fromPat x+fromPat (PApp (UnQual c) xs) = PCon (C $ fromName c) $ map (V . fromPatVar) xs+fromPat PWildCard = PWild+fromPat x = error $ "Unhandled fromPat: " ++ show x++fromPatVar :: H.Pat -> String+fromPatVar (PVar x) = fromName x+fromPatVar x = error $ "Unhandled fromPatVar: " ++ show x+++---------------------------------------------------------------------+-- TO HSE++toDecl :: Var -> Exp -> Decl+toDecl (V f) x = PatBind sl (PVar $ toName f) (UnGuardedRhs $ toExp x) (BDecls [])++toExp :: Exp -> H.Exp+toExp (Var (V x)) = H.Var $ UnQual $ toName x+toExp (Con (C x)) = H.Con $ UnQual $ toName x+toExp (Lam (V x) y) = Lambda sl [PVar $ toName x] $ toExp y+toExp (Let a b y) = H.Let (BDecls [toDecl a b]) $ toExp y+toExp (App x y) = H.App (toExp x) (toExp y)+toExp (Case x y) = H.Case (toExp x) (map toAlt y)++toAlt :: (Pat, Exp) -> Alt+toAlt (x,y) = Alt sl (toPat x) (UnGuardedRhs $ toExp y) (BDecls [])++toPat :: Pat -> H.Pat+toPat (PCon (C c) vs) = PApp (UnQual $ toName c) (map (PVar . Ident . fromVar) vs)+toPat PWild = PWildCard++toName :: String -> H.Name+toName xs@(x:_) | isAlphaNum x || x `elem` "'_(" = Ident xs+ | otherwise = Symbol xs
+ src/Proof/Exp/HSE.hs view
@@ -0,0 +1,161 @@+{-# LANGUAGE ViewPatterns, PatternGuards #-}++-- | Module for operating on haskell-src-exts expressions.+module Proof.Exp.HSE(deflate, inflate, sl) where++import Data.Data+import Data.List+import Language.Haskell.Exts+import Control.Monad.Trans.State+import Data.Generics.Uniplate.Data+import Control.Applicative+import Prelude+++-- Turn on to have better list comp desugaring in terms of mapMaybe for common cases+fasterListComp = False++sl = SrcLoc "" 0 0++names :: Data a => a -> [String]+names = map f . universeBi+ where f (Ident x) = x+ f (Symbol x) = x++fresh :: [String] -> [String]+fresh del = ["v" ++ show i | i <- [1..]] \\ del++---------------------------------------------------------------------+-- DEFLATE++-- | Use fewer constructors to express the same program.+deflate :: Data a => a -> a+deflate = transformBi deflateExp . transformBi deflatePat . transformBi deflateQName . transformBi deflateDecl . deflateWildcard++spec :: SpecialCon -> QName+spec UnitCon = UnQual $ Ident "()"+spec ListCon = UnQual $ Ident "[]" +spec Cons = UnQual $ Symbol ":"+spec (TupleCon Boxed i) = UnQual $ Ident $ "(" ++ replicate (i-1) ',' ++ ")"+spec x = Special x++deflateDecl :: Decl -> Decl+deflateDecl (FunBind [Match sl f vars Nothing (UnGuardedRhs x) decs]) =+ PatBind sl (PVar f) (UnGuardedRhs $ Lambda sl vars $ Let decs x) (BDecls [])+deflateDecl x = x++deflateQName :: QName -> QName+deflateQName (Special x) = spec x+deflateQName x = x++deflateExp :: Exp -> Exp+deflateExp (Lambda sl ps x) | length ps /= 1 = foldr (\p x -> Lambda sl [p] x) x ps+deflateExp (LeftSection x (QVarOp y)) = App (Var y) x+deflateExp (LeftSection x (QConOp y)) = App (Con y) x+deflateExp (RightSection (QVarOp y) x) = Paren $ Var (UnQual $ Ident "flip") `App` Var y `App` Paren x+deflateExp (RightSection (QConOp y) x) = Paren $ Var (UnQual $ Ident "flip") `App` Con y `App` Paren x+deflateExp (List []) = Con $ spec ListCon+deflateExp (List (x:xs)) = Paren $ Con (spec Cons) `App` Paren x `App` deflateExp (List xs)+deflateExp (Tuple b xs) = foldl App (Con $ spec $ TupleCon b $ length xs) xs+deflateExp (InfixApp a (QVarOp b) c) = Var b `App` a `App` c+deflateExp (InfixApp a (QConOp b) c) = Con b `App` a `App` c+deflateExp (Lit x) = Con $ UnQual $ Ident $ prettyPrint x+deflateExp (NegApp x) = Paren $ Var (UnQual $ Ident "negate") `App` Paren x+deflateExp o@(Lambda sl [p] e) | not $ isPVar p = Lambda sl [PVar new] $ Case (Var $ UnQual new) [Alt sl p (UnGuardedRhs e) $ BDecls []]+ where new:_ = map Ident $ fresh $ names o+deflateExp (Case (Var (UnQual v)) (Alt sl (PVar p) (UnGuardedRhs e) (BDecls []):_))+ | v == p = e+ | otherwise = Let (BDecls [PatBind sl (PVar p) (UnGuardedRhs $ Var $ UnQual v) (BDecls [])]) e+deflateExp (If a b c) = Case a [f "True" b, f "False" c]+ where f con x = Alt sl (PApp (UnQual $ Ident con) []) (UnGuardedRhs x) (BDecls [])+deflateExp (Let (BDecls bs) x) = foldr (\b x -> Let (BDecls [b]) x) x bs -- FIXME: Only safe if variables are not mutually recursive+deflateExp (EnumFromTo x y) = Paren $ Var (UnQual $ Ident "enumFromTo") `App` x `App` y+deflateExp (EnumFromThen x y) = Paren $ Var (UnQual $ Ident "enumFromThen") `App` x `App` y+deflateExp (EnumFromThenTo x y z) = Paren $ Var (UnQual $ Ident "enumFromThenTo") `App` x `App` y `App` z+deflateExp (EnumFrom x) = Paren $ Var (UnQual $ Ident "enumFrom") `App` x+deflateExp (ListComp res xs) = lst xs+ where+ -- variants returning a Maybe+ may [] = Just $ Con (UnQual $ Ident "Just") `App` Paren res+ may (QualStmt (LetStmt bind):xs) = deflateExp . Let bind <$> may xs+ may (QualStmt (Qualifier e):xs) = (\xs -> Paren $ deflateExp $ If e xs $ Con $ UnQual $ Ident "Nothing") <$> may xs+ may _ = Nothing++ -- optimised shortcuts (use map or mapMaybe)+ lst (QualStmt (Generator _ p e):[]) | fasterListComp, irrefutable p = Var (UnQual $ Ident "map") `App` deflateExp (Lambda sl [p] res) `App` e+ lst o@(QualStmt (Generator _ p e):xs) | fasterListComp, Just ans <- may xs =+ Var (UnQual $ Ident "mapMaybe") `App` deflateExp (Lambda sl [PVar new] $ bod ans) `App` e+ where new:_ = map Ident $ fresh $ names $ ListComp res o+ bod ans = deflateExp $ Case (Var $ UnQual new) $+ [Alt sl p (UnGuardedRhs ans) $ BDecls []] +++ [Alt sl PWildCard (UnGuardedRhs $ Con $ UnQual $ Ident "Nothing") $ BDecls [] | not $ irrefutable p]++ -- from the report, returning a list+ lst o@(QualStmt (Generator _ p e):xs) = Var (UnQual $ Ident "concatMap") `App` deflateExp (Lambda sl [PVar new] bod) `App` e+ where new:_ = map Ident $ fresh $ names $ ListComp res o+ bod = deflateExp $ Case (Var $ UnQual new)+ [Alt sl p (UnGuardedRhs $ lst xs) $ BDecls []+ ,Alt sl PWildCard (UnGuardedRhs $ deflateExp $ List []) $ BDecls []]+ lst (QualStmt (Qualifier e):xs) = Paren $ deflateExp $ If e (lst xs) (deflateExp $ List [])+ lst (QualStmt (LetStmt bind):xs) = Paren $ deflateExp $ Let bind $ lst xs+ lst [] = deflateExp $ List [res]+ lst xs = ListComp res xs+deflateExp x = x++irrefutable :: Pat -> Bool+irrefutable x = case deflatePat x of+ PApp (UnQual (Ident ('(':(dropWhile (== ',') -> ")")))) xs -> all irrefutable xs+ PVar{} -> True+ _ -> False++deflatePat :: Pat -> Pat+deflatePat (PInfixApp a b c) = PApp b [a,c]+deflatePat (PList []) = PApp (spec ListCon) []+deflatePat (PTuple b xs) = PApp (spec $ TupleCon b $ length xs) xs+deflatePat x = x++-- removing wildcards needs some state (the unused variables), so has to be monadic+deflateWildcard :: Data a => a -> a+deflateWildcard x = evalState (transformBiM f x) (["_" ++ show i | i <- [1..]] \\ names x)+ where f :: Pat -> State [String] Pat+ f PWildCard = do s:ss <- get; put ss; return $ PVar $ Ident s+ f x = return x++isPVar PVar{} = True; isPVar _ = False+++---------------------------------------------------------------------+-- INFLATE++-- | Add back in syntactic forms to make it more readable.+inflate :: Data a => a -> a+inflate =+ transformBi inflateRhs . transformBi inflateAlt . transformBi inflateRhs .+ transformBi inflatePat . transformBi inflateExp .+ transformBi Paren . transformBi PParen++inflateExp :: Exp -> Exp+inflateExp (Lambda sl ps (Paren x)) = inflateExp $ Lambda sl ps x+inflateExp (Lambda sl ps1 (Lambda _ ps2 x)) | null $ names ps1 `intersect` names ps2 = Lambda sl (ps1++ps2) x+inflateExp (Paren (Paren x)) = inflateExp $ Paren x+inflateExp (Paren (Var x)) = Var x+inflateExp (Paren (Con x)) = Con x+inflateExp (Paren (List x)) = List x+inflateExp (Paren (Lit x)) = Lit x+inflateExp (App (Paren (App a b)) c) = App (App a b) c+inflateExp (Con (UnQual (Symbol "[]"))) = List []+inflateExp x = x++inflatePat :: Pat -> Pat+inflatePat (PParen (PParen x)) = PParen x+inflatePat (PParen (PVar x)) = PVar x+inflatePat (PApp (UnQual (Symbol "[]")) []) = PList []+inflatePat x = x++inflateRhs :: Rhs -> Rhs+inflateRhs (UnGuardedRhs (Paren x)) = UnGuardedRhs x+inflateRhs x = x++inflateAlt :: Alt -> Alt+inflateAlt (Alt sl (PParen p) x y) = Alt sl p x y+inflateAlt x = x
+ src/Proof/Exp/Prop.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE DeriveDataTypeable, PatternGuards, TupleSections, ViewPatterns #-}++-- | Module for defining and manipulating expressions.+module Proof.Exp.Prop(+ Prop(..), sym, tautology, simplifyProp, (==>)+ ) where++import Proof.Exp.Core+import Proof.Util+import Data.Data+import Data.Maybe+import Data.List.Extra+import Control.DeepSeq++data Prop = Prop [Var] Exp Exp deriving (Eq,Data,Typeable)++instance NFData Prop where+ rnf (Prop a b c) = rnf3 a b c++sym :: Prop -> Prop+sym (Prop vs a b) = Prop vs b a++instance Show Prop where+ show (Prop vs a b) = unwords (map fromVar vs ++ ["=>"]) ++ "\n" ++ f a ++ "=" ++ drop 1 (f b)+ where f = unlines . map (" "++) . lines . show++instance Read Prop where+ readsPrec = simpleReadsPrec $ \x -> case () of+ _ | (quant, x) <- fromMaybe ("",x) $ stripInfix " => " x+ , Just (a,b) <- stripInfix " = " x+ -> Prop (map V $ words quant) (read a) (read b)++simplifyProp :: Prop -> Prop+simplifyProp = label . simple . unlam . simple+ where+ simple (Prop vs a b) = Prop vs (simplifyExp a) (simplifyExp b)++ unlam (Prop vs (Lam a1 a2) (Lam b1 b2))+ | v:_ <- fresh $ a1:b1:vs ++ vars a2 ++ vars b2+ = unlam $ Prop (v:vs) (subst [(a1,Var v)] a2) (subst [(b1,Var v)] b2)+ unlam x = x++ label (Prop vs a b) = Prop new (subst sub $ relabelAvoid (free a ++ new) a) (subst sub $ relabelAvoid (free b ++ new) b)+ where fv = nubOrd $ free a ++ free b+ vs2 = fv `intersect` vs+ new = take (length vs2) $ fresh $ fv \\ vs+ sub = zip vs2 $ map Var new+++-- Does the first property imply the second+(==>) :: Prop -> Prop -> Bool+(==>) a b = simplifyProp a == simplifyProp b || simplifyProp (sym a) == simplifyProp b++tautology :: Prop -> Bool+tautology (Prop vs a b) = a == b
+ src/Proof/QED.hs view
@@ -0,0 +1,461 @@+{-# LANGUAGE ViewPatterns, ScopedTypeVariables, RecordWildCards, TupleSections, PatternGuards #-}++module Proof.QED(+ QED, qed,+ imports, decl,+ Laws, law, laws,+ Proof, PropString, prove,+ Bind, satisfy, bind,+ rhs, lhs, bhs, at,+ recurse, unfold, unfold_, strict, expand, unlet, divide,+ twice, thrice, many, perhaps, skip,+ qedCheat, unsafeCheat+ ) where++import Proof.QED.Internal() -- so I test all the API's++import Proof.QED.Type+import Proof.QED.Trusted+import Proof.Exp.Prop+import Proof.Exp.Core+import Proof.Exp.HSE+import Control.Monad.IO.Class+import Control.Monad.Catch as C+import Control.Monad+import Language.Haskell.Exts hiding (Var, Exp, Con, Case, App, Let)+import Data.Maybe+import Data.List.Extra+import System.FilePath+import System.Directory+import Data.Generics.Uniplate.Data+import Paths_qed+import Control.Applicative hiding (many)+import Prelude++type PropString = String++law :: PropString -> QED Laws+law (read -> p) = do+ addAssumed p+ return $ Laws [p]++laws :: QED a -> QED Laws+laws act = do+ n <- length . assumed <$> getKnown+ act+ Laws . drop n . assumed <$> getKnown++imports :: FilePath -> QED ()+imports file = do+ dataDir <- liftIO getDataDir+ let poss = [dir </> file <.> ext | dir <- [".",dataDir </> "imports"], ext <- [".hs",""]]+ files <- liftIO $ filterM doesFileExist poss+ when (null files) $+ fail $ unlines $ ("imports: Could not find " ++ file ++ ", tried:") : map (" "++) poss+ src <- liftIO $ readFile $ head files+ let mode = defaultParseMode{parseFilename=file}+ let res = deflate $ fromParseResult $ parseFileContentsWithMode mode $ replace "..." "undefined" src+ mapM_ addDecl $ childrenBi res++decl :: String -> QED ()+decl = addDecl . deflate . fromParseResult . parseDecl++addDecl :: Decl -> QED ()+addDecl (PatBind _ (PVar name) (UnGuardedRhs bod) (BDecls [])) = addDefinition (V $ fromName name) (fromExp bod)+addDecl (DataDecl _ _ _ name _ ctrs _) = addType (fromName name) [(C $ fromName a, length b) | (QualConDecl _ _ _ (ConDecl a b)) <- ctrs]+addDecl x@ClassDecl{} = mapM_ addDecl $ children x+addDecl InfixDecl{} = return ()+addDecl InstDecl{} = return ()+addDecl TypeDecl{} = return ()+addDecl TypeSig{} = return ()+addDecl x = error $ "Cannot add declaration, " ++ prettyPrint x+++prove :: PropString -> Proof () -> QED ()+prove (read -> prop) proof = addProved prop proof++satisfy :: String -> Laws -> Bind () -> QED ()+satisfy msg (Laws ps) (runBind -> bind) = do+ liftIO $ putStrLn $ "Satisfy " ++ msg+ Known{..} <- getKnown+ forM_ ps $ \(Prop vs a b) -> do+ let p2 = Prop vs (subst bind a) (subst bind b)+ unless (any (==> p2) (assumed ++ proved)) $ do+ fail $ "Failed to satisfy:" ++ show p2+ liftIO $ putStrLn "QED\n"++unfold :: String -> Proof ()+unfold name = apply rewriteUnfold $ \Known{..} x -> case x of+ Var x | x == V name, Just e <- lookup x definitions -> Just e+ _ -> Nothing++unfold_ :: Proof ()+unfold_ = apply rewriteUnfold $ \Known{..} x -> case x of+ Var x | Just e <- lookup x definitions -> Just e+ _ -> Nothing++strict :: String -> Proof ()+strict name = apply rewriteEquivalent $ \Known{..} x -> case x of+ Var x -> Just $ Case (Var x)+ [ (PCon c vars, apps (Con c) $ map Var vars)+ | (c,vs) <- fromJust $ lookup name types, let vars = take vs $ fresh []]+ _ -> Nothing++recurse :: Proof ()+recurse = rewriteRecurse >> auto++expand :: Proof ()+expand = apply rewriteEquivalent $ \Known{..} o@(fromLams -> (vs, x)) -> Just $+ let v:_ = fresh $ vars o + in lams (vs ++ [v]) $ App x $ Var v+++unlet :: Proof ()+unlet = apply rewriteEquivalent $ \_ x ->+ case x of Let a b x -> Just $ subst [(a,b)] x; _ -> Nothing++divide :: Proof ()+divide = do+ rewriteSplit+ auto+++twice :: Proof () -> Proof ()+twice = replicateM_ 2++thrice :: Proof () -> Proof ()+thrice = replicateM_ 3++many :: Proof () -> Proof ()+many p = void $ p >> perhaps (forever p)++rhs :: Proof () -> Proof ()+rhs = side RHS++lhs :: Proof () -> Proof ()+lhs = side LHS++side :: Side -> Proof () -> Proof ()+side x act = C.bracket+ (focusSide . snd <$> getUnknown)+ setFocusSide $+ const $ setFocusSide (Just x) >> act++bhs :: Proof () -> Proof ()+bhs p = lhs p >> rhs p++at :: Int -> Proof () -> Proof ()+at i act = C.bracket+ (focusAt . snd <$> getUnknown)+ setFocusAt $+ const $ setFocusAt i >> act++bind :: String -> Bind ()+bind (deflate . fromParseResult . parseDecl -> PatBind _ (PVar name) (UnGuardedRhs bod) (BDecls [])) =+ addBind (V $ fromName name) (fromExp bod)+++apply :: (Prop -> Proof ()) -> (Known -> Exp -> Maybe Exp) -> Proof ()+apply run test = do+ (known, Unknown{..}, Goal pre (Prop vs lhs rhs)) <- getGoal+ let poss = (if focusSide /= Just RHS then map (,\lhs -> Prop vs lhs rhs) $ contexts lhs else []) +++ (if focusSide /= Just LHS then map (,\rhs -> Prop vs lhs rhs) $ contexts rhs else [])+ let xs = [gen2 $ gen x | ((test known -> Just x, gen),gen2) <- poss]+ case drop focusAt xs of+ [] -> badProof "Cannot apply, no suitable elements at index"+ x:_ -> run x >> auto++auto :: Proof ()+auto = f autos+ where+ autos = [rewriteTautology, autoSimplify, autoPeel]++ f [] = return ()+ f (a:as) = do+ r <- perhaps a+ f $ if r then autos else as+++autoSimplify :: Proof ()+autoSimplify = do+ (_, _, Goal _ x) <- getGoal+ let x2 = simplifyProp x+ if x2 == x then badProof "cannot autoSimplify" else rewriteEquivalent x2++autoPeel :: Proof ()+autoPeel = do+ (_, _, Goal _ (Prop vs a b)) <- getGoal+ if f vs a && f vs b then rewriteSplit else badProof "cannot autoPeel"+ where+ f vs Lam{} = True+ f vs Con{} = True+ f vs (App x _) = f vs x+ f vs (Var v) = v `elem` vs+ f vs (Case (Var v) _) = v `elem` vs+ f vs _ = False+++perhaps :: Proof () -> Proof Bool+perhaps x = not <$> isBadProof x++skip :: QED () -> QED ()+skip _ = return ()++{-+autoLaw :: State -> Goal -> Maybe [Goal]+autoLaw s (Goal pre x)+ | tautology x = Just []+ | any (==> x) (pre ++ proved s) = Just []+ | otherwise = Nothing++autoPeelCase :: Goal -> Maybe [Goal]+autoPeelCase (Goal pre (Prop vs a b))+ | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)+ | otherwise = Nothing+ where+ -- distinguishes the salient features+ pattern (Case on alts) = Just (on, map (patCon . fst) alts)+ pattern x = Nothing++ split (Case on alts) = [lams (patVars p) $ f on p x | (p,x) <- alts]+ where f (Var on) (PCon c vs) | on `notElem` vs = Let on (apps (Con c) (map Var vs))+ f _ _ = id++autoPeelCon :: Goal -> Maybe [Goal]+autoPeelCon (Goal pre (Prop vs a b))+ | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)+ | otherwise = Nothing+ where+ pattern (fromApps -> (Con ctr, args)) = Just (ctr, length args)+ pattern x = Nothing++ split (fromApps -> (Con ctr, args)) = map (lams vs) args++autoPeelVar :: Goal -> Maybe [Goal]+autoPeelVar (Goal pre (Prop vs a b))+ | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)+ | otherwise = Nothing+ where+ pattern (fromApps -> (Var v, args)) | v `elem` vs = Just (v, length args)+ pattern x = Nothing++ split (fromApps -> (Var v, args)) = args+-}+++{-++data State = State+ {defined :: [(Var, Exp)]+ ,types :: [(String, [(Con,Int)])]+ ,proved :: [Prop]+ ,goal :: [Goal] -- A list of And alternatives+ ,focusRhs :: Bool+ ,focusInd :: Int+ } deriving Show++instance NFData State where+ rnf x = rnf $ show x++instance Pretty State where+ pretty State{..} = unlines $+ [unwords $ "data" : x : "=" : intercalate ["|"] [fromCon y : replicate n "_" | (y,n) <- ys] | (x,ys) <- types] +++ ["\n" ++ fromVar x ++ " = " ++ pretty b | (x,b) <- defined] +++ ["\n" ++ pretty x | x <- proved] +++ ["\n-- GOAL " ++ show i ++ concat ["\n-- WHERE " ++ pretty p | p <- pre] ++ "\n" ++ pretty x | (i,Goal pre x) <- zip [1..] goal]++state0 = State [] [] [] [] False 0++data Goal = Goal [Prop] Prop deriving (Show,Eq)++state :: IORef State+state = unsafePerformIO $ newIORef $ state0++getState :: IO State+getState = readIORef state++modifyState :: (State -> State) -> IO ()+modifyState f = do+ s <- readIORef state+ let s2 = f s+ evaluate $ rnf s2+ writeIORef state s2++rhs :: IO a -> IO a+rhs f = bracket getState+ (\v -> modifyState $ \s -> s{focusRhs=focusRhs v})+ (\_ -> do modifyState $ \s -> s{focusRhs=True}; f)++ind :: Int -> IO a -> IO a+ind i f = bracket getState+ (\v -> modifyState $ \s -> s{focusInd=focusInd v})+ (\_ -> do modifyState $ \s -> s{focusInd=i}; f)++run :: IO a -> IO ()+run act = flip onException dump $ do+ writeIORef state state0+ act+ -- dump+ g <- goal <$> getState+ when (null g) $ putStrLn "QED"++dump :: IO ()+dump = do+ x <- getState+ putStrLn $ pretty x++cheat :: IO ()+cheat = modifyState $ \s -> s{goal = []}++define :: String -> IO ()+define x = case deflate $ fromParseResult $ parseDecl x of+ DataDecl _ _ _ name _ ctrs _ -> do+ let f (fromName -> x) = fromMaybe x $ lookup x [("Nil_","[]"),("Cons_",":")]+ modifyState $ \s -> s{types = types s ++ [(f name, [(C $ f a,length b) | (QualConDecl _ _ _ (ConDecl a b)) <- ctrs])]}+ PatBind _ (PVar x) (UnGuardedRhs bod) (BDecls []) -> do+ let res = fromExp bod+ evaluate $ show res+ modifyState $ \s -> s{defined = defined s ++ [(V $ fromName x, res)]}+ x -> error $ "Define not handled, " ++ show x++proof :: String -> String -> IO () -> IO (IO ())+proof (parse -> a) (parse -> b) = proofProp (Prop [] a b)++proofProp :: Prop -> IO () -> IO (IO ())+proofProp p c = do+ g <- goal <$> getState+ unless (null g) $ error "Can't call proof recursively"+ p <- return $ simplifyProp p+ modifyState $ \s -> s{goal = auto s $ Goal [] p}+ c+ g <- goal <$> getState+ unless (null g) $ error "proof did not prove the goal"+ modifyState $ \s -> s{proved = proved s ++ [p]}+ return c+++step :: String -> (State -> Exp -> Maybe Exp) -> IO ()+step msg f = modifyState $ \s ->+ let ff = f s+ Goal pre g1:gs = goal s+ swp = if focusRhs s then sym else id+ g2 = (!! focusInd s) $+ [swp $ gen e | (e, gen) <- contextsBi $ swp g1, Just e <- [ff e]] +++ error ("nothing matches, " ++ msg)+ in s{goal = auto s (Goal pre g2) ++ gs}++expand :: IO ()+expand = step "Eta expand" $ \_ o@(fromLams -> (vs,x)) -> Just $+ let v:_ = fresh $ vars o + in lams (vs ++ [v]) $ App x $ Var v++unfold :: String -> IO ()+unfold x = step ("unfold " ++ x) $ \s ->+ let rep =+ case () of+ _ | Just e <- lookup (V x) $ defined s -> \v -> if v == x then Just e else Nothing+ | Just e <- lookup x $ types s -> \v -> Just $ Case (Var (V v))+ [(PCon c vs, apps (Con c) (map Var vs)) | (c, n) <- e, let vs = take n $ fresh []]+ | otherwise -> error $ "Unknown unfolding for " ++ x+ in \x -> case x of Var (V v) -> rep v; _ -> Nothing++unlet :: IO ()+unlet = step "unlet" $ \_ x ->+ case x of Let a b x -> Just $ subst [(a,b)] x; _ -> Nothing++unsafeReplace :: String -> String -> IO ()+unsafeReplace (parse -> a) (parse -> b) = step "replace" $ \_ x ->+ if x == a then Just b else Nothing++auto :: State -> Goal -> [Goal]+auto s = f full+ where+ full = [autoSimplify, autoLaw s, autoPeelCase, autoPeelCon, autoPeelVar]++ f [] g = [g]+ f (x:xs) g = case x g of+ Nothing -> f xs g+ Just [g2] | g == g2 -> f xs g+ Just gs -> concatMap (f full) gs+++autoSimplify :: Goal -> Maybe [Goal]+autoSimplify (Goal pre x) = Just [Goal pre $ simplifyProp x]++autoLaw :: State -> Goal -> Maybe [Goal]+autoLaw s (Goal pre x)+ | tautology x = Just []+ | any (==> x) (pre ++ proved s) = Just []+ | otherwise = Nothing++autoPeelCase :: Goal -> Maybe [Goal]+autoPeelCase (Goal pre (Prop vs a b))+ | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)+ | otherwise = Nothing+ where+ -- distinguishes the salient features+ pattern (Case on alts) = Just (on, map (patCon . fst) alts)+ pattern x = Nothing++ split (Case on alts) = [lams (patVars p) $ f on p x | (p,x) <- alts]+ where f (Var on) (PCon c vs) | on `notElem` vs = Let on (apps (Con c) (map Var vs))+ f _ _ = id++autoPeelCon :: Goal -> Maybe [Goal]+autoPeelCon (Goal pre (Prop vs a b))+ | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)+ | otherwise = Nothing+ where+ pattern (fromApps -> (Con ctr, args)) = Just (ctr, length args)+ pattern x = Nothing++ split (fromApps -> (Con ctr, args)) = map (lams vs) args++autoPeelVar :: Goal -> Maybe [Goal]+autoPeelVar (Goal pre (Prop vs a b))+ | pattern a =^= pattern b = Just $ zipWith (\a b -> Goal pre $ Prop vs a b) (split a) (split b)+ | otherwise = Nothing+ where+ pattern (fromApps -> (Var v, args)) | v `elem` vs = Just (v, length args)+ pattern x = Nothing++ split (fromApps -> (Var v, args)) = args++{-++autoRemoveLam :: IO ()+autoRemoveLam = modifyState $ \s -> s{goal = [Goal pre $ f x | Goal pre x <- goal s]}+ where+ f (a :=: b) | unused <- pattern a `intersect` pattern b = split unused a :=: split unused b++ pattern (fromLams -> (vs, x)) = [i | (i,v) <- zip [0..] vs, v `notElem` free x]+ split unused (fromLams -> (vs, x)) = lams [v | (i,v) <- zip [0..] vs, i `notElem` unused] x+-}++recurse :: IO ()+recurse = modifyState $ \s ->+ let Goal pre p@(Prop vs a b):gs = goal s+ in case (reduce s a, reduce s b) of+ (Nothing, Nothing) -> error $ "Cannot reduce\n" ++ pretty a ++ "\n" ++ pretty b+ (aa, bb) -> s{goal = auto s (Goal (p:pre) $ Prop vs (fromMaybe a aa) (fromMaybe b bb)) ++ gs}++reduce :: State -> Exp -> Maybe Exp+reduce State{..} = f+ where+ f (Lam v x) = Lam v <$> f x+ f (App a b) = (`App` b) <$> f a+ f (Var v) = lookup v defined+ f (Case x xs) = (`Case` xs) <$> f x+ f x = error $ "step: Don't know, " ++ pretty x++divide :: IO ()+divide = modifyState $ \s ->+ let Goal pre (Prop vs a b):gs = goal s in+ case (f a, f b) of+ (Just (oa, ca), Just (ob, cb)) | oa == ob, length ca == length cb ->+ s{goal = concat (zipWith (\a b -> auto s $ Goal pre $ Prop vs a b) ca cb) ++ gs}+ where+ z = Var $ V ""+ f (App a b) = Just (App z z, [a,b])+ f _ = Nothing+-}
+ src/Proof/QED/Internal.hs view
@@ -0,0 +1,17 @@++module Proof.QED.Internal(+ Exp(..), Pat(..), Var(..), Con(..),+ Prop(..),+ Side(..),+ Known(..), getKnown,+ Unknown(..), getUnknown,+ Goal(..), getGoal,+ BadProof(..), badProof, isBadProof,+ Laws(..),+ module Proof.QED.Trusted+ ) where++import Proof.Exp.Core+import Proof.Exp.Prop+import Proof.QED.Type+import Proof.QED.Trusted
+ src/Proof/QED/Trusted.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE RecordWildCards, PatternGuards #-}++module Proof.QED.Trusted(+ rewriteUnfold,+ rewriteEquivalent,+ rewriteRecurse,+ rewriteSplit,+ rewriteTautology+ ) where++import Proof.Exp.Prop+import Proof.Exp.Core+import Proof.QED.Type+import Control.Monad+import Data.Maybe+import Data.Generics.Uniplate.Data+import Control.Applicative+import Prelude+++-- | Use a new prop which is the same as the previous goal, but with any number of unfoldings+rewriteUnfold :: Prop -> Proof ()+rewriteUnfold new@(Prop nv na nb) = do+ (Known{..}, _, Goal ps (Prop ov oa ob)) <- getGoal+ checkEqual nv ov+ checkUnfold definitions ov oa na+ checkUnfold definitions ov ob nb+ unsafeReplaceFirstGoal [Goal ps new]++checkEqual a b = when (a /= b) $ badProof $ "Not equal, " ++ show a ++ " vs " ++ show b++checkUnfold defs vars old new = unless (f old new) $ badProof $ "Trusted, invalid unfolding"+ where+ -- variables that have been captured, err on being too conservative+ vars2 = vars ++ concat [childrenBi $ descend (const $ Con $ C "") x | x <- universe old, not $ isVar x]++ f (Var v) e | e /= Var v, v `notElem` vars2, Just x <- lookup v defs = e == x+ f x y = descend (const $ Var $ V "") x == descend (const $ Var $ V "") y &&+ and (zipWith f (children x) (children y))+++-- | Use a new prop which is the same as the first goals prop, but with simplified/rearranged expressions+rewriteEquivalent :: Prop -> Proof ()+rewriteEquivalent new@(Prop nv na nb) = do+ (_, _, Goal pre (Prop ov oa ob)) <- getGoal+ unsafeReplaceFirstGoal [Goal pre new]+++-- | Apply the coinduction principle on the computation+rewriteRecurse :: Proof ()+rewriteRecurse = do+ (known, _, Goal pre p@(Prop vs a b)) <- getGoal+ case (reduce known a, reduce known b) of+ (Nothing, Nothing) -> badProof $ "Cannot reduce\n" ++ show a ++ "\n" ++ show b+ (aa, bb) -> unsafeReplaceFirstGoal [Goal (p:pre) $ Prop vs (fromMaybe a aa) (fromMaybe b bb)]++reduce :: Known -> Exp -> Maybe Exp+reduce Known{..} = f+ where+ f (Lam v x) = Lam v <$> f x+ f (App a b) = (`App` b) <$> f a+ f (Var v) = lookup v definitions+ f (Case x xs) = (`Case` xs) <$> f x+ f x = error $ "step: Don't know, " ++ show x+++-- | Split the expression into multiple subexpressions+rewriteSplit :: Proof ()+rewriteSplit = do+ (_, _, Goal pre (Prop vs a b)) <- getGoal+ checkEqual (descend (const $ Con $ C "") a) (descend (const $ Con $ C "") b)+ when (null $ children a) $ badProof "No children to split apart"+ case (a,b) of+ (Lam v a, Lam _ b) | v `notElem` vs -> unsafeReplaceFirstGoal [Goal pre $ Prop (vs ++ [v]) a b]+ _ -> unsafeReplaceFirstGoal $ zipWith (\a b -> Goal pre $ Prop vs a b) (f a) (f b)+ where+ f (App a b) = [a,b]+ f (Case a bs) = a : map g bs+ where g (PCon c vs, e) = lams vs e+ f (Let _ a b) = [a,b]+++-- | The first goal is a tautology+rewriteTautology :: Proof ()+rewriteTautology = do+ (Known{..}, _, Goal pre p) <- getGoal+ if tautology p || any (==> p) (pre ++ proved) then+ unsafeReplaceFirstGoal []+ else+ badProof "Not a tautology"
+ src/Proof/QED/Type.hs view
@@ -0,0 +1,175 @@+{-# LANGUAGE GeneralizedNewtypeDeriving, DeriveDataTypeable, BangPatterns, TupleSections, PatternGuards #-}++module Proof.QED.Type(+ Known(..), Unknown(..), Goal(..), Side(..),+ QED, getKnown, qed, qedCheat,+ addDefinition, addType, addAssumed, addProved,+ Proof, getUnknown, getGoal, setFocusSide, setFocusAt,+ BadProof(..), badProof, isBadProof,+ unsafeReplaceFirstGoal, unsafeCheat,+ Bind, addBind, runBind,+ Laws(..),+ ) where++import Control.Monad.Trans.State+import Control.Monad.Trans.Reader+import Control.Monad.Trans.Writer+import Control.Monad.Catch as C+import Control.Monad.IO.Class+import Control.Exception+import Control.DeepSeq+import Control.Monad+import Data.IORef+import Data.Typeable+import Proof.Util+import Proof.Exp.Core+import Proof.Exp.Prop+import Control.Applicative+import Data.Monoid+import Prelude++newtype Laws = Laws [Prop]+ deriving Monoid+++---------------------------------------------------------------------+-- KNOWN STATE++newtype QED a = QED (StateT Known IO a)+ deriving (Functor, Applicative, Monad, MonadIO)++qed :: QED a -> IO ()+qed (QED x) = void $ execStateT x (Known [] builtinTypes [] [] False)++qedCheat :: QED a -> IO ()+qedCheat act = qed $ do+ modifyKnown $ \s -> s{cheater=True}+ act++builtinTypes :: [(String,[(Con,Int)])]+builtinTypes =+ [("[]",[(C "[]",0),(C ":",2)])]++-- | All these things are append only+data Known = Known+ {definitions :: [(Var, Exp)]+ ,types :: [(String, [(Con,Int)])]+ ,assumed :: [Prop]+ ,proved :: [Prop]+ ,cheater :: Bool+ } deriving Show++instance NFData Known where+ rnf (Known a b c d e) = rnf5 a b c d e++getKnown :: QED Known+getKnown = QED get++modifyKnown :: (Known -> Known) -> QED ()+modifyKnown f = QED $ do+ x <- get+ x <- return $ f x+ liftIO $ evaluate $ rnf x+ put x++addDefinition :: Var -> Exp -> QED ()+addDefinition a b = modifyKnown $ \s -> s{definitions = definitions s ++ [(a,b)]}++addType :: String -> [(Con,Int)] -> QED ()+addType a b = modifyKnown $ \s -> s{types = types s ++ [(a,b)]}++addAssumed :: Prop -> QED ()+addAssumed a = modifyKnown $ \s -> s{assumed = assumed s ++ [a]}++addProved :: Prop -> Proof () -> QED ()+addProved prop proof = do+ liftIO $ putStr $ show prop+ unknown <- liftIO $ newIORef $ Unknown [Goal [] prop] Nothing 0+ Proof proof <- return $ do+ proof+ unknown <- getUnknown+ unless (null $ goals $ snd unknown) $ do+ badProof $ "Did not prove goals"+ known <- QED get+ liftIO $ proof `runReaderT` (known, unknown) `C.onException` do+ print . goals =<< readIORef unknown+ modifyKnown $ \s -> s{proved = proved s ++ [prop]}+ liftIO $ putStrLn "QED\n"+++---------------------------------------------------------------------+-- UNKNOWN STATE++data Unknown = Unknown+ {goals :: [Goal] -- A list of And alternatives+ ,focusSide :: Maybe Side+ ,focusAt :: Int+ } deriving Show++data Side = LHS | RHS deriving (Show,Eq)++data Goal = Goal [Prop] Prop deriving Show++instance NFData Unknown where+ rnf (Unknown a b c) = rnf3 a b c++instance NFData Side where+ rnf LHS = ()+ rnf RHS = ()++instance NFData Goal where+ rnf (Goal a b) = rnf2 a b++newtype Proof a = Proof (ReaderT (Known, IORef Unknown) IO a)+ deriving (Functor, Applicative, Monad, MonadIO, MonadThrow, MonadCatch, MonadMask)++getUnknown :: Proof (Known, Unknown)+getUnknown = Proof $ do (k,u) <- ask; liftIO $ (k,) <$> readIORef u++getGoal :: Proof (Known, Unknown, Goal)+getGoal = do+ (known, unknown) <- getUnknown+ case goals unknown of+ [] -> badProof "No goals left, proof is already complete"+ g:gs -> return (known, unknown, g)++unsafeReplaceFirstGoal :: [Goal] -> Proof ()+unsafeReplaceFirstGoal x = do+ liftIO $ evaluate $ rnf x+ (_, u) <- Proof ask+ liftIO $ modifyIORef u $ \s -> s{goals = x ++ drop 1 (goals s)}++unsafeCheat :: String -> Proof ()+unsafeCheat msg = do+ (known, _) <- getUnknown+ unless (cheater known) $ badProof "Must use qedCheat to enable cheating"+ unsafeReplaceFirstGoal []+ liftIO $ putStrLn $ "unsafeCheat: " ++ msg++setFocusSide :: Maybe Side -> Proof ()+setFocusSide x | () <- rnf x = do (_, u) <- Proof ask; liftIO $ modifyIORef u $ \s -> s{focusSide=x}++setFocusAt :: Int -> Proof ()+setFocusAt !x = do (_, u) <- Proof ask; liftIO $ modifyIORef u $ \s -> s{focusAt=x}++newtype BadProof = BadProof String deriving Typeable+instance Show BadProof where show (BadProof x) = "Bad proof: " ++ x+instance Exception BadProof++badProof :: String -> Proof a+badProof = throwM . BadProof++isBadProof :: Proof () -> Proof Bool+isBadProof act = C.catch (act >> return False) $ \BadProof{} -> return True++---------------------------------------------------------------------+-- BINDINGS++newtype Bind a = Bind (Writer [(Var,Exp)] a)+ deriving (Functor, Applicative, Monad)++addBind :: Var -> Exp -> Bind ()+addBind a b = Bind $ tell [(a,b)]++runBind :: Bind () -> [(Var,Exp)]+runBind (Bind x) = execWriter x
+ src/Proof/Util.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE PatternGuards #-}++-- | Generic utilities.+module Proof.Util(module Proof.Util) where++import System.IO.Unsafe+import System.Environment+import Control.DeepSeq+++rnf2 a b = rnf a `seq` rnf b+rnf3 a b c = rnf a `seq` rnf b `seq` rnf c+rnf4 a b c d = rnf a `seq` rnf b `seq` rnf c `seq` rnf d+rnf5 a b c d e = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e++headNote note (x:xs) = x+headNote note [] = error $ "headNote on [], " ++ note++fast = "--fast" `elem` unsafePerformIO getArgs++idempotent :: (Show a, Eq a) => String -> (a -> a) -> (a -> a)+idempotent name f x0+ | fast = x1+ | x1 == x2 = x1+ | otherwise = error $ unlines+ ["START Idempotent check failed for " ++ name ++ "!"+ ,"Input:"+ ,show x0+ ,"After first application:"+ ,show x1+ ,"After second application:"+ ,show x2+ ,"END Idempotent check failed for " ++ name ++ "!"+ ]+ where x1 = f x0+ x2 = f x1++equivalentOn :: (Show a, Show b, Eq b) => (a -> b) -> String -> a -> a -> a+equivalentOn op name x y+ | fast = y+ | xx == yy = y+ | otherwise = unsafePerformIO $ do+ writeFile "error.log" $ "-- Equivalent check failed for " ++ name ++ "\n" ++ show x+ error $ unlines+ ["START Equivalent check failed for " ++ name ++ "!"+ ,"Input:"+ ,show x+ ,"Output:"+ ,show y+ ,"Input (reduced):"+ ,show xx+ ,"Output (reduced):"+ ,show yy+ ,"END Equivalent check failed for " ++ name ++ "!"+ ]+ where xx = op x+ yy = op y++simpleReadsPrec :: (String -> a) -> (Int -> ReadS a)+simpleReadsPrec f _ s = [(f s, "")]
+ test/Classes.hs view
@@ -0,0 +1,131 @@++module Classes(classes) where++import Proof.QED+import Control.Monad++classes = do+ lawsMonoid <- laws $ do+ law "a => a <> mempty = a"+ law "a => mempty <> a = a"+ law "a b c => a <> (b <> c) = (a <> b) <> c"++ lawsFunctor <- laws $ do+ law "fmap id = id"+ law "f g => fmap f . fmap g = fmap (f . g)"++ lawsApplicative <- laws $ do+ law "v => pure id <*> v = v"+ law "u v w => pure (.) <*> u <*> v <*> w = u <*> (v <*> w)"+ law "f x => pure f <*> pure x = pure (f x)"+ law "u y => u <*> pure y = pure ($ y) <*> u"++ lawsMonad <- laws $ do+ law "a k => return a >>= k = k a"+ law "m => m >>= return = m"+ law "m k h => m >>= (\\x -> k x >>= h) = (m >>= k) >>= h"++ prove "x => [] ++ x = x" $ do+ unfold "++"++ prove "x => x ++ [] = x" $ do+ recurse+ rhs $ strict "[]"++ prove "x y z => (x ++ y) ++ z = x ++ (y ++ z)" $ do+ recurse+ bhs $ unfold "++"++ satisfy "Monoid []" lawsMonoid $ do+ bind "mempty = []"+ bind "(<>) = (++)"++ prove "map id = id" $ do+ bhs $ unfold "id"+ expand+ recurse+ rhs $ strict "[]"++ prove "f g => map f . map g = map (f . g)" $ do+ twice $ unfold "."+ twice unlet+ rhs expand+ recurse+ unfold "map"++ satisfy "Functor []" lawsFunctor $ do+ bind "fmap = map"++ decl "return_List = (:[])"+ decl "bind_List = flip concatMap"+ let unwind = mapM_ (perhaps . many . unfold) ["return_List","bind_List","concatMap","concat","flip","."]++ when False $ prove "a k => return_List a `bind_List` k = k a" $ do+ unwind+ unfold "map"+ unfold "foldr"+ unfold "foldr"+ unfold "map"++ prove "m => m `bind_List` return_List = m" $ do+ unwind+ recurse+ unfold "map"+ rhs $ strict "[]"+ twice $ unfold "++"++ prove "m k h => m `bind_List` (\\x -> k x `bind_List` h) = (m `bind_List` k) `bind_List` h" $ do+ unwind+ divide+ recurse+ rhs $ unfold "foldr"+ rhs $ unfold "map"+ rhs $ unfold "++"+ unsafeCheat "bored"++ skip $ satisfy "Monad []" lawsMonad $ do+ bind "return = return_List"+ bind "(>>=) = bind_List"++ prove "v => return id `ap` v = v" $ do+ unfold "ap"+ unfold "liftM2"+ unfold "$"+ unsafeCheat "need laws"++{-+-- (>>=) (return id) (\ b -> (>>=) a (\ c -> return (b c))) = a+-- return a >>= k = k a"+-- (>>=) a (\ c -> return c)) = a+-- a = a++data Monad a = Return a | forall x . Bind (Monad x) (x -> Monad a)++eval (Return a) = a+eval (Bind (Return a) f) = f a+eval ++-}++ skip $ prove "u v w => return (.) `ap` u `ap` v `ap` w = u `ap` (v `ap` w)" $ do+ replicateM_ 100 unfold_++ skip $ prove "f x => return f `ap` return x = return (f x)" $ do+ unfold "ap"+ unfold "liftM2"+ unfold "$"+ unlet+ return ()++ skip $ do+ prove "u y => u `ap` return y = return ($ y) `ap` u" $ do+ return ()++ lawsMonad <- laws $ do+ law "a k => return a >>= k = k a"+ law "m => m >>= return = m"+ law "m k h => m >>= (\\x -> k x >>= h) = (m >>= k) >>= h"++ satisfy "Applicative Monad" lawsApplicative $ do+ bind "pure = return"+ bind "(<*>) = ap"
+ test/HLint.hs view
@@ -0,0 +1,121 @@++module HLint(hlint) where++import Proof.QED+import Control.Monad.IO.Class++hlint = do+ decl "data Nat = S Nat | Z"+ decl "data Int = Neg Nat | Zero | Pos Nat"++ skip $ prove "n x => take n (repeat x) = replicate n x" $ do+ unfold "replicate"++ skip $ prove "n x => head (drop n x) = x !! n" $ do+ unfold "head"+ unfold "error"+ recurse+++ prove "f => (($) . f) = f" $ do+ unfold "$"+ unfold "."+ unlet+ twice $ rhs expand++ prove "f z g x => foldr f z (map g x) = foldr (f . g) z x" $ do+ unfold "."+ recurse+ unfold "map"++ prove "(\\x -> cycle [x]) = repeat" $ do+ rhs expand+ recurse+ unlet+ twice $ unfold "++"++ prove "f x => zipWith f (repeat x) = map (f x)" $ do+ expand+ rhs expand+ recurse+ unlet+ unfold "repeat"++ prove "x y => (if x then False else y) = not x && y" $ do+ many unfold_++ skip $ prove "map fromJust . filter isJust = catMaybes" $ do+ unfold "map"+ unfold "catMaybes"+ unfold "concatMap"+ unfold "concat"+ many $ unfold "."+ unlet+ recurse+ unfold "isJust"+ unfold "fromJust"+ bhs $ unfold "map"+ unfold "++"++ prove "mapMaybe id = catMaybes" $ do+ unfold "mapMaybe"+ unfold "."+ unlet+ rhs expand+ divide+ unfold "id"+ recurse+ rhs $ strict "[]"++ prove "f x => map f (repeat x) = repeat (f x)" $ do+ recurse+ unfold "repeat"+ unlet++ prove "f x y => map (uncurry f) (zip x y) = zipWith f x y" $ do+ unfold "zip"+ recurse+ unlet+ unfold "uncurry"+ unfold "zipWith"+ unlet+ unfold "fst"+ unfold "snd"++ prove "iterate id = repeat" $ do+ expand+ rhs expand+ recurse+ at 1 $ unfold "id"++ prove "f x => catMaybes (map f x) = mapMaybe f x" $ do+ unfold "mapMaybe"+ unfold "."++ skip $ prove "concatMap maybeToList = catMaybes" $ do+ unfold "catMaybes"+ liftIO $ print "here1"+ expand+ liftIO $ print "here2"+ twice divide+ unfold "maybeToList"++ skip $ prove "f g x => concatMap f (map g x) = concatMap (f . g) x" $ do+ twice $ unfold "concatMap"+ twice $ unfold "concat"++ skip $ prove "x => head (reverse x) = last x" $ do+ unfold "head"+ unfold "reverse"+ recurse+ unlet+ bhs unfold_+ unfold "foldl"+ unlet+ unfold "flip"+ error "generalise" -- unsafeReplace "flip (:) [] a" "a"+ recurse+ unlet+ unfold "flip"+ error "generalise" -- unsafeReplace "flip (:) a b" "a"+
+ test/Main.hs view
@@ -0,0 +1,27 @@++module Main(main) where++import Classes+import HLint+import Proof.QED++-- TODO: Formalise generalise properly. Can it be done as extraction? Is strict generalisation always sufficient?+-- TODO: Write an automatic prover++-- TOTHINK: What to do about type classes? How do you prove laws about instances? How do you associate laws?+-- Add an assume to a proof?+-- TOTHINK: What do I do about things like +? Do I assume them like I do for type classes?+-- TOTHINK: Do I just state the laws and leave it at that?++main = qedCheat $ do+ imports "Builtin"+ imports "Prelude"+ imports "List"+ imports "Maybe"+ imports "Monad"++ law "a b => a + b = b + a"+ law "a => a + 0 = a"++ classes+ hlint