> import TableConversion(display, normalize, unpack)
> import IOutilities(integralFromString, getCookedLine)


> main =
>  do
>    putStr promptFilename
>    filename <- getCookedLine
>    putStr queryFormat
>    format <- getCookedLine
>    (putStr . queryDigits . map toUpper) format
>    numberOfDigitsAsString <- getCookedLine
>    datafile <- readFile filename
>    putStr "\n"
>    (putStr .
>     display format (integralFromString numberOfDigitsAsString) .
>     normalize .
>     unpackFloat) datafile


specialize unpacking of file to interpret numbers in type Float

> unpackFloat :: String -> ([String], [String], [String], [[Float]])
> unpackFloat = unpack


interaction prompts

> promptFilename, queryFormat :: String
> promptFilename = "Enter name of data file: "
> queryFormat = "Common numeral (C) or Scientific notation (S)? "

> queryDigits :: String -> String
> queryDigits format
>   |format == "C"     = "Display how many decimal places? "
>   |otherwise         = "Display how many significant digits? "


Property T
  If m::Int, n::int, m > 0, n > 0, rs::[[a]] is a sequence of
  sequences with length(rs)=m, each element r in rs has
  length(r)=n, and cs=transpose(rs),
  then (1) length(cs)=n and
       (2) each element of c in cs has length(c)=m

proof

  let [r1, r2, ..., rm] denote rs    -- rs has m elements
  let [xi1, xi2, ..., xin] denote ri -- each r in rs has n elems 

   transpose rs
 = foldr p [ ] rs                     -- definition of transpose
    where p r cs =
          zipwith (:) row (columns ++ [ [], [], ... ])
 = r1 `p` (r2 `p` ... `p` (rm `p` [ ]) ...) -- def'n of foldr
 = r1 `p` (r2 `p` ... `p`
    (zipWith (:) rm [ [], [], ... ]))       -- def'n of p
 = r1 `p` (r2 `p` ... `p`
    (zipWith (:) [xm1, xm2, ..., xmn] [ [], [], ...])) --def'n of rm
 = r1 `p` (r2 `p` ... `p`
    [[xm1], [xm2], ..., [xmn]])              -- def'n of zipWith(:)
 = r1 `p` ([x21, x22, ..., x2n] `p` ...
            `p`  [[xm1], [xm2], ..., [xmn]]) -- def'n of r2
 = r1 `p` (zipWith (:)
                   [x21, x22, ..., x2n]      -- def'n of p
                   (zipWith (:)
                            ...
                            [[xm1], [xm2], ..., [xmn]])) 
 = r1 `p` [[x21, ..., xm1],
           [x22, ..., xm2]
            ...                              -- def'n of zipWith(:)
           [x2n, ..., xmn]]
 = zipWith (:) [x11, x12, ..., x1n]
               [[x21, ..., xm1],             -- def'ns of p and r1
                [x22, ..., xm2],
                 ...
                [x2n, ..., xmn]]
 = [[x11, x21, ..., xm1],
    [x12, x22, ..., xm2],
     ...                                     -- def'n of zipWith(:)
    [x1n, x2n, ..., xmn]]
 = [c1,
     ...                                     -- def'n of ci
    cn]
      where each ci has m elements           -- QED (2)
 = cs                                        -- def'n of cs
      where cs has n elements                -- QED (1)
                                                        QED