Hanoi.hs

{-# 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
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))