Safe Haskell | None |
---|
HetsAPI.Commands
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]
- translateTheory :: AnyComorphism -> G_theory -> Result G_theory
- showTheory :: G_theory -> String
- availableComorphisms :: G_theory -> [AnyComorphism]
- usableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
- usableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, 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])
- checkConsistency :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus
- checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory)
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
translateTheory :: AnyComorphism -> G_theory -> Result G_theory Source #
showTheory :: G_theory -> String Source #
availableComorphisms :: G_theory -> [AnyComorphism] Source #
availableComorphisms theory
yields all available comorphisms for theory
usableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #
usableProvers theory
checks for usable provers available on the machine
usableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)] Source #
usableConsistencyCheckers theory
checks for usable consistencey checkers
for theory
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
.
checkConsistency :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus Source #
checkConsistency includeTheorems cc comorphism libname libenv
dg node timeout
first applies the comorphism cc
to the theory at node
in the developmentGraph dg
inside the library libname
in the environment
libenv
, then checks the consistency using the consistency checker cc
with a timeout of timeout
seconds.
checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory) Source #