Hets - the Heterogeneous Tool Set
Safe HaskellNone




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

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.