Copyright	(c) Simon Ulbricht Uni Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	tekknix@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	None

Common.AutoProofUtils

Description

This module provides sturctures and methods for the automatic proofs module.

Synopsis

data FNode = FNode {
- name :: String
- node :: LNode DGNodeLab
- sublogic :: G_sublogics
- goals :: [String]
- results :: G_theory
}
toGtkGoals :: FNode -> [Goal]
goalsToPrefix :: [Goal] -> String
showStatus :: FNode -> String
initFNodes :: [LNode DGNodeLab] -> [FNode]
unchecked :: FNode -> Bool
timedout :: FNode -> Bool
allProved :: FNode -> Bool

Documentation

data FNode Source #

stores each node to be considered along with some further infomation

Constructors

FNode
Fields name :: String node :: LNode DGNodeLab sublogic :: G_sublogics goals :: [String] results :: G_theory

Instances

Instances details

Eq FNode Source #
Instance details Defined in Common.AutoProofUtils Methods (==) :: FNode -> FNode -> Bool (/=) :: FNode -> FNode -> Bool
Ord FNode Source #	for comparison, the goal status of each node is considered. only with equal goal status, nodes are sorted by name.
Instance details Defined in Common.AutoProofUtils Methods compare :: FNode -> FNode -> Ordering (<) :: FNode -> FNode -> Bool (<=) :: FNode -> FNode -> Bool (>) :: FNode -> FNode -> Bool (>=) :: FNode -> FNode -> Bool max :: FNode -> FNode -> FNode min :: FNode -> FNode -> FNode
Show FNode Source #	Get a markup string containing name and color
Instance details Defined in Common.AutoProofUtils Methods showsPrec :: Int -> FNode -> ShowS show :: FNode -> String showList :: [FNode] -> ShowS

toGtkGoals :: FNode -> [Goal] Source #

mostly for the purpose of proper display, the resulting G_theory of each FNode can be converted into a list of Goals.

goalsToPrefix :: [Goal] -> String Source #

as a Prefix for display purpose, the ratio of proven and total goals is shown

showStatus :: FNode -> String Source #

Displays every goal of a Node with a prefix showing the status and the goal name.

initFNodes :: [LNode DGNodeLab] -> [FNode] Source #

gets all Nodes from the DGraph as input and creates a list of FNodes only containing Nodes to be considered. The results status field is initialised with the nodes local theory

unchecked :: FNode -> Bool Source #

returns True if a node has not been proved jet

timedout :: FNode -> Bool Source #

returns True if at least one goal has been timed out

allProved :: FNode -> Bool Source #

returns True only if every goal has been proved