809N/ADescription : auxiliary datastructures for development graphs
809N/ACopyright : (c) DFKI GmbH 2011
809N/AMaintainer : Christian.Maeder@dfki.de
809N/Adata XPathPart = ElemName String | ChildIndex Int deriving Show
809N/A{- | name of a node in a DG; auxiliary nodes may have extension string
809N/A and non-zero number (for these, names are usually hidden). -}
instance Ord NodeName where
compare n1 n2 = compare (showName n1) (showName n2)
instance Eq NodeName where
n1 == n2 = compare n1 n2 == EQ
readXPath :: Monad m => String -> m [XPathPart]
readXPath = mapM readXPathComp . splitOn '/'
readXPathComp :: Monad m => String -> m XPathPart
readXPathComp s = case splitAt 5 s of
("Spec[", s') -> case readMaybe $ takeWhile (/= ']') s' of
Just i -> return $ ChildIndex i
Nothing -> fail "cannot read nodes ChildIndex"
isInternal :: NodeName -> Bool
isInternal n = extIndex n /= 0 || not (null $ extString n)
-- | test if a conservativity is open, return input for None
hasOpenConsStatus :: Bool -> ConsStatus -> Bool
hasOpenConsStatus b (ConsStatus cons _ thm) = case cons of
_ -> not $ isProvenThmLinkStatus thm
data DGNodeType = DGNodeType
, isInternalSpec :: Bool }
listDGNodeTypes :: [DGNodeType]
listDGNodeTypes = let bs = [False, True] in
, isProvenNode = isEmpty'
, isInternalSpec = spec }
unMod = NodeMod False False False False False
delAxMod = unMod { delAx = True }
delThMod = unMod { delTh = True }
delSenMod = delAxMod { delTh = True }
addSenMod = unMod { addSen = True }
senMod = delSenMod { addSen = True }
delSymMod = unMod { delSym = True }
addSymMod = unMod { addSym = True }
symMod = delSymMod { addSym = True }
mergeNodeMod :: NodeMod -> NodeMod -> NodeMod
= let delSym3 = delSym1 || delSym2
setSenMod a b = if delSym3 then False else a || b
{ delAx = setSenMod delAx1 delAx2
, delTh = setSenMod delTh1 delTh2
, addSen = setSenMod addSen1 addSen2
, addSym = addSym1 || addSym2 }
-- | unique number for edges
newtype EdgeId = EdgeId Int deriving (Show, Eq, Ord)
incEdgeId :: EdgeId -> EdgeId
incEdgeId (EdgeId i) = EdgeId $ i + 1
-- | the first edge in a graph
showEdgeId :: EdgeId -> String
showEdgeId (EdgeId i) = show i
newtype ProofBasis = ProofBasis { proofBasis ::
Set.Set EdgeId }
{- | Rules in the development graph calculus,
Sect. IV:4.4 of the CASL Reference Manual explains them in depth
| DGRuleWithEdge String EdgeId
| DGRuleLocalInference [(String, String)] -- renamed theorems
-- | proof status of a link
data ThmLinkStatus = LeftOpen | Proven DGRule ProofBasis deriving (Show, Eq)
isProvenThmLinkStatus :: ThmLinkStatus -> Bool
isProvenThmLinkStatus tls = case tls of
proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
proofBasisOfThmLinkStatus tls = case tls of
LeftOpen -> emptyProofBasis
updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
updProofBasisOfThmLinkStatus tls pB = case tls of
Proven r _ -> Proven r pB
data Scope = Local | Global deriving (Show, Eq, Ord)
data LinkKind = DefLink | ThmLink ThmLinkStatus deriving (Show, Eq)
data FreeOrCofree = Free | Cofree | NPFree
deriving (Show, Eq, Ord, Enum, Bounded, Read)
fcList = [minBound .. maxBound]
-- | required and proven conservativity (with a proof)
data ConsStatus = ConsStatus Conservativity Conservativity ThmLinkStatus
isProvenConsStatusLink :: ConsStatus -> Bool
isProvenConsStatusLink = not . hasOpenConsStatus False
mkConsStatus :: Conservativity -> ConsStatus
mkConsStatus c = ConsStatus c None LeftOpen
getConsOfStatus :: ConsStatus -> Conservativity
getConsOfStatus (ConsStatus c _ _) = c
-- | to be displayed as edge label
showConsStatus :: ConsStatus -> String
showConsStatus cs = case cs of
ConsStatus None None _ -> ""
ConsStatus None _ LeftOpen -> ""
ConsStatus c _ LeftOpen -> show c ++ "?"
ConsStatus _ cp _ -> show cp
-- | converts a DGEdgeType to a String
getDGEdgeTypeName :: DGEdgeType -> String
(if isInc e then (++ "Inc") else id)
$ getDGEdgeTypeModIncName $ edgeTypeModInc e
revertDGEdgeTypeName :: String -> DGEdgeType
$ find ((== tp) . getDGEdgeTypeName) listDGEdgeTypes
getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String
getDGEdgeTypeModIncName et = case et of
ThmType thm isPrvn _ _ ->
let prvn = (if isPrvn then "P" else "Unp") ++ "roven" in
HidingThm -> prvn ++ "HidingThm"
FreeOrCofreeThm fc -> prvn ++ shows fc "Thm"
GlobalOrLocalThm scope isHom ->
let het = if isHom then id else ("Het" ++) in
Global -> if isHom then "Global" else "") ++ prvn ++ "Thm"
FreeOrCofreeDef fc -> shows fc "Def"
data DGEdgeType = DGEdgeType
{ edgeTypeModInc :: DGEdgeTypeModInc
| FreeOrCofreeDef FreeOrCofree
| ThmType { thmEdgeType :: ThmTypes
| FreeOrCofreeThm FreeOrCofree
| GlobalOrLocalThm { thmScope :: Scope
-- | Creates a list with all DGEdgeType types
listDGEdgeTypes :: [DGEdgeType]
[ DGEdgeType { edgeTypeModInc = modinc
] ++ [ FreeOrCofreeDef fc | fc <- fcList ] ++
[ ThmType { thmEdgeType = thmType
: [ FreeOrCofreeThm fc | fc <- fcList ] ++
[ GlobalOrLocalThm { thmScope = scope
| scope <- [Local, Global]
, proven <- [True, False]
, pending <- [True, False]
, isInclusion' <- [True, False]
-- | check an EdgeType and see if its a definition link
isDefEdgeType :: DGEdgeType -> Bool
isDefEdgeType edgeTp = case edgeTypeModInc edgeTp of
-- * datatypes for storing the nodes of the ref tree in the global env
| NPBranch Node (
Map.Map IRI RTPointer)
-- here the leaves can be either NPUnit or NPComp
{- here the leaves can be NPUnit or NPComp
and roots are needed for inserting edges -}
mapRTNodes ::
Map.Map Node Node -> RTPointer -> RTPointer
NPUnit x -> NPUnit (app f x)
NPRef x y -> NPRef (app f x) (app f y)
NPBranch x g -> NPBranch (app f x) (
Map.map (mapRTNodes f) g)
NPComp g -> NPComp (
Map.map (mapRTNodes f) g)
compPointer :: RTPointer -> RTPointer -> RTPointer
compPointer (NPUnit n1) (NPUnit n2) = NPRef n1 n2
compPointer (NPUnit n1) (NPBranch _ f) = NPBranch n1 f
compPointer (NPUnit n1) (NPRef _ n2) = NPRef n1 n2
compPointer (NPRef n1 _) (NPRef _ n2) = NPRef n1 n2
compPointer (NPRef n1 _) (NPBranch _ f) = NPBranch n1 f
compPointer (NPBranch n1 f1) (NPComp f2) =
compPointer (NPComp f1) (NPComp f2) =
compPointer x y = error $ "compPointer:" ++ show x ++ " " ++ show y
refSource :: RTPointer -> Node
refSource (NPBranch n _) = n
refSource (NPRef n _) = n
refSource x = error ("refSource:" ++ show x)
data RTLeaves = RTLeaf Node | RTLeaves (
Map.Map IRI RTLeaves)
refTarget :: RTPointer -> RTLeaves
refTarget (NPUnit n) = RTLeaf n
refTarget (NPRef _ n) = RTLeaf n
refTarget (NPComp f) = RTLeaves $
Map.map refTarget f
refTarget (NPBranch _ f) = RTLeaves $
Map.map refTarget f
refTarget x = error ("refTarget:" ++ show x)
emptyNodeName :: NodeName
emptyNodeName = NodeName nullIRI "" 0 []
showExt :: NodeName -> String
showExt n = let i = extIndex n in extString n ++ if i == 0 then "" else show i
showName :: NodeName -> String
showName n = let ext = showExt n in
iriToStringShortUnsecure (getName n)
++ if null ext then ext else "__" ++ ext
makeName :: IRI -> NodeName
makeName n = NodeName n "" 0 [ElemName $ iriToStringShortUnsecure n]
parseNodeName :: String -> NodeName
parseNodeName s = case splitByList "__" s of
makeName $ fromJust $ parseCurie i
let n = makeName $ fromJust $ parseCurie i
(es, sf) = fromMaybe (e, 0) mSf
$ "parseNodeName: malformed NodeName, too many __: "
incBy :: Int -> NodeName -> NodeName
{ extIndex = extIndex n + i
, xpath = case xpath n of
ChildIndex j : r -> ChildIndex (j + i) : r
inc :: NodeName -> NodeName
extName :: String -> NodeName -> NodeName
{ extString = showExt n ++ take 1 s
, xpath = ElemName s : xpath n }
-- ** handle edge numbers and proof bases
-- | create a default ID which has to be changed when inserting a certain edge.
defaultEdgeId = EdgeId $ -1
emptyProofBasis :: ProofBasis
nullProofBasis :: ProofBasis -> Bool
addEdgeId :: ProofBasis -> EdgeId -> ProofBasis
addEdgeId (ProofBasis s) e = ProofBasis $
Set.insert e s
delEdgeId :: ProofBasis -> EdgeId -> ProofBasis
delEdgeId (ProofBasis s) e = ProofBasis $
Set.delete e s
updEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis
updEdgeId pb = addEdgeId . delEdgeId pb
-- | checks if the given edge is contained in the given proof basis..
edgeInProofBasis :: EdgeId -> ProofBasis -> Bool
topsortedLibsWithImports ::
Rel.Rel LibName -> [LibName]
getMapAndMaxIndex :: Ord k => k -> (b ->
Map.Map k a) -> b -> (
Map.Map k a, k)
getMapAndMaxIndex c f gctx =
liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr f g x = f x || g x