--[[ Carrie's Candy Bowl Module: Hashed Version
     CSci 658: Software Language Engineering, Fall 2013
     Exam 1, Problem 4
     H. Conrad Cunningham, Professor
     Computer and Information Science
     University of Mississippi

1234567890123456789012345678901234567890123456789012345678901234567890

2013-11-17: Experimental version before exam
2013-11-25: Modified, documented, and separated into module & driver
2013-12-03: Added ADT interface and implementation invariants, 
            preconditions, and postconditions.
            Corrections from what was distributed in class that day.
2013-12-08: Improved documentation


PROBLEM 4 DESCRIPTION FROM EXAM 1

Carrie's Candy Bowl. As you may have noticed, Carrie, the Department's
Administrative Secretary, has a candy bowl on her desk.  Often this
bowl gets filled with candy, which is quickly consumed by students and
professors.  Your task in this exercise is to represent that candy
bowl by a Lua module.

Design and implement Carrie's Candy Bowl as either a module or a
class.  Your module/class likely will need functions/methods similar
to the following:

CandyBowl() to create a new empty candy bowl

put(bowl,candyType) to add one piece of candy of type candyType to the
  bowl

take(bowl,candyType) to remove one piece of candy of type candyType
  from the bowl

has(bowl,candyType) to determine whether or not the bowl contains any
  candy of type candyType

howMany(bowl) to determine how many pieces of candy are in the bowl
  overall and howMany(bowl,candyType) to determine how many pieces of
  candy of type candyType are in the bowl

isEmpty(bowl) to determine whether or not the bowl is empty

inventory(bowl) to return a list-style table of pairs {candyType,
  count}.  The list should be in ascending order by candyType.  For
  example, if candyType is denoted by a string and there are two
  Snickers and one Hershey Kiss in the bowl, then the list returned
  would be something like { {'Hershey Kiss', 1}, {'Snickers', 2} }

combine(bowl1,bowl2) returns the bowl resulting from pouring bowl1 and
  bowl2 together to form a "larger" bowl

Note: The Lua functions in this module implement the above
functionality, plus some additional capability.


INVARIANTS FOR CandyBowl INSTANCES

The module defines the semantics of the CandyBowl abstract data type
(ADT) using (a) invariant assertions to characterize valid states of
its instances (between ADT function calls), (b) precondition and
postcondition assertions to characterize function behavior. The
invariants are implicitly conjuncted to the preconditions and
postconditions of the functions.

An ADT invariant must be true for any bowl ADT instance in the
argument list at the time of the call or any bowl instance returned at
the time of the return.  

An ADT interface invariant specifies the required value (i.e., state)
of the ADT instance in terms of an abstract model of the ADT and more
primitive functions in the public interface.  Here I use the "howMany"
function to formalize the invariant.

An ADT Interface Invariant for CandyBowl "bowl" can be stated as

      (ForAll c: validCandyType(c) :: howMany(bowl,c) >= 0)
  and (Sum c,n: n == howMany(bowl,c) :: n) == howMany(bowl)

where validCandyType(c) has an appropriate definition.

An ADT Implementation Invariant complements the interface invariant by
defining the abstract features in terms of concrete variables and data
structures.

This module represents the CandyBowl ADT with a hash table that maps
candyTypes to the count of the pieces of that type.  In addition,
special key SIZE maps to the count of the total number of pieces in
the table.

An ADT Implementation Invariant for CandyBowl "bowl" can be stated
 
  (ForAll c: validCandyType(c) :: 
      if bowl[c] ~= nil then bowl[c] == howMany(bowl,c))
      else howMany(bowl,c) = 0)  and
  bowl[SIZE] == howMany(bowl) 

where validCandyType(c) == (c ~= nil and c ~= SIZE), for all c.

I also define the semantics of the ADT functions using precondition
and postcondition assertions.  A precondition must hold at the time of
the call and may reference the arguments.  A postcondition must hold
at the time of the return and may reference both arguments and the
return values.  I prefix an argument instance with "arg_" and a
returned instance with "return_".

As currently implemented, all the required functions except "isEmpty"
are dependent upon the concrete implementation of the data.  Extended
functions "putcp", "takecp", "toBowl", and "combine2" are not.

For some function, the problem description does not specify whether a
function can modify its input arguments.


BETTER APPROACH TO SEMANTICS

As we see below, the ADT function "howMany" is sufficient for
specifying a constructive semantics for all functions except
itself. To formalize the ADT fully, a better approach would be to use
the mathematical concept of bag (or multiset) to model a candy bowl
instance's state.

The model used in the instructor's CookieJar ADT case study
illustrates the technique for a similar problem. See item 3(c) on the
following page from the Spring 2012 Multiparadigm Programming course:

  http://www.cs.olemiss.edu/~hcc/csci556/notes/556lectureNotes.html

The CookieJar case study uses a Scala trait to define the ADT
interface and an interface invariant, preconditions, and
postconditions to specify the ADT operations. It gives five different
implementation classes that mix-in the trait, each with its own
implementation invariant. Each implementation class uses a different
data representation for the CookieJar's bag.

A minimal way to hook a bag model into our invariants might be to AND
the following conjunct into the Interface Invariant:

  (ForAll c : validCandyType(c) :: 
      howMany(bowl,c) == OCCURRENCES(c,CandyBowlBag))

This new conjunct specifies the relationship between the Lua data
structure "bowl" and the mathematical bag "CandyBowlBag" used to model
the candy bowl instance.

In this assertion, function OCCURRENCES(c,B) denotes the number of
copies of element "c" occurring in bag "B".  (See the comment on the
CookieJar trait in the case study from the Multiparadigm Programming
class for a more detailed explanation of the bag concept.)

Perhaps the various preconditions and postconditions should be
restated in terms of CandyBowlBag properties instead of "howMany", but
that did not seem to be necessary.

--]]


-- Index in bowl table to hold count of elements
local SIZE = -1


-- Function CandyBowl(bowl) returns a new empty candy bowl if the
-- argument "bowl" is nil or unspecified; otherwise, it returns a
-- shallow copy of the argument "bowl".  The argument "bowl" is not
-- modified. The functionality of returning a copy of an existing bowl
-- is not required by the specification.

-- Pre:  arg_bowl == nil or arg_bowl satisfies ADT invariants
-- Post: if arg_bowl == nil then howMany(return_bowl) == 0
--       else (ForAll c: validCandyType(c) ::
--              howMany(return_bowl,c) == howMany(arg_bowl,c)) 

-- Reminder: The interface and implementation invariants are
-- implicitly ANDed into both the precondition and the postcondition
-- of each function for each instance of CandyBowl.

local function CandyBowl(bowl)
  local newbowl = {}
  if not bowl then
    newbowl[SIZE] = 0
  else -- do a shallow copy of argument
    for k,v in pairs(bowl) do
      newbowl[k] = v
    end
  end
  return newbowl
end


-- Function has(bowl,candyType) returns true if and only if "bowl"
-- contains one or more pieces of type "candyType" candy.  The
-- argument "bowl" is not modified.

-- Pre:  validCandyType(candyType)
-- Post: return == (howMany(arg_bowl,candyType) > 0

local function has(bowl, candyType)
  if not candyType or candyType == SIZE then
    error("Invalid candy type in 'has' " .. tostring(candyType))
  end
  local c = bowl[candyType]
  return c ~= nil and c > 0  -- c > 0 not needed
end


-- Function put(bowl,candyType,n) adds "n" pieces of "candyType" candy
-- to the argument "bowl".  "n" defaults to 1 if nil or unspecified.
-- "put" modifies its argument "bowl", but function "putcp" returns a
-- modified shallow copy of the argument instead.  Note: The
-- description does not specify whether the function can mutate its
-- table argument; these two functions implement both possibilities.

-- Pre:  validCandyType(candyType) and (n == nil or n > 0)
-- Post: ( if n == nil then 
--           howMany(return_bowl,candyType) 
--             == howMany(arg_bowl,candyType) + 1
--          else 
--           howMany(return_bowl,candyType) 
--             == howMany(arg_bowl,candyType) + n )  and 
--        (ForAll c: validCandyType(c) and c ~= candyType :: 
--            return_bowl[c] == arg_bowl[c]) and
--        return_bowl == arg_bowl
--
-- By return_bowl == arg_bowl, I mean they are the same table, not
-- that their attributes are identical.
          
local function put(bowl, candyType, n)
  if not candyType or candyType == SIZE then
    error("Invalid candy type in 'put' " .. tostring(candyType))
  end
  if not n then n = 1 end
  assert(n > 0,"Attempt to add zero or negative pieces to bowl.")
  if has(bowl,candyType) then
    bowl[candyType] = bowl[candyType] + n
  else
    bowl[candyType] = n
  end
  bowl[SIZE] = bowl[SIZE] + n
  return bowl
end

-- "putcp" has same precondition and postcondition except the
-- postcondition has return_bowl ~= arg_bowl instead of 
-- return_bowl == arg_bowl.  That is, they are different tables.

local function putcp(bowl, candyType, n)
  return put(CandyBowl(bowl), candyType, n)
end


-- Function take(bowl,candyType) removes one piece of "candyType"
-- candy from the argument "bowl". "take" modifies its argument
-- "bowl".  Function "takecp" returns a modified copy of the argument
-- "bowl" instead.  The specification does not specify whether the
-- function can mutate its table argument; these two functions
-- implement both possibilities.

-- Pre:  validCandyType(candyType) and howMany(arg_bowl,candyType) > 0
-- Post: ( howMany(return_bowl,candyType)
--         == howMany(arg_bowl,candyType) - 1 ) and
--        (ForAll c: validCandyType(c) and c ~= candyType :: 
--            return_bowl[c] == arg_bowl[c]) and
--        return_bowl == arg_bowl
--
-- By return_bowl == arg_bowl, I mean they are the same table, not
-- that their attributes are identical.
          

local function take(bowl, candyType) 
  if not candyType or candyType == SIZE then
    error("Invalid candy type in 'take' " .. tostring(candyType))
  end
  if has(bowl,candyType) then 
    bowl[candyType] = bowl[candyType] - 1
    if bowl[candyType] == 0 then bowl[candyType] = nil end 
    bowl[SIZE] = bowl[SIZE] - 1
    return bowl 
  else 
    error("Bowl does not contain type " .. tostring(candyType))
  end 
end

-- "takecp" has same precondition and postcondition except the
-- postcondition has return_bowl ~= arg_bowl instead of 
-- return_bowl == arg_bowl.  That is, they are different tables.

local function takecp(bowl, candyType)
  return take(CandyBowl(bowl), candyType)
end


-- Function howMany(bowl,candyType) returns the number of pieces of
-- candy that are in the "bowl" overall if "candyType" is nil;
-- otherwise, the function returns the count of the pieces of
-- "candyType" candy that are in the bowl.

-- Pre:  candyType == nil or validCandyType(candyType)
-- Post: if candyType == nil then
--           return == (Sum c,n: validCandyType(c) and
--                               n == howMany(arg_bowl,c) :: n)
--       else return == number of candyType candies in arg_bowl

-- Note: To formalize "number of candyType candies in arg_bowl" in the
-- postcondition, we need a richer abstract model for the ADT.  We
-- currently use the howMany(bowl,candyType) function to specify the
-- other functions.  As discussed in the BETTER APPROACH section of
-- the header comments, one approach is to use the mathematical
-- concept bag (or multiset) to model the ADT.  With that model, we
-- can restate the postcondition as: 
--       if candyType == nil then 
--         return == 
--         (Sum c,n: validCandyType(c) and n==howMany(arg_bowl,c)::n) 
--       else return == OCCURRENCES(candyType,CandyBowlBag)

local function howMany(bowl, candyType)
  candyType = candyType or SIZE
  return bowl[candyType] or 0
end


-- Function isEmpty(bowl) returns true if and only if the "bowl" is
-- empty.

-- Pre:  true
-- Post: howMany(bowl) == 0

local function isEmpty(bowl)
  return howMany(bowl) == 0
end


-- Definition useful in following functions
-- validInventory(inv) ==
--   inv ~= nil and type(inv) = "table" and
--   (ForAll i: i < 1 or i > #inv :: inv[i] == nil) and
--   (ForAll i: 1 <= i <= #inv ::
--     (Exists c,n: inv[i] == {c,n}:: validCandyType(c) and n > 0) )
--   and 
--   (ForAll i: 2 <= i <= #inv :: inv[i-1][1] < inv[i][1]) )


-- Function inventory(bowl) returns a list-style table of pairs
-- {candyType, count} with the list in ascending order by "candyType".

-- Pre:  true
-- Post: validInventory(return) and
--       (ForAll c,n: howMany(arg_bowl,c) == n and n > 0 ::
--         (Exists i: i > 0 :: return[i] == {c,n}) ))  and
--       (ForAll i,c,n: 1 <= i <= #return and return[i] == {c,n} ::
--           howMany(arg_bowl,c) == n) ) 

local function inventory(bowl)  
  local types = {}
  for c,n in pairs(bowl) do
    if c ~= SIZE then
      types[#types+1] = {c,n}
    end
  end
  table.sort(types,function(r,s) return r[1] < s[1] end)
  return types
end


-- Function toBowl(inv) takes an inventory "inv" (as returned by the
-- "inventory" function) and returns the corresponding bowl.  This
-- function is not required by the specification.

-- Pre:  validInventory(inv)
-- Post: (ForAll c,n: howMany(return_bowl,c) == n and n > 0 ::
--         (Exists i: i > 0 :: inv[i] == {c,n}) ))  and
--       (ForAll i,c,n: 1 <= i <= #inv and inv[i] == {c,n} ::
--           howMany(return_bowl,c) == n) ) 

local function toBowl(inv)
  local bowl = CandyBowl()
  for _,p in ipairs(inv) do
    put(bowl,p[1],p[2])
  end
  return bowl
end


-- Function combine(bowl1,bowl2) returns the bowl resulting from
-- pouring "bowl1" and "bowl2" together to form a new bowl.

-- Pre:  true (i.e., both bowl1 and bowl2 satisfy interface invariant)
-- Post: (ForAll c ::
--         howMany(return_bowl3,c) == howMany(arg_bowl1,c) + 
--                                    howMany(arg_bowl2,c) )

local function combine(bowl1,bowl2)
  local bowl3 = CandyBowl(bowl1)
  for c,n in pairs(bowl2) do
    if c ~= SIZE and n > 0 then put(bowl3,c,n) end
  end
  return bowl3
end


-- Function combine2(bowl1,bowl2) returns the bowl resulting from
-- pouring "bowl1" and "bowl2" together to form a new bowl.  Unlike
-- "combine", "combine2" does so without directly examining the
-- internal data representation.

-- Precondition and Postcondition same as "combine"

local function combine2(bowl1, bowl2)

  -- icopy list a into b from indexes i and j, respectively
  local function icopy(a,i,b,j)
    if i > #a then
      return b
    else
      b[j] = a[i]
      return icopy(a,i+1,b,j+1)
    end
  end

  -- merge ascending lists a and b into c from indexes i, j, and k
  local function merge(a,i,b,j,c,k)
    if i > #a then
      return icopy(b,j,c,k)
    elseif j > #b then
      return icopy(a,i,c,k)
    else 
      if a[i][1] < b[j][1] then
        c[k] = a[i]
        return merge(a,i+1,b,j,c,k+1)
      elseif a[i][1] == b[j][1] then
        c[k] = { a[i][1], a[i][2] + b[j][2] }
        return merge(a,i+1,b,j+1,c,k+1)
      else -- a[i][1] > b[j][1]
        c[k] = b[j]
        return merge(a,i,b,j+1,c,k+1)
      end
    end
  end

  local a, b, c = inventory(bowl1), inventory(bowl2), {}
  return toBowl(merge(a,1,b,1,c,1))
end


-- Module export

return { CandyBowl = CandyBowl,
         put       = put,
         putcp     = putcp,     -- extension
         take      = take,
         takecp    = takecp,    -- extension
         combine   = combine,
         combine2  = combine2,  -- extension
         inventory = inventory,
         toBowl    = toBowl,    -- extension
         has       = has,
         howMany   = howMany,
         isEmpty   = isEmpty
       }