simplify

Documentation/SBV/Examples/Uninterpreted/AUF.hs

@@ -6,7 +6,7 @@
 -- Maintainer: [email protected]
 -- Stability : experimental
 --
--- Formalizes and proves the following theorem, about arithmetic,
+-- Formalizes and proves the following theorem about arithmetic,
 -- uninterpreted functions, and arrays. (For reference, see <http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf>
 -- slide number 24):
 --
@@ -27,6 +27,7 @@
 -- The function @read@ and @write@ are usual array operations.
 -----------------------------------------------------------------------------
 
+{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
@@ -35,30 +36,22 @@ module Documentation.SBV.Examples.Uninterpreted.AUF where
 
 import Data.SBV
 
---------------------------------------------------------------
--- * Model using functional arrays
---------------------------------------------------------------
+#ifndef HADDOCK
+-- $setup
+-- >>> -- For doctest purposes only:
+-- >>> import Data.SBV
+#endif
 
 -- | Uninterpreted function in the theorem
 f :: SWord32 -> SWord64
 f = uninterpret "f"
 
--- | Correctness theorem. We state it for all values of @x@, @y@, and
--- the given array @a@. Note that we're being generic in the type of
--- array we're expecting.
+-- | Correctness theorem. We state it for all values of @x@, @y@, and the given array @a@. We have:
+--
+-- >>> prove thm
+-- Q.E.D.
 thm :: SWord32 -> SWord32 -> SArray Word32 Word32 -> SBool
 thm x y a = lhs .=> rhs
   where lhs = x + 2 .== y
         rhs =     f (readArray (writeArray a x 3) (y - 2))
               .== f (y - x + 1)
-
--- | Prove it using SMT-Lib arrays.
---
--- >>> proveSArray
--- Q.E.D.
-proveSArray :: IO ThmResult
-proveSArray = prove $ do
-                x <- free "x"
-                y <- free "y"
-                a :: SArray Word32 Word32 <- sArray_
-                return $ thm x y a