-- Shell commands for user help.
module HelpCommands where


import System.Console.Shell
import System.Console.Shell.ShellMonad
import Text.PrettyPrint

import ShellState



paragraph s = 
  let st = style { lineLength = 78, ribbonsPerLine=1.0 }
   in do shellPutStrLn . renderStyle st . fsep . map text . words $ s
         shellPutStrLn ""



cmdShowShellHelp :: Sh ShellState ()
cmdShowShellHelp = do
  shellPutStrLn $ unlines
    [ ""
    , "   FTSHELL USER GUIDE"
    ]
  paragraph $
    "This shell allows to automatically generate free theorems for "
    ++ "Haskell types. See `:help-theorems' for a short introduction to "
    ++ "free theorems."
  paragraph $ 
    "Interaction with this shell is done through entering commands at the "
    ++ "prompt. Every command is prefixed by a colon, i.e. the character `:'. "
    ++ "The list of available commands is shown when entering `:help' at the "
    ++ "prompt. Commands may be completed by pressing the TAB key."
  paragraph $
    "Besides entering commands, the user may also input types or type names at "
    ++ "the prompt. There also, TAB-completion is provided. The available "
    ++ "types can be obtained by entering either `:all-declarations' or "
    ++ "`:signatures'."
  paragraph $
    "When entering a valid type or the name of an already existing type, the "
    ++ "current context is switched to this type. The shell's commands are "
    ++ "then applied to this type and the theorem generated from it, which is "
    ++ "displayed directly after entering the type or by entering `:theorem'. "
    ++ "Commands working on the current theorem are `:lifts' to show the "
    ++ "definition of lifted relations and `:classes' to display class "
    ++ "constraints occurring in generated theorems."
  paragraph $
    "Relation variables of a theorem can be specialized to functions using "
    ++ "the `:specialise' or the `:specialise-inverse' command. The deduced "
    ++ "theorem is immediately printed afterwards. Every specialization may "
    ++ "be undone by the `:undo' command."
  paragraph $
    "The display of theorems may be modified by theorem options. They can be "
    ++ "by either `:show' or `:omit', and the current options are printed "
    ++ "when `:options' is entered at the prompt."




cmdShowTheoremHelp :: Sh ShellState ()
cmdShowTheoremHelp = do
  shellPutStrLn $ unlines
    [ ""
    , "   FREE THEOREMS IN A NUTSHELL"
    ]
  paragraph $
    "Free Theorems are results solely derived from the type of a function. "
    ++ "The key idea is to interpret types as relations. To reflect the "
    ++ "structure of types, a relational action, which maps relations to a "
    ++ "relation, is defined for every type constructor. Using relational "
    ++ "actions, a relation can be constructed for every type, and, by "
    ++ "applying the definitions of these relational actions, free theorems "
    ++ "are obtained."
  paragraph $
    "Recursion and selective strictness weaken free theorems. To study the "
    ++ "influences caused by adding these constructs, several sublanguages "
    ++ "are provided in this application. Here, `fix' corresponds to "
    ++ "languages where recursion is allowed, and `seq' describes "
    ++ "sublanguages where both recursion and selective strictness is "
    ++ "provided. Additionally, it is possible to derive equational and "
    ++ "inequational theorems."