    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Sudoku
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- The Sudoku solver, quintessential SMT solver example!
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Sudoku where

    import Data.List  (transpose)
    import Data.Maybe (fromJust)

    import Data.SBV

    -------------------------------------------------------------------
    -- * Modeling Sudoku
    -------------------------------------------------------------------
    -- | A row is a sequence of 8-bit words, too large indeed for representing 1-9, but does not harm
    type Row   = [SWord8]

    -- | A Sudoku board is a sequence of 9 rows
    type Board = [Row]

    -- | Given a series of elements, make sure they are all different
    -- and they all are numbers between 1 and 9
    check :: [SWord8] -> SBool
    check :: [SWord8] -> SBool
    check grp :: [SWord8]
    grp = [SBool] -> SBool
    sAnd ([SBool] -> SBool) -> [SBool] -> SBool
    forall a b. (a -> b) -> a -> b
    $ [SWord8] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct [SWord8]
    grp SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : (SWord8 -> SBool) -> [SWord8] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SWord8 -> SBool
    forall a. (OrdSymbolic a, Num a) => a -> SBool
    rangeFine [SWord8]
    grp
      where rangeFine :: a -> SBool
    rangeFine x :: a
    x = a
    x a -> a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> 0 SBool -> SBool -> SBool
    .&& a
    x a -> a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= 9

    -- | Given a full Sudoku board, check that it is valid
    valid :: Board -> SBool
    valid :: Board -> SBool
    valid rows :: Board
    rows = [SBool] -> SBool
    sAnd ([SBool] -> SBool) -> [SBool] -> SBool
    forall a b. (a -> b) -> a -> b
    $ Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal Bool
    sizesOK SBool -> [SBool] -> [SBool]
    forall a. a -> [a] -> [a]
    : ([SWord8] -> SBool) -> Board -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map [SWord8] -> SBool
    check (Board
    rows Board -> Board -> Board
    forall a. [a] -> [a] -> [a]
    ++ Board
    columns Board -> Board -> Board
    forall a. [a] -> [a] -> [a]
    ++ Board
    squares)
      where sizesOK :: Bool
    sizesOK = Board -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Board
    rows Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 9 Bool -> Bool -> Bool
    && ([SWord8] -> Bool) -> Board -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (\r :: [SWord8]
    r -> [SWord8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord8]
    r Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 9) Board
    rows
            columns :: Board
    columns = Board -> Board
    forall a. [[a]] -> [[a]]
    transpose Board
    rows
            regions :: [Board]
    regions = [Board] -> [Board]
    forall a. [[a]] -> [[a]]
    transpose [Int -> [SWord8] -> Board
    forall a. Int -> [a] -> [[a]]
    chunk 3 [SWord8]
    row | [SWord8]
    row <- Board
    rows]
            squares :: Board
    squares = [Board -> [SWord8]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat Board
    sq | Board
    sq <- Int -> Board -> [Board]
    forall a. Int -> [a] -> [[a]]
    chunk 3 ([Board] -> Board
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [Board]
    regions)]
            chunk :: Int -> [a] -> [[a]]
            chunk :: Int -> [a] -> [[a]]
    chunk _ [] = []
            chunk i :: Int
    i xs :: [a]
    xs = let (f :: [a]
    f, r :: [a]
    r) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i [a]
    xs in [a]
    f [a] -> [[a]] -> [[a]]
    forall a. a -> [a] -> [a]
    : Int -> [a] -> [[a]]
    forall a. Int -> [a] -> [[a]]
    chunk Int
    i [a]
    r

    -- | A puzzle is a pair: First is the number of missing elements, second
    -- is a function that given that many elements returns the final board.
    type Puzzle = (Int, [SWord8] -> Board)

    -------------------------------------------------------------------
    -- * Solving Sudoku puzzles
    -------------------------------------------------------------------

    -- | Solve a given puzzle and print the results
    sudoku :: Puzzle -> IO ()
    sudoku :: Puzzle -> IO ()
    sudoku p :: Puzzle
    p@(i :: Int
    i, f :: [SWord8] -> Board
    f) = do String -> IO ()
    putStrLn "Solving the puzzle.."
                         Either String (Bool, [Word8])
    model <- SatResult -> Either String (Bool, [Word8])
    forall a b.
    (Modelable a, SatModel b) =>
    a -> Either String (Bool, b)
    getModelAssignment (SatResult -> Either String (Bool, [Word8]))
    -> IO SatResult -> IO (Either String (Bool, [Word8]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` SymbolicT IO SBool -> IO SatResult
    forall a. Provable a => a -> IO SatResult
    sat ((Board -> SBool
    valid (Board -> SBool) -> ([SWord8] -> Board) -> [SWord8] -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SWord8] -> Board
    f) ([SWord8] -> SBool) -> SymbolicT IO [SWord8] -> SymbolicT IO SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Int -> SymbolicT IO [SWord8]
    forall a. SymVal a => Int -> Symbolic [SBV a]
    mkExistVars Int
    i)
                         case Either String (Bool, [Word8])
    model of
                           Right sln :: (Bool, [Word8])
    sln -> Puzzle -> (Bool, [Word8]) -> IO ()
    dispSolution Puzzle
    p (Bool, [Word8])
    sln
                           Left m :: String
    m    -> String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Unsolvable puzzle: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    m

    -- | Helper function to display results nicely, not really needed, but helps presentation
    dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()
    dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()
    dispSolution (i :: Int
    i, f :: [SWord8] -> Board
    f) (_, fs :: [Word8]
    fs)
      | Int
    lmod Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    i = String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Impossible! Backend solver returned " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    lmod String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " values, was expecting: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
      | Bool
    True      = do String -> IO ()
    putStrLn "Final board:"
                       ([SWord8] -> IO ()) -> Board -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [SWord8] -> IO ()
    forall (t :: * -> *) a.
    (Foldable t, Show a, SymVal a) =>
    t (SBV a) -> IO ()
    printRow Board
    final
                       String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Valid Check: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBool -> String
    forall a. Show a => a -> String
    show (Board -> SBool
    valid Board
    final)
                       String -> IO ()
    putStrLn "Done."
      where lmod :: Int
    lmod = [Word8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Word8]
    fs
            final :: Board
    final = [SWord8] -> Board
    f ((Word8 -> SWord8) -> [Word8] -> [SWord8]
    forall a b. (a -> b) -> [a] -> [b]
    map Word8 -> SWord8
    forall a. SymVal a => a -> SBV a
    literal [Word8]
    fs)
            printRow :: t (SBV a) -> IO ()
    printRow r :: t (SBV a)
    r = String -> IO ()
    putStr "   " IO () -> IO () -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (SBV a -> IO ()) -> t (SBV a) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\x :: SBV a
    x -> String -> IO ()
    putStr (a -> String
    forall a. Show a => a -> String
    show (Maybe a -> a
    forall a. HasCallStack => Maybe a -> a
    fromJust (SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    x)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " ")) t (SBV a)
    r IO () -> IO () -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> String -> IO ()
    putStrLn ""

    -- | Find all solutions to a puzzle
    solveAll :: Puzzle -> IO ()
    solveAll :: Puzzle -> IO ()
    solveAll p :: Puzzle
    p@(i :: Int
    i, f :: [SWord8] -> Board
    f) = do String -> IO ()
    putStrLn "Finding all solutions.."
                           AllSatResult
    res <- SymbolicT IO SBool -> IO AllSatResult
    forall a. Provable a => a -> IO AllSatResult
    allSat (SymbolicT IO SBool -> IO AllSatResult)
    -> SymbolicT IO SBool -> IO AllSatResult
    forall a b. (a -> b) -> a -> b
    $ (Board -> SBool
    valid (Board -> SBool) -> ([SWord8] -> Board) -> [SWord8] -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SWord8] -> Board
    f) ([SWord8] -> SBool) -> SymbolicT IO [SWord8] -> SymbolicT IO SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Int -> SymbolicT IO [SWord8]
    forall a. SymVal a => Int -> Symbolic [SBV a]
    mkExistVars Int
    i
                           Int
    cnt <- ([(Bool, [Word8])] -> [(Bool, [Word8])])
    -> (Int -> (Bool, [Word8]) -> IO ()) -> AllSatResult -> IO Int
    forall a.
    SatModel a =>
    ([(Bool, a)] -> [(Bool, a)])
    -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
    displayModels [(Bool, [Word8])] -> [(Bool, [Word8])]
    forall a. a -> a
    id Int -> (Bool, [Word8]) -> IO ()
    forall a. Show a => a -> (Bool, [Word8]) -> IO ()
    disp AllSatResult
    res
                           String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Found: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    cnt String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " solution(s)."
       where disp :: a -> (Bool, [Word8]) -> IO ()
    disp n :: a
    n s :: (Bool, [Word8])
    s = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Solution #" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    n
                           Puzzle -> (Bool, [Word8]) -> IO ()
    dispSolution Puzzle
    p (Bool, [Word8])
    s

    -------------------------------------------------------------------
    -- * Example boards
    -------------------------------------------------------------------

    -- | Find an arbitrary good board
    puzzle0 :: Puzzle
    puzzle0 :: Puzzle
    puzzle0 = (81, [SWord8] -> Board
    forall a. [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [ a1 :: a
    a1, a2 :: a
    a2, a3 :: a
    a3, a4 :: a
    a4, a5 :: a
    a5, a6 :: a
    a6, a7 :: a
    a7, a8 :: a
    a8, a9 :: a
    a9,
                  b1 :: a
    b1, b2 :: a
    b2, b3 :: a
    b3, b4 :: a
    b4, b5 :: a
    b5, b6 :: a
    b6, b7 :: a
    b7, b8 :: a
    b8, b9 :: a
    b9,
                  c1 :: a
    c1, c2 :: a
    c2, c3 :: a
    c3, c4 :: a
    c4, c5 :: a
    c5, c6 :: a
    c6, c7 :: a
    c7, c8 :: a
    c8, c9 :: a
    c9,
                  d1 :: a
    d1, d2 :: a
    d2, d3 :: a
    d3, d4 :: a
    d4, d5 :: a
    d5, d6 :: a
    d6, d7 :: a
    d7, d8 :: a
    d8, d9 :: a
    d9,
                  e1 :: a
    e1, e2 :: a
    e2, e3 :: a
    e3, e4 :: a
    e4, e5 :: a
    e5, e6 :: a
    e6, e7 :: a
    e7, e8 :: a
    e8, e9 :: a
    e9,
                  f1 :: a
    f1, f2 :: a
    f2, f3 :: a
    f3, f4 :: a
    f4, f5 :: a
    f5, f6 :: a
    f6, f7 :: a
    f7, f8 :: a
    f8, f9 :: a
    f9,
                  g1 :: a
    g1, g2 :: a
    g2, g3 :: a
    g3, g4 :: a
    g4, g5 :: a
    g5, g6 :: a
    g6, g7 :: a
    g7, g8 :: a
    g8, g9 :: a
    g9,
                  h1 :: a
    h1, h2 :: a
    h2, h3 :: a
    h3, h4 :: a
    h4, h5 :: a
    h5, h6 :: a
    h6, h7 :: a
    h7, h8 :: a
    h8, h9 :: a
    h9,
                  i1 :: a
    i1, i2 :: a
    i2, i3 :: a
    i3, i4 :: a
    i4, i5 :: a
    i5, i6 :: a
    i6, i7 :: a
    i7, i8 :: a
    i8, i9 :: a
    i9 ]
             = [ [a
    a1, a
    a2, a
    a3, a
    a4, a
    a5, a
    a6, a
    a7, a
    a8, a
    a9],
                 [a
    b1, a
    b2, a
    b3, a
    b4, a
    b5, a
    b6, a
    b7, a
    b8, a
    b9],
                 [a
    c1, a
    c2, a
    c3, a
    c4, a
    c5, a
    c6, a
    c7, a
    c8, a
    c9],
                 [a
    d1, a
    d2, a
    d3, a
    d4, a
    d5, a
    d6, a
    d7, a
    d8, a
    d9],
                 [a
    e1, a
    e2, a
    e3, a
    e4, a
    e5, a
    e6, a
    e7, a
    e8, a
    e9],
                 [a
    f1, a
    f2, a
    f3, a
    f4, a
    f5, a
    f6, a
    f7, a
    f8, a
    f9],
                 [a
    g1, a
    g2, a
    g3, a
    g4, a
    g5, a
    g6, a
    g7, a
    g8, a
    g9],
                 [a
    h1, a
    h2, a
    h3, a
    h4, a
    h5, a
    h6, a
    h7, a
    h8, a
    h9],
                 [a
    i1, a
    i2, a
    i3, a
    i4, a
    i5, a
    i6, a
    i7, a
    i8, a
    i9] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle0 needs exactly 81 elements!"

    -- | A random puzzle, found on the internet..
    puzzle1 :: Puzzle
    puzzle1 :: Puzzle
    puzzle1 = (49, [SWord8] -> Board
    forall a. Num a => [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [ a1 :: a
    a1,     a3 :: a
    a3, a4 :: a
    a4, a5 :: a
    a5, a6 :: a
    a6, a7 :: a
    a7,     a9 :: a
    a9,
                  b1 :: a
    b1, b2 :: a
    b2, b3 :: a
    b3,             b7 :: a
    b7, b8 :: a
    b8, b9 :: a
    b9,
                      c2 :: a
    c2,     c4 :: a
    c4, c5 :: a
    c5, c6 :: a
    c6,     c8 :: a
    c8,
                          d3 :: a
    d3,     d5 :: a
    d5,     d7 :: a
    d7,
                  e1 :: a
    e1, e2 :: a
    e2,     e4 :: a
    e4, e5 :: a
    e5, e6 :: a
    e6,     e8 :: a
    e8, e9 :: a
    e9,
                          f3 :: a
    f3,     f5 :: a
    f5,     f7 :: a
    f7,
                      g2 :: a
    g2,     g4 :: a
    g4, g5 :: a
    g5, g6 :: a
    g6,     g8 :: a
    g8,
                  h1 :: a
    h1, h2 :: a
    h2, h3 :: a
    h3,             h7 :: a
    h7, h8 :: a
    h8, h9 :: a
    h9,
                  i1 :: a
    i1,     i3 :: a
    i3, i4 :: a
    i4, i5 :: a
    i5, i6 :: a
    i6, i7 :: a
    i7,     i9 :: a
    i9 ]
             = [ [a
    a1,  6, a
    a3, a
    a4, a
    a5, a
    a6, a
    a7,  1, a
    a9],
                 [a
    b1, a
    b2, a
    b3,  6,  5,  1, a
    b7, a
    b8, a
    b9],
                 [ 1, a
    c2,  7, a
    c4, a
    c5, a
    c6,  6, a
    c8,  2],
                 [ 6,  2, a
    d3,  3, a
    d5,  5, a
    d7,  9,  4],
                 [a
    e1, a
    e2,  3, a
    e4, a
    e5, a
    e6,  2, a
    e8, a
    e9],
                 [ 4,  8, a
    f3,  9, a
    f5,  7, a
    f7,  3,  6],
                 [ 9, a
    g2,  6, a
    g4, a
    g5, a
    g6,  4, a
    g8,  8],
                 [a
    h1, a
    h2, a
    h3,  7,  9,  4, a
    h7, a
    h8, a
    h9],
                 [a
    i1,  5, a
    i3, a
    i4, a
    i5, a
    i6, a
    i7,  7, a
    i9] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle1 needs exactly 49 elements!"

    -- | Another random puzzle, found on the internet..
    puzzle2 :: Puzzle
    puzzle2 :: Puzzle
    puzzle2 = (55, [SWord8] -> Board
    forall a. Num a => [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [     a2 :: a
    a2,     a4 :: a
    a4, a5 :: a
    a5, a6 :: a
    a6, a7 :: a
    a7,     a9 :: a
    a9,
                  b1 :: a
    b1, b2 :: a
    b2,     b4 :: a
    b4,         b7 :: a
    b7, b8 :: a
    b8, b9 :: a
    b9,
                  c1 :: a
    c1,     c3 :: a
    c3, c4 :: a
    c4, c5 :: a
    c5, c6 :: a
    c6, c7 :: a
    c7, c8 :: a
    c8, c9 :: a
    c9,
                      d2 :: a
    d2, d3 :: a
    d3, d4 :: a
    d4,             d8 :: a
    d8, d9 :: a
    d9,
                  e1 :: a
    e1,     e3 :: a
    e3,     e5 :: a
    e5,     e7 :: a
    e7,     e9 :: a
    e9,
                  f1 :: a
    f1, f2 :: a
    f2,             f6 :: a
    f6, f7 :: a
    f7, f8 :: a
    f8,
                  g1 :: a
    g1, g2 :: a
    g2, g3 :: a
    g3, g4 :: a
    g4, g5 :: a
    g5, g6 :: a
    g6, g7 :: a
    g7,     g9 :: a
    g9,
                  h1 :: a
    h1, h2 :: a
    h2, h3 :: a
    h3,         h6 :: a
    h6,     h8 :: a
    h8, h9 :: a
    h9,
                  i1 :: a
    i1,     i3 :: a
    i3, i4 :: a
    i4, i5 :: a
    i5, i6 :: a
    i6,     i8 :: a
    i8     ]
             = [ [ 1, a
    a2,  3, a
    a4, a
    a5, a
    a6, a
    a7,  8, a
    a9],
                 [a
    b1, a
    b2,  6, a
    b4,  4,  8, a
    b7, a
    b8, a
    b9],
                 [a
    c1,  4, a
    c3, a
    c4, a
    c5, a
    c6, a
    c7, a
    c8, a
    c9],
                 [ 2, a
    d2, a
    d3, a
    d4,  9,  6,  1, a
    d8, a
    d9],
                 [a
    e1,  9, a
    e3,  8, a
    e5,  1, a
    e7,  4, a
    e9],
                 [a
    f1, a
    f2,  4,  3,  2, a
    f6, a
    f7, a
    f8,  8],
                 [a
    g1, a
    g2, a
    g3, a
    g4, a
    g5, a
    g6, a
    g7,  7, a
    g9],
                 [a
    h1, a
    h2, a
    h3,  1,  5, a
    h6,  4, a
    h8, a
    h9],
                 [a
    i1,  6, a
    i3, a
    i4, a
    i5, a
    i6,  2, a
    i8,  3] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle2 needs exactly 55 elements!"

    -- | Another random puzzle, found on the internet..
    puzzle3 :: Puzzle
    puzzle3 :: Puzzle
    puzzle3 = (56, [SWord8] -> Board
    forall a. Num a => [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [     a2 :: a
    a2, a3 :: a
    a3, a4 :: a
    a4,     a6 :: a
    a6,     a8 :: a
    a8, a9 :: a
    a9,
                      b2 :: a
    b2,     b4 :: a
    b4, b5 :: a
    b5, b6 :: a
    b6, b7 :: a
    b7, b8 :: a
    b8, b9 :: a
    b9,
                  c1 :: a
    c1, c2 :: a
    c2, c3 :: a
    c3, c4 :: a
    c4,     c6 :: a
    c6, c7 :: a
    c7,     c9 :: a
    c9,
                  d1 :: a
    d1,     d3 :: a
    d3,     d5 :: a
    d5,     d7 :: a
    d7,     d9 :: a
    d9,
                      e2 :: a
    e2, e3 :: a
    e3, e4 :: a
    e4,     e6 :: a
    e6, e7 :: a
    e7, e8 :: a
    e8,
                  f1 :: a
    f1,     f3 :: a
    f3,     f5 :: a
    f5,     f7 :: a
    f7,     f9 :: a
    f9,
                  g1 :: a
    g1,     g3 :: a
    g3, g4 :: a
    g4,     g6 :: a
    g6, g7 :: a
    g7, g8 :: a
    g8, g9 :: a
    g9,
                  h1 :: a
    h1, h2 :: a
    h2, h3 :: a
    h3, h4 :: a
    h4, h5 :: a
    h5, h6 :: a
    h6,     h8 :: a
    h8,
                  i1 :: a
    i1, i2 :: a
    i2,     i4 :: a
    i4,     i6 :: a
    i6, i7 :: a
    i7, i8 :: a
    i8     ]
             = [ [ 6, a
    a2, a
    a3, a
    a4,  1, a
    a6,  5, a
    a8, a
    a9],
                 [ 8, a
    b2,  3, a
    b4, a
    b5, a
    b6, a
    b7, a
    b8, a
    b9],
                 [a
    c1, a
    c2, a
    c3, a
    c4,  6, a
    c6, a
    c7,  2, a
    c9],
                 [a
    d1,  3, a
    d3,  1, a
    d5,  8, a
    d7,  9, a
    d9],
                 [ 1, a
    e2, a
    e3, a
    e4,  9, a
    e6, a
    e7, a
    e8,  4],
                 [a
    f1,  5, a
    f3,  2, a
    f5,  3, a
    f7,  1, a
    f9],
                 [a
    g1,  7, a
    g3, a
    g4,  3, a
    g6, a
    g7, a
    g8, a
    g9],
                 [a
    h1, a
    h2, a
    h3, a
    h4, a
    h5, a
    h6,  3, a
    h8,  6],
                 [a
    i1, a
    i2,  4, a
    i4,  5, a
    i6, a
    i7, a
    i8,  9] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle3 needs exactly 56 elements!"

    -- | According to the web, this is the toughest
    -- sudoku puzzle ever.. It even has a name: Al Escargot:
    -- <http://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html>
    puzzle4 :: Puzzle
    puzzle4 :: Puzzle
    puzzle4 = (58, [SWord8] -> Board
    forall a. Num a => [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [     a2 :: a
    a2, a3 :: a
    a3, a4 :: a
    a4, a5 :: a
    a5,     a7 :: a
    a7,     a9 :: a
    a9,
                  b1 :: a
    b1,     b3 :: a
    b3, b4 :: a
    b4,     b6 :: a
    b6, b7 :: a
    b7, b8 :: a
    b8,
                  c1 :: a
    c1, c2 :: a
    c2,         c5 :: a
    c5, c6 :: a
    c6,     c8 :: a
    c8, c9 :: a
    c9,
                  d1 :: a
    d1, d2 :: a
    d2,         d5 :: a
    d5, d6 :: a
    d6,     d8 :: a
    d8, d9 :: a
    d9,
                  e1 :: a
    e1,     e3 :: a
    e3, e4 :: a
    e4,     e6 :: a
    e6, e7 :: a
    e7, e8 :: a
    e8,
                      f2 :: a
    f2, f3 :: a
    f3, f4 :: a
    f4, f5 :: a
    f5,     f7 :: a
    f7, f8 :: a
    f8, f9 :: a
    f9,
                      g2 :: a
    g2, g3 :: a
    g3, g4 :: a
    g4, g5 :: a
    g5, g6 :: a
    g6, g7 :: a
    g7,     g9 :: a
    g9,
                  h1 :: a
    h1,     h3 :: a
    h3, h4 :: a
    h4, h5 :: a
    h5, h6 :: a
    h6, h7 :: a
    h7, h8 :: a
    h8,
                  i1 :: a
    i1, i2 :: a
    i2,     i4 :: a
    i4, i5 :: a
    i5, i6 :: a
    i6,     i8 :: a
    i8, i9 :: a
    i9 ]
             = [ [ 1, a
    a2, a
    a3, a
    a4, a
    a5,  7, a
    a7,  9, a
    a9],
                 [a
    b1,  3, a
    b3, a
    b4,  2, a
    b6, a
    b7, a
    b8,  8],
                 [a
    c1, a
    c2,  9,  6, a
    c5, a
    c6,  5, a
    c8, a
    c9],
                 [a
    d1, a
    d2,  5,  3, a
    d5, a
    d6,  9, a
    d8, a
    d9],
                 [a
    e1,  1, a
    e3, a
    e4,  8, a
    e6, a
    e7, a
    e8,  2],
                 [ 6, a
    f2, a
    f3, a
    f4, a
    f5,  4, a
    f7, a
    f8, a
    f9],
                 [ 3, a
    g2, a
    g3, a
    g4, a
    g5, a
    g6, a
    g7,  1, a
    g9],
                 [a
    h1,  4, a
    h3, a
    h4, a
    h5, a
    h6, a
    h7, a
    h8,  7],
                 [a
    i1, a
    i2,  7, a
    i4, a
    i5, a
    i6,  3, a
    i8, a
    i9] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle4 needs exactly 58 elements!"

    -- | This one has been called diabolical, apparently
    puzzle5 :: Puzzle
    puzzle5 :: Puzzle
    puzzle5 = (53, [SWord8] -> Board
    forall a. Num a => [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [ a1 :: a
    a1,     a3 :: a
    a3,     a5 :: a
    a5, a6 :: a
    a6,         a9 :: a
    a9,
                  b1 :: a
    b1,         b4 :: a
    b4, b5 :: a
    b5,     b7 :: a
    b7,     b9 :: a
    b9,
                      c2 :: a
    c2,     c4 :: a
    c4, c5 :: a
    c5, c6 :: a
    c6, c7 :: a
    c7, c8 :: a
    c8, c9 :: a
    c9,
                  d1 :: a
    d1, d2 :: a
    d2,     d4 :: a
    d4,     d6 :: a
    d6, d7 :: a
    d7, d8 :: a
    d8,
                  e1 :: a
    e1, e2 :: a
    e2, e3 :: a
    e3,     e5 :: a
    e5,     e7 :: a
    e7, e8 :: a
    e8, e9 :: a
    e9,
                      f2 :: a
    f2, f3 :: a
    f3, f4 :: a
    f4,     f6 :: a
    f6,     f8 :: a
    f8, f9 :: a
    f9,
                  g1 :: a
    g1, g2 :: a
    g2, g3 :: a
    g3, g4 :: a
    g4, g5 :: a
    g5, g6 :: a
    g6,     g8 :: a
    g8,
                  h1 :: a
    h1,     h3 :: a
    h3,     h5 :: a
    h5, h6 :: a
    h6,         h9 :: a
    h9,
                  i1 :: a
    i1,         i4 :: a
    i4, i5 :: a
    i5,     i7 :: a
    i7,     i9 :: a
    i9 ]
             = [ [a
    a1,  9, a
    a3,  7, a
    a5, a
    a6,  8,  6, a
    a9],
                 [a
    b1,  3,  1, a
    b4, a
    b5,  5, a
    b7,  2, a
    b9],
                 [ 8, a
    c2,  6, a
    c4, a
    c5, a
    c6, a
    c7, a
    c8, a
    c9],
                 [a
    d1, a
    d2,  7, a
    d4,  5, a
    d6, a
    d7, a
    d8,  6],
                 [a
    e1, a
    e2, a
    e3,  3, a
    e5,  7, a
    e7, a
    e8, a
    e9],
                 [ 5, a
    f2, a
    f3, a
    f4,  1, a
    f6,  7, a
    f8, a
    f9],
                 [a
    g1, a
    g2, a
    g3, a
    g4, a
    g5, a
    g6,  1, a
    g8,  9],
                 [a
    h1,  2, a
    h3,  6, a
    h5, a
    h6,  3,  5, a
    h9],
                 [a
    i1,  5,  4, a
    i4, a
    i5,  8, a
    i7,  7, a
    i9] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle5 needs exactly 53 elements!"

    -- | The following is nefarious according to
    -- <http://haskell.org/haskellwiki/Sudoku>
    puzzle6 :: Puzzle
    puzzle6 :: Puzzle
    puzzle6 = (64, [SWord8] -> Board
    forall a. Num a => [a] -> [[a]]
    f)
      where f :: [a] -> [[a]]
    f   [ a1 :: a
    a1, a2 :: a
    a2, a3 :: a
    a3, a4 :: a
    a4,     a6 :: a
    a6, a7 :: a
    a7,     a9 :: a
    a9,
                  b1 :: a
    b1,     b3 :: a
    b3, b4 :: a
    b4, b5 :: a
    b5, b6 :: a
    b6, b7 :: a
    b7, b8 :: a
    b8, b9 :: a
    b9,
                  c1 :: a
    c1, c2 :: a
    c2,     c4 :: a
    c4, c5 :: a
    c5, c6 :: a
    c6, c7 :: a
    c7, c8 :: a
    c8, c9 :: a
    c9,
                  d1 :: a
    d1,     d3 :: a
    d3, d4 :: a
    d4, d5 :: a
    d5, d6 :: a
    d6,     d8 :: a
    d8,
                      e2 :: a
    e2, e3 :: a
    e3, e4 :: a
    e4,     e6 :: a
    e6, e7 :: a
    e7, e8 :: a
    e8, e9 :: a
    e9,
                  f1 :: a
    f1, f2 :: a
    f2, f3 :: a
    f3, f4 :: a
    f4, f5 :: a
    f5, f6 :: a
    f6,     f8 :: a
    f8, f9 :: a
    f9,
                  g1 :: a
    g1, g2 :: a
    g2,         g5 :: a
    g5,     g7 :: a
    g7, g8 :: a
    g8, g9 :: a
    g9,
                      h2 :: a
    h2, h3 :: a
    h3,     h5 :: a
    h5, h6 :: a
    h6,     h8 :: a
    h8, h9 :: a
    h9,
                  i1 :: a
    i1, i2 :: a
    i2, i3 :: a
    i3, i4 :: a
    i4, i5 :: a
    i5, i6 :: a
    i6, i7 :: a
    i7,     i9 :: a
    i9  ]
             = [ [a
    a1, a
    a2, a
    a3, a
    a4,  6, a
    a6, a
    a7,  8, a
    a9],
                 [a
    b1,  2, a
    b3, a
    b4, a
    b5, a
    b6, a
    b7, a
    b8, a
    b9],
                 [a
    c1, a
    c2,  1, a
    c4, a
    c5, a
    c6, a
    c7, a
    c8, a
    c9],
                 [a
    d1,  7, a
    d3, a
    d4, a
    d5, a
    d6,  1, a
    d8,  2],
                 [ 5, a
    e2, a
    e3, a
    e4,  3, a
    e6, a
    e7, a
    e8, a
    e9],
                 [a
    f1, a
    f2, a
    f3, a
    f4, a
    f5, a
    f6,  4, a
    f8, a
    f9],
                 [a
    g1, a
    g2,  4,  2, a
    g5,  1, a
    g7, a
    g8, a
    g9],
                 [ 3, a
    h2, a
    h3,  7, a
    h5, a
    h6,  6, a
    h8, a
    h9],
                 [a
    i1, a
    i2, a
    i3, a
    i4, a
    i5, a
    i6, a
    i7,  5, a
    i9] ]
            f _ = String -> [[a]]
    forall a. HasCallStack => String -> a
    error "puzzle6 needs exactly 64 elements!"

    -- | Solve them all, this takes a fraction of a second to run for each case
    allPuzzles :: IO ()
    allPuzzles :: IO ()
    allPuzzles = (Puzzle -> IO ()) -> [Puzzle] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Puzzle -> IO ()
    sudoku [Puzzle
    puzzle0, Puzzle
    puzzle1, Puzzle
    puzzle2, Puzzle
    puzzle3, Puzzle
    puzzle4, Puzzle
    puzzle5, Puzzle
    puzzle6]