Safe Haskell | None |
---|
HetsAPI
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
- 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))
- getGraphForLibrary :: LibName -> LibEnv -> DGraph
- getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
- getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab]
- usableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
- autoProveNode :: G_theory -> Maybe G_prover -> Maybe AnyComorphism -> ResultT IO (G_theory, ProofState, [ProofStatus G_proof_tree])
- proveNode :: Bool -> Int -> [String] -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO (ProofState, [ProofStatus G_proof_tree])
Documentation
loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv)) 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
usableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #
usableProvers theory
checks for usable provers available on the machine
autoProveNode :: G_theory -> Maybe G_prover -> Maybe AnyComorphism -> ResultT IO (G_theory, ProofState, [ProofStatus G_proof_tree]) 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.
proveNode :: Bool -> Int -> [String] -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO (ProofState, [ProofStatus G_proof_tree]) Source #
proveNode sub timeout goals axioms theory (prover, comorphism)
proves
goals
with prover
after applying comorphism
. If goals
is empty all
goals are selected. Same for axioms
. If sub
is set theorems are used in
subsequent proofs. The runtime is restricted by timeout
.