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
data FNode = FNode { FNode -> String
name :: String
, FNode -> LNode DGNodeLab
node :: LNode DGNodeLab
, FNode -> G_sublogics
sublogic :: G_sublogics
, FNode -> [String]
goals :: [String]
, FNode -> G_theory
results :: G_theory }
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
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]
++ "] "
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
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
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
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
) []
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
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
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