content: {- |
  Module      :  ./Common/AutoProofUtils.hs
  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
  