summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNeilMitchell <>2015-11-03 22:18:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2015-11-03 22:18:00 (GMT)
commit8837af9d884281ff1a4938fff2c40cbc83e0a073 (patch)
tree60aab14a64f82709140343d4867c5e2e1af70535
version 0.0HEAD0.0master
-rw-r--r--CHANGES.txt4
-rw-r--r--LICENSE30
-rw-r--r--README.md5
-rw-r--r--Setup.hs2
-rw-r--r--imports/Builtin.hs15
-rw-r--r--imports/List.hs223
-rw-r--r--imports/Maybe.hs56
-rw-r--r--imports/Monad.hs86
-rw-r--r--imports/Prelude.hs1198
-rw-r--r--qed.cabal54
-rw-r--r--src/Proof/Exp/Core.hs282
-rw-r--r--src/Proof/Exp/HSE.hs161
-rw-r--r--src/Proof/Exp/Prop.hs55
-rw-r--r--src/Proof/QED.hs461
-rw-r--r--src/Proof/QED/Internal.hs17
-rw-r--r--src/Proof/QED/Trusted.hs90
-rw-r--r--src/Proof/QED/Type.hs175
-rw-r--r--src/Proof/Util.hs60
-rw-r--r--test/Classes.hs131
-rw-r--r--test/HLint.hs121
-rw-r--r--test/Main.hs27
21 files changed, 3253 insertions, 0 deletions
diff --git a/CHANGES.txt b/CHANGES.txt
new file mode 100644
index 0000000..5526546
--- /dev/null
+++ b/CHANGES.txt
@@ -0,0 +1,4 @@
+Changelog for QED
+
+0.0
+ Initial version
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..0028042
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..f6dd046
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+# QED Prover [![Hackage version](https://img.shields.io/hackage/v/qed.svg?label=Hackage)](https://hackage.haskell.org/package/qed) [![Build Status](https://img.shields.io/travis/ndmitchell/qed.svg)](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".
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/imports/Builtin.hs b/imports/Builtin.hs
new file mode 100644
index 0000000..23b006c
--- /dev/null
+++ b/imports/Builtin.hs
@@ -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
diff --git a/imports/List.hs b/imports/List.hs
new file mode 100644
index 0000000..2bcd481
--- /dev/null
+++ b/imports/List.hs
@@ -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)
diff --git a/imports/Maybe.hs b/imports/Maybe.hs
new file mode 100644
index 0000000..1caf4e2
--- /dev/null
+++ b/imports/Maybe.hs
@@ -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
diff --git a/imports/Monad.hs b/imports/Monad.hs
new file mode 100644
index 0000000..c0ed901
--- /dev/null
+++ b/imports/Monad.hs
@@ -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')
diff --git a/imports/Prelude.hs b/imports/Prelude.hs
new file mode 100644
index 0000000..57f35be
--- /dev/null
+++ b/imports/Prelude.hs
@@ -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
diff --git a/qed.cabal b/qed.cabal
new file mode 100644
index 0000000..b2d3b92
--- /dev/null
+++ b/qed.cabal
@@ -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
diff --git a/src/Proof/Exp/Core.hs b/src/Proof/Exp/Core.hs
new file mode 100644
index 0000000..e388f90
--- /dev/null
+++ b/src/Proof/Exp/Core.hs
@@ -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
diff --git a/src/Proof/Exp/HSE.hs b/src/Proof/Exp/HSE.hs
new file mode 100644
index 0000000..43541fa
--- /dev/null
+++ b/src/Proof/Exp/HSE.hs
@@ -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
diff --git a/src/Proof/Exp/Prop.hs b/src/Proof/Exp/Prop.hs
new file mode 100644
index 0000000..e84e4e2
--- /dev/null
+++ b/src/Proof/Exp/Prop.hs
@@ -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
diff --git a/src/Proof/QED.hs b/src/Proof/QED.hs
new file mode 100644
index 0000000..068f23c
--- /dev/null
+++ b/src/Proof/QED.hs
@@ -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
+-}
diff --git a/src/Proof/QED/Internal.hs b/src/Proof/QED/Internal.hs
new file mode 100644
index 0000000..0264405
--- /dev/null
+++ b/src/Proof/QED/Internal.hs
@@ -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
diff --git a/src/Proof/QED/Trusted.hs b/src/Proof/QED/Trusted.hs
new file mode 100644
index 0000000..902afb7
--- /dev/null
+++ b/src/Proof/QED/Trusted.hs
@@ -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"
diff --git a/src/Proof/QED/Type.hs b/src/Proof/QED/Type.hs
new file mode 100644
index 0000000..0ed11ad
--- /dev/null
+++ b/src/Proof/QED/Type.hs
@@ -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
diff --git a/src/Proof/Util.hs b/src/Proof/Util.hs
new file mode 100644
index 0000000..405cf35
--- /dev/null
+++ b/src/Proof/Util.hs
@@ -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, "")]
diff --git a/test/Classes.hs b/test/Classes.hs
new file mode 100644
index 0000000..458c179
--- /dev/null
+++ b/test/Classes.hs
@@ -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"
diff --git a/test/HLint.hs b/test/HLint.hs
new file mode 100644
index 0000000..6dd7edd
--- /dev/null
+++ b/test/HLint.hs
@@ -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"
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
index 0000000..ba53847
--- /dev/null
+++ b/test/Main.hs
@@ -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