
module Igor2.UI.Help (verboseHelp) where
import Igor2.Logging
import Igor2.Ppr

fillwords s = fillSep (map text $ words s)
bText = bold.text

verboseHelp :: Doc
verboseHelp =  
    bold (text "Example Igor2 session:") <$$>
    bold (text "==========================================") <$$>
    linebreak <>
    fillwords ("A typical Igor2 session would be as follows:") <$$>
    linebreak <>
    indent 10 (fillwords "IgorII > :load expl/Examples.hs")<$$>
    indent 10 (fillwords "File loaded in 1.0201s")<$$>
    indent 10 (fillwords "IgorII > :s +enhanced; :s +simplify")<$$>
    indent 10 (fillwords "IgorII > :g lasT")<$$>
    linebreak <>
    indent 10 (fillwords "      - - - - START SYNTHESIS WITH - - - -")<$$>
    indent 10 (fillwords "")<$$>
    indent 10 (fillwords "Targets              'lasT'")<$$>
    indent 10 (fillwords "Background           <none>")<$$>
    indent 10 (fillwords "Simplified           True")<$$>
    indent 10 (fillwords "Greedy rule-splitting False")<$$>
    indent 10 (fillwords "Enhanced             True")<$$>
    indent 10 (fillwords "Use paramorphisms    False")<$$>
    indent 10 (fillwords "Compare rec args     AWise")<$$>
    indent 10 (fillwords "DumpLog              False")<$$>
    indent 10 (fillwords "Debug                False")<$$>
    indent 10 (fillwords "Maximal tiers        0")<$$>
    indent 10 (fillwords "Maximal loops        -1")<$$>
    linebreak <>
    indent 10 (fillwords "      - - - - - - - FINISHED - - - - - - -")<$$> 
    linebreak <>
    indent 10 (fillwords "")<$$>
    indent 10 (fillwords "             lasT         in 2     loops")<$$>
    indent 10 (fillwords "            CPU: 0.0080s")<$$>
    indent 10 (fillwords "             ")<$$>
    linebreak <>
    indent 10 (fillwords "                 HYPOTHESIS 1 of 1")<$$>
    linebreak <>
    indent 10 (fillwords "lasT [a0] = a0")<$$>
    indent 10 (fillwords "lasT (_ : (a1 : a2)) = lasT (a1 : a2)")<$$>
    linebreak <>
    indent 10 (fillwords "IgorII > :quit")<$$>
    indent 10 (fillwords "Bye.")<$$>
    linebreak <>
    bold (text "Explanation of Igor2's commands:") <$$>
    bold (text "==========================================") <$$>
    linebreak <>
    fillwords ("Generally commands can be abbreviated with the first character \
               \of the long command preceeded by a colon, e.g. ':h' for \
               \':help'.")<$$>
    fillwords ("Multiple commands can be entered either one at a time, or \
               \together separated by a semicolon. Passing commands to Igor2 \
               \in batch mode or at command-line is similar. Except that you \
               \need to escape string quotes at command line with '\\\"'. For \
               \an example see the batch file 'expl/batch.txt'") <$$>
    linebreak <>
    (bText $ ":quit") <$$>
    indent 3 (fillwords "Quit the program.") <$$> 
    linebreak <>
    (bText $ ":help") <$$>
    indent 3 (fillwords "A short help text.") <$$> 
    linebreak <>
    (bText $ ":verboseHelp") <$$>
    indent 3 (fillwords "This longer helpt text.") <$$> 
    linebreak <>
    (bText $ ":load <path/to/file>") <$$>
    indent 3 (fillwords $ "Load a specification file into Igor2's context. The \
                          \file is required to be a correct Haskell module and \
                          \therefore has to type check. The I/O for a target \
                          \function must be non-recursive, of course. All \
                          \Prelude data types ([a], Bool, Maybe a, Either a b) \
                          \can be used and further data types can be defined \
                          \in this module. Imports are not supported, yet. \
                          \Note that the path is not expanded, so avoid \ 
                          \'~' for your home directory. Relativ paths do work, \
                          \ however use absolute paths to be on the safe \
                          \side.")<$$>
    linebreak <>
    (bText $ ":reset") <$$>
    indent 3 (fillwords $ "Resets the current context, and sets all options to \
                          \their default values.")<$$> 
    linebreak <>
    (bText $ ":batch <path/to/file>") <$$>
    indent 3 (fillwords $"Run all commands in the batch file until EOF, or \
                         \command is not exectuable, or ':quit'. Note that the \
                         \path is not expanded, so avoid '~'.") <$$> 
    linebreak <>
    (bText $ ":yell \"something\"") <$$>
    indent 3 (fillwords "Print \"something\" one the prompt.") <$$> 
    linebreak <>
    (bText $ ":set <option>") <$$>
    indent 3 (fillwords "Set an option, where <option> is one of the \
                        \following.") <$$>
    indent 5 (fill 20 (text "+debug") <> 
              align (fillwords "enable debug mode")) <$$>
    indent 5 (fill 20 (text "-debug") <> 
              align (fillwords "disable debug mode [default]")) <$$>
    indent 5 (fill 20 (text "+verbose") <> 
              align (fillwords "chatty ouput")) <$$>
    indent 5 (fill 20 (text "-verbose") <> 
              align (fillwords "normal output [default]")) <$$>
    indent 5 (fill 20 (text "+typeCheck") <> 
              align (fillwords "force typecheck of specification [default]")) <$$>
    indent 5 (fill 20 (text "-tyepcheck") <> 
              align (fillwords "accepts _ANY_ specification, (use at own risk)")) <$$>
    indent 5 (fill 20 (text "+greedySplt") <> 
              align (fillwords "Split rules greedily, i.e. split one rule at all possible pivot positions. Results in one successor with many patterns")) <$$>
    indent 5 (fill 20 (text "-greedySplt") <> 
              align (fillwords "Split at only one pivot position per rule, but make one split for each pivor position, results in multiple successor hypotheses with different patterns. [default]")) <$$>
    indent 5 (fill 20 (text "+accum") <>
              align (fillwords "Automatically introduce accumulator variables. Results in longer running times when it's not needed.")) <$$>
    indent 5 (fill 20 (text "-accum") <>
              align (fillwords "No accumulators are introduced. This is the [default]")) <$$>
    indent 5 (fill 20 (text "+greedyMtch") <>
              align (fillwords "Match calls greedily, i.e. only allow calls where a maximal number of parameters results in closed rules.")) <$$>
    indent 5 (fill 20 (text "+enhanced") <>
              align (fillwords "Enhanced mode, using type morphisms as program schemes")) <$$>
    indent 5 (fill 20 (text "-enhanced") <> 
              align (fillwords "normal mode, no morphisms [default]")) <$$>
    indent 5 (fill 20 (text "+para") <> 
              align (fillwords "if in enhanced mode, use paramorphisms instead of catamorphisms")) <$$>
    indent 5 (fill 20 (text "-para") <> 
              align (fillwords "use catamorphisms [default]")) <$$>
    indent 5 (fill 20 (text "+dumpLog") <> 
              align (fillwords "write a log file")) <$$>
    indent 5 (fill 20 (text "-dumpLog") <> 
              align (fillwords "do not write a log file [default]")) <$$>
    indent 5 (fill 20 (text "+simplify") <> 
              align (fillwords ("simplify the result by replacing constant \
                                \function calls"))) <$$>
    indent 5 (fill 20 (text "-simplify") <> 
              align (fillwords ("show Igor2's original solution \
                                \[default]"))) <$$>
    indent 5 (fill 20 (text "colWidth=N") <> 
              align (fillwords ("set the width of your display to N columns \
                                \[default 80]"))) <$$>
    indent 5 (fill 20 (text "maxLoops=N") <> 
              align (fillwords ("stop the synthesis cycle after N loops with a \
                                \(probably) partial result [default (-1)")))<$$>
    indent 5 (fill 20 (text "maxTiers=N") <> 
              align (fillwords ("A tiers is a set of hypotheses with the same \
                                \heuristic value. This option determines, how \
                                \many tiers are finished at most. N=0 just \
                                \stops when one solution has been found. For \
                                \N>0 all unfinished hypotheses which are as \  
                                \good as the current best are tried to finish \
                                \if they do not deteriorate. Thus, the N-best \
                                \hypotheses are returned. However they may be \
                                \partial. For N<0 search continues unitil the \
                                \search space is exhausted.\
                                \[default (0)]"))) <$$>
    indent 5 (fill 20 (text "dumpDir=\"dir\"") <> 
              align (fillwords ("This is the directory, where the log files \
                                \are 1dumped to [default \".\"]"))) <$$>
    indent 5 (fill 20 (text "redOrder=<mode>") <> 
              align (fillwords ("Sets the reduction Order to ensure \
                                \termination of the final program, \
                                \arguments of calling/called functions have to \
                                \be compared. <mode> states how this is done. \
                                \Use \"Linear\" to compare the total number of \
                                \constructor symbols in the arguments. To \
                                \compare the number of constructor symbols \
                                \argumentwise use \"AWise\" [default]. Given \
                                \two left-hand sides a = (a1 a2 ..) and b = \
                                \(b1 b2 ..), then a < b if a1 < b1 or a1 == b1 \
                                \and a2 < b2 or a1 == b1 and a2 == b2 ... . \
                                \This is necessary, if the size of arguments \
                                \does not change over all I/O examples, e.g. \
                                \if accumulator variables are involved."))) <$$>
    (bText $ ":info") <$$>
    indent 3 (fillwords $ "Shows the current context with the I/O examples of \
                          \the functions in scope, if 'verbose' is on, or the \
                          \number of the examples, otherwise. Furthermore, the \
                          \values of all options and flags are displayed as \
                          \well as specification details from the current \
                          \context.") <$$> 
    linebreak <>
    (bText $ ":generalise <tgts> [with <bgks>]") <$$>
    indent 3 (fillwords $ "Start Igor2 with one or more target functions to \
                          \generalise and optional functions as background \
                          \knowledge. <tgts> and <bgks> are list of names in \
                          \scope separated by commas.") <$$> 
    linebreak <>
    (bText $ ":test [<i>] <tgts> [with <bgks>] on \"cmd\"") <$$>
    indent 3 (fillwords $ "Test a previously generalised program. If there \
                          \were multiple hypotheses, <i> is the one you want \
                          \to test. If it is ommitted, all are tested. Please \
                          \note, that you have to exactly repeat the names of \
                          \target functions and backgroud knowledge of the run \
                          \you want to test.\n If the background knowledge \
                          \functions have already been synthesised, their \
                          \results are taken from the history, other wise the \
                          \I/O examples of them are used. Note, that this may \
                          \cause the interpreter to end with \" Non-exhaustive \
                          \patterns\"-errors. If the background functions had \
                          \multiple results, all combinations are tested.")<$$> 
    linebreak 
