{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
------------------------------------------------------------------------
-- |
-- Module : Hanoi
-- Copyright : (C) 2019, Adam Boniecki
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Adam Boniecki <adambonie@gmail.com>
-- Stability : provisional
-- Portability : non-portable (GHC extensions)
--
-- Solution to the famous Tower of Hanoi puzzle using tools for state
-- machine property-based testing.
--
-- The puzzle is to move N discs of different sizes from one peg to
-- another, with one auxiliary peg and a restriction that no disc may ever
-- be placed on top of a smaller disc. Only one disc can be moved at a time.
------------------------------------------------------------------------
module Hanoi
( prop_hanoi
) where
import Data.Array
import Data.Kind
(Type)
import Data.Maybe
import GHC.Generics
(Generic, Generic1)
import Prelude
import Test.QuickCheck
(Arbitrary(arbitrary), Gen, Property, choose,
suchThat, (===))
import Test.QuickCheck.Monadic
(monadicIO)
import Test.StateMachine
import Test.StateMachine.TreeDiff.Expr
()
import qualified Test.StateMachine.Types.Rank2 as Rank2
------------------------------------------------------------------------
-- The model keeps track of which disc is on which peg
newtype Model (r :: Type -> Type) = Model (Array Int [Int])
deriving stock (Show, Eq, Generic)
-- There are 3 pegs, so the bounds are (0, 2)
pegsBounds :: (Int,Int)
pegsBounds = (0, 2)
instance ToExpr (Model r) where
toExpr (Model a) = toExpr $ elems a
initModel :: Int -> Model r
initModel discs = Model $ listArray pegsBounds [[1..discs], [], []]
-- Allowed action is to move one disc from the top of one peg to the top of another
data Command (r :: Type -> Type) = Move (Int,Int)
deriving stock (Eq, Show, Generic1)
deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
instance Arbitrary (Command r) where
arbitrary = do
x <- choose pegsBounds
y <- choose pegsBounds `suchThat` (/= x)
return $ Move (x,y)
data Response (r :: Type -> Type) = Done
deriving stock (Show, Generic1)
deriving anyclass (Rank2.Foldable)
------------------------------------------------------------------------
transitions :: Model r -> Command r -> Response r -> Model r
transitions (Model pegs) (Move (from_, to_)) _ = case pegs ! from_ of
(x : xs) -> Model $ pegs // [(from_, xs), (to_, x : pegs ! to_)]
_ -> error "transition: impossible, due to preconditon"
preconditions :: Model Symbolic -> Command Symbolic -> Logic
preconditions (Model pegs) (Move (from_, to_)) = Boolean (isJust x) .&& x .<= y
where
x = listToMaybe (pegs ! from_)
-- Any disc can be placed on empty peg, so no disc counts as largest disc.
y = listToMaybe (pegs ! to_ ++ [maxBound])
-- Check if all discs are at the last peg. The invariant states that this is not
-- the case, so when it is not satisfied, we have a counter example that is a
-- solution to our puzzle.
postconditions :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postconditions m c r = length lst ./= sum (fmap length pegs)
where
lst = pegs ! (snd $ bounds pegs)
Model pegs = transitions m c r
------------------------------------------------------------------------
generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
generator _ = Just $ arbitrary
shrinker :: Model r -> Command r -> [Command r]
shrinker _ _ = []
------------------------------------------------------------------------
semantics :: Command Concrete -> IO (Response Concrete)
semantics _ = return Done
mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
mock _ _ = return Done
------------------------------------------------------------------------
sm :: Int -> StateMachine Model Command IO Response
sm discs = StateMachine (initModel discs) transitions preconditions postconditions
Nothing generator shrinker semantics mock noCleanup
-- A sequential property for Tower of Hanoi with n discs.
-- Note that optimal solution requires 2^n-1 moves and this is not guaranteeed
-- to find an optimal one (or any at all).
prop_hanoi :: Int -> Property
prop_hanoi n = forAllCommands (sm n) Nothing $ \cmds -> monadicIO $ do
(hist, _model, res) <- runCommands (sm n) cmds
prettyCommands (sm n) hist (checkCommandNames cmds (res === Ok))