Hets - the Heterogeneous Tool Set

Copyright(c) DFKI GmbH 2011
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Static.DgUtils

Contents

Description

 

Synopsis

node label types

data XPathPart Source #

Constructors

ElemName String 
ChildIndex Int 

Instances

Data XPathPart Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> XPathPart -> c XPathPart

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c XPathPart

toConstr :: XPathPart -> Constr

dataTypeOf :: XPathPart -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c XPathPart)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XPathPart)

gmapT :: (forall b. Data b => b -> b) -> XPathPart -> XPathPart

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XPathPart -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XPathPart -> r

gmapQ :: (forall d. Data d => d -> u) -> XPathPart -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> XPathPart -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart

Show XPathPart Source # 

Methods

showsPrec :: Int -> XPathPart -> ShowS

show :: XPathPart -> String

showList :: [XPathPart] -> ShowS

data NodeName Source #

name of a node in a DG; auxiliary nodes may have extension string and non-zero number (for these, names are usually hidden).

Constructors

NodeName 

Fields

Instances

Eq NodeName Source # 

Methods

(==) :: NodeName -> NodeName -> Bool

(/=) :: NodeName -> NodeName -> Bool

Data NodeName Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NodeName -> c NodeName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NodeName

toConstr :: NodeName -> Constr

dataTypeOf :: NodeName -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c NodeName)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeName)

gmapT :: (forall b. Data b => b -> b) -> NodeName -> NodeName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NodeName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NodeName -> r

gmapQ :: (forall d. Data d => d -> u) -> NodeName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NodeName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NodeName -> m NodeName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NodeName -> m NodeName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NodeName -> m NodeName

Ord NodeName Source # 

Methods

compare :: NodeName -> NodeName -> Ordering

(<) :: NodeName -> NodeName -> Bool

(<=) :: NodeName -> NodeName -> Bool

(>) :: NodeName -> NodeName -> Bool

(>=) :: NodeName -> NodeName -> Bool

max :: NodeName -> NodeName -> NodeName

min :: NodeName -> NodeName -> NodeName

Show NodeName Source # 

Methods

showsPrec :: Int -> NodeName -> ShowS

show :: NodeName -> String

showList :: [NodeName] -> ShowS

readXPath :: Monad m => String -> m [XPathPart] Source #

readXPathComp :: Monad m => String -> m XPathPart Source #

hasOpenConsStatus :: Bool -> ConsStatus -> Bool Source #

test if a conservativity is open, return input for None

data DGNodeType Source #

Constructors

DGNodeType 

Fields

Instances

Eq DGNodeType Source # 

Methods

(==) :: DGNodeType -> DGNodeType -> Bool

(/=) :: DGNodeType -> DGNodeType -> Bool

Data DGNodeType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DGNodeType -> c DGNodeType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DGNodeType

toConstr :: DGNodeType -> Constr

dataTypeOf :: DGNodeType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DGNodeType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGNodeType)

gmapT :: (forall b. Data b => b -> b) -> DGNodeType -> DGNodeType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGNodeType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGNodeType -> r

gmapQ :: (forall d. Data d => d -> u) -> DGNodeType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DGNodeType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType

Ord DGNodeType Source # 
Show DGNodeType Source # 

Methods

showsPrec :: Int -> DGNodeType -> ShowS

show :: DGNodeType -> String

showList :: [DGNodeType] -> ShowS

data NodeMod Source #

node modifications

Constructors

NodeMod 

Fields

Instances

Eq NodeMod Source # 

Methods

(==) :: NodeMod -> NodeMod -> Bool

(/=) :: NodeMod -> NodeMod -> Bool

Data NodeMod Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NodeMod -> c NodeMod

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NodeMod

toConstr :: NodeMod -> Constr

dataTypeOf :: NodeMod -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c NodeMod)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeMod)

gmapT :: (forall b. Data b => b -> b) -> NodeMod -> NodeMod

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NodeMod -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NodeMod -> r

gmapQ :: (forall d. Data d => d -> u) -> NodeMod -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NodeMod -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod

Ord NodeMod Source # 

Methods

compare :: NodeMod -> NodeMod -> Ordering

(<) :: NodeMod -> NodeMod -> Bool

(<=) :: NodeMod -> NodeMod -> Bool

(>) :: NodeMod -> NodeMod -> Bool

(>=) :: NodeMod -> NodeMod -> Bool

max :: NodeMod -> NodeMod -> NodeMod

min :: NodeMod -> NodeMod -> NodeMod

Show NodeMod Source # 

Methods

showsPrec :: Int -> NodeMod -> ShowS

show :: NodeMod -> String

showList :: [NodeMod] -> ShowS

unMod :: NodeMod Source #

an unmodified node

edge types

newtype EdgeId Source #

unique number for edges

Constructors

EdgeId 

Fields

Instances

Eq EdgeId Source # 

Methods

(==) :: EdgeId -> EdgeId -> Bool

(/=) :: EdgeId -> EdgeId -> Bool

Data EdgeId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EdgeId -> c EdgeId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EdgeId

toConstr :: EdgeId -> Constr

dataTypeOf :: EdgeId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c EdgeId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EdgeId)

gmapT :: (forall b. Data b => b -> b) -> EdgeId -> EdgeId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r

gmapQ :: (forall d. Data d => d -> u) -> EdgeId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EdgeId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId

Ord EdgeId Source # 

Methods

compare :: EdgeId -> EdgeId -> Ordering

(<) :: EdgeId -> EdgeId -> Bool

(<=) :: EdgeId -> EdgeId -> Bool

(>) :: EdgeId -> EdgeId -> Bool

(>=) :: EdgeId -> EdgeId -> Bool

max :: EdgeId -> EdgeId -> EdgeId

min :: EdgeId -> EdgeId -> EdgeId

Show EdgeId Source # 

Methods

showsPrec :: Int -> EdgeId -> ShowS

show :: EdgeId -> String

showList :: [EdgeId] -> ShowS

incEdgeId :: EdgeId -> EdgeId Source #

next edge id

startEdgeId :: EdgeId Source #

the first edge in a graph

showEdgeId :: EdgeId -> String Source #

newtype ProofBasis Source #

a set of used edges

Constructors

ProofBasis 

Fields

Instances

Eq ProofBasis Source # 

Methods

(==) :: ProofBasis -> ProofBasis -> Bool

(/=) :: ProofBasis -> ProofBasis -> Bool

Data ProofBasis Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofBasis -> c ProofBasis

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofBasis

toConstr :: ProofBasis -> Constr

dataTypeOf :: ProofBasis -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ProofBasis)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofBasis)

gmapT :: (forall b. Data b => b -> b) -> ProofBasis -> ProofBasis

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofBasis -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofBasis -> r

gmapQ :: (forall d. Data d => d -> u) -> ProofBasis -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofBasis -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis

Ord ProofBasis Source # 
Show ProofBasis Source # 

Methods

showsPrec :: Int -> ProofBasis -> ShowS

show :: ProofBasis -> String

showList :: [ProofBasis] -> ShowS

data DGRule Source #

Rules in the development graph calculus, Sect. IV:4.4 of the CASL Reference Manual explains them in depth

Constructors

DGRule String 
DGRuleWithEdge String EdgeId 
DGRuleLocalInference [(String, String)] 
Composition [EdgeId] 

Instances

Eq DGRule Source # 

Methods

(==) :: DGRule -> DGRule -> Bool

(/=) :: DGRule -> DGRule -> Bool

Data DGRule Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DGRule -> c DGRule

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DGRule

toConstr :: DGRule -> Constr

dataTypeOf :: DGRule -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DGRule)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGRule)

gmapT :: (forall b. Data b => b -> b) -> DGRule -> DGRule

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r

gmapQ :: (forall d. Data d => d -> u) -> DGRule -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DGRule -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DGRule -> m DGRule

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DGRule -> m DGRule

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DGRule -> m DGRule

Ord DGRule Source # 

Methods

compare :: DGRule -> DGRule -> Ordering

(<) :: DGRule -> DGRule -> Bool

(<=) :: DGRule -> DGRule -> Bool

(>) :: DGRule -> DGRule -> Bool

(>=) :: DGRule -> DGRule -> Bool

max :: DGRule -> DGRule -> DGRule

min :: DGRule -> DGRule -> DGRule

Show DGRule Source # 

Methods

showsPrec :: Int -> DGRule -> ShowS

show :: DGRule -> String

showList :: [DGRule] -> ShowS

data ThmLinkStatus Source #

proof status of a link

Instances

Eq ThmLinkStatus Source # 
Data ThmLinkStatus Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThmLinkStatus -> c ThmLinkStatus

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ThmLinkStatus

toConstr :: ThmLinkStatus -> Constr

dataTypeOf :: ThmLinkStatus -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ThmLinkStatus)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ThmLinkStatus)

gmapT :: (forall b. Data b => b -> b) -> ThmLinkStatus -> ThmLinkStatus

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r

gmapQ :: (forall d. Data d => d -> u) -> ThmLinkStatus -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThmLinkStatus -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus

Ord ThmLinkStatus Source # 
Show ThmLinkStatus Source # 

Methods

showsPrec :: Int -> ThmLinkStatus -> ShowS

show :: ThmLinkStatus -> String

showList :: [ThmLinkStatus] -> ShowS

data Scope Source #

Constructors

Local 
Global 

Instances

Eq Scope Source # 

Methods

(==) :: Scope -> Scope -> Bool

(/=) :: Scope -> Scope -> Bool

Data Scope Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scope -> c Scope

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Scope

toConstr :: Scope -> Constr

dataTypeOf :: Scope -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Scope)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope)

gmapT :: (forall b. Data b => b -> b) -> Scope -> Scope

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r

gmapQ :: (forall d. Data d => d -> u) -> Scope -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scope -> m Scope

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope -> m Scope

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope -> m Scope

Ord Scope Source # 

Methods

compare :: Scope -> Scope -> Ordering

(<) :: Scope -> Scope -> Bool

(<=) :: Scope -> Scope -> Bool

(>) :: Scope -> Scope -> Bool

(>=) :: Scope -> Scope -> Bool

max :: Scope -> Scope -> Scope

min :: Scope -> Scope -> Scope

Show Scope Source # 

Methods

showsPrec :: Int -> Scope -> ShowS

show :: Scope -> String

showList :: [Scope] -> ShowS

data LinkKind Source #

Instances

Eq LinkKind Source # 

Methods

(==) :: LinkKind -> LinkKind -> Bool

(/=) :: LinkKind -> LinkKind -> Bool

Data LinkKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LinkKind -> c LinkKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LinkKind

toConstr :: LinkKind -> Constr

dataTypeOf :: LinkKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c LinkKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LinkKind)

gmapT :: (forall b. Data b => b -> b) -> LinkKind -> LinkKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LinkKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LinkKind -> r

gmapQ :: (forall d. Data d => d -> u) -> LinkKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LinkKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind

Ord LinkKind Source # 

Methods

compare :: LinkKind -> LinkKind -> Ordering

(<) :: LinkKind -> LinkKind -> Bool

(<=) :: LinkKind -> LinkKind -> Bool

(>) :: LinkKind -> LinkKind -> Bool

(>=) :: LinkKind -> LinkKind -> Bool

max :: LinkKind -> LinkKind -> LinkKind

min :: LinkKind -> LinkKind -> LinkKind

Show LinkKind Source # 

Methods

showsPrec :: Int -> LinkKind -> ShowS

show :: LinkKind -> String

showList :: [LinkKind] -> ShowS

data FreeOrCofree Source #

Constructors

Free 
Cofree 
NPFree 
Minimize 

Instances

Bounded FreeOrCofree Source # 
Enum FreeOrCofree Source # 
Eq FreeOrCofree Source # 

Methods

(==) :: FreeOrCofree -> FreeOrCofree -> Bool

(/=) :: FreeOrCofree -> FreeOrCofree -> Bool

Data FreeOrCofree Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FreeOrCofree -> c FreeOrCofree

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FreeOrCofree

toConstr :: FreeOrCofree -> Constr

dataTypeOf :: FreeOrCofree -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c FreeOrCofree)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FreeOrCofree)

gmapT :: (forall b. Data b => b -> b) -> FreeOrCofree -> FreeOrCofree

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r

gmapQ :: (forall d. Data d => d -> u) -> FreeOrCofree -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FreeOrCofree -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree

Ord FreeOrCofree Source # 
Read FreeOrCofree Source # 

Methods

readsPrec :: Int -> ReadS FreeOrCofree

readList :: ReadS [FreeOrCofree]

readPrec :: ReadPrec FreeOrCofree

readListPrec :: ReadPrec [FreeOrCofree]

Show FreeOrCofree Source # 

Methods

showsPrec :: Int -> FreeOrCofree -> ShowS

show :: FreeOrCofree -> String

showList :: [FreeOrCofree] -> ShowS

data ConsStatus Source #

required and proven conservativity (with a proof)

Instances

Eq ConsStatus Source # 

Methods

(==) :: ConsStatus -> ConsStatus -> Bool

(/=) :: ConsStatus -> ConsStatus -> Bool

Data ConsStatus Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConsStatus -> c ConsStatus

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConsStatus

toConstr :: ConsStatus -> Constr

dataTypeOf :: ConsStatus -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ConsStatus)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConsStatus)

gmapT :: (forall b. Data b => b -> b) -> ConsStatus -> ConsStatus

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConsStatus -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConsStatus -> r

gmapQ :: (forall d. Data d => d -> u) -> ConsStatus -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConsStatus -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus

Ord ConsStatus Source # 
Show ConsStatus Source # 

Methods

showsPrec :: Int -> ConsStatus -> ShowS

show :: ConsStatus -> String

showList :: [ConsStatus] -> ShowS

showConsStatus :: ConsStatus -> String Source #

to be displayed as edge label

getDGEdgeTypeName :: DGEdgeType -> String Source #

converts a DGEdgeType to a String

data DGEdgeType Source #

Constructors

DGEdgeType 

Instances

Eq DGEdgeType Source # 

Methods

(==) :: DGEdgeType -> DGEdgeType -> Bool

(/=) :: DGEdgeType -> DGEdgeType -> Bool

Data DGEdgeType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DGEdgeType -> c DGEdgeType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DGEdgeType

toConstr :: DGEdgeType -> Constr

dataTypeOf :: DGEdgeType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DGEdgeType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGEdgeType)

gmapT :: (forall b. Data b => b -> b) -> DGEdgeType -> DGEdgeType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r

gmapQ :: (forall d. Data d => d -> u) -> DGEdgeType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DGEdgeType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType

Ord DGEdgeType Source # 
Show DGEdgeType Source # 

Methods

showsPrec :: Int -> DGEdgeType -> ShowS

show :: DGEdgeType -> String

showList :: [DGEdgeType] -> ShowS

data DGEdgeTypeModInc Source #

Instances

Eq DGEdgeTypeModInc Source # 
Data DGEdgeTypeModInc Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DGEdgeTypeModInc -> c DGEdgeTypeModInc

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DGEdgeTypeModInc

toConstr :: DGEdgeTypeModInc -> Constr

dataTypeOf :: DGEdgeTypeModInc -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DGEdgeTypeModInc)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGEdgeTypeModInc)

gmapT :: (forall b. Data b => b -> b) -> DGEdgeTypeModInc -> DGEdgeTypeModInc

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r

gmapQ :: (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DGEdgeTypeModInc -> m DGEdgeTypeModInc

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DGEdgeTypeModInc -> m DGEdgeTypeModInc

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DGEdgeTypeModInc -> m DGEdgeTypeModInc

Ord DGEdgeTypeModInc Source # 
Show DGEdgeTypeModInc Source # 

Methods

showsPrec :: Int -> DGEdgeTypeModInc -> ShowS

show :: DGEdgeTypeModInc -> String

showList :: [DGEdgeTypeModInc] -> ShowS

data ThmTypes Source #

Instances

Eq ThmTypes Source # 

Methods

(==) :: ThmTypes -> ThmTypes -> Bool

(/=) :: ThmTypes -> ThmTypes -> Bool

Data ThmTypes Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThmTypes -> c ThmTypes

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ThmTypes

toConstr :: ThmTypes -> Constr

dataTypeOf :: ThmTypes -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ThmTypes)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ThmTypes)

gmapT :: (forall b. Data b => b -> b) -> ThmTypes -> ThmTypes

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThmTypes -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThmTypes -> r

gmapQ :: (forall d. Data d => d -> u) -> ThmTypes -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThmTypes -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes

Ord ThmTypes Source # 

Methods

compare :: ThmTypes -> ThmTypes -> Ordering

(<) :: ThmTypes -> ThmTypes -> Bool

(<=) :: ThmTypes -> ThmTypes -> Bool

(>) :: ThmTypes -> ThmTypes -> Bool

(>=) :: ThmTypes -> ThmTypes -> Bool

max :: ThmTypes -> ThmTypes -> ThmTypes

min :: ThmTypes -> ThmTypes -> ThmTypes

Show ThmTypes Source # 

Methods

showsPrec :: Int -> ThmTypes -> ShowS

show :: ThmTypes -> String

showList :: [ThmTypes] -> ShowS

listDGEdgeTypes :: [DGEdgeType] Source #

Creates a list with all DGEdgeType types

isDefEdgeType :: DGEdgeType -> Bool Source #

check an EdgeType and see if its a definition link

datatypes for storing the nodes of the ref tree in the global env

data RTPointer Source #

Constructors

RTNone 
NPUnit Int 
NPBranch Int (Map IRI RTPointer) 
NPRef Int Int 
NPComp (Map IRI RTPointer) 

Instances

Eq RTPointer Source # 

Methods

(==) :: RTPointer -> RTPointer -> Bool

(/=) :: RTPointer -> RTPointer -> Bool

Data RTPointer Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTPointer -> c RTPointer

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTPointer

toConstr :: RTPointer -> Constr

dataTypeOf :: RTPointer -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c RTPointer)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTPointer)

gmapT :: (forall b. Data b => b -> b) -> RTPointer -> RTPointer

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTPointer -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTPointer -> r

gmapQ :: (forall d. Data d => d -> u) -> RTPointer -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTPointer -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer

Ord RTPointer Source # 

Methods

compare :: RTPointer -> RTPointer -> Ordering

(<) :: RTPointer -> RTPointer -> Bool

(<=) :: RTPointer -> RTPointer -> Bool

(>) :: RTPointer -> RTPointer -> Bool

(>=) :: RTPointer -> RTPointer -> Bool

max :: RTPointer -> RTPointer -> RTPointer

min :: RTPointer -> RTPointer -> RTPointer

Show RTPointer Source # 

Methods

showsPrec :: Int -> RTPointer -> ShowS

show :: RTPointer -> String

showList :: [RTPointer] -> ShowS

mapRTNodes :: Map Int Int -> RTPointer -> RTPointer Source #

data RTLeaves Source #

Constructors

RTLeaf Int 
RTLeaves (Map IRI RTLeaves) 

Instances

Data RTLeaves Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RTLeaves -> c RTLeaves

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RTLeaves

toConstr :: RTLeaves -> Constr

dataTypeOf :: RTLeaves -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c RTLeaves)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTLeaves)

gmapT :: (forall b. Data b => b -> b) -> RTLeaves -> RTLeaves

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RTLeaves -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RTLeaves -> r

gmapQ :: (forall d. Data d => d -> u) -> RTLeaves -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RTLeaves -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves

Show RTLeaves Source # 

Methods

showsPrec :: Int -> RTLeaves -> ShowS

show :: RTLeaves -> String

showList :: [RTLeaves] -> ShowS

for node names

showExt :: NodeName -> String Source #

showName :: NodeName -> String Source #

extName :: String -> NodeName -> NodeName Source #

handle edge numbers and proof bases

defaultEdgeId :: EdgeId Source #

create a default ID which has to be changed when inserting a certain edge.

edgeInProofBasis :: EdgeId -> ProofBasis -> Bool Source #

checks if the given edge is contained in the given proof basis..

utilities

getMapAndMaxIndex :: Ord k => k -> (b -> Map k a) -> b -> (Map k a, k) Source #

liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool Source #

or two predicates