| Copyright | (c) Otto-von-Guericke University of Magdeburg |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Safe Haskell | None |
HetsAPI.Commands
Description
Synopsis
- automatic :: LibName -> LibEnv -> LibEnv
- globalSubsume :: LibName -> LibEnv -> LibEnv
- globalDecomposition :: LibName -> LibEnv -> LibEnv
- localInference :: LibName -> LibEnv -> LibEnv
- localDecomposition :: LibName -> LibEnv -> LibEnv
- compositionProveEdges :: LibName -> LibEnv -> LibEnv
- compositionCreateEdges :: LibName -> LibEnv -> LibEnv
- conservativity :: LibName -> LibEnv -> LibEnv
- automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
- theoremHideShift :: LibName -> LibEnv -> Result LibEnv
- computeColimit :: LibName -> LibEnv -> Result LibEnv
- normalForm :: LibName -> LibEnv -> Result LibEnv
- triangleCons :: LibName -> LibEnv -> Result LibEnv
- freeness :: LibName -> LibEnv -> Result LibEnv
- libFlatImports :: LibName -> LibEnv -> Result LibEnv
- libFlatDUnions :: LibName -> LibEnv -> Result LibEnv
- libFlatRenamings :: LibName -> LibEnv -> Result LibEnv
- libFlatHiding :: LibName -> LibEnv -> Result LibEnv
- libFlatHeterogen :: LibName -> LibEnv -> Result LibEnv
- qualifyLibEnv :: LibName -> LibEnv -> Result LibEnv
- loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv))
- translateTheory :: AnyComorphism -> G_theory -> Result G_theory
- showTheory :: G_theory -> String
- getAvailableComorphisms :: G_theory -> [AnyComorphism]
- getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
- getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)]
- proveNode :: G_theory -> ProofOptions -> ResultT IO ProofResult
- checkConsistency :: TheoryPointer -> ConsCheckingOptions -> IO ConsistencyStatus
- checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory)
- getGraphForLibrary :: LibName -> LibEnv -> DGraph
- getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
- getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab]
- getAllSentences :: G_theory -> SentenceByName
- getAllAxioms :: G_theory -> SentenceByName
- getAllGoals :: G_theory -> SentenceByName
- getProvenGoals :: G_theory -> SentenceByName
- getUnprovenGoals :: G_theory -> SentenceByName
Documentation
loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv)) Source #
translateTheory :: AnyComorphism -> G_theory -> Result G_theory Source #
showTheory :: G_theory -> String Source #
getAvailableComorphisms :: G_theory -> [AnyComorphism] Source #
getAvailableComorphisms theory yields all available comorphisms for theory
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #
getUsableProvers theory checks for usable provers available on the machine
getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)] Source #
getUsableConsistencyCheckers theory checks for usable consistencey checkers
for theory available on the machine
proveNode :: G_theory -> ProofOptions -> ResultT IO ProofResult Source #
proveNode theory prover comorphism proves all goals in theory using all
all axioms in theory. If prover or comorphism is Nothing the first
usable prover or comorphism, respectively, is used.
checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory) Source #
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
getAllGoals :: G_theory -> SentenceByName Source #