From 569d3444260261462c71d45bce3b1596335d8d75 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Tue, 24 Dec 2024 11:36:20 -0800
Subject: [PATCH] simplify

---
 .../SBV/Examples/KnuckleDragger/Lists.hs      | 48 +++++++++----------
 Makefile                                      |  2 +-
 buildUtils/simpHaddock.hs                     | 26 ++++++----
 3 files changed, 43 insertions(+), 33 deletions(-)

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
index 89e1613e6..b69567a28 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
@@ -321,30 +321,6 @@ foldrFusion = runKDWith cvc5 $ do
 
    lemma "foldrFusion" (\(Forall @"xs" xs) -> p xs) [h1, h2, induct p]
 
--- * Foldr over append
-
--- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@
---
--- We have:
---
--- >>> foldrOverAppend
--- Lemma: foldrOverAppend                  Q.E.D.
--- [Proven] foldrOverAppend
-foldrOverAppend :: IO Proof
-foldrOverAppend = runKD $ do
-   let a :: SA
-       a = uninterpret "a"
-
-       f :: SA -> SA -> SA
-       f = uninterpret "f"
-
-       p xs ys = foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs
-
-   lemma "foldrOverAppend"
-          (\(Forall @"xs" xs) (Forall @"ys" ys) -> p xs ys)
-          -- Induction is done on the last element. Here we want to induct on xs, hence the flip below.
-          [induct (flip p)]
-
 -- * Map, append, and reverse
 
 -- | @map f (xs ++ ys) == map f xs ++ map f ys@
@@ -445,6 +421,30 @@ badRevLen = runKD $ do
 
    pure ()
 
+-- * Foldr over append
+
+-- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@
+--
+-- We have:
+--
+-- >>> foldrOverAppend
+-- Lemma: foldrOverAppend                  Q.E.D.
+-- [Proven] foldrOverAppend
+foldrOverAppend :: IO Proof
+foldrOverAppend = runKD $ do
+   let a :: SA
+       a = uninterpret "a"
+
+       f :: SA -> SA -> SA
+       f = uninterpret "f"
+
+       p xs ys = foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs
+
+   lemma "foldrOverAppend"
+          (\(Forall @"xs" xs) (Forall @"ys" ys) -> p xs ys)
+          -- Induction is done on the last element. Here we want to induct on xs, hence the flip below.
+          [induct (flip p)]
+
 {- Can't converge
 -- * Foldl over append
 
diff --git a/Makefile b/Makefile
index f8716030e..4e30da69e 100644
--- a/Makefile
+++ b/Makefile
@@ -60,7 +60,7 @@ install: tags
 	@$(TIME) cabal new-install --lib --force-reinstalls
 
 docs:
-	cabal new-haddock ${CABAL_OPTS} --haddock-option=--hyperlinked-source --haddock-option=--no-warnings --haddock-option="--optghc=-DHADDOCK" | ghc ./buildUtils/simpHaddock.hs -e main
+	cabal new-haddock ${CABAL_OPTS} --haddock-option=--no-warnings --haddock-option=--hyperlinked-source --haddock-option=--no-warnings --haddock-option="--optghc=-DHADDOCK" | ghc ./buildUtils/simpHaddock.hs -e main
 
 # To upload docs to hackage, first run the below target (part of release), then run the next target..
 hackage-docs:
diff --git a/buildUtils/simpHaddock.hs b/buildUtils/simpHaddock.hs
index 025306548..59e630fcc 100644
--- a/buildUtils/simpHaddock.hs
+++ b/buildUtils/simpHaddock.hs
@@ -2,6 +2,7 @@
 
 module Main where
 
+import Data.Char
 import Data.List
 import qualified Control.Exception as C
 
@@ -13,11 +14,13 @@ msg s | verbose = putStrLn $ "HADDOCK SIMPLIFY: " ++ s
       | True    = pure ()
 
 main :: IO ()
-main = go False
+main = go False Nothing
 
-go :: Bool -> IO ()
-go failed = do
-  mbLn <- (Just <$> getLine) `C.catch` (\(_ :: C.SomeException) -> return Nothing)
+go :: Bool -> Maybe String -> IO ()
+go failed mbInp = do
+  mbLn <- case mbInp of
+           Just s  -> pure $ Just s
+           Nothing -> (Just <$> getLine) `C.catch` (\(_ :: C.SomeException) -> return Nothing)
   case mbLn of
     Nothing -> if failed
                   then error "*** There were files that had missing haddock-documentation. Stopping."
@@ -31,16 +34,23 @@ go failed = do
                           if    l1 == "    You may be able to disambiguate the identifier by qualifying it or"
                              && l2 == "    by specifying the type/value namespace explicitly."
                              then do msg "Skipped lines"
-                                     go failed
+                                     go failed Nothing
                              else do msg ln
                                      msg l1
                                      msg l2
                                      msg l3
                                      msg l4
                                      msg l5
-                                     go failed
-                  else do putStrLn ln
-                          go (failed || bad ln)
+                                     go failed Nothing
+                  else if "Warning: " `isPrefixOf` ln && ": could not find link destinations for:" `isInfixOf` ln
+                          then do let skip = do l <- getLine
+                                                if ("-" `isPrefixOf` dropWhile isSpace l)
+                                                   then skip
+                                                   else pure l
+                                  l <- skip
+                                  go failed (Just l)
+                          else do putStrLn ln
+                                  go (failed || bad ln) Nothing
 
 bad :: String -> Bool
 bad ln