{- | Module :./CMDL/Commands.hs Description : list of all commands of CMDL interface Copyright : uni-bremen and DFKI License : GPLv2 or higher, see LICENSE.txt or LIZENZ.txt Maintainer : r.pascanu@jacobs-university.de Stability : provisional Portability : portable CMDL.Commands contains the description of all commands available -} module CMDL.Commands ( getCommands , proveAll , cmdlIgnoreFunc ) where import Interfaces.Command import Interfaces.CmdAction (globLibAct, globLibResultAct, globResultAct) import CMDL.DataTypes import CMDL.ProveCommands import CMDL.InfoCommands import CMDL.DgCommands (cDgSelect, cUse, cExpand, cAddView, commandDgAll, wrapResultDgAll) import CMDL.ProveConsistency (cConsChecker, cProver) import CMDL.UndoRedo (cRedo, cUndo) import CMDL.ConsCommands -- | Generates a command description given all parameters genCmd :: Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd :: Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd c :: Command c priority :: CmdlCmdPriority priority req :: CmdlCmdRequirements req fn :: CmdlCmdFnClasses fn = CmdlCmdDescription :: Command -> CmdlCmdPriority -> CmdlCmdFnClasses -> CmdlCmdRequirements -> CmdlCmdDescription CmdlCmdDescription { cmdDescription :: Command cmdDescription = Command c , cmdPriority :: CmdlCmdPriority cmdPriority = CmdlCmdPriority priority , cmdReq :: CmdlCmdRequirements cmdReq = CmdlCmdRequirements req , cmdFn :: CmdlCmdFnClasses cmdFn = CmdlCmdFnClasses fn } genGlobCmd :: GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd :: GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd gc :: GlobCmd gc = Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (GlobCmd -> Command GlobCmd GlobCmd gc) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> ((CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall b c a. (b -> c) -> (a -> b) -> a -> c . (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput reqOfSelectCmd :: SelectCmd -> CmdlCmdRequirements reqOfSelectCmd :: SelectCmd -> CmdlCmdRequirements reqOfSelectCmd sc :: SelectCmd sc = case SelectCmd sc of LibFile -> CmdlCmdRequirements ReqFile Lib -> CmdlCmdRequirements ReqFile Node -> CmdlCmdRequirements reqNodes ComorphismTranslation -> CmdlCmdRequirements ReqComorphism Prover -> CmdlCmdRequirements ReqProvers Goal -> Bool -> CmdlCmdRequirements ReqAxm Bool False ConsistencyChecker -> CmdlCmdRequirements ReqConsCheck Link -> CmdlCmdRequirements reqEdges ConservativityCheckerOpen -> Maybe Bool -> Maybe NodeOrEdgeFilter -> CmdlCmdRequirements ReqNodesOrEdges Maybe Bool forall a. Maybe a Nothing (Maybe NodeOrEdgeFilter -> CmdlCmdRequirements) -> Maybe NodeOrEdgeFilter -> CmdlCmdRequirements forall a b. (a -> b) -> a -> b $ NodeOrEdgeFilter -> Maybe NodeOrEdgeFilter forall a. a -> Maybe a Just NodeOrEdgeFilter OpenCons ConservativityChecker -> Maybe Bool -> Maybe NodeOrEdgeFilter -> CmdlCmdRequirements ReqNodesOrEdges Maybe Bool forall a. Maybe a Nothing Maybe NodeOrEdgeFilter forall a. Maybe a Nothing genSelectCmd :: SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd :: SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd sc :: SelectCmd sc = Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (SelectCmd -> Command mkSelectCmd SelectCmd sc) CmdlCmdPriority CmdNoPriority (SelectCmd -> CmdlCmdRequirements reqOfSelectCmd SelectCmd sc) (CmdlCmdFnClasses -> CmdlCmdDescription) -> ((String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall b c a. (b -> c) -> (a -> b) -> a -> c . (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdWithInput reqOfInspectCmd :: InspectCmd -> CmdlCmdRequirements reqOfInspectCmd :: InspectCmd -> CmdlCmdRequirements reqOfInspectCmd ic :: InspectCmd ic = case InspectCmd ic of EdgeInfo -> CmdlCmdRequirements reqEdges _ -> if InspectCmd -> Bool requiresNode InspectCmd ic then CmdlCmdRequirements reqNodes else CmdlCmdRequirements ReqNothing genGlobInspectCmd :: InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd :: InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd ic :: InspectCmd ic = Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (InspectCmd -> Maybe String -> Command InspectCmd InspectCmd ic Maybe String forall a. Maybe a Nothing) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> ((CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall b c a. (b -> c) -> (a -> b) -> a -> c . (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput genInspectCmd :: InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd :: InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd ic :: InspectCmd ic = Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (InspectCmd -> Maybe String -> Command InspectCmd InspectCmd ic (String -> Maybe String forall a. a -> Maybe a Just "")) CmdlCmdPriority CmdNoPriority (InspectCmd -> CmdlCmdRequirements reqOfInspectCmd InspectCmd ic) (CmdlCmdFnClasses -> CmdlCmdDescription) -> ((String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall b c a. (b -> c) -> (a -> b) -> a -> c . (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdWithInput genChangeCmd :: ChangeCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genChangeCmd :: ChangeCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genChangeCmd cc :: ChangeCmd cc = Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (ChangeCmd -> Command mkChangeCmd ChangeCmd cc) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> ((String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall b c a. (b -> c) -> (a -> b) -> a -> c . (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdWithInput cmdlIgnoreFunc :: String -> CmdlCmdDescription cmdlIgnoreFunc :: String -> CmdlCmdDescription cmdlIgnoreFunc r :: String r = Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (String -> Command CommentCmd String r) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return -- for the synonym "prove-all" proveAll :: CmdlCmdDescription proveAll :: CmdlCmdDescription proveAll = GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd ProveCurrent CmdlState -> IO CmdlState cProve disproveAll :: CmdlCmdDescription disproveAll :: CmdlCmdDescription disproveAll = GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd DisproveCurrent CmdlState -> IO CmdlState cDisprove reqEdges :: CmdlCmdRequirements reqEdges :: CmdlCmdRequirements reqEdges = Maybe Bool -> Maybe NodeOrEdgeFilter -> CmdlCmdRequirements ReqNodesOrEdges (Bool -> Maybe Bool forall a. a -> Maybe a Just Bool False) Maybe NodeOrEdgeFilter forall a. Maybe a Nothing reqNodes :: CmdlCmdRequirements reqNodes :: CmdlCmdRequirements reqNodes = Maybe Bool -> Maybe NodeOrEdgeFilter -> CmdlCmdRequirements ReqNodesOrEdges (Bool -> Maybe Bool forall a. a -> Maybe a Just Bool True) Maybe NodeOrEdgeFilter forall a. Maybe a Nothing -- | Generates the list of all possible commands as command description getCommands :: [CmdlCmdDescription] getCommands :: [CmdlCmdDescription] getCommands = ((GlobCmd, LibName -> LibEnv -> LibEnv) -> CmdlCmdDescription) -> [(GlobCmd, LibName -> LibEnv -> LibEnv)] -> [CmdlCmdDescription] forall a b. (a -> b) -> [a] -> [b] map (\ (cm :: GlobCmd cm, act :: LibName -> LibEnv -> LibEnv act) -> GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd cm ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState commandDgAll ((LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState) -> (LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ (LibName -> LibEnv -> LibEnv) -> LibName -> LibEnv -> Result LibEnv wrapResultDgAll LibName -> LibEnv -> LibEnv act) [(GlobCmd, LibName -> LibEnv -> LibEnv)] globLibAct [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ ((GlobCmd, LibName -> LibEnv -> Result LibEnv) -> CmdlCmdDescription) -> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)] -> [CmdlCmdDescription] forall a b. (a -> b) -> [a] -> [b] map (\ (cm :: GlobCmd cm, act :: LibName -> LibEnv -> Result LibEnv act) -> GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd cm ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState commandDgAll LibName -> LibEnv -> Result LibEnv act) [(GlobCmd, LibName -> LibEnv -> Result LibEnv)] globLibResultAct [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ ((GlobCmd, LibEnv -> Result LibEnv) -> CmdlCmdDescription) -> [(GlobCmd, LibEnv -> Result LibEnv)] -> [CmdlCmdDescription] forall a b. (a -> b) -> [a] -> [b] map (\ (cm :: GlobCmd cm, act :: LibEnv -> Result LibEnv act) -> GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd cm ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState commandDgAll ((LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState) -> (LibName -> LibEnv -> Result LibEnv) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ (LibEnv -> Result LibEnv) -> LibName -> LibEnv -> Result LibEnv forall a b. a -> b -> a const LibEnv -> Result LibEnv act) [(GlobCmd, LibEnv -> Result LibEnv)] globResultAct [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ [ GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd UndoCmd CmdlState -> IO CmdlState cUndo , GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd RedoCmd CmdlState -> IO CmdlState cRedo ] [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ [ Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (Bool -> Command ShowOutput Bool False) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput (Bool -> CmdlState -> IO CmdlState cShowOutput Bool False) , Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (Bool -> Command ShowOutput Bool True) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput (Bool -> CmdlState -> IO CmdlState cShowOutput Bool True)] [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ [ SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd LibFile String -> CmdlState -> IO CmdlState cUse , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd Node String -> CmdlState -> IO CmdlState cDgSelect , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd ComorphismTranslation String -> CmdlState -> IO CmdlState cTranslate , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd Prover String -> CmdlState -> IO CmdlState cProver , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd Goal ((String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ CmdlListAction -> CmdlGoalAxiom -> String -> CmdlState -> IO CmdlState cGoalsAxmGeneral CmdlListAction ActionSet CmdlGoalAxiom ChangeGoals , CmdlCmdDescription proveAll , CmdlCmdDescription disproveAll , GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd CheckConsistencyCurrent CmdlState -> IO CmdlState cConsistCheck , GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd CheckConservativityAll CmdlState -> IO CmdlState cConservCheckAll , GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobCmd GlobCmd DropTranslation CmdlState -> IO CmdlState cDropTranslations , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd ConsistencyChecker String -> CmdlState -> IO CmdlState cConsChecker , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd ConservativityCheckerOpen String -> CmdlState -> IO CmdlState cConservCheck , SelectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genSelectCmd SelectCmd ConservativityChecker String -> CmdlState -> IO CmdlState cConservCheck , Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (Int -> Command TimeLimit 0) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNumber (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdWithInput String -> CmdlState -> IO CmdlState cTimeLimit , Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd ([String] -> Command SetAxioms []) CmdlCmdPriority CmdNoPriority (Bool -> CmdlCmdRequirements ReqAxm Bool True) (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdWithInput ((String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses forall a b. (a -> b) -> a -> b $ CmdlListAction -> CmdlGoalAxiom -> String -> CmdlState -> IO CmdlState cGoalsAxmGeneral CmdlListAction ActionSet CmdlGoalAxiom ChangeAxioms ] [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ (Bool -> CmdlCmdDescription) -> [Bool] -> [CmdlCmdDescription] forall a b. (a -> b) -> [a] -> [b] map (\ b :: Bool b -> Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (Bool -> Command IncludeProvenTheorems Bool b) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput ((CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses forall a b. (a -> b) -> a -> b $ Bool -> CmdlState -> IO CmdlState cSetUseThms Bool b) [Bool True, Bool False] [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ [ InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd Nodes CmdlState -> IO CmdlState cNodes , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd Edges CmdlState -> IO CmdlState cEdges , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd UndoHist CmdlState -> IO CmdlState cUndoHistory , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd RedoHist CmdlState -> IO CmdlState cRedoHistory , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd CurrentComorphism CmdlState -> IO CmdlState cCurrentComorphism , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd ProvenGoals ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cShowNodeProvenGoals "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd UnprovenGoals ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cShowNodeUnprovenGoals "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd Axioms ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cShowNodeAxioms "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd AllGoals ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cShowTheoryGoals "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd Theory ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ CmdlUseTranslation -> String -> CmdlState -> IO CmdlState cShowTheory CmdlUseTranslation Dont_translate "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd TranslatedTheory ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ CmdlUseTranslation -> String -> CmdlState -> IO CmdlState cShowTheory CmdlUseTranslation Do_translate "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd Taxonomy ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cShowTaxonomy "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd Concept ((CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cShowConcept "" , InspectCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription genGlobInspectCmd InspectCmd NodeInfo CmdlState -> IO CmdlState cInfoCurrent , Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd (InspectCmd -> Maybe String -> Command InspectCmd InspectCmd ComorphismsTo Maybe String forall a. Maybe a Nothing) CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqLogic (CmdlCmdFnClasses -> CmdlCmdDescription) -> ((String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall b c a. (b -> c) -> (a -> b) -> a -> c . (String -> CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdWithInput ((String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ String -> CmdlState -> IO CmdlState cComorphismsTo , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd NodeInfo String -> CmdlState -> IO CmdlState cInfo , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd Theory ((String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ CmdlUseTranslation -> String -> CmdlState -> IO CmdlState cShowTheory CmdlUseTranslation Dont_translate , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd TranslatedTheory ((String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription) -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ CmdlUseTranslation -> String -> CmdlState -> IO CmdlState cShowTheory CmdlUseTranslation Do_translate , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd AllGoals String -> CmdlState -> IO CmdlState cShowTheoryGoals , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd ProvenGoals String -> CmdlState -> IO CmdlState cShowNodeProvenGoals , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd UnprovenGoals String -> CmdlState -> IO CmdlState cShowNodeUnprovenGoals , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd Axioms String -> CmdlState -> IO CmdlState cShowNodeAxioms , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd Taxonomy String -> CmdlState -> IO CmdlState cShowTaxonomy , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd Concept String -> CmdlState -> IO CmdlState cShowConcept , InspectCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genInspectCmd InspectCmd EdgeInfo String -> CmdlState -> IO CmdlState cInfo ] [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ [ ChangeCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genChangeCmd ChangeCmd Expand String -> CmdlState -> IO CmdlState cExpand , ChangeCmd -> (String -> CmdlState -> IO CmdlState) -> CmdlCmdDescription genChangeCmd ChangeCmd AddView String -> CmdlState -> IO CmdlState cAddView] [CmdlCmdDescription] -> [CmdlCmdDescription] -> [CmdlCmdDescription] forall a. [a] -> [a] -> [a] ++ [ Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd Command HelpCmd CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput ((CmdlState -> IO CmdlState) -> CmdlCmdFnClasses) -> (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses forall a b. (a -> b) -> a -> b $ [CmdlCmdDescription] -> CmdlState -> IO CmdlState cHelp [CmdlCmdDescription] getCommands , Command -> CmdlCmdPriority -> CmdlCmdRequirements -> CmdlCmdFnClasses -> CmdlCmdDescription genCmd Command ExitCmd CmdlCmdPriority CmdNoPriority CmdlCmdRequirements ReqNothing (CmdlCmdFnClasses -> CmdlCmdDescription) -> CmdlCmdFnClasses -> CmdlCmdDescription forall a b. (a -> b) -> a -> b $ (CmdlState -> IO CmdlState) -> CmdlCmdFnClasses CmdNoInput CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return ]