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

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Datatype for storing of the proof tree
-}

module Common.ProofTree where

import Data.Data

{- |
  Datatype for storing of the proof tree. The Show class is instantiated.
-}
data ProofTree = ProofTree String 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, Eq ProofTree
Eq ProofTree =>
(ProofTree -> ProofTree -> Ordering)
-> (ProofTree -> ProofTree -> Bool)
-> (ProofTree -> ProofTree -> Bool)
-> (ProofTree -> ProofTree -> Bool)
-> (ProofTree -> ProofTree -> Bool)
-> (ProofTree -> ProofTree -> ProofTree)
-> (ProofTree -> ProofTree -> ProofTree)
-> Ord ProofTree
ProofTree -> ProofTree -> Bool
ProofTree -> ProofTree -> Ordering
ProofTree -> ProofTree -> ProofTree
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ProofTree -> ProofTree -> ProofTree
$cmin :: ProofTree -> ProofTree -> ProofTree
max :: ProofTree -> ProofTree -> ProofTree
$cmax :: ProofTree -> ProofTree -> ProofTree
>= :: ProofTree -> ProofTree -> Bool
$c>= :: ProofTree -> ProofTree -> Bool
> :: ProofTree -> ProofTree -> Bool
$c> :: ProofTree -> ProofTree -> Bool
<= :: ProofTree -> ProofTree -> Bool
$c<= :: ProofTree -> ProofTree -> Bool
< :: ProofTree -> ProofTree -> Bool
$c< :: ProofTree -> ProofTree -> Bool
compare :: ProofTree -> ProofTree -> Ordering
$ccompare :: ProofTree -> ProofTree -> Ordering
$cp1Ord :: Eq ProofTree
Ord, Typeable, Typeable ProofTree
Constr
DataType
Typeable ProofTree =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProofTree -> c ProofTree)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProofTree)
-> (ProofTree -> Constr)
-> (ProofTree -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProofTree))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTree))
-> ((forall b. Data b => b -> b) -> ProofTree -> ProofTree)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofTree -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofTree -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProofTree -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProofTree -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProofTree -> m ProofTree)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofTree -> m ProofTree)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofTree -> m ProofTree)
-> Data ProofTree
ProofTree -> Constr
ProofTree -> DataType
(forall b. Data b => b -> b) -> ProofTree -> ProofTree
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTree -> c ProofTree
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTree
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProofTree -> u
forall u. (forall d. Data d => d -> u) -> ProofTree -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTree -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTree -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTree
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTree -> c ProofTree
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofTree)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTree)
$cProofTree :: Constr
$tProofTree :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
gmapMp :: (forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
gmapM :: (forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofTree -> m ProofTree
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofTree -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProofTree -> u
gmapQ :: (forall d. Data d => d -> u) -> ProofTree -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProofTree -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTree -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTree -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTree -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofTree -> r
gmapT :: (forall b. Data b => b -> b) -> ProofTree -> ProofTree
$cgmapT :: (forall b. Data b => b -> b) -> ProofTree -> ProofTree
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTree)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofTree)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProofTree)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofTree)
dataTypeOf :: ProofTree -> DataType
$cdataTypeOf :: ProofTree -> DataType
toConstr :: ProofTree -> Constr
$ctoConstr :: ProofTree -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTree
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofTree
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTree -> c ProofTree
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofTree -> c ProofTree
$cp1Data :: Typeable ProofTree
Data)

instance Show ProofTree where
  show :: ProofTree -> String
show (ProofTree st :: String
st) = String
st

emptyProofTree :: ProofTree
emptyProofTree :: ProofTree
emptyProofTree = String -> ProofTree
ProofTree ""