module COMMERCE_TYPES is

-------------------------------------------------------------------------------
-- Stocks held by suppliers and stores in the stock management example
-------------------------------------------------------------------------------

type Product is
   -- products are represented by a (range of) natural numbers
   range 0 .. 4 of Nat
   with ==, !=, <, succ, last
end type

-------------------------------------------------------------------------------

type Stock is
   -- a store is a list of products with their quantities
   empty,
   cons (p: Product, q: Nat, s: Stock)
end type

-------------------------------------------------------------------------------

function isAvailable (p: Product, q: Nat, s: Stock) : Bool is
   case s
      var p1: Product, q1: Nat, s1: Stock
   in
      empty ->
         return false
   |  cons (p1, q1, s1) ->
         if p == p1 then
	    return q1 >= q
	 else
	    return isAvailable (p, q, s1)
	 end if
   end case
end function

-------------------------------------------------------------------------------

function decrease (p: Product, q: Nat, s: Stock) : Stock is
   -- remove q instances of p from s
   case s
      var p1: Product, q1: Nat, s1: Stock
   in
      empty ->
         raise UNEXPECTED
   |  cons (p1, q1, s1) ->
         if p == p1 then
	    return cons (p1, q1 - q, s1)
	 else
	    return cons (p1, q1, decrease (p, q, s1))
	 end if
   end case
end function

-------------------------------------------------------------------------------

function increase (p: Product, q: Nat, s: Stock) : Stock is
   -- add q instances of p to s
   case s
      var p1: Product, q1: Nat, s1: Stock
   in
      empty ->
         raise UNEXPECTED
   |  cons (p1, q1, s1) ->
         if p == p1 then
	    return cons (p1, q1 + q, s1)
	 else
	    return cons (p1, q1, increase (p, q, s1))
	 end if
   end case
end function

-------------------------------------------------------------------------------

function extract (s: Stock) : Product is
   -- extract the smallest product absent from s
   case s
      var p1: Product, q1: Nat, s1: Stock
   in
      empty ->
         return 0 of Product
   |  cons (p1, q1, s1) ->
         if q1 == 0 then
	    return p1
	 else
	    return extract (s1)
	 end if
   end case
end function

-------------------------------------------------------------------------------
-- Definition of initial stocks held by suppliers and stores
-------------------------------------------------------------------------------

function stock_supplier_1 : Stock is
   return cons (1 of Product, 9,
          cons (2 of Product, 18,
          empty))
end function

-------------------------------------------------------------------------------

function stock_supplier_2 : Stock is
   return cons (3 of Product, 7,
          cons (4 of Product, 18,
          empty))
end function

-------------------------------------------------------------------------------

function stock_local_1 : Stock is
   return cons (1 of Product, 9,
          cons (2 of Product, 4,
          cons (3 of Product, 0,
          empty)))
end function

-------------------------------------------------------------------------------

function stock_local_2 : Stock is
   return cons (1 of Product, 4,
          cons (2 of Product, 0,
          cons (3 of Product, 8,
          empty)))
end function

-------------------------------------------------------------------------------

function stock_central : Stock is
   return cons (1 of Product, 6, cons (2 of Product, 5, cons (3 of Product, 8, empty)))
end function

-------------------------------------------------------------------------------

end module