Hets - the Heterogeneous Tool Set

Copyright	(c) Otto-von-Guericke University of Magdeburg
License	GPLv2 or higher, see LICENSE.txt
Safe Haskell	None

HetsAPI

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
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]
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
proveNode :: TheoryPointer -> ProofOptions -> ResultT IO ProofResult

Documentation

automatic :: LibName -> LibEnv -> LibEnv Source #

globalSubsume :: LibName -> LibEnv -> LibEnv Source #

globalDecomposition :: LibName -> LibEnv -> LibEnv Source #

localInference :: LibName -> LibEnv -> LibEnv Source #

localDecomposition :: LibName -> LibEnv -> LibEnv Source #

compositionProveEdges :: LibName -> LibEnv -> LibEnv Source #

conservativity :: LibName -> LibEnv -> LibEnv Source #

automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv Source #

theoremHideShift :: LibName -> LibEnv -> Result LibEnv Source #

computeColimit :: LibName -> LibEnv -> Result LibEnv Source #

normalForm :: LibName -> LibEnv -> Result LibEnv Source #

triangleCons :: LibName -> LibEnv -> Result LibEnv Source #

freeness :: LibName -> LibEnv -> Result LibEnv Source #

libFlatImports :: LibName -> LibEnv -> Result LibEnv Source #

libFlatDUnions :: LibName -> LibEnv -> Result LibEnv Source #

libFlatRenamings :: LibName -> LibEnv -> Result LibEnv Source #

libFlatHiding :: LibName -> LibEnv -> Result LibEnv Source #

libFlatHeterogen :: LibName -> LibEnv -> Result LibEnv Source #

qualifyLibEnv :: LibName -> LibEnv -> Result LibEnv Source #

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 :: TheoryPointer -> 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.