Hets - the Heterogeneous Tool Set
Copyright(c) Otto-von-Guericke University of Magdeburg
LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellNone

HetsAPI

Description

 
Synopsis

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

getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #

getUsableProvers theory checks for usable provers 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.