/*
 * Copyright (c) 2013-2014 Galois, Inc.
 * Distributed under the terms of the BSD3 license (see LICENSE file)
 */

module FoxChickenCorn where

type OneBank = [4]
type BankState =
    {left : OneBank
    ,right: OneBank
    }

startState      = { left = farmer || chicken || corn || fox, right = 0x0}
doneState       = { left = 0x0, right = farmer || chicken || corn || fox}

farmer  = 0x1
chicken = 0x2
corn    = 0x4
fox     = 0x8

// To see this work, try:
// :sat solutionInNmoves : [6]BankState -> Bit

solutionInNmoves : {n} (fin n) => [n] BankState -> Bit
property solutionInNmoves states = validMoveSequence ([startState] # states # [doneState])

validMoveSequence : {n} (fin n, n >= 1) => [n] BankState -> Bit
validMoveSequence states = all [validMove a b
                               | a <- states
                               | b <- drop`{1} states]

// Two states represent a valid move if they are both valid states (no carnage)
// and that whatever moved followed the rules
validMove : BankState -> BankState -> Bit
validMove b b' = validState b && validState b'
                 && stuffOnlyMovedWithFarmer b b'

stuffOnlyMovedWithFarmer : BankState -> BankState -> Bit
stuffOnlyMovedWithFarmer b b' =
    if farmerHere b.left
    then farmerHere b'.right && moveFollowsRules b.left b'.right (b'.right - b.right)
    else farmerHere b'.left  && moveFollowsRules b.right b'.left (b'.left - b.left)

// things can't move without the farmer, and the farmer can carry at most one thing
moveFollowsRules fromBank toBank whatMoved = farmerMoved && atMostOneObjectMoved where
    farmerMoved = (whatMoved && farmer) == farmer
    atMostOneObjectMoved = popCount (whatMoved && ~farmer) <= 1

// "conservation of items" rule - nothing spontaneously disappears
completeState : BankState -> Bit
completeState b = (b.left ^ b.right) == 0xf

// both banks are "carnage-free"
validState : BankState -> Bit
validState bs = completeState bs && validBank bs.left 
                && validBank bs.right && completeState bs

validBank : OneBank -> Bit
validBank b = farmerHere b || (~(foxWithChicken b) && ~(chickenWithCorn b))

farmerHere : OneBank -> Bit
farmerHere b = (b && farmer) > 0

chickenWithCorn : OneBank -> Bit
chickenWithCorn b = (b && (corn || chicken)) == (corn || chicken)

foxWithChicken : OneBank -> Bit
foxWithChicken b = (b && (fox || chicken)) == (fox || chicken)

// utilities
all : {n} (fin n) => [n] -> Bit
all xs = xs == ~zero

// "population count" - how many bits are on
popCount : {a,b} (fin a, b >= 1, b == (lg2 a)) => [a] -> [b]
popCount bs = ic ! 0 where
    ic = [0] # [ if elt then prev + 1 else prev | elt <- bs | prev <- ic]

// pretty printing
type StringRep = [7][8]
type DirRep = [5][8]
farmerString  = "farmer "
chickenString = "chicken"
cornString    = "corn   "
foxString     = "fox    "
noString      = "       "

ppArray = [farmerString, chickenString, cornString, foxString]

ppBits : [4] -> [4]StringRep
ppBits s =  [ if b then ppArray!i else noString 
            | b <- s
            | i <- [0 .. ]:[_][4] ]

// takes a sequence of states and derives what moved, and in which direction for each transition
extractMoves : {a} [a+1]BankState -> [a](DirRep, [4]StringRep)
extractMoves bankStates = [ getMove b b' | b <- bankStates | b' <- drop`{1} bankStates ] where
    getMove start end = ( dirString, thingsString thingsMoved ) where 
        dirString = if farmerHere start.left then " --> " else " <-- "
        thingsMoved = if farmerHere start.left
                      then end.right - start.right
                      else end.left - start.left
        thingsString bits = ppBits bits

// fcc> :sat solutionInNmoves : [6]BankState -> Bit
// solutionInNmoves : [6]BankState -> Bit [{left = 12, right = 3},
//                                      {left = 13, right = 2}, {left = 4, right = 11},
//                                      {left = 7, right = 8}, {left = 2, right = 13},
//                                      {left = 3, right = 12}] = True

// pretty printing: extractMoves ([startState] # [{left = 12, right = 3},{left = 13, right = 2}, {left = 4, right = 11}, {left =     7, right = 8}, {left = 2, right = 13}, {left = 3, right = 12}] # [doneState])
// [(" --> ", ["       ", "       ", "chicken", "farmer "]), // the farmer takes the chicken right
//  (" <-- ", ["       ", "       ", "       ", "farmer "]), // farmer goes back alone
//  (" --> ", ["fox    ", "       ", "       ", "farmer "]), // farmer takes the fox across
//  (" <-- ", ["       ", "       ", "chicken", "farmer "]), // brings the chicken back
//  (" --> ", ["       ", "corn   ", "       ", "farmer "]), // takes the corn over
//  (" <-- ", ["       ", "       ", "       ", "farmer "]), // goes back alone
//  (" --> ", ["       ", "       ", "chicken", "farmer "])] // brings the chicken over, all done