module DDCI.Core.Command.Help where

help :: String
help    = unlines
        [ "Commands available from the prompt:"
        , "  :quit              Exit DDCi-core" 
        , "  :help, :?          Display this help" 
        , ""
        , "Types"
        , "  :kind   TYPE       Show the kind of a type."
        , "  :tequiv TYPE TYPE  Check if two types are equivalent."
        , ""
        , "Witnesses"
        , "  :wtype   WITNESS   Show the type of a witness expression."
        , ""
        , "Expressions"
        , "  :check   EXP       Show the type, effect and closure of a value expression."
        , "  :type    EXP       Show the type    of a value expression."
        , "  :effect  EXP       Show the effect  of a value expression."
        , "  :closure EXP       Show the closure of a value expression." 
        , "  :ast     EXP       Show the abstract syntax tree of a value expression." 
        , "  :eval    EXP       Evaluate an expression."
        , ""
        , "Modes"
        , "  :set               Display active modes and transform"
        , "  :set +MODE         Enable a mode"
        , "  :set -MODE         Disable a mode"
        , ""
        , " Modes are:"
        , "  Indent             Pretty print expressions with indenting."
        , "  TraceEval          Show the expression at every step in the evaluation."
        , "  TraceStore         Show the store at every step in the evaluation." 
        , ""
        , "Transforms"
        , "  :set trans TRANS   Set the current transform."
        , "  :trans EXP         Transform the given expression."
        , "  :trun  EXP         Transform the given expression then evaluate it."
        , ""
        , "  TRANS ::= None | Anonymize | Beta"
        , ""
        ]