| 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
Description
Interfaces.Utils contains different utilitary functions for the abstract interface
- 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]
Returns the list of all nodes, if it is not up to date the function recomputes the list
getAllEdges :: IntIState -> [LEdge DGLinkLab]
Returns the list of all edges, if it is not up to date the funcrion recomputes the list
initNodeInfo :: ProofState -> Int -> Int_NodeInfo
Constructor for CMDLProofGUIState datatype
emptyIntIState :: LibEnv -> LibName -> IntIState
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)