> module Project3C(columns)
>  where
>  import SequenceUtilities(blocks)


columnsWith splits a sequence of items into a sequence of "columns"
of uniform height:
  columnsWith p c [x1, x2, ..., xn] = [col1, col2, ..., colc]
  where
    1  length(col1) = length(col3) = ... = length(colc) = h
       where h = ceiling(n/c)
    2  col1 ++ col2 ++ ... ++ colc  contains all the items supplied
       in [x1, x2, ..., xn], and in the same order; that is,
          [x1, x2, ..., xn] is a subsequence of concat(cols),
          where cols = [col1, col2, ..., colc]
    3  all elements of each column are among the supplied items,
       except that the last element in at most c-1 columns may be
       p, which is used if necessary to pad the column to height h

>  columnsWith :: a -> Int -> [a] -> [[a]]
>  columnsWith pad numberOfColumns items =
>    unpaddedColumns ++ [col ++ [pad] | col <- paddedColumns]
>    where
>    height = numberOfItems `div` numberOfColumns +
>             min 1 (numberOfItems `mod` numberOfColumns)
>    numberOfPaddedColumns = height*numberOfColumns - numberOfItems
>    numberOfUnpaddedColumns = numberOfColumns - numberOfPaddedColumns
>    (itemsInUnpaddedColumns, itemsInPaddedColumns) =
>      splitAt(numberOfUnpaddedColumns * height) items
>    unpaddedColumns = blocks height       itemsInUnpaddedColumns
>    paddedColumns   = blocks (height - 1) itemsInPaddedColumns
>    numberOfItems = length items


columns splits a sequence of strings
into a sequence of "columns" of strings
Examples:
   columns 3 ["Bool", "Char", "Int", "Float",
              "Double", "Integer", "String"] =
                                [["Bool", "Char", "Int"],
                                 ["Float", "Double", ""],
                                 ["Integer", "String", ""]]
   columns 3 ["Bool", "Char", "Int", "Float", "Double", "Integer"] =
                                [["Bool", "Char"],
                                 ["Int", "Float"],
                                 ["Double", "Integer"]]
   columns 3 ["Bool", "Char", "Int", "Float", "Double"] =
                                [["Bool", "Char"],
                                 ["Int", "Float"],
                                 ["Double", ""]]
   columns 3 [ ] = [ ]
   columns 3 (repeat "inf")  fails to deliver

>  columns :: Int -> [String] -> [[String]]
>  columns = columnsWith ""


Theorem Col (Property 2 of columnsWith)
   xs is a subsequence of concat(columnsWith p c xs)

proof:

The definition of columnsWith says that
   columnsWith p c items
   unpaddedColumns ++ [col ++ [pad] | col <- paddedColumns]
for certain definitions of unpaddedColumns and paddedcolumns.

Without the pad elements, the above sequence is
   unpaddedColumns ++ [col | col <- paddedColumns]
Therefore, it is sufficient to show that xs is a subsequence of
   concat(unpaddedColumns ++ [col | col <- paddedColumns])

Of course, [col | col <- paddedColumns] is just another way to
specify the sequence paddedColumns, so it is enough to show that
xs is a subsequence of
   concat(unpaddedColumns ++ paddedColumns)

And, since concat(xs ++ ys) = concat(xs) ++ concat(ys), it is
equivalent to show that xs is a subsequence of
   concat(unpaddedColumns) ++ concat(paddedColumns)

The where clause defines these sequences as follows:
   unpaddedColumns = blocks height itemsInUnpaddedColumns
and
   paddedColumns = blocks (height - 1) itemsInPaddedColumns

By a property of the function blocks, it follows that
   concat(unpaddedColumns) = itemsInUnpaddedColumns
and
   concat(paddedColumns) = itemsInPaddedColumns
 
So, concat(unpaddedColumns) ++ concat(paddedColumns) =
   itemsInPaddedColumns ++ itemsInUnpaddedColumns

The where clause defines these sequences as
   (itemsInUnpaddedColumns, itemsInPaddedColumns) =
          splitAt(numberOfUnpaddedColumns * height) xs
  -- remember xs is the name we are using for the argument
     corresponding to the formal parameter called items

So, by Theorem S, 
   xs = itemsInPaddedColumns ++ itemsInUnpaddedColumns

This means that xs is exactly the same sequence as, and
therefore also a subsequence of
   concat(unpaddedColumns) ++ concat(paddedColumns)
                                                      QED