{- | 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