{- |

Module :$Header$

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 c priority req fn = CmdlCmdDescription

{ cmdDescription = c

, cmdPriority = priority

, cmdReq = req

, cmdFn = fn }

genGlobCmd :: GlobCmd -> (CmdlState -> IO CmdlState) -> CmdlCmdDescription

genGlobCmd gc =

genCmd (GlobCmd gc) CmdNoPriority ReqNothing . CmdNoInput

reqOfSelectCmd :: SelectCmd -> CmdlCmdRequirements

reqOfSelectCmd sc = case sc of

LibFile -> ReqFile

Lib -> ReqFile

Node -> reqNodes

ComorphismTranslation -> ReqComorphism

Prover -> ReqProvers

Goal -> ReqAxm False

ConsistencyChecker -> ReqConsCheck

Link -> reqEdges

ConservativityCheckerOpen -> ReqNodesOrEdges Nothing $ Just OpenCons

ConservativityChecker -> ReqNodesOrEdges Nothing Nothing

genSelectCmd :: SelectCmd -> (String -> CmdlState -> IO CmdlState)

-> CmdlCmdDescription

genSelectCmd sc =

genCmd (mkSelectCmd sc) CmdNoPriority (reqOfSelectCmd sc) . CmdWithInput

reqOfInspectCmd :: InspectCmd -> CmdlCmdRequirements

reqOfInspectCmd ic = case ic of

EdgeInfo -> reqEdges

_ -> if requiresNode ic then reqNodes else ReqNothing

genGlobInspectCmd :: InspectCmd -> (CmdlState -> IO CmdlState)

-> CmdlCmdDescription

genGlobInspectCmd ic =

genCmd (InspectCmd ic Nothing) CmdNoPriority ReqNothing . CmdNoInput

genInspectCmd :: InspectCmd -> (String -> CmdlState -> IO CmdlState)

-> CmdlCmdDescription

genInspectCmd ic =

genCmd (InspectCmd ic (Just "")) CmdNoPriority (reqOfInspectCmd ic)

. CmdWithInput

genChangeCmd :: ChangeCmd -> (String -> CmdlState -> IO CmdlState)

-> CmdlCmdDescription

genChangeCmd cc =

genCmd (mkChangeCmd cc) CmdNoPriority ReqNothing . CmdWithInput

cmdlIgnoreFunc :: String -> CmdlCmdDescription

cmdlIgnoreFunc r =

genCmd (CommentCmd r) CmdNoPriority ReqNothing $ CmdNoInput return

-- for the synonym "prove-all"

proveAll :: CmdlCmdDescription

proveAll = genGlobCmd ProveCurrent cProve

disproveAll :: CmdlCmdDescription

disproveAll = genGlobCmd DisproveCurrent cDisprove

reqEdges :: CmdlCmdRequirements

reqEdges = ReqNodesOrEdges (Just False) Nothing

reqNodes :: CmdlCmdRequirements

reqNodes = ReqNodesOrEdges (Just True) Nothing

-- | Generates the list of all possible commands as command description

getCommands :: [CmdlCmdDescription]

getCommands =

map (\ (cm, act) -> genGlobCmd cm $ commandDgAll $ wrapResultDgAll act)

globLibAct

++ map (\ (cm, act) -> genGlobCmd cm $ commandDgAll act) globLibResultAct

++ map (\ (cm, act) -> genGlobCmd cm $ commandDgAll $ const act)

globResultAct

++

[ genGlobCmd UndoCmd cUndo

, genGlobCmd RedoCmd cRedo ]

++

[ genCmd (ShowOutput False) CmdNoPriority ReqNothing $

CmdNoInput (cShowOutput False)

, genCmd (ShowOutput True) CmdNoPriority ReqNothing $

CmdNoInput (cShowOutput True)]

++

[ genSelectCmd LibFile cUse

, genSelectCmd Node cDgSelect

, genSelectCmd ComorphismTranslation cTranslate

, genSelectCmd Prover cProver

, genSelectCmd Goal $ cGoalsAxmGeneral ActionSet ChangeGoals

, proveAll

, disproveAll

, genGlobCmd CheckConsistencyCurrent cConsistCheck

, genGlobCmd CheckConservativityAll cConservCheckAll

, genGlobCmd DropTranslation cDropTranslations

, genSelectCmd ConsistencyChecker cConsChecker

, genSelectCmd ConservativityCheckerOpen cConservCheck

, genSelectCmd ConservativityChecker cConservCheck

, genCmd (TimeLimit 0) CmdNoPriority ReqNumber $ CmdWithInput cTimeLimit

, genCmd (SetAxioms []) CmdNoPriority (ReqAxm True) $ CmdWithInput

$ cGoalsAxmGeneral ActionSet ChangeAxioms ]

++ map (\ b -> genCmd (IncludeProvenTheorems b) CmdNoPriority ReqNothing

$ CmdNoInput $ cSetUseThms b) [True, False]

++

[ genGlobInspectCmd Nodes cNodes

, genGlobInspectCmd Edges cEdges

, genGlobInspectCmd UndoHist cUndoHistory

, genGlobInspectCmd RedoHist cRedoHistory

, genGlobInspectCmd CurrentComorphism cCurrentComorphism

, genGlobInspectCmd ProvenGoals $ cShowNodeProvenGoals ""

, genGlobInspectCmd UnprovenGoals $ cShowNodeUnprovenGoals ""

, genGlobInspectCmd Axioms $ cShowNodeAxioms ""

, genGlobInspectCmd AllGoals $ cShowTheoryGoals ""

, genGlobInspectCmd Theory $ cShowTheory Dont_translate ""

, genGlobInspectCmd TranslatedTheory $ cShowTheory Do_translate ""

, genGlobInspectCmd Taxonomy $ cShowTaxonomy ""

, genGlobInspectCmd Concept $ cShowConcept ""

, genGlobInspectCmd NodeInfo cInfoCurrent

, genCmd (InspectCmd ComorphismsTo Nothing) CmdNoPriority ReqLogic

. CmdWithInput $ cComorphismsTo

, genInspectCmd NodeInfo cInfo

, genInspectCmd Theory $ cShowTheory Dont_translate

, genInspectCmd TranslatedTheory $ cShowTheory Do_translate

, genInspectCmd AllGoals cShowTheoryGoals

, genInspectCmd ProvenGoals cShowNodeProvenGoals

, genInspectCmd UnprovenGoals cShowNodeUnprovenGoals

, genInspectCmd Axioms cShowNodeAxioms

, genInspectCmd Taxonomy cShowTaxonomy

, genInspectCmd Concept cShowConcept

, genInspectCmd EdgeInfo cInfo ]

++

[ genChangeCmd Expand cExpand

, genChangeCmd AddView cAddView]

++

[ genCmd HelpCmd CmdNoPriority ReqNothing $ CmdNoInput $ cHelp getCommands

, genCmd ExitCmd CmdNoPriority ReqNothing $ CmdNoInput return ]