packages feed

Hoed-0.5.0: examples/Queens__with_properties/Queens.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
module Queens where
-- The queens problem made famous by Wirth.
import Debug.Hoed
import Data.List
import Test.QuickCheck
import Data.Maybe
import Test.QuickCheck
import Test.QuickCheck.Property
import Test.QuickCheck.Gen
import Test.QuickCheck.Random
import Properties
import Types

test1 :: IO ()
test1 = do
  (HoedAnalysis _ ct) <- runO' defaultHoedOptions (print $ queens 5)
  -- TODO compare ct with a stored version to do regression testing
  return ()

doit :: IO ()
doit = testOwp properties (prop_queens_set queens) 8

queens :: Int -> [Board]
queens = observe "queens" (\n -> valid n n)

-- How can we place m queens on an n*n board?
valid :: Int -> Int -> [Board]
valid = observe "valid" valid'
valid' 0 _ = [B []]
valid' m n
 -- A correct definition:
 = filter safe (extend n (valid (m-1) n))
 -- A defective definition:
 --  = filter safe (extend n (valid (m-1) (n-1)))

extend :: Int -> [Board] -> [Board]
extend = observe "extend" (\n bs -> consEach [1..n] bs)

consEach :: [Int] -> [Board] -> [Board]
consEach = observe "consEach" consEach'
consEach' [] bs    = []
consEach' (a:x) bs = map (\(B b) -> B (a:b)) bs ++ consEach x bs

safe :: Board -> Bool
safe = observe "safe" safe'
safe' (B (a:b)) = no_threat a (B b) 1

no_threat :: Int -> Board -> Int -> Bool
no_threat = observe "no_threat" no_threat'
no_threat' a (B []) m = True
no_threat' a (B (b:y)) m
 -- A correct definition:
 -- = a /= b && a+m /= b && a-m /= b && no_threat a (B y) (m+1)
 -- A defective definition:
  = a+m /= b && a-m /= b && no_threat a (B y) (m+1)

--------------------------------------------------------------------------------
-- demonstrating the need for parallel equality

configurations :: Int -> [Configuration]
configurations n = zipWith (\i b -> Configuration i (B b)) [1..] 
                        (configurations' n [1..n])
configurations' :: Int -> [Int] -> [[Int]]
configurations' n xs 
  | n > 0  = [x:t | x <- xs, t <- configurations' (n-1) xs]
  | n <= 0 = [[]]

queensFilter :: [Configuration] -> [Configuration]
queensFilter = observe "queensFilter" queensFilter'
queensFilter' (Configuration i b:t)
  | safe b    = Configuration i b : t
  | otherwise = t

doit2 :: IO ()
doit2 = printOwp properties2 (b1,b2)
  where ((Configuration _ b1) : (Configuration _ b2) : _) = queensFilter cs
        cs = (Configuration 1 (B [1,1,1,1])) : (Configuration 2 (B [2,4,1,3])) : [(Configuration 3 (B [1,1,1,1]))]

--------------------------------------------------------------------------------

showBoard :: Board -> String 
showBoard = observe "showBoard" showBoard'
showBoard' (B b) =
  let rank r qcol =
        map line ["o o o", " \\|/ ", " === "]
        where
        line crown_slice =
          concat (zipWith square [1..] b)
          where
          square scol _ =
            if scol == qcol then crown_slice
            else if scol `rem` (2::Int) == r `rem` (2::Int) then "....."
            else "     "
  in unlines (concat (zipWith rank [1..] b))