{- |
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 { FNode -> String
name :: String
                   , FNode -> LNode DGNodeLab
node :: LNode DGNodeLab
                   , FNode -> G_sublogics
sublogic :: G_sublogics
                   , FNode -> [String]
goals :: [String]
                     {- after proving, a new GTheory with the new Proofstatus
                     is computed -}
                   , FNode -> G_theory
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 :: FNode -> [Goal]
toGtkGoals fn :: FNode
fn = ((String, Maybe BasicProof) -> Goal)
-> [(String, Maybe BasicProof)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (String, Maybe BasicProof) -> Goal
toGtkGoal ([(String, Maybe BasicProof)] -> [Goal])
-> (G_theory -> [(String, Maybe BasicProof)]) -> G_theory -> [Goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Maybe BasicProof) -> Bool)
-> [(String, Maybe BasicProof)] -> [(String, Maybe BasicProof)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FNode -> [String]
goals FNode
fn) (String -> Bool)
-> ((String, Maybe BasicProof) -> String)
-> (String, Maybe BasicProof)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Maybe BasicProof) -> String
forall a b. (a, b) -> a
fst) ([(String, Maybe BasicProof)] -> [(String, Maybe BasicProof)])
-> (G_theory -> [(String, Maybe BasicProof)])
-> G_theory
-> [(String, Maybe BasicProof)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_theory -> [(String, Maybe BasicProof)]
getThGoals
  (G_theory -> [Goal]) -> G_theory -> [Goal]
forall a b. (a -> b) -> a -> b
$ FNode -> G_theory
results FNode
fn

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

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

-- | Get a markup string containing name and color
instance Show FNode where
  show :: FNode -> String
show fn :: FNode
fn = let gs :: [Goal]
gs = FNode -> [Goal]
toGtkGoals FNode
fn
                gmin :: GStatus
gmin = Goal -> GStatus
gStatus (Goal -> GStatus) -> Goal -> GStatus
forall a b. (a -> b) -> a -> b
$ [Goal] -> Goal
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Goal]
gs
            in
    "<span color=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ GStatus -> String
statusToColor GStatus
gmin String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\">"
     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Goal] -> String
goalsToPrefix [Goal]
gs String -> String -> String
forall a. [a] -> [a] -> [a]
++ FNode -> String
name FNode
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "</span>"

instance Eq FNode where
  == :: FNode -> FNode -> Bool
(==) f1 :: FNode
f1 f2 :: FNode
f2 = FNode -> FNode -> Ordering
forall a. Ord a => a -> a -> Ordering
compare FNode
f1 FNode
f2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
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 :: FNode -> FNode -> Ordering
compare = let gmin :: FNode -> (Goal, String)
gmin f :: FNode
f = ([Goal] -> Goal
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Goal] -> Goal) -> [Goal] -> Goal
forall a b. (a -> b) -> a -> b
$ FNode -> [Goal]
toGtkGoals FNode
f, FNode -> String
name FNode
f)
            in (FNode -> (Goal, String)) -> FNode -> FNode -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing FNode -> (Goal, String)
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 :: [LNode DGNodeLab] -> [FNode]
initFNodes = (LNode DGNodeLab -> [FNode] -> [FNode])
-> [FNode] -> [LNode DGNodeLab] -> [FNode]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ n :: LNode DGNodeLab
n@(_, l :: DGNodeLab
l) t :: [FNode]
t -> case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
l of
                      Nothing -> [FNode]
t
                      Just gt :: G_theory
gt ->
                        let gt' :: G_theory
gt' = DGNodeLab -> G_theory
dgn_theory DGNodeLab
l
                            gs :: [String]
gs = ((String, Maybe BasicProof) -> String)
-> [(String, Maybe BasicProof)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Maybe BasicProof) -> String
forall a b. (a, b) -> a
fst ([(String, Maybe BasicProof)] -> [String])
-> [(String, Maybe BasicProof)] -> [String]
forall a b. (a -> b) -> a -> b
$ G_theory -> [(String, Maybe BasicProof)]
getThGoals G_theory
gt'
                        in if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
gs then [FNode]
t else
                        String
-> LNode DGNodeLab -> G_sublogics -> [String] -> G_theory -> FNode
FNode (DGNodeLab -> String
getDGNodeName DGNodeLab
l) LNode DGNodeLab
n (G_theory -> G_sublogics
sublogicOfTh G_theory
gt) [String]
gs G_theory
gt' FNode -> [FNode] -> [FNode]
forall a. a -> [a] -> [a]
: [FNode]
t
              ) []

-- | returns True if a node has not been proved jet
unchecked :: FNode -> Bool
unchecked :: FNode -> Bool
unchecked fn :: FNode
fn = ((String, Maybe BasicProof) -> Bool)
-> [(String, Maybe BasicProof)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe BasicProof -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe BasicProof -> Bool)
-> ((String, Maybe BasicProof) -> Maybe BasicProof)
-> (String, Maybe BasicProof)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Maybe BasicProof) -> Maybe BasicProof
forall a b. (a, b) -> b
snd) ([(String, Maybe BasicProof)] -> Bool)
-> (G_theory -> [(String, Maybe BasicProof)]) -> G_theory -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_theory -> [(String, Maybe BasicProof)]
getThGoals (G_theory -> Bool) -> G_theory -> Bool
forall a b. (a -> b) -> a -> b
$ FNode -> G_theory
results FNode
fn

-- | returns True if at least one goal has been timed out
timedout :: FNode -> Bool
timedout :: FNode -> Bool
timedout fn :: FNode
fn = (Goal -> Bool) -> [Goal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a :: Goal
a -> Goal -> GStatus
gStatus Goal
a GStatus -> GStatus -> Bool
forall a. Eq a => a -> a -> Bool
== GStatus
GTimeout) ([Goal] -> Bool) -> [Goal] -> Bool
forall a b. (a -> b) -> a -> b
$ FNode -> [Goal]
toGtkGoals FNode
fn

-- | returns True only if every goal has been proved
allProved :: FNode -> Bool
allProved :: FNode -> Bool
allProved fn :: FNode
fn = (Goal -> Bool) -> [Goal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ a :: Goal
a -> Goal -> GStatus
gStatus Goal
a GStatus -> GStatus -> Bool
forall a. Eq a => a -> a -> Bool
== GStatus
GProved) ([Goal] -> Bool) -> [Goal] -> Bool
forall a b. (a -> b) -> a -> b
$ FNode -> [Goal]
toGtkGoals FNode
fn