{- |
Module      :  $Header$
Description :  Utils for automatic proving procedure of multiple nodes
Copyright   :  (c) Simon Ulbricht, Uni Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  tekknix@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

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

module Common.AutoProofUtils where

import Common.GtkGoal

import Data.Maybe
import Data.Graph.Inductive.Graph (LNode)
import Data.List
import Data.Ord (comparing)

import Logic.Grothendieck

import Static.DevGraph
import Static.GTheory

-- | stores each node to be considered along with some further infomation
data FNode = FNode { name :: String
                   , node :: LNode DGNodeLab
                   , sublogic :: G_sublogics
                   , goals :: [String]
                     {- after proving, a new GTheory with the new Proofstatus
                     is computed -}
                   , results :: G_theory }

{- | mostly for the purpose of proper display, the resulting G_theory of each
FNode can be converted into a list of Goals. -}
toGtkGoals :: FNode -> [Goal]
toGtkGoals fn = map toGtkGoal . filter ((`elem` goals fn) . fst) . getThGoals
  $ results fn

{- | as a Prefix for display purpose, the ratio of proven and total goals
is shown -}
goalsToPrefix :: [Goal] -> String
goalsToPrefix gs = let p = length $ filter (\ g -> gStatus g == GProved) gs
                   in "[" ++ show p ++ "/" ++ show (length gs) ++ "] "

{- | Displays every goal of a Node with a prefix showing the status and the
goal name. -}
showStatus :: FNode -> String
showStatus fn = intercalate "\n" . map (\ g -> statusToPrefix
                 (gStatus g) ++ show (gName g)) $ toGtkGoals fn

-- | Get a markup string containing name and color
instance Show FNode where
  show fn = let gs = toGtkGoals fn
                gmin = gStatus $ minimum gs
            in
    "<span color=\"" ++ statusToColor gmin ++ "\">"
     ++ goalsToPrefix gs ++ name fn ++ "</span>"

instance Eq FNode where
  (==) f1 f2 = compare f1 f2 == EQ

{- | for comparison, the goal status of each node is considered. only with
equal goal status, nodes are sorted by name. -}
instance Ord FNode where
  compare = let gmin f = (minimum $ toGtkGoals f, name f)
            in comparing gmin

{- | 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 -}
initFNodes :: [LNode DGNodeLab] -> [FNode]
initFNodes = foldr (\ n@(_, l) t -> case globalTheory l of
                      Nothing -> t
                      Just gt ->
                        let gt' = dgn_theory l
                            gs = map fst $ getThGoals gt'
                        in if null gs then t else
                        FNode (getDGNodeName l) n (sublogicOfTh gt) gs gt' : t
              ) []

-- | returns True if a node has not been proved jet
unchecked :: FNode -> Bool
unchecked fn = all (isNothing . snd) . getThGoals $ results fn

-- | returns True if at least one goal has been timed out
timedout :: FNode -> Bool
timedout fn = any (\ a -> gStatus a == GTimeout) $ toGtkGoals fn

-- | returns True only if every goal has been proved
allProved :: FNode -> Bool
allProved fn = all (\ a -> gStatus a == GProved) $ toGtkGoals fn
