{- |
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 ]