Command_Parser.hs revision e6d40133bc9f858308654afb1262b8b483ec5922
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann{- |
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannModule :$Header$
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannDescription : parser for Hets command line interface
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannCopyright : uni-bremen and Razvan Pascanu
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannLicence : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannMaintainer : r.pascanu@iu-bremen.de
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannStability : provisional
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannPortability : portable
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannParsing the comand line script.
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann TODO :
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann - add comments to the code
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann - delete the test functions
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-}
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannmodule PGIP.Command_Parser where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport PGIP.Commands
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport PGIP.Common
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport Data.Maybe
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport System.Console.Shell.Backend.Readline
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport System.Console.Shell.ShellMonad
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport System.Console.Shell
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport System.Console.Shell.Backend
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport Control.Monad.Trans
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport IO
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport qualified Control.Exception as Ex
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Checks the status to see if any library was loaded and generates the
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- corresponding prompter
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanngetFileUsed :: [Status] -> String
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanngetFileUsed ls
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = case ls of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (Address adr):_ -> takeName adr
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _:l -> getFileUsed l
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [] -> "Hets> "
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Removes any file extension from the name of the file
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanntakeName :: String -> String
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanntakeName ls
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = case ls of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ".casl" -> "> "
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann x :l -> x:(takeName l)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _ -> "> "
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | implements the command use for shellac
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellUse :: File -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellUse (File filename)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments filename
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cUse f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | implements the command dg-all auto for shellac
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgAutoAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgAutoAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllAuto "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgAuto :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgAuto input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str= stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAuto f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobSubsume :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobSubsume input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgGlobSubsume f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobDecomp :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobDecomp input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgGlobDecomp f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocInfer :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocInfer input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgLocInfer f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocDecomp :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocDecomp input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgLocDecomp f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgComp :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgComp input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgComp f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgCompNew :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgCompNew input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgCompNew f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgHideThm :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgHideThm input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgHideThm f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgBasic :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgBasic input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgInferBasic f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobSubsumeAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobSubsumeAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllGlobSubsume "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobDecompAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgGlobDecompAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllGlobDecomp "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocInferAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocInferAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllLocInfer "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocDecompAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgLocDecompAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllLocDecomp "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgCompAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgCompAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllComp "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgCompNewAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgCompNewAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllCompNew "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgHideThmAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgHideThmAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllHideThm "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgBasicAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDgBasicAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cDgAllInferBasic "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowDgGoals :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowDgGoals
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowDgGoals "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTheoryGoals :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTheoryGoals
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowTheory "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTheory :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTheory
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowNodeTheory "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellInfo :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellInfo
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowInfo "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTaxonomy :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTaxonomy
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowNodeTaxonomy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowConcept :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowConcept
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowNodeConcept "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellTranslate :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellTranslate input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cTranslate f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProver :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProver input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cProver f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellNodeNumber :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellNodeNumber input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cViewNodeNumber f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTheoryP :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTheoryP input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowNodeTheory f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellInfoP :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellInfoP input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowInfo f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTaxonomyP ::String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowTaxonomyP input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str=stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowNodeTaxonomy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowConceptP :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellShowConceptP input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str= stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO(cShowNodeConcept f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellEdges :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellEdges
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(cEdges "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellNodes :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellNodes
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(cNodes "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDetails :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDetails
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = shellPutStr printDetails
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannnothing :: [Status]->IO [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannnothing x
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = return x
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellComment :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellComment _
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val<- getShellSt >>= \state -> liftIO (nothing state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProve :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProve
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProveMix :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProveMix input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProveAllMix :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProveAllMix input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProveAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellProveAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetAxioms :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetAxioms input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(cDummy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetIncludeTheoremsTrue :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetIncludeTheoremsTrue
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetIncludeTheoremsFalse :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetIncludeTheoremsFalse
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state-> liftIO (cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetTimeLimit :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetTimeLimit input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetAxiomsAll ::Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellSetAxiomsAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellAddAxioms :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellAddAxioms input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellAddAxiomsAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellAddAxiomsAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDelAxioms :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDelAxioms input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str = stripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDelAxiomsAll :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDelAxiomsAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (cDummy "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDisplayGraph :: Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannshellDisplayGraph
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(cShowGraph "" state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | the 'doEvaluation' function evaluates an input which is not a command
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanndoEvaluation :: String -> [Status] -> IO [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanndoEvaluation str state
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = case str of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [] -> return []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _ -> case state of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [] -> do putStr ("Unkown input :"++str++"\n"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ++ "Type \'help\' for more information\n")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann return []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann LoadScript:_-> return ([More str])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _:l -> doEvaluation str l
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | the 'doFileEval' function evaluates an input which is not a command
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- in the case the input is provided as a file
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanndoFileEval :: String -> [Status] -> IO [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanndoFileEval str state
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = case str of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [] -> return []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _ -> case state of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [] -> do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann putStr ("\n Unkown input :" ++ str ++ "\n")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann return []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann LoadScript:_ -> return ([More str])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _:l -> doFileEval str l
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | The evaluation function is called when the input could not be parsed
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- as a command. If the input is an empty string do nothing, otherwise
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- print the error message
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipEvalFunc :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipEvalFunc str
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str= stripComments str
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <-getShellSt >>= \state -> liftIO(doEvaluation f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | The evaluation function in case shellac reads from a file.
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipFileEvalFunc :: String -> Sh [Status] ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipFileEvalFunc str
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let f_str= stripComments str
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann val <- getShellSt >>= \state -> liftIO (doFileEval f_str state)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann modifyShellSt (update val)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannstripComments :: String -> String
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannstripComments input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = case input of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann '#':_ -> []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [] -> []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann l:ls -> l:(stripComments ls)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Generates the list of all the shell commands toghether with a small help
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- message
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipShellCommands :: [ShellCommand [Status]]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipShellCommands
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = (exitCommand "exit")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (helpCommand "help")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "use" shellUse "open a file with HetCASL library")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg auto" shellDgAuto
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply automatic tactic to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg glob-subsume" shellDgGlobSubsume
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply global subsumption to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg glob-decomp" shellDgGlobDecomp
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply global decomposition to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg loc-infer" shellDgLocInfer
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply local inference to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg loc-decomp" shellDgLocDecomp
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply local decomposition to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg comp" shellDgComp
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply composition to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg comp-new" shellDgCompNew
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ("apply composition with speculation of new edges to"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " a list of goals"))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg hide-thm" shellDgHideThm
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply hide theorem shift to a list of goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg basic" shellDgBasic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "select a list of goals for proving")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all auto" shellDgAutoAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply automatic tactic to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all glob-subsume" shellDgGlobSubsumeAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply global subsumption to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all glob-decomp" shellDgGlobDecompAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply global decomposition to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all loc-infer" shellDgLocInferAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply local inference to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all loc-decomp" shellDgLocDecompAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply local decomposition to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all comp" shellDgCompAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply composition to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all comp-new" shellDgCompNewAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ("apply composition with speculation of new edges to"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " all goals"))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all hide-thm" shellDgHideThmAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "apply hide theorem shift to all goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "dg-all basic" shellDgBasicAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "select all goals for proving")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-dg-goals" shellShowDgGoals
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows list of all open dg goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-theory-goals" shellShowTheoryGoals
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows list of theory goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-theory-current" shellShowTheory
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows current theory and proof goals")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-theory" shellShowTheoryP
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows theory of the provided node")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "info-current" shellInfo
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows info about current dg node or edge")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "info" shellInfoP
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows info about the provided dg node")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-taxonomy-current" shellShowTaxonomy
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows taxonomy graph")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-taxonomy" shellShowTaxonomyP
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows taxonomy graph of the provided node")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-concept-current" shellShowConcept
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows concept graph")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-concept" shellShowConceptP
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "shows concept graph of the provided node")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "translate" shellTranslate
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "translate theory goals along comorphism")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "prover" shellProver
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "selects a prover")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "details" shellDetails
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "view details about the gramma of this interactive mode")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "node-number" shellNodeNumber
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " view node number")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "nodes" shellNodes
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "show all nodes of the development graph")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "edges" shellEdges
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "show all edges of the development graph")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "show-graph" shellDisplayGraph
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "displays the current dg graph")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "#" shellComment
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "comments")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "prove" shellProve
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Applies a theorem prover")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "prove-all" shellProveAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Applies a theorem prover to all theorems")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "prove {" shellProveMix
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Applies a theorem prove with a block of rules")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "prove-all {" shellProveAllMix
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Applies a theorem prover to all nodes")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "set axioms" shellSetAxioms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " A set of axioms to be used")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "set axioms-all" shellSetAxiomsAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " All axioms should be used")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "set include-theorems true"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann shellSetIncludeTheoremsTrue
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Include previous proved theorems")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "set include-theorems false"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann shellSetIncludeTheoremsFalse
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Do not include previous proved theorems")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "set time-limit" shellSetTimeLimit
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Time limit for the prover to run before abortion")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "add axioms" shellAddAxioms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Axioms to be considered by the prover")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "add axioms-all" shellAddAxiomsAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Axioms to be considered by the prover")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "del axioms" shellDelAxioms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Axioms that will not be considered by the prover")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : (cmd "del axioms-all" shellDelAxiomsAll
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Axioms that will not be considered by the prover")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann : []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Creates the Backend for reading from files
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfileBackend :: String -> ShellBackend Handle
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfileBackend filename =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let handle = openFile filename ReadMode in
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ShBackend
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { initBackend = handle
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , outputString = \_ -> basicOutput
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , flushOutput = \_ -> hFlush stdout
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , getSingleChar = \x -> fileGetSingleChar x
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , getInput = \x -> fileGetInput x
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , addHistory = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , setWordBreakChars = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , getWordBreakChars = \_ -> return " \t\n\r\v`~!@#$%^&*()=[]{};\\\'\",<>"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , onCancel = \_ -> hPutStrLn stdout "canceled...\n"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , setAttemptedCompletionFunction = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , setDefaultCompletionFunction = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , completeFilename = \_ _ -> return []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , completeUsername = \_ _ -> return []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , clearHistoryState = \_ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , getMaxHistoryEntries = \_ -> return 0
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , setMaxHistoryEntries = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , readHistory = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , writeHistory = \_ _ -> return ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann }
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Used to get one char from a file open for reading
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfileGetSingleChar :: Handle -> String -> IO (Maybe Char)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfileGetSingleChar file _ = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Ex.bracket (hGetBuffering file) (hSetBuffering file) $ \_ -> do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann hSetBuffering file NoBuffering
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann c <- hGetChar file
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann hPutStrLn stdout ""
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann return (Just c)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Used to get a line from a file open for reading
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfileGetInput :: Handle -> String -> IO (Maybe String)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfileGetInput file _ = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann x <- hGetLine file
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann return (Just x)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannbasicOutput :: BackendOutput -> IO ()
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannbasicOutput (RegularOutput out) = hPutStr stdout out
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannbasicOutput (InfoOutput out) = hPutStr stdout out
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannbasicOutput (ErrorOutput out) = hPutStr stderr out
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipInteractiveShellDescription :: ShellDescription [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipInteractiveShellDescription =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let wbc = "\n\r\v\\,;" in
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann initialShellDescription
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { shellCommands = pgipShellCommands
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , commandStyle = OnlyCommands
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , evaluateFunc = pgipEvalFunc
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , wordBreakChars = wbc
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , prompt = \x -> return (getFileUsed x)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , historyFile = Just ("consoleHistory.tmp")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann }
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipFileShellDescription :: ShellDescription [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipFileShellDescription =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let wbc = "\t\n\r\v\\,;" in
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann initialShellDescription
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { shellCommands = pgipShellCommands
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , commandStyle = OnlyCommands
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , evaluateFunc = pgipFileEvalFunc
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , wordBreakChars = wbc
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , prompt = \_ -> return ""
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , historyEnabled = False
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann }
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | The function runs hets in a shell
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipRunShell :: [String] ->IO [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipRunShell files
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann state <- getStatus files []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann runShell pgipInteractiveShellDescription {defaultCompletions = Just pgipCompletionFn}
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann readlineBackend
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann state
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | The function processes the file of instruction
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipProcessFile :: String -> IO [Status]
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannpgipProcessFile filename =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (runShell pgipFileShellDescription
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (fileBackend filename)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann []) `catch` (\_ -> return [])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannprintDetails :: String
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannprintDetails =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "\n\n Hets Interactive mode.The available grammar is\n\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- " -- Commands for development graph mode\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " use [PATH] -- open a file with a HetCASL library\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- this will compute a development graph\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- and a list of open proof obligations\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " dg [DG-COMMAND] [GOAL*] -- apply a proof step of the dg calculus\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " dg-all [DG-COMMAND] -- same as dg, but for all open goals\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " show-dg-goals -- display list of open dg goals\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- " -- commands for theory mode\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " show-theory-goals -- display list of theory goals\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " show-theory -- show current theory and proof goals\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " node-info -- show info about current\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- dg node (name, origin, sublogic)\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " show-taxonomy -- show taxonomy graph\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " show-concepts -- show conecpt graph\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " translate [COMORPHISM] -- translate theory goals \n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- along comorphism\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " prover [PROVER] -- select a prover\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " proof-script [FORMULA] [PROOF-SCRIPT] end-script\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- process proof script for one goal\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " cons-check PROVER -- check consistency\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- " -- interactive commands for theory mode\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " prove [FORMULA*] [AXIOM-SELECTION?]\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " prove-all [AXIOM-SELECTION?]\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " q/quit/exit -- exit hets\n\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " AXIOM-SELECTION ::=\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " with FORMULA+ -- include only specified axioms\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " exlcuding FORMULA+ -- exlcude specified axioms\n\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " PROOF-SCRIPT -- can be anything (prover specific)\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- the end is recognized with \"end-script\"\n\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " DG-COMMAND ::= \n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " auto -- automatic tactic\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " glob-subsume -- global subsumption\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " glob-decomp -- global decomposition\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " loc-infer -- local inference\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " loc-decomp -- local decomposition\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " comp -- composition\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " comp-new -- composition with speculation of new egdes\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " hide-thm -- Hide-Theorem-Shift\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " thm-hide -- Theorem-Hide-Shift\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " basic -- start proving at a particular node,\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " -- i.e. start local proving in a theory\n\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " GOAL ::= \n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " NODE -- select local goals at a node\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " NODE -> NODE -- select all edges between two given nodes\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " NODE - DIGIT* -> NODE -- select specific edge between two nodes\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "\n NODE ::= \n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " ID -- specify nodes with their names\n\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " COMORPHISM ::= ID ; ... ; ID -- composite of basic comorphisms\n\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " PROVER ::= ID -- name of prover\n\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " FORMULA ::= ID -- label of formula\n\n"++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " ID ::= -- identifier (String)\n\n"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann