Copyright | uni-bremen and DFKI |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | r.pascanu@jacobs-university.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Interfaces.Utils contains different utilitary functions for the abstract interface
Synopsis
- getAllNodes :: IntIState -> [LNode DGNodeLab]
- getAllEdges :: IntIState -> [LEdge DGLinkLab]
- initNodeInfo :: ProofState -> Int -> Int_NodeInfo
- emptyIntIState :: LibEnv -> LibName -> IntIState
- emptyIntState :: IntState
- wasProved :: ProofStatus proof_Tree -> Bool
- parseTimeLimit :: ProofStatus proof_tree -> Int
- addCommandHistoryToState :: IORef IntState -> ProofState -> Maybe (G_prover, AnyComorphism) -> [ProofStatus proof_tree] -> String -> (Bool, Int) -> IO ()
- checkConservativityNode :: Bool -> LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory)
- checkConservativityEdge :: Bool -> LEdge DGLinkLab -> LibEnv -> LibName -> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
- updateNodeProof :: LibName -> IntState -> LNode DGNodeLab -> G_theory -> (IntState, [DGChange])
Documentation
getAllNodes :: IntIState -> [LNode DGNodeLab] Source #
Returns the list of all nodes, if it is not up to date the function recomputes the list
getAllEdges :: IntIState -> [LEdge DGLinkLab] Source #
Returns the list of all edges, if it is not up to date the funcrion recomputes the list
initNodeInfo :: ProofState -> Int -> Int_NodeInfo Source #
Constructor for CMDLProofGUIState datatype
wasProved :: ProofStatus proof_Tree -> Bool Source #
parseTimeLimit :: ProofStatus proof_tree -> Int Source #
addCommandHistoryToState :: IORef IntState -> ProofState -> Maybe (G_prover, AnyComorphism) -> [ProofStatus proof_tree] -> String -> (Bool, Int) -> IO () Source #
checkConservativityNode :: Bool -> LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory) Source #
checkConservativityEdge :: Bool -> LEdge DGLinkLab -> LibEnv -> LibName -> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory) Source #