content: module Properties where
  import Debug.Hoed
  import Data.List
  import Data.Maybe
  import Test.QuickCheck hiding ((===))
  import Test.QuickCheck.Property hiding ((===))
  import Test.QuickCheck.Gen
  import Test.QuickCheck.Random
  import Control.Monad
  import Types
  
  properties3 = [ Propositions 
                  [ mkProposition m1 "prop_queens_sound"
                      `ofType` BoolProposition
                      `withSignature` [SubjectFunction,Argument 0]
                      `sizeHint` 4
                  , mkProposition m1 "prop_queens_complete" 
                       `ofType` QuickCheckProposition
                       `withSignature` [SubjectFunction,Argument 0,Random]
                       `sizeHint` 4
                  ] Specify "queens" [m2a,m3]
               , Propositions 
                  [ mkProposition m1 "prop_valid_sound" 
                      `ofType` BoolProposition
                      `withSignature` [SubjectFunction,Argument 0,Argument 1]
                       `sizeHint` 4
                  , mkProposition m1 "prop_valid_complete" 
                      `ofType` QuickCheckProposition
                      `withSignature` [SubjectFunction,Argument 0,Argument 1,Random]
                       `sizeHint` 4
                  ] Specify "valid" [m2a,m3]
               , Propositions 
                  [ mkProposition m1 "prop_extend_sound"
                      `ofType` BoolProposition `withSignature` [SubjectFunction,Argument 0,Argument 1]
                  , mkProposition m1 "prop_extend_complete"
                      `ofType` BoolProposition `withSignature` [SubjectFunction,Argument 0,Argument 1]
                  ] Specify "extend" [m2a,m3]
               , Propositions 
                  [ mkProposition m1 "spec_safe"
                      `ofType` QuickCheckProposition `withSignature` [SubjectFunction,Argument 0]
                  ] Specify "safe" [m2a,m3]
               , Propositions 
                  [ mkProposition m1 "spec_no_threat"
                      `ofType` QuickCheckProposition `withSignature` [SubjectFunction,Argument 0,Argument 1,Argument 2]
                  ] Specify "no_threat" [m2a,m3]
               ]
    where
    m2a = Module "Queens3"     "../examples/Queens__with_properties/"
  
  properties2 = [ Propositions 
                  [ mkProposition m1 "spec_queensFilter"
                      `ofType` BoolProposition
                      `withSignature` [SubjectFunction,Argument 0]
                  , mkProposition m1 "spec_queensFilter_p"
                      `ofType` BoolProposition
                      `withSignature` [SubjectFunction,Argument 0]
                  ] Specify "queensFilter" [m2,m3]
                ]
  
  properties = [ Propositions 
                  [ mkProposition m1 "prop_queens_sound"
                      `ofType` BoolProposition
                      `withSignature` [SubjectFunction,Argument 0]
                      `sizeHint` 4
                  , mkProposition m1 "prop_queens_complete" 
                       `ofType` QuickCheckProposition
                       `withSignature` [SubjectFunction,Argument 0,Random]
                       `sizeHint` 4
                  ] Specify "queens" [m2,m3]
               , Propositions 
                  [ mkProposition m1 "prop_valid_sound" 
                      `ofType` BoolProposition
                      `withSignature` [SubjectFunction,Argument 0,Argument 1]
                       `sizeHint` 4
                  , mkProposition m1 "prop_valid_complete" 
                      `ofType` QuickCheckProposition
                      `withSignature` [SubjectFunction,Argument 0,Argument 1,Random]
                       `sizeHint` 4
                  ] Specify "valid" [m2,m3]
               , Propositions 
                  [ mkProposition m1 "prop_extend_sound"
                      `ofType` BoolProposition `withSignature` [SubjectFunction,Argument 0,Argument 1]
                  , mkProposition m1 "prop_extend_complete"
                      `ofType` BoolProposition `withSignature` [SubjectFunction,Argument 0,Argument 1]
                  ] Specify "extend" [m2,m3]
               , Propositions 
                  [ mkProposition m1 "spec_safe"
                      `ofType` QuickCheckProposition `withSignature` [SubjectFunction,Argument 0]
                  ] Specify "safe" [m2,m3]
               , Propositions 
                  [ mkProposition m1 "spec_no_threat"
                      `ofType` QuickCheckProposition `withSignature` [SubjectFunction,Argument 0,Argument 1,Argument 2]
                  ] Specify "no_threat" [m2,m3]
               ]
  
  m1 = Module "Properties" "../examples/Queens__with_properties/"
  m2 = Module "Queens"     "../examples/Queens__with_properties/"
  m3 = Module "Types"     "../examples/Queens__with_properties/"
  
  prop_queens_set q n = all (\(B b) -> isSet b) (q n)
  
  prop_safe_set s b = not (isSet b && s (B b))
  
  prop_queens_sound q n      = all (\b -> completeSolution n b && validSolution n n b) (q n)
  prop_queens_complete q n b = completeSolution n b && validSolution n n b ==> b `elem` (q n)
  
  prop_valid_sound :: (Int -> Int -> [Board]) -> Int -> Int -> Bool
  prop_valid_sound v m n = all (\b -> validSolution m n b) (v m n)
  
  prop_valid_complete v m n b = completeSolution m b && validSolution m n b ==> b `elem` (v m n)
  
  completeSolution :: Int -> Board -> Bool
  completeSolution m (B b) = length b == m && all (`elem` [1..m]) b
  
  norepeats (B b) = nub b == b
  
  validSolution' :: Board -> Bool
  validSolution' (B [])  = True
  validSolution' (B [x]) = True
  validSolution' (B b)   = validSolution (maximum b) (max (length b) (maximum b)) (B b)
  
  validSolution :: Int -> Int -> Board -> Bool
  validSolution 0 n (B b) = b == []
  validSolution m n (B b)
    -- = m >= n &&
    = onBoard n b && isSet b
    && isSet (diagonals n b) && isSet (diagonals n (reverse b))
  
  onBoard :: Int -> [Int] -> Bool
  onBoard n b = all (\i -> i > 0 && i <= n) b
  
  spec_safe :: (Board -> Bool) -> Board -> Property
  spec_safe s b = nonEmptyBoard b && validSolution' (btail b) ==> s b == validSolution' b
  
  nonEmptyBoard (B b) = b /= []
  
  spec_no_threat :: (Int -> Board -> Int -> Bool) -> Int -> Board -> Int -> Property
  spec_no_threat n a (B b) m = validSolution' (B b) ==> validSolution' (B (a:b)) == n a (B b) m
  
  -- In a set every element occurs exactly once
  isSet xs = all (\x -> length (filter (==x) xs) == 1) xs
  
  -- Give for each queen on the board (i.e. the list of column
  -- positions) in which diagonal this queen is placed.
  --
  --  3   2   1   0
  --  2   1   0  -1
  --  1   0  -1  -2
  --  0  -1  -2  -3
  --
  diagonals :: Int -> [Int] -> [Int]
  diagonals n b = zipWith (-) b [1..n]
  
  prop_extend_complete e n bs = length (e n bs) == n * (length bs)
  
  prop_extend_sound :: (Int -> [Board] -> [Board]) -> Int -> [Board] -> Bool
  prop_extend_sound e n bs 
    | all (completeSolution n) bs && all norepeats bs
        = all extend_sound_board (zip3 bs' is ds)
    | otherwise                   = True
    where ds = e n bs
          is = cycle [1..n]
          bs' = foldr (\b z -> replicate n b ++ z) [] bs
  
  extend_sound_board (B b, i, B [])    = False
  extend_sound_board (B b, i, B (j:e)) = i == j && b == e
  
  btail (B b) = B (tail b)
  bnull (B b)  = null b
  bcon a (B b) = B (a:b)
  ball f (B b) = all f b
  
  spec_queensFilter_p, spec_queensFilter :: ([Configuration] -> [Configuration]) -> [Configuration] -> Bool
  spec_queensFilter   q cs = q cs == filter validConfiguration cs
  spec_queensFilter_p q cs = q cs === filter validConfiguration cs
  
  validConfiguration (Configuration i b) = validSolution' b
  