{-# LANGUAGE DeriveDataTypeable, FlexibleInstances #-}
{- |
Module      :  ./Common/ProofTree.hs
Description :  a simple proof tree
Copyright   :  (c) DFKI GmbH, Uni Bremen 2002-2008, Tom Kranz 2021-2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via DeriveDataTypeable, FlexibleInstances)

Datatype for storing of the proof tree.
  Actual proof tree (dag) structures can be printed as dot (Graphviz) digraphs.
-}

module Common.ProofTree ( ProofTree(ProofTree,ProofGraph)
                        , ProofGraphNode
                        , emptyProofTree
                        ) where

import Data.Data
import Data.List (intercalate)
import Data.Graph.Inductive.PatriciaTree (Gr)
import Data.Graph.Inductive.Graph
import ATerm.Lib

import Text.Printf

-- This should be
-- data ProofgraphNode = ProofGraphInference String | ProofGraphSentence String String
-- but ShATermConvertible doens't like to be instantiated this way.
type ProofGraphNode = Either String (String,String)
data ProofTree = ProofTree String | ProofGraph (Gr ProofGraphNode Int) deriving (ProofTree -> ProofTree -> Bool
(ProofTree -> ProofTree -> Bool)
-> (ProofTree -> ProofTree -> Bool) -> Eq ProofTree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofTree -> ProofTree -> Bool
$c/= :: ProofTree -> ProofTree -> Bool
== :: ProofTree -> ProofTree -> Bool
$c== :: ProofTree -> ProofTree -> Bool
Eq, Typeable)

instance Ord ProofTree where
  compare :: ProofTree -> ProofTree -> Ordering
compare (ProofTree _) (ProofGraph _) = Ordering
LT
  compare (ProofGraph _) (ProofTree _) = Ordering
GT
  compare (ProofTree s :: String
s) (ProofTree s' :: String
s') = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare String
s String
s'
  compare (ProofGraph g :: Gr ProofGraphNode Int
g) (ProofGraph g' :: Gr ProofGraphNode Int
g') = OrdGr Gr ProofGraphNode Int
-> OrdGr Gr ProofGraphNode Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Gr ProofGraphNode Int -> OrdGr Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b. gr a b -> OrdGr gr a b
OrdGr Gr ProofGraphNode Int
g) (Gr ProofGraphNode Int -> OrdGr Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b. gr a b -> OrdGr gr a b
OrdGr Gr ProofGraphNode Int
g')

instance ShATermConvertible (Gr ProofGraphNode Int) where
  toShATermAux :: ATermTable -> Gr ProofGraphNode Int -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Gr ProofGraphNode Int
xv = do
    (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable
-> ([LNode ProofGraphNode], [LEdge Int]) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 (Gr ProofGraphNode Int -> [LNode ProofGraphNode]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr ProofGraphNode Int
xv, Gr ProofGraphNode Int -> [LEdge Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr ProofGraphNode Int
xv)
    (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "PatriciaTree.Gr" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Gr ProofGraphNode Int)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PatriciaTree.Gr" [a :: Int
a] _ ->
      case Int
-> ATermTable
-> (ATermTable, ([LNode ProofGraphNode], [LEdge Int]))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, (aNodes :: [LNode ProofGraphNode]
aNodes,aEdges :: [LEdge Int]
aEdges)) ->
      (ATermTable
att1, [LNode ProofGraphNode] -> [LEdge Int] -> Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [LNode ProofGraphNode]
aNodes [LEdge Int]
aEdges) }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Gr ProofGraphNode Int)
forall a. String -> ShATerm -> a
fromShATermError "PatriciaTree.Gr" ShATerm
u

instance Show ProofTree where
  show :: ProofTree -> String
show (ProofTree st :: String
st) = String
st
  -- This is a dot graph description
  show (ProofGraph gr :: Gr ProofGraphNode Int
gr) =
    "digraph {\n"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LNode ProofGraphNode -> String)
-> [LNode ProofGraphNode] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LNode ProofGraphNode -> String
dotNode (Gr ProofGraphNode Int -> [LNode ProofGraphNode]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr ProofGraphNode Int
gr)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LEdge Int -> String) -> [LEdge Int] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LEdge Int -> String
dotEdge (Gr ProofGraphNode Int -> [LEdge Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr ProofGraphNode Int
gr)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
dotSubgraph (Gr ProofGraphNode Int -> [Int]
forall (g :: * -> * -> *) a b. Graph g => g a b -> [Int]
axiomInferences Gr ProofGraphNode Int
gr)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
dotSubgraph (Gr ProofGraphNode Int -> [Int]
forall (g :: * -> * -> *) a b. Graph g => g a b -> [Int]
axiomSentences Gr ProofGraphNode Int
gr)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "}\n"
      where
        dotNode :: LNode ProofGraphNode -> String
        dotNode :: LNode ProofGraphNode -> String
dotNode (i :: Int
i,l :: ProofGraphNode
l) = (String -> Int -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf :: String -> Int -> String -> String -> String -> String) "%d [shape=%s,tooltip=\"%s\",label=\"%s\"];\n" Int
i (ProofGraphNode -> String
nShape ProofGraphNode
l) (ProofGraphNode -> String
xShow ProofGraphNode
l) (ProofGraphNode -> String
lShow ProofGraphNode
l)
        dotEdge :: LEdge Int -> String
        dotEdge :: LEdge Int -> String
dotEdge (s :: Int
s,t :: Int
t,i :: Int
i) = (String -> Int -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf :: String -> Int -> Int -> Int -> String) "%d -> %d [label=\"%d\"];\n" Int
s Int
t Int
i
        dotSubgraph :: [Node] -> String
        dotSubgraph :: [Int] -> String
dotSubgraph [] = ""
        dotSubgraph ns :: [Int]
ns = (String -> ShowS
forall r. PrintfType r => String -> r
printf :: String -> String -> String) "subgraph { rank = same; %s }\n" (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "; " ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [Int]
ns))
        axiomInferences :: Graph g => g a b -> [Node]
        axiomInferences :: g a b -> [Int]
axiomInferences g :: g a b
g = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==0)(Int -> Bool) -> (Int -> Int) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.g a b -> Int -> Int
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> Int
indeg g a b
g) (g a b -> [Int]
forall (g :: * -> * -> *) a b. Graph g => g a b -> [Int]
nodes g a b
g)
        axiomSentences :: Graph g => g a b -> [Node]
        axiomSentences :: g a b -> [Int]
axiomSentences g :: g a b
g = (Int -> [Int]) -> [Int] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (g a b -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
suc g a b
g) (g a b -> [Int]
forall (g :: * -> * -> *) a b. Graph g => g a b -> [Int]
axiomInferences g a b
g)
        escape :: String -> String
        escape :: ShowS
escape = (Char -> String) -> ShowS
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\c :: Char
c->(if Char
cChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
=='"' Bool -> Bool -> Bool
|| Char
cChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
=='\\' then "\\" else [])String -> ShowS
forall a. [a] -> [a] -> [a]
++[Char
c])
        lString :: ProofGraphNode -> String
        lString :: ProofGraphNode -> String
lString (Left s :: String
s) = String
s
        lString (Right (s :: String
s,_)) = String
s
        lShow :: ProofGraphNode -> String
        lShow :: ProofGraphNode -> String
lShow = ShowS
escapeShowS -> (ProofGraphNode -> String) -> ProofGraphNode -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ProofGraphNode -> String
lString
        xString :: ProofGraphNode -> String
        xString :: ProofGraphNode -> String
xString (Left _) = ""
        xString (Right (_,s :: String
s)) = String
s
        xShow :: ProofGraphNode -> String
        xShow :: ProofGraphNode -> String
xShow = ShowS
escapeShowS -> (ProofGraphNode -> String) -> ProofGraphNode -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ProofGraphNode -> String
xString
        nShape :: ProofGraphNode -> String
        nShape :: ProofGraphNode -> String
nShape (Left _) = "box"
        nShape (Right _) = "oval"

emptyProofTree :: ProofTree
emptyProofTree :: ProofTree
emptyProofTree = Gr ProofGraphNode Int -> ProofTree
ProofGraph Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
empty