Hets - the Heterogeneous Tool Set
Copyright(c) C. Maeder DFKI 2009
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

Proofs.VSE

Description

call an adaption of VSE II to hets

the prover should be attached to a node's menu (if applicable) but take the whole library environment as in- and output like development graph rules.

Synopsis

Documentation

thName :: LibName -> LNode DGNodeLab -> String Source #

getSubGraph :: Node -> DGraph -> DGraph Source #

proveVSE :: (LibName, Node) -> LibEnv -> IO (Result LibEnv) Source #

applies basic inference to a given node and whole import tree above

getLinksTo :: LibName -> DGraph -> LNode DGNodeLab -> IO String Source #

hetMorToSSexpr :: GMorphism -> [SExpr] Source #