b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaDescription : Utils for automatic proving procedure of multiple nodes
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaCopyright : (c) Simon Ulbricht, Uni Bremen 2010
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaLicense : GPLv2 or higher, see LICENSE.txt
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaMaintainer : tekknix@informatik.uni-bremen.de
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaStability : provisional
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaPortability : portable
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaThis module provides sturctures and methods for the automatic proofs module.
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastaimport Data.Ord (comparing)
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta-- | stores each node to be considered along with some further infomation
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastadata FNode = FNode { name :: String
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta , node :: LNode DGNodeLab
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta , sublogic :: G_sublogics
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta , goals :: [String]
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta {- after proving, a new GTheory with the new Proofstatus
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta is computed -}
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta , results :: G_theory }
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta{- | mostly for the purpose of proper display, the resulting G_theory of each
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaFNode can be converted into a list of Goals. -}
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastatoGtkGoals :: FNode -> [Goal]
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastatoGtkGoals fn = map toGtkGoal . filter ((`elem` goals fn) . fst) . getThGoals
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta $ results fn
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta{- | as a Prefix for display purpose, the ratio of proven and total goals
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastagoalsToPrefix :: [Goal] -> String
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastagoalsToPrefix gs = let p = length $ filter (\ g -> gStatus g == GProved) gs
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta in "[" ++ show p ++ "/" ++ show (length gs) ++ "] "
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta{- | Displays every goal of a Node with a prefix showing the status and the
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastagoal name. -}
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastashowStatus :: FNode -> String
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastashowStatus fn = intercalate "\n" . map (\ g -> statusToPrefix
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta (gStatus g) ++ show (gName g)) $ toGtkGoals fn
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta-- | Get a markup string containing name and color
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastainstance Show FNode where
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta show fn = let gs = toGtkGoals fn
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta gmin = gStatus $ minimum gs
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta "<span color=\"" ++ statusToColor gmin ++ "\">"
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta ++ goalsToPrefix gs ++ name fn ++ "</span>"
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastainstance Eq FNode where
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta (==) f1 f2 = compare f1 f2 == EQ
73505920a70e33977e84c69b4c3c598f683b7526Ondrej Kos{- | for comparison, the goal status of each node is considered. only with
73505920a70e33977e84c69b4c3c598f683b7526Ondrej Kosequal goal status, nodes are sorted by name. -}
73505920a70e33977e84c69b4c3c598f683b7526Ondrej Kosinstance Ord FNode where
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta compare = let gmin f = (minimum $ toGtkGoals f, name f)
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta in comparing gmin
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta{- | gets all Nodes from the DGraph as input and creates a list of FNodes only
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastacontaining Nodes to be considered.
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastaThe results status field is initialised with the nodes local theory -}
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastainitFNodes :: [LNode DGNodeLab] -> [FNode]
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan CholastainitFNodes = foldr (\ n@(_, l) t -> case globalTheory l of
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta Nothing -> t
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta let gt' = dgn_theory l
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta gs = map fst $ getThGoals gt'
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta in if null gs then t else
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta FNode (getDGNodeName l) n (sublogicOfTh gt) gs gt' : t
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta-- | returns True if a node has not been proved jet
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastaunchecked :: FNode -> Bool
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastaunchecked fn = all (isNothing . snd) . getThGoals $ results fn
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholasta-- | returns True if at least one goal has been timed out
b35f20cd8ecdc8308a3201e55752fb0443ec6ae4Jan Cholastatimedout :: FNode -> Bool