Copyright	(c) Otto-von-Guericke University of Magdeburg
License	GPLv2 or higher, see LICENSE.txt
Safe Haskell	None

HetsAPI.InfoCommands

Description

Synopsis

getGraphForLibrary :: LibName -> LibEnv -> DGraph
getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab]
getEdgesFromDevelopmentGraph :: DGraph -> [DGLinkLab]
getLEdgesFromDevelopmentGraph :: DGraph -> [LEdge DGLinkLab]
getAllSentences :: G_theory -> TheorySentenceByName
getAllAxioms :: G_theory -> TheorySentenceByName
getAllGoals :: G_theory -> TheorySentenceByName
getProvenGoals :: G_theory -> TheorySentenceByName
getUnprovenGoals :: G_theory -> TheorySentenceByName
prettySentence :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Sentence -> String
prettySentenceOfTheory :: G_theory -> Sentence -> String
prettyTheory :: G_theory -> String
getDevelopmentGraphNodeType :: DGNodeLab -> DGNodeType
theorySentenceIsAxiom :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceWasTheorem :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceIsDefined :: SenAttr a (ThmStatus tStatus) -> Bool
theorySentenceGetTheoremStatus :: SenAttr a (ThmStatus tStatus) -> [tStatus]
theorySentencePriority :: SenAttr a (ThmStatus tStatus) -> Maybe String
theorySentenceContent :: SenAttr a (ThmStatus tStatus) -> a
theorySentenceBestProof :: Ord proof => SenAttr a (ThmStatus (c, proof)) -> Maybe proof
getLibraryDependencies :: LibEnv -> [(LibName, LibName)]
getRefinementTree :: String -> DGraph -> Maybe (Gr RefinementTreeNode RefinementTreeLink)
getAvailableSpecificationsForRefinement :: DGraph -> [String]

Documentation

getGraphForLibrary :: LibName -> LibEnv -> DGraph Source #

getDevelopmentGraphByName name env returns the development graph for the library name in the environment env.

getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab] Source #

getNodesFromDevelopmentGraph graph returns the nodes of the development graph graph

getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab] Source #

getNodesFromDevelopmentGraph graph returns the nodes of the development graph graph

getEdgesFromDevelopmentGraph :: DGraph -> [DGLinkLab] Source #

getLEdgesFromDevelopmentGraph :: DGraph -> [LEdge DGLinkLab] Source #

getAllSentences :: G_theory -> TheorySentenceByName Source #

getAllAxioms :: G_theory -> TheorySentenceByName Source #

getAllGoals :: G_theory -> TheorySentenceByName Source #

getProvenGoals :: G_theory -> TheorySentenceByName Source #

getUnprovenGoals :: G_theory -> TheorySentenceByName Source #

prettySentence :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Sentence -> String Source #

prettySentenceOfTheory :: G_theory -> Sentence -> String Source #

prettyTheory :: G_theory -> String Source #

getDevelopmentGraphNodeType :: DGNodeLab -> DGNodeType Source #

theorySentenceIsAxiom :: SenAttr a (ThmStatus tStatus) -> Bool Source #

theorySentenceWasTheorem :: SenAttr a (ThmStatus tStatus) -> Bool Source #

theorySentenceIsDefined :: SenAttr a (ThmStatus tStatus) -> Bool Source #

theorySentenceGetTheoremStatus :: SenAttr a (ThmStatus tStatus) -> [tStatus] Source #

theorySentencePriority :: SenAttr a (ThmStatus tStatus) -> Maybe String Source #

theorySentenceContent :: SenAttr a (ThmStatus tStatus) -> a Source #

theorySentenceBestProof :: Ord proof => SenAttr a (ThmStatus (c, proof)) -> Maybe proof Source #

getLibraryDependencies :: LibEnv -> [(LibName, LibName)] Source #

getRefinementTree :: String -> DGraph -> Maybe (Gr RefinementTreeNode RefinementTreeLink) Source #

getAvailableSpecificationsForRefinement :: DGraph -> [String] Source #