{-# LANGUAGE RankNTypes, DeriveDataTypeable #-}
{- |
Module      :  ./Static/DevGraph.hs
Description :  Central datastructures for development graphs
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

Central datastructures for development graphs
   Follows Sect. IV:4.2 of the CASL Reference Manual.

We also provide functions for constructing and modifying development graphs.
However note that these changes need to be propagated to the GUI if they
also shall be visible in the displayed development graph.
-}

{-
   References:

   T. Mossakowski, S. Autexier and D. Hutter:
   Extending Development Graphs With Hiding.
   H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
   Lecture Notes in Computer Science 2029, p. 269-283,
   Springer-Verlag 2001.

   T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
   CASL Proof calculus. In: CASL reference manual, part IV.
   Available from http://www.cofi.info

-}

module Static.DevGraph where

import Syntax.AS_Structured
import Syntax.AS_Library
import Static.GTheory
import Static.DgUtils
import qualified Static.XGraph as XGraph

import Logic.Logic
import Logic.ExtSign
import Logic.Comorphism
import Logic.Grothendieck
import Logic.Prover

import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.Graph as Tree
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.SizedList as SizedList
import qualified Common.OrderedMap as OMap
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.LibName
import Common.Consistency

import Control.Concurrent.MVar

import Data.Graph.Inductive.Basic
import Data.Graph.Inductive.Graph as Graph
import Data.Graph.Inductive.Query.DFS

import Data.List
import Data.Maybe
import Data.Ord
import Data.Typeable
import qualified Data.Map as Map
import qualified Data.Set as Set

import Common.Result

import qualified Control.Monad.Fail as Fail

-- * types for structured specification analysis

-- ** basic types

-- | Node with signature in a DG
data NodeSig = NodeSig { NodeSig -> Node
getNode :: Node, NodeSig -> G_sign
getSig :: G_sign }
    deriving (Node -> NodeSig -> ShowS
[NodeSig] -> ShowS
NodeSig -> String
(Node -> NodeSig -> ShowS)
-> (NodeSig -> String) -> ([NodeSig] -> ShowS) -> Show NodeSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NodeSig] -> ShowS
$cshowList :: [NodeSig] -> ShowS
show :: NodeSig -> String
$cshow :: NodeSig -> String
showsPrec :: Node -> NodeSig -> ShowS
$cshowsPrec :: Node -> NodeSig -> ShowS
Show, NodeSig -> NodeSig -> Bool
(NodeSig -> NodeSig -> Bool)
-> (NodeSig -> NodeSig -> Bool) -> Eq NodeSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeSig -> NodeSig -> Bool
$c/= :: NodeSig -> NodeSig -> Bool
== :: NodeSig -> NodeSig -> Bool
$c== :: NodeSig -> NodeSig -> Bool
Eq, Typeable)

{- | NodeSig or possibly the empty sig in a logic
     (but since we want to avoid lots of vsacuous nodes with empty sig,
     we do not assign a real node in the DG here) -}
data MaybeNode = JustNode NodeSig | EmptyNode AnyLogic
  deriving (Node -> MaybeNode -> ShowS
[MaybeNode] -> ShowS
MaybeNode -> String
(Node -> MaybeNode -> ShowS)
-> (MaybeNode -> String)
-> ([MaybeNode] -> ShowS)
-> Show MaybeNode
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MaybeNode] -> ShowS
$cshowList :: [MaybeNode] -> ShowS
show :: MaybeNode -> String
$cshow :: MaybeNode -> String
showsPrec :: Node -> MaybeNode -> ShowS
$cshowsPrec :: Node -> MaybeNode -> ShowS
Show, MaybeNode -> MaybeNode -> Bool
(MaybeNode -> MaybeNode -> Bool)
-> (MaybeNode -> MaybeNode -> Bool) -> Eq MaybeNode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MaybeNode -> MaybeNode -> Bool
$c/= :: MaybeNode -> MaybeNode -> Bool
== :: MaybeNode -> MaybeNode -> Bool
$c== :: MaybeNode -> MaybeNode -> Bool
Eq, Typeable)

getMaybeNodes :: MaybeNode -> Set.Set Node
getMaybeNodes :: MaybeNode -> Set Node
getMaybeNodes m :: MaybeNode
m = case MaybeNode
m of
  EmptyNode _ -> Set Node
forall a. Set a
Set.empty
  JustNode n :: NodeSig
n -> Node -> Set Node
forall a. a -> Set a
Set.singleton (Node -> Set Node) -> Node -> Set Node
forall a b. (a -> b) -> a -> b
$ NodeSig -> Node
getNode NodeSig
n

-- | a wrapper for renamings with a trivial Ord instance
newtype Renamed = Renamed RENAMING deriving (Node -> Renamed -> ShowS
[Renamed] -> ShowS
Renamed -> String
(Node -> Renamed -> ShowS)
-> (Renamed -> String) -> ([Renamed] -> ShowS) -> Show Renamed
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Renamed] -> ShowS
$cshowList :: [Renamed] -> ShowS
show :: Renamed -> String
$cshow :: Renamed -> String
showsPrec :: Node -> Renamed -> ShowS
$cshowsPrec :: Node -> Renamed -> ShowS
Show, Typeable)

instance Ord Renamed where
  compare :: Renamed -> Renamed -> Ordering
compare _ _ = Ordering
EQ

instance Eq Renamed where
  _ == :: Renamed -> Renamed -> Bool
== _ = Bool
True

-- | a wrapper for restrictions with a trivial Ord instance
data MaybeRestricted = NoRestriction | Restricted RESTRICTION
  deriving (Node -> MaybeRestricted -> ShowS
[MaybeRestricted] -> ShowS
MaybeRestricted -> String
(Node -> MaybeRestricted -> ShowS)
-> (MaybeRestricted -> String)
-> ([MaybeRestricted] -> ShowS)
-> Show MaybeRestricted
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MaybeRestricted] -> ShowS
$cshowList :: [MaybeRestricted] -> ShowS
show :: MaybeRestricted -> String
$cshow :: MaybeRestricted -> String
showsPrec :: Node -> MaybeRestricted -> ShowS
$cshowsPrec :: Node -> MaybeRestricted -> ShowS
Show, Typeable)

instance Ord MaybeRestricted where
  compare :: MaybeRestricted -> MaybeRestricted -> Ordering
compare _ _ = Ordering
EQ

instance Eq MaybeRestricted where
  _ == :: MaybeRestricted -> MaybeRestricted -> Bool
== _ = Bool
True

{- | Data type indicating the origin of nodes and edges in the input language
     This is not used in the DG calculus, only may be used in the future
     for reconstruction of input and management of change. -}
data DGOrigin =
    DGEmpty
  | DGBasic
  | DGBasicSpec (Maybe G_basic_spec) G_sign (Set.Set G_symbol)
  | DGExtension
  | DGLogicCoercion
  | DGTranslation Renamed
  | DGUnion
  | DGIntersect
  | DGExtract
  | DGRestriction (MaybeRestricted) (Set.Set G_symbol)
  | DGRevealTranslation
  | DGFreeOrCofree FreeOrCofree
  | DGLocal
  | DGClosed
  | DGLogicQual
  | DGData
  | DGFormalParams
  | DGVerificationGeneric
  | DGImports
  | DGInst IRI
  | DGFitSpec
  | DGFitView IRI
  | DGProof
  | DGNormalForm Node
  | DGintegratedSCC
  | DGFlattening
  | DGAlignment
  | DGTest
    deriving (Node -> DGOrigin -> ShowS
[DGOrigin] -> ShowS
DGOrigin -> String
(Node -> DGOrigin -> ShowS)
-> (DGOrigin -> String) -> ([DGOrigin] -> ShowS) -> Show DGOrigin
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGOrigin] -> ShowS
$cshowList :: [DGOrigin] -> ShowS
show :: DGOrigin -> String
$cshow :: DGOrigin -> String
showsPrec :: Node -> DGOrigin -> ShowS
$cshowsPrec :: Node -> DGOrigin -> ShowS
Show, DGOrigin -> DGOrigin -> Bool
(DGOrigin -> DGOrigin -> Bool)
-> (DGOrigin -> DGOrigin -> Bool) -> Eq DGOrigin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGOrigin -> DGOrigin -> Bool
$c/= :: DGOrigin -> DGOrigin -> Bool
== :: DGOrigin -> DGOrigin -> Bool
$c== :: DGOrigin -> DGOrigin -> Bool
Eq, Eq DGOrigin
Eq DGOrigin =>
(DGOrigin -> DGOrigin -> Ordering)
-> (DGOrigin -> DGOrigin -> Bool)
-> (DGOrigin -> DGOrigin -> Bool)
-> (DGOrigin -> DGOrigin -> Bool)
-> (DGOrigin -> DGOrigin -> Bool)
-> (DGOrigin -> DGOrigin -> DGOrigin)
-> (DGOrigin -> DGOrigin -> DGOrigin)
-> Ord DGOrigin
DGOrigin -> DGOrigin -> Bool
DGOrigin -> DGOrigin -> Ordering
DGOrigin -> DGOrigin -> DGOrigin
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DGOrigin -> DGOrigin -> DGOrigin
$cmin :: DGOrigin -> DGOrigin -> DGOrigin
max :: DGOrigin -> DGOrigin -> DGOrigin
$cmax :: DGOrigin -> DGOrigin -> DGOrigin
>= :: DGOrigin -> DGOrigin -> Bool
$c>= :: DGOrigin -> DGOrigin -> Bool
> :: DGOrigin -> DGOrigin -> Bool
$c> :: DGOrigin -> DGOrigin -> Bool
<= :: DGOrigin -> DGOrigin -> Bool
$c<= :: DGOrigin -> DGOrigin -> Bool
< :: DGOrigin -> DGOrigin -> Bool
$c< :: DGOrigin -> DGOrigin -> Bool
compare :: DGOrigin -> DGOrigin -> Ordering
$ccompare :: DGOrigin -> DGOrigin -> Ordering
$cp1Ord :: Eq DGOrigin
Ord, Typeable)

-- | node content or reference to another library's node
data DGNodeInfo = DGNode
  { DGNodeInfo -> DGOrigin
node_origin :: DGOrigin       -- origin in input language
  , DGNodeInfo -> ConsStatus
node_cons_status :: ConsStatus } -- like a link from the empty signature
  | DGRef                        -- reference to node in a different DG
  { DGNodeInfo -> LibName
ref_libname :: LibName      -- pointer to DG where ref'd node resides
  , DGNodeInfo -> Node
ref_node :: Node             -- pointer to ref'd node
  } deriving (Node -> DGNodeInfo -> ShowS
[DGNodeInfo] -> ShowS
DGNodeInfo -> String
(Node -> DGNodeInfo -> ShowS)
-> (DGNodeInfo -> String)
-> ([DGNodeInfo] -> ShowS)
-> Show DGNodeInfo
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGNodeInfo] -> ShowS
$cshowList :: [DGNodeInfo] -> ShowS
show :: DGNodeInfo -> String
$cshow :: DGNodeInfo -> String
showsPrec :: Node -> DGNodeInfo -> ShowS
$cshowsPrec :: Node -> DGNodeInfo -> ShowS
Show, DGNodeInfo -> DGNodeInfo -> Bool
(DGNodeInfo -> DGNodeInfo -> Bool)
-> (DGNodeInfo -> DGNodeInfo -> Bool) -> Eq DGNodeInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGNodeInfo -> DGNodeInfo -> Bool
$c/= :: DGNodeInfo -> DGNodeInfo -> Bool
== :: DGNodeInfo -> DGNodeInfo -> Bool
$c== :: DGNodeInfo -> DGNodeInfo -> Bool
Eq, Typeable)

{- | node inscriptions in development graphs.
Nothing entries indicate "not computed yet" -}
data DGNodeLab =
  DGNodeLab
  { DGNodeLab -> NodeName
dgn_name :: NodeName        -- name in the input language
  , DGNodeLab -> G_theory
dgn_theory :: G_theory      -- local theory
  , DGNodeLab -> Maybe G_theory
globalTheory :: Maybe G_theory -- global theory
  , DGNodeLab -> Bool
labelHasHiding :: Bool      -- has this node an ingoing hiding link
  , DGNodeLab -> Bool
labelHasFree :: Bool        -- has incoming free definition link
  , DGNodeLab -> Maybe Node
dgn_nf :: Maybe Node         -- normal form, for Theorem-Hide-Shift
  , DGNodeLab -> Maybe GMorphism
dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature
  , DGNodeLab -> Maybe Node
dgn_freenf :: Maybe Node -- normal form for freeness
  , DGNodeLab -> Maybe GMorphism
dgn_phi :: Maybe GMorphism -- morphism from signature to nffree signature
  , DGNodeLab -> DGNodeInfo
nodeInfo :: DGNodeInfo
  , DGNodeLab -> NodeMod
nodeMod :: NodeMod
  , DGNodeLab -> Maybe XNode
xnode :: Maybe XGraph.XNode
  , DGNodeLab -> Maybe (MVar ())
dgn_lock :: Maybe (MVar ())
  } deriving Typeable

instance Show DGNodeLab where
  show :: DGNodeLab -> String
show _ = "<a DG node label>"

isDGRef :: DGNodeLab -> Bool
isDGRef :: DGNodeLab -> Bool
isDGRef l :: DGNodeLab
l = case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
l of
    DGNode {} -> Bool
False
    DGRef {} -> Bool
True

sensWithKind :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)
             -> G_theory -> [String]
sensWithKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> G_theory -> [String]
sensWithKind f :: forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
f (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Map k a -> [k]
Map.keys (ThSens sentence (AnyComorphism, BasicProof) -> [String])
-> ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall a b. (a -> b) -> a -> b
$ (SenStatus sentence (AnyComorphism, BasicProof) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenStatus sentence (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
f ThSens sentence (AnyComorphism, BasicProof)
sens

hasSenKind :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)
           -> DGNodeLab -> Bool
hasSenKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> DGNodeLab -> Bool
hasSenKind f :: forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
f = Bool -> Bool
not (Bool -> Bool) -> (DGNodeLab -> Bool) -> DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> (DGNodeLab -> [String]) -> DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> G_theory -> [String]
sensWithKind forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
f (G_theory -> [String])
-> (DGNodeLab -> G_theory) -> DGNodeLab -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> G_theory
dgn_theory

-- | test if a given node label has local open goals
hasOpenGoals :: DGNodeLab -> Bool
hasOpenGoals :: DGNodeLab -> Bool
hasOpenGoals = (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool)
-> DGNodeLab -> Bool
hasSenKind (\ s :: SenStatus a (AnyComorphism, BasicProof)
s -> Bool -> Bool
not (SenStatus a (AnyComorphism, BasicProof) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenStatus a (AnyComorphism, BasicProof)
s) Bool -> Bool -> Bool
&& Bool -> Bool
not (SenStatus a (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenStatus a (AnyComorphism, BasicProof)
s))

-- | check if the node has an internal name
isInternalNode :: DGNodeLab -> Bool
isInternalNode :: DGNodeLab -> Bool
isInternalNode DGNodeLab {dgn_name :: DGNodeLab -> NodeName
dgn_name = NodeName
n} = NodeName -> Bool
isInternal NodeName
n

getNodeConsStatus :: DGNodeLab -> ConsStatus
getNodeConsStatus :: DGNodeLab -> ConsStatus
getNodeConsStatus lbl :: DGNodeLab
lbl = case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lbl of
   DGRef {} -> Conservativity -> ConsStatus
mkConsStatus Conservativity
None
   DGNode { node_cons_status :: DGNodeInfo -> ConsStatus
node_cons_status = ConsStatus
c } -> ConsStatus
c

getNodeCons :: DGNodeLab -> Conservativity
getNodeCons :: DGNodeLab -> Conservativity
getNodeCons = ConsStatus -> Conservativity
getConsOfStatus (ConsStatus -> Conservativity)
-> (DGNodeLab -> ConsStatus) -> DGNodeLab -> Conservativity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> ConsStatus
getNodeConsStatus

-- | returns the Conservativity if the given node has one, otherwise none
getNodeConservativity :: LNode DGNodeLab -> Conservativity
getNodeConservativity :: LNode DGNodeLab -> Conservativity
getNodeConservativity = DGNodeLab -> Conservativity
getNodeCons (DGNodeLab -> Conservativity)
-> (LNode DGNodeLab -> DGNodeLab)
-> LNode DGNodeLab
-> Conservativity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd

{- | test if a node conservativity is open,
return input for refs or nodes with normal forms -}
hasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus b :: Bool
b lbl :: DGNodeLab
lbl = if Maybe Node -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Node -> Bool) -> Maybe Node -> Bool
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Maybe Node
dgn_nf DGNodeLab
lbl then Bool
b else
  Bool -> ConsStatus -> Bool
hasOpenConsStatus Bool
b (ConsStatus -> Bool) -> ConsStatus -> Bool
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> ConsStatus
getNodeConsStatus DGNodeLab
lbl

markNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistency newc :: Conservativity
newc str :: String
str dgnode :: DGNodeLab
dgnode = DGNodeLab
dgnode
  { nodeInfo :: DGNodeInfo
nodeInfo = case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
dgnode of
      ninfo :: DGNodeInfo
ninfo@DGNode { node_cons_status :: DGNodeInfo -> ConsStatus
node_cons_status = ConsStatus c :: Conservativity
c pc :: Conservativity
pc thm :: ThmLinkStatus
thm } ->
          if Conservativity
pc Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
newc Bool -> Bool -> Bool
&& ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
thm then DGNodeInfo
ninfo else
          DGNodeInfo
ninfo { node_cons_status :: ConsStatus
node_cons_status = Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
c Conservativity
newc
                  (ThmLinkStatus -> ConsStatus) -> ThmLinkStatus -> ConsStatus
forall a b. (a -> b) -> a -> b
$ DGRule -> ProofBasis -> ThmLinkStatus
Proven (String -> DGRule
DGRule (String -> DGRule) -> String -> DGRule
forall a b. (a -> b) -> a -> b
$ Conservativity -> String
showConsistencyStatus Conservativity
newc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str)
                    ProofBasis
emptyProofBasis }
      ninfo :: DGNodeInfo
ninfo -> DGNodeInfo
ninfo }

markNodeConsistent :: String -> DGNodeLab -> DGNodeLab
markNodeConsistent :: String -> DGNodeLab -> DGNodeLab
markNodeConsistent = Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistency Conservativity
Cons

markNodeInconsistent :: String -> DGNodeLab -> DGNodeLab
markNodeInconsistent :: String -> DGNodeLab -> DGNodeLab
markNodeInconsistent = Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistency Conservativity
Inconsistent

-- | creates a DGNodeType from a DGNodeLab
getRealDGNodeType :: DGNodeLab -> DGNodeType
getRealDGNodeType :: DGNodeLab -> DGNodeType
getRealDGNodeType dgnlab :: DGNodeLab
dgnlab = DGNodeType :: Bool -> Bool -> Bool -> Bool -> DGNodeType
DGNodeType
  { isRefType :: Bool
isRefType = DGNodeLab -> Bool
isDGRef DGNodeLab
dgnlab
  , isProvenNode :: Bool
isProvenNode = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Bool
hasOpenGoals DGNodeLab
dgnlab
  , isProvenCons :: Bool
isProvenCons = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus Bool
False DGNodeLab
dgnlab
  , isInternalSpec :: Bool
isInternalSpec = DGNodeLab -> Bool
isInternalNode DGNodeLab
dgnlab }

-- | a wrapper for fitting morphisms with a trivial Eq instance
newtype Fitted = Fitted [G_mapping] deriving (Node -> Fitted -> ShowS
[Fitted] -> ShowS
Fitted -> String
(Node -> Fitted -> ShowS)
-> (Fitted -> String) -> ([Fitted] -> ShowS) -> Show Fitted
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Fitted] -> ShowS
$cshowList :: [Fitted] -> ShowS
show :: Fitted -> String
$cshow :: Fitted -> String
showsPrec :: Node -> Fitted -> ShowS
$cshowsPrec :: Node -> Fitted -> ShowS
Show, Typeable)

instance Eq Fitted where
  _ == :: Fitted -> Fitted -> Bool
== _ = Bool
True

data DGLinkOrigin =
    SeeTarget
  | SeeSource
  | TEST
  | DGLinkVerif
  | DGImpliesLink
  | DGLinkExtension
  | DGLinkTranslation
  | DGLinkClosedLenv
  | DGLinkImports
  | DGLinkIntersect
  | DGLinkMorph IRI
  | DGLinkInst IRI Fitted
  | DGLinkInstArg IRI
  | DGLinkView IRI Fitted
  | DGLinkAlign IRI
  | DGLinkFitView IRI
  | DGLinkFitViewImp IRI
  | DGLinkProof
  | DGLinkFlatteningUnion
  | DGLinkFlatteningRename
  | DGLinkRefinement IRI
    deriving (Node -> DGLinkOrigin -> ShowS
[DGLinkOrigin] -> ShowS
DGLinkOrigin -> String
(Node -> DGLinkOrigin -> ShowS)
-> (DGLinkOrigin -> String)
-> ([DGLinkOrigin] -> ShowS)
-> Show DGLinkOrigin
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGLinkOrigin] -> ShowS
$cshowList :: [DGLinkOrigin] -> ShowS
show :: DGLinkOrigin -> String
$cshow :: DGLinkOrigin -> String
showsPrec :: Node -> DGLinkOrigin -> ShowS
$cshowsPrec :: Node -> DGLinkOrigin -> ShowS
Show, DGLinkOrigin -> DGLinkOrigin -> Bool
(DGLinkOrigin -> DGLinkOrigin -> Bool)
-> (DGLinkOrigin -> DGLinkOrigin -> Bool) -> Eq DGLinkOrigin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGLinkOrigin -> DGLinkOrigin -> Bool
$c/= :: DGLinkOrigin -> DGLinkOrigin -> Bool
== :: DGLinkOrigin -> DGLinkOrigin -> Bool
$c== :: DGLinkOrigin -> DGLinkOrigin -> Bool
Eq, Typeable)

{- | Link types of development graphs,
     Sect. IV:4.2 of the CASL Reference Manual explains them in depth. -}
data DGLinkType =
    ScopedLink Scope LinkKind ConsStatus
  | HidingDefLink
  | FreeOrCofreeDefLink FreeOrCofree MaybeNode -- the "parameter" node
  | HidingFreeOrCofreeThm (Maybe FreeOrCofree) Node GMorphism ThmLinkStatus
    {- DGLink S1 S2 m2 (DGLinkType m1 p) n
    corresponds to a span of morphisms
    S1 <--m1-- S --m2--> S2 -}
    deriving (Node -> DGLinkType -> ShowS
[DGLinkType] -> ShowS
DGLinkType -> String
(Node -> DGLinkType -> ShowS)
-> (DGLinkType -> String)
-> ([DGLinkType] -> ShowS)
-> Show DGLinkType
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGLinkType] -> ShowS
$cshowList :: [DGLinkType] -> ShowS
show :: DGLinkType -> String
$cshow :: DGLinkType -> String
showsPrec :: Node -> DGLinkType -> ShowS
$cshowsPrec :: Node -> DGLinkType -> ShowS
Show, DGLinkType -> DGLinkType -> Bool
(DGLinkType -> DGLinkType -> Bool)
-> (DGLinkType -> DGLinkType -> Bool) -> Eq DGLinkType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGLinkType -> DGLinkType -> Bool
$c/= :: DGLinkType -> DGLinkType -> Bool
== :: DGLinkType -> DGLinkType -> Bool
$c== :: DGLinkType -> DGLinkType -> Bool
Eq, Typeable)

-- | extract theorem link status from link type
thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus t :: DGLinkType
t = case DGLinkType
t of
    ScopedLink _ (ThmLink s :: ThmLinkStatus
s) _ -> ThmLinkStatus -> Maybe ThmLinkStatus
forall a. a -> Maybe a
Just ThmLinkStatus
s
    HidingFreeOrCofreeThm _ _ _ s :: ThmLinkStatus
s -> ThmLinkStatus -> Maybe ThmLinkStatus
forall a. a -> Maybe a
Just ThmLinkStatus
s
    _ -> Maybe ThmLinkStatus
forall a. Maybe a
Nothing

-- | extract proof basis from link type
thmProofBasis :: DGLinkType -> ProofBasis
thmProofBasis :: DGLinkType -> ProofBasis
thmProofBasis = ProofBasis
-> (ThmLinkStatus -> ProofBasis)
-> Maybe ThmLinkStatus
-> ProofBasis
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ProofBasis
emptyProofBasis ThmLinkStatus -> ProofBasis
proofBasisOfThmLinkStatus (Maybe ThmLinkStatus -> ProofBasis)
-> (DGLinkType -> Maybe ThmLinkStatus) -> DGLinkType -> ProofBasis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus

updThmProofBasis :: DGLinkType -> ProofBasis -> DGLinkType
updThmProofBasis :: DGLinkType -> ProofBasis -> DGLinkType
updThmProofBasis t :: DGLinkType
t pB :: ProofBasis
pB = case DGLinkType
t of
    ScopedLink sc :: Scope
sc (ThmLink s :: ThmLinkStatus
s) cs :: ConsStatus
cs -> Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc
      (ThmLinkStatus -> LinkKind
ThmLink (ThmLinkStatus -> LinkKind) -> ThmLinkStatus -> LinkKind
forall a b. (a -> b) -> a -> b
$ ThmLinkStatus -> ProofBasis -> ThmLinkStatus
updProofBasisOfThmLinkStatus ThmLinkStatus
s ProofBasis
pB) ConsStatus
cs
    HidingFreeOrCofreeThm h :: Maybe FreeOrCofree
h n :: Node
n m :: GMorphism
m s :: ThmLinkStatus
s -> Maybe FreeOrCofree
-> Node -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm Maybe FreeOrCofree
h Node
n GMorphism
m
      (ThmLinkStatus -> DGLinkType) -> ThmLinkStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ ThmLinkStatus -> ProofBasis -> ThmLinkStatus
updProofBasisOfThmLinkStatus ThmLinkStatus
s ProofBasis
pB
    _ -> DGLinkType
t

-- | link inscriptions in development graphs
data DGLinkLab = DGLink
  { DGLinkLab -> GMorphism
dgl_morphism :: GMorphism  -- signature morphism of link
  , DGLinkLab -> DGLinkType
dgl_type :: DGLinkType     -- type: local, global, def, thm?
  , DGLinkLab -> DGLinkOrigin
dgl_origin :: DGLinkOrigin -- origin in input language
  , DGLinkLab -> Bool
dglPending :: Bool        -- open proofs of edges in proof basis
  , DGLinkLab -> EdgeId
dgl_id :: EdgeId          -- id of the edge
  , DGLinkLab -> String
dglName :: String         -- name of the edge
  } deriving (DGLinkLab -> DGLinkLab -> Bool
(DGLinkLab -> DGLinkLab -> Bool)
-> (DGLinkLab -> DGLinkLab -> Bool) -> Eq DGLinkLab
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGLinkLab -> DGLinkLab -> Bool
$c/= :: DGLinkLab -> DGLinkLab -> Bool
== :: DGLinkLab -> DGLinkLab -> Bool
$c== :: DGLinkLab -> DGLinkLab -> Bool
Eq, Typeable)

instance Show DGLinkLab where
  show :: DGLinkLab -> String
show _ = "<a DG link label>"

mkDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> String -> EdgeId
         -> DGLinkLab
mkDGLink :: GMorphism
-> DGLinkType -> DGLinkOrigin -> String -> EdgeId -> DGLinkLab
mkDGLink mor :: GMorphism
mor ty :: DGLinkType
ty orig :: DGLinkOrigin
orig nn :: String
nn ei :: EdgeId
ei = DGLink :: GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Bool
-> EdgeId
-> String
-> DGLinkLab
DGLink
  { dgl_morphism :: GMorphism
dgl_morphism = GMorphism
mor
  , dgl_type :: DGLinkType
dgl_type = DGLinkType
ty
  , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
orig
  , dglPending :: Bool
dglPending = Bool
False
  , dgl_id :: EdgeId
dgl_id = EdgeId
ei
  , dglName :: String
dglName = String
nn }

-- | name a link
nameDGLink :: String -> DGLinkLab -> DGLinkLab
nameDGLink :: String -> DGLinkLab -> DGLinkLab
nameDGLink nn :: String
nn l :: DGLinkLab
l = DGLinkLab
l { dglName :: String
dglName = String
nn }

defDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
{- See svn-version 13804 for a naming concept which unfortunately introduced
same names for different links. -}
defDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink m :: GMorphism
m ty :: DGLinkType
ty orig :: DGLinkOrigin
orig = GMorphism
-> DGLinkType -> DGLinkOrigin -> String -> EdgeId -> DGLinkLab
mkDGLink GMorphism
m DGLinkType
ty DGLinkOrigin
orig "" EdgeId
defaultEdgeId

defDGLinkId :: GMorphism -> DGLinkType -> DGLinkOrigin -> EdgeId -> DGLinkLab
defDGLinkId :: GMorphism -> DGLinkType -> DGLinkOrigin -> EdgeId -> DGLinkLab
defDGLinkId m :: GMorphism
m ty :: DGLinkType
ty orig :: DGLinkOrigin
orig ei :: EdgeId
ei = (GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
m DGLinkType
ty DGLinkOrigin
orig) { dgl_id :: EdgeId
dgl_id = EdgeId
ei }

globDefLink :: GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink :: GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink m :: GMorphism
m = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
m DGLinkType
globalDef

-- | describe the link type of the label
getDGLinkType :: DGLinkLab -> String
getDGLinkType :: DGLinkLab -> String
getDGLinkType = DGEdgeType -> String
getDGEdgeTypeName (DGEdgeType -> String)
-> (DGLinkLab -> DGEdgeType) -> DGLinkLab -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGEdgeType
getRealDGLinkType

getHomEdgeType :: Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc
getHomEdgeType :: Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc
getHomEdgeType isPend :: Bool
isPend isHom :: Bool
isHom lt :: DGLinkType
lt = case DGLinkType
lt of
      ScopedLink scope :: Scope
scope lk :: LinkKind
lk cons :: ConsStatus
cons -> case LinkKind
lk of
          DefLink -> case Scope
scope of
            Local -> DGEdgeTypeModInc
LocalDef
            Global -> if Bool
isHom then DGEdgeTypeModInc
GlobalDef else DGEdgeTypeModInc
HetDef
          ThmLink st :: ThmLinkStatus
st -> ThmType :: ThmTypes -> Bool -> Bool -> Bool -> DGEdgeTypeModInc
ThmType
            { thmEdgeType :: ThmTypes
thmEdgeType = Scope -> Bool -> ThmTypes
GlobalOrLocalThm Scope
scope Bool
isHom
            , isProvenEdge :: Bool
isProvenEdge = ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
st
            , isConservativ :: Bool
isConservativ = ConsStatus -> Bool
isProvenConsStatusLink ConsStatus
cons
            , isPending :: Bool
isPending = Bool
isPend } -- needs to be checked
      HidingDefLink -> DGEdgeTypeModInc
HidingDef
      FreeOrCofreeDefLink fc :: FreeOrCofree
fc _ -> FreeOrCofree -> DGEdgeTypeModInc
FreeOrCofreeDef FreeOrCofree
fc
      HidingFreeOrCofreeThm mh :: Maybe FreeOrCofree
mh _ _ st :: ThmLinkStatus
st -> ThmType :: ThmTypes -> Bool -> Bool -> Bool -> DGEdgeTypeModInc
ThmType
        { thmEdgeType :: ThmTypes
thmEdgeType = case Maybe FreeOrCofree
mh of
            Nothing -> ThmTypes
HidingThm
            Just fc :: FreeOrCofree
fc -> FreeOrCofree -> ThmTypes
FreeOrCofreeThm FreeOrCofree
fc
        , isProvenEdge :: Bool
isProvenEdge = ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
st
        , isConservativ :: Bool
isConservativ = Bool
True
        , isPending :: Bool
isPending = Bool
isPend }

-- | creates a DGEdgeType from a DGLinkLab
getRealDGLinkType :: DGLinkLab -> DGEdgeType
getRealDGLinkType :: DGLinkLab -> DGEdgeType
getRealDGLinkType lnk :: DGLinkLab
lnk = let
  gmor :: GMorphism
gmor = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lnk
  in DGEdgeType :: DGEdgeTypeModInc -> Bool -> DGEdgeType
DGEdgeType
  { edgeTypeModInc :: DGEdgeTypeModInc
edgeTypeModInc = Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc
getHomEdgeType (DGLinkLab -> Bool
dglPending DGLinkLab
lnk) (GMorphism -> Bool
isHomogeneous GMorphism
gmor)
      (DGLinkType -> DGEdgeTypeModInc) -> DGLinkType -> DGEdgeTypeModInc
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lnk
  , isInc :: Bool
isInc = case GMorphism
gmor of
      GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _ -> cid -> Bool
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> Bool
isInclusionComorphism cid
cid Bool -> Bool -> Bool
&& morphism2 -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isInclusion morphism2
mor
  }

-- | return the proof basis of the given linklab
getProofBasis :: DGLinkLab -> ProofBasis
getProofBasis :: DGLinkLab -> ProofBasis
getProofBasis = DGLinkType -> ProofBasis
thmProofBasis (DGLinkType -> ProofBasis)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> ProofBasis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type

-- | set proof for theorem links
setProof :: ThmLinkStatus -> DGLinkType -> DGLinkType
setProof :: ThmLinkStatus -> DGLinkType -> DGLinkType
setProof p :: ThmLinkStatus
p lt :: DGLinkType
lt = case DGLinkType
lt of
    ScopedLink sc :: Scope
sc (ThmLink _) cs :: ConsStatus
cs -> Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc (ThmLinkStatus -> LinkKind
ThmLink ThmLinkStatus
p) ConsStatus
cs
    HidingFreeOrCofreeThm hm :: Maybe FreeOrCofree
hm n :: Node
n mor :: GMorphism
mor _ -> Maybe FreeOrCofree
-> Node -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm Maybe FreeOrCofree
hm Node
n GMorphism
mor ThmLinkStatus
p
    _ -> DGLinkType
lt

-- * methods to check the type of an edge

isProven :: DGLinkType -> Bool
isProven :: DGLinkType -> Bool
isProven edge :: DGLinkType
edge = case DGLinkType
edge of
    ScopedLink _ DefLink _ -> Bool
True
    _ -> case DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus DGLinkType
edge of
           Just (Proven _ _) -> Bool
True
           _ -> Bool
False

isGlobalEdge :: DGLinkType -> Bool
isGlobalEdge :: DGLinkType -> Bool
isGlobalEdge edge :: DGLinkType
edge = case DGLinkType
edge of
    ScopedLink Global _ _ -> Bool
True
    _ -> Bool
False

isGlobalThm :: DGLinkType -> Bool
isGlobalThm :: DGLinkType -> Bool
isGlobalThm edge :: DGLinkType
edge = case DGLinkType
edge of
    ScopedLink Global (ThmLink _) _ -> Bool
True
    _ -> Bool
False

isUnprovenGlobalThm :: DGLinkType -> Bool
isUnprovenGlobalThm :: DGLinkType -> Bool
isUnprovenGlobalThm lt :: DGLinkType
lt = case DGLinkType
lt of
    ScopedLink Global (ThmLink LeftOpen) _ -> Bool
True
    _ -> Bool
False

isLocalThm :: DGLinkType -> Bool
isLocalThm :: DGLinkType -> Bool
isLocalThm edge :: DGLinkType
edge = case DGLinkType
edge of
    ScopedLink Local (ThmLink _) _ -> Bool
True
    _ -> Bool
False

isUnprovenLocalThm :: DGLinkType -> Bool
isUnprovenLocalThm :: DGLinkType -> Bool
isUnprovenLocalThm lt :: DGLinkType
lt = case DGLinkType
lt of
    ScopedLink Local (ThmLink LeftOpen) _ -> Bool
True
    _ -> Bool
False

isUnprovenHidingThm :: DGLinkType -> Bool
isUnprovenHidingThm :: DGLinkType -> Bool
isUnprovenHidingThm lt :: DGLinkType
lt = case DGLinkType
lt of
    HidingFreeOrCofreeThm Nothing _ _ LeftOpen -> Bool
True
    _ -> Bool
False

isFreeEdge :: DGLinkType -> Bool
isFreeEdge :: DGLinkType -> Bool
isFreeEdge edge :: DGLinkType
edge = case DGLinkType
edge of
    FreeOrCofreeDefLink Free _ -> Bool
True
    _ -> Bool
False

isCofreeEdge :: DGLinkType -> Bool
isCofreeEdge :: DGLinkType -> Bool
isCofreeEdge edge :: DGLinkType
edge = case DGLinkType
edge of
    FreeOrCofreeDefLink Cofree _ -> Bool
True
    _ -> Bool
False

hasOutgoingFreeEdge :: DGraph -> Node -> Bool
hasOutgoingFreeEdge :: DGraph -> Node -> Bool
hasOutgoingFreeEdge dg :: DGraph
dg n :: Node
n =
 let nEdges :: [LEdge DGLinkLab]
nEdges = DGraph -> Node -> [LEdge DGLinkLab]
outDG DGraph
dg Node
n in
 Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([LEdge DGLinkLab] -> Bool) -> [LEdge DGLinkLab] -> Bool
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(_,_, e :: DGLinkLab
e) -> DGLinkType -> Bool
isFreeEdge (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
e) [LEdge DGLinkLab]
nEdges 

-- ** types for global environments

-- | import, formal parameters and united signature of formal params
data GenSig = GenSig MaybeNode [NodeSig] MaybeNode deriving (Node -> GenSig -> ShowS
[GenSig] -> ShowS
GenSig -> String
(Node -> GenSig -> ShowS)
-> (GenSig -> String) -> ([GenSig] -> ShowS) -> Show GenSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenSig] -> ShowS
$cshowList :: [GenSig] -> ShowS
show :: GenSig -> String
$cshow :: GenSig -> String
showsPrec :: Node -> GenSig -> ShowS
$cshowsPrec :: Node -> GenSig -> ShowS
Show, Typeable)

getGenSigNodes :: GenSig -> Set.Set Node
getGenSigNodes :: GenSig -> Set Node
getGenSigNodes (GenSig m1 :: MaybeNode
m1 ns :: [NodeSig]
ns m2 :: MaybeNode
m2) = [Set Node] -> Set Node
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
  [ MaybeNode -> Set Node
getMaybeNodes MaybeNode
m1
  , [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
$ (NodeSig -> Node) -> [NodeSig] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> Node
getNode [NodeSig]
ns
  , MaybeNode -> Set Node
getMaybeNodes MaybeNode
m2 ]

-- | genericity and body
data ExtGenSig = ExtGenSig
  { ExtGenSig -> GenSig
genericity :: GenSig
  , ExtGenSig -> NodeSig
extGenBody :: NodeSig }
  deriving (Node -> ExtGenSig -> ShowS
[ExtGenSig] -> ShowS
ExtGenSig -> String
(Node -> ExtGenSig -> ShowS)
-> (ExtGenSig -> String)
-> ([ExtGenSig] -> ShowS)
-> Show ExtGenSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtGenSig] -> ShowS
$cshowList :: [ExtGenSig] -> ShowS
show :: ExtGenSig -> String
$cshow :: ExtGenSig -> String
showsPrec :: Node -> ExtGenSig -> ShowS
$cshowsPrec :: Node -> ExtGenSig -> ShowS
Show, Typeable)

getExtGenSigNodes :: ExtGenSig -> Set.Set Node
getExtGenSigNodes :: ExtGenSig -> Set Node
getExtGenSigNodes (ExtGenSig g :: GenSig
g n :: NodeSig
n) = Node -> Set Node -> Set Node
forall a. Ord a => a -> Set a -> Set a
Set.insert (NodeSig -> Node
getNode NodeSig
n) (Set Node -> Set Node) -> Set Node -> Set Node
forall a b. (a -> b) -> a -> b
$ GenSig -> Set Node
getGenSigNodes GenSig
g

-- | source, morphism, parameterized target
data ExtViewSig = ExtViewSig NodeSig GMorphism ExtGenSig
  deriving (Node -> ExtViewSig -> ShowS
[ExtViewSig] -> ShowS
ExtViewSig -> String
(Node -> ExtViewSig -> ShowS)
-> (ExtViewSig -> String)
-> ([ExtViewSig] -> ShowS)
-> Show ExtViewSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtViewSig] -> ShowS
$cshowList :: [ExtViewSig] -> ShowS
show :: ExtViewSig -> String
$cshow :: ExtViewSig -> String
showsPrec :: Node -> ExtViewSig -> ShowS
$cshowsPrec :: Node -> ExtViewSig -> ShowS
Show, Typeable)

getExtViewSigNodes :: ExtViewSig -> Set.Set Node
getExtViewSigNodes :: ExtViewSig -> Set Node
getExtViewSigNodes (ExtViewSig n :: NodeSig
n _ e :: ExtGenSig
e) =
  Node -> Set Node -> Set Node
forall a. Ord a => a -> Set a -> Set a
Set.insert (NodeSig -> Node
getNode NodeSig
n) (Set Node -> Set Node) -> Set Node -> Set Node
forall a b. (a -> b) -> a -> b
$ ExtGenSig -> Set Node
getExtGenSigNodes ExtGenSig
e

{- ** types for architectural and unit specification analysis
    (as defined for basic static semantics in Chap. III:5.1) -}

data UnitSig = UnitSig [NodeSig] NodeSig (Maybe NodeSig)
  deriving (Node -> UnitSig -> ShowS
[UnitSig] -> ShowS
UnitSig -> String
(Node -> UnitSig -> ShowS)
-> (UnitSig -> String) -> ([UnitSig] -> ShowS) -> Show UnitSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnitSig] -> ShowS
$cshowList :: [UnitSig] -> ShowS
show :: UnitSig -> String
$cshow :: UnitSig -> String
showsPrec :: Node -> UnitSig -> ShowS
$cshowsPrec :: Node -> UnitSig -> ShowS
Show, UnitSig -> UnitSig -> Bool
(UnitSig -> UnitSig -> Bool)
-> (UnitSig -> UnitSig -> Bool) -> Eq UnitSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnitSig -> UnitSig -> Bool
$c/= :: UnitSig -> UnitSig -> Bool
== :: UnitSig -> UnitSig -> Bool
$c== :: UnitSig -> UnitSig -> Bool
Eq, Typeable)
{- Maybe NodeSig stores the union of the parameters
the node is needed for consistency checks -}

getUnitSigNodes :: UnitSig -> Set.Set Node
getUnitSigNodes :: UnitSig -> Set Node
getUnitSigNodes (UnitSig ns :: [NodeSig]
ns n :: NodeSig
n m :: Maybe NodeSig
m) =
  [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
$ (NodeSig -> Node) -> [NodeSig] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> Node
getNode (NodeSig
n NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
ns [NodeSig] -> [NodeSig] -> [NodeSig]
forall a. [a] -> [a] -> [a]
++ Maybe NodeSig -> [NodeSig]
forall a. Maybe a -> [a]
maybeToList Maybe NodeSig
m)

data ImpUnitSigOrSig = ImpUnitSig MaybeNode UnitSig | Sig NodeSig
   deriving (Node -> ImpUnitSigOrSig -> ShowS
[ImpUnitSigOrSig] -> ShowS
ImpUnitSigOrSig -> String
(Node -> ImpUnitSigOrSig -> ShowS)
-> (ImpUnitSigOrSig -> String)
-> ([ImpUnitSigOrSig] -> ShowS)
-> Show ImpUnitSigOrSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ImpUnitSigOrSig] -> ShowS
$cshowList :: [ImpUnitSigOrSig] -> ShowS
show :: ImpUnitSigOrSig -> String
$cshow :: ImpUnitSigOrSig -> String
showsPrec :: Node -> ImpUnitSigOrSig -> ShowS
$cshowsPrec :: Node -> ImpUnitSigOrSig -> ShowS
Show, ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool
(ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool)
-> (ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool)
-> Eq ImpUnitSigOrSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool
$c/= :: ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool
== :: ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool
$c== :: ImpUnitSigOrSig -> ImpUnitSigOrSig -> Bool
Eq, Typeable)

type StUnitCtx = Map.Map IRI ImpUnitSigOrSig

emptyStUnitCtx :: StUnitCtx
emptyStUnitCtx :: StUnitCtx
emptyStUnitCtx = StUnitCtx
forall k a. Map k a
Map.empty

{- data ArchSig = ArchSig StUnitCtx UnitSig deriving (Show, Typeable)
this type is superseeded by RefSig -}

type RefSigMap = Map.Map IRI RefSig

getSigMapNodes :: RefSigMap -> Set.Set Node
getSigMapNodes :: RefSigMap -> Set Node
getSigMapNodes = [Set Node] -> Set Node
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Node] -> Set Node)
-> (RefSigMap -> [Set Node]) -> RefSigMap -> Set Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RefSig -> Set Node) -> [RefSig] -> [Set Node]
forall a b. (a -> b) -> [a] -> [b]
map RefSig -> Set Node
getRefSigNodes ([RefSig] -> [Set Node])
-> (RefSigMap -> [RefSig]) -> RefSigMap -> [Set Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefSigMap -> [RefSig]
forall k a. Map k a -> [a]
Map.elems

type BStContext = Map.Map IRI RefSig

getBStContextNodes :: BStContext -> Set.Set Node
getBStContextNodes :: RefSigMap -> Set Node
getBStContextNodes = [Set Node] -> Set Node
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Node] -> Set Node)
-> (RefSigMap -> [Set Node]) -> RefSigMap -> Set Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RefSig -> Set Node) -> [RefSig] -> [Set Node]
forall a b. (a -> b) -> [a] -> [b]
map RefSig -> Set Node
getRefSigNodes ([RefSig] -> [Set Node])
-> (RefSigMap -> [RefSig]) -> RefSigMap -> [Set Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefSigMap -> [RefSig]
forall k a. Map k a -> [a]
Map.elems

-- there should be only BranchRefSigs

data RefSig = BranchRefSig RTPointer (UnitSig, Maybe BranchSig)
            | ComponentRefSig RTPointer RefSigMap
              deriving (RefSig -> RefSig -> Bool
(RefSig -> RefSig -> Bool)
-> (RefSig -> RefSig -> Bool) -> Eq RefSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RefSig -> RefSig -> Bool
$c/= :: RefSig -> RefSig -> Bool
== :: RefSig -> RefSig -> Bool
$c== :: RefSig -> RefSig -> Bool
Eq, Typeable)

getRefSigNodes :: RefSig -> Set.Set Node
getRefSigNodes :: RefSig -> Set Node
getRefSigNodes rs :: RefSig
rs = case RefSig
rs of
  BranchRefSig _ (u :: UnitSig
u, m :: Maybe BranchSig
m) -> Set Node -> Set Node -> Set Node
forall a. Ord a => Set a -> Set a -> Set a
Set.union (UnitSig -> Set Node
getUnitSigNodes UnitSig
u)
    (Set Node -> Set Node) -> Set Node -> Set Node
forall a b. (a -> b) -> a -> b
$ Set Node -> (BranchSig -> Set Node) -> Maybe BranchSig -> Set Node
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Node
forall a. Set a
Set.empty BranchSig -> Set Node
getBranchSigNodes Maybe BranchSig
m
  ComponentRefSig _ m :: RefSigMap
m -> RefSigMap -> Set Node
getSigMapNodes RefSigMap
m

instance Show RefSig where
-- made this instance for debugging purposes
  show :: RefSig -> String
show (BranchRefSig _ (usig :: UnitSig
usig, mbsig :: Maybe BranchSig
mbsig)) =
    let bStr :: String
bStr = case Maybe BranchSig
mbsig of
                 Nothing -> "Bottom\n "
                 Just bsig :: BranchSig
bsig -> case BranchSig
bsig of
                   UnitSigAsBranchSig u :: UnitSig
u ->
                     if UnitSig
u UnitSig -> UnitSig -> Bool
forall a. Eq a => a -> a -> Bool
== UnitSig
usig then "same"
                     else "UnitSigAsBranch:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitSig -> ShowS
forall a. Show a => a -> ShowS
shows UnitSig
u "\n "
                   BranchStaticContext bst :: RefSigMap
bst ->
                     (String -> ShowS) -> String -> [String] -> String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl String -> ShowS
forall a. [a] -> [a] -> [a]
(++) "branching: "
                     ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((IRI, RefSig) -> String) -> [(IRI, RefSig)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: IRI
n, s :: RefSig
s) -> IRI -> ShowS
forall a. Show a => a -> ShowS
shows IRI
n " mapped to\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ RefSig -> ShowS
forall a. Show a => a -> ShowS
shows RefSig
s "\n")
                     ([(IRI, RefSig)] -> [String]) -> [(IRI, RefSig)] -> [String]
forall a b. (a -> b) -> a -> b
$ RefSigMap -> [(IRI, RefSig)]
forall k a. Map k a -> [(k, a)]
Map.toList RefSigMap
bst
    in
      "Branch: \n before refinement:\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitSig -> String
forall a. Show a => a -> String
show UnitSig
usig String -> ShowS
forall a. [a] -> [a] -> [a]
++
      "\n  after refinement: \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
bStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n"
  show (ComponentRefSig _ rsm :: RefSigMap
rsm) =
   (String -> ShowS) -> String -> [String] -> String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl String -> ShowS
forall a. [a] -> [a] -> [a]
(++) "CompRefSig:" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((IRI, RefSig) -> String) -> [(IRI, RefSig)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: (IRI, RefSig)
n -> (IRI, RefSig) -> String
forall a. Show a => a -> String
show (IRI, RefSig)
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n ") ([(IRI, RefSig)] -> [String]) -> [(IRI, RefSig)] -> [String]
forall a b. (a -> b) -> a -> b
$
     RefSigMap -> [(IRI, RefSig)]
forall k a. Map k a -> [(k, a)]
Map.toList RefSigMap
rsm

getPointerFromRef :: RefSig -> RTPointer
getPointerFromRef :: RefSig -> RTPointer
getPointerFromRef (BranchRefSig p :: RTPointer
p _) = RTPointer
p
getPointerFromRef (ComponentRefSig p :: RTPointer
p _) = RTPointer
p

setPointerInRef :: RefSig -> RTPointer -> RefSig
setPointerInRef :: RefSig -> RTPointer -> RefSig
setPointerInRef (BranchRefSig _ x :: (UnitSig, Maybe BranchSig)
x) y :: RTPointer
y = RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
y (UnitSig, Maybe BranchSig)
x
setPointerInRef (ComponentRefSig _ x :: RefSigMap
x) y :: RTPointer
y = RTPointer -> RefSigMap -> RefSig
ComponentRefSig RTPointer
y RefSigMap
x

setUnitSigInRef :: RefSig -> UnitSig -> RefSig
setUnitSigInRef :: RefSig -> UnitSig -> RefSig
setUnitSigInRef (BranchRefSig x :: RTPointer
x (_, y :: Maybe BranchSig
y)) usig :: UnitSig
usig = RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
x (UnitSig
usig, Maybe BranchSig
y)
setUnitSigInRef _ _ = String -> RefSig
forall a. HasCallStack => String -> a
error "setUnitSigInRef"

getUnitSigFromRef :: RefSig -> Result UnitSig
getUnitSigFromRef :: RefSig -> Result UnitSig
getUnitSigFromRef (BranchRefSig _ (usig :: UnitSig
usig, _)) = UnitSig -> Result UnitSig
forall (m :: * -> *) a. Monad m => a -> m a
return UnitSig
usig
getUnitSigFromRef (ComponentRefSig _ rsm :: RefSigMap
rsm) =
   String -> Result UnitSig
forall a. HasCallStack => String -> a
error (String -> Result UnitSig) -> String -> Result UnitSig
forall a b. (a -> b) -> a -> b
$ "getUnitSigFromRef:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [IRI] -> String
forall a. Show a => a -> String
show (RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsm)

mkRefSigFromUnit :: UnitSig -> RefSig
mkRefSigFromUnit :: UnitSig -> RefSig
mkRefSigFromUnit usig :: UnitSig
usig = RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
RTNone
                          (UnitSig
usig, BranchSig -> Maybe BranchSig
forall a. a -> Maybe a
Just (BranchSig -> Maybe BranchSig) -> BranchSig -> Maybe BranchSig
forall a b. (a -> b) -> a -> b
$ UnitSig -> BranchSig
UnitSigAsBranchSig UnitSig
usig)

mkBotSigFromUnit :: UnitSig -> RefSig
mkBotSigFromUnit :: UnitSig -> RefSig
mkBotSigFromUnit usig :: UnitSig
usig = RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
RTNone (UnitSig
usig, Maybe BranchSig
forall a. Maybe a
Nothing)

data BranchSig = UnitSigAsBranchSig UnitSig
               | BranchStaticContext BStContext
                 deriving (Node -> BranchSig -> ShowS
[BranchSig] -> ShowS
BranchSig -> String
(Node -> BranchSig -> ShowS)
-> (BranchSig -> String)
-> ([BranchSig] -> ShowS)
-> Show BranchSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BranchSig] -> ShowS
$cshowList :: [BranchSig] -> ShowS
show :: BranchSig -> String
$cshow :: BranchSig -> String
showsPrec :: Node -> BranchSig -> ShowS
$cshowsPrec :: Node -> BranchSig -> ShowS
Show, BranchSig -> BranchSig -> Bool
(BranchSig -> BranchSig -> Bool)
-> (BranchSig -> BranchSig -> Bool) -> Eq BranchSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BranchSig -> BranchSig -> Bool
$c/= :: BranchSig -> BranchSig -> Bool
== :: BranchSig -> BranchSig -> Bool
$c== :: BranchSig -> BranchSig -> Bool
Eq, Typeable)

getBranchSigNodes :: BranchSig -> Set.Set Node
getBranchSigNodes :: BranchSig -> Set Node
getBranchSigNodes bs :: BranchSig
bs = case BranchSig
bs of
  UnitSigAsBranchSig u :: UnitSig
u -> UnitSig -> Set Node
getUnitSigNodes UnitSig
u
  BranchStaticContext b :: RefSigMap
b -> RefSigMap -> Set Node
getBStContextNodes RefSigMap
b

type RefStUnitCtx = Map.Map IRI RefSig
-- only BranchRefSigs allowed

emptyRefStUnitCtx :: RefStUnitCtx
emptyRefStUnitCtx :: RefSigMap
emptyRefStUnitCtx = RefSigMap
forall k a. Map k a
Map.empty

-- Auxiliaries for refinament signatures composition
matchesContext :: RefSigMap -> BStContext -> Bool
matchesContext :: RefSigMap -> RefSigMap -> Bool
matchesContext rsmap :: RefSigMap
rsmap bstc :: RefSigMap
bstc =
  Bool -> Bool
not ((IRI -> Bool) -> [IRI] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (IRI -> [IRI] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
bstc) ([IRI] -> Bool) -> [IRI] -> Bool
forall a b. (a -> b) -> a -> b
$ RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap)
  Bool -> Bool -> Bool
&& [IRI] -> RefSigMap -> RefSigMap -> Bool
namesMatchCtx (RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap) RefSigMap
bstc RefSigMap
rsmap

equalSigs :: UnitSig -> UnitSig -> Bool
equalSigs :: UnitSig -> UnitSig -> Bool
equalSigs (UnitSig ls1 :: [NodeSig]
ls1 ns1 :: NodeSig
ns1 _) (UnitSig ls2 :: [NodeSig]
ls2 ns2 :: NodeSig
ns2 _) =
  [NodeSig] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [NodeSig]
ls1 Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== [NodeSig] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [NodeSig]
ls2 Bool -> Bool -> Bool
&& NodeSig -> G_sign
getSig NodeSig
ns1 G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== NodeSig -> G_sign
getSig NodeSig
ns2
    Bool -> Bool -> Bool
&& ((NodeSig, NodeSig) -> Bool) -> [(NodeSig, NodeSig)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (x1 :: NodeSig
x1, x2 :: NodeSig
x2) -> NodeSig -> G_sign
getSig NodeSig
x1 G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== NodeSig -> G_sign
getSig NodeSig
x2) ([NodeSig] -> [NodeSig] -> [(NodeSig, NodeSig)]
forall a b. [a] -> [b] -> [(a, b)]
zip [NodeSig]
ls1 [NodeSig]
ls2)

namesMatchCtx :: [IRI] -> BStContext -> RefSigMap -> Bool
namesMatchCtx :: [IRI] -> RefSigMap -> RefSigMap -> Bool
namesMatchCtx [] _ _ = Bool
True
namesMatchCtx (un :: IRI
un : unitNames :: [IRI]
unitNames) bstc :: RefSigMap
bstc rsmap :: RefSigMap
rsmap = -- trace ("nMC:" ++ show un)$
 case RefSig -> IRI -> RefSigMap -> RefSig
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> RefSig
forall a. HasCallStack => String -> a
error "namesMatchCtx")
            IRI
un RefSigMap
bstc of
  BranchRefSig _ (_usig :: UnitSig
_usig, mbsig :: Maybe BranchSig
mbsig) -> case Maybe BranchSig
mbsig of
    Nothing -> Bool
False -- should not be the case
    Just bsig :: BranchSig
bsig -> case BranchSig
bsig of
     UnitSigAsBranchSig usig' :: UnitSig
usig' ->
       case RefSig -> IRI -> RefSigMap -> RefSig
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> RefSig
forall a. HasCallStack => String -> a
error "USABS") IRI
un RefSigMap
rsmap of
         BranchRefSig _ (usig'' :: UnitSig
usig'', _mbsig' :: Maybe BranchSig
_mbsig') -> UnitSig -> UnitSig -> Bool
equalSigs UnitSig
usig' UnitSig
usig'' Bool -> Bool -> Bool
&&
                                         [IRI] -> RefSigMap -> RefSigMap -> Bool
namesMatchCtx [IRI]
unitNames RefSigMap
bstc RefSigMap
rsmap
         _ -> Bool
False
     BranchStaticContext bstc' :: RefSigMap
bstc' ->
       case RefSigMap
rsmap RefSigMap -> IRI -> RefSig
forall k a. Ord k => Map k a -> k -> a
Map.! IRI
un of
         ComponentRefSig _ rsmap' :: RefSigMap
rsmap' ->
                RefSigMap -> RefSigMap -> Bool
matchesContext RefSigMap
rsmap' RefSigMap
bstc' Bool -> Bool -> Bool
&&
                 [IRI] -> RefSigMap -> RefSigMap -> Bool
namesMatchCtx [IRI]
unitNames RefSigMap
bstc RefSigMap
rsmap
  {- This is where I introduce something new wrt to the original paper:
  if bstc' has only one element
  it suffices to have the signature of that element
  matching the signature from rsmap' -}
         _ -> RefSigMap -> Node
forall k a. Map k a -> Node
Map.size RefSigMap
bstc' Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
&&
                let un1 :: IRI
un1 = [IRI] -> IRI
forall a. [a] -> a
head ([IRI] -> IRI) -> [IRI] -> IRI
forall a b. (a -> b) -> a -> b
$ RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
bstc'
                    rsmap' :: RefSigMap
rsmap' = (IRI -> IRI) -> RefSigMap -> RefSigMap
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\ x :: IRI
x -> if IRI
x IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
un then IRI
un1 else IRI
x)
                               RefSigMap
rsmap
                in [IRI] -> RefSigMap -> RefSigMap -> Bool
namesMatchCtx [IRI
un1] RefSigMap
bstc' RefSigMap
rsmap' Bool -> Bool -> Bool
&&
                   [IRI] -> RefSigMap -> RefSigMap -> Bool
namesMatchCtx [IRI]
unitNames RefSigMap
bstc RefSigMap
rsmap
  _ -> Bool
False -- this should never be the case

modifyCtx :: [IRI] -> RefSigMap -> BStContext -> BStContext
modifyCtx :: [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [] _ bstc :: RefSigMap
bstc = RefSigMap
bstc
modifyCtx (un :: IRI
un : unitNames :: [IRI]
unitNames) rsmap :: RefSigMap
rsmap bstc :: RefSigMap
bstc =
 case RefSigMap
bstc RefSigMap -> IRI -> RefSig
forall k a. Ord k => Map k a -> k -> a
Map.! IRI
un of
   BranchRefSig n1 :: RTPointer
n1 (usig :: UnitSig
usig, mbsig :: Maybe BranchSig
mbsig) -> case Maybe BranchSig
mbsig of
     Nothing -> [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI]
unitNames RefSigMap
rsmap RefSigMap
bstc -- should not be the case
     Just bsig :: BranchSig
bsig -> case BranchSig
bsig of
       UnitSigAsBranchSig usig' :: UnitSig
usig' ->
          case RefSigMap
rsmap RefSigMap -> IRI -> RefSig
forall k a. Ord k => Map k a -> k -> a
Map.! IRI
un of
            BranchRefSig n2 :: RTPointer
n2 (usig'' :: UnitSig
usig'', bsig'' :: Maybe BranchSig
bsig'') -> if UnitSig -> UnitSig -> Bool
equalSigs UnitSig
usig' UnitSig
usig'' then
                 [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI]
unitNames RefSigMap
rsmap (RefSigMap -> RefSigMap) -> RefSigMap -> RefSigMap
forall a b. (a -> b) -> a -> b
$
                 IRI -> RefSig -> RefSigMap -> RefSigMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
un (RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig (RTPointer -> RTPointer -> RTPointer
compPointer RTPointer
n1 RTPointer
n2)
                            (UnitSig
usig, Maybe BranchSig
bsig'')) RefSigMap
bstc -- was usig'
                else String -> RefSigMap
forall a. HasCallStack => String -> a
error "illegal composition"
            _ -> [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI]
unitNames RefSigMap
rsmap RefSigMap
bstc
       BranchStaticContext bstc' :: RefSigMap
bstc' ->
          case RefSigMap
rsmap RefSigMap -> IRI -> RefSig
forall k a. Ord k => Map k a -> k -> a
Map.! IRI
un of
            ComponentRefSig n2 :: RTPointer
n2 rsmap' :: RefSigMap
rsmap' -> [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI]
unitNames RefSigMap
rsmap (RefSigMap -> RefSigMap) -> RefSigMap -> RefSigMap
forall a b. (a -> b) -> a -> b
$
             IRI -> RefSig -> RefSigMap -> RefSigMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
un
             (RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig (RTPointer -> RTPointer -> RTPointer
compPointer RTPointer
n1 RTPointer
n2) (UnitSig
usig, BranchSig -> Maybe BranchSig
forall a. a -> Maybe a
Just (BranchSig -> Maybe BranchSig) -> BranchSig -> Maybe BranchSig
forall a b. (a -> b) -> a -> b
$
               RefSigMap -> BranchSig
BranchStaticContext (RefSigMap -> BranchSig) -> RefSigMap -> BranchSig
forall a b. (a -> b) -> a -> b
$ [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx (RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap') RefSigMap
rsmap' RefSigMap
bstc'))
             RefSigMap
bstc
            _ -> let f :: RefSigMap
f = if RefSigMap -> Node
forall k a. Map k a -> Node
Map.size RefSigMap
bstc' Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then
                             let un1 :: IRI
un1 = [IRI] -> IRI
forall a. [a] -> a
head ([IRI] -> IRI) -> [IRI] -> IRI
forall a b. (a -> b) -> a -> b
$ RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
bstc'
                                 rsmap' :: RefSigMap
rsmap' = (IRI -> IRI) -> RefSigMap -> RefSigMap
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys
                                          (\ x :: IRI
x -> if IRI
x IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
un then IRI
un1 else IRI
x)
                                           RefSigMap
rsmap
                                 bstc'' :: RefSigMap
bstc'' = [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI
un1] RefSigMap
rsmap' RefSigMap
bstc'
                             in IRI -> RefSig -> RefSigMap
forall k a. k -> a -> Map k a
Map.singleton IRI
un (RefSig -> RefSigMap) -> RefSig -> RefSigMap
forall a b. (a -> b) -> a -> b
$
                                RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
RTNone (UnitSig
usig, BranchSig -> Maybe BranchSig
forall a. a -> Maybe a
Just
                                (BranchSig -> Maybe BranchSig) -> BranchSig -> Maybe BranchSig
forall a b. (a -> b) -> a -> b
$ RefSigMap -> BranchSig
BranchStaticContext RefSigMap
bstc'')
                           else RefSigMap
forall k a. Map k a
Map.empty
                 in RefSigMap -> RefSigMap -> RefSigMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RefSigMap
f (RefSigMap -> RefSigMap) -> RefSigMap -> RefSigMap
forall a b. (a -> b) -> a -> b
$ [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI]
unitNames RefSigMap
rsmap RefSigMap
bstc
   _ -> [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx [IRI]
unitNames RefSigMap
rsmap RefSigMap
bstc -- same as above

-- Signature composition
refSigComposition :: RefSig -> RefSig -> Result RefSig
refSigComposition :: RefSig -> RefSig -> Result RefSig
refSigComposition (BranchRefSig n1 :: RTPointer
n1 (usig1 :: UnitSig
usig1, Just (UnitSigAsBranchSig usig2 :: UnitSig
usig2)))
                  (BranchRefSig n2 :: RTPointer
n2 (usig3 :: UnitSig
usig3, bsig :: Maybe BranchSig
bsig)) =
  if UnitSig -> UnitSig -> Bool
equalSigs UnitSig
usig2 UnitSig
usig3 then
    RefSig -> Result RefSig
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> Result RefSig) -> RefSig -> Result RefSig
forall a b. (a -> b) -> a -> b
$ RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig (RTPointer -> RTPointer -> RTPointer
compPointer RTPointer
n1 RTPointer
n2) (UnitSig
usig1, Maybe BranchSig
bsig)
    else String -> Result RefSig
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result RefSig) -> String -> Result RefSig
forall a b. (a -> b) -> a -> b
$ "Signatures: \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitSig -> String
forall a. Show a => a -> String
show UnitSig
usig2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n and \n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitSig -> String
forall a. Show a => a -> String
show UnitSig
usig3 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                "  do not compose"

refSigComposition _rsig1 :: RefSig
_rsig1@(BranchRefSig n1 :: RTPointer
n1
                       (usig1 :: UnitSig
usig1, Just (BranchStaticContext bstc :: RefSigMap
bstc)))
                  _rsig2 :: RefSig
_rsig2@(ComponentRefSig n2 :: RTPointer
n2 rsmap :: RefSigMap
rsmap) =
  if RefSigMap -> RefSigMap -> Bool
matchesContext RefSigMap
rsmap RefSigMap
bstc then
          RefSig -> Result RefSig
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> Result RefSig) -> RefSig -> Result RefSig
forall a b. (a -> b) -> a -> b
$ RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig (RTPointer -> RTPointer -> RTPointer
compPointer RTPointer
n1 RTPointer
n2)
                   (UnitSig
usig1, BranchSig -> Maybe BranchSig
forall a. a -> Maybe a
Just (BranchSig -> Maybe BranchSig) -> BranchSig -> Maybe BranchSig
forall a b. (a -> b) -> a -> b
$ RefSigMap -> BranchSig
BranchStaticContext (RefSigMap -> BranchSig) -> RefSigMap -> BranchSig
forall a b. (a -> b) -> a -> b
$
                          [IRI] -> RefSigMap -> RefSigMap -> RefSigMap
modifyCtx (RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap) RefSigMap
rsmap RefSigMap
bstc)
      else String -> Result RefSig
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Signatures do not match:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [IRI] -> String
forall a. Show a => a -> String
show (RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
bstc) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ [IRI] -> String
forall a. Show a => a -> String
show (RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap))

refSigComposition (ComponentRefSig n1 :: RTPointer
n1 rsmap1 :: RefSigMap
rsmap1) (ComponentRefSig n2 :: RTPointer
n2 rsmap2 :: RefSigMap
rsmap2) = do
  [(IRI, RefSig)]
upd <- (IRI -> Result (IRI, RefSig)) -> [IRI] -> Result [(IRI, RefSig)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ x :: IRI
x -> do
                 RefSig
s <- RefSig -> RefSig -> Result RefSig
refSigComposition (RefSigMap
rsmap1 RefSigMap -> IRI -> RefSig
forall k a. Ord k => Map k a -> k -> a
Map.! IRI
x) (RefSigMap
rsmap2 RefSigMap -> IRI -> RefSig
forall k a. Ord k => Map k a -> k -> a
Map.! IRI
x)
                 (IRI, RefSig) -> Result (IRI, RefSig)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI
x, RefSig
s))
         ([IRI] -> Result [(IRI, RefSig)])
-> [IRI] -> Result [(IRI, RefSig)]
forall a b. (a -> b) -> a -> b
$ (IRI -> Bool) -> [IRI] -> [IRI]
forall a. (a -> Bool) -> [a] -> [a]
filter (IRI -> [IRI] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap1) ([IRI] -> [IRI]) -> [IRI] -> [IRI]
forall a b. (a -> b) -> a -> b
$ RefSigMap -> [IRI]
forall k a. Map k a -> [k]
Map.keys RefSigMap
rsmap2
  let unionMap :: RefSigMap
unionMap = RefSigMap -> RefSigMap -> RefSigMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(IRI, RefSig)] -> RefSigMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(IRI, RefSig)]
upd) (RefSigMap -> RefSigMap) -> RefSigMap -> RefSigMap
forall a b. (a -> b) -> a -> b
$
                 RefSigMap -> RefSigMap -> RefSigMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RefSigMap
rsmap1 RefSigMap
rsmap2
  RefSig -> Result RefSig
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> Result RefSig) -> RefSig -> Result RefSig
forall a b. (a -> b) -> a -> b
$ RTPointer -> RefSigMap -> RefSig
ComponentRefSig (RTPointer -> RTPointer -> RTPointer
compPointer RTPointer
n1 RTPointer
n2) RefSigMap
unionMap

refSigComposition _rsig1 :: RefSig
_rsig1 _rsig2 :: RefSig
_rsig2 =
  String -> Result RefSig
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "composition of refinement signatures"

-- | an entry of the global environment
data GlobalEntry =
    SpecEntry ExtGenSig
  | ViewOrStructEntry Bool ExtViewSig
  | ArchOrRefEntry Bool RefSig
  | AlignEntry AlignSig
  | UnitEntry UnitSig
  | NetworkEntry GDiagram
    deriving (Node -> GlobalEntry -> ShowS
[GlobalEntry] -> ShowS
GlobalEntry -> String
(Node -> GlobalEntry -> ShowS)
-> (GlobalEntry -> String)
-> ([GlobalEntry] -> ShowS)
-> Show GlobalEntry
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GlobalEntry] -> ShowS
$cshowList :: [GlobalEntry] -> ShowS
show :: GlobalEntry -> String
$cshow :: GlobalEntry -> String
showsPrec :: Node -> GlobalEntry -> ShowS
$cshowsPrec :: Node -> GlobalEntry -> ShowS
Show, Typeable)

getGlobEntryNodes :: GlobalEntry -> Set.Set Node
getGlobEntryNodes :: GlobalEntry -> Set Node
getGlobEntryNodes g :: GlobalEntry
g = case GlobalEntry
g of
  SpecEntry e :: ExtGenSig
e -> ExtGenSig -> Set Node
getExtGenSigNodes ExtGenSig
e
  ViewOrStructEntry _ e :: ExtViewSig
e -> ExtViewSig -> Set Node
getExtViewSigNodes ExtViewSig
e
  UnitEntry u :: UnitSig
u -> UnitSig -> Set Node
getUnitSigNodes UnitSig
u
  ArchOrRefEntry _ r :: RefSig
r -> RefSig -> Set Node
getRefSigNodes RefSig
r
  NetworkEntry gdiag :: GDiagram
gdiag -> [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
$ GDiagram -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes GDiagram
gdiag
  _ -> Set Node
forall a. Set a
Set.empty

data AlignSig = AlignMor NodeSig GMorphism NodeSig
              | AlignSpan NodeSig GMorphism NodeSig GMorphism NodeSig
              | WAlign
                          NodeSig GMorphism GMorphism -- s1, i1:s1 to b, sig1: s1 to t1
                          NodeSig GMorphism GMorphism -- s2, i2: s2 to b, sig2: s2 to t2
                          NodeSig                     -- t1
                          NodeSig                     -- t2
                          NodeSig                     -- b
  deriving (Node -> AlignSig -> ShowS
[AlignSig] -> ShowS
AlignSig -> String
(Node -> AlignSig -> ShowS)
-> (AlignSig -> String) -> ([AlignSig] -> ShowS) -> Show AlignSig
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AlignSig] -> ShowS
$cshowList :: [AlignSig] -> ShowS
show :: AlignSig -> String
$cshow :: AlignSig -> String
showsPrec :: Node -> AlignSig -> ShowS
$cshowsPrec :: Node -> AlignSig -> ShowS
Show, AlignSig -> AlignSig -> Bool
(AlignSig -> AlignSig -> Bool)
-> (AlignSig -> AlignSig -> Bool) -> Eq AlignSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AlignSig -> AlignSig -> Bool
$c/= :: AlignSig -> AlignSig -> Bool
== :: AlignSig -> AlignSig -> Bool
$c== :: AlignSig -> AlignSig -> Bool
Eq, Typeable)

type GlobalEnv = Map.Map IRI GlobalEntry

getGlobNodes :: GlobalEnv -> Set.Set Node
getGlobNodes :: GlobalEnv -> Set Node
getGlobNodes = [Set Node] -> Set Node
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Node] -> Set Node)
-> (GlobalEnv -> [Set Node]) -> GlobalEnv -> Set Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GlobalEntry -> Set Node) -> [GlobalEntry] -> [Set Node]
forall a b. (a -> b) -> [a] -> [b]
map GlobalEntry -> Set Node
getGlobEntryNodes ([GlobalEntry] -> [Set Node])
-> (GlobalEnv -> [GlobalEntry]) -> GlobalEnv -> [Set Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalEnv -> [GlobalEntry]
forall k a. Map k a -> [a]
Map.elems

-- ** change and history types

-- | the edit operations of the DGraph
data DGChange =
    InsertNode (LNode DGNodeLab)
  | DeleteNode (LNode DGNodeLab)
  | InsertEdge (LEdge DGLinkLab)
  | DeleteEdge (LEdge DGLinkLab)
  -- it contains the old label and new label with node
  | SetNodeLab DGNodeLab (LNode DGNodeLab)
  deriving (Node -> DGChange -> ShowS
[DGChange] -> ShowS
DGChange -> String
(Node -> DGChange -> ShowS)
-> (DGChange -> String) -> ([DGChange] -> ShowS) -> Show DGChange
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGChange] -> ShowS
$cshowList :: [DGChange] -> ShowS
show :: DGChange -> String
$cshow :: DGChange -> String
showsPrec :: Node -> DGChange -> ShowS
$cshowsPrec :: Node -> DGChange -> ShowS
Show, Typeable)

data HistElem =
    HistElem DGChange
  | HistGroup DGRule ProofHistory
  deriving Typeable

type ProofHistory = SizedList.SizedList HistElem

-- datatypes for the refinement tree

data RTNodeType = RTPlain UnitSig | RTRef Node deriving (RTNodeType -> RTNodeType -> Bool
(RTNodeType -> RTNodeType -> Bool)
-> (RTNodeType -> RTNodeType -> Bool) -> Eq RTNodeType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RTNodeType -> RTNodeType -> Bool
$c/= :: RTNodeType -> RTNodeType -> Bool
== :: RTNodeType -> RTNodeType -> Bool
$c== :: RTNodeType -> RTNodeType -> Bool
Eq, Typeable)

instance Show RTNodeType where
  show :: RTNodeType -> String
show (RTPlain u :: UnitSig
u) = "RTPlain\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitSig -> String
forall a. Show a => a -> String
show UnitSig
u
  show (RTRef n :: Node
n) = Node -> String
forall a. Show a => a -> String
show Node
n

data RTNodeLab = RTNodeLab
  { RTNodeLab -> RTNodeType
rtn_type :: RTNodeType
  , RTNodeLab -> String
rtn_name :: String
  , RTNodeLab -> String
rtn_diag :: String
  } deriving (RTNodeLab -> RTNodeLab -> Bool
(RTNodeLab -> RTNodeLab -> Bool)
-> (RTNodeLab -> RTNodeLab -> Bool) -> Eq RTNodeLab
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RTNodeLab -> RTNodeLab -> Bool
$c/= :: RTNodeLab -> RTNodeLab -> Bool
== :: RTNodeLab -> RTNodeLab -> Bool
$c== :: RTNodeLab -> RTNodeLab -> Bool
Eq, Typeable)

instance Show RTNodeLab where
 show :: RTNodeLab -> String
show r :: RTNodeLab
r =
  let
   name :: String
name = RTNodeLab -> String
rtn_name RTNodeLab
r
   t :: RTNodeType
t = RTNodeLab -> RTNodeType
rtn_type RTNodeLab
r
   d :: String
d = RTNodeLab -> String
rtn_diag RTNodeLab
r
   t1 :: String
t1 = case RTNodeType
t of
          RTPlain u :: UnitSig
u -> "plain: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitSig -> String
forall a. Show a => a -> String
show UnitSig
u
          RTRef n :: Node
n -> Node -> String
forall a. Show a => a -> String
show Node
n
  in "Name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n diag :" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t1

data RTLinkType =
    RTRefine
  | RTComp
  deriving (Node -> RTLinkType -> ShowS
[RTLinkType] -> ShowS
RTLinkType -> String
(Node -> RTLinkType -> ShowS)
-> (RTLinkType -> String)
-> ([RTLinkType] -> ShowS)
-> Show RTLinkType
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RTLinkType] -> ShowS
$cshowList :: [RTLinkType] -> ShowS
show :: RTLinkType -> String
$cshow :: RTLinkType -> String
showsPrec :: Node -> RTLinkType -> ShowS
$cshowsPrec :: Node -> RTLinkType -> ShowS
Show, RTLinkType -> RTLinkType -> Bool
(RTLinkType -> RTLinkType -> Bool)
-> (RTLinkType -> RTLinkType -> Bool) -> Eq RTLinkType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RTLinkType -> RTLinkType -> Bool
$c/= :: RTLinkType -> RTLinkType -> Bool
== :: RTLinkType -> RTLinkType -> Bool
$c== :: RTLinkType -> RTLinkType -> Bool
Eq, Typeable)

data RTLinkLab = RTLink
  { RTLinkLab -> RTLinkType
rtl_type :: RTLinkType
  } deriving (Node -> RTLinkLab -> ShowS
[RTLinkLab] -> ShowS
RTLinkLab -> String
(Node -> RTLinkLab -> ShowS)
-> (RTLinkLab -> String)
-> ([RTLinkLab] -> ShowS)
-> Show RTLinkLab
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RTLinkLab] -> ShowS
$cshowList :: [RTLinkLab] -> ShowS
show :: RTLinkLab -> String
$cshow :: RTLinkLab -> String
showsPrec :: Node -> RTLinkLab -> ShowS
$cshowsPrec :: Node -> RTLinkLab -> ShowS
Show, RTLinkLab -> RTLinkLab -> Bool
(RTLinkLab -> RTLinkLab -> Bool)
-> (RTLinkLab -> RTLinkLab -> Bool) -> Eq RTLinkLab
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RTLinkLab -> RTLinkLab -> Bool
$c/= :: RTLinkLab -> RTLinkLab -> Bool
== :: RTLinkLab -> RTLinkLab -> Bool
$c== :: RTLinkLab -> RTLinkLab -> Bool
Eq, Typeable)

-- utility functions for handling refinement tree

addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT dg :: DGraph
dg usig :: UnitSig
usig s :: String
s =
 let
  g :: Gr RTNodeLab RTLinkLab
g = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
  n :: Node
n = Gr RTNodeLab RTLinkLab -> Node
forall a b. Gr a b -> Node
Tree.getNewNode Gr RTNodeLab RTLinkLab
g
  l :: RTNodeLab
l = RTNodeLab :: RTNodeType -> String -> String -> RTNodeLab
RTNodeLab {
        rtn_type :: RTNodeType
rtn_type = UnitSig -> RTNodeType
RTPlain UnitSig
usig
        , rtn_name :: String
rtn_name = String
s
        , rtn_diag :: String
rtn_diag = String
s
       }
 in (Node
n, DGraph
dg {refTree :: Gr RTNodeLab RTLinkLab
refTree = LNode RTNodeLab -> Gr RTNodeLab RTLinkLab -> Gr RTNodeLab RTLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Node
n, RTNodeLab
l) Gr RTNodeLab RTLinkLab
g})

addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)
addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)
addSpecNodeRT dg :: DGraph
dg usig :: UnitSig
usig s :: String
s =
 let
  (n :: Node
n, dg' :: DGraph
dg') = DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT DGraph
dg UnitSig
usig String
s
  f :: Map String [Node]
f = String -> [Node] -> Map String [Node] -> Map String [Node]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s [Node
n] (Map String [Node] -> Map String [Node])
-> Map String [Node] -> Map String [Node]
forall a b. (a -> b) -> a -> b
$ DGraph -> Map String [Node]
specRoots DGraph
dg'
 in (Node
n, DGraph
dg' {specRoots :: Map String [Node]
specRoots = Map String [Node]
f})

updateNodeNameRT :: DGraph -> Node -> Bool -> String -> DGraph
-- the Bool flag tells if the diag name should change too
updateNodeNameRT :: DGraph -> Node -> Bool -> String -> DGraph
updateNodeNameRT dg :: DGraph
dg n :: Node
n flag :: Bool
flag s :: String
s =
 let
  g :: Gr RTNodeLab RTLinkLab
g = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
  l :: Maybe RTNodeLab
l = Gr RTNodeLab RTLinkLab -> Node -> Maybe RTNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
Graph.lab Gr RTNodeLab RTLinkLab
g Node
n
 in case Maybe RTNodeLab
l of
     Nothing -> DGraph
dg
     Just oldL :: RTNodeLab
oldL ->
      let
       newL :: RTNodeLab
newL = if Bool
flag then RTNodeLab
oldL {rtn_name :: String
rtn_name = String
s, rtn_diag :: String
rtn_diag = String
s}
              else RTNodeLab
oldL {rtn_name :: String
rtn_name = String
s}
       (g' :: Gr RTNodeLab RTLinkLab
g', _) = LNode RTNodeLab
-> Gr RTNodeLab RTLinkLab -> (Gr RTNodeLab RTLinkLab, RTNodeLab)
forall a b. LNode a -> Gr a b -> (Gr a b, a)
Tree.labelNode (Node
n, RTNodeLab
newL) Gr RTNodeLab RTLinkLab
g
      in DGraph
dg {refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
g'}

updateSigRT :: DGraph -> Node -> UnitSig -> DGraph
updateSigRT :: DGraph -> Node -> UnitSig -> DGraph
updateSigRT dg :: DGraph
dg n :: Node
n usig :: UnitSig
usig =
 let
  g :: Gr RTNodeLab RTLinkLab
g = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
  l :: Maybe RTNodeLab
l = Gr RTNodeLab RTLinkLab -> Node -> Maybe RTNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
Graph.lab Gr RTNodeLab RTLinkLab
g Node
n
 in case Maybe RTNodeLab
l of
     Nothing -> DGraph
dg
     Just oldL :: RTNodeLab
oldL -> let
       newL :: RTNodeLab
newL = RTNodeLab
oldL {rtn_type :: RTNodeType
rtn_type = UnitSig -> RTNodeType
RTPlain UnitSig
usig}
       (g' :: Gr RTNodeLab RTLinkLab
g', _) = LNode RTNodeLab
-> Gr RTNodeLab RTLinkLab -> (Gr RTNodeLab RTLinkLab, RTNodeLab)
forall a b. LNode a -> Gr a b -> (Gr a b, a)
Tree.labelNode (Node
n, RTNodeLab
newL) Gr RTNodeLab RTLinkLab
g
                  in DGraph
dg {refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
g'}

updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph
updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph
updateNodeNameSpecRT dg :: DGraph
dg n :: Node
n s :: String
s =
 let dg' :: DGraph
dg' = DGraph -> Node -> Bool -> String -> DGraph
updateNodeNameRT DGraph
dg Node
n Bool
False String
s
 in DGraph
dg' {specRoots :: Map String [Node]
specRoots = String -> [Node] -> Map String [Node] -> Map String [Node]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s [Node
n] (Map String [Node] -> Map String [Node])
-> Map String [Node] -> Map String [Node]
forall a b. (a -> b) -> a -> b
$ DGraph -> Map String [Node]
specRoots DGraph
dg}

addSubTree :: DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree :: DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree dg :: DGraph
dg Nothing (NPComp h :: Map IRI RTPointer
h) =
  ((DGraph, RTPointer) -> (IRI, RTPointer) -> (DGraph, RTPointer))
-> (DGraph, RTPointer) -> [(IRI, RTPointer)] -> (DGraph, RTPointer)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
   (\ ~(d :: DGraph
d, NPComp cp :: Map IRI RTPointer
cp) (k :: IRI
k, p :: RTPointer
p) -> let
         (d' :: DGraph
d', p' :: RTPointer
p') = DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree DGraph
d Maybe RTLeaves
forall a. Maybe a
Nothing RTPointer
p
       in (DGraph
d', Map IRI RTPointer -> RTPointer
NPComp (IRI -> RTPointer -> Map IRI RTPointer -> Map IRI RTPointer
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
k RTPointer
p' Map IRI RTPointer
cp)))
   (DGraph
dg, Map IRI RTPointer -> RTPointer
NPComp Map IRI RTPointer
forall k a. Map k a
Map.empty) ([(IRI, RTPointer)] -> (DGraph, RTPointer))
-> [(IRI, RTPointer)] -> (DGraph, RTPointer)
forall a b. (a -> b) -> a -> b
$ Map IRI RTPointer -> [(IRI, RTPointer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map IRI RTPointer
h
addSubTree dg :: DGraph
dg Nothing p :: RTPointer
p = let
   s :: Node
s = RTPointer -> Node
refSource RTPointer
p
   (dg' :: DGraph
dg', f :: Map Node Node
f) = DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)
copySubTree DGraph
dg Node
s Maybe Node
forall a. Maybe a
Nothing
   p' :: RTPointer
p' = Map Node Node -> RTPointer -> RTPointer
mapRTNodes Map Node Node
f RTPointer
p
  in (DGraph
dg', RTPointer
p')
addSubTree dg :: DGraph
dg (Just (RTLeaf x :: Node
x)) p :: RTPointer
p = let
   s :: Node
s = RTPointer -> Node
refSource RTPointer
p
   (dg' :: DGraph
dg', f :: Map Node Node
f) = DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)
copySubTree DGraph
dg Node
s (Maybe Node -> (DGraph, Map Node Node))
-> Maybe Node -> (DGraph, Map Node Node)
forall a b. (a -> b) -> a -> b
$ Node -> Maybe Node
forall a. a -> Maybe a
Just Node
x
   p' :: RTPointer
p' = Map Node Node -> RTPointer -> RTPointer
mapRTNodes Map Node Node
f RTPointer
p
  in (DGraph
dg', RTPointer
p')
addSubTree dg :: DGraph
dg (Just (RTLeaves g :: Map IRI RTLeaves
g)) (NPComp h :: Map IRI RTPointer
h) =
 ((DGraph, RTPointer) -> (IRI, RTPointer) -> (DGraph, RTPointer))
-> (DGraph, RTPointer) -> [(IRI, RTPointer)] -> (DGraph, RTPointer)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
   (\ ~(d :: DGraph
d, NPComp cp :: Map IRI RTPointer
cp) (k :: IRI
k, p :: RTPointer
p) -> let
         l :: RTLeaves
l = RTLeaves -> IRI -> Map IRI RTLeaves -> RTLeaves
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> RTLeaves
forall a. HasCallStack => String -> a
error (String -> RTLeaves) -> String -> RTLeaves
forall a b. (a -> b) -> a -> b
$ "addSubTree:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ IRI -> String
forall a. Show a => a -> String
show IRI
k) IRI
k Map IRI RTLeaves
g
         (d' :: DGraph
d', p' :: RTPointer
p') = DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree DGraph
d (RTLeaves -> Maybe RTLeaves
forall a. a -> Maybe a
Just RTLeaves
l) RTPointer
p
       in (DGraph
d', Map IRI RTPointer -> RTPointer
NPComp (IRI -> RTPointer -> Map IRI RTPointer -> Map IRI RTPointer
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
k RTPointer
p' Map IRI RTPointer
cp)))
   (DGraph
dg, Map IRI RTPointer -> RTPointer
NPComp Map IRI RTPointer
forall k a. Map k a
Map.empty) ([(IRI, RTPointer)] -> (DGraph, RTPointer))
-> [(IRI, RTPointer)] -> (DGraph, RTPointer)
forall a b. (a -> b) -> a -> b
$ Map IRI RTPointer -> [(IRI, RTPointer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map IRI RTPointer
h
addSubTree _ _ _ = String -> (DGraph, RTPointer)
forall a. HasCallStack => String -> a
error "addSubTree"

copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map.Map Node Node)
copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)
copySubTree dg :: DGraph
dg n :: Node
n mN :: Maybe Node
mN =
 case Maybe Node
mN of
   Nothing -> let
     rTree :: Gr RTNodeLab RTLinkLab
rTree = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
     n' :: Node
n' = Gr RTNodeLab RTLinkLab -> Node
forall a b. Gr a b -> Node
Tree.getNewNode Gr RTNodeLab RTLinkLab
rTree
     nLab :: RTNodeLab
nLab = RTNodeLab -> Maybe RTNodeLab -> RTNodeLab
forall a. a -> Maybe a -> a
fromMaybe (String -> RTNodeLab
forall a. HasCallStack => String -> a
error "copyNode") (Maybe RTNodeLab -> RTNodeLab) -> Maybe RTNodeLab -> RTNodeLab
forall a b. (a -> b) -> a -> b
$ Gr RTNodeLab RTLinkLab -> Node -> Maybe RTNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab Gr RTNodeLab RTLinkLab
rTree Node
n
     rTree' :: Gr RTNodeLab RTLinkLab
rTree' = LNode RTNodeLab -> Gr RTNodeLab RTLinkLab -> Gr RTNodeLab RTLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Node
n', RTNodeLab
nLab) Gr RTNodeLab RTLinkLab
rTree
    in DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node)
copySubTreeN DGraph
dg {refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
rTree'} [Node
n] (Map Node Node -> (DGraph, Map Node Node))
-> Map Node Node -> (DGraph, Map Node Node)
forall a b. (a -> b) -> a -> b
$ [(Node, Node)] -> Map Node Node
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node
n, Node
n')]
   Just y :: Node
y -> DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node)
copySubTreeN DGraph
dg [Node
n] (Map Node Node -> (DGraph, Map Node Node))
-> Map Node Node -> (DGraph, Map Node Node)
forall a b. (a -> b) -> a -> b
$ [(Node, Node)] -> Map Node Node
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Node
n, Node
y)]

copySubTreeN :: DGraph -> [Node] -> Map.Map Node Node
             -> (DGraph, Map.Map Node Node)
copySubTreeN :: DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node)
copySubTreeN dg :: DGraph
dg nList :: [Node]
nList pairs :: Map Node Node
pairs =
 case [Node]
nList of
  [] -> (DGraph
dg, Map Node Node
pairs)
  n :: Node
n : nList' :: [Node]
nList' -> let
    rTree :: Gr RTNodeLab RTLinkLab
rTree = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
    pairsN :: Node
pairsN = Node -> Node -> Map Node Node -> Node
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Node
forall a. HasCallStack => String -> a
error "copy") Node
n Map Node Node
pairs
    descs :: [(Node, RTLinkLab)]
descs = Gr RTNodeLab RTLinkLab -> Node -> [(Node, RTLinkLab)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [(Node, b)]
lsuc Gr RTNodeLab RTLinkLab
rTree Node
n
    (dg' :: DGraph
dg', pairs' :: Map Node Node
pairs') = ((DGraph, Map Node Node)
 -> (Node, RTLinkLab) -> (DGraph, Map Node Node))
-> (DGraph, Map Node Node)
-> [(Node, RTLinkLab)]
-> (DGraph, Map Node Node)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Node
-> (DGraph, Map Node Node)
-> (Node, RTLinkLab)
-> (DGraph, Map Node Node)
copyNode Node
pairsN) (DGraph
dg, Map Node Node
pairs) [(Node, RTLinkLab)]
descs
   in DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node)
copySubTreeN DGraph
dg' ([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node]
nList' [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ ((Node, RTLinkLab) -> Node) -> [(Node, RTLinkLab)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (Node, RTLinkLab) -> Node
forall a b. (a, b) -> a
fst [(Node, RTLinkLab)]
descs) Map Node Node
pairs'

copyNode :: Node -> (DGraph, Map.Map Node Node) -> LNode RTLinkLab
           -> (DGraph, Map.Map Node Node)
copyNode :: Node
-> (DGraph, Map Node Node)
-> (Node, RTLinkLab)
-> (DGraph, Map Node Node)
copyNode s :: Node
s (dg :: DGraph
dg, nMap :: Map Node Node
nMap) (n :: Node
n, eLab :: RTLinkLab
eLab) = let
   rTree :: Gr RTNodeLab RTLinkLab
rTree = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
   nLab :: RTNodeLab
nLab = RTNodeLab -> Maybe RTNodeLab -> RTNodeLab
forall a. a -> Maybe a -> a
fromMaybe (String -> RTNodeLab
forall a. HasCallStack => String -> a
error "copyNode") (Maybe RTNodeLab -> RTNodeLab) -> Maybe RTNodeLab -> RTNodeLab
forall a b. (a -> b) -> a -> b
$ Gr RTNodeLab RTLinkLab -> Node -> Maybe RTNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab Gr RTNodeLab RTLinkLab
rTree Node
n
   n' :: Node
n' = Gr RTNodeLab RTLinkLab -> Node
forall a b. Gr a b -> Node
Tree.getNewNode Gr RTNodeLab RTLinkLab
rTree
   rTree' :: Gr RTNodeLab RTLinkLab
rTree' = LNode RTNodeLab -> Gr RTNodeLab RTLinkLab -> Gr RTNodeLab RTLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Node
n', RTNodeLab
nLab) Gr RTNodeLab RTLinkLab
rTree
   orderRT :: p -> p -> Ordering
orderRT _ _ = Ordering
GT
   (rTree'' :: Gr RTNodeLab RTLinkLab
rTree'', _) = Bool
-> (RTLinkLab -> RTLinkLab -> Ordering)
-> LEdge RTLinkLab
-> Gr RTNodeLab RTLinkLab
-> (Gr RTNodeLab RTLinkLab, Bool)
forall b a.
Bool -> (b -> b -> Ordering) -> LEdge b -> Gr a b -> (Gr a b, Bool)
Tree.insLEdge Bool
True RTLinkLab -> RTLinkLab -> Ordering
forall p p. p -> p -> Ordering
orderRT (Node
s, Node
n', RTLinkLab
eLab) Gr RTNodeLab RTLinkLab
rTree'
 in (DGraph
dg {refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
rTree''}, Node -> Node -> Map Node Node -> Map Node Node
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Node
n Node
n' Map Node Node
nMap)

addRefEdgeRT :: DGraph -> Node -> Node -> DGraph
addRefEdgeRT :: DGraph -> Node -> Node -> DGraph
addRefEdgeRT dg :: DGraph
dg n1 :: Node
n1 n2 :: Node
n2 =
 let
  g :: Gr RTNodeLab RTLinkLab
g = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg
  orderRT :: p -> p -> Ordering
orderRT _ _ = Ordering
GT
  (g' :: Gr RTNodeLab RTLinkLab
g', b :: Bool
b) = Bool
-> (RTLinkLab -> RTLinkLab -> Ordering)
-> LEdge RTLinkLab
-> Gr RTNodeLab RTLinkLab
-> (Gr RTNodeLab RTLinkLab, Bool)
forall b a.
Bool -> (b -> b -> Ordering) -> LEdge b -> Gr a b -> (Gr a b, Bool)
Tree.insLEdge Bool
True RTLinkLab -> RTLinkLab -> Ordering
forall p p. p -> p -> Ordering
orderRT
                                 (Node
n1, Node
n2, RTLink :: RTLinkType -> RTLinkLab
RTLink {rtl_type :: RTLinkType
rtl_type = RTLinkType
RTRefine}) Gr RTNodeLab RTLinkLab
g
 in if Bool
b then DGraph
dg {refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
g'}
    else String -> DGraph
forall a. HasCallStack => String -> a
error "addRefEdgeRT"

addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph
addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph
addEdgesToNodeRT dg' :: DGraph
dg' rnodes :: [Node]
rnodes n' :: Node
n' =
 let
  g :: Gr RTNodeLab RTLinkLab
g = DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg'
  orderRT :: p -> p -> Ordering
orderRT _ _ = Ordering
GT
  (g' :: Gr RTNodeLab RTLinkLab
g', b :: Bool
b) = ((Gr RTNodeLab RTLinkLab, Bool)
 -> Node -> (Gr RTNodeLab RTLinkLab, Bool))
-> (Gr RTNodeLab RTLinkLab, Bool)
-> [Node]
-> (Gr RTNodeLab RTLinkLab, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (g0 :: Gr RTNodeLab RTLinkLab
g0, b0 :: Bool
b0) n0 :: Node
n0 -> let
                      (g1 :: Gr RTNodeLab RTLinkLab
g1, b1 :: Bool
b1) = Bool
-> (RTLinkLab -> RTLinkLab -> Ordering)
-> LEdge RTLinkLab
-> Gr RTNodeLab RTLinkLab
-> (Gr RTNodeLab RTLinkLab, Bool)
forall b a.
Bool -> (b -> b -> Ordering) -> LEdge b -> Gr a b -> (Gr a b, Bool)
Tree.insLEdge Bool
True RTLinkLab -> RTLinkLab -> Ordering
forall p p. p -> p -> Ordering
orderRT
                                 (Node
n', Node
n0, RTLink :: RTLinkType -> RTLinkLab
RTLink {rtl_type :: RTLinkType
rtl_type = RTLinkType
RTComp}) Gr RTNodeLab RTLinkLab
g0

                                    in (Gr RTNodeLab RTLinkLab
g1, Bool
b1 Bool -> Bool -> Bool
&& Bool
b0))
            (Gr RTNodeLab RTLinkLab
g, Bool
True) [Node]
rnodes
 in if Bool -> Bool
not Bool
b then String -> DGraph
forall a. HasCallStack => String -> a
error "addEdgesToNodeRT"
    else DGraph
dg' {refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
g'}


{- I copied these types from ArchDiagram
to store the diagrams of the arch specs in the dgraph -}

data DiagNodeLab = DiagNode { DiagNodeLab -> NodeSig
dn_sig :: NodeSig, DiagNodeLab -> String
dn_desc :: String }
 deriving (Node -> DiagNodeLab -> ShowS
[DiagNodeLab] -> ShowS
DiagNodeLab -> String
(Node -> DiagNodeLab -> ShowS)
-> (DiagNodeLab -> String)
-> ([DiagNodeLab] -> ShowS)
-> Show DiagNodeLab
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagNodeLab] -> ShowS
$cshowList :: [DiagNodeLab] -> ShowS
show :: DiagNodeLab -> String
$cshow :: DiagNodeLab -> String
showsPrec :: Node -> DiagNodeLab -> ShowS
$cshowsPrec :: Node -> DiagNodeLab -> ShowS
Show, Typeable)

data DiagLinkLab = DiagLink { DiagLinkLab -> GMorphism
dl_morphism :: GMorphism, DiagLinkLab -> Node
dl_number :: Int }
  deriving Typeable

instance Show DiagLinkLab where
 show :: DiagLinkLab -> String
show _ = ""

data Diag = Diagram
  { Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph :: Tree.Gr DiagNodeLab DiagLinkLab
  , Diag -> Node
numberOfEdges :: Int
  } deriving (Node -> Diag -> ShowS
[Diag] -> ShowS
Diag -> String
(Node -> Diag -> ShowS)
-> (Diag -> String) -> ([Diag] -> ShowS) -> Show Diag
forall a.
(Node -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Diag] -> ShowS
$cshowList :: [Diag] -> ShowS
show :: Diag -> String
$cshow :: Diag -> String
showsPrec :: Node -> Diag -> ShowS
$cshowsPrec :: Node -> Diag -> ShowS
Show, Typeable)

{- | the actual development graph with auxiliary information. A
  'G_sign' should be stored in 'sigMap' under its 'gSignSelfIdx'. The
  same applies to 'G_morphism' with 'morMap' and 'gMorphismSelfIdx'
  resp. 'G_theory' with 'thMap' and 'gTheorySelfIdx'. -}
data DGraph = DGraph
  { DGraph -> GlobalAnnos
globalAnnos :: GlobalAnnos -- ^ global annos of library
  , DGraph -> Maybe LIB_DEFN
optLibDefn :: Maybe LIB_DEFN
  , DGraph -> GlobalEnv
globalEnv :: GlobalEnv -- ^ name entities (specs, views) of a library
  , DGraph -> Gr DGNodeLab DGLinkLab
dgBody :: Tree.Gr DGNodeLab DGLinkLab  -- ^ actual 'DGraph` tree
  , DGraph -> Maybe NodeSig
currentBaseTheory :: Maybe NodeSig
  , DGraph -> Gr RTNodeLab RTLinkLab
refTree :: Tree.Gr RTNodeLab RTLinkLab -- ^ the refinement tree
  , DGraph -> Map String [Node]
specRoots :: Map.Map String [Node] -- ^ root nodes for named specs, several for comp ref
  , DGraph -> MapSet String Node
nameMap :: MapSet.MapSet String Node -- ^ all nodes by name
  , DGraph -> Map String Diag
archSpecDiags :: Map.Map String Diag
      -- ^ dependency diagrams between units
  , DGraph -> EdgeId
getNewEdgeId :: EdgeId  -- ^ edge counter
  , DGraph -> Map (LibName, Node) Node
allRefNodes :: Map.Map (LibName, Node) Node -- ^ all DGRef's
  , DGraph -> Map SigId G_sign
sigMap :: Map.Map SigId G_sign -- ^ signature map
  , DGraph -> Map ThId G_theory
thMap :: Map.Map ThId G_theory -- ^ theory map
  , DGraph -> Map MorId G_morphism
morMap :: Map.Map MorId G_morphism -- ^ morphism map
  , DGraph -> ProofHistory
proofHistory :: ProofHistory -- ^ applied proof steps
  , DGraph -> ProofHistory
redoHistory :: ProofHistory -- ^ undone proofs steps
  } deriving Typeable

instance Show DGraph where
  show :: DGraph -> String
show _ = "<a development graph>"

emptyDG :: DGraph
emptyDG :: DGraph
emptyDG = DGraph :: GlobalAnnos
-> Maybe LIB_DEFN
-> GlobalEnv
-> Gr DGNodeLab DGLinkLab
-> Maybe NodeSig
-> Gr RTNodeLab RTLinkLab
-> Map String [Node]
-> MapSet String Node
-> Map String Diag
-> EdgeId
-> Map (LibName, Node) Node
-> Map SigId G_sign
-> Map ThId G_theory
-> Map MorId G_morphism
-> ProofHistory
-> ProofHistory
-> DGraph
DGraph
  { globalAnnos :: GlobalAnnos
globalAnnos = GlobalAnnos
emptyGlobalAnnos
  , optLibDefn :: Maybe LIB_DEFN
optLibDefn = Maybe LIB_DEFN
forall a. Maybe a
Nothing
  , globalEnv :: GlobalEnv
globalEnv = GlobalEnv
forall k a. Map k a
Map.empty
  , dgBody :: Gr DGNodeLab DGLinkLab
dgBody = Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty
  , currentBaseTheory :: Maybe NodeSig
currentBaseTheory = Maybe NodeSig
forall a. Maybe a
Nothing
  , refTree :: Gr RTNodeLab RTLinkLab
refTree = Gr RTNodeLab RTLinkLab
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty
  , specRoots :: Map String [Node]
specRoots = Map String [Node]
forall k a. Map k a
Map.empty
  , nameMap :: MapSet String Node
nameMap = MapSet String Node
forall a b. MapSet a b
MapSet.empty
  , archSpecDiags :: Map String Diag
archSpecDiags = Map String Diag
forall k a. Map k a
Map.empty
  , getNewEdgeId :: EdgeId
getNewEdgeId = EdgeId
startEdgeId
  , allRefNodes :: Map (LibName, Node) Node
allRefNodes = Map (LibName, Node) Node
forall k a. Map k a
Map.empty
  , sigMap :: Map SigId G_sign
sigMap = Map SigId G_sign
forall k a. Map k a
Map.empty
  , thMap :: Map ThId G_theory
thMap = Map ThId G_theory
forall k a. Map k a
Map.empty
  , morMap :: Map MorId G_morphism
morMap = Map MorId G_morphism
forall k a. Map k a
Map.empty
  , proofHistory :: ProofHistory
proofHistory = ProofHistory
forall a. SizedList a
SizedList.empty
  , redoHistory :: ProofHistory
redoHistory = ProofHistory
forall a. SizedList a
SizedList.empty }

type LibEnv = Map.Map LibName DGraph

-- | an empty environment
emptyLibEnv :: LibEnv
emptyLibEnv :: LibEnv
emptyLibEnv = LibEnv
forall k a. Map k a
Map.empty

-- * utility functions

-- ** for node signatures

emptyG_sign :: AnyLogic -> G_sign
emptyG_sign :: AnyLogic -> G_sign
emptyG_sign (Logic lid :: lid
lid) = lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid (lid -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol
ext_empty_signature lid
lid) SigId
startSigId

getMaybeSig :: MaybeNode -> G_sign
getMaybeSig :: MaybeNode -> G_sign
getMaybeSig (JustNode ns :: NodeSig
ns) = NodeSig -> G_sign
getSig NodeSig
ns
getMaybeSig (EmptyNode l :: AnyLogic
l) = AnyLogic -> G_sign
emptyG_sign AnyLogic
l

getLogic :: MaybeNode -> AnyLogic
getLogic :: MaybeNode -> AnyLogic
getLogic = G_sign -> AnyLogic
logicOfGsign (G_sign -> AnyLogic)
-> (MaybeNode -> G_sign) -> MaybeNode -> AnyLogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeNode -> G_sign
getMaybeSig

getNodeLogic :: NodeSig -> AnyLogic
getNodeLogic :: NodeSig -> AnyLogic
getNodeLogic = G_sign -> AnyLogic
logicOfGsign (G_sign -> AnyLogic) -> (NodeSig -> G_sign) -> NodeSig -> AnyLogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeSig -> G_sign
getSig

-- ** accessing node label

-- | get the origin of a non-reference node (partial)
dgn_origin :: DGNodeLab -> DGOrigin
dgn_origin :: DGNodeLab -> DGOrigin
dgn_origin = DGNodeInfo -> DGOrigin
node_origin (DGNodeInfo -> DGOrigin)
-> (DGNodeLab -> DGNodeInfo) -> DGNodeLab -> DGOrigin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> DGNodeInfo
nodeInfo

-- | get the referenced library (partial)
dgn_libname :: DGNodeLab -> LibName
dgn_libname :: DGNodeLab -> LibName
dgn_libname = DGNodeInfo -> LibName
ref_libname (DGNodeInfo -> LibName)
-> (DGNodeLab -> DGNodeInfo) -> DGNodeLab -> LibName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> DGNodeInfo
nodeInfo

-- | get the referenced node (partial)
dgn_node :: DGNodeLab -> Node
dgn_node :: DGNodeLab -> Node
dgn_node = DGNodeInfo -> Node
ref_node (DGNodeInfo -> Node)
-> (DGNodeLab -> DGNodeInfo) -> DGNodeLab -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> DGNodeInfo
nodeInfo

-- | get the signature of a node's theory (total)
dgn_sign :: DGNodeLab -> G_sign
dgn_sign :: DGNodeLab -> G_sign
dgn_sign = G_theory -> G_sign
signOf (G_theory -> G_sign)
-> (DGNodeLab -> G_theory) -> DGNodeLab -> G_sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> G_theory
dgn_theory

-- | gets the name of a development graph node as a string (total)
getDGNodeName :: DGNodeLab -> String
getDGNodeName :: DGNodeLab -> String
getDGNodeName = NodeName -> String
showName (NodeName -> String)
-> (DGNodeLab -> NodeName) -> DGNodeLab -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> NodeName
dgn_name

-- | get the global theory of a node or the local one if missing
globOrLocTh :: DGNodeLab -> G_theory
globOrLocTh :: DGNodeLab -> G_theory
globOrLocTh lbl :: DGNodeLab
lbl = G_theory -> Maybe G_theory -> G_theory
forall a. a -> Maybe a -> a
fromMaybe (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl) (Maybe G_theory -> G_theory) -> Maybe G_theory -> G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl

-- ** creating node content and label

-- | create node info
newConsNodeInfo :: DGOrigin -> Conservativity -> DGNodeInfo
newConsNodeInfo :: DGOrigin -> Conservativity -> DGNodeInfo
newConsNodeInfo orig :: DGOrigin
orig cs :: Conservativity
cs = DGNode :: DGOrigin -> ConsStatus -> DGNodeInfo
DGNode
  { node_origin :: DGOrigin
node_origin = DGOrigin
orig
  , node_cons_status :: ConsStatus
node_cons_status = Conservativity -> ConsStatus
mkConsStatus Conservativity
cs }

-- | create default content
newNodeInfo :: DGOrigin -> DGNodeInfo
newNodeInfo :: DGOrigin -> DGNodeInfo
newNodeInfo orig :: DGOrigin
orig = DGOrigin -> Conservativity -> DGNodeInfo
newConsNodeInfo DGOrigin
orig Conservativity
None

-- | create a reference node part
newRefInfo :: LibName -> Node -> DGNodeInfo
newRefInfo :: LibName -> Node -> DGNodeInfo
newRefInfo ln :: LibName
ln n :: Node
n = DGRef :: LibName -> Node -> DGNodeInfo
DGRef
  { ref_libname :: LibName
ref_libname = LibName
ln
  , ref_node :: Node
ref_node = Node
n }

-- | create a new node label
newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab name :: NodeName
name info :: DGNodeInfo
info gTh :: G_theory
gTh = DGNodeLab :: NodeName
-> G_theory
-> Maybe G_theory
-> Bool
-> Bool
-> Maybe Node
-> Maybe GMorphism
-> Maybe Node
-> Maybe GMorphism
-> DGNodeInfo
-> NodeMod
-> Maybe XNode
-> Maybe (MVar ())
-> DGNodeLab
DGNodeLab
  { dgn_name :: NodeName
dgn_name = NodeName
name
  , dgn_theory :: G_theory
dgn_theory = G_theory
gTh
  , globalTheory :: Maybe G_theory
globalTheory = Maybe G_theory
forall a. Maybe a
Nothing
  , labelHasHiding :: Bool
labelHasHiding = Bool
False
  , labelHasFree :: Bool
labelHasFree = Bool
False
  , dgn_nf :: Maybe Node
dgn_nf = Maybe Node
forall a. Maybe a
Nothing
  , dgn_sigma :: Maybe GMorphism
dgn_sigma = Maybe GMorphism
forall a. Maybe a
Nothing
  , dgn_freenf :: Maybe Node
dgn_freenf = Maybe Node
forall a. Maybe a
Nothing
  , dgn_phi :: Maybe GMorphism
dgn_phi = Maybe GMorphism
forall a. Maybe a
Nothing
  , nodeInfo :: DGNodeInfo
nodeInfo = DGNodeInfo
info
  , nodeMod :: NodeMod
nodeMod = NodeMod
unMod
  , xnode :: Maybe XNode
xnode = Maybe XNode
forall a. Maybe a
Nothing
  , dgn_lock :: Maybe (MVar ())
dgn_lock = Maybe (MVar ())
forall a. Maybe a
Nothing }

-- | create a new node label using 'newNodeInfo' and 'newInfoNodeLab'
newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab name :: NodeName
name = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
name (DGNodeInfo -> G_theory -> DGNodeLab)
-> (DGOrigin -> DGNodeInfo) -> DGOrigin -> G_theory -> DGNodeLab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGOrigin -> DGNodeInfo
newNodeInfo

-- ** handle the lock of a node

-- | wrapper to access the maybe lock
treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a
treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a
treatNodeLock f :: MVar () -> a
f = a -> (MVar () -> a) -> Maybe (MVar ()) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> a
forall a. HasCallStack => String -> a
error "MVar not initialised") MVar () -> a
f (Maybe (MVar ()) -> a)
-> (DGNodeLab -> Maybe (MVar ())) -> DGNodeLab -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> Maybe (MVar ())
dgn_lock

-- | Tries to acquire the local lock. Return False if already acquired.
tryLockLocal :: DGNodeLab -> IO Bool
tryLockLocal :: DGNodeLab -> IO Bool
tryLockLocal = (MVar () -> IO Bool) -> DGNodeLab -> IO Bool
forall a. (MVar () -> a) -> DGNodeLab -> a
treatNodeLock ((MVar () -> IO Bool) -> DGNodeLab -> IO Bool)
-> (MVar () -> IO Bool) -> DGNodeLab -> IO Bool
forall a b. (a -> b) -> a -> b
$ (MVar () -> () -> IO Bool) -> () -> MVar () -> IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip MVar () -> () -> IO Bool
forall a. MVar a -> a -> IO Bool
tryPutMVar ()

-- | Releases the local lock.
unlockLocal :: DGNodeLab -> IO ()
unlockLocal :: DGNodeLab -> IO ()
unlockLocal = (MVar () -> IO ()) -> DGNodeLab -> IO ()
forall a. (MVar () -> a) -> DGNodeLab -> a
treatNodeLock ((MVar () -> IO ()) -> DGNodeLab -> IO ())
-> (MVar () -> IO ()) -> DGNodeLab -> IO ()
forall a b. (a -> b) -> a -> b
$ \ lock :: MVar ()
lock ->
  MVar () -> IO (Maybe ())
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar ()
lock IO (Maybe ()) -> (Maybe () -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO () -> (() -> IO ()) -> Maybe () -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> IO ()
forall a. HasCallStack => String -> a
error "Local lock wasn't locked.") () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return

-- | checks if locking MVar is initialized
hasLock :: DGNodeLab -> Bool
hasLock :: DGNodeLab -> Bool
hasLock = Maybe (MVar ()) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (MVar ()) -> Bool)
-> (DGNodeLab -> Maybe (MVar ())) -> DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> Maybe (MVar ())
dgn_lock

-- ** edge label equalities

-- | equality without comparing the edge ids
eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabContent l1 :: DGLinkLab
l1 l2 :: DGLinkLab
l2 = let
    i1 :: EdgeId
i1 = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l1
    i2 :: EdgeId
i2 = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l2
  in (EdgeId
i1 EdgeId -> EdgeId -> Bool
forall a. Ord a => a -> a -> Bool
<= EdgeId
defaultEdgeId Bool -> Bool -> Bool
|| EdgeId
i2 EdgeId -> EdgeId -> Bool
forall a. Ord a => a -> a -> Bool
<= EdgeId
defaultEdgeId Bool -> Bool -> Bool
|| EdgeId
i1 EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== EdgeId
i2)
  Bool -> Bool -> Bool
&& DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l1 GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l2
  Bool -> Bool -> Bool
&& DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l1 DGLinkType -> DGLinkType -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l2
  Bool -> Bool -> Bool
&& DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
l1 DGLinkOrigin -> DGLinkOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
l2
  Bool -> Bool -> Bool
&& DGLinkLab -> String
dglName DGLinkLab
l1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> String
dglName DGLinkLab
l2

-- | equality comparing ids only
eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabById l1 :: DGLinkLab
l1 l2 :: DGLinkLab
l2 = let
    i1 :: EdgeId
i1 = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l1
    i2 :: EdgeId
i2 = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l2
    in if EdgeId
i1 EdgeId -> EdgeId -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeId
defaultEdgeId Bool -> Bool -> Bool
&& EdgeId
i2 EdgeId -> EdgeId -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeId
defaultEdgeId then EdgeId
i1 EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== EdgeId
i2 else
       String -> Bool
forall a. HasCallStack => String -> a
error "eqDGLinkLabById"

-- ** setting index maps

{- these index maps should be global for all libraries,
   therefore their contents need to be copied -}
cpIndexMaps :: DGraph -> DGraph -> DGraph
cpIndexMaps :: DGraph -> DGraph -> DGraph
cpIndexMaps from :: DGraph
from to :: DGraph
to =
  DGraph
to { sigMap :: Map SigId G_sign
sigMap = DGraph -> Map SigId G_sign
sigMap DGraph
from
     , thMap :: Map ThId G_theory
thMap = DGraph -> Map ThId G_theory
thMap DGraph
from
     , morMap :: Map MorId G_morphism
morMap = DGraph -> Map MorId G_morphism
morMap DGraph
from }

setSigMapDG :: Map.Map SigId G_sign -> DGraph -> DGraph
setSigMapDG :: Map SigId G_sign -> DGraph -> DGraph
setSigMapDG m :: Map SigId G_sign
m dg :: DGraph
dg = DGraph
dg { sigMap :: Map SigId G_sign
sigMap = Map SigId G_sign
m }

setThMapDG :: Map.Map ThId G_theory -> DGraph -> DGraph
setThMapDG :: Map ThId G_theory -> DGraph -> DGraph
setThMapDG m :: Map ThId G_theory
m dg :: DGraph
dg = DGraph
dg { thMap :: Map ThId G_theory
thMap = Map ThId G_theory
m }

setMorMapDG :: Map.Map MorId G_morphism -> DGraph -> DGraph
setMorMapDG :: Map MorId G_morphism -> DGraph -> DGraph
setMorMapDG m :: Map MorId G_morphism
m dg :: DGraph
dg = DGraph
dg { morMap :: Map MorId G_morphism
morMap = Map MorId G_morphism
m }

-- ** looking up in index maps

lookupSigMapDG :: SigId -> DGraph -> Maybe G_sign
lookupSigMapDG :: SigId -> DGraph -> Maybe G_sign
lookupSigMapDG i :: SigId
i = SigId -> Map SigId G_sign -> Maybe G_sign
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SigId
i (Map SigId G_sign -> Maybe G_sign)
-> (DGraph -> Map SigId G_sign) -> DGraph -> Maybe G_sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Map SigId G_sign
sigMap

lookupThMapDG :: ThId -> DGraph -> Maybe G_theory
lookupThMapDG :: ThId -> DGraph -> Maybe G_theory
lookupThMapDG i :: ThId
i = ThId -> Map ThId G_theory -> Maybe G_theory
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThId
i (Map ThId G_theory -> Maybe G_theory)
-> (DGraph -> Map ThId G_theory) -> DGraph -> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Map ThId G_theory
thMap

lookupMorMapDG :: MorId -> DGraph -> Maybe G_morphism
lookupMorMapDG :: MorId -> DGraph -> Maybe G_morphism
lookupMorMapDG i :: MorId
i = MorId -> Map MorId G_morphism -> Maybe G_morphism
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup MorId
i (Map MorId G_morphism -> Maybe G_morphism)
-> (DGraph -> Map MorId G_morphism) -> DGraph -> Maybe G_morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Map MorId G_morphism
morMap

-- ** getting index maps and their maximal index

sigMapI :: DGraph -> (Map.Map SigId G_sign, SigId)
sigMapI :: DGraph -> (Map SigId G_sign, SigId)
sigMapI = SigId
-> (DGraph -> Map SigId G_sign)
-> DGraph
-> (Map SigId G_sign, SigId)
forall k b a. Ord k => k -> (b -> Map k a) -> b -> (Map k a, k)
getMapAndMaxIndex SigId
startSigId DGraph -> Map SigId G_sign
sigMap

thMapI :: DGraph -> (Map.Map ThId G_theory, ThId)
thMapI :: DGraph -> (Map ThId G_theory, ThId)
thMapI = ThId
-> (DGraph -> Map ThId G_theory)
-> DGraph
-> (Map ThId G_theory, ThId)
forall k b a. Ord k => k -> (b -> Map k a) -> b -> (Map k a, k)
getMapAndMaxIndex ThId
startThId DGraph -> Map ThId G_theory
thMap

morMapI :: DGraph -> (Map.Map MorId G_morphism, MorId)
morMapI :: DGraph -> (Map MorId G_morphism, MorId)
morMapI = MorId
-> (DGraph -> Map MorId G_morphism)
-> DGraph
-> (Map MorId G_morphism, MorId)
forall k b a. Ord k => k -> (b -> Map k a) -> b -> (Map k a, k)
getMapAndMaxIndex MorId
startMorId DGraph -> Map MorId G_morphism
morMap

-- ** lookup other graph parts

lookupGlobalEnvDG :: IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG :: IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG sid :: IRI
sid dg :: DGraph
dg = let
    gEnv :: GlobalEnv
gEnv = DGraph -> GlobalEnv
globalEnv DGraph
dg
    shortIRI :: String
shortIRI = IRI -> String
iriToStringShortUnsecure IRI
sid
    in case IRI -> GlobalEnv -> Maybe GlobalEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
sid GlobalEnv
gEnv of
    Nothing -> String -> Map String GlobalEntry -> Maybe GlobalEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
shortIRI (Map String GlobalEntry -> Maybe GlobalEntry)
-> Map String GlobalEntry -> Maybe GlobalEntry
forall a b. (a -> b) -> a -> b
$
               (IRI -> String) -> GlobalEnv -> Map String GlobalEntry
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys IRI -> String
iriToStringShortUnsecure GlobalEnv
gEnv
    m :: Maybe GlobalEntry
m -> Maybe GlobalEntry
m

-- | lookup a reference node for a given libname and node
lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node
lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node
lookupInAllRefNodesDG ref :: DGNodeInfo
ref dg :: DGraph
dg = case DGNodeInfo
ref of
    DGRef libn :: LibName
libn refn :: Node
refn ->
        (LibName, Node) -> Map (LibName, Node) Node -> Maybe Node
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName
libn, Node
refn) (Map (LibName, Node) Node -> Maybe Node)
-> Map (LibName, Node) Node -> Maybe Node
forall a b. (a -> b) -> a -> b
$ DGraph -> Map (LibName, Node) Node
allRefNodes DGraph
dg
    _ -> Maybe Node
forall a. Maybe a
Nothing

-- ** lookup nodes by their names or other properties

{- | lookup a node in the graph by its name, using showName
to convert nodenames. -}
lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab]
lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab]
lookupNodeByName s :: String
s dg :: DGraph
dg = (Node -> LNode DGNodeLab) -> [Node] -> [LNode DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Node
n -> (Node
n, DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
n)) ([Node] -> [LNode DGNodeLab])
-> (MapSet String Node -> [Node])
-> MapSet String Node
-> [LNode DGNodeLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Node -> [Node]
forall a. Set a -> [a]
Set.toList
  (Set Node -> [Node])
-> (MapSet String Node -> Set Node) -> MapSet String Node -> [Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> MapSet String Node -> Set Node
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup String
s (MapSet String Node -> [LNode DGNodeLab])
-> MapSet String Node -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> MapSet String Node
nameMap DGraph
dg

lookupUniqueNodeByName :: String -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName :: String -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName s :: String
s dg :: DGraph
dg =
  case Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> Set Node -> [Node]
forall a b. (a -> b) -> a -> b
$ String -> MapSet String Node -> Set Node
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup String
s (MapSet String Node -> Set Node) -> MapSet String Node -> Set Node
forall a b. (a -> b) -> a -> b
$ DGraph -> MapSet String Node
nameMap DGraph
dg of
    [n :: Node
n] -> do
      DGNodeLab
l <- Gr DGNodeLab DGLinkLab -> Node -> Maybe DGNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg) Node
n
      LNode DGNodeLab -> Maybe (LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
n, DGNodeLab
l)
    _ -> Maybe (LNode DGNodeLab)
forall a. Maybe a
Nothing

{- | filters all local nodes in the graph by their names, using showName
to convert nodenames. See also 'lookupNodeByName'. -}
filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab]
filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab]
filterLocalNodesByName s :: String
s = (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (LNode DGNodeLab -> Bool) -> LNode DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> Bool
isDGRef (DGNodeLab -> Bool)
-> (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd) ([LNode DGNodeLab] -> [LNode DGNodeLab])
-> (DGraph -> [LNode DGNodeLab]) -> DGraph -> [LNode DGNodeLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> DGraph -> [LNode DGNodeLab]
lookupNodeByName String
s

{- | filter all ref nodes in the graph by their names, using showName
to convert nodenames. See also 'lookupNodeByName'. -}
filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab]
filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab]
filterRefNodesByName s :: String
s ln :: LibName
ln =
  (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, lbl :: DGNodeLab
lbl) -> DGNodeLab -> Bool
isDGRef DGNodeLab
lbl Bool -> Bool -> Bool
&& DGNodeLab -> LibName
dgn_libname DGNodeLab
lbl LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln)
  ([LNode DGNodeLab] -> [LNode DGNodeLab])
-> (DGraph -> [LNode DGNodeLab]) -> DGraph -> [LNode DGNodeLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> DGraph -> [LNode DGNodeLab]
lookupNodeByName String
s

{- | Given a 'LibEnv' we search each DGraph in it for a (maybe referenced) node
 with the given name. We return the labeled node and the Graph where this node
 resides as local node. See also 'lookupLocalNode'. -}
lookupLocalNodeByNameInEnv :: LibEnv -> String
  -> Maybe (DGraph, LNode DGNodeLab)
lookupLocalNodeByNameInEnv :: LibEnv -> String -> Maybe (DGraph, LNode DGNodeLab)
lookupLocalNodeByNameInEnv le :: LibEnv
le s :: String
s = [DGraph] -> Maybe (DGraph, LNode DGNodeLab)
f ([DGraph] -> Maybe (DGraph, LNode DGNodeLab))
-> [DGraph] -> Maybe (DGraph, LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ LibEnv -> [DGraph]
forall k a. Map k a -> [a]
Map.elems LibEnv
le where
    f :: [DGraph] -> Maybe (DGraph, LNode DGNodeLab)
f [] = Maybe (DGraph, LNode DGNodeLab)
forall a. Maybe a
Nothing
    f (dg :: DGraph
dg : l :: [DGraph]
l) = case String -> DGraph -> [LNode DGNodeLab]
lookupNodeByName String
s DGraph
dg of
                 (nd :: Node
nd, _) : _ -> (DGraph, LNode DGNodeLab) -> Maybe (DGraph, LNode DGNodeLab)
forall a. a -> Maybe a
Just ((DGraph, LNode DGNodeLab) -> Maybe (DGraph, LNode DGNodeLab))
-> (DGraph, LNode DGNodeLab) -> Maybe (DGraph, LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)
lookupLocalNode LibEnv
le DGraph
dg Node
nd
                 _ -> [DGraph] -> Maybe (DGraph, LNode DGNodeLab)
f [DGraph]
l

{- | We search only the given 'DGraph' for a (maybe referenced) node with the
 given name. We return the labeled node and the Graph where this node resides
 as local node. See also 'lookupLocalNode'. -}
lookupLocalNodeByName :: LibEnv -> DGraph -> String
  -> Maybe (DGraph, LNode DGNodeLab)
lookupLocalNodeByName :: LibEnv -> DGraph -> String -> Maybe (DGraph, LNode DGNodeLab)
lookupLocalNodeByName le :: LibEnv
le dg :: DGraph
dg s :: String
s =
    case String -> DGraph -> [LNode DGNodeLab]
lookupNodeByName String
s DGraph
dg of
      (nd :: Node
nd, _) : _ -> (DGraph, LNode DGNodeLab) -> Maybe (DGraph, LNode DGNodeLab)
forall a. a -> Maybe a
Just ((DGraph, LNode DGNodeLab) -> Maybe (DGraph, LNode DGNodeLab))
-> (DGraph, LNode DGNodeLab) -> Maybe (DGraph, LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)
lookupLocalNode LibEnv
le DGraph
dg Node
nd
      _ -> Maybe (DGraph, LNode DGNodeLab)
forall a. Maybe a
Nothing

{- | Given a Node and a 'DGraph' we follow the node to the graph where it is
 defined as a local node. -}
lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)
lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)
lookupLocalNode le :: LibEnv
le dg :: DGraph
dg n :: Node
n = let
  (_, refDg :: DGraph
refDg, p :: LNode DGNodeLab
p) = LibEnv
-> Maybe LibName
-> DGraph
-> Node
-> (Maybe LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM LibEnv
le Maybe LibName
forall a. Maybe a
Nothing DGraph
dg Node
n
  in (DGraph
refDg, LNode DGNodeLab
p)

{- | Given a Node and a 'DGraph' we follow the node to the graph where it is
 defined . -}
lookupRefNode :: LibEnv -> LibName -> DGraph -> Node
   -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNode :: LibEnv
-> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNode le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg n :: Node
n = let
  (mLn :: Maybe LibName
mLn, refDg :: DGraph
refDg, p :: LNode DGNodeLab
p) = LibEnv
-> Maybe LibName
-> DGraph
-> Node
-> (Maybe LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM LibEnv
le Maybe LibName
forall a. Maybe a
Nothing DGraph
dg Node
n
  in (LibName -> Maybe LibName -> LibName
forall a. a -> Maybe a -> a
fromMaybe LibName
ln Maybe LibName
mLn, DGraph
refDg, LNode DGNodeLab
p)

lookupRefNodeM :: LibEnv -> Maybe LibName -> DGraph -> Node
   -> (Maybe LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM :: LibEnv
-> Maybe LibName
-> DGraph
-> Node
-> (Maybe LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM le :: LibEnv
le libName :: Maybe LibName
libName dg :: DGraph
dg n :: Node
n = let x :: DGNodeLab
x = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
n in
  if DGNodeLab -> Bool
isDGRef DGNodeLab
x then let
    ln :: LibName
ln = DGNodeLab -> LibName
dgn_libname DGNodeLab
x
    n' :: Node
n' = DGNodeLab -> Node
dgn_node DGNodeLab
x in LibEnv
-> Maybe LibName
-> DGraph
-> Node
-> (Maybe LibName, DGraph, LNode DGNodeLab)
lookupRefNodeM LibEnv
le (LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
ln) (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le) Node
n'
  else (Maybe LibName
libName, DGraph
dg, (Node
n, DGNodeLab
x))

-- ** accessing the actual graph

-- | get the next available node id
getNewNodeDG :: DGraph -> Node
getNewNodeDG :: DGraph -> Node
getNewNodeDG = Gr DGNodeLab DGLinkLab -> Node
forall a b. Gr a b -> Node
Tree.getNewNode (Gr DGNodeLab DGLinkLab -> Node)
-> (DGraph -> Gr DGNodeLab DGLinkLab) -> DGraph -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | get all the nodes
labNodesDG :: DGraph -> [LNode DGNodeLab]
labNodesDG :: DGraph -> [LNode DGNodeLab]
labNodesDG = Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab])
-> (DGraph -> Gr DGNodeLab DGLinkLab)
-> DGraph
-> [LNode DGNodeLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | get all the edges
labEdgesDG :: DGraph -> [LEdge DGLinkLab]
labEdgesDG :: DGraph -> [LEdge DGLinkLab]
labEdgesDG = Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab])
-> (DGraph -> Gr DGNodeLab DGLinkLab)
-> DGraph
-> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | checks if a DG is empty or not.
isEmptyDG :: DGraph -> Bool
isEmptyDG :: DGraph -> Bool
isEmptyDG = Gr DGNodeLab DGLinkLab -> Bool
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Bool
isEmpty (Gr DGNodeLab DGLinkLab -> Bool)
-> (DGraph -> Gr DGNodeLab DGLinkLab) -> DGraph -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | checks if a given node belongs to a given DG
gelemDG :: Node -> DGraph -> Bool
gelemDG :: Node -> DGraph -> Bool
gelemDG n :: Node
n = Node -> Gr DGNodeLab DGLinkLab -> Bool
forall (gr :: * -> * -> *) a b. Graph gr => Node -> gr a b -> Bool
gelem Node
n (Gr DGNodeLab DGLinkLab -> Bool)
-> (DGraph -> Gr DGNodeLab DGLinkLab) -> DGraph -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | get all the incoming ledges of the given node in a given DG
innDG :: DGraph -> Node -> [LEdge DGLinkLab]
innDG :: DGraph -> Node -> [LEdge DGLinkLab]
innDG = Gr DGNodeLab DGLinkLab -> Node -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
inn (Gr DGNodeLab DGLinkLab -> Node -> [LEdge DGLinkLab])
-> (DGraph -> Gr DGNodeLab DGLinkLab)
-> DGraph
-> Node
-> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | get all the outgoing ledges of the given node in a given DG
outDG :: DGraph -> Node -> [LEdge DGLinkLab]
outDG :: DGraph -> Node -> [LEdge DGLinkLab]
outDG = Gr DGNodeLab DGLinkLab -> Node -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
out (Gr DGNodeLab DGLinkLab -> Node -> [LEdge DGLinkLab])
-> (DGraph -> Gr DGNodeLab DGLinkLab)
-> DGraph
-> Node
-> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | get all the nodes of the given DG
nodesDG :: DGraph -> [Node]
nodesDG :: DGraph -> [Node]
nodesDG = Gr DGNodeLab DGLinkLab -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes (Gr DGNodeLab DGLinkLab -> [Node])
-> (DGraph -> Gr DGNodeLab DGLinkLab) -> DGraph -> [Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | tries to get the label of the given node in a given DG
labDG :: DGraph -> Node -> DGNodeLab
labDG :: DGraph -> Node -> DGNodeLab
labDG dg :: DGraph
dg n :: Node
n = DGNodeLab -> Maybe DGNodeLab -> DGNodeLab
forall a. a -> Maybe a -> a
fromMaybe (String -> DGNodeLab
forall a. HasCallStack => String -> a
error (String -> DGNodeLab) -> String -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ "labDG " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
n) (Maybe DGNodeLab -> DGNodeLab) -> Maybe DGNodeLab -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> Node -> Maybe DGNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg) Node
n

-- | tries to get the label of the given node in a given RT
labRT :: DGraph -> Node -> RTNodeLab
labRT :: DGraph -> Node -> RTNodeLab
labRT dg :: DGraph
dg = RTNodeLab -> Maybe RTNodeLab -> RTNodeLab
forall a. a -> Maybe a -> a
fromMaybe (String -> RTNodeLab
forall a. HasCallStack => String -> a
error "labRT") (Maybe RTNodeLab -> RTNodeLab)
-> (Node -> Maybe RTNodeLab) -> Node -> RTNodeLab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gr RTNodeLab RTLinkLab -> Node -> Maybe RTNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (DGraph -> Gr RTNodeLab RTLinkLab
refTree DGraph
dg)


-- | get the name of a node from the number of node
getNameOfNode :: Node -> DGraph -> String
getNameOfNode :: Node -> DGraph -> String
getNameOfNode index :: Node
index gc :: DGraph
gc = DGNodeLab -> String
getDGNodeName (DGNodeLab -> String) -> DGNodeLab -> String
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
gc Node
index

-- | gets the given number of new node-ids in a given DG.
newNodesDG :: Int -> DGraph -> [Node]
newNodesDG :: Node -> DGraph -> [Node]
newNodesDG n :: Node
n = Node -> Gr DGNodeLab DGLinkLab -> [Node]
forall (gr :: * -> * -> *) a b.
Graph gr =>
Node -> gr a b -> [Node]
newNodes Node
n (Gr DGNodeLab DGLinkLab -> [Node])
-> (DGraph -> Gr DGNodeLab DGLinkLab) -> DGraph -> [Node]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody

-- | get the context and throw input string as error message
safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab
safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab
safeContextDG s :: String
s = String
-> Gr DGNodeLab DGLinkLab -> Node -> Context DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
String -> gr a b -> Node -> Context a b
safeContext String
s (Gr DGNodeLab DGLinkLab -> Node -> Context DGNodeLab DGLinkLab)
-> (DGraph -> Gr DGNodeLab DGLinkLab)
-> DGraph
-> Node
-> Context DGNodeLab DGLinkLab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Gr DGNodeLab DGLinkLab
dgBody where
  safeContext :: String -> gr a b -> Node -> Context a b
safeContext err :: String
err g :: gr a b
g v :: Node
v = -- same as context with extra message
    Context a b -> Maybe (Context a b) -> Context a b
forall a. a -> Maybe a -> a
fromMaybe (String -> Context a b
forall a. HasCallStack => String -> a
error (String -> Context a b) -> String -> Context a b
forall a b. (a -> b) -> a -> b
$ String
err String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": Match Exception, Node: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
v)
    (Maybe (Context a b) -> Context a b)
-> ((Maybe (Context a b), gr a b) -> Maybe (Context a b))
-> (Maybe (Context a b), gr a b)
-> Context a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (Context a b), gr a b) -> Maybe (Context a b)
forall a b. (a, b) -> a
fst ((Maybe (Context a b), gr a b) -> Context a b)
-> (Maybe (Context a b), gr a b) -> Context a b
forall a b. (a -> b) -> a -> b
$ Node -> gr a b -> (Maybe (Context a b), gr a b)
forall (gr :: * -> * -> *) a b.
Graph gr =>
Node -> gr a b -> Decomp gr a b
match Node
v gr a b
g

-- ** manipulate graph

-- | sets the node with new label and returns the new graph and the old label
labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG p :: LNode DGNodeLab
p@(n :: Node
n, lbl :: DGNodeLab
lbl) dg :: DGraph
dg =
    let (b :: Gr DGNodeLab DGLinkLab
b, l :: DGNodeLab
l) = LNode DGNodeLab
-> Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, DGNodeLab)
forall a b. LNode a -> Gr a b -> (Gr a b, a)
Tree.labelNode LNode DGNodeLab
p (Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, DGNodeLab))
-> Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, DGNodeLab)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
        oldN :: String
oldN = DGNodeLab -> String
getDGNodeName DGNodeLab
l
        newN :: String
newN = DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
        oldInf :: DGNodeInfo
oldInf = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
l
        newInf :: DGNodeInfo
newInf = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lbl
        nMap :: MapSet String Node
nMap = DGraph -> MapSet String Node
nameMap DGraph
dg
        refs :: Map (LibName, Node) Node
refs = DGraph -> Map (LibName, Node) Node
allRefNodes DGraph
dg
    in (DGraph
dg { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = Gr DGNodeLab DGLinkLab
b
           , nameMap :: MapSet String Node
nameMap = if String
oldN String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
newN then MapSet String Node
nMap else
               String -> Node -> MapSet String Node -> MapSet String Node
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert String
newN Node
n (MapSet String Node -> MapSet String Node)
-> MapSet String Node -> MapSet String Node
forall a b. (a -> b) -> a -> b
$ String -> Node -> MapSet String Node -> MapSet String Node
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete String
oldN Node
n MapSet String Node
nMap
           , allRefNodes :: Map (LibName, Node) Node
allRefNodes = case (DGNodeInfo
oldInf, DGNodeInfo
newInf) of
               (DGRef libn :: LibName
libn refn :: Node
refn, DGRef nLibn :: LibName
nLibn nRefn :: Node
nRefn) ->
                   if DGNodeInfo
newInf DGNodeInfo -> DGNodeInfo -> Bool
forall a. Eq a => a -> a -> Bool
== DGNodeInfo
oldInf then Map (LibName, Node) Node
refs
                     else (LibName, Node)
-> Node -> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
nLibn, Node
nRefn) Node
n
                          (Map (LibName, Node) Node -> Map (LibName, Node) Node)
-> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall a b. (a -> b) -> a -> b
$ (LibName, Node)
-> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (LibName
libn, Node
refn) Map (LibName, Node) Node
refs
               (DGRef libn :: LibName
libn refn :: Node
refn, _) -> (LibName, Node)
-> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (LibName
libn, Node
refn) Map (LibName, Node) Node
refs
               (_, DGRef nLibn :: LibName
nLibn nRefn :: Node
nRefn) -> (LibName, Node)
-> Node -> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
nLibn, Node
nRefn) Node
n Map (LibName, Node) Node
refs
               _ -> Map (LibName, Node) Node
refs }, DGNodeLab
l)

-- | delete the node out of the given DG
delNodeDG :: Node -> DGraph -> DGraph
delNodeDG :: Node -> DGraph -> DGraph
delNodeDG n :: Node
n dg :: DGraph
dg = case Node -> Gr DGNodeLab DGLinkLab -> Decomp Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
Node -> gr a b -> Decomp gr a b
match Node
n (Gr DGNodeLab DGLinkLab -> Decomp Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Decomp Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg of
  (Just (_, _, lbl :: DGNodeLab
lbl, _), rg :: Gr DGNodeLab DGLinkLab
rg) -> let refs :: Map (LibName, Node) Node
refs = DGraph -> Map (LibName, Node) Node
allRefNodes DGraph
dg in DGraph
dg
     { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = Gr DGNodeLab DGLinkLab
rg
     , nameMap :: MapSet String Node
nameMap = String -> Node -> MapSet String Node -> MapSet String Node
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete (DGNodeLab -> String
getDGNodeName DGNodeLab
lbl) Node
n (MapSet String Node -> MapSet String Node)
-> MapSet String Node -> MapSet String Node
forall a b. (a -> b) -> a -> b
$ DGraph -> MapSet String Node
nameMap DGraph
dg
     , allRefNodes :: Map (LibName, Node) Node
allRefNodes = case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lbl of
         DGRef libn :: LibName
libn refn :: Node
refn -> (LibName, Node)
-> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (LibName
libn, Node
refn) Map (LibName, Node) Node
refs
         _ -> Map (LibName, Node) Node
refs }
  _ -> String -> DGraph
forall a. HasCallStack => String -> a
error (String -> DGraph) -> String -> DGraph
forall a b. (a -> b) -> a -> b
$ "delNodeDG " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
n

-- | delete a list of nodes out of the given DG
delNodesDG :: [Node] -> DGraph -> DGraph
delNodesDG :: [Node] -> DGraph -> DGraph
delNodesDG = (DGraph -> [Node] -> DGraph) -> [Node] -> DGraph -> DGraph
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((DGraph -> [Node] -> DGraph) -> [Node] -> DGraph -> DGraph)
-> (DGraph -> [Node] -> DGraph) -> [Node] -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ (Node -> DGraph -> DGraph) -> DGraph -> [Node] -> DGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Node -> DGraph -> DGraph
delNodeDG

-- | insert a new node into given DGraph
insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
insNodeDG n :: LNode DGNodeLab
n@(i :: Node
i, l :: DGNodeLab
l) dg :: DGraph
dg = let refs :: Map (LibName, Node) Node
refs = DGraph -> Map (LibName, Node) Node
allRefNodes DGraph
dg in DGraph
dg
  { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = LNode DGNodeLab -> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode LNode DGNodeLab
n (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
  , nameMap :: MapSet String Node
nameMap = String -> Node -> MapSet String Node -> MapSet String Node
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (DGNodeLab -> String
getDGNodeName DGNodeLab
l) Node
i (MapSet String Node -> MapSet String Node)
-> MapSet String Node -> MapSet String Node
forall a b. (a -> b) -> a -> b
$ DGraph -> MapSet String Node
nameMap DGraph
dg
  , allRefNodes :: Map (LibName, Node) Node
allRefNodes = case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
l of
      DGRef libn :: LibName
libn refn :: Node
refn -> (LibName, Node)
-> Node -> Map (LibName, Node) Node -> Map (LibName, Node) Node
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
libn, Node
refn) Node
i Map (LibName, Node) Node
refs
      _ -> Map (LibName, Node) Node
refs }

-- | inserts a lnode into a given DG
insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG n :: LNode DGNodeLab
n@(v :: Node
v, _) g :: DGraph
g =
    if Node -> DGraph -> Bool
gelemDG Node
v DGraph
g then String -> DGraph
forall a. HasCallStack => String -> a
error (String -> DGraph) -> String -> DGraph
forall a b. (a -> b) -> a -> b
$ "insLNodeDG " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
v else LNode DGNodeLab -> DGraph -> DGraph
insNodeDG LNode DGNodeLab
n DGraph
g

-- | insert a new node with the given node content into a given DGraph
insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph
insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph
insNodesDG = (DGraph -> [LNode DGNodeLab] -> DGraph)
-> [LNode DGNodeLab] -> DGraph -> DGraph
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((DGraph -> [LNode DGNodeLab] -> DGraph)
 -> [LNode DGNodeLab] -> DGraph -> DGraph)
-> (DGraph -> [LNode DGNodeLab] -> DGraph)
-> [LNode DGNodeLab]
-> DGraph
-> DGraph
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> DGraph -> DGraph)
-> DGraph -> [LNode DGNodeLab] -> DGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr LNode DGNodeLab -> DGraph -> DGraph
insNodeDG

-- | delete a labeled edge out of the given DG
delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph
delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph
delLEdgeDG e :: LEdge DGLinkLab
e g :: DGraph
g = DGraph
g
    { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = (DGLinkLab -> DGLinkLab -> Ordering)
-> LEdge DGLinkLab
-> Gr DGNodeLab DGLinkLab
-> Gr DGNodeLab DGLinkLab
forall b a. (b -> b -> Ordering) -> LEdge b -> Gr a b -> Gr a b
Tree.delLEdge ((DGLinkLab -> EdgeId) -> DGLinkLab -> DGLinkLab -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing DGLinkLab -> EdgeId
dgl_id) LEdge DGLinkLab
e
      (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
g }

-- | inserts an edge between two nodes, labelled with inclusion
insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig ->
                  Result DGraph
insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> Result DGraph
insInclEdgeDG lgraph :: LogicGraph
lgraph dg :: DGraph
dg s :: NodeSig
s t :: NodeSig
t = do
  GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lgraph (NodeSig -> G_sign
getSig NodeSig
s) (NodeSig -> G_sign
getSig NodeSig
t)
  let l :: DGLinkLab
l = GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
incl DGLinkOrigin
DGLinkImports
      (_, dg' :: DGraph
dg') = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (NodeSig -> Node
getNode NodeSig
s, NodeSig -> Node
getNode NodeSig
t, DGLinkLab
l) DGraph
dg
  DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg'

-- | insert a labeled edge into a given DG, return possibly new id of edge
insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (s :: Node
s, t :: Node
t, l :: DGLinkLab
l) g :: DGraph
g =
  let eId :: EdgeId
eId = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l
      nId :: EdgeId
nId = DGraph -> EdgeId
getNewEdgeId DGraph
g
      newId :: Bool
newId = EdgeId
eId EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== EdgeId
defaultEdgeId
      e :: LEdge DGLinkLab
e = (Node
s, Node
t, if Bool
newId then DGLinkLab
l { dgl_id :: EdgeId
dgl_id = EdgeId
nId } else DGLinkLab
l)
  in (LEdge DGLinkLab
e, DGraph
g
    { getNewEdgeId :: EdgeId
getNewEdgeId = if Bool
newId then EdgeId -> EdgeId
incEdgeId EdgeId
nId else EdgeId -> EdgeId -> EdgeId
forall a. Ord a => a -> a -> a
max EdgeId
nId (EdgeId -> EdgeId) -> EdgeId -> EdgeId
forall a b. (a -> b) -> a -> b
$ EdgeId -> EdgeId
incEdgeId EdgeId
eId
    , dgBody :: Gr DGNodeLab DGLinkLab
dgBody = (Gr DGNodeLab DGLinkLab, Bool) -> Gr DGNodeLab DGLinkLab
forall a b. (a, b) -> a
fst ((Gr DGNodeLab DGLinkLab, Bool) -> Gr DGNodeLab DGLinkLab)
-> (Gr DGNodeLab DGLinkLab, Bool) -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ Bool
-> (DGLinkLab -> DGLinkLab -> Ordering)
-> LEdge DGLinkLab
-> Gr DGNodeLab DGLinkLab
-> (Gr DGNodeLab DGLinkLab, Bool)
forall b a.
Bool -> (b -> b -> Ordering) -> LEdge b -> Gr a b -> (Gr a b, Bool)
Tree.insLEdge Bool
True DGLinkLab -> DGLinkLab -> Ordering
compareLinks LEdge DGLinkLab
e (Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, Bool))
-> Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, Bool)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
g })

compareLinks :: DGLinkLab -> DGLinkLab -> Ordering
compareLinks :: DGLinkLab -> DGLinkLab -> Ordering
compareLinks l1 :: DGLinkLab
l1 l2 :: DGLinkLab
l2 = if DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabContent DGLinkLab
l1 { dgl_id :: EdgeId
dgl_id = EdgeId
defaultEdgeId } DGLinkLab
l2
        then Ordering
EQ else (DGLinkLab -> EdgeId) -> DGLinkLab -> DGLinkLab -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing DGLinkLab -> EdgeId
dgl_id DGLinkLab
l1 DGLinkLab
l2

{- | tries to insert a labeled edge into a given DG, but if this edge
     already exists, then does nothing. -}
insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph
insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph
insLEdgeNubDG (v :: Node
v, w :: Node
w, l :: DGLinkLab
l) g :: DGraph
g =
  let oldEdgeId :: EdgeId
oldEdgeId = DGraph -> EdgeId
getNewEdgeId DGraph
g
      (ng :: Gr DGNodeLab DGLinkLab
ng, change :: Bool
change) = Bool
-> (DGLinkLab -> DGLinkLab -> Ordering)
-> LEdge DGLinkLab
-> Gr DGNodeLab DGLinkLab
-> (Gr DGNodeLab DGLinkLab, Bool)
forall b a.
Bool -> (b -> b -> Ordering) -> LEdge b -> Gr a b -> (Gr a b, Bool)
Tree.insLEdge Bool
False DGLinkLab -> DGLinkLab -> Ordering
compareLinks
        (Node
v, Node
w, DGLinkLab
l { dgl_id :: EdgeId
dgl_id = EdgeId
oldEdgeId }) (Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, Bool))
-> Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, Bool)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
g
  in
     DGraph
g { getNewEdgeId :: EdgeId
getNewEdgeId = if Bool
change then EdgeId -> EdgeId
incEdgeId EdgeId
oldEdgeId else EdgeId
oldEdgeId
       , dgBody :: Gr DGNodeLab DGLinkLab
dgBody = Gr DGNodeLab DGLinkLab
ng }

{- | inserts a new edge into the DGraph using it's own edgeId.
ATTENTION: the caller must ensure that an edgeId is not used twice -}
insEdgeAsIs :: LEdge DGLinkLab -> DGraph -> DGraph
insEdgeAsIs :: LEdge DGLinkLab -> DGraph -> DGraph
insEdgeAsIs (v :: Node
v, w :: Node
w, l :: DGLinkLab
l) g :: DGraph
g = let
  ei :: EdgeId
ei = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l
  in if EdgeId
ei EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== EdgeId
defaultEdgeId then String -> DGraph
forall a. HasCallStack => String -> a
error "illegal link id" else
     DGraph
g { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = (Gr DGNodeLab DGLinkLab, Bool) -> Gr DGNodeLab DGLinkLab
forall a b. (a, b) -> a
fst ((Gr DGNodeLab DGLinkLab, Bool) -> Gr DGNodeLab DGLinkLab)
-> (Gr DGNodeLab DGLinkLab, Bool) -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ Bool
-> (DGLinkLab -> DGLinkLab -> Ordering)
-> LEdge DGLinkLab
-> Gr DGNodeLab DGLinkLab
-> (Gr DGNodeLab DGLinkLab, Bool)
forall b a.
Bool -> (b -> b -> Ordering) -> LEdge b -> Gr a b -> (Gr a b, Bool)
Tree.insLEdge Bool
False DGLinkLab -> DGLinkLab -> Ordering
compareLinks
        (Node
v, Node
w, DGLinkLab
l) (Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, Bool))
-> Gr DGNodeLab DGLinkLab -> (Gr DGNodeLab DGLinkLab, Bool)
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
g }

-- | insert a list of labeled edge into a given DG
insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
insEdgesDG = (DGraph -> [LEdge DGLinkLab] -> DGraph)
-> [LEdge DGLinkLab] -> DGraph -> DGraph
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((DGraph -> [LEdge DGLinkLab] -> DGraph)
 -> [LEdge DGLinkLab] -> DGraph -> DGraph)
-> (DGraph -> [LEdge DGLinkLab] -> DGraph)
-> [LEdge DGLinkLab]
-> DGraph
-> DGraph
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> DGraph -> DGraph)
-> DGraph -> [LEdge DGLinkLab] -> DGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr LEdge DGLinkLab -> DGraph -> DGraph
insLEdgeNubDG

-- | merge a list of lnodes and ledges into a given DG
mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph
mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph
mkGraphDG ns :: [LNode DGNodeLab]
ns ls :: [LEdge DGLinkLab]
ls = [LEdge DGLinkLab] -> DGraph -> DGraph
insEdgesDG [LEdge DGLinkLab]
ls (DGraph -> DGraph) -> (DGraph -> DGraph) -> DGraph -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LNode DGNodeLab] -> DGraph -> DGraph
insNodesDG [LNode DGNodeLab]
ns

-- | get links by id (inefficiently)
getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab]
getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab]
getDGLinksById e :: EdgeId
e = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> EdgeId
e EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkLab -> EdgeId
dgl_id DGLinkLab
l) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> (DGraph -> [LEdge DGLinkLab]) -> DGraph -> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> [LEdge DGLinkLab]
labEdgesDG

-- | find a unique link given its source node and edgeId
lookupUniqueLink :: Fail.MonadFail m => Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)
lookupUniqueLink :: Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)
lookupUniqueLink s :: Node
s ei :: EdgeId
ei dg :: DGraph
dg = let (Just (_, _, _, outs :: Adj DGLinkLab
outs), _) = Node -> Gr DGNodeLab DGLinkLab -> Decomp Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
Node -> gr a b -> Decomp gr a b
match Node
s (Gr DGNodeLab DGLinkLab -> Decomp Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Decomp Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
  in case ((DGLinkLab, Node) -> Bool) -> Adj DGLinkLab -> Adj DGLinkLab
forall a. (a -> Bool) -> [a] -> [a]
filter ((EdgeId -> EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== EdgeId
ei) (EdgeId -> Bool)
-> ((DGLinkLab, Node) -> EdgeId) -> (DGLinkLab, Node) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> EdgeId
dgl_id (DGLinkLab -> EdgeId)
-> ((DGLinkLab, Node) -> DGLinkLab) -> (DGLinkLab, Node) -> EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DGLinkLab, Node) -> DGLinkLab
forall a b. (a, b) -> a
fst) Adj DGLinkLab
outs of
    [] -> String -> m (LEdge DGLinkLab)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (LEdge DGLinkLab)) -> String -> m (LEdge DGLinkLab)
forall a b. (a -> b) -> a -> b
$ "could not find linkId #" String -> ShowS
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
forall a. Show a => a -> String
show EdgeId
ei
    [(lbl :: DGLinkLab
lbl, t :: Node
t)] -> LEdge DGLinkLab -> m (LEdge DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
s, Node
t, DGLinkLab
lbl)
    _ -> String -> m (LEdge DGLinkLab)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (LEdge DGLinkLab)) -> String -> m (LEdge DGLinkLab)
forall a b. (a -> b) -> a -> b
$ "ambigous occurance of linkId #" String -> ShowS
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
forall a. Show a => a -> String
show EdgeId
ei

-- ** top-level functions

-- | initializes the MVar for locking if nessesary
initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab)
initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab)
initLocking dg :: DGraph
dg (node :: Node
node, dgn :: DGNodeLab
dgn) = do
  MVar ()
lock <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
  let dgn' :: DGNodeLab
dgn' = DGNodeLab
dgn { dgn_lock :: Maybe (MVar ())
dgn_lock = MVar () -> Maybe (MVar ())
forall a. a -> Maybe a
Just MVar ()
lock }
  (DGraph, DGNodeLab) -> IO (DGraph, DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return ((DGraph, DGNodeLab) -> DGraph
forall a b. (a, b) -> a
fst ((DGraph, DGNodeLab) -> DGraph) -> (DGraph, DGNodeLab) -> DGraph
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG (Node
node, DGNodeLab
dgn') DGraph
dg, DGNodeLab
dgn')

-- | returns the DGraph that belongs to the given library name
lookupDGraph :: LibName -> LibEnv -> DGraph
lookupDGraph :: LibName -> LibEnv -> DGraph
lookupDGraph ln :: LibName
ln = DGraph -> LibName -> LibEnv -> DGraph
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> DGraph
forall a. HasCallStack => String -> a
error (String -> DGraph) -> String -> DGraph
forall a b. (a -> b) -> a -> b
$ "lookupDGraph " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
ln) LibName
ln

{- | compute the theory of a given node.
   If this node is a DGRef, the referenced node is looked up first. -}
computeLocalTheory :: Monad m => LibEnv -> LibName -> Node -> m G_theory
computeLocalTheory :: LibEnv -> LibName -> Node -> m G_theory
computeLocalTheory libEnv :: LibEnv
libEnv ln :: LibName
ln =
  LibEnv -> DGraph -> Node -> m G_theory
forall (m :: * -> *).
Monad m =>
LibEnv -> DGraph -> Node -> m G_theory
computeLocalNodeTheory LibEnv
libEnv (DGraph -> Node -> m G_theory) -> DGraph -> Node -> m G_theory
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv

computeLocalNodeTheory :: Monad m => LibEnv -> DGraph -> Node -> m G_theory
computeLocalNodeTheory :: LibEnv -> DGraph -> Node -> m G_theory
computeLocalNodeTheory libEnv :: LibEnv
libEnv dg :: DGraph
dg = LibEnv -> DGNodeLab -> m G_theory
forall (m :: * -> *). Monad m => LibEnv -> DGNodeLab -> m G_theory
computeLocalLabelTheory LibEnv
libEnv (DGNodeLab -> m G_theory)
-> (Node -> DGNodeLab) -> Node -> m G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dg

computeLocalLabelTheory :: Monad m => LibEnv -> DGNodeLab -> m G_theory
computeLocalLabelTheory :: LibEnv -> DGNodeLab -> m G_theory
computeLocalLabelTheory libEnv :: LibEnv
libEnv nodeLab :: DGNodeLab
nodeLab =
  if DGNodeLab -> Bool
isDGRef DGNodeLab
nodeLab
    then
      LibEnv -> LibName -> Node -> m G_theory
forall (m :: * -> *).
Monad m =>
LibEnv -> LibName -> Node -> m G_theory
computeLocalTheory LibEnv
libEnv (DGNodeLab -> LibName
dgn_libname DGNodeLab
nodeLab) (Node -> m G_theory) -> Node -> m G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Node
dgn_node DGNodeLab
nodeLab
    else G_theory -> m G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> m G_theory) -> G_theory -> m G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
nodeLab

-- ** test link types

liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE f :: DGLinkType -> a
f (_, _, edgeLab :: DGLinkLab
edgeLab) = DGLinkType -> a
f (DGLinkType -> a) -> DGLinkType -> a
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
edgeLab

isGlobalDef :: DGLinkType -> Bool
isGlobalDef :: DGLinkType -> Bool
isGlobalDef lt :: DGLinkType
lt = case DGLinkType
lt of
    ScopedLink Global DefLink _ -> Bool
True
    _ -> Bool
False

isLocalDef :: DGLinkType -> Bool
isLocalDef :: DGLinkType -> Bool
isLocalDef lt :: DGLinkType
lt = case DGLinkType
lt of
    ScopedLink Local DefLink _ -> Bool
True
    _ -> Bool
False

isHidingDef :: DGLinkType -> Bool
isHidingDef :: DGLinkType -> Bool
isHidingDef lt :: DGLinkType
lt = case DGLinkType
lt of
    HidingDefLink -> Bool
True
    _ -> Bool
False

isDefEdge :: DGLinkType -> Bool
isDefEdge :: DGLinkType -> Bool
isDefEdge edge :: DGLinkType
edge = case DGLinkType
edge of
    ScopedLink _ DefLink _ -> Bool
True
    HidingDefLink -> Bool
True
    FreeOrCofreeDefLink _ _ -> Bool
True
    _ -> Bool
False

isLocalEdge :: DGLinkType -> Bool
isLocalEdge :: DGLinkType -> Bool
isLocalEdge edge :: DGLinkType
edge = case DGLinkType
edge of
    ScopedLink Local _ _ -> Bool
True
    _ -> Bool
False

isHidingEdge :: DGLinkType -> Bool
isHidingEdge :: DGLinkType -> Bool
isHidingEdge edge :: DGLinkType
edge = case DGLinkType
edge of
    HidingDefLink -> Bool
True
    HidingFreeOrCofreeThm Nothing _ _ _ -> Bool
True
    _ -> Bool
False

-- ** create link types

hidingThm :: Node -> GMorphism -> DGLinkType
hidingThm :: Node -> GMorphism -> DGLinkType
hidingThm n :: Node
n m :: GMorphism
m = Maybe FreeOrCofree
-> Node -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm Maybe FreeOrCofree
forall a. Maybe a
Nothing Node
n GMorphism
m ThmLinkStatus
LeftOpen

globalThm :: DGLinkType
globalThm :: DGLinkType
globalThm = Scope -> Conservativity -> DGLinkType
localOrGlobalThm Scope
Global Conservativity
None

localThm :: DGLinkType
localThm :: DGLinkType
localThm = Scope -> Conservativity -> DGLinkType
localOrGlobalThm Scope
Local Conservativity
None

globalConsThm :: Conservativity -> DGLinkType
globalConsThm :: Conservativity -> DGLinkType
globalConsThm = Scope -> Conservativity -> DGLinkType
localOrGlobalThm Scope
Global

localConsThm :: Conservativity -> DGLinkType
localConsThm :: Conservativity -> DGLinkType
localConsThm = Scope -> Conservativity -> DGLinkType
localOrGlobalThm Scope
Local

localOrGlobalThm :: Scope -> Conservativity -> DGLinkType
localOrGlobalThm :: Scope -> Conservativity -> DGLinkType
localOrGlobalThm sc :: Scope
sc = Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc (ThmLinkStatus -> LinkKind
ThmLink ThmLinkStatus
LeftOpen) (ConsStatus -> DGLinkType)
-> (Conservativity -> ConsStatus) -> Conservativity -> DGLinkType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Conservativity -> ConsStatus
mkConsStatus

localOrGlobalDef :: Scope -> Conservativity -> DGLinkType
localOrGlobalDef :: Scope -> Conservativity -> DGLinkType
localOrGlobalDef sc :: Scope
sc = Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc LinkKind
DefLink (ConsStatus -> DGLinkType)
-> (Conservativity -> ConsStatus) -> Conservativity -> DGLinkType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Conservativity -> ConsStatus
mkConsStatus

globalConsDef :: Conservativity -> DGLinkType
globalConsDef :: Conservativity -> DGLinkType
globalConsDef = Scope -> Conservativity -> DGLinkType
localOrGlobalDef Scope
Global

globalDef :: DGLinkType
globalDef :: DGLinkType
globalDef = Scope -> Conservativity -> DGLinkType
localOrGlobalDef Scope
Global Conservativity
None

localDef :: DGLinkType
localDef :: DGLinkType
localDef = Scope -> Conservativity -> DGLinkType
localOrGlobalDef Scope
Local Conservativity
None

-- ** link conservativity

getLinkConsStatus :: DGLinkType -> ConsStatus
getLinkConsStatus :: DGLinkType -> ConsStatus
getLinkConsStatus lt :: DGLinkType
lt = case DGLinkType
lt of
  ScopedLink _ _ c :: ConsStatus
c -> ConsStatus
c
  _ -> Conservativity -> ConsStatus
mkConsStatus Conservativity
None

getEdgeConsStatus :: DGLinkLab -> ConsStatus
getEdgeConsStatus :: DGLinkLab -> ConsStatus
getEdgeConsStatus = DGLinkType -> ConsStatus
getLinkConsStatus (DGLinkType -> ConsStatus)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> ConsStatus
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type

getCons :: DGLinkType -> Conservativity
getCons :: DGLinkType -> Conservativity
getCons = ConsStatus -> Conservativity
getConsOfStatus (ConsStatus -> Conservativity)
-> (DGLinkType -> ConsStatus) -> DGLinkType -> Conservativity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkType -> ConsStatus
getLinkConsStatus

-- | returns the Conservativity if the given edge has one, otherwise none
getConservativity :: LEdge DGLinkLab -> Conservativity
getConservativity :: LEdge DGLinkLab -> Conservativity
getConservativity (_, _, edgeLab :: DGLinkLab
edgeLab) = ConsStatus -> Conservativity
getConsOfStatus (ConsStatus -> Conservativity) -> ConsStatus -> Conservativity
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> ConsStatus
getEdgeConsStatus DGLinkLab
edgeLab

-- | returns the conservativity of the given path
getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity
getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity
getConservativityOfPath path :: [LEdge DGLinkLab]
path = [Conservativity] -> Conservativity
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [LEdge DGLinkLab -> Conservativity
getConservativity LEdge DGLinkLab
e | LEdge DGLinkLab
e <- [LEdge DGLinkLab]
path]

-- * bottom up traversal

-- | Creates a LibName relation wrt dependencies via reference nodes
getLibDepRel :: LibEnv -> Rel.Rel LibName
getLibDepRel :: LibEnv -> Rel LibName
getLibDepRel = Rel LibName -> Rel LibName
forall a. Ord a => Rel a -> Rel a
Rel.transClosure
  (Rel LibName -> Rel LibName)
-> (LibEnv -> Rel LibName) -> LibEnv -> Rel LibName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (LibName, LibName) -> Rel LibName
forall a. Ord a => Set (a, a) -> Rel a
Rel.fromSet (Set (LibName, LibName) -> Rel LibName)
-> (LibEnv -> Set (LibName, LibName)) -> LibEnv -> Rel LibName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibName
 -> DGraph -> Set (LibName, LibName) -> Set (LibName, LibName))
-> Set (LibName, LibName) -> LibEnv -> Set (LibName, LibName)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ ln :: LibName
ln dg :: DGraph
dg s :: Set (LibName, LibName)
s ->
    (LNode DGNodeLab
 -> Set (LibName, LibName) -> Set (LibName, LibName))
-> Set (LibName, LibName)
-> [LNode DGNodeLab]
-> Set (LibName, LibName)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\ x :: DGNodeLab
x -> if DGNodeLab -> Bool
isDGRef DGNodeLab
x then (LibName, LibName)
-> Set (LibName, LibName) -> Set (LibName, LibName)
forall a. Ord a => a -> Set a -> Set a
Set.insert (LibName
ln, DGNodeLab -> LibName
dgn_libname DGNodeLab
x) else Set (LibName, LibName) -> Set (LibName, LibName)
forall a. a -> a
id)
           (DGNodeLab -> Set (LibName, LibName) -> Set (LibName, LibName))
-> (LNode DGNodeLab -> DGNodeLab)
-> LNode DGNodeLab
-> Set (LibName, LibName)
-> Set (LibName, LibName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd) Set (LibName, LibName)
s ([LNode DGNodeLab] -> Set (LibName, LibName))
-> [LNode DGNodeLab] -> Set (LibName, LibName)
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg) Set (LibName, LibName)
forall a. Set a
Set.empty

getTopsortedLibs :: LibEnv -> [LibName]
getTopsortedLibs :: LibEnv -> [LibName]
getTopsortedLibs le :: LibEnv
le = let
  rel :: Rel LibName
rel = LibEnv -> Rel LibName
getLibDepRel LibEnv
le
  ls :: [LibName]
ls = [LibName] -> [LibName]
forall a. [a] -> [a]
reverse ([LibName] -> [LibName]) -> [LibName] -> [LibName]
forall a b. (a -> b) -> a -> b
$ Rel LibName -> [LibName]
topsortedLibsWithImports Rel LibName
rel
  restLs :: [LibName]
restLs = Set LibName -> [LibName]
forall a. Set a -> [a]
Set.toList (Set LibName -> [LibName]) -> Set LibName -> [LibName]
forall a b. (a -> b) -> a -> b
$ Set LibName -> Set LibName -> Set LibName
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (LibEnv -> Set LibName
forall k a. Map k a -> Set k
Map.keysSet LibEnv
le) (Set LibName -> Set LibName) -> Set LibName -> Set LibName
forall a b. (a -> b) -> a -> b
$ Rel LibName -> Set LibName
forall a. Ord a => Rel a -> Set a
Rel.nodes Rel LibName
rel
  in [LibName]
ls [LibName] -> [LibName] -> [LibName]
forall a. [a] -> [a] -> [a]
++ [LibName]
restLs

{- | Get imported libs in topological order, i.e.  lib(s) without imports first.
     The input lib-name will be last -}
dependentLibs :: LibName -> LibEnv -> [LibName]
dependentLibs :: LibName -> LibEnv -> [LibName]
dependentLibs ln :: LibName
ln le :: LibEnv
le =
  let rel :: Rel LibName
rel = LibEnv -> Rel LibName
getLibDepRel LibEnv
le
      ts :: [LibName]
ts = Rel LibName -> [LibName]
topsortedLibsWithImports Rel LibName
rel
      is :: [LibName]
is = Set LibName -> [LibName]
forall a. Set a -> [a]
Set.toList (Rel LibName -> LibName -> Set LibName
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel LibName
rel LibName
ln)
  in [LibName] -> [LibName]
forall a. [a] -> [a]
reverse ([LibName] -> [LibName]) -> [LibName] -> [LibName]
forall a b. (a -> b) -> a -> b
$ LibName
ln LibName -> [LibName] -> [LibName]
forall a. a -> [a] -> [a]
: [LibName] -> [LibName] -> [LibName]
forall a. Eq a => [a] -> [a] -> [a]
intersect [LibName]
ts [LibName]
is

topsortedNodes :: DGraph -> [LNode DGNodeLab]
topsortedNodes :: DGraph -> [LNode DGNodeLab]
topsortedNodes dgraph :: DGraph
dgraph = let dg :: Gr DGNodeLab DGLinkLab
dg = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph in
  [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. [a] -> [a]
reverse ([LNode DGNodeLab] -> [LNode DGNodeLab])
-> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ [Tree (LNode DGNodeLab)] -> [LNode DGNodeLab]
forall a. [Tree a] -> [a]
postorderF ([Tree (LNode DGNodeLab)] -> [LNode DGNodeLab])
-> [Tree (LNode DGNodeLab)] -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ CFun DGNodeLab DGLinkLab (LNode DGNodeLab)
-> [Node] -> Gr DGNodeLab DGLinkLab -> [Tree (LNode DGNodeLab)]
forall (gr :: * -> * -> *) a b c.
Graph gr =>
CFun a b c -> [Node] -> gr a b -> [Tree c]
dffWith (\ (_, n :: Node
n, nl :: DGNodeLab
nl, _) -> (Node
n, DGNodeLab
nl)) (Gr DGNodeLab DGLinkLab -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes Gr DGNodeLab DGLinkLab
dg)
    (Gr DGNodeLab DGLinkLab -> [Tree (LNode DGNodeLab)])
-> Gr DGNodeLab DGLinkLab -> [Tree (LNode DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(LEdge b -> Bool) -> gr a b -> gr a b
efilter (\ (s :: Node
s, t :: Node
t, el :: DGLinkLab
el) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
t Bool -> Bool -> Bool
&& DGLinkType -> Bool
isDefEdge (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el)) Gr DGNodeLab DGLinkLab
dg

changedPendingEdges :: DGraph -> [LEdge DGLinkLab]
changedPendingEdges :: DGraph -> [LEdge DGLinkLab]
changedPendingEdges dg :: DGraph
dg = let
  ls :: [LEdge DGLinkLab]
ls = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool)
-> (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkType -> Bool
isDefEdge) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
  (ms :: Map EdgeId (Bool, Node, Node, Set EdgeId)
ms, ps :: Set EdgeId
ps) = (LEdge DGLinkLab
 -> (Map EdgeId (Bool, Node, Node, Set EdgeId), Set EdgeId)
 -> (Map EdgeId (Bool, Node, Node, Set EdgeId), Set EdgeId))
-> (Map EdgeId (Bool, Node, Node, Set EdgeId), Set EdgeId)
-> [LEdge DGLinkLab]
-> (Map EdgeId (Bool, Node, Node, Set EdgeId), Set EdgeId)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (s :: Node
s, t :: Node
t, l :: DGLinkLab
l) (m :: Map EdgeId (Bool, Node, Node, Set EdgeId)
m, es :: Set EdgeId
es) ->
       let b :: Bool
b = DGLinkLab -> Bool
dglPending DGLinkLab
l
           e :: EdgeId
e = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l
           ty :: DGLinkType
ty = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l
       in ( EdgeId
-> (Bool, Node, Node, Set EdgeId)
-> Map EdgeId (Bool, Node, Node, Set EdgeId)
-> Map EdgeId (Bool, Node, Node, Set EdgeId)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert EdgeId
e (Bool
b, Node
s, Node
t, ProofBasis -> Set EdgeId
proofBasis (ProofBasis -> Set EdgeId) -> ProofBasis -> Set EdgeId
forall a b. (a -> b) -> a -> b
$ DGLinkType -> ProofBasis
thmProofBasis DGLinkType
ty) Map EdgeId (Bool, Node, Node, Set EdgeId)
m
          , if Bool
b Bool -> Bool -> Bool
&& DGLinkType -> Bool
isLocalEdge DGLinkType
ty then EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.insert EdgeId
e Set EdgeId
es else Set EdgeId
es))
    (Map EdgeId (Bool, Node, Node, Set EdgeId)
forall k a. Map k a
Map.empty, Set EdgeId
forall a. Set a
Set.empty) [LEdge DGLinkLab]
ls
  close :: Set EdgeId -> Set EdgeId
close known :: Set EdgeId
known =
      let nxt :: Set EdgeId
nxt = Map EdgeId (Bool, Node, Node, Set EdgeId) -> Set EdgeId
forall k a. Map k a -> Set k
Map.keysSet (Map EdgeId (Bool, Node, Node, Set EdgeId) -> Set EdgeId)
-> Map EdgeId (Bool, Node, Node, Set EdgeId) -> Set EdgeId
forall a b. (a -> b) -> a -> b
$ ((Bool, Node, Node, Set EdgeId) -> Bool)
-> Map EdgeId (Bool, Node, Node, Set EdgeId)
-> Map EdgeId (Bool, Node, Node, Set EdgeId)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter
                (\ (_, _, _, s :: Set EdgeId
s) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set EdgeId -> Bool
forall a. Set a -> Bool
Set.null (Set EdgeId -> Bool) -> Set EdgeId -> Bool
forall a b. (a -> b) -> a -> b
$ Set EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set EdgeId
s Set EdgeId
known)
                Map EdgeId (Bool, Node, Node, Set EdgeId)
ms
          new :: Set EdgeId
new = Set EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set EdgeId
nxt Set EdgeId
known
      in if Set EdgeId
new Set EdgeId -> Set EdgeId -> Bool
forall a. Eq a => a -> a -> Bool
== Set EdgeId
known then Set EdgeId
new else Set EdgeId -> Set EdgeId
close Set EdgeId
new
  aPs :: Set EdgeId
aPs = Set EdgeId -> Set EdgeId
close Set EdgeId
ps
  in (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> Bool
dglPending DGLinkLab
l Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (DGLinkLab -> EdgeId
dgl_id DGLinkLab
l) Set EdgeId
aPs) [LEdge DGLinkLab]
ls

changedLocalTheorems :: DGraph -> LNode DGNodeLab -> [LEdge DGLinkLab]
changedLocalTheorems :: DGraph -> LNode DGNodeLab -> [LEdge DGLinkLab]
changedLocalTheorems dg :: DGraph
dg (v :: Node
v, lbl :: DGNodeLab
lbl) =
  case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
    G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
      (LEdge DGLinkLab -> [LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ e :: LEdge DGLinkLab
e@(_, _, el :: DGLinkLab
el) l :: [LEdge DGLinkLab]
l ->
        let pend :: Bool
pend = DGLinkLab -> Bool
dglPending DGLinkLab
el
            psens :: Set String
psens = ThSens sentence (AnyComorphism, BasicProof) -> Set String
forall k a. Map k a -> Set k
Map.keysSet (ThSens sentence (AnyComorphism, BasicProof) -> Set String)
-> ThSens sentence (AnyComorphism, BasicProof) -> Set String
forall a b. (a -> b) -> a -> b
$ (SenStatus sentence (AnyComorphism, BasicProof) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenStatus sentence (AnyComorphism, BasicProof) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus ThSens sentence (AnyComorphism, BasicProof)
sens
        in case DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus (DGLinkType -> Maybe ThmLinkStatus)
-> DGLinkType -> Maybe ThmLinkStatus
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el of
        Just (Proven (DGRuleLocalInference nms :: [(String, String)]
nms) _) | Bool
pend
          Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Set String -> Set String -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf ([String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
nms) Set String
psens -> LEdge DGLinkLab
e LEdge DGLinkLab -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. a -> [a] -> [a]
: [LEdge DGLinkLab]
l
        _ -> [LEdge DGLinkLab]
l
         ) []
      ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool)
-> (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a b. (a -> b) -> a -> b
$ \ e :: DGLinkType
e -> DGLinkType -> Bool
isLocalEdge DGLinkType
e Bool -> Bool -> Bool
&& Bool -> Bool
not (DGLinkType -> Bool
isLocalDef DGLinkType
e))
      ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
v

duplicateDefEdges :: DGraph -> [Edge]
duplicateDefEdges :: DGraph -> [(Node, Node)]
duplicateDefEdges = [[(Node, Node)]] -> [(Node, Node)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Node, Node)]] -> [(Node, Node)])
-> (DGraph -> [[(Node, Node)]]) -> DGraph -> [(Node, Node)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ([(Node, Node)] -> Bool) -> [[(Node, Node)]] -> [[(Node, Node)]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ([(Node, Node)] -> Bool) -> [(Node, Node)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Node, Node)] -> Bool
forall a. [a] -> Bool
isSingle) ([[(Node, Node)]] -> [[(Node, Node)]])
-> (DGraph -> [[(Node, Node)]]) -> DGraph -> [[(Node, Node)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Node, Node)] -> [[(Node, Node)]]
forall a. Eq a => [a] -> [[a]]
group ([(Node, Node)] -> [[(Node, Node)]])
-> (DGraph -> [(Node, Node)]) -> DGraph -> [[(Node, Node)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LEdge DGLinkLab -> (Node, Node))
-> [LEdge DGLinkLab] -> [(Node, Node)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, t :: Node
t, _) -> (Node
s, Node
t))
  ([LEdge DGLinkLab] -> [(Node, Node)])
-> (DGraph -> [LEdge DGLinkLab]) -> DGraph -> [(Node, Node)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isDefEdge) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> (DGraph -> [LEdge DGLinkLab]) -> DGraph -> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> [LEdge DGLinkLab]
labEdgesDG

ensureUniqueNames :: DGraph -> IRI -> Int -> NodeName
ensureUniqueNames :: DGraph -> IRI -> Node -> NodeName
ensureUniqueNames dg :: DGraph
dg anIRI :: IRI
anIRI n :: Node
n = 
 let allNames :: [IRI]
allNames = (LNode DGNodeLab -> IRI) -> [LNode DGNodeLab] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map (NodeName -> IRI
getName (NodeName -> IRI)
-> (LNode DGNodeLab -> NodeName) -> LNode DGNodeLab -> IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> NodeName
dgn_name (DGNodeLab -> NodeName)
-> (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> NodeName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd) ([LNode DGNodeLab] -> [IRI]) -> [LNode DGNodeLab] -> [IRI]
forall a b. (a -> b) -> a -> b
$  DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg
     iri' :: IRI
iri' = String -> IRI -> IRI
addSuffixToIRI (Node -> String
forall a. Show a => a -> String
show Node
n) IRI
anIRI
 in if IRI
iri' IRI -> [IRI] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [IRI]
allNames 
     then DGraph -> IRI -> Node -> NodeName
ensureUniqueNames DGraph
dg IRI
anIRI (Node
n Node -> Node -> Node
forall a. Num a => a -> a -> a
+ 1) 
     else IRI -> NodeName
makeName IRI
iri'