-- This file:
--   http://angg.twu.net/IDRIS/brady/02/Average.idr.html
--   http://angg.twu.net/IDRIS/brady/02/Average.idr
--           (find-angg "IDRIS/brady/02/Average.idr")
--
-- (find-pdf-like-intro "7. Shorter hyperlinks to PDF files")
-- (find-bradytddfile "Chapter2/")
-- (find-bradytddfile "Chapter2/Average.idr")
-- (find-books "__comp/__comp.el" "brady")
-- (find-bradytddpage (+ 26  45)   "Modules and namespaces")
-- (find-bradytddtext (+ 26  45)   "Modules and namespaces")

module Average

-- See: https://idris2.readthedocs.io/en/latest/typedd/typedd.html
import Data.Strings -- for `words`
import Data.List    -- for `length` on lists

||| Calculate the average length of words in a string.
||| @str a string containing words separated by whitespace.
export
average : (str : String) -> Double
average str = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords
  where
    wordCount : String -> Nat
    wordCount str = length (words str)

    allLengths : List String -> List Nat
    allLengths strs = map length strs



{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris2 Average.idr
average "How long are these words?"
:t average
:printdef average
:?
-- :browse Average
-- :core average
-- :verbosity 4
-- :proofs

-}


{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris Average
average "How long are these words?"
:t average
:?
:browse Average
:core average
:printdef average
:verbosity 4
:proofs

-}