Copyright	(c) DFKI GmbH 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Static.DgUtils

Contents

node label types
edge types
datatypes for storing the nodes of the ref tree in the global env
- for node names
- handle edge numbers and proof bases
utilities

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 getName :: IRI extString :: String extIndex :: Int xpath :: [XPathPart] srcRange :: Range

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 #

isInternal :: NodeName -> Bool Source #

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

test if a conservativity is open, return input for None

data DGNodeType Source #

Constructors

DGNodeType
Fields isRefType :: Bool isProvenNode :: Bool isProvenCons :: Bool isInternalSpec :: Bool

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 #
Methods compare :: DGNodeType -> DGNodeType -> Ordering (<) :: DGNodeType -> DGNodeType -> Bool (<=) :: DGNodeType -> DGNodeType -> Bool (>) :: DGNodeType -> DGNodeType -> Bool (>=) :: DGNodeType -> DGNodeType -> Bool max :: DGNodeType -> DGNodeType -> DGNodeType min :: DGNodeType -> DGNodeType -> DGNodeType
Show DGNodeType Source #
Methods showsPrec :: Int -> DGNodeType -> ShowS show :: DGNodeType -> String showList :: [DGNodeType] -> ShowS

listDGNodeTypes :: [DGNodeType] Source #

data NodeMod Source #

node modifications

Constructors

NodeMod
Fields delAx :: Bool delTh :: Bool addSen :: Bool delSym :: Bool addSym :: Bool

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

delAxMod :: NodeMod Source #

delThMod :: NodeMod Source #

delSenMod :: NodeMod Source #

addSenMod :: NodeMod Source #

senMod :: NodeMod Source #

delSymMod :: NodeMod Source #

addSymMod :: NodeMod Source #

symMod :: NodeMod Source #

mergeNodeMod :: NodeMod -> NodeMod -> NodeMod Source #

edge types

newtype EdgeId Source #

unique number for edges

Constructors

EdgeId
Fields getEdgeNum :: Int

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 proofBasis :: Set EdgeId

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 #
Methods compare :: ProofBasis -> ProofBasis -> Ordering (<) :: ProofBasis -> ProofBasis -> Bool (<=) :: ProofBasis -> ProofBasis -> Bool (>) :: ProofBasis -> ProofBasis -> Bool (>=) :: ProofBasis -> ProofBasis -> Bool max :: ProofBasis -> ProofBasis -> ProofBasis min :: ProofBasis -> ProofBasis -> ProofBasis
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

Constructors

LeftOpen
Proven DGRule ProofBasis

Instances

Eq ThmLinkStatus Source #
Methods (==) :: ThmLinkStatus -> ThmLinkStatus -> Bool (/=) :: ThmLinkStatus -> ThmLinkStatus -> Bool
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 #
Methods compare :: ThmLinkStatus -> ThmLinkStatus -> Ordering (<) :: ThmLinkStatus -> ThmLinkStatus -> Bool (<=) :: ThmLinkStatus -> ThmLinkStatus -> Bool (>) :: ThmLinkStatus -> ThmLinkStatus -> Bool (>=) :: ThmLinkStatus -> ThmLinkStatus -> Bool max :: ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus min :: ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus
Show ThmLinkStatus Source #
Methods showsPrec :: Int -> ThmLinkStatus -> ShowS show :: ThmLinkStatus -> String showList :: [ThmLinkStatus] -> ShowS

isProvenThmLinkStatus :: ThmLinkStatus -> Bool Source #

proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis Source #

updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus Source #

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 #

Constructors

DefLink
ThmLink ThmLinkStatus

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 #
Methods minBound :: FreeOrCofree maxBound :: FreeOrCofree
Enum FreeOrCofree Source #
Methods succ :: FreeOrCofree -> FreeOrCofree pred :: FreeOrCofree -> FreeOrCofree toEnum :: Int -> FreeOrCofree fromEnum :: FreeOrCofree -> Int enumFrom :: FreeOrCofree -> [FreeOrCofree] enumFromThen :: FreeOrCofree -> FreeOrCofree -> [FreeOrCofree] enumFromTo :: FreeOrCofree -> FreeOrCofree -> [FreeOrCofree] enumFromThenTo :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
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 #
Methods compare :: FreeOrCofree -> FreeOrCofree -> Ordering (<) :: FreeOrCofree -> FreeOrCofree -> Bool (<=) :: FreeOrCofree -> FreeOrCofree -> Bool (>) :: FreeOrCofree -> FreeOrCofree -> Bool (>=) :: FreeOrCofree -> FreeOrCofree -> Bool max :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree min :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree
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

fcList :: [FreeOrCofree] Source #

data ConsStatus Source #

required and proven conservativity (with a proof)

Constructors

ConsStatus Conservativity Conservativity ThmLinkStatus

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 #
Methods compare :: ConsStatus -> ConsStatus -> Ordering (<) :: ConsStatus -> ConsStatus -> Bool (<=) :: ConsStatus -> ConsStatus -> Bool (>) :: ConsStatus -> ConsStatus -> Bool (>=) :: ConsStatus -> ConsStatus -> Bool max :: ConsStatus -> ConsStatus -> ConsStatus min :: ConsStatus -> ConsStatus -> ConsStatus
Show ConsStatus Source #
Methods showsPrec :: Int -> ConsStatus -> ShowS show :: ConsStatus -> String showList :: [ConsStatus] -> ShowS

isProvenConsStatusLink :: ConsStatus -> Bool Source #

mkConsStatus :: Conservativity -> ConsStatus Source #

getConsOfStatus :: ConsStatus -> Conservativity Source #

showConsStatus :: ConsStatus -> String Source #

to be displayed as edge label

getDGEdgeTypeName :: DGEdgeType -> String Source #

converts a DGEdgeType to a String

revertDGEdgeTypeName :: String -> DGEdgeType Source #

getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String Source #

data DGEdgeType Source #

Constructors

DGEdgeType
Fields edgeTypeModInc :: DGEdgeTypeModInc isInc :: Bool

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 #
Methods compare :: DGEdgeType -> DGEdgeType -> Ordering (<) :: DGEdgeType -> DGEdgeType -> Bool (<=) :: DGEdgeType -> DGEdgeType -> Bool (>) :: DGEdgeType -> DGEdgeType -> Bool (>=) :: DGEdgeType -> DGEdgeType -> Bool max :: DGEdgeType -> DGEdgeType -> DGEdgeType min :: DGEdgeType -> DGEdgeType -> DGEdgeType
Show DGEdgeType Source #
Methods showsPrec :: Int -> DGEdgeType -> ShowS show :: DGEdgeType -> String showList :: [DGEdgeType] -> ShowS

data DGEdgeTypeModInc Source #

Constructors

GlobalDef
HetDef
HidingDef
LocalDef
FreeOrCofreeDef FreeOrCofree
ThmType
Fields thmEdgeType :: ThmTypes isProvenEdge :: Bool isConservativ :: Bool isPending :: Bool

Instances

Eq DGEdgeTypeModInc Source #
Methods (==) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool (/=) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
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 #
Methods compare :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Ordering (<) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool (<=) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool (>) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool (>=) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool max :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc min :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc
Show DGEdgeTypeModInc Source #
Methods showsPrec :: Int -> DGEdgeTypeModInc -> ShowS show :: DGEdgeTypeModInc -> String showList :: [DGEdgeTypeModInc] -> ShowS

data ThmTypes Source #

Constructors

HidingThm
FreeOrCofreeThm FreeOrCofree
GlobalOrLocalThm
Fields thmScope :: Scope isHomThm :: Bool

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 #

compPointer :: RTPointer -> RTPointer -> RTPointer Source #

refSource :: RTPointer -> Int 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