{- |

Module : $Header$

Description : auxiliary datastructures for development graphs

Copyright : (c) DFKI GmbH 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

-}

module Static.DgUtils where

import qualified Common.Lib.Rel as Rel

import Common.IRI

import Common.Utils

import Common.LibName

import Common.Consistency

import Data.List

import Data.Maybe

import qualified Data.Map as Map

import qualified Data.Set as Set

-- ** node label types

data XPathPart = ElemName String | ChildIndex Int deriving Show

{- | name of a node in a DG; auxiliary nodes may have extension string

and non-zero number (for these, names are usually hidden). -}

data NodeName = NodeName

{ getName :: IRI

, extString :: String

, extIndex :: Int

, xpath :: [XPathPart]

} deriving Show

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"

_ -> return $ ElemName s

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

None -> b

_ -> not $ isProvenThmLinkStatus thm

data DGNodeType = DGNodeType

{ isRefType :: Bool

, isProvenNode :: Bool

, isProvenCons :: Bool

, isInternalSpec :: Bool }

deriving (Eq, Ord, Show)

listDGNodeTypes :: [DGNodeType]

listDGNodeTypes = let bs = [False, True] in

[ DGNodeType

{ isRefType = ref

, isProvenNode = isEmpty'

, isProvenCons = proven

, isInternalSpec = spec }

| ref <- bs

, isEmpty' <- bs

, proven <- bs

, spec <- bs ]

-- | node modifications

data NodeMod = NodeMod

{ delAx :: Bool

, delTh :: Bool

, addSen :: Bool

, delSym :: Bool

, addSym :: Bool }

deriving (Show, Eq)

-- | an unmodified node

unMod :: NodeMod

unMod = NodeMod False False False False False

delAxMod :: NodeMod

delAxMod = unMod { delAx = True }

delThMod :: NodeMod

delThMod = unMod { delTh = True }

delSenMod :: NodeMod

delSenMod = delAxMod { delTh = True }

addSenMod :: NodeMod

addSenMod = unMod { addSen = True }

senMod :: NodeMod

senMod = delSenMod { addSen = True }

delSymMod :: NodeMod

delSymMod = unMod { delSym = True }

addSymMod :: NodeMod

addSymMod = unMod { addSym = True }

symMod :: NodeMod

symMod = delSymMod { addSym = True }

mergeNodeMod :: NodeMod -> NodeMod -> NodeMod

mergeNodeMod NodeMod

{ delAx = delAx1

, delTh = delTh1

, addSen = addSen1

, delSym = delSym1

, addSym = addSym1 }

NodeMod

{ delAx = delAx2

, delTh = delTh2

, addSen = addSen2

, delSym = delSym2

, addSym = addSym2 }

= let delSym3 = delSym1 || delSym2

setSenMod a b = not delSym3 && (a || b)

in NodeMod

{ delAx = setSenMod delAx1 delAx2

, delTh = setSenMod delTh1 delTh2

, addSen = setSenMod addSen1 addSen2

, delSym = delSym3

, addSym = addSym1 || addSym2 }

-- ** edge types

-- | unique number for edges

newtype EdgeId = EdgeId Int deriving (Show, Eq, Ord)

-- | next edge id

incEdgeId :: EdgeId -> EdgeId

incEdgeId (EdgeId i) = EdgeId $ i + 1

-- | the first edge in a graph

startEdgeId :: EdgeId

startEdgeId = EdgeId 0

showEdgeId :: EdgeId -> String

showEdgeId (EdgeId i) = show i

-- | a set of used edges

newtype ProofBasis = ProofBasis { proofBasis :: Set.Set EdgeId }

deriving (Show, Eq, Ord)

{- | Rules in the development graph calculus,

Sect. IV:4.4 of the CASL Reference Manual explains them in depth

-}

data DGRule =

DGRule String

| DGRuleWithEdge String EdgeId

| DGRuleLocalInference [(String, String)] -- renamed theorems

| Composition [EdgeId]

deriving (Show, Eq)

-- | proof status of a link

data ThmLinkStatus = LeftOpen | Proven DGRule ProofBasis deriving (Show, Eq)

isProvenThmLinkStatus :: ThmLinkStatus -> Bool

isProvenThmLinkStatus tls = case tls of

LeftOpen -> False

_ -> True

proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis

proofBasisOfThmLinkStatus tls = case tls of

LeftOpen -> emptyProofBasis

Proven _ pB -> pB

updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus

updProofBasisOfThmLinkStatus tls pB = case tls of

LeftOpen -> tls

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 | Minimize

deriving (Show, Eq, Ord, Enum, Bounded, Read)

fcList :: [FreeOrCofree]

fcList = [minBound .. maxBound]

-- | required and proven conservativity (with a proof)

data ConsStatus = ConsStatus Conservativity Conservativity ThmLinkStatus

deriving (Show, Eq)

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

getDGEdgeTypeName e =

(if isInc e then (++ "Inc") else id)

$ getDGEdgeTypeModIncName $ edgeTypeModInc e

revertDGEdgeTypeName :: String -> DGEdgeType

revertDGEdgeTypeName tp = fromMaybe (error "DevGraph.revertDGEdgeTypeName")

$ 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

case thm of

HidingThm -> prvn ++ "HidingThm"

FreeOrCofreeThm fc -> prvn ++ shows fc "Thm"

GlobalOrLocalThm scope isHom ->

let het = if isHom then id else ("Het" ++) in

het (case scope of

Local -> "Local"

Global -> if isHom then "Global" else "") ++ prvn ++ "Thm"

FreeOrCofreeDef fc -> shows fc "Def"

_ -> show et

data DGEdgeType = DGEdgeType

{ edgeTypeModInc :: DGEdgeTypeModInc

, isInc :: Bool }

deriving (Eq, Ord, Show)

data DGEdgeTypeModInc =

GlobalDef

| HetDef

| HidingDef

| LocalDef

| FreeOrCofreeDef FreeOrCofree

| ThmType { thmEdgeType :: ThmTypes

, isProvenEdge :: Bool

, isConservativ :: Bool

, isPending :: Bool }

deriving (Eq, Ord, Show)

data ThmTypes =

HidingThm

| FreeOrCofreeThm FreeOrCofree

| GlobalOrLocalThm { thmScope :: Scope

, isHomThm :: Bool }

deriving (Eq, Ord, Show)

-- | Creates a list with all DGEdgeType types

listDGEdgeTypes :: [DGEdgeType]

listDGEdgeTypes =

[ DGEdgeType { edgeTypeModInc = modinc

, isInc = isInclusion' }

| modinc <-

[ GlobalDef

, HetDef

, HidingDef

, LocalDef

] ++ [ FreeOrCofreeDef fc | fc <- fcList ] ++

[ ThmType { thmEdgeType = thmType

, isProvenEdge = proven

, isConservativ = cons

, isPending = pending }

| thmType <- HidingThm

: [ FreeOrCofreeThm fc | fc <- fcList ] ++

[ GlobalOrLocalThm { thmScope = scope

, isHomThm = hom }

| scope <- [Local, Global]

, hom <- [True, False]

]

, proven <- [True, False]

, cons <- [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

ThmType {} -> False

_ -> True

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

data RTPointer =

RTNone

| NPUnit Int

| NPBranch Int (Map.Map IRI RTPointer)

-- here the leaves can be either NPUnit or NPComp

| NPRef Int Int

| NPComp (Map.Map IRI RTPointer)

{- here the leaves can be NPUnit or NPComp

and roots are needed for inserting edges -}

deriving (Show, Eq)

-- map nodes

mapRTNodes :: Map.Map Int Int -> RTPointer -> RTPointer

mapRTNodes f rtp = let app = flip $ Map.findWithDefault (error "mapRTNodes")

in case rtp of

RTNone -> RTNone

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)

-- compositions

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) =

NPBranch n1 (Map.unionWith (\ _ y -> y) f1 f2 )

compPointer (NPComp f1) (NPComp f2) =

NPComp (Map.unionWith (\ _ y -> y) f1 f2)

compPointer x y = error $ "compPointer:" ++ show x ++ " " ++ show y

-- sources

refSource :: RTPointer -> Int

refSource (NPUnit n) = n

refSource (NPBranch n _) = n

refSource (NPRef n _) = n

refSource x = error ("refSource:" ++ show x)

data RTLeaves = RTLeaf Int | RTLeaves (Map.Map IRI RTLeaves)

deriving Show

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)

-- ** for node names

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 (setAngles False $ 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 =

let err msg = error $ "parseNodeName: malformed NodeName" ++ msg ++ s

mkName = makeName . fromMaybe (err ": ") . parseCurie

in case splitByList "__" s of

[i] -> mkName i

[i, e] ->

let n = mkName i

mSf = numberSuffix e

(es, sf) = fromMaybe (e, 0) mSf

in n { extString = es

, extIndex = sf }

_ -> err ", too many __: "

incBy :: Int -> NodeName -> NodeName

incBy i n = n

{ extIndex = extIndex n + i

, xpath = case xpath n of

ChildIndex j : r -> ChildIndex (j + i) : r

l -> ChildIndex i : l }

inc :: NodeName -> NodeName

inc = incBy 1

extName :: String -> NodeName -> NodeName

extName s n = n

{ extString = showExt n ++ take 1 s

, extIndex = 0

, 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

defaultEdgeId = EdgeId $ -1

emptyProofBasis :: ProofBasis

emptyProofBasis = ProofBasis Set.empty

nullProofBasis :: ProofBasis -> Bool

nullProofBasis = Set.null . proofBasis

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

edgeInProofBasis e = Set.member e . proofBasis

-- * utilities

topsortedLibsWithImports :: Rel.Rel LibName -> [LibName]

topsortedLibsWithImports = concatMap Set.toList . Rel.topSort

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

getMapAndMaxIndex c f gctx =

let m = f gctx in (m, if Map.null m then c else fst $ Map.findMax m)

-- | or two predicates

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

liftOr f g x = f x || g x