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

data XPathPart
- = ElemName String
- | ChildIndex Int
data NodeName = NodeName {
- getName :: IRI
- extString :: String
- extIndex :: Int
- xpath :: [XPathPart]
- srcRange :: Range
}
readXPath :: MonadFail m => String -> m [XPathPart]
readXPathComp :: MonadFail m => String -> m XPathPart
isInternal :: NodeName -> Bool
hasOpenConsStatus :: Bool -> ConsStatus -> Bool
data DGNodeType = DGNodeType {
- isRefType :: Bool
- isProvenNode :: Bool
- isProvenCons :: Bool
- isInternalSpec :: Bool
}
listDGNodeTypes :: [DGNodeType]
data NodeMod = NodeMod {
- delAx :: Bool
- delTh :: Bool
- addSen :: Bool
- delSym :: Bool
- addSym :: Bool
}
unMod :: NodeMod
delAxMod :: NodeMod
delThMod :: NodeMod
delSenMod :: NodeMod
addSenMod :: NodeMod
senMod :: NodeMod
delSymMod :: NodeMod
addSymMod :: NodeMod
symMod :: NodeMod
mergeNodeMod :: NodeMod -> NodeMod -> NodeMod
newtype EdgeId = EdgeId {
- getEdgeNum :: Int
}
incEdgeId :: EdgeId -> EdgeId
startEdgeId :: EdgeId
showEdgeId :: EdgeId -> String
newtype ProofBasis = ProofBasis {
- proofBasis :: Set EdgeId
}
data DGRule
- = DGRule String
- | DGRuleWithEdge String EdgeId
- | DGRuleLocalInference [(String, String)]
- | Composition [EdgeId]
data ThmLinkStatus
- = LeftOpen
- | Proven DGRule ProofBasis
isProvenThmLinkStatus :: ThmLinkStatus -> Bool
proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
data Scope
- = Local
- | Global
data LinkKind
- = DefLink
- | ThmLink ThmLinkStatus
data FreeOrCofree
- = Free
- | Cofree
- | NPFree
- | Minimize
fcList :: [FreeOrCofree]
data ConsStatus = ConsStatus {
- requiredConservativity :: Conservativity
- provenConservativity :: Conservativity
- linkStatus :: ThmLinkStatus
}
isProvenConsStatusLink :: ConsStatus -> Bool
mkConsStatus :: Conservativity -> ConsStatus
getConsOfStatus :: ConsStatus -> Conservativity
showConsStatus :: ConsStatus -> String
getDGEdgeTypeName :: DGEdgeType -> String
revertDGEdgeTypeName :: String -> DGEdgeType
getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String
data DGEdgeType = DGEdgeType {
- edgeTypeModInc :: DGEdgeTypeModInc
- isInc :: Bool
}
data DGEdgeTypeModInc
- = GlobalDef
- | HetDef
- | HidingDef
- | LocalDef
- | FreeOrCofreeDef FreeOrCofree
- | ThmType {
  - thmEdgeType :: ThmTypes
  - isProvenEdge :: Bool
  - isConservativ :: Bool
  - isPending :: Bool
  }
data ThmTypes
- = HidingThm
- | FreeOrCofreeThm FreeOrCofree
- | GlobalOrLocalThm {
  - thmScope :: Scope
  - isHomThm :: Bool
  }
listDGEdgeTypes :: [DGEdgeType]
isDefEdgeType :: DGEdgeType -> Bool
data RTPointer
- = RTNone
- | NPUnit Int
- | NPBranch Int (Map IRI RTPointer)
- | NPRef Int Int
- | NPComp (Map IRI RTPointer)
mapRTNodes :: Map Int Int -> RTPointer -> RTPointer
compPointer :: RTPointer -> RTPointer -> RTPointer
refSource :: RTPointer -> Int
data RTLeaves
- = RTLeaf Int
- | RTLeaves (Map IRI RTLeaves)
refTarget :: RTPointer -> RTLeaves
emptyNodeName :: NodeName
showExt :: NodeName -> String
showName :: NodeName -> String
makeRgName :: IRI -> Range -> NodeName
makeName :: IRI -> NodeName
setSrcRange :: Range -> NodeName -> NodeName
parseNodeName :: String -> NodeName
incBy :: Int -> NodeName -> NodeName
inc :: NodeName -> NodeName
extName :: String -> NodeName -> NodeName
defaultEdgeId :: EdgeId
emptyProofBasis :: ProofBasis
nullProofBasis :: ProofBasis -> Bool
addEdgeId :: ProofBasis -> EdgeId -> ProofBasis
delEdgeId :: ProofBasis -> EdgeId -> ProofBasis
updEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis
edgeInProofBasis :: EdgeId -> ProofBasis -> Bool
topsortedLibsWithImports :: Rel LibName -> [LibName]
getMapAndMaxIndex :: Ord k => k -> (b -> Map k a) -> b -> (Map k a, k)
liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool

node label types

data XPathPart Source #

Constructors

ElemName String
ChildIndex Int

Instances

Instances details

Data XPathPart Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> XPathPart -> ShowS show :: XPathPart -> String showList :: [XPathPart] -> ShowS
ShATermLG XPathPart Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> XPathPart -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, XPathPart) Source #

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

Instances details

Eq NodeName Source #
Instance details Defined in Static.DgUtils Methods (==) :: NodeName -> NodeName -> Bool (/=) :: NodeName -> NodeName -> Bool
Data NodeName Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> NodeName -> ShowS show :: NodeName -> String showList :: [NodeName] -> ShowS
Pretty NodeName Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: NodeName -> Doc Source # pretties :: [NodeName] -> Doc Source #
ShATermLG NodeName Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> NodeName -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, NodeName) Source #

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

readXPathComp :: MonadFail 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

Instances details

Eq DGNodeType Source #
Instance details Defined in Static.DgUtils Methods (==) :: DGNodeType -> DGNodeType -> Bool (/=) :: DGNodeType -> DGNodeType -> Bool
Data DGNodeType Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> DGNodeType -> ShowS show :: DGNodeType -> String showList :: [DGNodeType] -> ShowS
ShATermLG DGNodeType Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> DGNodeType -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeType) Source #

listDGNodeTypes :: [DGNodeType] Source #

data NodeMod Source #

node modifications

Constructors

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

Instances

Instances details

Eq NodeMod Source #
Instance details Defined in Static.DgUtils Methods (==) :: NodeMod -> NodeMod -> Bool (/=) :: NodeMod -> NodeMod -> Bool
Data NodeMod Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> NodeMod -> ShowS show :: NodeMod -> String showList :: [NodeMod] -> ShowS
ShATermLG NodeMod Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> NodeMod -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, NodeMod) Source #

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

Instances details

Eq EdgeId Source #
Instance details Defined in Static.DgUtils Methods (==) :: EdgeId -> EdgeId -> Bool (/=) :: EdgeId -> EdgeId -> Bool
Data EdgeId Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> EdgeId -> ShowS show :: EdgeId -> String showList :: [EdgeId] -> ShowS
Pretty EdgeId Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: EdgeId -> Doc Source # pretties :: [EdgeId] -> Doc Source #
ShATermLG EdgeId Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> EdgeId -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, EdgeId) Source #
Eq (DaVinciArc EdgeValue)
Instance details Defined in GUI.GraphAbstraction Methods (==) :: DaVinciArc EdgeValue -> DaVinciArc EdgeValue -> Bool (/=) :: DaVinciArc EdgeValue -> DaVinciArc EdgeValue -> Bool

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

Instances details

Eq ProofBasis Source #
Instance details Defined in Static.DgUtils Methods (==) :: ProofBasis -> ProofBasis -> Bool (/=) :: ProofBasis -> ProofBasis -> Bool
Data ProofBasis Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> ProofBasis -> ShowS show :: ProofBasis -> String showList :: [ProofBasis] -> ShowS
ShATermLG ProofBasis Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> ProofBasis -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ProofBasis) Source #

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

Instances details

Eq DGRule Source #
Instance details Defined in Static.DgUtils Methods (==) :: DGRule -> DGRule -> Bool (/=) :: DGRule -> DGRule -> Bool
Data DGRule Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> DGRule -> ShowS show :: DGRule -> String showList :: [DGRule] -> ShowS
Pretty DGRule Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: DGRule -> Doc Source # pretties :: [DGRule] -> Doc Source #
ShATermLG DGRule Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> DGRule -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGRule) Source #

data ThmLinkStatus Source #

proof status of a link

Constructors

LeftOpen
Proven DGRule ProofBasis

Instances

Instances details

Eq ThmLinkStatus Source #
Instance details Defined in Static.DgUtils Methods (==) :: ThmLinkStatus -> ThmLinkStatus -> Bool (/=) :: ThmLinkStatus -> ThmLinkStatus -> Bool
Data ThmLinkStatus Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> ThmLinkStatus -> ShowS show :: ThmLinkStatus -> String showList :: [ThmLinkStatus] -> ShowS
Pretty ThmLinkStatus Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: ThmLinkStatus -> Doc Source # pretties :: [ThmLinkStatus] -> Doc Source #
ShATermLG ThmLinkStatus Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> ThmLinkStatus -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ThmLinkStatus) Source #

isProvenThmLinkStatus :: ThmLinkStatus -> Bool Source #

proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis Source #

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

data Scope Source #

Constructors

Local
Global

Instances

Instances details

Eq Scope Source #
Instance details Defined in Static.DgUtils Methods (==) :: Scope -> Scope -> Bool (/=) :: Scope -> Scope -> Bool
Data Scope Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> Scope -> ShowS show :: Scope -> String showList :: [Scope] -> ShowS
ShATermLG Scope Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> Scope -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Scope) Source #

data LinkKind Source #

Constructors

DefLink
ThmLink ThmLinkStatus

Instances

Instances details

Eq LinkKind Source #
Instance details Defined in Static.DgUtils Methods (==) :: LinkKind -> LinkKind -> Bool (/=) :: LinkKind -> LinkKind -> Bool
Data LinkKind Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> LinkKind -> ShowS show :: LinkKind -> String showList :: [LinkKind] -> ShowS
ShATermLG LinkKind Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> LinkKind -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, LinkKind) Source #

data FreeOrCofree Source #

Constructors

Free
Cofree
NPFree
Minimize

Instances

Instances details

Bounded FreeOrCofree Source #
Instance details Defined in Static.DgUtils Methods minBound :: FreeOrCofree maxBound :: FreeOrCofree
Enum FreeOrCofree Source #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods (==) :: FreeOrCofree -> FreeOrCofree -> Bool (/=) :: FreeOrCofree -> FreeOrCofree -> Bool
Data FreeOrCofree Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods readsPrec :: Int -> ReadS FreeOrCofree readList :: ReadS [FreeOrCofree] readPrec :: ReadPrec FreeOrCofree readListPrec :: ReadPrec [FreeOrCofree]
Show FreeOrCofree Source #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> FreeOrCofree -> ShowS show :: FreeOrCofree -> String showList :: [FreeOrCofree] -> ShowS
ShATermLG FreeOrCofree Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> FreeOrCofree -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, FreeOrCofree) Source #

fcList :: [FreeOrCofree] Source #

data ConsStatus Source #

required and proven conservativity (with a proof)

Constructors

ConsStatus
Fields requiredConservativity :: Conservativity provenConservativity :: Conservativity linkStatus :: ThmLinkStatus

Instances

Instances details

Eq ConsStatus Source #
Instance details Defined in Static.DgUtils Methods (==) :: ConsStatus -> ConsStatus -> Bool (/=) :: ConsStatus -> ConsStatus -> Bool
Data ConsStatus Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> ConsStatus -> ShowS show :: ConsStatus -> String showList :: [ConsStatus] -> ShowS
Pretty ConsStatus Source #
Instance details Defined in Static.PrintDevGraph Methods pretty :: ConsStatus -> Doc Source # pretties :: [ConsStatus] -> Doc Source #
ShATermLG ConsStatus Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> ConsStatus -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ConsStatus) Source #

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

Instances details

Eq DGEdgeType Source #
Instance details Defined in Static.DgUtils Methods (==) :: DGEdgeType -> DGEdgeType -> Bool (/=) :: DGEdgeType -> DGEdgeType -> Bool
Data DGEdgeType Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> DGEdgeType -> ShowS show :: DGEdgeType -> String showList :: [DGEdgeType] -> ShowS
ShATermLG DGEdgeType Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> DGEdgeType -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGEdgeType) Source #

data DGEdgeTypeModInc Source #

Constructors

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

Instances

Instances details

Eq DGEdgeTypeModInc Source #
Instance details Defined in Static.DgUtils Methods (==) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool (/=) :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
Data DGEdgeTypeModInc Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> DGEdgeTypeModInc -> ShowS show :: DGEdgeTypeModInc -> String showList :: [DGEdgeTypeModInc] -> ShowS
ShATermLG DGEdgeTypeModInc Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> DGEdgeTypeModInc -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGEdgeTypeModInc) Source #

data ThmTypes Source #

Constructors

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

Instances

Instances details

Eq ThmTypes Source #
Instance details Defined in Static.DgUtils Methods (==) :: ThmTypes -> ThmTypes -> Bool (/=) :: ThmTypes -> ThmTypes -> Bool
Data ThmTypes Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> ThmTypes -> ShowS show :: ThmTypes -> String showList :: [ThmTypes] -> ShowS
ShATermLG ThmTypes Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> ThmTypes -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ThmTypes) Source #

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

Instances details

Eq RTPointer Source #
Instance details Defined in Static.DgUtils Methods (==) :: RTPointer -> RTPointer -> Bool (/=) :: RTPointer -> RTPointer -> Bool
Data RTPointer Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils 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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> RTPointer -> ShowS show :: RTPointer -> String showList :: [RTPointer] -> ShowS
ShATermLG RTPointer Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> RTPointer -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTPointer) Source #

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

Instances details

Data RTLeaves Source #
Instance details Defined in Static.DgUtils 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 :: forall r r'. (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 #
Instance details Defined in Static.DgUtils Methods showsPrec :: Int -> RTLeaves -> ShowS show :: RTLeaves -> String showList :: [RTLeaves] -> ShowS
ShATermLG RTLeaves Source #
Instance details Defined in ATC.DgUtils Methods toShATermLG :: ATermTable -> RTLeaves -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTLeaves) Source #