{- |

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 (IRI, nullIRI, iriToStringShortUnsecure, parseCurie)

import Common.Utils (numberSuffix, splitByList, splitOn, readMaybe)

import Common.LibName

import Common.Consistency

import Data.Graph.Inductive.Graph (Node)

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 Node

| NPBranch Node (Map.Map IRI RTPointer)

-- here the leaves can be either NPUnit or NPComp

| NPRef Node Node

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

refSource (NPUnit n) = n

refSource (NPBranch n _) = n

refSource (NPRef n _) = n

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

data RTLeaves = RTLeaf Node | 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 (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

[i] ->

makeName $ fromJust $ parseCurie i

[i, e] ->

let n = makeName $ fromJust $ parseCurie i

mSf = numberSuffix e

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

in n { extString = es

, extIndex = sf }

_ ->

error

$ "parseNodeName: malformed NodeName, too many __: "

++ s

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