ftshell-0.2: src/Shell.hs

-- Configures and runs the shell.
module Shell where



import Paths_ftshell (version)

import Control.Monad (foldM, when)
import Data.Maybe (catMaybes, maybeToList)
import Data.Version (showVersion)
import Language.Haskell.FreeTheorems
import Language.Haskell.FreeTheorems.Syntax
import System.Console.Shell
import System.Console.Shell.ShellMonad
import System.Environment (getProgName)

import Settings
import ShellState
import Evaluate
import Commands
import HelpCommands



-- Initialises and runs the shell.
initAndRunShell :: Settings -> IO ()
initAndRunShell settings = do
  -- show the name and the purpose of the application, and give a quick command
  -- overview
  showGreetingMessage settings

  -- create an initial state from the settings given at the command line
  let initialState = initialShellState settings
  
  -- load the declarations files given at the command line
  let files = maybeToList (prelude settings) ++ inputFiles settings
  state <- foldM (\s f -> loadDeclarations f s) initialState files
  when (not (null files)) (putStrLn "")
  
  -- initialise the shell and run it
  let shellDescription = createShellDescription
  let shellBackend = backend settings
  runShell shellDescription shellBackend state
  return ()
      


-- Shows a short message giving the name, version, purpose and the most 
-- important commands of the shell.
showGreetingMessage :: Settings -> IO ()
showGreetingMessage settings = 
  putStr $ unlines
    [ "FTshell (version " ++ showVersion version ++ ") - " ++ 
      "Automatic generation of free theorems"
    , ""
    , "Press `:help' for help or `:quit' to quit."
    , ""
    ]



-- Creates the settings for the shell.
createShellDescription :: ShellDescription ShellState
createShellDescription =
  initialShellDescription {

    -- set the available commands, see also the function 'commands'
    shellCommands      = commands,

    -- commands are prefixed with a colon character
    commandStyle       = CharPrefixCommands ':',
    
    -- set the function called when something else than a command was entered
    evaluateFunc       = evaluate,

    -- set the prompt of the shell, this is based on the current context
    -- see 'createPrompt' for more information
    prompt             = createPrompt,

    -- signatures can be entered directly, tab completion of signatures
    -- is provided (if the readline backend is used)
    defaultCompletions = Just signatureCompletion,

    -- command history is turned on
    historyEnabled     = True,

    -- the maximum number of commands remembered in one session
    maxHistoryEntries  = 100,

    -- there is no file storing the commands of previous sessions
    historyFile        = Nothing
  }



-- Creates the prompt of the shell based on the current context.
createPrompt :: ShellState -> IO String
createPrompt state =
  case getCurrentContext state of
    Nothing    -> return "> "
    Just (s,_) -> let getName = unpackIdent . signatureName . rawSignature
                   in return (getName s ++ " > ")



-- Maps short and long command names to command functions.
commands :: [ShellCommand ShellState]
commands =
  [ helpCommand "help"

  , cmd "help-shell" cmdShowShellHelp
        "Display the shell user guide"

  , cmd "help-free-theorems" cmdShowTheoremHelp
        "Display an introduction to free theorems\n"
  
  , cmd "load" cmdLoad
        "Load a file of declarations"

  , cmd "unload" cmdUnload
        "Unload a file of declarations"

  , cmd "reload-all" cmdReload
        "Reload all declarations files"

  , cmd "files" cmdShowLoadedFiles
        "Display all loaded declarations files\n"
  
  , cmd "all-declarations" cmdShowAllDeclarations
        "Display all declared constructors"

  , cmd "declaration" cmdShowDeclaration
        "Display a declaration"

  , cmd "signatures" cmdShowSignatures
        "Display all available signatures"

 ,  cmd "current-signature" cmdShowCurrentSignature
        "Display the current signature\n"
  
  , cmd "language-subset" cmdShowLanguageSubset
        "Display the current language subset"
  
  , cmd "basic-subset" (cmdSetLanguageSubset $ BasicSubset)
        "Set `basic' as the current language subset"
  
  , cmd "fix-equational"
        (cmdSetLanguageSubset $ SubsetWithFix EquationalTheorem)
        "Set `fix-equational' as the current language subset"
  
  , cmd "fix-inequational"
        (cmdSetLanguageSubset $ SubsetWithFix InequationalTheorem)
        "Set `fix-inequational' as the current language subset"
  
  , cmd "seq-equational"
        (cmdSetLanguageSubset $ SubsetWithSeq EquationalTheorem)
        "Set `seq-equational' as the current language subset"
  
  , cmd "seq-inequational"  
        (cmdSetLanguageSubset $ SubsetWithSeq InequationalTheorem)
        "Set `seq-inequational' as the current language subset\n"

  , cmd "theorem" cmdShowTheorem
        "Display the current theorem"
  
  , cmd "lifts" cmdShowLiftedRelations
        "Display definitions for the lifted relations"
  
  , cmd "classes" cmdShowClasses
        "Display definitions for the class constraints"
  
  , cmd "relation-variables" cmdShowRelationVariables
        "Display all relation variables which can be specialised"
  
  , cmd "specialise" cmdSpecialise
        "Specialise a relation variable to a function"
  
  , cmd "specialise-inverse" cmdSpecialiseInverse
        "Specialise a relation variable to an inverse function"
  
  , cmd "undo" cmdUndo
        "Undo the last specialisation to a function"
  
  , cmd "options" cmdShowCurrentTheoremOptions
        "Display the currently selected theorem options"
  
  , cmd "show" cmdTheoremOptionShow
        "Turn on a theorem option"

  , cmd "omit" cmdTheoremOptionOmit
        "Turn off a theorem option\n"
  
  , exitCommand "quit"
  ]