Tidying up nofib examples

plutus-benchmark/bench/Main.hs

@@ -1,3 +1,5 @@
+{- | Plutus benchmarks based on some nofib examples. -}
+
 module Main where
 
 import           Criterion.Main
@@ -45,7 +47,6 @@ benchKnights depth sz =
 config :: Config
 config = defaultConfig
   { reportFile = Just "report.html"
-  , jsonFile   = Just "report.json"
   , template   = "./default.tpl"
   , timeLimit  = 60.0  -- Run each benchmark for at least one minute
   }
@@ -65,33 +66,38 @@ config = defaultConfig
 
 main :: IO ()
 main = defaultMainWith config [
-    bgroup "clausify" [ bench "formula3" $ benchClausify Clausify.F3
+    bgroup "clausify" [ bench "formula1" $ benchClausify Clausify.F1
+                      , bench "formula2" $ benchClausify Clausify.F2
+                      , bench "formula3" $ benchClausify Clausify.F3
                       , bench "formula4" $ benchClausify Clausify.F4
                       , bench "formula5" $ benchClausify Clausify.F5
-                      , bench "formula6" $ benchClausify Clausify.F6
-                      , bench "formula7" $ benchClausify Clausify.F7
                       ]
-  , bgroup "primetest" [ bench "5digits"  $ benchPrime Prime.P5
-                       , bench "8digits"  $ benchPrime Prime.P8
+  , bgroup "primetest" [ bench "05digits" $ benchPrime Prime.P5
+                       , bench "08digits" $ benchPrime Prime.P8
                        , bench "10digits" $ benchPrime Prime.P10
                        , bench "20digits" $ benchPrime Prime.P20
                        , bench "30digits" $ benchPrime Prime.P30
                        , bench "40digits" $ benchPrime Prime.P40
                        , bench "50digits" $ benchPrime Prime.P50
                        , bench "60digits" $ benchPrime Prime.P60
                        ]
-  , bgroup "queens" [ -- N-queens problem on a 5x5 board
+  , bgroup "queens4x4" [ -- N-queens problem on a 4x4 board
+                      bench "bt"    $ benchQueens 4 Queens.Bt
+                    , bench "bm"    $ benchQueens 4 Queens.Bm
+                    , bench "bjbt1" $ benchQueens 4 Queens.Bjbt1
+                    , bench "bjbt2" $ benchQueens 4 Queens.Bjbt2
+                    , bench "fc"    $ benchQueens 4 Queens.Fc
+                    ]
+  , bgroup "queens5x5" [ -- N-queens problem on a 5x5 board
                       bench "bt"    $ benchQueens 5 Queens.Bt
                     , bench "bm"    $ benchQueens 5 Queens.Bm
-                    , bench "bjbt"  $ benchQueens 5 Queens.Bjbt
                     , bench "bjbt1" $ benchQueens 5 Queens.Bjbt1
+                    , bench "bjbt2" $ benchQueens 5 Queens.Bjbt2
                     , bench "fc"    $ benchQueens 5 Queens.Fc
                     ]
   , bgroup "knights" [ -- Knight's tour on an NxN board; no solutions for N odd or N=4
                        bench "4x4" $ benchKnights 150 4
-                     , bench "5x5" $ benchKnights 150 5
                      , bench "6x6" $ benchKnights 150 6
-                     , bench "7x7" $ benchKnights 150 7
                      , bench "8x8" $ benchKnights 150 8
                      ]
        ]

plutus-benchmark/src/Plutus/Benchmark/Clausify.hs

@@ -121,47 +121,47 @@ replicate :: Integer -> a -> [a]
 replicate n a = if n <= 0 then []
                 else a:(replicate (n-1) a)
 
-{-# INLINABLE formula1 #-}  -- Overflow
-formula1 :: Formula  -- (a = a = a) = (a = a = a) = (a = a = a)
-formula1 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
-               (Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
-                    (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1))))
-
-{-# INLINABLE formula2 #-} -- Overflow
-formula2 :: Formula -- (a = b = c) = (d = e = f) = (g = h = i)
-formula2 = Eqv (Eqv (Sym 1) (Eqv (Sym 2) (Sym 3)))
-               (Eqv (Eqv (Sym 4) (Eqv (Sym 5) (Sym 6)))
-                    (Eqv (Sym 7) (Eqv (Sym 8) (Sym 9))))
-
-{-# INLINABLE formula3 #-}
-formula3 :: Formula  -- (a = a = a) = (a = a = a)
-formula3 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
-               (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
-
-{-# INLINABLE formula4 #-} -- One execution takes about 0.35s and 300 MB
-formula4 :: Formula  -- (a = a) = (a = a) = (a = a)
-formula4 = Eqv (Eqv (Sym 1) (Sym 1))
+{-# INLINABLE formula1 #-}
+formula1 :: Formula  -- (a = a) = (a = a) = (a = a)
+formula1 = Eqv (Eqv (Sym 1) (Sym 1))
                (Eqv (Eqv (Sym 1) (Sym 1))
                     (Eqv (Sym 1) (Sym 1)))
 
-{-# INLINABLE formula5 #-}  -- One execution takes about 1.5s and 660 MB
-formula5 :: Formula  -- (a = a = a) = (a = a) = (a = a)
-formula5 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
+{-# INLINABLE formula2 #-} -- One execution takes about 0.35s and 300 MB
+formula2 :: Formula  -- (a = a = a) = (a = a = a)
+formula2 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
+               (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
+
+{-# INLINABLE formula3 #-}  -- One execution takes about 1.5s and 660 MB
+formula3 :: Formula  -- (a = a = a) = (a = a) = (a = a)
+formula3 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
                (Eqv (Eqv (Sym 1) (Sym 1))
                     (Eqv (Sym 1) (Sym 1)))
 
-{-# INLINABLE formula6 #-}  -- One execution takes about 2s and 1 GB
-formula6 :: Formula  -- (a = b = c) = (d = e) = (f = g)
-formula6 = Eqv (Eqv (Sym 1) (Eqv (Sym 2) (Sym 3)))
+{-# INLINABLE formula4 #-}  -- One execution takes about 2s and 1 GB
+formula4 :: Formula  -- (a = b = c) = (d = e) = (f = g)
+formula4 = Eqv (Eqv (Sym 1) (Eqv (Sym 2) (Sym 3)))
                (Eqv (Eqv (Sym 4) (Sym 5))
                     (Eqv (Sym 6) (Sym 7)))
 
-{-# INLINABLE formula7 #-}  -- One execution takes about 11s and 5 GB
-formula7 :: Formula  -- (a = a = a) = (a = a = a) = (a = a)
-formula7 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
+{-# INLINABLE formula5 #-}  -- One execution takes about 11s and 5 GB
+formula5 :: Formula  -- (a = a = a) = (a = a = a) = (a = a)
+formula5 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
                (Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
                     (Eqv (Sym 1) (Sym 1)))
 
+{-# INLINABLE formula6 #-}  -- Overflow
+formula6 :: Formula  -- (a = a = a) = (a = a = a) = (a = a = a)
+formula6 = Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
+               (Eqv (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1)))
+                    (Eqv (Sym 1) (Eqv (Sym 1) (Sym 1))))
+
+{-# INLINABLE formula7 #-} -- Overflow
+formula7 :: Formula -- (a = b = c) = (d = e = f) = (g = h = i)
+formula7 = Eqv (Eqv (Sym 1) (Eqv (Sym 2) (Sym 3)))
+               (Eqv (Eqv (Sym 4) (Eqv (Sym 5) (Sym 6)))
+                    (Eqv (Sym 7) (Eqv (Sym 8) (Sym 9))))
+
 data StaticFormula = F1 | F2 | F3 | F4 | F5 | F6 | F7
 
 {-# INLINABLE getFormula #-}

plutus-benchmark/src/Plutus/Benchmark/Knights.hs

@@ -45,7 +45,7 @@ repl n a =
     if n == 0 then []
     else a:(repl (n-1) a)
 
--- Original version used infinite lists.
+--% Original version used infinite lists.
 {-# INLINABLE mkStarts #-}
 mkStarts :: Integer -> [(Integer, ChessSet)]
 mkStarts sze =
@@ -57,21 +57,21 @@ mkStarts sze =
 root :: Integer -> Queue (Integer, ChessSet)
 root sze = addAllFront (mkStarts sze) createQueue
 
-{- Original version
+{-% Original version
 root sze = addAllFront
              (Tx.zip [-(sze*sze)+1,-(sze*sze)+1..]
                   (zipWith
                      startTour
                       [(x,y) | x <- [1..sze], y <- [1..sze]]
                      (take' (sze*sze) [sze,sze..])))
              createQueue
--}
+%-}
 
 
 type P = (Integer, ChessSet)
 
 {-# INLINABLE depthSearch #-}
--- Added a depth parameter to stop things getting out of hand in the strict world.
+--% Added a depth parameter to stop things getting out of hand in the strict world.
 depthSearch :: (Eq a) => Integer -> Queue a -> (a -> [a]) -> (a -> Bool) -> Queue a
 depthSearch depth q growFn finFn
    | depth == 0             = []
@@ -84,7 +84,7 @@ depthSearch depth q growFn finFn
                                  growFn
                                  finFn
 
--- Only for textual output of PLC scripts
+--% Only for textual output of PLC scripts
 unindent :: PLC.Doc ann -> [String]
 unindent d = map (dropWhile isSpace) $ (lines . show $ d)
 

plutus-benchmark/src/Plutus/Benchmark/Knights/ChessSetList.hs

@@ -21,10 +21,10 @@ import           Language.PlutusTx.Prelude as Tx hiding (init)
 type Tile     = (Integer,Integer)
 
 data ChessSet = Board
-                Integer      -- Size of board (along edge)
-                Integer      -- Current move number
-                (Maybe Tile) -- Initial square: see Note [deleteFirst] below
-                [Tile]       -- All squares visited (in reverse: the last element is the initial square).
+                Integer      --% Size of board (along edge)
+                Integer      --% Current move number
+                (Maybe Tile) --% Initial square: see Note [deleteFirst] below
+                [Tile]       --% All squares visited (in reverse: the last element is the initial square).
 
 instance Tx.Eq ChessSet where
     _ == _ = True
@@ -48,7 +48,7 @@ noPieces (Board _ n _ _) = n
 addPiece :: Tile -> ChessSet -> ChessSet
 addPiece t (Board s n f ts) = Board s (n+1) f (t:ts)
 
--- Remove the last element from a list
+--% Remove the last element from a list
 {-# INLINABLE init #-}
 init :: [a] -> [a]
 init l = case reverse l of
@@ -64,17 +64,17 @@ secondLast l =
       _:a:_ -> Just a
 
 
-{-  Note [deleteFirst].
-   deleteFirst removes the first position from the tour.
-   Since the sequence of positions (ts) is stored in reverse this involves
-   deleting the last element of ts and also storing the second-last element of
-   ts as the new starting position.  In the strict world this will *fail* if the
-   length of ts is 1.  The lazy version got away with this because the starting
-   position is never examined in that case (possibly just through luck: with
-   enough backtracking that might still happen).  To solve this we have to store
-   the starting position as a Maybe value, deferring any error until we actually
-   look at it.
--}
+{-%  Note [deleteFirst].
+    deleteFirst removes the first position from the tour.
+    Since the sequence of positions (ts) is stored in reverse this involves
+    deleting the last element of ts and also storing the second-last element of
+    ts as the new starting position.  In the strict world this will *fail* if the
+    length of ts is 1.  The lazy version got away with this because the starting
+    position is never examined in that case (possibly just through luck: with
+    enough backtracking that might still happen).  To solve this we have to store
+    the starting position as a Maybe value, deferring any error until we actually
+    look at it.
+%-}
 
 {-# INLINABLE deleteFirst #-}
 deleteFirst :: ChessSet -> ChessSet
@@ -121,9 +121,12 @@ isSquareFree x (Board _ _ _ ts) = notIn x ts
 
 {-
 
-{-# INLINABLE shint #-}
-shint :: Tx.Integer -> Tx.String
-shint n =
+--% Everything below here is only needed for printing boards.
+--% This is useful for debugging.
+
+{-# INLINABLE showInteger #-}
+showInteger :: Tx.Integer -> Tx.String
+showInteger n =
     if n == 0 then "0"
        else if n == 1 then "1"
             else if n == 2 then "2"
@@ -133,18 +136,15 @@ shint n =
                                 else if n == 6 then "6"
                                      else if n == 7 then "7"
                                           else "?"
-{-# INLINABLE shl #-}
-shl :: [Integer] -> String
-shl []        = "0"
-shl [_]       = "1"
-shl [_,_]     = "2"
-shl [_,_,_]   = "3"
-shl [_,_,_,_] = "4"
-shl _         = "?"
-
-
--- Everything below here is only needed for printing boards.
--- This is useful for debugging.
+
+{-# INLINABLE showList #-}
+showList :: [Integer] -> String
+showList []        = "0"
+showList [_]       = "1"
+showList [_,_]     = "2"
+showList [_,_,_]   = "3"
+showList [_,_,_,_] = "4"
+showList _         = "?"
 
 instance Show ChessSet where
    showsPrec _ (Board sze n _ ts)

plutus-benchmark/src/Plutus/Benchmark/Knights/Sort.hs

@@ -42,7 +42,7 @@ quickSort []     = []
 quickSort (x:xs) = (quickSort [y | y<-xs, y Tx.< x]) ++ [x] ++
                    (quickSort [y | y<-xs, y Tx.>= x])
 
-{-
+{-% These don't work in Plutus, and aren't used in the original program.
 {-# INLINABLE lazySortLe #-}
 lazySortLe :: (a -> a -> Bool) -> [a] -> [a]
 lazySortLe le l = lazyQsort le   l []
@@ -88,7 +88,7 @@ rqpart le x (y:ys) rle rgt r =
         rqpart le x ys (y:rle) rgt r
     else
         rqpart le x ys rle (y:rgt) r
--}
+%-}
 
 {-# INLINABLE randomIntegers #-}
 randomIntegers :: Integer -> Integer -> [Integer]

plutus-benchmark/src/Plutus/Benchmark/Knights/Utils.hs

@@ -6,22 +6,7 @@ import           Language.PlutusTx          as PlutusTx
 import           Language.PlutusTx.Builtins as Tx
 import           Language.PlutusTx.Prelude  as PLC
 
-{-
-{-# INLINABLE length' #-}
-length' :: [a] -> Integer
-length' []    = 0
-length' (_:t) = 1 + length' t
--}
-
 {-# INLINABLE take' #-}
 take' :: Integer -> [a] -> [a]
 take' _ []     = []
 take' n (a:as) = a:(take' (n-1) as)
-
-{-
-{-# INLINABLE nth #-}
-nth :: Integer -> [a] -> a
-nth _ []     = Tx.error ()
-nth 0 (a:_)  = a
-nth n (_:as) = nth (n-1) as
--}

plutus-benchmark/src/Plutus/Benchmark/LastPiece.hs

@@ -1,16 +1,16 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-{- Last piece puzzle, adapted from nofib/spectral/last-piece.
-   This is a solver for a jigsaw problem:
+{-% Last piece puzzle, adapted from nofib/spectral/last-piece.
+    This is a solver for a jigsaw problem:
         see https://www.nicklevine.org/contest/2003/index.html.
 
- I've removed prettyprinting code for solutions and replaced Map.Map with an
- association list.  The original version collected the entire search tree,
- including paths which led to failure, and the PLC version quickly ran out of
- memory. This version prunes the search tree to keep only successful paths.  It
- still doesn't work on the CEK machine (I don't know about the CK machine: that
- took forever).
--}
+  I've removed prettyprinting code for solutions and replaced Map.Map with an
+  association list.  The original version collected the entire search tree,
+  including paths which led to failure, and the PLC version quickly ran out of
+  memory. This version prunes the search tree to keep only successful paths.  It
+  still doesn't work on the CEK machine (I don't know about the CK machine: that
+  took forever).
+%-}
 
 module Plutus.Benchmark.LastPiece where
 
@@ -94,7 +94,7 @@ search square sex board ps
                  os <- oss]
 
 {-# INLINABLE prune #-}
--- An attempt to cut down on the size of the result (not in the original program)
+--% An attempt to cut down on the size of the result (not in the original program)
 prune :: [Solution] -> Solution
 prune ss =
     case filter nonFailure ss of
@@ -183,7 +183,7 @@ pickOne xs0 = go id xs0
 --      The initial setup
 
 {-# INLINABLE fromJust #-}
--- Library functions is not inlinable
+--% Library functions is not inlinable
 fromJust :: Maybe a -> a
 fromJust Nothing  = Tx.error ()
 fromJust (Just x) = x